jordan_totient_multiplicativity_unique_counts

forall k a b u v w. (forall jt_divisor_arbitrary_coprime. (exists jt_factor_arbitrary_coprimea. (a)=(jt_divisor_arbitrary_coprime)*jt_factor_arbitrary_coprimea) -> (exists jt_factor_arbitrary_coprimeb. (b)=(jt_divisor_arbitrary_coprime)*jt_factor_arbitrary_coprimeb) -> jt_divisor_arbitrary_coprime=1) -> (((~((k)=0)) /\ (((~((a)=0)) /\ (exists jt_codes_arbitrary_left jt_code_scale_arbitrary_left jt_scales_arbitrary_left jt_scale_scale_arbitrary_left. ((forall jt_i_arbitrary_leftenum. (exists jt_gap_arbitrary_leftenumsoundindex. jt_gap_arbitrary_leftenumsoundindex+S (jt_i_arbitrary_leftenum)=(u)) -> exists jt_b_arbitrary_leftenum jt_c_arbitrary_leftenum. ((((((exists fs_h_jt_arbitrary_leftenumsoundcode. fs_h_jt_arbitrary_leftenumsoundcode + S (jt_b_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumsoundcode. jt_codes_arbitrary_left = fs_q_jt_arbitrary_leftenumsoundcode * S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left) + (jt_b_arbitrary_leftenum))) /\ (((exists fs_h_jt_arbitrary_leftenumsoundscale. fs_h_jt_arbitrary_leftenumsoundscale + S (jt_c_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumsoundscale. jt_scales_arbitrary_left = fs_q_jt_arbitrary_leftenumsoundscale * S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left) + (jt_c_arbitrary_leftenum))))) /\ (((forall jt_index_arbitrary_leftenumbound. (exists jt_gap_arbitrary_leftenumboundindex. jt_gap_arbitrary_leftenumboundindex+S (jt_index_arbitrary_leftenumbound)=(k)) -> exists jt_value_arbitrary_leftenumbound. ((((exists fs_h_jt_arbitrary_leftenumboundat. fs_h_jt_arbitrary_leftenumboundat + S (jt_value_arbitrary_leftenumbound) = S ((S (jt_index_arbitrary_leftenumbound)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumboundat. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumboundat * S ((S (jt_index_arbitrary_leftenumbound)) * jt_c_arbitrary_leftenum) + (jt_value_arbitrary_leftenumbound))) /\ (exists jt_gap_arbitrary_leftenumboundvalue. jt_gap_arbitrary_leftenumboundvalue+S (jt_value_arbitrary_leftenumbound)=(a)))) /\ (forall jt_divisor_arbitrary_leftenumprimitive. (exists jt_factor_arbitrary_leftenumprimitivemodulus. (a)=(jt_divisor_arbitrary_leftenumprimitive)*jt_factor_arbitrary_leftenumprimitivemodulus) -> (forall jt_index_arbitrary_leftenumprimitivecoordinates jt_value_arbitrary_leftenumprimitivecoordinates. (exists jt_gap_arbitrary_leftenumprimitivecoordinatesindex. jt_gap_arbitrary_leftenumprimitivecoordinatesindex+S (jt_index_arbitrary_leftenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_leftenumprimitivecoordinatesat. fs_h_jt_arbitrary_leftenumprimitivecoordinatesat + S (jt_value_arbitrary_leftenumprimitivecoordinates) = S ((S (jt_index_arbitrary_leftenumprimitivecoordinates)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumprimitivecoordinatesat. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumprimitivecoordinatesat * S ((S (jt_index_arbitrary_leftenumprimitivecoordinates)) * jt_c_arbitrary_leftenum) + (jt_value_arbitrary_leftenumprimitivecoordinates))) -> (exists jt_factor_arbitrary_leftenumprimitivecoordinatesdivides. (jt_value_arbitrary_leftenumprimitivecoordinates)=(jt_divisor_arbitrary_leftenumprimitive)*jt_factor_arbitrary_leftenumprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_leftenumprimitive=1))))) /\ (((forall jt_b_arbitrary_leftenum jt_c_arbitrary_leftenum. (forall jt_index_arbitrary_leftenuminputbound. (exists jt_gap_arbitrary_leftenuminputboundindex. jt_gap_arbitrary_leftenuminputboundindex+S (jt_index_arbitrary_leftenuminputbound)=(k)) -> exists jt_value_arbitrary_leftenuminputbound. ((((exists fs_h_jt_arbitrary_leftenuminputboundat. fs_h_jt_arbitrary_leftenuminputboundat + S (jt_value_arbitrary_leftenuminputbound) = S ((S (jt_index_arbitrary_leftenuminputbound)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenuminputboundat. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenuminputboundat * S ((S (jt_index_arbitrary_leftenuminputbound)) * jt_c_arbitrary_leftenum) + (jt_value_arbitrary_leftenuminputbound))) /\ (exists jt_gap_arbitrary_leftenuminputboundvalue. jt_gap_arbitrary_leftenuminputboundvalue+S (jt_value_arbitrary_leftenuminputbound)=(a)))) -> (forall jt_divisor_arbitrary_leftenuminputprimitive. (exists jt_factor_arbitrary_leftenuminputprimitivemodulus. (a)=(jt_divisor_arbitrary_leftenuminputprimitive)*jt_factor_arbitrary_leftenuminputprimitivemodulus) -> (forall jt_index_arbitrary_leftenuminputprimitivecoordinates jt_value_arbitrary_leftenuminputprimitivecoordinates. (exists jt_gap_arbitrary_leftenuminputprimitivecoordinatesindex. jt_gap_arbitrary_leftenuminputprimitivecoordinatesindex+S (jt_index_arbitrary_leftenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_leftenuminputprimitivecoordinatesat. fs_h_jt_arbitrary_leftenuminputprimitivecoordinatesat + S (jt_value_arbitrary_leftenuminputprimitivecoordinates) = S ((S (jt_index_arbitrary_leftenuminputprimitivecoordinates)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenuminputprimitivecoordinatesat. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenuminputprimitivecoordinatesat * S ((S (jt_index_arbitrary_leftenuminputprimitivecoordinates)) * jt_c_arbitrary_leftenum) + (jt_value_arbitrary_leftenuminputprimitivecoordinates))) -> (exists jt_factor_arbitrary_leftenuminputprimitivecoordinatesdivides. (jt_value_arbitrary_leftenuminputprimitivecoordinates)=(jt_divisor_arbitrary_leftenuminputprimitive)*jt_factor_arbitrary_leftenuminputprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_leftenuminputprimitive=1) -> exists jt_i_arbitrary_leftenum jt_d_arbitrary_leftenum jt_e_arbitrary_leftenum. ((exists jt_gap_arbitrary_leftenumcompleteindex. jt_gap_arbitrary_leftenumcompleteindex+S (jt_i_arbitrary_leftenum)=(u)) /\ (((((((exists fs_h_jt_arbitrary_leftenumcompletecode. fs_h_jt_arbitrary_leftenumcompletecode + S (jt_d_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumcompletecode. jt_codes_arbitrary_left = fs_q_jt_arbitrary_leftenumcompletecode * S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left) + (jt_d_arbitrary_leftenum))) /\ (((exists fs_h_jt_arbitrary_leftenumcompletescale. fs_h_jt_arbitrary_leftenumcompletescale + S (jt_e_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumcompletescale. jt_scales_arbitrary_left = fs_q_jt_arbitrary_leftenumcompletescale * S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left) + (jt_e_arbitrary_leftenum))))) /\ (forall jt_index_arbitrary_leftenumrepresented jt_left_arbitrary_leftenumrepresented jt_right_arbitrary_leftenumrepresented. (exists jt_gap_arbitrary_leftenumrepresentedindex. jt_gap_arbitrary_leftenumrepresentedindex+S (jt_index_arbitrary_leftenumrepresented)=(k)) -> (((exists fs_h_jt_arbitrary_leftenumrepresentedleft. fs_h_jt_arbitrary_leftenumrepresentedleft + S (jt_left_arbitrary_leftenumrepresented) = S ((S (jt_index_arbitrary_leftenumrepresented)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumrepresentedleft. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumrepresentedleft * S ((S (jt_index_arbitrary_leftenumrepresented)) * jt_c_arbitrary_leftenum) + (jt_left_arbitrary_leftenumrepresented))) -> (((exists fs_h_jt_arbitrary_leftenumrepresentedright. fs_h_jt_arbitrary_leftenumrepresentedright + S (jt_right_arbitrary_leftenumrepresented) = S ((S (jt_index_arbitrary_leftenumrepresented)) * jt_e_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumrepresentedright. jt_d_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumrepresentedright * S ((S (jt_index_arbitrary_leftenumrepresented)) * jt_e_arbitrary_leftenum) + (jt_right_arbitrary_leftenumrepresented))) -> jt_left_arbitrary_leftenumrepresented=jt_right_arbitrary_leftenumrepresented))))) /\ (forall jt_i_arbitrary_leftenum jt_h_arbitrary_leftenum jt_b_arbitrary_leftenum jt_c_arbitrary_leftenum jt_d_arbitrary_leftenum jt_e_arbitrary_leftenum. (exists jt_gap_arbitrary_leftenumfirstindex. jt_gap_arbitrary_leftenumfirstindex+S (jt_i_arbitrary_leftenum)=(u)) -> (exists jt_gap_arbitrary_leftenumsecondindex. jt_gap_arbitrary_leftenumsecondindex+S (jt_h_arbitrary_leftenum)=(u)) -> (((((exists fs_h_jt_arbitrary_leftenumfirstcode. fs_h_jt_arbitrary_leftenumfirstcode + S (jt_b_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumfirstcode. jt_codes_arbitrary_left = fs_q_jt_arbitrary_leftenumfirstcode * S ((S (jt_i_arbitrary_leftenum)) * jt_code_scale_arbitrary_left) + (jt_b_arbitrary_leftenum))) /\ (((exists fs_h_jt_arbitrary_leftenumfirstscale. fs_h_jt_arbitrary_leftenumfirstscale + S (jt_c_arbitrary_leftenum) = S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumfirstscale. jt_scales_arbitrary_left = fs_q_jt_arbitrary_leftenumfirstscale * S ((S (jt_i_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left) + (jt_c_arbitrary_leftenum))))) -> (((((exists fs_h_jt_arbitrary_leftenumsecondcode. fs_h_jt_arbitrary_leftenumsecondcode + S (jt_d_arbitrary_leftenum) = S ((S (jt_h_arbitrary_leftenum)) * jt_code_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumsecondcode. jt_codes_arbitrary_left = fs_q_jt_arbitrary_leftenumsecondcode * S ((S (jt_h_arbitrary_leftenum)) * jt_code_scale_arbitrary_left) + (jt_d_arbitrary_leftenum))) /\ (((exists fs_h_jt_arbitrary_leftenumsecondscale. fs_h_jt_arbitrary_leftenumsecondscale + S (jt_e_arbitrary_leftenum) = S ((S (jt_h_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left)) /\ exists fs_q_jt_arbitrary_leftenumsecondscale. jt_scales_arbitrary_left = fs_q_jt_arbitrary_leftenumsecondscale * S ((S (jt_h_arbitrary_leftenum)) * jt_scale_scale_arbitrary_left) + (jt_e_arbitrary_leftenum))))) -> (forall jt_index_arbitrary_leftenumsame jt_left_arbitrary_leftenumsame jt_right_arbitrary_leftenumsame. (exists jt_gap_arbitrary_leftenumsameindex. jt_gap_arbitrary_leftenumsameindex+S (jt_index_arbitrary_leftenumsame)=(k)) -> (((exists fs_h_jt_arbitrary_leftenumsameleft. fs_h_jt_arbitrary_leftenumsameleft + S (jt_left_arbitrary_leftenumsame) = S ((S (jt_index_arbitrary_leftenumsame)) * jt_c_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumsameleft. jt_b_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumsameleft * S ((S (jt_index_arbitrary_leftenumsame)) * jt_c_arbitrary_leftenum) + (jt_left_arbitrary_leftenumsame))) -> (((exists fs_h_jt_arbitrary_leftenumsameright. fs_h_jt_arbitrary_leftenumsameright + S (jt_right_arbitrary_leftenumsame) = S ((S (jt_index_arbitrary_leftenumsame)) * jt_e_arbitrary_leftenum)) /\ exists fs_q_jt_arbitrary_leftenumsameright. jt_d_arbitrary_leftenum = fs_q_jt_arbitrary_leftenumsameright * S ((S (jt_index_arbitrary_leftenumsame)) * jt_e_arbitrary_leftenum) + (jt_right_arbitrary_leftenumsame))) -> jt_left_arbitrary_leftenumsame=jt_right_arbitrary_leftenumsame) -> jt_i_arbitrary_leftenum=jt_h_arbitrary_leftenum))))))))) -> (((~((k)=0)) /\ (((~((b)=0)) /\ (exists jt_codes_arbitrary_right jt_code_scale_arbitrary_right jt_scales_arbitrary_right jt_scale_scale_arbitrary_right. ((forall jt_i_arbitrary_rightenum. (exists jt_gap_arbitrary_rightenumsoundindex. jt_gap_arbitrary_rightenumsoundindex+S (jt_i_arbitrary_rightenum)=(v)) -> exists jt_b_arbitrary_rightenum jt_c_arbitrary_rightenum. ((((((exists fs_h_jt_arbitrary_rightenumsoundcode. fs_h_jt_arbitrary_rightenumsoundcode + S (jt_b_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumsoundcode. jt_codes_arbitrary_right = fs_q_jt_arbitrary_rightenumsoundcode * S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right) + (jt_b_arbitrary_rightenum))) /\ (((exists fs_h_jt_arbitrary_rightenumsoundscale. fs_h_jt_arbitrary_rightenumsoundscale + S (jt_c_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumsoundscale. jt_scales_arbitrary_right = fs_q_jt_arbitrary_rightenumsoundscale * S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right) + (jt_c_arbitrary_rightenum))))) /\ (((forall jt_index_arbitrary_rightenumbound. (exists jt_gap_arbitrary_rightenumboundindex. jt_gap_arbitrary_rightenumboundindex+S (jt_index_arbitrary_rightenumbound)=(k)) -> exists jt_value_arbitrary_rightenumbound. ((((exists fs_h_jt_arbitrary_rightenumboundat. fs_h_jt_arbitrary_rightenumboundat + S (jt_value_arbitrary_rightenumbound) = S ((S (jt_index_arbitrary_rightenumbound)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumboundat. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumboundat * S ((S (jt_index_arbitrary_rightenumbound)) * jt_c_arbitrary_rightenum) + (jt_value_arbitrary_rightenumbound))) /\ (exists jt_gap_arbitrary_rightenumboundvalue. jt_gap_arbitrary_rightenumboundvalue+S (jt_value_arbitrary_rightenumbound)=(b)))) /\ (forall jt_divisor_arbitrary_rightenumprimitive. (exists jt_factor_arbitrary_rightenumprimitivemodulus. (b)=(jt_divisor_arbitrary_rightenumprimitive)*jt_factor_arbitrary_rightenumprimitivemodulus) -> (forall jt_index_arbitrary_rightenumprimitivecoordinates jt_value_arbitrary_rightenumprimitivecoordinates. (exists jt_gap_arbitrary_rightenumprimitivecoordinatesindex. jt_gap_arbitrary_rightenumprimitivecoordinatesindex+S (jt_index_arbitrary_rightenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_rightenumprimitivecoordinatesat. fs_h_jt_arbitrary_rightenumprimitivecoordinatesat + S (jt_value_arbitrary_rightenumprimitivecoordinates) = S ((S (jt_index_arbitrary_rightenumprimitivecoordinates)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumprimitivecoordinatesat. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumprimitivecoordinatesat * S ((S (jt_index_arbitrary_rightenumprimitivecoordinates)) * jt_c_arbitrary_rightenum) + (jt_value_arbitrary_rightenumprimitivecoordinates))) -> (exists jt_factor_arbitrary_rightenumprimitivecoordinatesdivides. (jt_value_arbitrary_rightenumprimitivecoordinates)=(jt_divisor_arbitrary_rightenumprimitive)*jt_factor_arbitrary_rightenumprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_rightenumprimitive=1))))) /\ (((forall jt_b_arbitrary_rightenum jt_c_arbitrary_rightenum. (forall jt_index_arbitrary_rightenuminputbound. (exists jt_gap_arbitrary_rightenuminputboundindex. jt_gap_arbitrary_rightenuminputboundindex+S (jt_index_arbitrary_rightenuminputbound)=(k)) -> exists jt_value_arbitrary_rightenuminputbound. ((((exists fs_h_jt_arbitrary_rightenuminputboundat. fs_h_jt_arbitrary_rightenuminputboundat + S (jt_value_arbitrary_rightenuminputbound) = S ((S (jt_index_arbitrary_rightenuminputbound)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenuminputboundat. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenuminputboundat * S ((S (jt_index_arbitrary_rightenuminputbound)) * jt_c_arbitrary_rightenum) + (jt_value_arbitrary_rightenuminputbound))) /\ (exists jt_gap_arbitrary_rightenuminputboundvalue. jt_gap_arbitrary_rightenuminputboundvalue+S (jt_value_arbitrary_rightenuminputbound)=(b)))) -> (forall jt_divisor_arbitrary_rightenuminputprimitive. (exists jt_factor_arbitrary_rightenuminputprimitivemodulus. (b)=(jt_divisor_arbitrary_rightenuminputprimitive)*jt_factor_arbitrary_rightenuminputprimitivemodulus) -> (forall jt_index_arbitrary_rightenuminputprimitivecoordinates jt_value_arbitrary_rightenuminputprimitivecoordinates. (exists jt_gap_arbitrary_rightenuminputprimitivecoordinatesindex. jt_gap_arbitrary_rightenuminputprimitivecoordinatesindex+S (jt_index_arbitrary_rightenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_rightenuminputprimitivecoordinatesat. fs_h_jt_arbitrary_rightenuminputprimitivecoordinatesat + S (jt_value_arbitrary_rightenuminputprimitivecoordinates) = S ((S (jt_index_arbitrary_rightenuminputprimitivecoordinates)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenuminputprimitivecoordinatesat. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenuminputprimitivecoordinatesat * S ((S (jt_index_arbitrary_rightenuminputprimitivecoordinates)) * jt_c_arbitrary_rightenum) + (jt_value_arbitrary_rightenuminputprimitivecoordinates))) -> (exists jt_factor_arbitrary_rightenuminputprimitivecoordinatesdivides. (jt_value_arbitrary_rightenuminputprimitivecoordinates)=(jt_divisor_arbitrary_rightenuminputprimitive)*jt_factor_arbitrary_rightenuminputprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_rightenuminputprimitive=1) -> exists jt_i_arbitrary_rightenum jt_d_arbitrary_rightenum jt_e_arbitrary_rightenum. ((exists jt_gap_arbitrary_rightenumcompleteindex. jt_gap_arbitrary_rightenumcompleteindex+S (jt_i_arbitrary_rightenum)=(v)) /\ (((((((exists fs_h_jt_arbitrary_rightenumcompletecode. fs_h_jt_arbitrary_rightenumcompletecode + S (jt_d_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumcompletecode. jt_codes_arbitrary_right = fs_q_jt_arbitrary_rightenumcompletecode * S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right) + (jt_d_arbitrary_rightenum))) /\ (((exists fs_h_jt_arbitrary_rightenumcompletescale. fs_h_jt_arbitrary_rightenumcompletescale + S (jt_e_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumcompletescale. jt_scales_arbitrary_right = fs_q_jt_arbitrary_rightenumcompletescale * S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right) + (jt_e_arbitrary_rightenum))))) /\ (forall jt_index_arbitrary_rightenumrepresented jt_left_arbitrary_rightenumrepresented jt_right_arbitrary_rightenumrepresented. (exists jt_gap_arbitrary_rightenumrepresentedindex. jt_gap_arbitrary_rightenumrepresentedindex+S (jt_index_arbitrary_rightenumrepresented)=(k)) -> (((exists fs_h_jt_arbitrary_rightenumrepresentedleft. fs_h_jt_arbitrary_rightenumrepresentedleft + S (jt_left_arbitrary_rightenumrepresented) = S ((S (jt_index_arbitrary_rightenumrepresented)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumrepresentedleft. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumrepresentedleft * S ((S (jt_index_arbitrary_rightenumrepresented)) * jt_c_arbitrary_rightenum) + (jt_left_arbitrary_rightenumrepresented))) -> (((exists fs_h_jt_arbitrary_rightenumrepresentedright. fs_h_jt_arbitrary_rightenumrepresentedright + S (jt_right_arbitrary_rightenumrepresented) = S ((S (jt_index_arbitrary_rightenumrepresented)) * jt_e_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumrepresentedright. jt_d_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumrepresentedright * S ((S (jt_index_arbitrary_rightenumrepresented)) * jt_e_arbitrary_rightenum) + (jt_right_arbitrary_rightenumrepresented))) -> jt_left_arbitrary_rightenumrepresented=jt_right_arbitrary_rightenumrepresented))))) /\ (forall jt_i_arbitrary_rightenum jt_h_arbitrary_rightenum jt_b_arbitrary_rightenum jt_c_arbitrary_rightenum jt_d_arbitrary_rightenum jt_e_arbitrary_rightenum. (exists jt_gap_arbitrary_rightenumfirstindex. jt_gap_arbitrary_rightenumfirstindex+S (jt_i_arbitrary_rightenum)=(v)) -> (exists jt_gap_arbitrary_rightenumsecondindex. jt_gap_arbitrary_rightenumsecondindex+S (jt_h_arbitrary_rightenum)=(v)) -> (((((exists fs_h_jt_arbitrary_rightenumfirstcode. fs_h_jt_arbitrary_rightenumfirstcode + S (jt_b_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumfirstcode. jt_codes_arbitrary_right = fs_q_jt_arbitrary_rightenumfirstcode * S ((S (jt_i_arbitrary_rightenum)) * jt_code_scale_arbitrary_right) + (jt_b_arbitrary_rightenum))) /\ (((exists fs_h_jt_arbitrary_rightenumfirstscale. fs_h_jt_arbitrary_rightenumfirstscale + S (jt_c_arbitrary_rightenum) = S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumfirstscale. jt_scales_arbitrary_right = fs_q_jt_arbitrary_rightenumfirstscale * S ((S (jt_i_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right) + (jt_c_arbitrary_rightenum))))) -> (((((exists fs_h_jt_arbitrary_rightenumsecondcode. fs_h_jt_arbitrary_rightenumsecondcode + S (jt_d_arbitrary_rightenum) = S ((S (jt_h_arbitrary_rightenum)) * jt_code_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumsecondcode. jt_codes_arbitrary_right = fs_q_jt_arbitrary_rightenumsecondcode * S ((S (jt_h_arbitrary_rightenum)) * jt_code_scale_arbitrary_right) + (jt_d_arbitrary_rightenum))) /\ (((exists fs_h_jt_arbitrary_rightenumsecondscale. fs_h_jt_arbitrary_rightenumsecondscale + S (jt_e_arbitrary_rightenum) = S ((S (jt_h_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right)) /\ exists fs_q_jt_arbitrary_rightenumsecondscale. jt_scales_arbitrary_right = fs_q_jt_arbitrary_rightenumsecondscale * S ((S (jt_h_arbitrary_rightenum)) * jt_scale_scale_arbitrary_right) + (jt_e_arbitrary_rightenum))))) -> (forall jt_index_arbitrary_rightenumsame jt_left_arbitrary_rightenumsame jt_right_arbitrary_rightenumsame. (exists jt_gap_arbitrary_rightenumsameindex. jt_gap_arbitrary_rightenumsameindex+S (jt_index_arbitrary_rightenumsame)=(k)) -> (((exists fs_h_jt_arbitrary_rightenumsameleft. fs_h_jt_arbitrary_rightenumsameleft + S (jt_left_arbitrary_rightenumsame) = S ((S (jt_index_arbitrary_rightenumsame)) * jt_c_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumsameleft. jt_b_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumsameleft * S ((S (jt_index_arbitrary_rightenumsame)) * jt_c_arbitrary_rightenum) + (jt_left_arbitrary_rightenumsame))) -> (((exists fs_h_jt_arbitrary_rightenumsameright. fs_h_jt_arbitrary_rightenumsameright + S (jt_right_arbitrary_rightenumsame) = S ((S (jt_index_arbitrary_rightenumsame)) * jt_e_arbitrary_rightenum)) /\ exists fs_q_jt_arbitrary_rightenumsameright. jt_d_arbitrary_rightenum = fs_q_jt_arbitrary_rightenumsameright * S ((S (jt_index_arbitrary_rightenumsame)) * jt_e_arbitrary_rightenum) + (jt_right_arbitrary_rightenumsame))) -> jt_left_arbitrary_rightenumsame=jt_right_arbitrary_rightenumsame) -> jt_i_arbitrary_rightenum=jt_h_arbitrary_rightenum))))))))) -> (((~((k)=0)) /\ (((~((a*b)=0)) /\ (exists jt_codes_arbitrary_product jt_code_scale_arbitrary_product jt_scales_arbitrary_product jt_scale_scale_arbitrary_product. ((forall jt_i_arbitrary_productenum. (exists jt_gap_arbitrary_productenumsoundindex. jt_gap_arbitrary_productenumsoundindex+S (jt_i_arbitrary_productenum)=(w)) -> exists jt_b_arbitrary_productenum jt_c_arbitrary_productenum. ((((((exists fs_h_jt_arbitrary_productenumsoundcode. fs_h_jt_arbitrary_productenumsoundcode + S (jt_b_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumsoundcode. jt_codes_arbitrary_product = fs_q_jt_arbitrary_productenumsoundcode * S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product) + (jt_b_arbitrary_productenum))) /\ (((exists fs_h_jt_arbitrary_productenumsoundscale. fs_h_jt_arbitrary_productenumsoundscale + S (jt_c_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumsoundscale. jt_scales_arbitrary_product = fs_q_jt_arbitrary_productenumsoundscale * S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product) + (jt_c_arbitrary_productenum))))) /\ (((forall jt_index_arbitrary_productenumbound. (exists jt_gap_arbitrary_productenumboundindex. jt_gap_arbitrary_productenumboundindex+S (jt_index_arbitrary_productenumbound)=(k)) -> exists jt_value_arbitrary_productenumbound. ((((exists fs_h_jt_arbitrary_productenumboundat. fs_h_jt_arbitrary_productenumboundat + S (jt_value_arbitrary_productenumbound) = S ((S (jt_index_arbitrary_productenumbound)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumboundat. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenumboundat * S ((S (jt_index_arbitrary_productenumbound)) * jt_c_arbitrary_productenum) + (jt_value_arbitrary_productenumbound))) /\ (exists jt_gap_arbitrary_productenumboundvalue. jt_gap_arbitrary_productenumboundvalue+S (jt_value_arbitrary_productenumbound)=(a*b)))) /\ (forall jt_divisor_arbitrary_productenumprimitive. (exists jt_factor_arbitrary_productenumprimitivemodulus. (a*b)=(jt_divisor_arbitrary_productenumprimitive)*jt_factor_arbitrary_productenumprimitivemodulus) -> (forall jt_index_arbitrary_productenumprimitivecoordinates jt_value_arbitrary_productenumprimitivecoordinates. (exists jt_gap_arbitrary_productenumprimitivecoordinatesindex. jt_gap_arbitrary_productenumprimitivecoordinatesindex+S (jt_index_arbitrary_productenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_productenumprimitivecoordinatesat. fs_h_jt_arbitrary_productenumprimitivecoordinatesat + S (jt_value_arbitrary_productenumprimitivecoordinates) = S ((S (jt_index_arbitrary_productenumprimitivecoordinates)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumprimitivecoordinatesat. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenumprimitivecoordinatesat * S ((S (jt_index_arbitrary_productenumprimitivecoordinates)) * jt_c_arbitrary_productenum) + (jt_value_arbitrary_productenumprimitivecoordinates))) -> (exists jt_factor_arbitrary_productenumprimitivecoordinatesdivides. (jt_value_arbitrary_productenumprimitivecoordinates)=(jt_divisor_arbitrary_productenumprimitive)*jt_factor_arbitrary_productenumprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_productenumprimitive=1))))) /\ (((forall jt_b_arbitrary_productenum jt_c_arbitrary_productenum. (forall jt_index_arbitrary_productenuminputbound. (exists jt_gap_arbitrary_productenuminputboundindex. jt_gap_arbitrary_productenuminputboundindex+S (jt_index_arbitrary_productenuminputbound)=(k)) -> exists jt_value_arbitrary_productenuminputbound. ((((exists fs_h_jt_arbitrary_productenuminputboundat. fs_h_jt_arbitrary_productenuminputboundat + S (jt_value_arbitrary_productenuminputbound) = S ((S (jt_index_arbitrary_productenuminputbound)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenuminputboundat. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenuminputboundat * S ((S (jt_index_arbitrary_productenuminputbound)) * jt_c_arbitrary_productenum) + (jt_value_arbitrary_productenuminputbound))) /\ (exists jt_gap_arbitrary_productenuminputboundvalue. jt_gap_arbitrary_productenuminputboundvalue+S (jt_value_arbitrary_productenuminputbound)=(a*b)))) -> (forall jt_divisor_arbitrary_productenuminputprimitive. (exists jt_factor_arbitrary_productenuminputprimitivemodulus. (a*b)=(jt_divisor_arbitrary_productenuminputprimitive)*jt_factor_arbitrary_productenuminputprimitivemodulus) -> (forall jt_index_arbitrary_productenuminputprimitivecoordinates jt_value_arbitrary_productenuminputprimitivecoordinates. (exists jt_gap_arbitrary_productenuminputprimitivecoordinatesindex. jt_gap_arbitrary_productenuminputprimitivecoordinatesindex+S (jt_index_arbitrary_productenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_arbitrary_productenuminputprimitivecoordinatesat. fs_h_jt_arbitrary_productenuminputprimitivecoordinatesat + S (jt_value_arbitrary_productenuminputprimitivecoordinates) = S ((S (jt_index_arbitrary_productenuminputprimitivecoordinates)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenuminputprimitivecoordinatesat. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenuminputprimitivecoordinatesat * S ((S (jt_index_arbitrary_productenuminputprimitivecoordinates)) * jt_c_arbitrary_productenum) + (jt_value_arbitrary_productenuminputprimitivecoordinates))) -> (exists jt_factor_arbitrary_productenuminputprimitivecoordinatesdivides. (jt_value_arbitrary_productenuminputprimitivecoordinates)=(jt_divisor_arbitrary_productenuminputprimitive)*jt_factor_arbitrary_productenuminputprimitivecoordinatesdivides)) -> jt_divisor_arbitrary_productenuminputprimitive=1) -> exists jt_i_arbitrary_productenum jt_d_arbitrary_productenum jt_e_arbitrary_productenum. ((exists jt_gap_arbitrary_productenumcompleteindex. jt_gap_arbitrary_productenumcompleteindex+S (jt_i_arbitrary_productenum)=(w)) /\ (((((((exists fs_h_jt_arbitrary_productenumcompletecode. fs_h_jt_arbitrary_productenumcompletecode + S (jt_d_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumcompletecode. jt_codes_arbitrary_product = fs_q_jt_arbitrary_productenumcompletecode * S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product) + (jt_d_arbitrary_productenum))) /\ (((exists fs_h_jt_arbitrary_productenumcompletescale. fs_h_jt_arbitrary_productenumcompletescale + S (jt_e_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumcompletescale. jt_scales_arbitrary_product = fs_q_jt_arbitrary_productenumcompletescale * S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product) + (jt_e_arbitrary_productenum))))) /\ (forall jt_index_arbitrary_productenumrepresented jt_left_arbitrary_productenumrepresented jt_right_arbitrary_productenumrepresented. (exists jt_gap_arbitrary_productenumrepresentedindex. jt_gap_arbitrary_productenumrepresentedindex+S (jt_index_arbitrary_productenumrepresented)=(k)) -> (((exists fs_h_jt_arbitrary_productenumrepresentedleft. fs_h_jt_arbitrary_productenumrepresentedleft + S (jt_left_arbitrary_productenumrepresented) = S ((S (jt_index_arbitrary_productenumrepresented)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumrepresentedleft. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenumrepresentedleft * S ((S (jt_index_arbitrary_productenumrepresented)) * jt_c_arbitrary_productenum) + (jt_left_arbitrary_productenumrepresented))) -> (((exists fs_h_jt_arbitrary_productenumrepresentedright. fs_h_jt_arbitrary_productenumrepresentedright + S (jt_right_arbitrary_productenumrepresented) = S ((S (jt_index_arbitrary_productenumrepresented)) * jt_e_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumrepresentedright. jt_d_arbitrary_productenum = fs_q_jt_arbitrary_productenumrepresentedright * S ((S (jt_index_arbitrary_productenumrepresented)) * jt_e_arbitrary_productenum) + (jt_right_arbitrary_productenumrepresented))) -> jt_left_arbitrary_productenumrepresented=jt_right_arbitrary_productenumrepresented))))) /\ (forall jt_i_arbitrary_productenum jt_h_arbitrary_productenum jt_b_arbitrary_productenum jt_c_arbitrary_productenum jt_d_arbitrary_productenum jt_e_arbitrary_productenum. (exists jt_gap_arbitrary_productenumfirstindex. jt_gap_arbitrary_productenumfirstindex+S (jt_i_arbitrary_productenum)=(w)) -> (exists jt_gap_arbitrary_productenumsecondindex. jt_gap_arbitrary_productenumsecondindex+S (jt_h_arbitrary_productenum)=(w)) -> (((((exists fs_h_jt_arbitrary_productenumfirstcode. fs_h_jt_arbitrary_productenumfirstcode + S (jt_b_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumfirstcode. jt_codes_arbitrary_product = fs_q_jt_arbitrary_productenumfirstcode * S ((S (jt_i_arbitrary_productenum)) * jt_code_scale_arbitrary_product) + (jt_b_arbitrary_productenum))) /\ (((exists fs_h_jt_arbitrary_productenumfirstscale. fs_h_jt_arbitrary_productenumfirstscale + S (jt_c_arbitrary_productenum) = S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumfirstscale. jt_scales_arbitrary_product = fs_q_jt_arbitrary_productenumfirstscale * S ((S (jt_i_arbitrary_productenum)) * jt_scale_scale_arbitrary_product) + (jt_c_arbitrary_productenum))))) -> (((((exists fs_h_jt_arbitrary_productenumsecondcode. fs_h_jt_arbitrary_productenumsecondcode + S (jt_d_arbitrary_productenum) = S ((S (jt_h_arbitrary_productenum)) * jt_code_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumsecondcode. jt_codes_arbitrary_product = fs_q_jt_arbitrary_productenumsecondcode * S ((S (jt_h_arbitrary_productenum)) * jt_code_scale_arbitrary_product) + (jt_d_arbitrary_productenum))) /\ (((exists fs_h_jt_arbitrary_productenumsecondscale. fs_h_jt_arbitrary_productenumsecondscale + S (jt_e_arbitrary_productenum) = S ((S (jt_h_arbitrary_productenum)) * jt_scale_scale_arbitrary_product)) /\ exists fs_q_jt_arbitrary_productenumsecondscale. jt_scales_arbitrary_product = fs_q_jt_arbitrary_productenumsecondscale * S ((S (jt_h_arbitrary_productenum)) * jt_scale_scale_arbitrary_product) + (jt_e_arbitrary_productenum))))) -> (forall jt_index_arbitrary_productenumsame jt_left_arbitrary_productenumsame jt_right_arbitrary_productenumsame. (exists jt_gap_arbitrary_productenumsameindex. jt_gap_arbitrary_productenumsameindex+S (jt_index_arbitrary_productenumsame)=(k)) -> (((exists fs_h_jt_arbitrary_productenumsameleft. fs_h_jt_arbitrary_productenumsameleft + S (jt_left_arbitrary_productenumsame) = S ((S (jt_index_arbitrary_productenumsame)) * jt_c_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumsameleft. jt_b_arbitrary_productenum = fs_q_jt_arbitrary_productenumsameleft * S ((S (jt_index_arbitrary_productenumsame)) * jt_c_arbitrary_productenum) + (jt_left_arbitrary_productenumsame))) -> (((exists fs_h_jt_arbitrary_productenumsameright. fs_h_jt_arbitrary_productenumsameright + S (jt_right_arbitrary_productenumsame) = S ((S (jt_index_arbitrary_productenumsame)) * jt_e_arbitrary_productenum)) /\ exists fs_q_jt_arbitrary_productenumsameright. jt_d_arbitrary_productenum = fs_q_jt_arbitrary_productenumsameright * S ((S (jt_index_arbitrary_productenumsame)) * jt_e_arbitrary_productenum) + (jt_right_arbitrary_productenumsame))) -> jt_left_arbitrary_productenumsame=jt_right_arbitrary_productenumsame) -> jt_i_arbitrary_productenum=jt_h_arbitrary_productenum))))))))) -> (w=u*v)