jordan_totient_multiplicativity_exists

Exact expanded first-order arithmetic statement

forall k a b. ~(k=0) -> ~(a=0) -> ~(b=0) -> (forall jt_divisor_jendpointcop. (exists jt_factor_jendpointcopa. (a)=(jt_divisor_jendpointcop)*jt_factor_jendpointcopa) -> (exists jt_factor_jendpointcopb. (b)=(jt_divisor_jendpointcop)*jt_factor_jendpointcopb) -> jt_divisor_jendpointcop=1) -> exists u v w. ((((~((k)=0)) /\ (((~((a)=0)) /\ (exists jt_codes_jendpointleft jt_code_scale_jendpointleft jt_scales_jendpointleft jt_scale_scale_jendpointleft. ((forall jt_i_jendpointleftenum. (exists jt_gap_jendpointleftenumsoundindex. jt_gap_jendpointleftenumsoundindex+S (jt_i_jendpointleftenum)=(u)) -> exists jt_b_jendpointleftenum jt_c_jendpointleftenum. ((((((exists fs_h_jt_jendpointleftenumsoundcode. fs_h_jt_jendpointleftenumsoundcode + S (jt_b_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumsoundcode. jt_codes_jendpointleft = fs_q_jt_jendpointleftenumsoundcode * S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft) + (jt_b_jendpointleftenum))) /\ (((exists fs_h_jt_jendpointleftenumsoundscale. fs_h_jt_jendpointleftenumsoundscale + S (jt_c_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumsoundscale. jt_scales_jendpointleft = fs_q_jt_jendpointleftenumsoundscale * S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft) + (jt_c_jendpointleftenum))))) /\ (((forall jt_index_jendpointleftenumbound. (exists jt_gap_jendpointleftenumboundindex. jt_gap_jendpointleftenumboundindex+S (jt_index_jendpointleftenumbound)=(k)) -> exists jt_value_jendpointleftenumbound. ((((exists fs_h_jt_jendpointleftenumboundat. fs_h_jt_jendpointleftenumboundat + S (jt_value_jendpointleftenumbound) = S ((S (jt_index_jendpointleftenumbound)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumboundat. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenumboundat * S ((S (jt_index_jendpointleftenumbound)) * jt_c_jendpointleftenum) + (jt_value_jendpointleftenumbound))) /\ (exists jt_gap_jendpointleftenumboundvalue. jt_gap_jendpointleftenumboundvalue+S (jt_value_jendpointleftenumbound)=(a)))) /\ (forall jt_divisor_jendpointleftenumprimitive. (exists jt_factor_jendpointleftenumprimitivemodulus. (a)=(jt_divisor_jendpointleftenumprimitive)*jt_factor_jendpointleftenumprimitivemodulus) -> (forall jt_index_jendpointleftenumprimitivecoordinates jt_value_jendpointleftenumprimitivecoordinates. (exists jt_gap_jendpointleftenumprimitivecoordinatesindex. jt_gap_jendpointleftenumprimitivecoordinatesindex+S (jt_index_jendpointleftenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointleftenumprimitivecoordinatesat. fs_h_jt_jendpointleftenumprimitivecoordinatesat + S (jt_value_jendpointleftenumprimitivecoordinates) = S ((S (jt_index_jendpointleftenumprimitivecoordinates)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumprimitivecoordinatesat. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenumprimitivecoordinatesat * S ((S (jt_index_jendpointleftenumprimitivecoordinates)) * jt_c_jendpointleftenum) + (jt_value_jendpointleftenumprimitivecoordinates))) -> (exists jt_factor_jendpointleftenumprimitivecoordinatesdivides. (jt_value_jendpointleftenumprimitivecoordinates)=(jt_divisor_jendpointleftenumprimitive)*jt_factor_jendpointleftenumprimitivecoordinatesdivides)) -> jt_divisor_jendpointleftenumprimitive=1))))) /\ (((forall jt_b_jendpointleftenum jt_c_jendpointleftenum. (forall jt_index_jendpointleftenuminputbound. (exists jt_gap_jendpointleftenuminputboundindex. jt_gap_jendpointleftenuminputboundindex+S (jt_index_jendpointleftenuminputbound)=(k)) -> exists jt_value_jendpointleftenuminputbound. ((((exists fs_h_jt_jendpointleftenuminputboundat. fs_h_jt_jendpointleftenuminputboundat + S (jt_value_jendpointleftenuminputbound) = S ((S (jt_index_jendpointleftenuminputbound)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenuminputboundat. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenuminputboundat * S ((S (jt_index_jendpointleftenuminputbound)) * jt_c_jendpointleftenum) + (jt_value_jendpointleftenuminputbound))) /\ (exists jt_gap_jendpointleftenuminputboundvalue. jt_gap_jendpointleftenuminputboundvalue+S (jt_value_jendpointleftenuminputbound)=(a)))) -> (forall jt_divisor_jendpointleftenuminputprimitive. (exists jt_factor_jendpointleftenuminputprimitivemodulus. (a)=(jt_divisor_jendpointleftenuminputprimitive)*jt_factor_jendpointleftenuminputprimitivemodulus) -> (forall jt_index_jendpointleftenuminputprimitivecoordinates jt_value_jendpointleftenuminputprimitivecoordinates. (exists jt_gap_jendpointleftenuminputprimitivecoordinatesindex. jt_gap_jendpointleftenuminputprimitivecoordinatesindex+S (jt_index_jendpointleftenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointleftenuminputprimitivecoordinatesat. fs_h_jt_jendpointleftenuminputprimitivecoordinatesat + S (jt_value_jendpointleftenuminputprimitivecoordinates) = S ((S (jt_index_jendpointleftenuminputprimitivecoordinates)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenuminputprimitivecoordinatesat. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenuminputprimitivecoordinatesat * S ((S (jt_index_jendpointleftenuminputprimitivecoordinates)) * jt_c_jendpointleftenum) + (jt_value_jendpointleftenuminputprimitivecoordinates))) -> (exists jt_factor_jendpointleftenuminputprimitivecoordinatesdivides. (jt_value_jendpointleftenuminputprimitivecoordinates)=(jt_divisor_jendpointleftenuminputprimitive)*jt_factor_jendpointleftenuminputprimitivecoordinatesdivides)) -> jt_divisor_jendpointleftenuminputprimitive=1) -> exists jt_i_jendpointleftenum jt_d_jendpointleftenum jt_e_jendpointleftenum. ((exists jt_gap_jendpointleftenumcompleteindex. jt_gap_jendpointleftenumcompleteindex+S (jt_i_jendpointleftenum)=(u)) /\ (((((((exists fs_h_jt_jendpointleftenumcompletecode. fs_h_jt_jendpointleftenumcompletecode + S (jt_d_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumcompletecode. jt_codes_jendpointleft = fs_q_jt_jendpointleftenumcompletecode * S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft) + (jt_d_jendpointleftenum))) /\ (((exists fs_h_jt_jendpointleftenumcompletescale. fs_h_jt_jendpointleftenumcompletescale + S (jt_e_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumcompletescale. jt_scales_jendpointleft = fs_q_jt_jendpointleftenumcompletescale * S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft) + (jt_e_jendpointleftenum))))) /\ (forall jt_index_jendpointleftenumrepresented jt_left_jendpointleftenumrepresented jt_right_jendpointleftenumrepresented. (exists jt_gap_jendpointleftenumrepresentedindex. jt_gap_jendpointleftenumrepresentedindex+S (jt_index_jendpointleftenumrepresented)=(k)) -> (((exists fs_h_jt_jendpointleftenumrepresentedleft. fs_h_jt_jendpointleftenumrepresentedleft + S (jt_left_jendpointleftenumrepresented) = S ((S (jt_index_jendpointleftenumrepresented)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumrepresentedleft. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenumrepresentedleft * S ((S (jt_index_jendpointleftenumrepresented)) * jt_c_jendpointleftenum) + (jt_left_jendpointleftenumrepresented))) -> (((exists fs_h_jt_jendpointleftenumrepresentedright. fs_h_jt_jendpointleftenumrepresentedright + S (jt_right_jendpointleftenumrepresented) = S ((S (jt_index_jendpointleftenumrepresented)) * jt_e_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumrepresentedright. jt_d_jendpointleftenum = fs_q_jt_jendpointleftenumrepresentedright * S ((S (jt_index_jendpointleftenumrepresented)) * jt_e_jendpointleftenum) + (jt_right_jendpointleftenumrepresented))) -> jt_left_jendpointleftenumrepresented=jt_right_jendpointleftenumrepresented))))) /\ (forall jt_i_jendpointleftenum jt_h_jendpointleftenum jt_b_jendpointleftenum jt_c_jendpointleftenum jt_d_jendpointleftenum jt_e_jendpointleftenum. (exists jt_gap_jendpointleftenumfirstindex. jt_gap_jendpointleftenumfirstindex+S (jt_i_jendpointleftenum)=(u)) -> (exists jt_gap_jendpointleftenumsecondindex. jt_gap_jendpointleftenumsecondindex+S (jt_h_jendpointleftenum)=(u)) -> (((((exists fs_h_jt_jendpointleftenumfirstcode. fs_h_jt_jendpointleftenumfirstcode + S (jt_b_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumfirstcode. jt_codes_jendpointleft = fs_q_jt_jendpointleftenumfirstcode * S ((S (jt_i_jendpointleftenum)) * jt_code_scale_jendpointleft) + (jt_b_jendpointleftenum))) /\ (((exists fs_h_jt_jendpointleftenumfirstscale. fs_h_jt_jendpointleftenumfirstscale + S (jt_c_jendpointleftenum) = S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumfirstscale. jt_scales_jendpointleft = fs_q_jt_jendpointleftenumfirstscale * S ((S (jt_i_jendpointleftenum)) * jt_scale_scale_jendpointleft) + (jt_c_jendpointleftenum))))) -> (((((exists fs_h_jt_jendpointleftenumsecondcode. fs_h_jt_jendpointleftenumsecondcode + S (jt_d_jendpointleftenum) = S ((S (jt_h_jendpointleftenum)) * jt_code_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumsecondcode. jt_codes_jendpointleft = fs_q_jt_jendpointleftenumsecondcode * S ((S (jt_h_jendpointleftenum)) * jt_code_scale_jendpointleft) + (jt_d_jendpointleftenum))) /\ (((exists fs_h_jt_jendpointleftenumsecondscale. fs_h_jt_jendpointleftenumsecondscale + S (jt_e_jendpointleftenum) = S ((S (jt_h_jendpointleftenum)) * jt_scale_scale_jendpointleft)) /\ exists fs_q_jt_jendpointleftenumsecondscale. jt_scales_jendpointleft = fs_q_jt_jendpointleftenumsecondscale * S ((S (jt_h_jendpointleftenum)) * jt_scale_scale_jendpointleft) + (jt_e_jendpointleftenum))))) -> (forall jt_index_jendpointleftenumsame jt_left_jendpointleftenumsame jt_right_jendpointleftenumsame. (exists jt_gap_jendpointleftenumsameindex. jt_gap_jendpointleftenumsameindex+S (jt_index_jendpointleftenumsame)=(k)) -> (((exists fs_h_jt_jendpointleftenumsameleft. fs_h_jt_jendpointleftenumsameleft + S (jt_left_jendpointleftenumsame) = S ((S (jt_index_jendpointleftenumsame)) * jt_c_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumsameleft. jt_b_jendpointleftenum = fs_q_jt_jendpointleftenumsameleft * S ((S (jt_index_jendpointleftenumsame)) * jt_c_jendpointleftenum) + (jt_left_jendpointleftenumsame))) -> (((exists fs_h_jt_jendpointleftenumsameright. fs_h_jt_jendpointleftenumsameright + S (jt_right_jendpointleftenumsame) = S ((S (jt_index_jendpointleftenumsame)) * jt_e_jendpointleftenum)) /\ exists fs_q_jt_jendpointleftenumsameright. jt_d_jendpointleftenum = fs_q_jt_jendpointleftenumsameright * S ((S (jt_index_jendpointleftenumsame)) * jt_e_jendpointleftenum) + (jt_right_jendpointleftenumsame))) -> jt_left_jendpointleftenumsame=jt_right_jendpointleftenumsame) -> jt_i_jendpointleftenum=jt_h_jendpointleftenum))))))))) /\ (((((~((k)=0)) /\ (((~((b)=0)) /\ (exists jt_codes_jendpointright jt_code_scale_jendpointright jt_scales_jendpointright jt_scale_scale_jendpointright. ((forall jt_i_jendpointrightenum. (exists jt_gap_jendpointrightenumsoundindex. jt_gap_jendpointrightenumsoundindex+S (jt_i_jendpointrightenum)=(v)) -> exists jt_b_jendpointrightenum jt_c_jendpointrightenum. ((((((exists fs_h_jt_jendpointrightenumsoundcode. fs_h_jt_jendpointrightenumsoundcode + S (jt_b_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumsoundcode. jt_codes_jendpointright = fs_q_jt_jendpointrightenumsoundcode * S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright) + (jt_b_jendpointrightenum))) /\ (((exists fs_h_jt_jendpointrightenumsoundscale. fs_h_jt_jendpointrightenumsoundscale + S (jt_c_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumsoundscale. jt_scales_jendpointright = fs_q_jt_jendpointrightenumsoundscale * S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright) + (jt_c_jendpointrightenum))))) /\ (((forall jt_index_jendpointrightenumbound. (exists jt_gap_jendpointrightenumboundindex. jt_gap_jendpointrightenumboundindex+S (jt_index_jendpointrightenumbound)=(k)) -> exists jt_value_jendpointrightenumbound. ((((exists fs_h_jt_jendpointrightenumboundat. fs_h_jt_jendpointrightenumboundat + S (jt_value_jendpointrightenumbound) = S ((S (jt_index_jendpointrightenumbound)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumboundat. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenumboundat * S ((S (jt_index_jendpointrightenumbound)) * jt_c_jendpointrightenum) + (jt_value_jendpointrightenumbound))) /\ (exists jt_gap_jendpointrightenumboundvalue. jt_gap_jendpointrightenumboundvalue+S (jt_value_jendpointrightenumbound)=(b)))) /\ (forall jt_divisor_jendpointrightenumprimitive. (exists jt_factor_jendpointrightenumprimitivemodulus. (b)=(jt_divisor_jendpointrightenumprimitive)*jt_factor_jendpointrightenumprimitivemodulus) -> (forall jt_index_jendpointrightenumprimitivecoordinates jt_value_jendpointrightenumprimitivecoordinates. (exists jt_gap_jendpointrightenumprimitivecoordinatesindex. jt_gap_jendpointrightenumprimitivecoordinatesindex+S (jt_index_jendpointrightenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointrightenumprimitivecoordinatesat. fs_h_jt_jendpointrightenumprimitivecoordinatesat + S (jt_value_jendpointrightenumprimitivecoordinates) = S ((S (jt_index_jendpointrightenumprimitivecoordinates)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumprimitivecoordinatesat. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenumprimitivecoordinatesat * S ((S (jt_index_jendpointrightenumprimitivecoordinates)) * jt_c_jendpointrightenum) + (jt_value_jendpointrightenumprimitivecoordinates))) -> (exists jt_factor_jendpointrightenumprimitivecoordinatesdivides. (jt_value_jendpointrightenumprimitivecoordinates)=(jt_divisor_jendpointrightenumprimitive)*jt_factor_jendpointrightenumprimitivecoordinatesdivides)) -> jt_divisor_jendpointrightenumprimitive=1))))) /\ (((forall jt_b_jendpointrightenum jt_c_jendpointrightenum. (forall jt_index_jendpointrightenuminputbound. (exists jt_gap_jendpointrightenuminputboundindex. jt_gap_jendpointrightenuminputboundindex+S (jt_index_jendpointrightenuminputbound)=(k)) -> exists jt_value_jendpointrightenuminputbound. ((((exists fs_h_jt_jendpointrightenuminputboundat. fs_h_jt_jendpointrightenuminputboundat + S (jt_value_jendpointrightenuminputbound) = S ((S (jt_index_jendpointrightenuminputbound)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenuminputboundat. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenuminputboundat * S ((S (jt_index_jendpointrightenuminputbound)) * jt_c_jendpointrightenum) + (jt_value_jendpointrightenuminputbound))) /\ (exists jt_gap_jendpointrightenuminputboundvalue. jt_gap_jendpointrightenuminputboundvalue+S (jt_value_jendpointrightenuminputbound)=(b)))) -> (forall jt_divisor_jendpointrightenuminputprimitive. (exists jt_factor_jendpointrightenuminputprimitivemodulus. (b)=(jt_divisor_jendpointrightenuminputprimitive)*jt_factor_jendpointrightenuminputprimitivemodulus) -> (forall jt_index_jendpointrightenuminputprimitivecoordinates jt_value_jendpointrightenuminputprimitivecoordinates. (exists jt_gap_jendpointrightenuminputprimitivecoordinatesindex. jt_gap_jendpointrightenuminputprimitivecoordinatesindex+S (jt_index_jendpointrightenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointrightenuminputprimitivecoordinatesat. fs_h_jt_jendpointrightenuminputprimitivecoordinatesat + S (jt_value_jendpointrightenuminputprimitivecoordinates) = S ((S (jt_index_jendpointrightenuminputprimitivecoordinates)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenuminputprimitivecoordinatesat. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenuminputprimitivecoordinatesat * S ((S (jt_index_jendpointrightenuminputprimitivecoordinates)) * jt_c_jendpointrightenum) + (jt_value_jendpointrightenuminputprimitivecoordinates))) -> (exists jt_factor_jendpointrightenuminputprimitivecoordinatesdivides. (jt_value_jendpointrightenuminputprimitivecoordinates)=(jt_divisor_jendpointrightenuminputprimitive)*jt_factor_jendpointrightenuminputprimitivecoordinatesdivides)) -> jt_divisor_jendpointrightenuminputprimitive=1) -> exists jt_i_jendpointrightenum jt_d_jendpointrightenum jt_e_jendpointrightenum. ((exists jt_gap_jendpointrightenumcompleteindex. jt_gap_jendpointrightenumcompleteindex+S (jt_i_jendpointrightenum)=(v)) /\ (((((((exists fs_h_jt_jendpointrightenumcompletecode. fs_h_jt_jendpointrightenumcompletecode + S (jt_d_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumcompletecode. jt_codes_jendpointright = fs_q_jt_jendpointrightenumcompletecode * S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright) + (jt_d_jendpointrightenum))) /\ (((exists fs_h_jt_jendpointrightenumcompletescale. fs_h_jt_jendpointrightenumcompletescale + S (jt_e_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumcompletescale. jt_scales_jendpointright = fs_q_jt_jendpointrightenumcompletescale * S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright) + (jt_e_jendpointrightenum))))) /\ (forall jt_index_jendpointrightenumrepresented jt_left_jendpointrightenumrepresented jt_right_jendpointrightenumrepresented. (exists jt_gap_jendpointrightenumrepresentedindex. jt_gap_jendpointrightenumrepresentedindex+S (jt_index_jendpointrightenumrepresented)=(k)) -> (((exists fs_h_jt_jendpointrightenumrepresentedleft. fs_h_jt_jendpointrightenumrepresentedleft + S (jt_left_jendpointrightenumrepresented) = S ((S (jt_index_jendpointrightenumrepresented)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumrepresentedleft. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenumrepresentedleft * S ((S (jt_index_jendpointrightenumrepresented)) * jt_c_jendpointrightenum) + (jt_left_jendpointrightenumrepresented))) -> (((exists fs_h_jt_jendpointrightenumrepresentedright. fs_h_jt_jendpointrightenumrepresentedright + S (jt_right_jendpointrightenumrepresented) = S ((S (jt_index_jendpointrightenumrepresented)) * jt_e_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumrepresentedright. jt_d_jendpointrightenum = fs_q_jt_jendpointrightenumrepresentedright * S ((S (jt_index_jendpointrightenumrepresented)) * jt_e_jendpointrightenum) + (jt_right_jendpointrightenumrepresented))) -> jt_left_jendpointrightenumrepresented=jt_right_jendpointrightenumrepresented))))) /\ (forall jt_i_jendpointrightenum jt_h_jendpointrightenum jt_b_jendpointrightenum jt_c_jendpointrightenum jt_d_jendpointrightenum jt_e_jendpointrightenum. (exists jt_gap_jendpointrightenumfirstindex. jt_gap_jendpointrightenumfirstindex+S (jt_i_jendpointrightenum)=(v)) -> (exists jt_gap_jendpointrightenumsecondindex. jt_gap_jendpointrightenumsecondindex+S (jt_h_jendpointrightenum)=(v)) -> (((((exists fs_h_jt_jendpointrightenumfirstcode. fs_h_jt_jendpointrightenumfirstcode + S (jt_b_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumfirstcode. jt_codes_jendpointright = fs_q_jt_jendpointrightenumfirstcode * S ((S (jt_i_jendpointrightenum)) * jt_code_scale_jendpointright) + (jt_b_jendpointrightenum))) /\ (((exists fs_h_jt_jendpointrightenumfirstscale. fs_h_jt_jendpointrightenumfirstscale + S (jt_c_jendpointrightenum) = S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumfirstscale. jt_scales_jendpointright = fs_q_jt_jendpointrightenumfirstscale * S ((S (jt_i_jendpointrightenum)) * jt_scale_scale_jendpointright) + (jt_c_jendpointrightenum))))) -> (((((exists fs_h_jt_jendpointrightenumsecondcode. fs_h_jt_jendpointrightenumsecondcode + S (jt_d_jendpointrightenum) = S ((S (jt_h_jendpointrightenum)) * jt_code_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumsecondcode. jt_codes_jendpointright = fs_q_jt_jendpointrightenumsecondcode * S ((S (jt_h_jendpointrightenum)) * jt_code_scale_jendpointright) + (jt_d_jendpointrightenum))) /\ (((exists fs_h_jt_jendpointrightenumsecondscale. fs_h_jt_jendpointrightenumsecondscale + S (jt_e_jendpointrightenum) = S ((S (jt_h_jendpointrightenum)) * jt_scale_scale_jendpointright)) /\ exists fs_q_jt_jendpointrightenumsecondscale. jt_scales_jendpointright = fs_q_jt_jendpointrightenumsecondscale * S ((S (jt_h_jendpointrightenum)) * jt_scale_scale_jendpointright) + (jt_e_jendpointrightenum))))) -> (forall jt_index_jendpointrightenumsame jt_left_jendpointrightenumsame jt_right_jendpointrightenumsame. (exists jt_gap_jendpointrightenumsameindex. jt_gap_jendpointrightenumsameindex+S (jt_index_jendpointrightenumsame)=(k)) -> (((exists fs_h_jt_jendpointrightenumsameleft. fs_h_jt_jendpointrightenumsameleft + S (jt_left_jendpointrightenumsame) = S ((S (jt_index_jendpointrightenumsame)) * jt_c_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumsameleft. jt_b_jendpointrightenum = fs_q_jt_jendpointrightenumsameleft * S ((S (jt_index_jendpointrightenumsame)) * jt_c_jendpointrightenum) + (jt_left_jendpointrightenumsame))) -> (((exists fs_h_jt_jendpointrightenumsameright. fs_h_jt_jendpointrightenumsameright + S (jt_right_jendpointrightenumsame) = S ((S (jt_index_jendpointrightenumsame)) * jt_e_jendpointrightenum)) /\ exists fs_q_jt_jendpointrightenumsameright. jt_d_jendpointrightenum = fs_q_jt_jendpointrightenumsameright * S ((S (jt_index_jendpointrightenumsame)) * jt_e_jendpointrightenum) + (jt_right_jendpointrightenumsame))) -> jt_left_jendpointrightenumsame=jt_right_jendpointrightenumsame) -> jt_i_jendpointrightenum=jt_h_jendpointrightenum))))))))) /\ (((((~((k)=0)) /\ (((~((a*b)=0)) /\ (exists jt_codes_jendpointproduct jt_code_scale_jendpointproduct jt_scales_jendpointproduct jt_scale_scale_jendpointproduct. ((forall jt_i_jendpointproductenum. (exists jt_gap_jendpointproductenumsoundindex. jt_gap_jendpointproductenumsoundindex+S (jt_i_jendpointproductenum)=(w)) -> exists jt_b_jendpointproductenum jt_c_jendpointproductenum. ((((((exists fs_h_jt_jendpointproductenumsoundcode. fs_h_jt_jendpointproductenumsoundcode + S (jt_b_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumsoundcode. jt_codes_jendpointproduct = fs_q_jt_jendpointproductenumsoundcode * S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct) + (jt_b_jendpointproductenum))) /\ (((exists fs_h_jt_jendpointproductenumsoundscale. fs_h_jt_jendpointproductenumsoundscale + S (jt_c_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumsoundscale. jt_scales_jendpointproduct = fs_q_jt_jendpointproductenumsoundscale * S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct) + (jt_c_jendpointproductenum))))) /\ (((forall jt_index_jendpointproductenumbound. (exists jt_gap_jendpointproductenumboundindex. jt_gap_jendpointproductenumboundindex+S (jt_index_jendpointproductenumbound)=(k)) -> exists jt_value_jendpointproductenumbound. ((((exists fs_h_jt_jendpointproductenumboundat. fs_h_jt_jendpointproductenumboundat + S (jt_value_jendpointproductenumbound) = S ((S (jt_index_jendpointproductenumbound)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumboundat. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenumboundat * S ((S (jt_index_jendpointproductenumbound)) * jt_c_jendpointproductenum) + (jt_value_jendpointproductenumbound))) /\ (exists jt_gap_jendpointproductenumboundvalue. jt_gap_jendpointproductenumboundvalue+S (jt_value_jendpointproductenumbound)=(a*b)))) /\ (forall jt_divisor_jendpointproductenumprimitive. (exists jt_factor_jendpointproductenumprimitivemodulus. (a*b)=(jt_divisor_jendpointproductenumprimitive)*jt_factor_jendpointproductenumprimitivemodulus) -> (forall jt_index_jendpointproductenumprimitivecoordinates jt_value_jendpointproductenumprimitivecoordinates. (exists jt_gap_jendpointproductenumprimitivecoordinatesindex. jt_gap_jendpointproductenumprimitivecoordinatesindex+S (jt_index_jendpointproductenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointproductenumprimitivecoordinatesat. fs_h_jt_jendpointproductenumprimitivecoordinatesat + S (jt_value_jendpointproductenumprimitivecoordinates) = S ((S (jt_index_jendpointproductenumprimitivecoordinates)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumprimitivecoordinatesat. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenumprimitivecoordinatesat * S ((S (jt_index_jendpointproductenumprimitivecoordinates)) * jt_c_jendpointproductenum) + (jt_value_jendpointproductenumprimitivecoordinates))) -> (exists jt_factor_jendpointproductenumprimitivecoordinatesdivides. (jt_value_jendpointproductenumprimitivecoordinates)=(jt_divisor_jendpointproductenumprimitive)*jt_factor_jendpointproductenumprimitivecoordinatesdivides)) -> jt_divisor_jendpointproductenumprimitive=1))))) /\ (((forall jt_b_jendpointproductenum jt_c_jendpointproductenum. (forall jt_index_jendpointproductenuminputbound. (exists jt_gap_jendpointproductenuminputboundindex. jt_gap_jendpointproductenuminputboundindex+S (jt_index_jendpointproductenuminputbound)=(k)) -> exists jt_value_jendpointproductenuminputbound. ((((exists fs_h_jt_jendpointproductenuminputboundat. fs_h_jt_jendpointproductenuminputboundat + S (jt_value_jendpointproductenuminputbound) = S ((S (jt_index_jendpointproductenuminputbound)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenuminputboundat. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenuminputboundat * S ((S (jt_index_jendpointproductenuminputbound)) * jt_c_jendpointproductenum) + (jt_value_jendpointproductenuminputbound))) /\ (exists jt_gap_jendpointproductenuminputboundvalue. jt_gap_jendpointproductenuminputboundvalue+S (jt_value_jendpointproductenuminputbound)=(a*b)))) -> (forall jt_divisor_jendpointproductenuminputprimitive. (exists jt_factor_jendpointproductenuminputprimitivemodulus. (a*b)=(jt_divisor_jendpointproductenuminputprimitive)*jt_factor_jendpointproductenuminputprimitivemodulus) -> (forall jt_index_jendpointproductenuminputprimitivecoordinates jt_value_jendpointproductenuminputprimitivecoordinates. (exists jt_gap_jendpointproductenuminputprimitivecoordinatesindex. jt_gap_jendpointproductenuminputprimitivecoordinatesindex+S (jt_index_jendpointproductenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_jendpointproductenuminputprimitivecoordinatesat. fs_h_jt_jendpointproductenuminputprimitivecoordinatesat + S (jt_value_jendpointproductenuminputprimitivecoordinates) = S ((S (jt_index_jendpointproductenuminputprimitivecoordinates)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenuminputprimitivecoordinatesat. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenuminputprimitivecoordinatesat * S ((S (jt_index_jendpointproductenuminputprimitivecoordinates)) * jt_c_jendpointproductenum) + (jt_value_jendpointproductenuminputprimitivecoordinates))) -> (exists jt_factor_jendpointproductenuminputprimitivecoordinatesdivides. (jt_value_jendpointproductenuminputprimitivecoordinates)=(jt_divisor_jendpointproductenuminputprimitive)*jt_factor_jendpointproductenuminputprimitivecoordinatesdivides)) -> jt_divisor_jendpointproductenuminputprimitive=1) -> exists jt_i_jendpointproductenum jt_d_jendpointproductenum jt_e_jendpointproductenum. ((exists jt_gap_jendpointproductenumcompleteindex. jt_gap_jendpointproductenumcompleteindex+S (jt_i_jendpointproductenum)=(w)) /\ (((((((exists fs_h_jt_jendpointproductenumcompletecode. fs_h_jt_jendpointproductenumcompletecode + S (jt_d_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumcompletecode. jt_codes_jendpointproduct = fs_q_jt_jendpointproductenumcompletecode * S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct) + (jt_d_jendpointproductenum))) /\ (((exists fs_h_jt_jendpointproductenumcompletescale. fs_h_jt_jendpointproductenumcompletescale + S (jt_e_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumcompletescale. jt_scales_jendpointproduct = fs_q_jt_jendpointproductenumcompletescale * S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct) + (jt_e_jendpointproductenum))))) /\ (forall jt_index_jendpointproductenumrepresented jt_left_jendpointproductenumrepresented jt_right_jendpointproductenumrepresented. (exists jt_gap_jendpointproductenumrepresentedindex. jt_gap_jendpointproductenumrepresentedindex+S (jt_index_jendpointproductenumrepresented)=(k)) -> (((exists fs_h_jt_jendpointproductenumrepresentedleft. fs_h_jt_jendpointproductenumrepresentedleft + S (jt_left_jendpointproductenumrepresented) = S ((S (jt_index_jendpointproductenumrepresented)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumrepresentedleft. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenumrepresentedleft * S ((S (jt_index_jendpointproductenumrepresented)) * jt_c_jendpointproductenum) + (jt_left_jendpointproductenumrepresented))) -> (((exists fs_h_jt_jendpointproductenumrepresentedright. fs_h_jt_jendpointproductenumrepresentedright + S (jt_right_jendpointproductenumrepresented) = S ((S (jt_index_jendpointproductenumrepresented)) * jt_e_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumrepresentedright. jt_d_jendpointproductenum = fs_q_jt_jendpointproductenumrepresentedright * S ((S (jt_index_jendpointproductenumrepresented)) * jt_e_jendpointproductenum) + (jt_right_jendpointproductenumrepresented))) -> jt_left_jendpointproductenumrepresented=jt_right_jendpointproductenumrepresented))))) /\ (forall jt_i_jendpointproductenum jt_h_jendpointproductenum jt_b_jendpointproductenum jt_c_jendpointproductenum jt_d_jendpointproductenum jt_e_jendpointproductenum. (exists jt_gap_jendpointproductenumfirstindex. jt_gap_jendpointproductenumfirstindex+S (jt_i_jendpointproductenum)=(w)) -> (exists jt_gap_jendpointproductenumsecondindex. jt_gap_jendpointproductenumsecondindex+S (jt_h_jendpointproductenum)=(w)) -> (((((exists fs_h_jt_jendpointproductenumfirstcode. fs_h_jt_jendpointproductenumfirstcode + S (jt_b_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumfirstcode. jt_codes_jendpointproduct = fs_q_jt_jendpointproductenumfirstcode * S ((S (jt_i_jendpointproductenum)) * jt_code_scale_jendpointproduct) + (jt_b_jendpointproductenum))) /\ (((exists fs_h_jt_jendpointproductenumfirstscale. fs_h_jt_jendpointproductenumfirstscale + S (jt_c_jendpointproductenum) = S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumfirstscale. jt_scales_jendpointproduct = fs_q_jt_jendpointproductenumfirstscale * S ((S (jt_i_jendpointproductenum)) * jt_scale_scale_jendpointproduct) + (jt_c_jendpointproductenum))))) -> (((((exists fs_h_jt_jendpointproductenumsecondcode. fs_h_jt_jendpointproductenumsecondcode + S (jt_d_jendpointproductenum) = S ((S (jt_h_jendpointproductenum)) * jt_code_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumsecondcode. jt_codes_jendpointproduct = fs_q_jt_jendpointproductenumsecondcode * S ((S (jt_h_jendpointproductenum)) * jt_code_scale_jendpointproduct) + (jt_d_jendpointproductenum))) /\ (((exists fs_h_jt_jendpointproductenumsecondscale. fs_h_jt_jendpointproductenumsecondscale + S (jt_e_jendpointproductenum) = S ((S (jt_h_jendpointproductenum)) * jt_scale_scale_jendpointproduct)) /\ exists fs_q_jt_jendpointproductenumsecondscale. jt_scales_jendpointproduct = fs_q_jt_jendpointproductenumsecondscale * S ((S (jt_h_jendpointproductenum)) * jt_scale_scale_jendpointproduct) + (jt_e_jendpointproductenum))))) -> (forall jt_index_jendpointproductenumsame jt_left_jendpointproductenumsame jt_right_jendpointproductenumsame. (exists jt_gap_jendpointproductenumsameindex. jt_gap_jendpointproductenumsameindex+S (jt_index_jendpointproductenumsame)=(k)) -> (((exists fs_h_jt_jendpointproductenumsameleft. fs_h_jt_jendpointproductenumsameleft + S (jt_left_jendpointproductenumsame) = S ((S (jt_index_jendpointproductenumsame)) * jt_c_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumsameleft. jt_b_jendpointproductenum = fs_q_jt_jendpointproductenumsameleft * S ((S (jt_index_jendpointproductenumsame)) * jt_c_jendpointproductenum) + (jt_left_jendpointproductenumsame))) -> (((exists fs_h_jt_jendpointproductenumsameright. fs_h_jt_jendpointproductenumsameright + S (jt_right_jendpointproductenumsame) = S ((S (jt_index_jendpointproductenumsame)) * jt_e_jendpointproductenum)) /\ exists fs_q_jt_jendpointproductenumsameright. jt_d_jendpointproductenum = fs_q_jt_jendpointproductenumsameright * S ((S (jt_index_jendpointproductenumsame)) * jt_e_jendpointproductenum) + (jt_right_jendpointproductenumsame))) -> jt_left_jendpointproductenumsame=jt_right_jendpointproductenumsame) -> jt_i_jendpointproductenum=jt_h_jendpointproductenum))))))))) /\ (w=u*v))))))