jordan_rectangle_crt_covers

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v P Q R T b c. ~(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_index_coverbound. (exists jt_gap_coverboundindex. jt_gap_coverboundindex+S (jt_index_coverbound)=(k)) -> exists jt_value_coverbound. ((((exists fs_h_jt_coverboundat. fs_h_jt_coverboundat + S (jt_value_coverbound) = S ((S (jt_index_coverbound)) * c)) /\ exists fs_q_jt_coverboundat. b = fs_q_jt_coverboundat * S ((S (jt_index_coverbound)) * c) + (jt_value_coverbound))) /\ (exists jt_gap_coverboundvalue. jt_gap_coverboundvalue+S (jt_value_coverbound)=(m*n)))) -> (forall jt_divisor_coverprim. (exists jt_factor_coverprimmodulus. (m*n)=(jt_divisor_coverprim)*jt_factor_coverprimmodulus) -> (forall jt_index_coverprimcoordinates jt_value_coverprimcoordinates. (exists jt_gap_coverprimcoordinatesindex. jt_gap_coverprimcoordinatesindex+S (jt_index_coverprimcoordinates)=(k)) -> (((exists fs_h_jt_coverprimcoordinatesat. fs_h_jt_coverprimcoordinatesat + S (jt_value_coverprimcoordinates) = S ((S (jt_index_coverprimcoordinates)) * c)) /\ exists fs_q_jt_coverprimcoordinatesat. b = fs_q_jt_coverprimcoordinatesat * S ((S (jt_index_coverprimcoordinates)) * c) + (jt_value_coverprimcoordinates))) -> (exists jt_factor_coverprimcoordinatesdivides. (jt_value_coverprimcoordinates)=(jt_divisor_coverprim)*jt_factor_coverprimcoordinatesdivides)) -> jt_divisor_coverprim=1) -> (exists jt_index_coverlisted jt_code_coverlisted jt_scale_coverlisted. ((exists jt_gap_coverlistedindex. jt_gap_coverlistedindex+S (jt_index_coverlisted)=(u*v)) /\ (((((((exists fs_h_jt_coverlistedcode. fs_h_jt_coverlistedcode + S (jt_code_coverlisted) = S ((S (jt_index_coverlisted)) * Q)) /\ exists fs_q_jt_coverlistedcode. P = fs_q_jt_coverlistedcode * S ((S (jt_index_coverlisted)) * Q) + (jt_code_coverlisted))) /\ (((exists fs_h_jt_coverlistedscale. fs_h_jt_coverlistedscale + S (jt_scale_coverlisted) = S ((S (jt_index_coverlisted)) * T)) /\ exists fs_q_jt_coverlistedscale. R = fs_q_jt_coverlistedscale * S ((S (jt_index_coverlisted)) * T) + (jt_scale_coverlisted))))) /\ (forall jt_index_coverlistedequal jt_left_coverlistedequal jt_right_coverlistedequal. (exists jt_gap_coverlistedequalindex. jt_gap_coverlistedequalindex+S (jt_index_coverlistedequal)=(k)) -> (((exists fs_h_jt_coverlistedequalleft. fs_h_jt_coverlistedequalleft + S (jt_left_coverlistedequal) = S ((S (jt_index_coverlistedequal)) * c)) /\ exists fs_q_jt_coverlistedequalleft. b = fs_q_jt_coverlistedequalleft * S ((S (jt_index_coverlistedequal)) * c) + (jt_left_coverlistedequal))) -> (((exists fs_h_jt_coverlistedequalright. fs_h_jt_coverlistedequalright + S (jt_right_coverlistedequal) = S ((S (jt_index_coverlistedequal)) * jt_scale_coverlisted)) /\ exists fs_q_jt_coverlistedequalright. jt_code_coverlisted = fs_q_jt_coverlistedequalright * S ((S (jt_index_coverlistedequal)) * jt_scale_coverlisted) + (jt_right_coverlistedequal))) -> jt_left_coverlistedequal=jt_right_coverlistedequal)))))