jordan_rectangle_crt_exists

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v. ~(m=0) -> ~(n=0) -> (forall jt_divisor_rectexistscop. (exists jt_factor_rectexistscopa. (m)=(jt_divisor_rectexistscop)*jt_factor_rectexistscopa) -> (exists jt_factor_rectexistscopb. (n)=(jt_divisor_rectexistscop)*jt_factor_rectexistscopb) -> jt_divisor_rectexistscop=1) -> (((forall jt_i_rectexistsleft. (exists jt_gap_rectexistsleftsoundindex. jt_gap_rectexistsleftsoundindex+S (jt_i_rectexistsleft)=(u)) -> exists jt_b_rectexistsleft jt_c_rectexistsleft. ((((((exists fs_h_jt_rectexistsleftsoundcode. fs_h_jt_rectexistsleftsoundcode + S (jt_b_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * B)) /\ exists fs_q_jt_rectexistsleftsoundcode. A = fs_q_jt_rectexistsleftsoundcode * S ((S (jt_i_rectexistsleft)) * B) + (jt_b_rectexistsleft))) /\ (((exists fs_h_jt_rectexistsleftsoundscale. fs_h_jt_rectexistsleftsoundscale + S (jt_c_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * D)) /\ exists fs_q_jt_rectexistsleftsoundscale. C = fs_q_jt_rectexistsleftsoundscale * S ((S (jt_i_rectexistsleft)) * D) + (jt_c_rectexistsleft))))) /\ (((forall jt_index_rectexistsleftbound. (exists jt_gap_rectexistsleftboundindex. jt_gap_rectexistsleftboundindex+S (jt_index_rectexistsleftbound)=(k)) -> exists jt_value_rectexistsleftbound. ((((exists fs_h_jt_rectexistsleftboundat. fs_h_jt_rectexistsleftboundat + S (jt_value_rectexistsleftbound) = S ((S (jt_index_rectexistsleftbound)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftboundat. jt_b_rectexistsleft = fs_q_jt_rectexistsleftboundat * S ((S (jt_index_rectexistsleftbound)) * jt_c_rectexistsleft) + (jt_value_rectexistsleftbound))) /\ (exists jt_gap_rectexistsleftboundvalue. jt_gap_rectexistsleftboundvalue+S (jt_value_rectexistsleftbound)=(m)))) /\ (forall jt_divisor_rectexistsleftprimitive. (exists jt_factor_rectexistsleftprimitivemodulus. (m)=(jt_divisor_rectexistsleftprimitive)*jt_factor_rectexistsleftprimitivemodulus) -> (forall jt_index_rectexistsleftprimitivecoordinates jt_value_rectexistsleftprimitivecoordinates. (exists jt_gap_rectexistsleftprimitivecoordinatesindex. jt_gap_rectexistsleftprimitivecoordinatesindex+S (jt_index_rectexistsleftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectexistsleftprimitivecoordinatesat. fs_h_jt_rectexistsleftprimitivecoordinatesat + S (jt_value_rectexistsleftprimitivecoordinates) = S ((S (jt_index_rectexistsleftprimitivecoordinates)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftprimitivecoordinatesat. jt_b_rectexistsleft = fs_q_jt_rectexistsleftprimitivecoordinatesat * S ((S (jt_index_rectexistsleftprimitivecoordinates)) * jt_c_rectexistsleft) + (jt_value_rectexistsleftprimitivecoordinates))) -> (exists jt_factor_rectexistsleftprimitivecoordinatesdivides. (jt_value_rectexistsleftprimitivecoordinates)=(jt_divisor_rectexistsleftprimitive)*jt_factor_rectexistsleftprimitivecoordinatesdivides)) -> jt_divisor_rectexistsleftprimitive=1))))) /\ (((forall jt_b_rectexistsleft jt_c_rectexistsleft. (forall jt_index_rectexistsleftinputbound. (exists jt_gap_rectexistsleftinputboundindex. jt_gap_rectexistsleftinputboundindex+S (jt_index_rectexistsleftinputbound)=(k)) -> exists jt_value_rectexistsleftinputbound. ((((exists fs_h_jt_rectexistsleftinputboundat. fs_h_jt_rectexistsleftinputboundat + S (jt_value_rectexistsleftinputbound) = S ((S (jt_index_rectexistsleftinputbound)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftinputboundat. jt_b_rectexistsleft = fs_q_jt_rectexistsleftinputboundat * S ((S (jt_index_rectexistsleftinputbound)) * jt_c_rectexistsleft) + (jt_value_rectexistsleftinputbound))) /\ (exists jt_gap_rectexistsleftinputboundvalue. jt_gap_rectexistsleftinputboundvalue+S (jt_value_rectexistsleftinputbound)=(m)))) -> (forall jt_divisor_rectexistsleftinputprimitive. (exists jt_factor_rectexistsleftinputprimitivemodulus. (m)=(jt_divisor_rectexistsleftinputprimitive)*jt_factor_rectexistsleftinputprimitivemodulus) -> (forall jt_index_rectexistsleftinputprimitivecoordinates jt_value_rectexistsleftinputprimitivecoordinates. (exists jt_gap_rectexistsleftinputprimitivecoordinatesindex. jt_gap_rectexistsleftinputprimitivecoordinatesindex+S (jt_index_rectexistsleftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectexistsleftinputprimitivecoordinatesat. fs_h_jt_rectexistsleftinputprimitivecoordinatesat + S (jt_value_rectexistsleftinputprimitivecoordinates) = S ((S (jt_index_rectexistsleftinputprimitivecoordinates)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftinputprimitivecoordinatesat. jt_b_rectexistsleft = fs_q_jt_rectexistsleftinputprimitivecoordinatesat * S ((S (jt_index_rectexistsleftinputprimitivecoordinates)) * jt_c_rectexistsleft) + (jt_value_rectexistsleftinputprimitivecoordinates))) -> (exists jt_factor_rectexistsleftinputprimitivecoordinatesdivides. (jt_value_rectexistsleftinputprimitivecoordinates)=(jt_divisor_rectexistsleftinputprimitive)*jt_factor_rectexistsleftinputprimitivecoordinatesdivides)) -> jt_divisor_rectexistsleftinputprimitive=1) -> exists jt_i_rectexistsleft jt_d_rectexistsleft jt_e_rectexistsleft. ((exists jt_gap_rectexistsleftcompleteindex. jt_gap_rectexistsleftcompleteindex+S (jt_i_rectexistsleft)=(u)) /\ (((((((exists fs_h_jt_rectexistsleftcompletecode. fs_h_jt_rectexistsleftcompletecode + S (jt_d_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * B)) /\ exists fs_q_jt_rectexistsleftcompletecode. A = fs_q_jt_rectexistsleftcompletecode * S ((S (jt_i_rectexistsleft)) * B) + (jt_d_rectexistsleft))) /\ (((exists fs_h_jt_rectexistsleftcompletescale. fs_h_jt_rectexistsleftcompletescale + S (jt_e_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * D)) /\ exists fs_q_jt_rectexistsleftcompletescale. C = fs_q_jt_rectexistsleftcompletescale * S ((S (jt_i_rectexistsleft)) * D) + (jt_e_rectexistsleft))))) /\ (forall jt_index_rectexistsleftrepresented jt_left_rectexistsleftrepresented jt_right_rectexistsleftrepresented. (exists jt_gap_rectexistsleftrepresentedindex. jt_gap_rectexistsleftrepresentedindex+S (jt_index_rectexistsleftrepresented)=(k)) -> (((exists fs_h_jt_rectexistsleftrepresentedleft. fs_h_jt_rectexistsleftrepresentedleft + S (jt_left_rectexistsleftrepresented) = S ((S (jt_index_rectexistsleftrepresented)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftrepresentedleft. jt_b_rectexistsleft = fs_q_jt_rectexistsleftrepresentedleft * S ((S (jt_index_rectexistsleftrepresented)) * jt_c_rectexistsleft) + (jt_left_rectexistsleftrepresented))) -> (((exists fs_h_jt_rectexistsleftrepresentedright. fs_h_jt_rectexistsleftrepresentedright + S (jt_right_rectexistsleftrepresented) = S ((S (jt_index_rectexistsleftrepresented)) * jt_e_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftrepresentedright. jt_d_rectexistsleft = fs_q_jt_rectexistsleftrepresentedright * S ((S (jt_index_rectexistsleftrepresented)) * jt_e_rectexistsleft) + (jt_right_rectexistsleftrepresented))) -> jt_left_rectexistsleftrepresented=jt_right_rectexistsleftrepresented))))) /\ (forall jt_i_rectexistsleft jt_h_rectexistsleft jt_b_rectexistsleft jt_c_rectexistsleft jt_d_rectexistsleft jt_e_rectexistsleft. (exists jt_gap_rectexistsleftfirstindex. jt_gap_rectexistsleftfirstindex+S (jt_i_rectexistsleft)=(u)) -> (exists jt_gap_rectexistsleftsecondindex. jt_gap_rectexistsleftsecondindex+S (jt_h_rectexistsleft)=(u)) -> (((((exists fs_h_jt_rectexistsleftfirstcode. fs_h_jt_rectexistsleftfirstcode + S (jt_b_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * B)) /\ exists fs_q_jt_rectexistsleftfirstcode. A = fs_q_jt_rectexistsleftfirstcode * S ((S (jt_i_rectexistsleft)) * B) + (jt_b_rectexistsleft))) /\ (((exists fs_h_jt_rectexistsleftfirstscale. fs_h_jt_rectexistsleftfirstscale + S (jt_c_rectexistsleft) = S ((S (jt_i_rectexistsleft)) * D)) /\ exists fs_q_jt_rectexistsleftfirstscale. C = fs_q_jt_rectexistsleftfirstscale * S ((S (jt_i_rectexistsleft)) * D) + (jt_c_rectexistsleft))))) -> (((((exists fs_h_jt_rectexistsleftsecondcode. fs_h_jt_rectexistsleftsecondcode + S (jt_d_rectexistsleft) = S ((S (jt_h_rectexistsleft)) * B)) /\ exists fs_q_jt_rectexistsleftsecondcode. A = fs_q_jt_rectexistsleftsecondcode * S ((S (jt_h_rectexistsleft)) * B) + (jt_d_rectexistsleft))) /\ (((exists fs_h_jt_rectexistsleftsecondscale. fs_h_jt_rectexistsleftsecondscale + S (jt_e_rectexistsleft) = S ((S (jt_h_rectexistsleft)) * D)) /\ exists fs_q_jt_rectexistsleftsecondscale. C = fs_q_jt_rectexistsleftsecondscale * S ((S (jt_h_rectexistsleft)) * D) + (jt_e_rectexistsleft))))) -> (forall jt_index_rectexistsleftsame jt_left_rectexistsleftsame jt_right_rectexistsleftsame. (exists jt_gap_rectexistsleftsameindex. jt_gap_rectexistsleftsameindex+S (jt_index_rectexistsleftsame)=(k)) -> (((exists fs_h_jt_rectexistsleftsameleft. fs_h_jt_rectexistsleftsameleft + S (jt_left_rectexistsleftsame) = S ((S (jt_index_rectexistsleftsame)) * jt_c_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftsameleft. jt_b_rectexistsleft = fs_q_jt_rectexistsleftsameleft * S ((S (jt_index_rectexistsleftsame)) * jt_c_rectexistsleft) + (jt_left_rectexistsleftsame))) -> (((exists fs_h_jt_rectexistsleftsameright. fs_h_jt_rectexistsleftsameright + S (jt_right_rectexistsleftsame) = S ((S (jt_index_rectexistsleftsame)) * jt_e_rectexistsleft)) /\ exists fs_q_jt_rectexistsleftsameright. jt_d_rectexistsleft = fs_q_jt_rectexistsleftsameright * S ((S (jt_index_rectexistsleftsame)) * jt_e_rectexistsleft) + (jt_right_rectexistsleftsame))) -> jt_left_rectexistsleftsame=jt_right_rectexistsleftsame) -> jt_i_rectexistsleft=jt_h_rectexistsleft))))) -> (((forall jt_i_rectexistsright. (exists jt_gap_rectexistsrightsoundindex. jt_gap_rectexistsrightsoundindex+S (jt_i_rectexistsright)=(v)) -> exists jt_b_rectexistsright jt_c_rectexistsright. ((((((exists fs_h_jt_rectexistsrightsoundcode. fs_h_jt_rectexistsrightsoundcode + S (jt_b_rectexistsright) = S ((S (jt_i_rectexistsright)) * F)) /\ exists fs_q_jt_rectexistsrightsoundcode. E = fs_q_jt_rectexistsrightsoundcode * S ((S (jt_i_rectexistsright)) * F) + (jt_b_rectexistsright))) /\ (((exists fs_h_jt_rectexistsrightsoundscale. fs_h_jt_rectexistsrightsoundscale + S (jt_c_rectexistsright) = S ((S (jt_i_rectexistsright)) * H)) /\ exists fs_q_jt_rectexistsrightsoundscale. G = fs_q_jt_rectexistsrightsoundscale * S ((S (jt_i_rectexistsright)) * H) + (jt_c_rectexistsright))))) /\ (((forall jt_index_rectexistsrightbound. (exists jt_gap_rectexistsrightboundindex. jt_gap_rectexistsrightboundindex+S (jt_index_rectexistsrightbound)=(k)) -> exists jt_value_rectexistsrightbound. ((((exists fs_h_jt_rectexistsrightboundat. fs_h_jt_rectexistsrightboundat + S (jt_value_rectexistsrightbound) = S ((S (jt_index_rectexistsrightbound)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightboundat. jt_b_rectexistsright = fs_q_jt_rectexistsrightboundat * S ((S (jt_index_rectexistsrightbound)) * jt_c_rectexistsright) + (jt_value_rectexistsrightbound))) /\ (exists jt_gap_rectexistsrightboundvalue. jt_gap_rectexistsrightboundvalue+S (jt_value_rectexistsrightbound)=(n)))) /\ (forall jt_divisor_rectexistsrightprimitive. (exists jt_factor_rectexistsrightprimitivemodulus. (n)=(jt_divisor_rectexistsrightprimitive)*jt_factor_rectexistsrightprimitivemodulus) -> (forall jt_index_rectexistsrightprimitivecoordinates jt_value_rectexistsrightprimitivecoordinates. (exists jt_gap_rectexistsrightprimitivecoordinatesindex. jt_gap_rectexistsrightprimitivecoordinatesindex+S (jt_index_rectexistsrightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectexistsrightprimitivecoordinatesat. fs_h_jt_rectexistsrightprimitivecoordinatesat + S (jt_value_rectexistsrightprimitivecoordinates) = S ((S (jt_index_rectexistsrightprimitivecoordinates)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightprimitivecoordinatesat. jt_b_rectexistsright = fs_q_jt_rectexistsrightprimitivecoordinatesat * S ((S (jt_index_rectexistsrightprimitivecoordinates)) * jt_c_rectexistsright) + (jt_value_rectexistsrightprimitivecoordinates))) -> (exists jt_factor_rectexistsrightprimitivecoordinatesdivides. (jt_value_rectexistsrightprimitivecoordinates)=(jt_divisor_rectexistsrightprimitive)*jt_factor_rectexistsrightprimitivecoordinatesdivides)) -> jt_divisor_rectexistsrightprimitive=1))))) /\ (((forall jt_b_rectexistsright jt_c_rectexistsright. (forall jt_index_rectexistsrightinputbound. (exists jt_gap_rectexistsrightinputboundindex. jt_gap_rectexistsrightinputboundindex+S (jt_index_rectexistsrightinputbound)=(k)) -> exists jt_value_rectexistsrightinputbound. ((((exists fs_h_jt_rectexistsrightinputboundat. fs_h_jt_rectexistsrightinputboundat + S (jt_value_rectexistsrightinputbound) = S ((S (jt_index_rectexistsrightinputbound)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightinputboundat. jt_b_rectexistsright = fs_q_jt_rectexistsrightinputboundat * S ((S (jt_index_rectexistsrightinputbound)) * jt_c_rectexistsright) + (jt_value_rectexistsrightinputbound))) /\ (exists jt_gap_rectexistsrightinputboundvalue. jt_gap_rectexistsrightinputboundvalue+S (jt_value_rectexistsrightinputbound)=(n)))) -> (forall jt_divisor_rectexistsrightinputprimitive. (exists jt_factor_rectexistsrightinputprimitivemodulus. (n)=(jt_divisor_rectexistsrightinputprimitive)*jt_factor_rectexistsrightinputprimitivemodulus) -> (forall jt_index_rectexistsrightinputprimitivecoordinates jt_value_rectexistsrightinputprimitivecoordinates. (exists jt_gap_rectexistsrightinputprimitivecoordinatesindex. jt_gap_rectexistsrightinputprimitivecoordinatesindex+S (jt_index_rectexistsrightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectexistsrightinputprimitivecoordinatesat. fs_h_jt_rectexistsrightinputprimitivecoordinatesat + S (jt_value_rectexistsrightinputprimitivecoordinates) = S ((S (jt_index_rectexistsrightinputprimitivecoordinates)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightinputprimitivecoordinatesat. jt_b_rectexistsright = fs_q_jt_rectexistsrightinputprimitivecoordinatesat * S ((S (jt_index_rectexistsrightinputprimitivecoordinates)) * jt_c_rectexistsright) + (jt_value_rectexistsrightinputprimitivecoordinates))) -> (exists jt_factor_rectexistsrightinputprimitivecoordinatesdivides. (jt_value_rectexistsrightinputprimitivecoordinates)=(jt_divisor_rectexistsrightinputprimitive)*jt_factor_rectexistsrightinputprimitivecoordinatesdivides)) -> jt_divisor_rectexistsrightinputprimitive=1) -> exists jt_i_rectexistsright jt_d_rectexistsright jt_e_rectexistsright. ((exists jt_gap_rectexistsrightcompleteindex. jt_gap_rectexistsrightcompleteindex+S (jt_i_rectexistsright)=(v)) /\ (((((((exists fs_h_jt_rectexistsrightcompletecode. fs_h_jt_rectexistsrightcompletecode + S (jt_d_rectexistsright) = S ((S (jt_i_rectexistsright)) * F)) /\ exists fs_q_jt_rectexistsrightcompletecode. E = fs_q_jt_rectexistsrightcompletecode * S ((S (jt_i_rectexistsright)) * F) + (jt_d_rectexistsright))) /\ (((exists fs_h_jt_rectexistsrightcompletescale. fs_h_jt_rectexistsrightcompletescale + S (jt_e_rectexistsright) = S ((S (jt_i_rectexistsright)) * H)) /\ exists fs_q_jt_rectexistsrightcompletescale. G = fs_q_jt_rectexistsrightcompletescale * S ((S (jt_i_rectexistsright)) * H) + (jt_e_rectexistsright))))) /\ (forall jt_index_rectexistsrightrepresented jt_left_rectexistsrightrepresented jt_right_rectexistsrightrepresented. (exists jt_gap_rectexistsrightrepresentedindex. jt_gap_rectexistsrightrepresentedindex+S (jt_index_rectexistsrightrepresented)=(k)) -> (((exists fs_h_jt_rectexistsrightrepresentedleft. fs_h_jt_rectexistsrightrepresentedleft + S (jt_left_rectexistsrightrepresented) = S ((S (jt_index_rectexistsrightrepresented)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightrepresentedleft. jt_b_rectexistsright = fs_q_jt_rectexistsrightrepresentedleft * S ((S (jt_index_rectexistsrightrepresented)) * jt_c_rectexistsright) + (jt_left_rectexistsrightrepresented))) -> (((exists fs_h_jt_rectexistsrightrepresentedright. fs_h_jt_rectexistsrightrepresentedright + S (jt_right_rectexistsrightrepresented) = S ((S (jt_index_rectexistsrightrepresented)) * jt_e_rectexistsright)) /\ exists fs_q_jt_rectexistsrightrepresentedright. jt_d_rectexistsright = fs_q_jt_rectexistsrightrepresentedright * S ((S (jt_index_rectexistsrightrepresented)) * jt_e_rectexistsright) + (jt_right_rectexistsrightrepresented))) -> jt_left_rectexistsrightrepresented=jt_right_rectexistsrightrepresented))))) /\ (forall jt_i_rectexistsright jt_h_rectexistsright jt_b_rectexistsright jt_c_rectexistsright jt_d_rectexistsright jt_e_rectexistsright. (exists jt_gap_rectexistsrightfirstindex. jt_gap_rectexistsrightfirstindex+S (jt_i_rectexistsright)=(v)) -> (exists jt_gap_rectexistsrightsecondindex. jt_gap_rectexistsrightsecondindex+S (jt_h_rectexistsright)=(v)) -> (((((exists fs_h_jt_rectexistsrightfirstcode. fs_h_jt_rectexistsrightfirstcode + S (jt_b_rectexistsright) = S ((S (jt_i_rectexistsright)) * F)) /\ exists fs_q_jt_rectexistsrightfirstcode. E = fs_q_jt_rectexistsrightfirstcode * S ((S (jt_i_rectexistsright)) * F) + (jt_b_rectexistsright))) /\ (((exists fs_h_jt_rectexistsrightfirstscale. fs_h_jt_rectexistsrightfirstscale + S (jt_c_rectexistsright) = S ((S (jt_i_rectexistsright)) * H)) /\ exists fs_q_jt_rectexistsrightfirstscale. G = fs_q_jt_rectexistsrightfirstscale * S ((S (jt_i_rectexistsright)) * H) + (jt_c_rectexistsright))))) -> (((((exists fs_h_jt_rectexistsrightsecondcode. fs_h_jt_rectexistsrightsecondcode + S (jt_d_rectexistsright) = S ((S (jt_h_rectexistsright)) * F)) /\ exists fs_q_jt_rectexistsrightsecondcode. E = fs_q_jt_rectexistsrightsecondcode * S ((S (jt_h_rectexistsright)) * F) + (jt_d_rectexistsright))) /\ (((exists fs_h_jt_rectexistsrightsecondscale. fs_h_jt_rectexistsrightsecondscale + S (jt_e_rectexistsright) = S ((S (jt_h_rectexistsright)) * H)) /\ exists fs_q_jt_rectexistsrightsecondscale. G = fs_q_jt_rectexistsrightsecondscale * S ((S (jt_h_rectexistsright)) * H) + (jt_e_rectexistsright))))) -> (forall jt_index_rectexistsrightsame jt_left_rectexistsrightsame jt_right_rectexistsrightsame. (exists jt_gap_rectexistsrightsameindex. jt_gap_rectexistsrightsameindex+S (jt_index_rectexistsrightsame)=(k)) -> (((exists fs_h_jt_rectexistsrightsameleft. fs_h_jt_rectexistsrightsameleft + S (jt_left_rectexistsrightsame) = S ((S (jt_index_rectexistsrightsame)) * jt_c_rectexistsright)) /\ exists fs_q_jt_rectexistsrightsameleft. jt_b_rectexistsright = fs_q_jt_rectexistsrightsameleft * S ((S (jt_index_rectexistsrightsame)) * jt_c_rectexistsright) + (jt_left_rectexistsrightsame))) -> (((exists fs_h_jt_rectexistsrightsameright. fs_h_jt_rectexistsrightsameright + S (jt_right_rectexistsrightsame) = S ((S (jt_index_rectexistsrightsame)) * jt_e_rectexistsright)) /\ exists fs_q_jt_rectexistsrightsameright. jt_d_rectexistsright = fs_q_jt_rectexistsrightsameright * S ((S (jt_index_rectexistsrightsame)) * jt_e_rectexistsright) + (jt_right_rectexistsrightsame))) -> jt_left_rectexistsrightsame=jt_right_rectexistsrightsame) -> jt_i_rectexistsright=jt_h_rectexistsright))))) -> forall q. (exists jt_gap_rectexistsbound. jt_gap_rectexistsbound+(q)=(u*v)) -> exists P Q R T. forall jt_index_rectexiststarget. (exists jt_gap_rectexiststargetindex. jt_gap_rectexiststargetindex+S (jt_index_rectexiststarget)=(q)) -> exists jt_row_rectexiststarget jt_column_rectexiststarget jt_b_rectexiststarget jt_c_rectexiststarget jt_d_rectexiststarget jt_e_rectexiststarget jt_f_rectexiststarget jt_g_rectexiststarget. ((exists jt_gap_rectexiststargetrow. jt_gap_rectexiststargetrow+S (jt_row_rectexiststarget)=(u)) /\ (((exists jt_gap_rectexiststargetcolumn. jt_gap_rectexiststargetcolumn+S (jt_column_rectexiststarget)=(v)) /\ (((jt_index_rectexiststarget=(v)*jt_row_rectexiststarget+jt_column_rectexiststarget) /\ (((((((exists fs_h_jt_rectexiststargetleftcode. fs_h_jt_rectexiststargetleftcode + S (jt_b_rectexiststarget) = S ((S (jt_row_rectexiststarget)) * B)) /\ exists fs_q_jt_rectexiststargetleftcode. A = fs_q_jt_rectexiststargetleftcode * S ((S (jt_row_rectexiststarget)) * B) + (jt_b_rectexiststarget))) /\ (((exists fs_h_jt_rectexiststargetleftscale. fs_h_jt_rectexiststargetleftscale + S (jt_c_rectexiststarget) = S ((S (jt_row_rectexiststarget)) * D)) /\ exists fs_q_jt_rectexiststargetleftscale. C = fs_q_jt_rectexiststargetleftscale * S ((S (jt_row_rectexiststarget)) * D) + (jt_c_rectexiststarget))))) /\ (((((((exists fs_h_jt_rectexiststargetrightcode. fs_h_jt_rectexiststargetrightcode + S (jt_d_rectexiststarget) = S ((S (jt_column_rectexiststarget)) * F)) /\ exists fs_q_jt_rectexiststargetrightcode. E = fs_q_jt_rectexiststargetrightcode * S ((S (jt_column_rectexiststarget)) * F) + (jt_d_rectexiststarget))) /\ (((exists fs_h_jt_rectexiststargetrightscale. fs_h_jt_rectexiststargetrightscale + S (jt_e_rectexiststarget) = S ((S (jt_column_rectexiststarget)) * H)) /\ exists fs_q_jt_rectexiststargetrightscale. G = fs_q_jt_rectexiststargetrightscale * S ((S (jt_column_rectexiststarget)) * H) + (jt_e_rectexiststarget))))) /\ (((((((exists fs_h_jt_rectexiststargetoutputcode. fs_h_jt_rectexiststargetoutputcode + S (jt_f_rectexiststarget) = S ((S (jt_index_rectexiststarget)) * Q)) /\ exists fs_q_jt_rectexiststargetoutputcode. P = fs_q_jt_rectexiststargetoutputcode * S ((S (jt_index_rectexiststarget)) * Q) + (jt_f_rectexiststarget))) /\ (((exists fs_h_jt_rectexiststargetoutputscale. fs_h_jt_rectexiststargetoutputscale + S (jt_g_rectexiststarget) = S ((S (jt_index_rectexiststarget)) * T)) /\ exists fs_q_jt_rectexiststargetoutputscale. R = fs_q_jt_rectexiststargetoutputscale * S ((S (jt_index_rectexiststarget)) * T) + (jt_g_rectexiststarget))))) /\ (((((forall jt_index_rectexiststargetcrtbound. (exists jt_gap_rectexiststargetcrtboundindex. jt_gap_rectexiststargetcrtboundindex+S (jt_index_rectexiststargetcrtbound)=(k)) -> exists jt_value_rectexiststargetcrtbound. ((((exists fs_h_jt_rectexiststargetcrtboundat. fs_h_jt_rectexiststargetcrtboundat + S (jt_value_rectexiststargetcrtbound) = S ((S (jt_index_rectexiststargetcrtbound)) * jt_g_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetcrtboundat. jt_f_rectexiststarget = fs_q_jt_rectexiststargetcrtboundat * S ((S (jt_index_rectexiststargetcrtbound)) * jt_g_rectexiststarget) + (jt_value_rectexiststargetcrtbound))) /\ (exists jt_gap_rectexiststargetcrtboundvalue. jt_gap_rectexiststargetcrtboundvalue+S (jt_value_rectexiststargetcrtbound)=(m*n)))) /\ (((forall jt_index_rectexiststargetcrtleft jt_left_rectexiststargetcrtleft jt_right_rectexiststargetcrtleft. (exists jt_gap_rectexiststargetcrtleftindex. jt_gap_rectexiststargetcrtleftindex+S (jt_index_rectexiststargetcrtleft)=(k)) -> (((exists fs_h_jt_rectexiststargetcrtleftleft. fs_h_jt_rectexiststargetcrtleftleft + S (jt_left_rectexiststargetcrtleft) = S ((S (jt_index_rectexiststargetcrtleft)) * jt_g_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetcrtleftleft. jt_f_rectexiststarget = fs_q_jt_rectexiststargetcrtleftleft * S ((S (jt_index_rectexiststargetcrtleft)) * jt_g_rectexiststarget) + (jt_left_rectexiststargetcrtleft))) -> (((exists fs_h_jt_rectexiststargetcrtleftright. fs_h_jt_rectexiststargetcrtleftright + S (jt_right_rectexiststargetcrtleft) = S ((S (jt_index_rectexiststargetcrtleft)) * jt_c_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetcrtleftright. jt_b_rectexiststarget = fs_q_jt_rectexiststargetcrtleftright * S ((S (jt_index_rectexiststargetcrtleft)) * jt_c_rectexiststarget) + (jt_right_rectexiststargetcrtleft))) -> (exists jt_left_rectexiststargetcrtleftmod jt_right_rectexiststargetcrtleftmod. (jt_left_rectexiststargetcrtleft)+(m)*jt_left_rectexiststargetcrtleftmod=(jt_right_rectexiststargetcrtleft)+(m)*jt_right_rectexiststargetcrtleftmod)) /\ (forall jt_index_rectexiststargetcrtright jt_left_rectexiststargetcrtright jt_right_rectexiststargetcrtright. (exists jt_gap_rectexiststargetcrtrightindex. jt_gap_rectexiststargetcrtrightindex+S (jt_index_rectexiststargetcrtright)=(k)) -> (((exists fs_h_jt_rectexiststargetcrtrightleft. fs_h_jt_rectexiststargetcrtrightleft + S (jt_left_rectexiststargetcrtright) = S ((S (jt_index_rectexiststargetcrtright)) * jt_g_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetcrtrightleft. jt_f_rectexiststarget = fs_q_jt_rectexiststargetcrtrightleft * S ((S (jt_index_rectexiststargetcrtright)) * jt_g_rectexiststarget) + (jt_left_rectexiststargetcrtright))) -> (((exists fs_h_jt_rectexiststargetcrtrightright. fs_h_jt_rectexiststargetcrtrightright + S (jt_right_rectexiststargetcrtright) = S ((S (jt_index_rectexiststargetcrtright)) * jt_e_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetcrtrightright. jt_d_rectexiststarget = fs_q_jt_rectexiststargetcrtrightright * S ((S (jt_index_rectexiststargetcrtright)) * jt_e_rectexiststarget) + (jt_right_rectexiststargetcrtright))) -> (exists jt_left_rectexiststargetcrtrightmod jt_right_rectexiststargetcrtrightmod. (jt_left_rectexiststargetcrtright)+(n)*jt_left_rectexiststargetcrtrightmod=(jt_right_rectexiststargetcrtright)+(n)*jt_right_rectexiststargetcrtrightmod)))))) /\ (forall jt_divisor_rectexiststargetprimitive. (exists jt_factor_rectexiststargetprimitivemodulus. (m*n)=(jt_divisor_rectexiststargetprimitive)*jt_factor_rectexiststargetprimitivemodulus) -> (forall jt_index_rectexiststargetprimitivecoordinates jt_value_rectexiststargetprimitivecoordinates. (exists jt_gap_rectexiststargetprimitivecoordinatesindex. jt_gap_rectexiststargetprimitivecoordinatesindex+S (jt_index_rectexiststargetprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectexiststargetprimitivecoordinatesat. fs_h_jt_rectexiststargetprimitivecoordinatesat + S (jt_value_rectexiststargetprimitivecoordinates) = S ((S (jt_index_rectexiststargetprimitivecoordinates)) * jt_g_rectexiststarget)) /\ exists fs_q_jt_rectexiststargetprimitivecoordinatesat. jt_f_rectexiststarget = fs_q_jt_rectexiststargetprimitivecoordinatesat * S ((S (jt_index_rectexiststargetprimitivecoordinates)) * jt_g_rectexiststarget) + (jt_value_rectexiststargetprimitivecoordinates))) -> (exists jt_factor_rectexiststargetprimitivecoordinatesdivides. (jt_value_rectexiststargetprimitivecoordinates)=(jt_divisor_rectexiststargetprimitive)*jt_factor_rectexiststargetprimitivecoordinatesdivides)) -> jt_divisor_rectexiststargetprimitive=1))))))))))))))