jordan_product_enumeration_exists

forall m n k A B C D u E F G H v. ~(m=0) -> ~(n=0) -> (forall jt_divisor_mulenumcop. (exists jt_factor_mulenumcopa. (m)=(jt_divisor_mulenumcop)*jt_factor_mulenumcopa) -> (exists jt_factor_mulenumcopb. (n)=(jt_divisor_mulenumcop)*jt_factor_mulenumcopb) -> jt_divisor_mulenumcop=1) -> (((forall jt_i_mulenumleft. (exists jt_gap_mulenumleftsoundindex. jt_gap_mulenumleftsoundindex+S (jt_i_mulenumleft)=(u)) -> exists jt_b_mulenumleft jt_c_mulenumleft. ((((((exists fs_h_jt_mulenumleftsoundcode. fs_h_jt_mulenumleftsoundcode + S (jt_b_mulenumleft) = S ((S (jt_i_mulenumleft)) * B)) /\ exists fs_q_jt_mulenumleftsoundcode. A = fs_q_jt_mulenumleftsoundcode * S ((S (jt_i_mulenumleft)) * B) + (jt_b_mulenumleft))) /\ (((exists fs_h_jt_mulenumleftsoundscale. fs_h_jt_mulenumleftsoundscale + S (jt_c_mulenumleft) = S ((S (jt_i_mulenumleft)) * D)) /\ exists fs_q_jt_mulenumleftsoundscale. C = fs_q_jt_mulenumleftsoundscale * S ((S (jt_i_mulenumleft)) * D) + (jt_c_mulenumleft))))) /\ (((forall jt_index_mulenumleftbound. (exists jt_gap_mulenumleftboundindex. jt_gap_mulenumleftboundindex+S (jt_index_mulenumleftbound)=(k)) -> exists jt_value_mulenumleftbound. ((((exists fs_h_jt_mulenumleftboundat. fs_h_jt_mulenumleftboundat + S (jt_value_mulenumleftbound) = S ((S (jt_index_mulenumleftbound)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftboundat. jt_b_mulenumleft = fs_q_jt_mulenumleftboundat * S ((S (jt_index_mulenumleftbound)) * jt_c_mulenumleft) + (jt_value_mulenumleftbound))) /\ (exists jt_gap_mulenumleftboundvalue. jt_gap_mulenumleftboundvalue+S (jt_value_mulenumleftbound)=(m)))) /\ (forall jt_divisor_mulenumleftprimitive. (exists jt_factor_mulenumleftprimitivemodulus. (m)=(jt_divisor_mulenumleftprimitive)*jt_factor_mulenumleftprimitivemodulus) -> (forall jt_index_mulenumleftprimitivecoordinates jt_value_mulenumleftprimitivecoordinates. (exists jt_gap_mulenumleftprimitivecoordinatesindex. jt_gap_mulenumleftprimitivecoordinatesindex+S (jt_index_mulenumleftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumleftprimitivecoordinatesat. fs_h_jt_mulenumleftprimitivecoordinatesat + S (jt_value_mulenumleftprimitivecoordinates) = S ((S (jt_index_mulenumleftprimitivecoordinates)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftprimitivecoordinatesat. jt_b_mulenumleft = fs_q_jt_mulenumleftprimitivecoordinatesat * S ((S (jt_index_mulenumleftprimitivecoordinates)) * jt_c_mulenumleft) + (jt_value_mulenumleftprimitivecoordinates))) -> (exists jt_factor_mulenumleftprimitivecoordinatesdivides. (jt_value_mulenumleftprimitivecoordinates)=(jt_divisor_mulenumleftprimitive)*jt_factor_mulenumleftprimitivecoordinatesdivides)) -> jt_divisor_mulenumleftprimitive=1))))) /\ (((forall jt_b_mulenumleft jt_c_mulenumleft. (forall jt_index_mulenumleftinputbound. (exists jt_gap_mulenumleftinputboundindex. jt_gap_mulenumleftinputboundindex+S (jt_index_mulenumleftinputbound)=(k)) -> exists jt_value_mulenumleftinputbound. ((((exists fs_h_jt_mulenumleftinputboundat. fs_h_jt_mulenumleftinputboundat + S (jt_value_mulenumleftinputbound) = S ((S (jt_index_mulenumleftinputbound)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftinputboundat. jt_b_mulenumleft = fs_q_jt_mulenumleftinputboundat * S ((S (jt_index_mulenumleftinputbound)) * jt_c_mulenumleft) + (jt_value_mulenumleftinputbound))) /\ (exists jt_gap_mulenumleftinputboundvalue. jt_gap_mulenumleftinputboundvalue+S (jt_value_mulenumleftinputbound)=(m)))) -> (forall jt_divisor_mulenumleftinputprimitive. (exists jt_factor_mulenumleftinputprimitivemodulus. (m)=(jt_divisor_mulenumleftinputprimitive)*jt_factor_mulenumleftinputprimitivemodulus) -> (forall jt_index_mulenumleftinputprimitivecoordinates jt_value_mulenumleftinputprimitivecoordinates. (exists jt_gap_mulenumleftinputprimitivecoordinatesindex. jt_gap_mulenumleftinputprimitivecoordinatesindex+S (jt_index_mulenumleftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumleftinputprimitivecoordinatesat. fs_h_jt_mulenumleftinputprimitivecoordinatesat + S (jt_value_mulenumleftinputprimitivecoordinates) = S ((S (jt_index_mulenumleftinputprimitivecoordinates)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftinputprimitivecoordinatesat. jt_b_mulenumleft = fs_q_jt_mulenumleftinputprimitivecoordinatesat * S ((S (jt_index_mulenumleftinputprimitivecoordinates)) * jt_c_mulenumleft) + (jt_value_mulenumleftinputprimitivecoordinates))) -> (exists jt_factor_mulenumleftinputprimitivecoordinatesdivides. (jt_value_mulenumleftinputprimitivecoordinates)=(jt_divisor_mulenumleftinputprimitive)*jt_factor_mulenumleftinputprimitivecoordinatesdivides)) -> jt_divisor_mulenumleftinputprimitive=1) -> exists jt_i_mulenumleft jt_d_mulenumleft jt_e_mulenumleft. ((exists jt_gap_mulenumleftcompleteindex. jt_gap_mulenumleftcompleteindex+S (jt_i_mulenumleft)=(u)) /\ (((((((exists fs_h_jt_mulenumleftcompletecode. fs_h_jt_mulenumleftcompletecode + S (jt_d_mulenumleft) = S ((S (jt_i_mulenumleft)) * B)) /\ exists fs_q_jt_mulenumleftcompletecode. A = fs_q_jt_mulenumleftcompletecode * S ((S (jt_i_mulenumleft)) * B) + (jt_d_mulenumleft))) /\ (((exists fs_h_jt_mulenumleftcompletescale. fs_h_jt_mulenumleftcompletescale + S (jt_e_mulenumleft) = S ((S (jt_i_mulenumleft)) * D)) /\ exists fs_q_jt_mulenumleftcompletescale. C = fs_q_jt_mulenumleftcompletescale * S ((S (jt_i_mulenumleft)) * D) + (jt_e_mulenumleft))))) /\ (forall jt_index_mulenumleftrepresented jt_left_mulenumleftrepresented jt_right_mulenumleftrepresented. (exists jt_gap_mulenumleftrepresentedindex. jt_gap_mulenumleftrepresentedindex+S (jt_index_mulenumleftrepresented)=(k)) -> (((exists fs_h_jt_mulenumleftrepresentedleft. fs_h_jt_mulenumleftrepresentedleft + S (jt_left_mulenumleftrepresented) = S ((S (jt_index_mulenumleftrepresented)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftrepresentedleft. jt_b_mulenumleft = fs_q_jt_mulenumleftrepresentedleft * S ((S (jt_index_mulenumleftrepresented)) * jt_c_mulenumleft) + (jt_left_mulenumleftrepresented))) -> (((exists fs_h_jt_mulenumleftrepresentedright. fs_h_jt_mulenumleftrepresentedright + S (jt_right_mulenumleftrepresented) = S ((S (jt_index_mulenumleftrepresented)) * jt_e_mulenumleft)) /\ exists fs_q_jt_mulenumleftrepresentedright. jt_d_mulenumleft = fs_q_jt_mulenumleftrepresentedright * S ((S (jt_index_mulenumleftrepresented)) * jt_e_mulenumleft) + (jt_right_mulenumleftrepresented))) -> jt_left_mulenumleftrepresented=jt_right_mulenumleftrepresented))))) /\ (forall jt_i_mulenumleft jt_h_mulenumleft jt_b_mulenumleft jt_c_mulenumleft jt_d_mulenumleft jt_e_mulenumleft. (exists jt_gap_mulenumleftfirstindex. jt_gap_mulenumleftfirstindex+S (jt_i_mulenumleft)=(u)) -> (exists jt_gap_mulenumleftsecondindex. jt_gap_mulenumleftsecondindex+S (jt_h_mulenumleft)=(u)) -> (((((exists fs_h_jt_mulenumleftfirstcode. fs_h_jt_mulenumleftfirstcode + S (jt_b_mulenumleft) = S ((S (jt_i_mulenumleft)) * B)) /\ exists fs_q_jt_mulenumleftfirstcode. A = fs_q_jt_mulenumleftfirstcode * S ((S (jt_i_mulenumleft)) * B) + (jt_b_mulenumleft))) /\ (((exists fs_h_jt_mulenumleftfirstscale. fs_h_jt_mulenumleftfirstscale + S (jt_c_mulenumleft) = S ((S (jt_i_mulenumleft)) * D)) /\ exists fs_q_jt_mulenumleftfirstscale. C = fs_q_jt_mulenumleftfirstscale * S ((S (jt_i_mulenumleft)) * D) + (jt_c_mulenumleft))))) -> (((((exists fs_h_jt_mulenumleftsecondcode. fs_h_jt_mulenumleftsecondcode + S (jt_d_mulenumleft) = S ((S (jt_h_mulenumleft)) * B)) /\ exists fs_q_jt_mulenumleftsecondcode. A = fs_q_jt_mulenumleftsecondcode * S ((S (jt_h_mulenumleft)) * B) + (jt_d_mulenumleft))) /\ (((exists fs_h_jt_mulenumleftsecondscale. fs_h_jt_mulenumleftsecondscale + S (jt_e_mulenumleft) = S ((S (jt_h_mulenumleft)) * D)) /\ exists fs_q_jt_mulenumleftsecondscale. C = fs_q_jt_mulenumleftsecondscale * S ((S (jt_h_mulenumleft)) * D) + (jt_e_mulenumleft))))) -> (forall jt_index_mulenumleftsame jt_left_mulenumleftsame jt_right_mulenumleftsame. (exists jt_gap_mulenumleftsameindex. jt_gap_mulenumleftsameindex+S (jt_index_mulenumleftsame)=(k)) -> (((exists fs_h_jt_mulenumleftsameleft. fs_h_jt_mulenumleftsameleft + S (jt_left_mulenumleftsame) = S ((S (jt_index_mulenumleftsame)) * jt_c_mulenumleft)) /\ exists fs_q_jt_mulenumleftsameleft. jt_b_mulenumleft = fs_q_jt_mulenumleftsameleft * S ((S (jt_index_mulenumleftsame)) * jt_c_mulenumleft) + (jt_left_mulenumleftsame))) -> (((exists fs_h_jt_mulenumleftsameright. fs_h_jt_mulenumleftsameright + S (jt_right_mulenumleftsame) = S ((S (jt_index_mulenumleftsame)) * jt_e_mulenumleft)) /\ exists fs_q_jt_mulenumleftsameright. jt_d_mulenumleft = fs_q_jt_mulenumleftsameright * S ((S (jt_index_mulenumleftsame)) * jt_e_mulenumleft) + (jt_right_mulenumleftsame))) -> jt_left_mulenumleftsame=jt_right_mulenumleftsame) -> jt_i_mulenumleft=jt_h_mulenumleft))))) -> (((forall jt_i_mulenumright. (exists jt_gap_mulenumrightsoundindex. jt_gap_mulenumrightsoundindex+S (jt_i_mulenumright)=(v)) -> exists jt_b_mulenumright jt_c_mulenumright. ((((((exists fs_h_jt_mulenumrightsoundcode. fs_h_jt_mulenumrightsoundcode + S (jt_b_mulenumright) = S ((S (jt_i_mulenumright)) * F)) /\ exists fs_q_jt_mulenumrightsoundcode. E = fs_q_jt_mulenumrightsoundcode * S ((S (jt_i_mulenumright)) * F) + (jt_b_mulenumright))) /\ (((exists fs_h_jt_mulenumrightsoundscale. fs_h_jt_mulenumrightsoundscale + S (jt_c_mulenumright) = S ((S (jt_i_mulenumright)) * H)) /\ exists fs_q_jt_mulenumrightsoundscale. G = fs_q_jt_mulenumrightsoundscale * S ((S (jt_i_mulenumright)) * H) + (jt_c_mulenumright))))) /\ (((forall jt_index_mulenumrightbound. (exists jt_gap_mulenumrightboundindex. jt_gap_mulenumrightboundindex+S (jt_index_mulenumrightbound)=(k)) -> exists jt_value_mulenumrightbound. ((((exists fs_h_jt_mulenumrightboundat. fs_h_jt_mulenumrightboundat + S (jt_value_mulenumrightbound) = S ((S (jt_index_mulenumrightbound)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightboundat. jt_b_mulenumright = fs_q_jt_mulenumrightboundat * S ((S (jt_index_mulenumrightbound)) * jt_c_mulenumright) + (jt_value_mulenumrightbound))) /\ (exists jt_gap_mulenumrightboundvalue. jt_gap_mulenumrightboundvalue+S (jt_value_mulenumrightbound)=(n)))) /\ (forall jt_divisor_mulenumrightprimitive. (exists jt_factor_mulenumrightprimitivemodulus. (n)=(jt_divisor_mulenumrightprimitive)*jt_factor_mulenumrightprimitivemodulus) -> (forall jt_index_mulenumrightprimitivecoordinates jt_value_mulenumrightprimitivecoordinates. (exists jt_gap_mulenumrightprimitivecoordinatesindex. jt_gap_mulenumrightprimitivecoordinatesindex+S (jt_index_mulenumrightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumrightprimitivecoordinatesat. fs_h_jt_mulenumrightprimitivecoordinatesat + S (jt_value_mulenumrightprimitivecoordinates) = S ((S (jt_index_mulenumrightprimitivecoordinates)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightprimitivecoordinatesat. jt_b_mulenumright = fs_q_jt_mulenumrightprimitivecoordinatesat * S ((S (jt_index_mulenumrightprimitivecoordinates)) * jt_c_mulenumright) + (jt_value_mulenumrightprimitivecoordinates))) -> (exists jt_factor_mulenumrightprimitivecoordinatesdivides. (jt_value_mulenumrightprimitivecoordinates)=(jt_divisor_mulenumrightprimitive)*jt_factor_mulenumrightprimitivecoordinatesdivides)) -> jt_divisor_mulenumrightprimitive=1))))) /\ (((forall jt_b_mulenumright jt_c_mulenumright. (forall jt_index_mulenumrightinputbound. (exists jt_gap_mulenumrightinputboundindex. jt_gap_mulenumrightinputboundindex+S (jt_index_mulenumrightinputbound)=(k)) -> exists jt_value_mulenumrightinputbound. ((((exists fs_h_jt_mulenumrightinputboundat. fs_h_jt_mulenumrightinputboundat + S (jt_value_mulenumrightinputbound) = S ((S (jt_index_mulenumrightinputbound)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightinputboundat. jt_b_mulenumright = fs_q_jt_mulenumrightinputboundat * S ((S (jt_index_mulenumrightinputbound)) * jt_c_mulenumright) + (jt_value_mulenumrightinputbound))) /\ (exists jt_gap_mulenumrightinputboundvalue. jt_gap_mulenumrightinputboundvalue+S (jt_value_mulenumrightinputbound)=(n)))) -> (forall jt_divisor_mulenumrightinputprimitive. (exists jt_factor_mulenumrightinputprimitivemodulus. (n)=(jt_divisor_mulenumrightinputprimitive)*jt_factor_mulenumrightinputprimitivemodulus) -> (forall jt_index_mulenumrightinputprimitivecoordinates jt_value_mulenumrightinputprimitivecoordinates. (exists jt_gap_mulenumrightinputprimitivecoordinatesindex. jt_gap_mulenumrightinputprimitivecoordinatesindex+S (jt_index_mulenumrightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumrightinputprimitivecoordinatesat. fs_h_jt_mulenumrightinputprimitivecoordinatesat + S (jt_value_mulenumrightinputprimitivecoordinates) = S ((S (jt_index_mulenumrightinputprimitivecoordinates)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightinputprimitivecoordinatesat. jt_b_mulenumright = fs_q_jt_mulenumrightinputprimitivecoordinatesat * S ((S (jt_index_mulenumrightinputprimitivecoordinates)) * jt_c_mulenumright) + (jt_value_mulenumrightinputprimitivecoordinates))) -> (exists jt_factor_mulenumrightinputprimitivecoordinatesdivides. (jt_value_mulenumrightinputprimitivecoordinates)=(jt_divisor_mulenumrightinputprimitive)*jt_factor_mulenumrightinputprimitivecoordinatesdivides)) -> jt_divisor_mulenumrightinputprimitive=1) -> exists jt_i_mulenumright jt_d_mulenumright jt_e_mulenumright. ((exists jt_gap_mulenumrightcompleteindex. jt_gap_mulenumrightcompleteindex+S (jt_i_mulenumright)=(v)) /\ (((((((exists fs_h_jt_mulenumrightcompletecode. fs_h_jt_mulenumrightcompletecode + S (jt_d_mulenumright) = S ((S (jt_i_mulenumright)) * F)) /\ exists fs_q_jt_mulenumrightcompletecode. E = fs_q_jt_mulenumrightcompletecode * S ((S (jt_i_mulenumright)) * F) + (jt_d_mulenumright))) /\ (((exists fs_h_jt_mulenumrightcompletescale. fs_h_jt_mulenumrightcompletescale + S (jt_e_mulenumright) = S ((S (jt_i_mulenumright)) * H)) /\ exists fs_q_jt_mulenumrightcompletescale. G = fs_q_jt_mulenumrightcompletescale * S ((S (jt_i_mulenumright)) * H) + (jt_e_mulenumright))))) /\ (forall jt_index_mulenumrightrepresented jt_left_mulenumrightrepresented jt_right_mulenumrightrepresented. (exists jt_gap_mulenumrightrepresentedindex. jt_gap_mulenumrightrepresentedindex+S (jt_index_mulenumrightrepresented)=(k)) -> (((exists fs_h_jt_mulenumrightrepresentedleft. fs_h_jt_mulenumrightrepresentedleft + S (jt_left_mulenumrightrepresented) = S ((S (jt_index_mulenumrightrepresented)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightrepresentedleft. jt_b_mulenumright = fs_q_jt_mulenumrightrepresentedleft * S ((S (jt_index_mulenumrightrepresented)) * jt_c_mulenumright) + (jt_left_mulenumrightrepresented))) -> (((exists fs_h_jt_mulenumrightrepresentedright. fs_h_jt_mulenumrightrepresentedright + S (jt_right_mulenumrightrepresented) = S ((S (jt_index_mulenumrightrepresented)) * jt_e_mulenumright)) /\ exists fs_q_jt_mulenumrightrepresentedright. jt_d_mulenumright = fs_q_jt_mulenumrightrepresentedright * S ((S (jt_index_mulenumrightrepresented)) * jt_e_mulenumright) + (jt_right_mulenumrightrepresented))) -> jt_left_mulenumrightrepresented=jt_right_mulenumrightrepresented))))) /\ (forall jt_i_mulenumright jt_h_mulenumright jt_b_mulenumright jt_c_mulenumright jt_d_mulenumright jt_e_mulenumright. (exists jt_gap_mulenumrightfirstindex. jt_gap_mulenumrightfirstindex+S (jt_i_mulenumright)=(v)) -> (exists jt_gap_mulenumrightsecondindex. jt_gap_mulenumrightsecondindex+S (jt_h_mulenumright)=(v)) -> (((((exists fs_h_jt_mulenumrightfirstcode. fs_h_jt_mulenumrightfirstcode + S (jt_b_mulenumright) = S ((S (jt_i_mulenumright)) * F)) /\ exists fs_q_jt_mulenumrightfirstcode. E = fs_q_jt_mulenumrightfirstcode * S ((S (jt_i_mulenumright)) * F) + (jt_b_mulenumright))) /\ (((exists fs_h_jt_mulenumrightfirstscale. fs_h_jt_mulenumrightfirstscale + S (jt_c_mulenumright) = S ((S (jt_i_mulenumright)) * H)) /\ exists fs_q_jt_mulenumrightfirstscale. G = fs_q_jt_mulenumrightfirstscale * S ((S (jt_i_mulenumright)) * H) + (jt_c_mulenumright))))) -> (((((exists fs_h_jt_mulenumrightsecondcode. fs_h_jt_mulenumrightsecondcode + S (jt_d_mulenumright) = S ((S (jt_h_mulenumright)) * F)) /\ exists fs_q_jt_mulenumrightsecondcode. E = fs_q_jt_mulenumrightsecondcode * S ((S (jt_h_mulenumright)) * F) + (jt_d_mulenumright))) /\ (((exists fs_h_jt_mulenumrightsecondscale. fs_h_jt_mulenumrightsecondscale + S (jt_e_mulenumright) = S ((S (jt_h_mulenumright)) * H)) /\ exists fs_q_jt_mulenumrightsecondscale. G = fs_q_jt_mulenumrightsecondscale * S ((S (jt_h_mulenumright)) * H) + (jt_e_mulenumright))))) -> (forall jt_index_mulenumrightsame jt_left_mulenumrightsame jt_right_mulenumrightsame. (exists jt_gap_mulenumrightsameindex. jt_gap_mulenumrightsameindex+S (jt_index_mulenumrightsame)=(k)) -> (((exists fs_h_jt_mulenumrightsameleft. fs_h_jt_mulenumrightsameleft + S (jt_left_mulenumrightsame) = S ((S (jt_index_mulenumrightsame)) * jt_c_mulenumright)) /\ exists fs_q_jt_mulenumrightsameleft. jt_b_mulenumright = fs_q_jt_mulenumrightsameleft * S ((S (jt_index_mulenumrightsame)) * jt_c_mulenumright) + (jt_left_mulenumrightsame))) -> (((exists fs_h_jt_mulenumrightsameright. fs_h_jt_mulenumrightsameright + S (jt_right_mulenumrightsame) = S ((S (jt_index_mulenumrightsame)) * jt_e_mulenumright)) /\ exists fs_q_jt_mulenumrightsameright. jt_d_mulenumright = fs_q_jt_mulenumrightsameright * S ((S (jt_index_mulenumrightsame)) * jt_e_mulenumright) + (jt_right_mulenumrightsame))) -> jt_left_mulenumrightsame=jt_right_mulenumrightsame) -> jt_i_mulenumright=jt_h_mulenumright))))) -> exists P Q R T. ((forall jt_i_mulenumoutput. (exists jt_gap_mulenumoutputsoundindex. jt_gap_mulenumoutputsoundindex+S (jt_i_mulenumoutput)=(u*v)) -> exists jt_b_mulenumoutput jt_c_mulenumoutput. ((((((exists fs_h_jt_mulenumoutputsoundcode. fs_h_jt_mulenumoutputsoundcode + S (jt_b_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * Q)) /\ exists fs_q_jt_mulenumoutputsoundcode. P = fs_q_jt_mulenumoutputsoundcode * S ((S (jt_i_mulenumoutput)) * Q) + (jt_b_mulenumoutput))) /\ (((exists fs_h_jt_mulenumoutputsoundscale. fs_h_jt_mulenumoutputsoundscale + S (jt_c_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * T)) /\ exists fs_q_jt_mulenumoutputsoundscale. R = fs_q_jt_mulenumoutputsoundscale * S ((S (jt_i_mulenumoutput)) * T) + (jt_c_mulenumoutput))))) /\ (((forall jt_index_mulenumoutputbound. (exists jt_gap_mulenumoutputboundindex. jt_gap_mulenumoutputboundindex+S (jt_index_mulenumoutputbound)=(k)) -> exists jt_value_mulenumoutputbound. ((((exists fs_h_jt_mulenumoutputboundat. fs_h_jt_mulenumoutputboundat + S (jt_value_mulenumoutputbound) = S ((S (jt_index_mulenumoutputbound)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputboundat. jt_b_mulenumoutput = fs_q_jt_mulenumoutputboundat * S ((S (jt_index_mulenumoutputbound)) * jt_c_mulenumoutput) + (jt_value_mulenumoutputbound))) /\ (exists jt_gap_mulenumoutputboundvalue. jt_gap_mulenumoutputboundvalue+S (jt_value_mulenumoutputbound)=(m*n)))) /\ (forall jt_divisor_mulenumoutputprimitive. (exists jt_factor_mulenumoutputprimitivemodulus. (m*n)=(jt_divisor_mulenumoutputprimitive)*jt_factor_mulenumoutputprimitivemodulus) -> (forall jt_index_mulenumoutputprimitivecoordinates jt_value_mulenumoutputprimitivecoordinates. (exists jt_gap_mulenumoutputprimitivecoordinatesindex. jt_gap_mulenumoutputprimitivecoordinatesindex+S (jt_index_mulenumoutputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumoutputprimitivecoordinatesat. fs_h_jt_mulenumoutputprimitivecoordinatesat + S (jt_value_mulenumoutputprimitivecoordinates) = S ((S (jt_index_mulenumoutputprimitivecoordinates)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputprimitivecoordinatesat. jt_b_mulenumoutput = fs_q_jt_mulenumoutputprimitivecoordinatesat * S ((S (jt_index_mulenumoutputprimitivecoordinates)) * jt_c_mulenumoutput) + (jt_value_mulenumoutputprimitivecoordinates))) -> (exists jt_factor_mulenumoutputprimitivecoordinatesdivides. (jt_value_mulenumoutputprimitivecoordinates)=(jt_divisor_mulenumoutputprimitive)*jt_factor_mulenumoutputprimitivecoordinatesdivides)) -> jt_divisor_mulenumoutputprimitive=1))))) /\ (((forall jt_b_mulenumoutput jt_c_mulenumoutput. (forall jt_index_mulenumoutputinputbound. (exists jt_gap_mulenumoutputinputboundindex. jt_gap_mulenumoutputinputboundindex+S (jt_index_mulenumoutputinputbound)=(k)) -> exists jt_value_mulenumoutputinputbound. ((((exists fs_h_jt_mulenumoutputinputboundat. fs_h_jt_mulenumoutputinputboundat + S (jt_value_mulenumoutputinputbound) = S ((S (jt_index_mulenumoutputinputbound)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputinputboundat. jt_b_mulenumoutput = fs_q_jt_mulenumoutputinputboundat * S ((S (jt_index_mulenumoutputinputbound)) * jt_c_mulenumoutput) + (jt_value_mulenumoutputinputbound))) /\ (exists jt_gap_mulenumoutputinputboundvalue. jt_gap_mulenumoutputinputboundvalue+S (jt_value_mulenumoutputinputbound)=(m*n)))) -> (forall jt_divisor_mulenumoutputinputprimitive. (exists jt_factor_mulenumoutputinputprimitivemodulus. (m*n)=(jt_divisor_mulenumoutputinputprimitive)*jt_factor_mulenumoutputinputprimitivemodulus) -> (forall jt_index_mulenumoutputinputprimitivecoordinates jt_value_mulenumoutputinputprimitivecoordinates. (exists jt_gap_mulenumoutputinputprimitivecoordinatesindex. jt_gap_mulenumoutputinputprimitivecoordinatesindex+S (jt_index_mulenumoutputinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_mulenumoutputinputprimitivecoordinatesat. fs_h_jt_mulenumoutputinputprimitivecoordinatesat + S (jt_value_mulenumoutputinputprimitivecoordinates) = S ((S (jt_index_mulenumoutputinputprimitivecoordinates)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputinputprimitivecoordinatesat. jt_b_mulenumoutput = fs_q_jt_mulenumoutputinputprimitivecoordinatesat * S ((S (jt_index_mulenumoutputinputprimitivecoordinates)) * jt_c_mulenumoutput) + (jt_value_mulenumoutputinputprimitivecoordinates))) -> (exists jt_factor_mulenumoutputinputprimitivecoordinatesdivides. (jt_value_mulenumoutputinputprimitivecoordinates)=(jt_divisor_mulenumoutputinputprimitive)*jt_factor_mulenumoutputinputprimitivecoordinatesdivides)) -> jt_divisor_mulenumoutputinputprimitive=1) -> exists jt_i_mulenumoutput jt_d_mulenumoutput jt_e_mulenumoutput. ((exists jt_gap_mulenumoutputcompleteindex. jt_gap_mulenumoutputcompleteindex+S (jt_i_mulenumoutput)=(u*v)) /\ (((((((exists fs_h_jt_mulenumoutputcompletecode. fs_h_jt_mulenumoutputcompletecode + S (jt_d_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * Q)) /\ exists fs_q_jt_mulenumoutputcompletecode. P = fs_q_jt_mulenumoutputcompletecode * S ((S (jt_i_mulenumoutput)) * Q) + (jt_d_mulenumoutput))) /\ (((exists fs_h_jt_mulenumoutputcompletescale. fs_h_jt_mulenumoutputcompletescale + S (jt_e_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * T)) /\ exists fs_q_jt_mulenumoutputcompletescale. R = fs_q_jt_mulenumoutputcompletescale * S ((S (jt_i_mulenumoutput)) * T) + (jt_e_mulenumoutput))))) /\ (forall jt_index_mulenumoutputrepresented jt_left_mulenumoutputrepresented jt_right_mulenumoutputrepresented. (exists jt_gap_mulenumoutputrepresentedindex. jt_gap_mulenumoutputrepresentedindex+S (jt_index_mulenumoutputrepresented)=(k)) -> (((exists fs_h_jt_mulenumoutputrepresentedleft. fs_h_jt_mulenumoutputrepresentedleft + S (jt_left_mulenumoutputrepresented) = S ((S (jt_index_mulenumoutputrepresented)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputrepresentedleft. jt_b_mulenumoutput = fs_q_jt_mulenumoutputrepresentedleft * S ((S (jt_index_mulenumoutputrepresented)) * jt_c_mulenumoutput) + (jt_left_mulenumoutputrepresented))) -> (((exists fs_h_jt_mulenumoutputrepresentedright. fs_h_jt_mulenumoutputrepresentedright + S (jt_right_mulenumoutputrepresented) = S ((S (jt_index_mulenumoutputrepresented)) * jt_e_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputrepresentedright. jt_d_mulenumoutput = fs_q_jt_mulenumoutputrepresentedright * S ((S (jt_index_mulenumoutputrepresented)) * jt_e_mulenumoutput) + (jt_right_mulenumoutputrepresented))) -> jt_left_mulenumoutputrepresented=jt_right_mulenumoutputrepresented))))) /\ (forall jt_i_mulenumoutput jt_h_mulenumoutput jt_b_mulenumoutput jt_c_mulenumoutput jt_d_mulenumoutput jt_e_mulenumoutput. (exists jt_gap_mulenumoutputfirstindex. jt_gap_mulenumoutputfirstindex+S (jt_i_mulenumoutput)=(u*v)) -> (exists jt_gap_mulenumoutputsecondindex. jt_gap_mulenumoutputsecondindex+S (jt_h_mulenumoutput)=(u*v)) -> (((((exists fs_h_jt_mulenumoutputfirstcode. fs_h_jt_mulenumoutputfirstcode + S (jt_b_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * Q)) /\ exists fs_q_jt_mulenumoutputfirstcode. P = fs_q_jt_mulenumoutputfirstcode * S ((S (jt_i_mulenumoutput)) * Q) + (jt_b_mulenumoutput))) /\ (((exists fs_h_jt_mulenumoutputfirstscale. fs_h_jt_mulenumoutputfirstscale + S (jt_c_mulenumoutput) = S ((S (jt_i_mulenumoutput)) * T)) /\ exists fs_q_jt_mulenumoutputfirstscale. R = fs_q_jt_mulenumoutputfirstscale * S ((S (jt_i_mulenumoutput)) * T) + (jt_c_mulenumoutput))))) -> (((((exists fs_h_jt_mulenumoutputsecondcode. fs_h_jt_mulenumoutputsecondcode + S (jt_d_mulenumoutput) = S ((S (jt_h_mulenumoutput)) * Q)) /\ exists fs_q_jt_mulenumoutputsecondcode. P = fs_q_jt_mulenumoutputsecondcode * S ((S (jt_h_mulenumoutput)) * Q) + (jt_d_mulenumoutput))) /\ (((exists fs_h_jt_mulenumoutputsecondscale. fs_h_jt_mulenumoutputsecondscale + S (jt_e_mulenumoutput) = S ((S (jt_h_mulenumoutput)) * T)) /\ exists fs_q_jt_mulenumoutputsecondscale. R = fs_q_jt_mulenumoutputsecondscale * S ((S (jt_h_mulenumoutput)) * T) + (jt_e_mulenumoutput))))) -> (forall jt_index_mulenumoutputsame jt_left_mulenumoutputsame jt_right_mulenumoutputsame. (exists jt_gap_mulenumoutputsameindex. jt_gap_mulenumoutputsameindex+S (jt_index_mulenumoutputsame)=(k)) -> (((exists fs_h_jt_mulenumoutputsameleft. fs_h_jt_mulenumoutputsameleft + S (jt_left_mulenumoutputsame) = S ((S (jt_index_mulenumoutputsame)) * jt_c_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputsameleft. jt_b_mulenumoutput = fs_q_jt_mulenumoutputsameleft * S ((S (jt_index_mulenumoutputsame)) * jt_c_mulenumoutput) + (jt_left_mulenumoutputsame))) -> (((exists fs_h_jt_mulenumoutputsameright. fs_h_jt_mulenumoutputsameright + S (jt_right_mulenumoutputsame) = S ((S (jt_index_mulenumoutputsame)) * jt_e_mulenumoutput)) /\ exists fs_q_jt_mulenumoutputsameright. jt_d_mulenumoutput = fs_q_jt_mulenumoutputsameright * S ((S (jt_index_mulenumoutputsame)) * jt_e_mulenumoutput) + (jt_right_mulenumoutputsame))) -> jt_left_mulenumoutputsame=jt_right_mulenumoutputsame) -> jt_i_mulenumoutput=jt_h_mulenumoutput))))