jordan_rectangle_crt_enumeration

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v P Q R T. ~(m=0) -> ~(n=0) -> (forall jt_divisor_rectenumcop. (exists jt_factor_rectenumcopa. (m)=(jt_divisor_rectenumcop)*jt_factor_rectenumcopa) -> (exists jt_factor_rectenumcopb. (n)=(jt_divisor_rectenumcop)*jt_factor_rectenumcopb) -> jt_divisor_rectenumcop=1) -> (((forall jt_i_enumleft. (exists jt_gap_enumleftsoundindex. jt_gap_enumleftsoundindex+S (jt_i_enumleft)=(u)) -> exists jt_b_enumleft jt_c_enumleft. ((((((exists fs_h_jt_enumleftsoundcode. fs_h_jt_enumleftsoundcode + S (jt_b_enumleft) = S ((S (jt_i_enumleft)) * B)) /\ exists fs_q_jt_enumleftsoundcode. A = fs_q_jt_enumleftsoundcode * S ((S (jt_i_enumleft)) * B) + (jt_b_enumleft))) /\ (((exists fs_h_jt_enumleftsoundscale. fs_h_jt_enumleftsoundscale + S (jt_c_enumleft) = S ((S (jt_i_enumleft)) * D)) /\ exists fs_q_jt_enumleftsoundscale. C = fs_q_jt_enumleftsoundscale * S ((S (jt_i_enumleft)) * D) + (jt_c_enumleft))))) /\ (((forall jt_index_enumleftbound. (exists jt_gap_enumleftboundindex. jt_gap_enumleftboundindex+S (jt_index_enumleftbound)=(k)) -> exists jt_value_enumleftbound. ((((exists fs_h_jt_enumleftboundat. fs_h_jt_enumleftboundat + S (jt_value_enumleftbound) = S ((S (jt_index_enumleftbound)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftboundat. jt_b_enumleft = fs_q_jt_enumleftboundat * S ((S (jt_index_enumleftbound)) * jt_c_enumleft) + (jt_value_enumleftbound))) /\ (exists jt_gap_enumleftboundvalue. jt_gap_enumleftboundvalue+S (jt_value_enumleftbound)=(m)))) /\ (forall jt_divisor_enumleftprimitive. (exists jt_factor_enumleftprimitivemodulus. (m)=(jt_divisor_enumleftprimitive)*jt_factor_enumleftprimitivemodulus) -> (forall jt_index_enumleftprimitivecoordinates jt_value_enumleftprimitivecoordinates. (exists jt_gap_enumleftprimitivecoordinatesindex. jt_gap_enumleftprimitivecoordinatesindex+S (jt_index_enumleftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_enumleftprimitivecoordinatesat. fs_h_jt_enumleftprimitivecoordinatesat + S (jt_value_enumleftprimitivecoordinates) = S ((S (jt_index_enumleftprimitivecoordinates)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftprimitivecoordinatesat. jt_b_enumleft = fs_q_jt_enumleftprimitivecoordinatesat * S ((S (jt_index_enumleftprimitivecoordinates)) * jt_c_enumleft) + (jt_value_enumleftprimitivecoordinates))) -> (exists jt_factor_enumleftprimitivecoordinatesdivides. (jt_value_enumleftprimitivecoordinates)=(jt_divisor_enumleftprimitive)*jt_factor_enumleftprimitivecoordinatesdivides)) -> jt_divisor_enumleftprimitive=1))))) /\ (((forall jt_b_enumleft jt_c_enumleft. (forall jt_index_enumleftinputbound. (exists jt_gap_enumleftinputboundindex. jt_gap_enumleftinputboundindex+S (jt_index_enumleftinputbound)=(k)) -> exists jt_value_enumleftinputbound. ((((exists fs_h_jt_enumleftinputboundat. fs_h_jt_enumleftinputboundat + S (jt_value_enumleftinputbound) = S ((S (jt_index_enumleftinputbound)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftinputboundat. jt_b_enumleft = fs_q_jt_enumleftinputboundat * S ((S (jt_index_enumleftinputbound)) * jt_c_enumleft) + (jt_value_enumleftinputbound))) /\ (exists jt_gap_enumleftinputboundvalue. jt_gap_enumleftinputboundvalue+S (jt_value_enumleftinputbound)=(m)))) -> (forall jt_divisor_enumleftinputprimitive. (exists jt_factor_enumleftinputprimitivemodulus. (m)=(jt_divisor_enumleftinputprimitive)*jt_factor_enumleftinputprimitivemodulus) -> (forall jt_index_enumleftinputprimitivecoordinates jt_value_enumleftinputprimitivecoordinates. (exists jt_gap_enumleftinputprimitivecoordinatesindex. jt_gap_enumleftinputprimitivecoordinatesindex+S (jt_index_enumleftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_enumleftinputprimitivecoordinatesat. fs_h_jt_enumleftinputprimitivecoordinatesat + S (jt_value_enumleftinputprimitivecoordinates) = S ((S (jt_index_enumleftinputprimitivecoordinates)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftinputprimitivecoordinatesat. jt_b_enumleft = fs_q_jt_enumleftinputprimitivecoordinatesat * S ((S (jt_index_enumleftinputprimitivecoordinates)) * jt_c_enumleft) + (jt_value_enumleftinputprimitivecoordinates))) -> (exists jt_factor_enumleftinputprimitivecoordinatesdivides. (jt_value_enumleftinputprimitivecoordinates)=(jt_divisor_enumleftinputprimitive)*jt_factor_enumleftinputprimitivecoordinatesdivides)) -> jt_divisor_enumleftinputprimitive=1) -> exists jt_i_enumleft jt_d_enumleft jt_e_enumleft. ((exists jt_gap_enumleftcompleteindex. jt_gap_enumleftcompleteindex+S (jt_i_enumleft)=(u)) /\ (((((((exists fs_h_jt_enumleftcompletecode. fs_h_jt_enumleftcompletecode + S (jt_d_enumleft) = S ((S (jt_i_enumleft)) * B)) /\ exists fs_q_jt_enumleftcompletecode. A = fs_q_jt_enumleftcompletecode * S ((S (jt_i_enumleft)) * B) + (jt_d_enumleft))) /\ (((exists fs_h_jt_enumleftcompletescale. fs_h_jt_enumleftcompletescale + S (jt_e_enumleft) = S ((S (jt_i_enumleft)) * D)) /\ exists fs_q_jt_enumleftcompletescale. C = fs_q_jt_enumleftcompletescale * S ((S (jt_i_enumleft)) * D) + (jt_e_enumleft))))) /\ (forall jt_index_enumleftrepresented jt_left_enumleftrepresented jt_right_enumleftrepresented. (exists jt_gap_enumleftrepresentedindex. jt_gap_enumleftrepresentedindex+S (jt_index_enumleftrepresented)=(k)) -> (((exists fs_h_jt_enumleftrepresentedleft. fs_h_jt_enumleftrepresentedleft + S (jt_left_enumleftrepresented) = S ((S (jt_index_enumleftrepresented)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftrepresentedleft. jt_b_enumleft = fs_q_jt_enumleftrepresentedleft * S ((S (jt_index_enumleftrepresented)) * jt_c_enumleft) + (jt_left_enumleftrepresented))) -> (((exists fs_h_jt_enumleftrepresentedright. fs_h_jt_enumleftrepresentedright + S (jt_right_enumleftrepresented) = S ((S (jt_index_enumleftrepresented)) * jt_e_enumleft)) /\ exists fs_q_jt_enumleftrepresentedright. jt_d_enumleft = fs_q_jt_enumleftrepresentedright * S ((S (jt_index_enumleftrepresented)) * jt_e_enumleft) + (jt_right_enumleftrepresented))) -> jt_left_enumleftrepresented=jt_right_enumleftrepresented))))) /\ (forall jt_i_enumleft jt_h_enumleft jt_b_enumleft jt_c_enumleft jt_d_enumleft jt_e_enumleft. (exists jt_gap_enumleftfirstindex. jt_gap_enumleftfirstindex+S (jt_i_enumleft)=(u)) -> (exists jt_gap_enumleftsecondindex. jt_gap_enumleftsecondindex+S (jt_h_enumleft)=(u)) -> (((((exists fs_h_jt_enumleftfirstcode. fs_h_jt_enumleftfirstcode + S (jt_b_enumleft) = S ((S (jt_i_enumleft)) * B)) /\ exists fs_q_jt_enumleftfirstcode. A = fs_q_jt_enumleftfirstcode * S ((S (jt_i_enumleft)) * B) + (jt_b_enumleft))) /\ (((exists fs_h_jt_enumleftfirstscale. fs_h_jt_enumleftfirstscale + S (jt_c_enumleft) = S ((S (jt_i_enumleft)) * D)) /\ exists fs_q_jt_enumleftfirstscale. C = fs_q_jt_enumleftfirstscale * S ((S (jt_i_enumleft)) * D) + (jt_c_enumleft))))) -> (((((exists fs_h_jt_enumleftsecondcode. fs_h_jt_enumleftsecondcode + S (jt_d_enumleft) = S ((S (jt_h_enumleft)) * B)) /\ exists fs_q_jt_enumleftsecondcode. A = fs_q_jt_enumleftsecondcode * S ((S (jt_h_enumleft)) * B) + (jt_d_enumleft))) /\ (((exists fs_h_jt_enumleftsecondscale. fs_h_jt_enumleftsecondscale + S (jt_e_enumleft) = S ((S (jt_h_enumleft)) * D)) /\ exists fs_q_jt_enumleftsecondscale. C = fs_q_jt_enumleftsecondscale * S ((S (jt_h_enumleft)) * D) + (jt_e_enumleft))))) -> (forall jt_index_enumleftsame jt_left_enumleftsame jt_right_enumleftsame. (exists jt_gap_enumleftsameindex. jt_gap_enumleftsameindex+S (jt_index_enumleftsame)=(k)) -> (((exists fs_h_jt_enumleftsameleft. fs_h_jt_enumleftsameleft + S (jt_left_enumleftsame) = S ((S (jt_index_enumleftsame)) * jt_c_enumleft)) /\ exists fs_q_jt_enumleftsameleft. jt_b_enumleft = fs_q_jt_enumleftsameleft * S ((S (jt_index_enumleftsame)) * jt_c_enumleft) + (jt_left_enumleftsame))) -> (((exists fs_h_jt_enumleftsameright. fs_h_jt_enumleftsameright + S (jt_right_enumleftsame) = S ((S (jt_index_enumleftsame)) * jt_e_enumleft)) /\ exists fs_q_jt_enumleftsameright. jt_d_enumleft = fs_q_jt_enumleftsameright * S ((S (jt_index_enumleftsame)) * jt_e_enumleft) + (jt_right_enumleftsame))) -> jt_left_enumleftsame=jt_right_enumleftsame) -> jt_i_enumleft=jt_h_enumleft))))) -> (((forall jt_i_enumright. (exists jt_gap_enumrightsoundindex. jt_gap_enumrightsoundindex+S (jt_i_enumright)=(v)) -> exists jt_b_enumright jt_c_enumright. ((((((exists fs_h_jt_enumrightsoundcode. fs_h_jt_enumrightsoundcode + S (jt_b_enumright) = S ((S (jt_i_enumright)) * F)) /\ exists fs_q_jt_enumrightsoundcode. E = fs_q_jt_enumrightsoundcode * S ((S (jt_i_enumright)) * F) + (jt_b_enumright))) /\ (((exists fs_h_jt_enumrightsoundscale. fs_h_jt_enumrightsoundscale + S (jt_c_enumright) = S ((S (jt_i_enumright)) * H)) /\ exists fs_q_jt_enumrightsoundscale. G = fs_q_jt_enumrightsoundscale * S ((S (jt_i_enumright)) * H) + (jt_c_enumright))))) /\ (((forall jt_index_enumrightbound. (exists jt_gap_enumrightboundindex. jt_gap_enumrightboundindex+S (jt_index_enumrightbound)=(k)) -> exists jt_value_enumrightbound. ((((exists fs_h_jt_enumrightboundat. fs_h_jt_enumrightboundat + S (jt_value_enumrightbound) = S ((S (jt_index_enumrightbound)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightboundat. jt_b_enumright = fs_q_jt_enumrightboundat * S ((S (jt_index_enumrightbound)) * jt_c_enumright) + (jt_value_enumrightbound))) /\ (exists jt_gap_enumrightboundvalue. jt_gap_enumrightboundvalue+S (jt_value_enumrightbound)=(n)))) /\ (forall jt_divisor_enumrightprimitive. (exists jt_factor_enumrightprimitivemodulus. (n)=(jt_divisor_enumrightprimitive)*jt_factor_enumrightprimitivemodulus) -> (forall jt_index_enumrightprimitivecoordinates jt_value_enumrightprimitivecoordinates. (exists jt_gap_enumrightprimitivecoordinatesindex. jt_gap_enumrightprimitivecoordinatesindex+S (jt_index_enumrightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_enumrightprimitivecoordinatesat. fs_h_jt_enumrightprimitivecoordinatesat + S (jt_value_enumrightprimitivecoordinates) = S ((S (jt_index_enumrightprimitivecoordinates)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightprimitivecoordinatesat. jt_b_enumright = fs_q_jt_enumrightprimitivecoordinatesat * S ((S (jt_index_enumrightprimitivecoordinates)) * jt_c_enumright) + (jt_value_enumrightprimitivecoordinates))) -> (exists jt_factor_enumrightprimitivecoordinatesdivides. (jt_value_enumrightprimitivecoordinates)=(jt_divisor_enumrightprimitive)*jt_factor_enumrightprimitivecoordinatesdivides)) -> jt_divisor_enumrightprimitive=1))))) /\ (((forall jt_b_enumright jt_c_enumright. (forall jt_index_enumrightinputbound. (exists jt_gap_enumrightinputboundindex. jt_gap_enumrightinputboundindex+S (jt_index_enumrightinputbound)=(k)) -> exists jt_value_enumrightinputbound. ((((exists fs_h_jt_enumrightinputboundat. fs_h_jt_enumrightinputboundat + S (jt_value_enumrightinputbound) = S ((S (jt_index_enumrightinputbound)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightinputboundat. jt_b_enumright = fs_q_jt_enumrightinputboundat * S ((S (jt_index_enumrightinputbound)) * jt_c_enumright) + (jt_value_enumrightinputbound))) /\ (exists jt_gap_enumrightinputboundvalue. jt_gap_enumrightinputboundvalue+S (jt_value_enumrightinputbound)=(n)))) -> (forall jt_divisor_enumrightinputprimitive. (exists jt_factor_enumrightinputprimitivemodulus. (n)=(jt_divisor_enumrightinputprimitive)*jt_factor_enumrightinputprimitivemodulus) -> (forall jt_index_enumrightinputprimitivecoordinates jt_value_enumrightinputprimitivecoordinates. (exists jt_gap_enumrightinputprimitivecoordinatesindex. jt_gap_enumrightinputprimitivecoordinatesindex+S (jt_index_enumrightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_enumrightinputprimitivecoordinatesat. fs_h_jt_enumrightinputprimitivecoordinatesat + S (jt_value_enumrightinputprimitivecoordinates) = S ((S (jt_index_enumrightinputprimitivecoordinates)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightinputprimitivecoordinatesat. jt_b_enumright = fs_q_jt_enumrightinputprimitivecoordinatesat * S ((S (jt_index_enumrightinputprimitivecoordinates)) * jt_c_enumright) + (jt_value_enumrightinputprimitivecoordinates))) -> (exists jt_factor_enumrightinputprimitivecoordinatesdivides. (jt_value_enumrightinputprimitivecoordinates)=(jt_divisor_enumrightinputprimitive)*jt_factor_enumrightinputprimitivecoordinatesdivides)) -> jt_divisor_enumrightinputprimitive=1) -> exists jt_i_enumright jt_d_enumright jt_e_enumright. ((exists jt_gap_enumrightcompleteindex. jt_gap_enumrightcompleteindex+S (jt_i_enumright)=(v)) /\ (((((((exists fs_h_jt_enumrightcompletecode. fs_h_jt_enumrightcompletecode + S (jt_d_enumright) = S ((S (jt_i_enumright)) * F)) /\ exists fs_q_jt_enumrightcompletecode. E = fs_q_jt_enumrightcompletecode * S ((S (jt_i_enumright)) * F) + (jt_d_enumright))) /\ (((exists fs_h_jt_enumrightcompletescale. fs_h_jt_enumrightcompletescale + S (jt_e_enumright) = S ((S (jt_i_enumright)) * H)) /\ exists fs_q_jt_enumrightcompletescale. G = fs_q_jt_enumrightcompletescale * S ((S (jt_i_enumright)) * H) + (jt_e_enumright))))) /\ (forall jt_index_enumrightrepresented jt_left_enumrightrepresented jt_right_enumrightrepresented. (exists jt_gap_enumrightrepresentedindex. jt_gap_enumrightrepresentedindex+S (jt_index_enumrightrepresented)=(k)) -> (((exists fs_h_jt_enumrightrepresentedleft. fs_h_jt_enumrightrepresentedleft + S (jt_left_enumrightrepresented) = S ((S (jt_index_enumrightrepresented)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightrepresentedleft. jt_b_enumright = fs_q_jt_enumrightrepresentedleft * S ((S (jt_index_enumrightrepresented)) * jt_c_enumright) + (jt_left_enumrightrepresented))) -> (((exists fs_h_jt_enumrightrepresentedright. fs_h_jt_enumrightrepresentedright + S (jt_right_enumrightrepresented) = S ((S (jt_index_enumrightrepresented)) * jt_e_enumright)) /\ exists fs_q_jt_enumrightrepresentedright. jt_d_enumright = fs_q_jt_enumrightrepresentedright * S ((S (jt_index_enumrightrepresented)) * jt_e_enumright) + (jt_right_enumrightrepresented))) -> jt_left_enumrightrepresented=jt_right_enumrightrepresented))))) /\ (forall jt_i_enumright jt_h_enumright jt_b_enumright jt_c_enumright jt_d_enumright jt_e_enumright. (exists jt_gap_enumrightfirstindex. jt_gap_enumrightfirstindex+S (jt_i_enumright)=(v)) -> (exists jt_gap_enumrightsecondindex. jt_gap_enumrightsecondindex+S (jt_h_enumright)=(v)) -> (((((exists fs_h_jt_enumrightfirstcode. fs_h_jt_enumrightfirstcode + S (jt_b_enumright) = S ((S (jt_i_enumright)) * F)) /\ exists fs_q_jt_enumrightfirstcode. E = fs_q_jt_enumrightfirstcode * S ((S (jt_i_enumright)) * F) + (jt_b_enumright))) /\ (((exists fs_h_jt_enumrightfirstscale. fs_h_jt_enumrightfirstscale + S (jt_c_enumright) = S ((S (jt_i_enumright)) * H)) /\ exists fs_q_jt_enumrightfirstscale. G = fs_q_jt_enumrightfirstscale * S ((S (jt_i_enumright)) * H) + (jt_c_enumright))))) -> (((((exists fs_h_jt_enumrightsecondcode. fs_h_jt_enumrightsecondcode + S (jt_d_enumright) = S ((S (jt_h_enumright)) * F)) /\ exists fs_q_jt_enumrightsecondcode. E = fs_q_jt_enumrightsecondcode * S ((S (jt_h_enumright)) * F) + (jt_d_enumright))) /\ (((exists fs_h_jt_enumrightsecondscale. fs_h_jt_enumrightsecondscale + S (jt_e_enumright) = S ((S (jt_h_enumright)) * H)) /\ exists fs_q_jt_enumrightsecondscale. G = fs_q_jt_enumrightsecondscale * S ((S (jt_h_enumright)) * H) + (jt_e_enumright))))) -> (forall jt_index_enumrightsame jt_left_enumrightsame jt_right_enumrightsame. (exists jt_gap_enumrightsameindex. jt_gap_enumrightsameindex+S (jt_index_enumrightsame)=(k)) -> (((exists fs_h_jt_enumrightsameleft. fs_h_jt_enumrightsameleft + S (jt_left_enumrightsame) = S ((S (jt_index_enumrightsame)) * jt_c_enumright)) /\ exists fs_q_jt_enumrightsameleft. jt_b_enumright = fs_q_jt_enumrightsameleft * S ((S (jt_index_enumrightsame)) * jt_c_enumright) + (jt_left_enumrightsame))) -> (((exists fs_h_jt_enumrightsameright. fs_h_jt_enumrightsameright + S (jt_right_enumrightsame) = S ((S (jt_index_enumrightsame)) * jt_e_enumright)) /\ exists fs_q_jt_enumrightsameright. jt_d_enumright = fs_q_jt_enumrightsameright * S ((S (jt_index_enumrightsame)) * jt_e_enumright) + (jt_right_enumrightsame))) -> jt_left_enumrightsame=jt_right_enumrightsame) -> jt_i_enumright=jt_h_enumright))))) -> (forall jt_index_enumrect. (exists jt_gap_enumrectindex. jt_gap_enumrectindex+S (jt_index_enumrect)=(u*v)) -> exists jt_row_enumrect jt_column_enumrect jt_b_enumrect jt_c_enumrect jt_d_enumrect jt_e_enumrect jt_f_enumrect jt_g_enumrect. ((exists jt_gap_enumrectrow. jt_gap_enumrectrow+S (jt_row_enumrect)=(u)) /\ (((exists jt_gap_enumrectcolumn. jt_gap_enumrectcolumn+S (jt_column_enumrect)=(v)) /\ (((jt_index_enumrect=(v)*jt_row_enumrect+jt_column_enumrect) /\ (((((((exists fs_h_jt_enumrectleftcode. fs_h_jt_enumrectleftcode + S (jt_b_enumrect) = S ((S (jt_row_enumrect)) * B)) /\ exists fs_q_jt_enumrectleftcode. A = fs_q_jt_enumrectleftcode * S ((S (jt_row_enumrect)) * B) + (jt_b_enumrect))) /\ (((exists fs_h_jt_enumrectleftscale. fs_h_jt_enumrectleftscale + S (jt_c_enumrect) = S ((S (jt_row_enumrect)) * D)) /\ exists fs_q_jt_enumrectleftscale. C = fs_q_jt_enumrectleftscale * S ((S (jt_row_enumrect)) * D) + (jt_c_enumrect))))) /\ (((((((exists fs_h_jt_enumrectrightcode. fs_h_jt_enumrectrightcode + S (jt_d_enumrect) = S ((S (jt_column_enumrect)) * F)) /\ exists fs_q_jt_enumrectrightcode. E = fs_q_jt_enumrectrightcode * S ((S (jt_column_enumrect)) * F) + (jt_d_enumrect))) /\ (((exists fs_h_jt_enumrectrightscale. fs_h_jt_enumrectrightscale + S (jt_e_enumrect) = S ((S (jt_column_enumrect)) * H)) /\ exists fs_q_jt_enumrectrightscale. G = fs_q_jt_enumrectrightscale * S ((S (jt_column_enumrect)) * H) + (jt_e_enumrect))))) /\ (((((((exists fs_h_jt_enumrectoutputcode. fs_h_jt_enumrectoutputcode + S (jt_f_enumrect) = S ((S (jt_index_enumrect)) * Q)) /\ exists fs_q_jt_enumrectoutputcode. P = fs_q_jt_enumrectoutputcode * S ((S (jt_index_enumrect)) * Q) + (jt_f_enumrect))) /\ (((exists fs_h_jt_enumrectoutputscale. fs_h_jt_enumrectoutputscale + S (jt_g_enumrect) = S ((S (jt_index_enumrect)) * T)) /\ exists fs_q_jt_enumrectoutputscale. R = fs_q_jt_enumrectoutputscale * S ((S (jt_index_enumrect)) * T) + (jt_g_enumrect))))) /\ (((((forall jt_index_enumrectcrtbound. (exists jt_gap_enumrectcrtboundindex. jt_gap_enumrectcrtboundindex+S (jt_index_enumrectcrtbound)=(k)) -> exists jt_value_enumrectcrtbound. ((((exists fs_h_jt_enumrectcrtboundat. fs_h_jt_enumrectcrtboundat + S (jt_value_enumrectcrtbound) = S ((S (jt_index_enumrectcrtbound)) * jt_g_enumrect)) /\ exists fs_q_jt_enumrectcrtboundat. jt_f_enumrect = fs_q_jt_enumrectcrtboundat * S ((S (jt_index_enumrectcrtbound)) * jt_g_enumrect) + (jt_value_enumrectcrtbound))) /\ (exists jt_gap_enumrectcrtboundvalue. jt_gap_enumrectcrtboundvalue+S (jt_value_enumrectcrtbound)=(m*n)))) /\ (((forall jt_index_enumrectcrtleft jt_left_enumrectcrtleft jt_right_enumrectcrtleft. (exists jt_gap_enumrectcrtleftindex. jt_gap_enumrectcrtleftindex+S (jt_index_enumrectcrtleft)=(k)) -> (((exists fs_h_jt_enumrectcrtleftleft. fs_h_jt_enumrectcrtleftleft + S (jt_left_enumrectcrtleft) = S ((S (jt_index_enumrectcrtleft)) * jt_g_enumrect)) /\ exists fs_q_jt_enumrectcrtleftleft. jt_f_enumrect = fs_q_jt_enumrectcrtleftleft * S ((S (jt_index_enumrectcrtleft)) * jt_g_enumrect) + (jt_left_enumrectcrtleft))) -> (((exists fs_h_jt_enumrectcrtleftright. fs_h_jt_enumrectcrtleftright + S (jt_right_enumrectcrtleft) = S ((S (jt_index_enumrectcrtleft)) * jt_c_enumrect)) /\ exists fs_q_jt_enumrectcrtleftright. jt_b_enumrect = fs_q_jt_enumrectcrtleftright * S ((S (jt_index_enumrectcrtleft)) * jt_c_enumrect) + (jt_right_enumrectcrtleft))) -> (exists jt_left_enumrectcrtleftmod jt_right_enumrectcrtleftmod. (jt_left_enumrectcrtleft)+(m)*jt_left_enumrectcrtleftmod=(jt_right_enumrectcrtleft)+(m)*jt_right_enumrectcrtleftmod)) /\ (forall jt_index_enumrectcrtright jt_left_enumrectcrtright jt_right_enumrectcrtright. (exists jt_gap_enumrectcrtrightindex. jt_gap_enumrectcrtrightindex+S (jt_index_enumrectcrtright)=(k)) -> (((exists fs_h_jt_enumrectcrtrightleft. fs_h_jt_enumrectcrtrightleft + S (jt_left_enumrectcrtright) = S ((S (jt_index_enumrectcrtright)) * jt_g_enumrect)) /\ exists fs_q_jt_enumrectcrtrightleft. jt_f_enumrect = fs_q_jt_enumrectcrtrightleft * S ((S (jt_index_enumrectcrtright)) * jt_g_enumrect) + (jt_left_enumrectcrtright))) -> (((exists fs_h_jt_enumrectcrtrightright. fs_h_jt_enumrectcrtrightright + S (jt_right_enumrectcrtright) = S ((S (jt_index_enumrectcrtright)) * jt_e_enumrect)) /\ exists fs_q_jt_enumrectcrtrightright. jt_d_enumrect = fs_q_jt_enumrectcrtrightright * S ((S (jt_index_enumrectcrtright)) * jt_e_enumrect) + (jt_right_enumrectcrtright))) -> (exists jt_left_enumrectcrtrightmod jt_right_enumrectcrtrightmod. (jt_left_enumrectcrtright)+(n)*jt_left_enumrectcrtrightmod=(jt_right_enumrectcrtright)+(n)*jt_right_enumrectcrtrightmod)))))) /\ (forall jt_divisor_enumrectprimitive. (exists jt_factor_enumrectprimitivemodulus. (m*n)=(jt_divisor_enumrectprimitive)*jt_factor_enumrectprimitivemodulus) -> (forall jt_index_enumrectprimitivecoordinates jt_value_enumrectprimitivecoordinates. (exists jt_gap_enumrectprimitivecoordinatesindex. jt_gap_enumrectprimitivecoordinatesindex+S (jt_index_enumrectprimitivecoordinates)=(k)) -> (((exists fs_h_jt_enumrectprimitivecoordinatesat. fs_h_jt_enumrectprimitivecoordinatesat + S (jt_value_enumrectprimitivecoordinates) = S ((S (jt_index_enumrectprimitivecoordinates)) * jt_g_enumrect)) /\ exists fs_q_jt_enumrectprimitivecoordinatesat. jt_f_enumrect = fs_q_jt_enumrectprimitivecoordinatesat * S ((S (jt_index_enumrectprimitivecoordinates)) * jt_g_enumrect) + (jt_value_enumrectprimitivecoordinates))) -> (exists jt_factor_enumrectprimitivecoordinatesdivides. (jt_value_enumrectprimitivecoordinates)=(jt_divisor_enumrectprimitive)*jt_factor_enumrectprimitivecoordinatesdivides)) -> jt_divisor_enumrectprimitive=1))))))))))))))) -> ((forall jt_i_productenum. (exists jt_gap_productenumsoundindex. jt_gap_productenumsoundindex+S (jt_i_productenum)=(u*v)) -> exists jt_b_productenum jt_c_productenum. ((((((exists fs_h_jt_productenumsoundcode. fs_h_jt_productenumsoundcode + S (jt_b_productenum) = S ((S (jt_i_productenum)) * Q)) /\ exists fs_q_jt_productenumsoundcode. P = fs_q_jt_productenumsoundcode * S ((S (jt_i_productenum)) * Q) + (jt_b_productenum))) /\ (((exists fs_h_jt_productenumsoundscale. fs_h_jt_productenumsoundscale + S (jt_c_productenum) = S ((S (jt_i_productenum)) * T)) /\ exists fs_q_jt_productenumsoundscale. R = fs_q_jt_productenumsoundscale * S ((S (jt_i_productenum)) * T) + (jt_c_productenum))))) /\ (((forall jt_index_productenumbound. (exists jt_gap_productenumboundindex. jt_gap_productenumboundindex+S (jt_index_productenumbound)=(k)) -> exists jt_value_productenumbound. ((((exists fs_h_jt_productenumboundat. fs_h_jt_productenumboundat + S (jt_value_productenumbound) = S ((S (jt_index_productenumbound)) * jt_c_productenum)) /\ exists fs_q_jt_productenumboundat. jt_b_productenum = fs_q_jt_productenumboundat * S ((S (jt_index_productenumbound)) * jt_c_productenum) + (jt_value_productenumbound))) /\ (exists jt_gap_productenumboundvalue. jt_gap_productenumboundvalue+S (jt_value_productenumbound)=(m*n)))) /\ (forall jt_divisor_productenumprimitive. (exists jt_factor_productenumprimitivemodulus. (m*n)=(jt_divisor_productenumprimitive)*jt_factor_productenumprimitivemodulus) -> (forall jt_index_productenumprimitivecoordinates jt_value_productenumprimitivecoordinates. (exists jt_gap_productenumprimitivecoordinatesindex. jt_gap_productenumprimitivecoordinatesindex+S (jt_index_productenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_productenumprimitivecoordinatesat. fs_h_jt_productenumprimitivecoordinatesat + S (jt_value_productenumprimitivecoordinates) = S ((S (jt_index_productenumprimitivecoordinates)) * jt_c_productenum)) /\ exists fs_q_jt_productenumprimitivecoordinatesat. jt_b_productenum = fs_q_jt_productenumprimitivecoordinatesat * S ((S (jt_index_productenumprimitivecoordinates)) * jt_c_productenum) + (jt_value_productenumprimitivecoordinates))) -> (exists jt_factor_productenumprimitivecoordinatesdivides. (jt_value_productenumprimitivecoordinates)=(jt_divisor_productenumprimitive)*jt_factor_productenumprimitivecoordinatesdivides)) -> jt_divisor_productenumprimitive=1))))) /\ (((forall jt_b_productenum jt_c_productenum. (forall jt_index_productenuminputbound. (exists jt_gap_productenuminputboundindex. jt_gap_productenuminputboundindex+S (jt_index_productenuminputbound)=(k)) -> exists jt_value_productenuminputbound. ((((exists fs_h_jt_productenuminputboundat. fs_h_jt_productenuminputboundat + S (jt_value_productenuminputbound) = S ((S (jt_index_productenuminputbound)) * jt_c_productenum)) /\ exists fs_q_jt_productenuminputboundat. jt_b_productenum = fs_q_jt_productenuminputboundat * S ((S (jt_index_productenuminputbound)) * jt_c_productenum) + (jt_value_productenuminputbound))) /\ (exists jt_gap_productenuminputboundvalue. jt_gap_productenuminputboundvalue+S (jt_value_productenuminputbound)=(m*n)))) -> (forall jt_divisor_productenuminputprimitive. (exists jt_factor_productenuminputprimitivemodulus. (m*n)=(jt_divisor_productenuminputprimitive)*jt_factor_productenuminputprimitivemodulus) -> (forall jt_index_productenuminputprimitivecoordinates jt_value_productenuminputprimitivecoordinates. (exists jt_gap_productenuminputprimitivecoordinatesindex. jt_gap_productenuminputprimitivecoordinatesindex+S (jt_index_productenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_productenuminputprimitivecoordinatesat. fs_h_jt_productenuminputprimitivecoordinatesat + S (jt_value_productenuminputprimitivecoordinates) = S ((S (jt_index_productenuminputprimitivecoordinates)) * jt_c_productenum)) /\ exists fs_q_jt_productenuminputprimitivecoordinatesat. jt_b_productenum = fs_q_jt_productenuminputprimitivecoordinatesat * S ((S (jt_index_productenuminputprimitivecoordinates)) * jt_c_productenum) + (jt_value_productenuminputprimitivecoordinates))) -> (exists jt_factor_productenuminputprimitivecoordinatesdivides. (jt_value_productenuminputprimitivecoordinates)=(jt_divisor_productenuminputprimitive)*jt_factor_productenuminputprimitivecoordinatesdivides)) -> jt_divisor_productenuminputprimitive=1) -> exists jt_i_productenum jt_d_productenum jt_e_productenum. ((exists jt_gap_productenumcompleteindex. jt_gap_productenumcompleteindex+S (jt_i_productenum)=(u*v)) /\ (((((((exists fs_h_jt_productenumcompletecode. fs_h_jt_productenumcompletecode + S (jt_d_productenum) = S ((S (jt_i_productenum)) * Q)) /\ exists fs_q_jt_productenumcompletecode. P = fs_q_jt_productenumcompletecode * S ((S (jt_i_productenum)) * Q) + (jt_d_productenum))) /\ (((exists fs_h_jt_productenumcompletescale. fs_h_jt_productenumcompletescale + S (jt_e_productenum) = S ((S (jt_i_productenum)) * T)) /\ exists fs_q_jt_productenumcompletescale. R = fs_q_jt_productenumcompletescale * S ((S (jt_i_productenum)) * T) + (jt_e_productenum))))) /\ (forall jt_index_productenumrepresented jt_left_productenumrepresented jt_right_productenumrepresented. (exists jt_gap_productenumrepresentedindex. jt_gap_productenumrepresentedindex+S (jt_index_productenumrepresented)=(k)) -> (((exists fs_h_jt_productenumrepresentedleft. fs_h_jt_productenumrepresentedleft + S (jt_left_productenumrepresented) = S ((S (jt_index_productenumrepresented)) * jt_c_productenum)) /\ exists fs_q_jt_productenumrepresentedleft. jt_b_productenum = fs_q_jt_productenumrepresentedleft * S ((S (jt_index_productenumrepresented)) * jt_c_productenum) + (jt_left_productenumrepresented))) -> (((exists fs_h_jt_productenumrepresentedright. fs_h_jt_productenumrepresentedright + S (jt_right_productenumrepresented) = S ((S (jt_index_productenumrepresented)) * jt_e_productenum)) /\ exists fs_q_jt_productenumrepresentedright. jt_d_productenum = fs_q_jt_productenumrepresentedright * S ((S (jt_index_productenumrepresented)) * jt_e_productenum) + (jt_right_productenumrepresented))) -> jt_left_productenumrepresented=jt_right_productenumrepresented))))) /\ (forall jt_i_productenum jt_h_productenum jt_b_productenum jt_c_productenum jt_d_productenum jt_e_productenum. (exists jt_gap_productenumfirstindex. jt_gap_productenumfirstindex+S (jt_i_productenum)=(u*v)) -> (exists jt_gap_productenumsecondindex. jt_gap_productenumsecondindex+S (jt_h_productenum)=(u*v)) -> (((((exists fs_h_jt_productenumfirstcode. fs_h_jt_productenumfirstcode + S (jt_b_productenum) = S ((S (jt_i_productenum)) * Q)) /\ exists fs_q_jt_productenumfirstcode. P = fs_q_jt_productenumfirstcode * S ((S (jt_i_productenum)) * Q) + (jt_b_productenum))) /\ (((exists fs_h_jt_productenumfirstscale. fs_h_jt_productenumfirstscale + S (jt_c_productenum) = S ((S (jt_i_productenum)) * T)) /\ exists fs_q_jt_productenumfirstscale. R = fs_q_jt_productenumfirstscale * S ((S (jt_i_productenum)) * T) + (jt_c_productenum))))) -> (((((exists fs_h_jt_productenumsecondcode. fs_h_jt_productenumsecondcode + S (jt_d_productenum) = S ((S (jt_h_productenum)) * Q)) /\ exists fs_q_jt_productenumsecondcode. P = fs_q_jt_productenumsecondcode * S ((S (jt_h_productenum)) * Q) + (jt_d_productenum))) /\ (((exists fs_h_jt_productenumsecondscale. fs_h_jt_productenumsecondscale + S (jt_e_productenum) = S ((S (jt_h_productenum)) * T)) /\ exists fs_q_jt_productenumsecondscale. R = fs_q_jt_productenumsecondscale * S ((S (jt_h_productenum)) * T) + (jt_e_productenum))))) -> (forall jt_index_productenumsame jt_left_productenumsame jt_right_productenumsame. (exists jt_gap_productenumsameindex. jt_gap_productenumsameindex+S (jt_index_productenumsame)=(k)) -> (((exists fs_h_jt_productenumsameleft. fs_h_jt_productenumsameleft + S (jt_left_productenumsame) = S ((S (jt_index_productenumsame)) * jt_c_productenum)) /\ exists fs_q_jt_productenumsameleft. jt_b_productenum = fs_q_jt_productenumsameleft * S ((S (jt_index_productenumsame)) * jt_c_productenum) + (jt_left_productenumsame))) -> (((exists fs_h_jt_productenumsameright. fs_h_jt_productenumsameright + S (jt_right_productenumsame) = S ((S (jt_index_productenumsame)) * jt_e_productenum)) /\ exists fs_q_jt_productenumsameright. jt_d_productenum = fs_q_jt_productenumsameright * S ((S (jt_index_productenumsame)) * jt_e_productenum) + (jt_right_productenumsame))) -> jt_left_productenumsame=jt_right_productenumsame) -> jt_i_productenum=jt_h_productenum))))