jordan_totient_coprime_product

forall k a b u v. (forall jt_divisor_jmulcop. (exists jt_factor_jmulcopa. (a)=(jt_divisor_jmulcop)*jt_factor_jmulcopa) -> (exists jt_factor_jmulcopb. (b)=(jt_divisor_jmulcop)*jt_factor_jmulcopb) -> jt_divisor_jmulcop=1) -> (((~((k)=0)) /\ (((~((a)=0)) /\ (exists jt_codes_jmulleft jt_code_scale_jmulleft jt_scales_jmulleft jt_scale_scale_jmulleft. ((forall jt_i_jmulleftenum. (exists jt_gap_jmulleftenumsoundindex. jt_gap_jmulleftenumsoundindex+S (jt_i_jmulleftenum)=(u)) -> exists jt_b_jmulleftenum jt_c_jmulleftenum. ((((((exists fs_h_jt_jmulleftenumsoundcode. fs_h_jt_jmulleftenumsoundcode + S (jt_b_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumsoundcode. jt_codes_jmulleft = fs_q_jt_jmulleftenumsoundcode * S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft) + (jt_b_jmulleftenum))) /\ (((exists fs_h_jt_jmulleftenumsoundscale. fs_h_jt_jmulleftenumsoundscale + S (jt_c_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumsoundscale. jt_scales_jmulleft = fs_q_jt_jmulleftenumsoundscale * S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft) + (jt_c_jmulleftenum))))) /\ (((forall jt_index_jmulleftenumbound. (exists jt_gap_jmulleftenumboundindex. jt_gap_jmulleftenumboundindex+S (jt_index_jmulleftenumbound)=(k)) -> exists jt_value_jmulleftenumbound. ((((exists fs_h_jt_jmulleftenumboundat. fs_h_jt_jmulleftenumboundat + S (jt_value_jmulleftenumbound) = S ((S (jt_index_jmulleftenumbound)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumboundat. jt_b_jmulleftenum = fs_q_jt_jmulleftenumboundat * S ((S (jt_index_jmulleftenumbound)) * jt_c_jmulleftenum) + (jt_value_jmulleftenumbound))) /\ (exists jt_gap_jmulleftenumboundvalue. jt_gap_jmulleftenumboundvalue+S (jt_value_jmulleftenumbound)=(a)))) /\ (forall jt_divisor_jmulleftenumprimitive. (exists jt_factor_jmulleftenumprimitivemodulus. (a)=(jt_divisor_jmulleftenumprimitive)*jt_factor_jmulleftenumprimitivemodulus) -> (forall jt_index_jmulleftenumprimitivecoordinates jt_value_jmulleftenumprimitivecoordinates. (exists jt_gap_jmulleftenumprimitivecoordinatesindex. jt_gap_jmulleftenumprimitivecoordinatesindex+S (jt_index_jmulleftenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulleftenumprimitivecoordinatesat. fs_h_jt_jmulleftenumprimitivecoordinatesat + S (jt_value_jmulleftenumprimitivecoordinates) = S ((S (jt_index_jmulleftenumprimitivecoordinates)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumprimitivecoordinatesat. jt_b_jmulleftenum = fs_q_jt_jmulleftenumprimitivecoordinatesat * S ((S (jt_index_jmulleftenumprimitivecoordinates)) * jt_c_jmulleftenum) + (jt_value_jmulleftenumprimitivecoordinates))) -> (exists jt_factor_jmulleftenumprimitivecoordinatesdivides. (jt_value_jmulleftenumprimitivecoordinates)=(jt_divisor_jmulleftenumprimitive)*jt_factor_jmulleftenumprimitivecoordinatesdivides)) -> jt_divisor_jmulleftenumprimitive=1))))) /\ (((forall jt_b_jmulleftenum jt_c_jmulleftenum. (forall jt_index_jmulleftenuminputbound. (exists jt_gap_jmulleftenuminputboundindex. jt_gap_jmulleftenuminputboundindex+S (jt_index_jmulleftenuminputbound)=(k)) -> exists jt_value_jmulleftenuminputbound. ((((exists fs_h_jt_jmulleftenuminputboundat. fs_h_jt_jmulleftenuminputboundat + S (jt_value_jmulleftenuminputbound) = S ((S (jt_index_jmulleftenuminputbound)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenuminputboundat. jt_b_jmulleftenum = fs_q_jt_jmulleftenuminputboundat * S ((S (jt_index_jmulleftenuminputbound)) * jt_c_jmulleftenum) + (jt_value_jmulleftenuminputbound))) /\ (exists jt_gap_jmulleftenuminputboundvalue. jt_gap_jmulleftenuminputboundvalue+S (jt_value_jmulleftenuminputbound)=(a)))) -> (forall jt_divisor_jmulleftenuminputprimitive. (exists jt_factor_jmulleftenuminputprimitivemodulus. (a)=(jt_divisor_jmulleftenuminputprimitive)*jt_factor_jmulleftenuminputprimitivemodulus) -> (forall jt_index_jmulleftenuminputprimitivecoordinates jt_value_jmulleftenuminputprimitivecoordinates. (exists jt_gap_jmulleftenuminputprimitivecoordinatesindex. jt_gap_jmulleftenuminputprimitivecoordinatesindex+S (jt_index_jmulleftenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulleftenuminputprimitivecoordinatesat. fs_h_jt_jmulleftenuminputprimitivecoordinatesat + S (jt_value_jmulleftenuminputprimitivecoordinates) = S ((S (jt_index_jmulleftenuminputprimitivecoordinates)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenuminputprimitivecoordinatesat. jt_b_jmulleftenum = fs_q_jt_jmulleftenuminputprimitivecoordinatesat * S ((S (jt_index_jmulleftenuminputprimitivecoordinates)) * jt_c_jmulleftenum) + (jt_value_jmulleftenuminputprimitivecoordinates))) -> (exists jt_factor_jmulleftenuminputprimitivecoordinatesdivides. (jt_value_jmulleftenuminputprimitivecoordinates)=(jt_divisor_jmulleftenuminputprimitive)*jt_factor_jmulleftenuminputprimitivecoordinatesdivides)) -> jt_divisor_jmulleftenuminputprimitive=1) -> exists jt_i_jmulleftenum jt_d_jmulleftenum jt_e_jmulleftenum. ((exists jt_gap_jmulleftenumcompleteindex. jt_gap_jmulleftenumcompleteindex+S (jt_i_jmulleftenum)=(u)) /\ (((((((exists fs_h_jt_jmulleftenumcompletecode. fs_h_jt_jmulleftenumcompletecode + S (jt_d_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumcompletecode. jt_codes_jmulleft = fs_q_jt_jmulleftenumcompletecode * S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft) + (jt_d_jmulleftenum))) /\ (((exists fs_h_jt_jmulleftenumcompletescale. fs_h_jt_jmulleftenumcompletescale + S (jt_e_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumcompletescale. jt_scales_jmulleft = fs_q_jt_jmulleftenumcompletescale * S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft) + (jt_e_jmulleftenum))))) /\ (forall jt_index_jmulleftenumrepresented jt_left_jmulleftenumrepresented jt_right_jmulleftenumrepresented. (exists jt_gap_jmulleftenumrepresentedindex. jt_gap_jmulleftenumrepresentedindex+S (jt_index_jmulleftenumrepresented)=(k)) -> (((exists fs_h_jt_jmulleftenumrepresentedleft. fs_h_jt_jmulleftenumrepresentedleft + S (jt_left_jmulleftenumrepresented) = S ((S (jt_index_jmulleftenumrepresented)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumrepresentedleft. jt_b_jmulleftenum = fs_q_jt_jmulleftenumrepresentedleft * S ((S (jt_index_jmulleftenumrepresented)) * jt_c_jmulleftenum) + (jt_left_jmulleftenumrepresented))) -> (((exists fs_h_jt_jmulleftenumrepresentedright. fs_h_jt_jmulleftenumrepresentedright + S (jt_right_jmulleftenumrepresented) = S ((S (jt_index_jmulleftenumrepresented)) * jt_e_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumrepresentedright. jt_d_jmulleftenum = fs_q_jt_jmulleftenumrepresentedright * S ((S (jt_index_jmulleftenumrepresented)) * jt_e_jmulleftenum) + (jt_right_jmulleftenumrepresented))) -> jt_left_jmulleftenumrepresented=jt_right_jmulleftenumrepresented))))) /\ (forall jt_i_jmulleftenum jt_h_jmulleftenum jt_b_jmulleftenum jt_c_jmulleftenum jt_d_jmulleftenum jt_e_jmulleftenum. (exists jt_gap_jmulleftenumfirstindex. jt_gap_jmulleftenumfirstindex+S (jt_i_jmulleftenum)=(u)) -> (exists jt_gap_jmulleftenumsecondindex. jt_gap_jmulleftenumsecondindex+S (jt_h_jmulleftenum)=(u)) -> (((((exists fs_h_jt_jmulleftenumfirstcode. fs_h_jt_jmulleftenumfirstcode + S (jt_b_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumfirstcode. jt_codes_jmulleft = fs_q_jt_jmulleftenumfirstcode * S ((S (jt_i_jmulleftenum)) * jt_code_scale_jmulleft) + (jt_b_jmulleftenum))) /\ (((exists fs_h_jt_jmulleftenumfirstscale. fs_h_jt_jmulleftenumfirstscale + S (jt_c_jmulleftenum) = S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumfirstscale. jt_scales_jmulleft = fs_q_jt_jmulleftenumfirstscale * S ((S (jt_i_jmulleftenum)) * jt_scale_scale_jmulleft) + (jt_c_jmulleftenum))))) -> (((((exists fs_h_jt_jmulleftenumsecondcode. fs_h_jt_jmulleftenumsecondcode + S (jt_d_jmulleftenum) = S ((S (jt_h_jmulleftenum)) * jt_code_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumsecondcode. jt_codes_jmulleft = fs_q_jt_jmulleftenumsecondcode * S ((S (jt_h_jmulleftenum)) * jt_code_scale_jmulleft) + (jt_d_jmulleftenum))) /\ (((exists fs_h_jt_jmulleftenumsecondscale. fs_h_jt_jmulleftenumsecondscale + S (jt_e_jmulleftenum) = S ((S (jt_h_jmulleftenum)) * jt_scale_scale_jmulleft)) /\ exists fs_q_jt_jmulleftenumsecondscale. jt_scales_jmulleft = fs_q_jt_jmulleftenumsecondscale * S ((S (jt_h_jmulleftenum)) * jt_scale_scale_jmulleft) + (jt_e_jmulleftenum))))) -> (forall jt_index_jmulleftenumsame jt_left_jmulleftenumsame jt_right_jmulleftenumsame. (exists jt_gap_jmulleftenumsameindex. jt_gap_jmulleftenumsameindex+S (jt_index_jmulleftenumsame)=(k)) -> (((exists fs_h_jt_jmulleftenumsameleft. fs_h_jt_jmulleftenumsameleft + S (jt_left_jmulleftenumsame) = S ((S (jt_index_jmulleftenumsame)) * jt_c_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumsameleft. jt_b_jmulleftenum = fs_q_jt_jmulleftenumsameleft * S ((S (jt_index_jmulleftenumsame)) * jt_c_jmulleftenum) + (jt_left_jmulleftenumsame))) -> (((exists fs_h_jt_jmulleftenumsameright. fs_h_jt_jmulleftenumsameright + S (jt_right_jmulleftenumsame) = S ((S (jt_index_jmulleftenumsame)) * jt_e_jmulleftenum)) /\ exists fs_q_jt_jmulleftenumsameright. jt_d_jmulleftenum = fs_q_jt_jmulleftenumsameright * S ((S (jt_index_jmulleftenumsame)) * jt_e_jmulleftenum) + (jt_right_jmulleftenumsame))) -> jt_left_jmulleftenumsame=jt_right_jmulleftenumsame) -> jt_i_jmulleftenum=jt_h_jmulleftenum))))))))) -> (((~((k)=0)) /\ (((~((b)=0)) /\ (exists jt_codes_jmulright jt_code_scale_jmulright jt_scales_jmulright jt_scale_scale_jmulright. ((forall jt_i_jmulrightenum. (exists jt_gap_jmulrightenumsoundindex. jt_gap_jmulrightenumsoundindex+S (jt_i_jmulrightenum)=(v)) -> exists jt_b_jmulrightenum jt_c_jmulrightenum. ((((((exists fs_h_jt_jmulrightenumsoundcode. fs_h_jt_jmulrightenumsoundcode + S (jt_b_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumsoundcode. jt_codes_jmulright = fs_q_jt_jmulrightenumsoundcode * S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright) + (jt_b_jmulrightenum))) /\ (((exists fs_h_jt_jmulrightenumsoundscale. fs_h_jt_jmulrightenumsoundscale + S (jt_c_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumsoundscale. jt_scales_jmulright = fs_q_jt_jmulrightenumsoundscale * S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright) + (jt_c_jmulrightenum))))) /\ (((forall jt_index_jmulrightenumbound. (exists jt_gap_jmulrightenumboundindex. jt_gap_jmulrightenumboundindex+S (jt_index_jmulrightenumbound)=(k)) -> exists jt_value_jmulrightenumbound. ((((exists fs_h_jt_jmulrightenumboundat. fs_h_jt_jmulrightenumboundat + S (jt_value_jmulrightenumbound) = S ((S (jt_index_jmulrightenumbound)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumboundat. jt_b_jmulrightenum = fs_q_jt_jmulrightenumboundat * S ((S (jt_index_jmulrightenumbound)) * jt_c_jmulrightenum) + (jt_value_jmulrightenumbound))) /\ (exists jt_gap_jmulrightenumboundvalue. jt_gap_jmulrightenumboundvalue+S (jt_value_jmulrightenumbound)=(b)))) /\ (forall jt_divisor_jmulrightenumprimitive. (exists jt_factor_jmulrightenumprimitivemodulus. (b)=(jt_divisor_jmulrightenumprimitive)*jt_factor_jmulrightenumprimitivemodulus) -> (forall jt_index_jmulrightenumprimitivecoordinates jt_value_jmulrightenumprimitivecoordinates. (exists jt_gap_jmulrightenumprimitivecoordinatesindex. jt_gap_jmulrightenumprimitivecoordinatesindex+S (jt_index_jmulrightenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulrightenumprimitivecoordinatesat. fs_h_jt_jmulrightenumprimitivecoordinatesat + S (jt_value_jmulrightenumprimitivecoordinates) = S ((S (jt_index_jmulrightenumprimitivecoordinates)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumprimitivecoordinatesat. jt_b_jmulrightenum = fs_q_jt_jmulrightenumprimitivecoordinatesat * S ((S (jt_index_jmulrightenumprimitivecoordinates)) * jt_c_jmulrightenum) + (jt_value_jmulrightenumprimitivecoordinates))) -> (exists jt_factor_jmulrightenumprimitivecoordinatesdivides. (jt_value_jmulrightenumprimitivecoordinates)=(jt_divisor_jmulrightenumprimitive)*jt_factor_jmulrightenumprimitivecoordinatesdivides)) -> jt_divisor_jmulrightenumprimitive=1))))) /\ (((forall jt_b_jmulrightenum jt_c_jmulrightenum. (forall jt_index_jmulrightenuminputbound. (exists jt_gap_jmulrightenuminputboundindex. jt_gap_jmulrightenuminputboundindex+S (jt_index_jmulrightenuminputbound)=(k)) -> exists jt_value_jmulrightenuminputbound. ((((exists fs_h_jt_jmulrightenuminputboundat. fs_h_jt_jmulrightenuminputboundat + S (jt_value_jmulrightenuminputbound) = S ((S (jt_index_jmulrightenuminputbound)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenuminputboundat. jt_b_jmulrightenum = fs_q_jt_jmulrightenuminputboundat * S ((S (jt_index_jmulrightenuminputbound)) * jt_c_jmulrightenum) + (jt_value_jmulrightenuminputbound))) /\ (exists jt_gap_jmulrightenuminputboundvalue. jt_gap_jmulrightenuminputboundvalue+S (jt_value_jmulrightenuminputbound)=(b)))) -> (forall jt_divisor_jmulrightenuminputprimitive. (exists jt_factor_jmulrightenuminputprimitivemodulus. (b)=(jt_divisor_jmulrightenuminputprimitive)*jt_factor_jmulrightenuminputprimitivemodulus) -> (forall jt_index_jmulrightenuminputprimitivecoordinates jt_value_jmulrightenuminputprimitivecoordinates. (exists jt_gap_jmulrightenuminputprimitivecoordinatesindex. jt_gap_jmulrightenuminputprimitivecoordinatesindex+S (jt_index_jmulrightenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulrightenuminputprimitivecoordinatesat. fs_h_jt_jmulrightenuminputprimitivecoordinatesat + S (jt_value_jmulrightenuminputprimitivecoordinates) = S ((S (jt_index_jmulrightenuminputprimitivecoordinates)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenuminputprimitivecoordinatesat. jt_b_jmulrightenum = fs_q_jt_jmulrightenuminputprimitivecoordinatesat * S ((S (jt_index_jmulrightenuminputprimitivecoordinates)) * jt_c_jmulrightenum) + (jt_value_jmulrightenuminputprimitivecoordinates))) -> (exists jt_factor_jmulrightenuminputprimitivecoordinatesdivides. (jt_value_jmulrightenuminputprimitivecoordinates)=(jt_divisor_jmulrightenuminputprimitive)*jt_factor_jmulrightenuminputprimitivecoordinatesdivides)) -> jt_divisor_jmulrightenuminputprimitive=1) -> exists jt_i_jmulrightenum jt_d_jmulrightenum jt_e_jmulrightenum. ((exists jt_gap_jmulrightenumcompleteindex. jt_gap_jmulrightenumcompleteindex+S (jt_i_jmulrightenum)=(v)) /\ (((((((exists fs_h_jt_jmulrightenumcompletecode. fs_h_jt_jmulrightenumcompletecode + S (jt_d_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumcompletecode. jt_codes_jmulright = fs_q_jt_jmulrightenumcompletecode * S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright) + (jt_d_jmulrightenum))) /\ (((exists fs_h_jt_jmulrightenumcompletescale. fs_h_jt_jmulrightenumcompletescale + S (jt_e_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumcompletescale. jt_scales_jmulright = fs_q_jt_jmulrightenumcompletescale * S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright) + (jt_e_jmulrightenum))))) /\ (forall jt_index_jmulrightenumrepresented jt_left_jmulrightenumrepresented jt_right_jmulrightenumrepresented. (exists jt_gap_jmulrightenumrepresentedindex. jt_gap_jmulrightenumrepresentedindex+S (jt_index_jmulrightenumrepresented)=(k)) -> (((exists fs_h_jt_jmulrightenumrepresentedleft. fs_h_jt_jmulrightenumrepresentedleft + S (jt_left_jmulrightenumrepresented) = S ((S (jt_index_jmulrightenumrepresented)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumrepresentedleft. jt_b_jmulrightenum = fs_q_jt_jmulrightenumrepresentedleft * S ((S (jt_index_jmulrightenumrepresented)) * jt_c_jmulrightenum) + (jt_left_jmulrightenumrepresented))) -> (((exists fs_h_jt_jmulrightenumrepresentedright. fs_h_jt_jmulrightenumrepresentedright + S (jt_right_jmulrightenumrepresented) = S ((S (jt_index_jmulrightenumrepresented)) * jt_e_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumrepresentedright. jt_d_jmulrightenum = fs_q_jt_jmulrightenumrepresentedright * S ((S (jt_index_jmulrightenumrepresented)) * jt_e_jmulrightenum) + (jt_right_jmulrightenumrepresented))) -> jt_left_jmulrightenumrepresented=jt_right_jmulrightenumrepresented))))) /\ (forall jt_i_jmulrightenum jt_h_jmulrightenum jt_b_jmulrightenum jt_c_jmulrightenum jt_d_jmulrightenum jt_e_jmulrightenum. (exists jt_gap_jmulrightenumfirstindex. jt_gap_jmulrightenumfirstindex+S (jt_i_jmulrightenum)=(v)) -> (exists jt_gap_jmulrightenumsecondindex. jt_gap_jmulrightenumsecondindex+S (jt_h_jmulrightenum)=(v)) -> (((((exists fs_h_jt_jmulrightenumfirstcode. fs_h_jt_jmulrightenumfirstcode + S (jt_b_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumfirstcode. jt_codes_jmulright = fs_q_jt_jmulrightenumfirstcode * S ((S (jt_i_jmulrightenum)) * jt_code_scale_jmulright) + (jt_b_jmulrightenum))) /\ (((exists fs_h_jt_jmulrightenumfirstscale. fs_h_jt_jmulrightenumfirstscale + S (jt_c_jmulrightenum) = S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumfirstscale. jt_scales_jmulright = fs_q_jt_jmulrightenumfirstscale * S ((S (jt_i_jmulrightenum)) * jt_scale_scale_jmulright) + (jt_c_jmulrightenum))))) -> (((((exists fs_h_jt_jmulrightenumsecondcode. fs_h_jt_jmulrightenumsecondcode + S (jt_d_jmulrightenum) = S ((S (jt_h_jmulrightenum)) * jt_code_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumsecondcode. jt_codes_jmulright = fs_q_jt_jmulrightenumsecondcode * S ((S (jt_h_jmulrightenum)) * jt_code_scale_jmulright) + (jt_d_jmulrightenum))) /\ (((exists fs_h_jt_jmulrightenumsecondscale. fs_h_jt_jmulrightenumsecondscale + S (jt_e_jmulrightenum) = S ((S (jt_h_jmulrightenum)) * jt_scale_scale_jmulright)) /\ exists fs_q_jt_jmulrightenumsecondscale. jt_scales_jmulright = fs_q_jt_jmulrightenumsecondscale * S ((S (jt_h_jmulrightenum)) * jt_scale_scale_jmulright) + (jt_e_jmulrightenum))))) -> (forall jt_index_jmulrightenumsame jt_left_jmulrightenumsame jt_right_jmulrightenumsame. (exists jt_gap_jmulrightenumsameindex. jt_gap_jmulrightenumsameindex+S (jt_index_jmulrightenumsame)=(k)) -> (((exists fs_h_jt_jmulrightenumsameleft. fs_h_jt_jmulrightenumsameleft + S (jt_left_jmulrightenumsame) = S ((S (jt_index_jmulrightenumsame)) * jt_c_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumsameleft. jt_b_jmulrightenum = fs_q_jt_jmulrightenumsameleft * S ((S (jt_index_jmulrightenumsame)) * jt_c_jmulrightenum) + (jt_left_jmulrightenumsame))) -> (((exists fs_h_jt_jmulrightenumsameright. fs_h_jt_jmulrightenumsameright + S (jt_right_jmulrightenumsame) = S ((S (jt_index_jmulrightenumsame)) * jt_e_jmulrightenum)) /\ exists fs_q_jt_jmulrightenumsameright. jt_d_jmulrightenum = fs_q_jt_jmulrightenumsameright * S ((S (jt_index_jmulrightenumsame)) * jt_e_jmulrightenum) + (jt_right_jmulrightenumsame))) -> jt_left_jmulrightenumsame=jt_right_jmulrightenumsame) -> jt_i_jmulrightenum=jt_h_jmulrightenum))))))))) -> (((~((k)=0)) /\ (((~((a*b)=0)) /\ (exists jt_codes_jmulresult jt_code_scale_jmulresult jt_scales_jmulresult jt_scale_scale_jmulresult. ((forall jt_i_jmulresultenum. (exists jt_gap_jmulresultenumsoundindex. jt_gap_jmulresultenumsoundindex+S (jt_i_jmulresultenum)=(u*v)) -> exists jt_b_jmulresultenum jt_c_jmulresultenum. ((((((exists fs_h_jt_jmulresultenumsoundcode. fs_h_jt_jmulresultenumsoundcode + S (jt_b_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumsoundcode. jt_codes_jmulresult = fs_q_jt_jmulresultenumsoundcode * S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult) + (jt_b_jmulresultenum))) /\ (((exists fs_h_jt_jmulresultenumsoundscale. fs_h_jt_jmulresultenumsoundscale + S (jt_c_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumsoundscale. jt_scales_jmulresult = fs_q_jt_jmulresultenumsoundscale * S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult) + (jt_c_jmulresultenum))))) /\ (((forall jt_index_jmulresultenumbound. (exists jt_gap_jmulresultenumboundindex. jt_gap_jmulresultenumboundindex+S (jt_index_jmulresultenumbound)=(k)) -> exists jt_value_jmulresultenumbound. ((((exists fs_h_jt_jmulresultenumboundat. fs_h_jt_jmulresultenumboundat + S (jt_value_jmulresultenumbound) = S ((S (jt_index_jmulresultenumbound)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumboundat. jt_b_jmulresultenum = fs_q_jt_jmulresultenumboundat * S ((S (jt_index_jmulresultenumbound)) * jt_c_jmulresultenum) + (jt_value_jmulresultenumbound))) /\ (exists jt_gap_jmulresultenumboundvalue. jt_gap_jmulresultenumboundvalue+S (jt_value_jmulresultenumbound)=(a*b)))) /\ (forall jt_divisor_jmulresultenumprimitive. (exists jt_factor_jmulresultenumprimitivemodulus. (a*b)=(jt_divisor_jmulresultenumprimitive)*jt_factor_jmulresultenumprimitivemodulus) -> (forall jt_index_jmulresultenumprimitivecoordinates jt_value_jmulresultenumprimitivecoordinates. (exists jt_gap_jmulresultenumprimitivecoordinatesindex. jt_gap_jmulresultenumprimitivecoordinatesindex+S (jt_index_jmulresultenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulresultenumprimitivecoordinatesat. fs_h_jt_jmulresultenumprimitivecoordinatesat + S (jt_value_jmulresultenumprimitivecoordinates) = S ((S (jt_index_jmulresultenumprimitivecoordinates)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumprimitivecoordinatesat. jt_b_jmulresultenum = fs_q_jt_jmulresultenumprimitivecoordinatesat * S ((S (jt_index_jmulresultenumprimitivecoordinates)) * jt_c_jmulresultenum) + (jt_value_jmulresultenumprimitivecoordinates))) -> (exists jt_factor_jmulresultenumprimitivecoordinatesdivides. (jt_value_jmulresultenumprimitivecoordinates)=(jt_divisor_jmulresultenumprimitive)*jt_factor_jmulresultenumprimitivecoordinatesdivides)) -> jt_divisor_jmulresultenumprimitive=1))))) /\ (((forall jt_b_jmulresultenum jt_c_jmulresultenum. (forall jt_index_jmulresultenuminputbound. (exists jt_gap_jmulresultenuminputboundindex. jt_gap_jmulresultenuminputboundindex+S (jt_index_jmulresultenuminputbound)=(k)) -> exists jt_value_jmulresultenuminputbound. ((((exists fs_h_jt_jmulresultenuminputboundat. fs_h_jt_jmulresultenuminputboundat + S (jt_value_jmulresultenuminputbound) = S ((S (jt_index_jmulresultenuminputbound)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenuminputboundat. jt_b_jmulresultenum = fs_q_jt_jmulresultenuminputboundat * S ((S (jt_index_jmulresultenuminputbound)) * jt_c_jmulresultenum) + (jt_value_jmulresultenuminputbound))) /\ (exists jt_gap_jmulresultenuminputboundvalue. jt_gap_jmulresultenuminputboundvalue+S (jt_value_jmulresultenuminputbound)=(a*b)))) -> (forall jt_divisor_jmulresultenuminputprimitive. (exists jt_factor_jmulresultenuminputprimitivemodulus. (a*b)=(jt_divisor_jmulresultenuminputprimitive)*jt_factor_jmulresultenuminputprimitivemodulus) -> (forall jt_index_jmulresultenuminputprimitivecoordinates jt_value_jmulresultenuminputprimitivecoordinates. (exists jt_gap_jmulresultenuminputprimitivecoordinatesindex. jt_gap_jmulresultenuminputprimitivecoordinatesindex+S (jt_index_jmulresultenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jmulresultenuminputprimitivecoordinatesat. fs_h_jt_jmulresultenuminputprimitivecoordinatesat + S (jt_value_jmulresultenuminputprimitivecoordinates) = S ((S (jt_index_jmulresultenuminputprimitivecoordinates)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenuminputprimitivecoordinatesat. jt_b_jmulresultenum = fs_q_jt_jmulresultenuminputprimitivecoordinatesat * S ((S (jt_index_jmulresultenuminputprimitivecoordinates)) * jt_c_jmulresultenum) + (jt_value_jmulresultenuminputprimitivecoordinates))) -> (exists jt_factor_jmulresultenuminputprimitivecoordinatesdivides. (jt_value_jmulresultenuminputprimitivecoordinates)=(jt_divisor_jmulresultenuminputprimitive)*jt_factor_jmulresultenuminputprimitivecoordinatesdivides)) -> jt_divisor_jmulresultenuminputprimitive=1) -> exists jt_i_jmulresultenum jt_d_jmulresultenum jt_e_jmulresultenum. ((exists jt_gap_jmulresultenumcompleteindex. jt_gap_jmulresultenumcompleteindex+S (jt_i_jmulresultenum)=(u*v)) /\ (((((((exists fs_h_jt_jmulresultenumcompletecode. fs_h_jt_jmulresultenumcompletecode + S (jt_d_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumcompletecode. jt_codes_jmulresult = fs_q_jt_jmulresultenumcompletecode * S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult) + (jt_d_jmulresultenum))) /\ (((exists fs_h_jt_jmulresultenumcompletescale. fs_h_jt_jmulresultenumcompletescale + S (jt_e_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumcompletescale. jt_scales_jmulresult = fs_q_jt_jmulresultenumcompletescale * S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult) + (jt_e_jmulresultenum))))) /\ (forall jt_index_jmulresultenumrepresented jt_left_jmulresultenumrepresented jt_right_jmulresultenumrepresented. (exists jt_gap_jmulresultenumrepresentedindex. jt_gap_jmulresultenumrepresentedindex+S (jt_index_jmulresultenumrepresented)=(k)) -> (((exists fs_h_jt_jmulresultenumrepresentedleft. fs_h_jt_jmulresultenumrepresentedleft + S (jt_left_jmulresultenumrepresented) = S ((S (jt_index_jmulresultenumrepresented)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumrepresentedleft. jt_b_jmulresultenum = fs_q_jt_jmulresultenumrepresentedleft * S ((S (jt_index_jmulresultenumrepresented)) * jt_c_jmulresultenum) + (jt_left_jmulresultenumrepresented))) -> (((exists fs_h_jt_jmulresultenumrepresentedright. fs_h_jt_jmulresultenumrepresentedright + S (jt_right_jmulresultenumrepresented) = S ((S (jt_index_jmulresultenumrepresented)) * jt_e_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumrepresentedright. jt_d_jmulresultenum = fs_q_jt_jmulresultenumrepresentedright * S ((S (jt_index_jmulresultenumrepresented)) * jt_e_jmulresultenum) + (jt_right_jmulresultenumrepresented))) -> jt_left_jmulresultenumrepresented=jt_right_jmulresultenumrepresented))))) /\ (forall jt_i_jmulresultenum jt_h_jmulresultenum jt_b_jmulresultenum jt_c_jmulresultenum jt_d_jmulresultenum jt_e_jmulresultenum. (exists jt_gap_jmulresultenumfirstindex. jt_gap_jmulresultenumfirstindex+S (jt_i_jmulresultenum)=(u*v)) -> (exists jt_gap_jmulresultenumsecondindex. jt_gap_jmulresultenumsecondindex+S (jt_h_jmulresultenum)=(u*v)) -> (((((exists fs_h_jt_jmulresultenumfirstcode. fs_h_jt_jmulresultenumfirstcode + S (jt_b_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumfirstcode. jt_codes_jmulresult = fs_q_jt_jmulresultenumfirstcode * S ((S (jt_i_jmulresultenum)) * jt_code_scale_jmulresult) + (jt_b_jmulresultenum))) /\ (((exists fs_h_jt_jmulresultenumfirstscale. fs_h_jt_jmulresultenumfirstscale + S (jt_c_jmulresultenum) = S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumfirstscale. jt_scales_jmulresult = fs_q_jt_jmulresultenumfirstscale * S ((S (jt_i_jmulresultenum)) * jt_scale_scale_jmulresult) + (jt_c_jmulresultenum))))) -> (((((exists fs_h_jt_jmulresultenumsecondcode. fs_h_jt_jmulresultenumsecondcode + S (jt_d_jmulresultenum) = S ((S (jt_h_jmulresultenum)) * jt_code_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumsecondcode. jt_codes_jmulresult = fs_q_jt_jmulresultenumsecondcode * S ((S (jt_h_jmulresultenum)) * jt_code_scale_jmulresult) + (jt_d_jmulresultenum))) /\ (((exists fs_h_jt_jmulresultenumsecondscale. fs_h_jt_jmulresultenumsecondscale + S (jt_e_jmulresultenum) = S ((S (jt_h_jmulresultenum)) * jt_scale_scale_jmulresult)) /\ exists fs_q_jt_jmulresultenumsecondscale. jt_scales_jmulresult = fs_q_jt_jmulresultenumsecondscale * S ((S (jt_h_jmulresultenum)) * jt_scale_scale_jmulresult) + (jt_e_jmulresultenum))))) -> (forall jt_index_jmulresultenumsame jt_left_jmulresultenumsame jt_right_jmulresultenumsame. (exists jt_gap_jmulresultenumsameindex. jt_gap_jmulresultenumsameindex+S (jt_index_jmulresultenumsame)=(k)) -> (((exists fs_h_jt_jmulresultenumsameleft. fs_h_jt_jmulresultenumsameleft + S (jt_left_jmulresultenumsame) = S ((S (jt_index_jmulresultenumsame)) * jt_c_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumsameleft. jt_b_jmulresultenum = fs_q_jt_jmulresultenumsameleft * S ((S (jt_index_jmulresultenumsame)) * jt_c_jmulresultenum) + (jt_left_jmulresultenumsame))) -> (((exists fs_h_jt_jmulresultenumsameright. fs_h_jt_jmulresultenumsameright + S (jt_right_jmulresultenumsame) = S ((S (jt_index_jmulresultenumsame)) * jt_e_jmulresultenum)) /\ exists fs_q_jt_jmulresultenumsameright. jt_d_jmulresultenum = fs_q_jt_jmulresultenumsameright * S ((S (jt_index_jmulresultenumsame)) * jt_e_jmulresultenum) + (jt_right_jmulresultenumsame))) -> jt_left_jmulresultenumsame=jt_right_jmulresultenumsame) -> jt_i_jmulresultenum=jt_h_jmulresultenum)))))))))