jordan_rectangle_crt_append

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v P Q R T q. ~(m=0) -> ~(n=0) -> (forall jt_divisor_rectappendcop. (exists jt_factor_rectappendcopa. (m)=(jt_divisor_rectappendcop)*jt_factor_rectappendcopa) -> (exists jt_factor_rectappendcopb. (n)=(jt_divisor_rectappendcop)*jt_factor_rectappendcopb) -> jt_divisor_rectappendcop=1) -> (((forall jt_i_rectappendleft. (exists jt_gap_rectappendleftsoundindex. jt_gap_rectappendleftsoundindex+S (jt_i_rectappendleft)=(u)) -> exists jt_b_rectappendleft jt_c_rectappendleft. ((((((exists fs_h_jt_rectappendleftsoundcode. fs_h_jt_rectappendleftsoundcode + S (jt_b_rectappendleft) = S ((S (jt_i_rectappendleft)) * B)) /\ exists fs_q_jt_rectappendleftsoundcode. A = fs_q_jt_rectappendleftsoundcode * S ((S (jt_i_rectappendleft)) * B) + (jt_b_rectappendleft))) /\ (((exists fs_h_jt_rectappendleftsoundscale. fs_h_jt_rectappendleftsoundscale + S (jt_c_rectappendleft) = S ((S (jt_i_rectappendleft)) * D)) /\ exists fs_q_jt_rectappendleftsoundscale. C = fs_q_jt_rectappendleftsoundscale * S ((S (jt_i_rectappendleft)) * D) + (jt_c_rectappendleft))))) /\ (((forall jt_index_rectappendleftbound. (exists jt_gap_rectappendleftboundindex. jt_gap_rectappendleftboundindex+S (jt_index_rectappendleftbound)=(k)) -> exists jt_value_rectappendleftbound. ((((exists fs_h_jt_rectappendleftboundat. fs_h_jt_rectappendleftboundat + S (jt_value_rectappendleftbound) = S ((S (jt_index_rectappendleftbound)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftboundat. jt_b_rectappendleft = fs_q_jt_rectappendleftboundat * S ((S (jt_index_rectappendleftbound)) * jt_c_rectappendleft) + (jt_value_rectappendleftbound))) /\ (exists jt_gap_rectappendleftboundvalue. jt_gap_rectappendleftboundvalue+S (jt_value_rectappendleftbound)=(m)))) /\ (forall jt_divisor_rectappendleftprimitive. (exists jt_factor_rectappendleftprimitivemodulus. (m)=(jt_divisor_rectappendleftprimitive)*jt_factor_rectappendleftprimitivemodulus) -> (forall jt_index_rectappendleftprimitivecoordinates jt_value_rectappendleftprimitivecoordinates. (exists jt_gap_rectappendleftprimitivecoordinatesindex. jt_gap_rectappendleftprimitivecoordinatesindex+S (jt_index_rectappendleftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendleftprimitivecoordinatesat. fs_h_jt_rectappendleftprimitivecoordinatesat + S (jt_value_rectappendleftprimitivecoordinates) = S ((S (jt_index_rectappendleftprimitivecoordinates)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftprimitivecoordinatesat. jt_b_rectappendleft = fs_q_jt_rectappendleftprimitivecoordinatesat * S ((S (jt_index_rectappendleftprimitivecoordinates)) * jt_c_rectappendleft) + (jt_value_rectappendleftprimitivecoordinates))) -> (exists jt_factor_rectappendleftprimitivecoordinatesdivides. (jt_value_rectappendleftprimitivecoordinates)=(jt_divisor_rectappendleftprimitive)*jt_factor_rectappendleftprimitivecoordinatesdivides)) -> jt_divisor_rectappendleftprimitive=1))))) /\ (((forall jt_b_rectappendleft jt_c_rectappendleft. (forall jt_index_rectappendleftinputbound. (exists jt_gap_rectappendleftinputboundindex. jt_gap_rectappendleftinputboundindex+S (jt_index_rectappendleftinputbound)=(k)) -> exists jt_value_rectappendleftinputbound. ((((exists fs_h_jt_rectappendleftinputboundat. fs_h_jt_rectappendleftinputboundat + S (jt_value_rectappendleftinputbound) = S ((S (jt_index_rectappendleftinputbound)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftinputboundat. jt_b_rectappendleft = fs_q_jt_rectappendleftinputboundat * S ((S (jt_index_rectappendleftinputbound)) * jt_c_rectappendleft) + (jt_value_rectappendleftinputbound))) /\ (exists jt_gap_rectappendleftinputboundvalue. jt_gap_rectappendleftinputboundvalue+S (jt_value_rectappendleftinputbound)=(m)))) -> (forall jt_divisor_rectappendleftinputprimitive. (exists jt_factor_rectappendleftinputprimitivemodulus. (m)=(jt_divisor_rectappendleftinputprimitive)*jt_factor_rectappendleftinputprimitivemodulus) -> (forall jt_index_rectappendleftinputprimitivecoordinates jt_value_rectappendleftinputprimitivecoordinates. (exists jt_gap_rectappendleftinputprimitivecoordinatesindex. jt_gap_rectappendleftinputprimitivecoordinatesindex+S (jt_index_rectappendleftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendleftinputprimitivecoordinatesat. fs_h_jt_rectappendleftinputprimitivecoordinatesat + S (jt_value_rectappendleftinputprimitivecoordinates) = S ((S (jt_index_rectappendleftinputprimitivecoordinates)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftinputprimitivecoordinatesat. jt_b_rectappendleft = fs_q_jt_rectappendleftinputprimitivecoordinatesat * S ((S (jt_index_rectappendleftinputprimitivecoordinates)) * jt_c_rectappendleft) + (jt_value_rectappendleftinputprimitivecoordinates))) -> (exists jt_factor_rectappendleftinputprimitivecoordinatesdivides. (jt_value_rectappendleftinputprimitivecoordinates)=(jt_divisor_rectappendleftinputprimitive)*jt_factor_rectappendleftinputprimitivecoordinatesdivides)) -> jt_divisor_rectappendleftinputprimitive=1) -> exists jt_i_rectappendleft jt_d_rectappendleft jt_e_rectappendleft. ((exists jt_gap_rectappendleftcompleteindex. jt_gap_rectappendleftcompleteindex+S (jt_i_rectappendleft)=(u)) /\ (((((((exists fs_h_jt_rectappendleftcompletecode. fs_h_jt_rectappendleftcompletecode + S (jt_d_rectappendleft) = S ((S (jt_i_rectappendleft)) * B)) /\ exists fs_q_jt_rectappendleftcompletecode. A = fs_q_jt_rectappendleftcompletecode * S ((S (jt_i_rectappendleft)) * B) + (jt_d_rectappendleft))) /\ (((exists fs_h_jt_rectappendleftcompletescale. fs_h_jt_rectappendleftcompletescale + S (jt_e_rectappendleft) = S ((S (jt_i_rectappendleft)) * D)) /\ exists fs_q_jt_rectappendleftcompletescale. C = fs_q_jt_rectappendleftcompletescale * S ((S (jt_i_rectappendleft)) * D) + (jt_e_rectappendleft))))) /\ (forall jt_index_rectappendleftrepresented jt_left_rectappendleftrepresented jt_right_rectappendleftrepresented. (exists jt_gap_rectappendleftrepresentedindex. jt_gap_rectappendleftrepresentedindex+S (jt_index_rectappendleftrepresented)=(k)) -> (((exists fs_h_jt_rectappendleftrepresentedleft. fs_h_jt_rectappendleftrepresentedleft + S (jt_left_rectappendleftrepresented) = S ((S (jt_index_rectappendleftrepresented)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftrepresentedleft. jt_b_rectappendleft = fs_q_jt_rectappendleftrepresentedleft * S ((S (jt_index_rectappendleftrepresented)) * jt_c_rectappendleft) + (jt_left_rectappendleftrepresented))) -> (((exists fs_h_jt_rectappendleftrepresentedright. fs_h_jt_rectappendleftrepresentedright + S (jt_right_rectappendleftrepresented) = S ((S (jt_index_rectappendleftrepresented)) * jt_e_rectappendleft)) /\ exists fs_q_jt_rectappendleftrepresentedright. jt_d_rectappendleft = fs_q_jt_rectappendleftrepresentedright * S ((S (jt_index_rectappendleftrepresented)) * jt_e_rectappendleft) + (jt_right_rectappendleftrepresented))) -> jt_left_rectappendleftrepresented=jt_right_rectappendleftrepresented))))) /\ (forall jt_i_rectappendleft jt_h_rectappendleft jt_b_rectappendleft jt_c_rectappendleft jt_d_rectappendleft jt_e_rectappendleft. (exists jt_gap_rectappendleftfirstindex. jt_gap_rectappendleftfirstindex+S (jt_i_rectappendleft)=(u)) -> (exists jt_gap_rectappendleftsecondindex. jt_gap_rectappendleftsecondindex+S (jt_h_rectappendleft)=(u)) -> (((((exists fs_h_jt_rectappendleftfirstcode. fs_h_jt_rectappendleftfirstcode + S (jt_b_rectappendleft) = S ((S (jt_i_rectappendleft)) * B)) /\ exists fs_q_jt_rectappendleftfirstcode. A = fs_q_jt_rectappendleftfirstcode * S ((S (jt_i_rectappendleft)) * B) + (jt_b_rectappendleft))) /\ (((exists fs_h_jt_rectappendleftfirstscale. fs_h_jt_rectappendleftfirstscale + S (jt_c_rectappendleft) = S ((S (jt_i_rectappendleft)) * D)) /\ exists fs_q_jt_rectappendleftfirstscale. C = fs_q_jt_rectappendleftfirstscale * S ((S (jt_i_rectappendleft)) * D) + (jt_c_rectappendleft))))) -> (((((exists fs_h_jt_rectappendleftsecondcode. fs_h_jt_rectappendleftsecondcode + S (jt_d_rectappendleft) = S ((S (jt_h_rectappendleft)) * B)) /\ exists fs_q_jt_rectappendleftsecondcode. A = fs_q_jt_rectappendleftsecondcode * S ((S (jt_h_rectappendleft)) * B) + (jt_d_rectappendleft))) /\ (((exists fs_h_jt_rectappendleftsecondscale. fs_h_jt_rectappendleftsecondscale + S (jt_e_rectappendleft) = S ((S (jt_h_rectappendleft)) * D)) /\ exists fs_q_jt_rectappendleftsecondscale. C = fs_q_jt_rectappendleftsecondscale * S ((S (jt_h_rectappendleft)) * D) + (jt_e_rectappendleft))))) -> (forall jt_index_rectappendleftsame jt_left_rectappendleftsame jt_right_rectappendleftsame. (exists jt_gap_rectappendleftsameindex. jt_gap_rectappendleftsameindex+S (jt_index_rectappendleftsame)=(k)) -> (((exists fs_h_jt_rectappendleftsameleft. fs_h_jt_rectappendleftsameleft + S (jt_left_rectappendleftsame) = S ((S (jt_index_rectappendleftsame)) * jt_c_rectappendleft)) /\ exists fs_q_jt_rectappendleftsameleft. jt_b_rectappendleft = fs_q_jt_rectappendleftsameleft * S ((S (jt_index_rectappendleftsame)) * jt_c_rectappendleft) + (jt_left_rectappendleftsame))) -> (((exists fs_h_jt_rectappendleftsameright. fs_h_jt_rectappendleftsameright + S (jt_right_rectappendleftsame) = S ((S (jt_index_rectappendleftsame)) * jt_e_rectappendleft)) /\ exists fs_q_jt_rectappendleftsameright. jt_d_rectappendleft = fs_q_jt_rectappendleftsameright * S ((S (jt_index_rectappendleftsame)) * jt_e_rectappendleft) + (jt_right_rectappendleftsame))) -> jt_left_rectappendleftsame=jt_right_rectappendleftsame) -> jt_i_rectappendleft=jt_h_rectappendleft))))) -> (((forall jt_i_rectappendright. (exists jt_gap_rectappendrightsoundindex. jt_gap_rectappendrightsoundindex+S (jt_i_rectappendright)=(v)) -> exists jt_b_rectappendright jt_c_rectappendright. ((((((exists fs_h_jt_rectappendrightsoundcode. fs_h_jt_rectappendrightsoundcode + S (jt_b_rectappendright) = S ((S (jt_i_rectappendright)) * F)) /\ exists fs_q_jt_rectappendrightsoundcode. E = fs_q_jt_rectappendrightsoundcode * S ((S (jt_i_rectappendright)) * F) + (jt_b_rectappendright))) /\ (((exists fs_h_jt_rectappendrightsoundscale. fs_h_jt_rectappendrightsoundscale + S (jt_c_rectappendright) = S ((S (jt_i_rectappendright)) * H)) /\ exists fs_q_jt_rectappendrightsoundscale. G = fs_q_jt_rectappendrightsoundscale * S ((S (jt_i_rectappendright)) * H) + (jt_c_rectappendright))))) /\ (((forall jt_index_rectappendrightbound. (exists jt_gap_rectappendrightboundindex. jt_gap_rectappendrightboundindex+S (jt_index_rectappendrightbound)=(k)) -> exists jt_value_rectappendrightbound. ((((exists fs_h_jt_rectappendrightboundat. fs_h_jt_rectappendrightboundat + S (jt_value_rectappendrightbound) = S ((S (jt_index_rectappendrightbound)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightboundat. jt_b_rectappendright = fs_q_jt_rectappendrightboundat * S ((S (jt_index_rectappendrightbound)) * jt_c_rectappendright) + (jt_value_rectappendrightbound))) /\ (exists jt_gap_rectappendrightboundvalue. jt_gap_rectappendrightboundvalue+S (jt_value_rectappendrightbound)=(n)))) /\ (forall jt_divisor_rectappendrightprimitive. (exists jt_factor_rectappendrightprimitivemodulus. (n)=(jt_divisor_rectappendrightprimitive)*jt_factor_rectappendrightprimitivemodulus) -> (forall jt_index_rectappendrightprimitivecoordinates jt_value_rectappendrightprimitivecoordinates. (exists jt_gap_rectappendrightprimitivecoordinatesindex. jt_gap_rectappendrightprimitivecoordinatesindex+S (jt_index_rectappendrightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendrightprimitivecoordinatesat. fs_h_jt_rectappendrightprimitivecoordinatesat + S (jt_value_rectappendrightprimitivecoordinates) = S ((S (jt_index_rectappendrightprimitivecoordinates)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightprimitivecoordinatesat. jt_b_rectappendright = fs_q_jt_rectappendrightprimitivecoordinatesat * S ((S (jt_index_rectappendrightprimitivecoordinates)) * jt_c_rectappendright) + (jt_value_rectappendrightprimitivecoordinates))) -> (exists jt_factor_rectappendrightprimitivecoordinatesdivides. (jt_value_rectappendrightprimitivecoordinates)=(jt_divisor_rectappendrightprimitive)*jt_factor_rectappendrightprimitivecoordinatesdivides)) -> jt_divisor_rectappendrightprimitive=1))))) /\ (((forall jt_b_rectappendright jt_c_rectappendright. (forall jt_index_rectappendrightinputbound. (exists jt_gap_rectappendrightinputboundindex. jt_gap_rectappendrightinputboundindex+S (jt_index_rectappendrightinputbound)=(k)) -> exists jt_value_rectappendrightinputbound. ((((exists fs_h_jt_rectappendrightinputboundat. fs_h_jt_rectappendrightinputboundat + S (jt_value_rectappendrightinputbound) = S ((S (jt_index_rectappendrightinputbound)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightinputboundat. jt_b_rectappendright = fs_q_jt_rectappendrightinputboundat * S ((S (jt_index_rectappendrightinputbound)) * jt_c_rectappendright) + (jt_value_rectappendrightinputbound))) /\ (exists jt_gap_rectappendrightinputboundvalue. jt_gap_rectappendrightinputboundvalue+S (jt_value_rectappendrightinputbound)=(n)))) -> (forall jt_divisor_rectappendrightinputprimitive. (exists jt_factor_rectappendrightinputprimitivemodulus. (n)=(jt_divisor_rectappendrightinputprimitive)*jt_factor_rectappendrightinputprimitivemodulus) -> (forall jt_index_rectappendrightinputprimitivecoordinates jt_value_rectappendrightinputprimitivecoordinates. (exists jt_gap_rectappendrightinputprimitivecoordinatesindex. jt_gap_rectappendrightinputprimitivecoordinatesindex+S (jt_index_rectappendrightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendrightinputprimitivecoordinatesat. fs_h_jt_rectappendrightinputprimitivecoordinatesat + S (jt_value_rectappendrightinputprimitivecoordinates) = S ((S (jt_index_rectappendrightinputprimitivecoordinates)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightinputprimitivecoordinatesat. jt_b_rectappendright = fs_q_jt_rectappendrightinputprimitivecoordinatesat * S ((S (jt_index_rectappendrightinputprimitivecoordinates)) * jt_c_rectappendright) + (jt_value_rectappendrightinputprimitivecoordinates))) -> (exists jt_factor_rectappendrightinputprimitivecoordinatesdivides. (jt_value_rectappendrightinputprimitivecoordinates)=(jt_divisor_rectappendrightinputprimitive)*jt_factor_rectappendrightinputprimitivecoordinatesdivides)) -> jt_divisor_rectappendrightinputprimitive=1) -> exists jt_i_rectappendright jt_d_rectappendright jt_e_rectappendright. ((exists jt_gap_rectappendrightcompleteindex. jt_gap_rectappendrightcompleteindex+S (jt_i_rectappendright)=(v)) /\ (((((((exists fs_h_jt_rectappendrightcompletecode. fs_h_jt_rectappendrightcompletecode + S (jt_d_rectappendright) = S ((S (jt_i_rectappendright)) * F)) /\ exists fs_q_jt_rectappendrightcompletecode. E = fs_q_jt_rectappendrightcompletecode * S ((S (jt_i_rectappendright)) * F) + (jt_d_rectappendright))) /\ (((exists fs_h_jt_rectappendrightcompletescale. fs_h_jt_rectappendrightcompletescale + S (jt_e_rectappendright) = S ((S (jt_i_rectappendright)) * H)) /\ exists fs_q_jt_rectappendrightcompletescale. G = fs_q_jt_rectappendrightcompletescale * S ((S (jt_i_rectappendright)) * H) + (jt_e_rectappendright))))) /\ (forall jt_index_rectappendrightrepresented jt_left_rectappendrightrepresented jt_right_rectappendrightrepresented. (exists jt_gap_rectappendrightrepresentedindex. jt_gap_rectappendrightrepresentedindex+S (jt_index_rectappendrightrepresented)=(k)) -> (((exists fs_h_jt_rectappendrightrepresentedleft. fs_h_jt_rectappendrightrepresentedleft + S (jt_left_rectappendrightrepresented) = S ((S (jt_index_rectappendrightrepresented)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightrepresentedleft. jt_b_rectappendright = fs_q_jt_rectappendrightrepresentedleft * S ((S (jt_index_rectappendrightrepresented)) * jt_c_rectappendright) + (jt_left_rectappendrightrepresented))) -> (((exists fs_h_jt_rectappendrightrepresentedright. fs_h_jt_rectappendrightrepresentedright + S (jt_right_rectappendrightrepresented) = S ((S (jt_index_rectappendrightrepresented)) * jt_e_rectappendright)) /\ exists fs_q_jt_rectappendrightrepresentedright. jt_d_rectappendright = fs_q_jt_rectappendrightrepresentedright * S ((S (jt_index_rectappendrightrepresented)) * jt_e_rectappendright) + (jt_right_rectappendrightrepresented))) -> jt_left_rectappendrightrepresented=jt_right_rectappendrightrepresented))))) /\ (forall jt_i_rectappendright jt_h_rectappendright jt_b_rectappendright jt_c_rectappendright jt_d_rectappendright jt_e_rectappendright. (exists jt_gap_rectappendrightfirstindex. jt_gap_rectappendrightfirstindex+S (jt_i_rectappendright)=(v)) -> (exists jt_gap_rectappendrightsecondindex. jt_gap_rectappendrightsecondindex+S (jt_h_rectappendright)=(v)) -> (((((exists fs_h_jt_rectappendrightfirstcode. fs_h_jt_rectappendrightfirstcode + S (jt_b_rectappendright) = S ((S (jt_i_rectappendright)) * F)) /\ exists fs_q_jt_rectappendrightfirstcode. E = fs_q_jt_rectappendrightfirstcode * S ((S (jt_i_rectappendright)) * F) + (jt_b_rectappendright))) /\ (((exists fs_h_jt_rectappendrightfirstscale. fs_h_jt_rectappendrightfirstscale + S (jt_c_rectappendright) = S ((S (jt_i_rectappendright)) * H)) /\ exists fs_q_jt_rectappendrightfirstscale. G = fs_q_jt_rectappendrightfirstscale * S ((S (jt_i_rectappendright)) * H) + (jt_c_rectappendright))))) -> (((((exists fs_h_jt_rectappendrightsecondcode. fs_h_jt_rectappendrightsecondcode + S (jt_d_rectappendright) = S ((S (jt_h_rectappendright)) * F)) /\ exists fs_q_jt_rectappendrightsecondcode. E = fs_q_jt_rectappendrightsecondcode * S ((S (jt_h_rectappendright)) * F) + (jt_d_rectappendright))) /\ (((exists fs_h_jt_rectappendrightsecondscale. fs_h_jt_rectappendrightsecondscale + S (jt_e_rectappendright) = S ((S (jt_h_rectappendright)) * H)) /\ exists fs_q_jt_rectappendrightsecondscale. G = fs_q_jt_rectappendrightsecondscale * S ((S (jt_h_rectappendright)) * H) + (jt_e_rectappendright))))) -> (forall jt_index_rectappendrightsame jt_left_rectappendrightsame jt_right_rectappendrightsame. (exists jt_gap_rectappendrightsameindex. jt_gap_rectappendrightsameindex+S (jt_index_rectappendrightsame)=(k)) -> (((exists fs_h_jt_rectappendrightsameleft. fs_h_jt_rectappendrightsameleft + S (jt_left_rectappendrightsame) = S ((S (jt_index_rectappendrightsame)) * jt_c_rectappendright)) /\ exists fs_q_jt_rectappendrightsameleft. jt_b_rectappendright = fs_q_jt_rectappendrightsameleft * S ((S (jt_index_rectappendrightsame)) * jt_c_rectappendright) + (jt_left_rectappendrightsame))) -> (((exists fs_h_jt_rectappendrightsameright. fs_h_jt_rectappendrightsameright + S (jt_right_rectappendrightsame) = S ((S (jt_index_rectappendrightsame)) * jt_e_rectappendright)) /\ exists fs_q_jt_rectappendrightsameright. jt_d_rectappendright = fs_q_jt_rectappendrightsameright * S ((S (jt_index_rectappendrightsame)) * jt_e_rectappendright) + (jt_right_rectappendrightsame))) -> jt_left_rectappendrightsame=jt_right_rectappendrightsame) -> jt_i_rectappendright=jt_h_rectappendright))))) -> (forall jt_index_rectappendold. (exists jt_gap_rectappendoldindex. jt_gap_rectappendoldindex+S (jt_index_rectappendold)=(q)) -> exists jt_row_rectappendold jt_column_rectappendold jt_b_rectappendold jt_c_rectappendold jt_d_rectappendold jt_e_rectappendold jt_f_rectappendold jt_g_rectappendold. ((exists jt_gap_rectappendoldrow. jt_gap_rectappendoldrow+S (jt_row_rectappendold)=(u)) /\ (((exists jt_gap_rectappendoldcolumn. jt_gap_rectappendoldcolumn+S (jt_column_rectappendold)=(v)) /\ (((jt_index_rectappendold=(v)*jt_row_rectappendold+jt_column_rectappendold) /\ (((((((exists fs_h_jt_rectappendoldleftcode. fs_h_jt_rectappendoldleftcode + S (jt_b_rectappendold) = S ((S (jt_row_rectappendold)) * B)) /\ exists fs_q_jt_rectappendoldleftcode. A = fs_q_jt_rectappendoldleftcode * S ((S (jt_row_rectappendold)) * B) + (jt_b_rectappendold))) /\ (((exists fs_h_jt_rectappendoldleftscale. fs_h_jt_rectappendoldleftscale + S (jt_c_rectappendold) = S ((S (jt_row_rectappendold)) * D)) /\ exists fs_q_jt_rectappendoldleftscale. C = fs_q_jt_rectappendoldleftscale * S ((S (jt_row_rectappendold)) * D) + (jt_c_rectappendold))))) /\ (((((((exists fs_h_jt_rectappendoldrightcode. fs_h_jt_rectappendoldrightcode + S (jt_d_rectappendold) = S ((S (jt_column_rectappendold)) * F)) /\ exists fs_q_jt_rectappendoldrightcode. E = fs_q_jt_rectappendoldrightcode * S ((S (jt_column_rectappendold)) * F) + (jt_d_rectappendold))) /\ (((exists fs_h_jt_rectappendoldrightscale. fs_h_jt_rectappendoldrightscale + S (jt_e_rectappendold) = S ((S (jt_column_rectappendold)) * H)) /\ exists fs_q_jt_rectappendoldrightscale. G = fs_q_jt_rectappendoldrightscale * S ((S (jt_column_rectappendold)) * H) + (jt_e_rectappendold))))) /\ (((((((exists fs_h_jt_rectappendoldoutputcode. fs_h_jt_rectappendoldoutputcode + S (jt_f_rectappendold) = S ((S (jt_index_rectappendold)) * Q)) /\ exists fs_q_jt_rectappendoldoutputcode. P = fs_q_jt_rectappendoldoutputcode * S ((S (jt_index_rectappendold)) * Q) + (jt_f_rectappendold))) /\ (((exists fs_h_jt_rectappendoldoutputscale. fs_h_jt_rectappendoldoutputscale + S (jt_g_rectappendold) = S ((S (jt_index_rectappendold)) * T)) /\ exists fs_q_jt_rectappendoldoutputscale. R = fs_q_jt_rectappendoldoutputscale * S ((S (jt_index_rectappendold)) * T) + (jt_g_rectappendold))))) /\ (((((forall jt_index_rectappendoldcrtbound. (exists jt_gap_rectappendoldcrtboundindex. jt_gap_rectappendoldcrtboundindex+S (jt_index_rectappendoldcrtbound)=(k)) -> exists jt_value_rectappendoldcrtbound. ((((exists fs_h_jt_rectappendoldcrtboundat. fs_h_jt_rectappendoldcrtboundat + S (jt_value_rectappendoldcrtbound) = S ((S (jt_index_rectappendoldcrtbound)) * jt_g_rectappendold)) /\ exists fs_q_jt_rectappendoldcrtboundat. jt_f_rectappendold = fs_q_jt_rectappendoldcrtboundat * S ((S (jt_index_rectappendoldcrtbound)) * jt_g_rectappendold) + (jt_value_rectappendoldcrtbound))) /\ (exists jt_gap_rectappendoldcrtboundvalue. jt_gap_rectappendoldcrtboundvalue+S (jt_value_rectappendoldcrtbound)=(m*n)))) /\ (((forall jt_index_rectappendoldcrtleft jt_left_rectappendoldcrtleft jt_right_rectappendoldcrtleft. (exists jt_gap_rectappendoldcrtleftindex. jt_gap_rectappendoldcrtleftindex+S (jt_index_rectappendoldcrtleft)=(k)) -> (((exists fs_h_jt_rectappendoldcrtleftleft. fs_h_jt_rectappendoldcrtleftleft + S (jt_left_rectappendoldcrtleft) = S ((S (jt_index_rectappendoldcrtleft)) * jt_g_rectappendold)) /\ exists fs_q_jt_rectappendoldcrtleftleft. jt_f_rectappendold = fs_q_jt_rectappendoldcrtleftleft * S ((S (jt_index_rectappendoldcrtleft)) * jt_g_rectappendold) + (jt_left_rectappendoldcrtleft))) -> (((exists fs_h_jt_rectappendoldcrtleftright. fs_h_jt_rectappendoldcrtleftright + S (jt_right_rectappendoldcrtleft) = S ((S (jt_index_rectappendoldcrtleft)) * jt_c_rectappendold)) /\ exists fs_q_jt_rectappendoldcrtleftright. jt_b_rectappendold = fs_q_jt_rectappendoldcrtleftright * S ((S (jt_index_rectappendoldcrtleft)) * jt_c_rectappendold) + (jt_right_rectappendoldcrtleft))) -> (exists jt_left_rectappendoldcrtleftmod jt_right_rectappendoldcrtleftmod. (jt_left_rectappendoldcrtleft)+(m)*jt_left_rectappendoldcrtleftmod=(jt_right_rectappendoldcrtleft)+(m)*jt_right_rectappendoldcrtleftmod)) /\ (forall jt_index_rectappendoldcrtright jt_left_rectappendoldcrtright jt_right_rectappendoldcrtright. (exists jt_gap_rectappendoldcrtrightindex. jt_gap_rectappendoldcrtrightindex+S (jt_index_rectappendoldcrtright)=(k)) -> (((exists fs_h_jt_rectappendoldcrtrightleft. fs_h_jt_rectappendoldcrtrightleft + S (jt_left_rectappendoldcrtright) = S ((S (jt_index_rectappendoldcrtright)) * jt_g_rectappendold)) /\ exists fs_q_jt_rectappendoldcrtrightleft. jt_f_rectappendold = fs_q_jt_rectappendoldcrtrightleft * S ((S (jt_index_rectappendoldcrtright)) * jt_g_rectappendold) + (jt_left_rectappendoldcrtright))) -> (((exists fs_h_jt_rectappendoldcrtrightright. fs_h_jt_rectappendoldcrtrightright + S (jt_right_rectappendoldcrtright) = S ((S (jt_index_rectappendoldcrtright)) * jt_e_rectappendold)) /\ exists fs_q_jt_rectappendoldcrtrightright. jt_d_rectappendold = fs_q_jt_rectappendoldcrtrightright * S ((S (jt_index_rectappendoldcrtright)) * jt_e_rectappendold) + (jt_right_rectappendoldcrtright))) -> (exists jt_left_rectappendoldcrtrightmod jt_right_rectappendoldcrtrightmod. (jt_left_rectappendoldcrtright)+(n)*jt_left_rectappendoldcrtrightmod=(jt_right_rectappendoldcrtright)+(n)*jt_right_rectappendoldcrtrightmod)))))) /\ (forall jt_divisor_rectappendoldprimitive. (exists jt_factor_rectappendoldprimitivemodulus. (m*n)=(jt_divisor_rectappendoldprimitive)*jt_factor_rectappendoldprimitivemodulus) -> (forall jt_index_rectappendoldprimitivecoordinates jt_value_rectappendoldprimitivecoordinates. (exists jt_gap_rectappendoldprimitivecoordinatesindex. jt_gap_rectappendoldprimitivecoordinatesindex+S (jt_index_rectappendoldprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendoldprimitivecoordinatesat. fs_h_jt_rectappendoldprimitivecoordinatesat + S (jt_value_rectappendoldprimitivecoordinates) = S ((S (jt_index_rectappendoldprimitivecoordinates)) * jt_g_rectappendold)) /\ exists fs_q_jt_rectappendoldprimitivecoordinatesat. jt_f_rectappendold = fs_q_jt_rectappendoldprimitivecoordinatesat * S ((S (jt_index_rectappendoldprimitivecoordinates)) * jt_g_rectappendold) + (jt_value_rectappendoldprimitivecoordinates))) -> (exists jt_factor_rectappendoldprimitivecoordinatesdivides. (jt_value_rectappendoldprimitivecoordinates)=(jt_divisor_rectappendoldprimitive)*jt_factor_rectappendoldprimitivecoordinatesdivides)) -> jt_divisor_rectappendoldprimitive=1))))))))))))))) -> (exists jt_gap_rectappendbound. jt_gap_rectappendbound+S (q)=(u*v)) -> exists U V W X. forall jt_index_rectappendnew. (exists jt_gap_rectappendnewindex. jt_gap_rectappendnewindex+S (jt_index_rectappendnew)=(S q)) -> exists jt_row_rectappendnew jt_column_rectappendnew jt_b_rectappendnew jt_c_rectappendnew jt_d_rectappendnew jt_e_rectappendnew jt_f_rectappendnew jt_g_rectappendnew. ((exists jt_gap_rectappendnewrow. jt_gap_rectappendnewrow+S (jt_row_rectappendnew)=(u)) /\ (((exists jt_gap_rectappendnewcolumn. jt_gap_rectappendnewcolumn+S (jt_column_rectappendnew)=(v)) /\ (((jt_index_rectappendnew=(v)*jt_row_rectappendnew+jt_column_rectappendnew) /\ (((((((exists fs_h_jt_rectappendnewleftcode. fs_h_jt_rectappendnewleftcode + S (jt_b_rectappendnew) = S ((S (jt_row_rectappendnew)) * B)) /\ exists fs_q_jt_rectappendnewleftcode. A = fs_q_jt_rectappendnewleftcode * S ((S (jt_row_rectappendnew)) * B) + (jt_b_rectappendnew))) /\ (((exists fs_h_jt_rectappendnewleftscale. fs_h_jt_rectappendnewleftscale + S (jt_c_rectappendnew) = S ((S (jt_row_rectappendnew)) * D)) /\ exists fs_q_jt_rectappendnewleftscale. C = fs_q_jt_rectappendnewleftscale * S ((S (jt_row_rectappendnew)) * D) + (jt_c_rectappendnew))))) /\ (((((((exists fs_h_jt_rectappendnewrightcode. fs_h_jt_rectappendnewrightcode + S (jt_d_rectappendnew) = S ((S (jt_column_rectappendnew)) * F)) /\ exists fs_q_jt_rectappendnewrightcode. E = fs_q_jt_rectappendnewrightcode * S ((S (jt_column_rectappendnew)) * F) + (jt_d_rectappendnew))) /\ (((exists fs_h_jt_rectappendnewrightscale. fs_h_jt_rectappendnewrightscale + S (jt_e_rectappendnew) = S ((S (jt_column_rectappendnew)) * H)) /\ exists fs_q_jt_rectappendnewrightscale. G = fs_q_jt_rectappendnewrightscale * S ((S (jt_column_rectappendnew)) * H) + (jt_e_rectappendnew))))) /\ (((((((exists fs_h_jt_rectappendnewoutputcode. fs_h_jt_rectappendnewoutputcode + S (jt_f_rectappendnew) = S ((S (jt_index_rectappendnew)) * V)) /\ exists fs_q_jt_rectappendnewoutputcode. U = fs_q_jt_rectappendnewoutputcode * S ((S (jt_index_rectappendnew)) * V) + (jt_f_rectappendnew))) /\ (((exists fs_h_jt_rectappendnewoutputscale. fs_h_jt_rectappendnewoutputscale + S (jt_g_rectappendnew) = S ((S (jt_index_rectappendnew)) * X)) /\ exists fs_q_jt_rectappendnewoutputscale. W = fs_q_jt_rectappendnewoutputscale * S ((S (jt_index_rectappendnew)) * X) + (jt_g_rectappendnew))))) /\ (((((forall jt_index_rectappendnewcrtbound. (exists jt_gap_rectappendnewcrtboundindex. jt_gap_rectappendnewcrtboundindex+S (jt_index_rectappendnewcrtbound)=(k)) -> exists jt_value_rectappendnewcrtbound. ((((exists fs_h_jt_rectappendnewcrtboundat. fs_h_jt_rectappendnewcrtboundat + S (jt_value_rectappendnewcrtbound) = S ((S (jt_index_rectappendnewcrtbound)) * jt_g_rectappendnew)) /\ exists fs_q_jt_rectappendnewcrtboundat. jt_f_rectappendnew = fs_q_jt_rectappendnewcrtboundat * S ((S (jt_index_rectappendnewcrtbound)) * jt_g_rectappendnew) + (jt_value_rectappendnewcrtbound))) /\ (exists jt_gap_rectappendnewcrtboundvalue. jt_gap_rectappendnewcrtboundvalue+S (jt_value_rectappendnewcrtbound)=(m*n)))) /\ (((forall jt_index_rectappendnewcrtleft jt_left_rectappendnewcrtleft jt_right_rectappendnewcrtleft. (exists jt_gap_rectappendnewcrtleftindex. jt_gap_rectappendnewcrtleftindex+S (jt_index_rectappendnewcrtleft)=(k)) -> (((exists fs_h_jt_rectappendnewcrtleftleft. fs_h_jt_rectappendnewcrtleftleft + S (jt_left_rectappendnewcrtleft) = S ((S (jt_index_rectappendnewcrtleft)) * jt_g_rectappendnew)) /\ exists fs_q_jt_rectappendnewcrtleftleft. jt_f_rectappendnew = fs_q_jt_rectappendnewcrtleftleft * S ((S (jt_index_rectappendnewcrtleft)) * jt_g_rectappendnew) + (jt_left_rectappendnewcrtleft))) -> (((exists fs_h_jt_rectappendnewcrtleftright. fs_h_jt_rectappendnewcrtleftright + S (jt_right_rectappendnewcrtleft) = S ((S (jt_index_rectappendnewcrtleft)) * jt_c_rectappendnew)) /\ exists fs_q_jt_rectappendnewcrtleftright. jt_b_rectappendnew = fs_q_jt_rectappendnewcrtleftright * S ((S (jt_index_rectappendnewcrtleft)) * jt_c_rectappendnew) + (jt_right_rectappendnewcrtleft))) -> (exists jt_left_rectappendnewcrtleftmod jt_right_rectappendnewcrtleftmod. (jt_left_rectappendnewcrtleft)+(m)*jt_left_rectappendnewcrtleftmod=(jt_right_rectappendnewcrtleft)+(m)*jt_right_rectappendnewcrtleftmod)) /\ (forall jt_index_rectappendnewcrtright jt_left_rectappendnewcrtright jt_right_rectappendnewcrtright. (exists jt_gap_rectappendnewcrtrightindex. jt_gap_rectappendnewcrtrightindex+S (jt_index_rectappendnewcrtright)=(k)) -> (((exists fs_h_jt_rectappendnewcrtrightleft. fs_h_jt_rectappendnewcrtrightleft + S (jt_left_rectappendnewcrtright) = S ((S (jt_index_rectappendnewcrtright)) * jt_g_rectappendnew)) /\ exists fs_q_jt_rectappendnewcrtrightleft. jt_f_rectappendnew = fs_q_jt_rectappendnewcrtrightleft * S ((S (jt_index_rectappendnewcrtright)) * jt_g_rectappendnew) + (jt_left_rectappendnewcrtright))) -> (((exists fs_h_jt_rectappendnewcrtrightright. fs_h_jt_rectappendnewcrtrightright + S (jt_right_rectappendnewcrtright) = S ((S (jt_index_rectappendnewcrtright)) * jt_e_rectappendnew)) /\ exists fs_q_jt_rectappendnewcrtrightright. jt_d_rectappendnew = fs_q_jt_rectappendnewcrtrightright * S ((S (jt_index_rectappendnewcrtright)) * jt_e_rectappendnew) + (jt_right_rectappendnewcrtright))) -> (exists jt_left_rectappendnewcrtrightmod jt_right_rectappendnewcrtrightmod. (jt_left_rectappendnewcrtright)+(n)*jt_left_rectappendnewcrtrightmod=(jt_right_rectappendnewcrtright)+(n)*jt_right_rectappendnewcrtrightmod)))))) /\ (forall jt_divisor_rectappendnewprimitive. (exists jt_factor_rectappendnewprimitivemodulus. (m*n)=(jt_divisor_rectappendnewprimitive)*jt_factor_rectappendnewprimitivemodulus) -> (forall jt_index_rectappendnewprimitivecoordinates jt_value_rectappendnewprimitivecoordinates. (exists jt_gap_rectappendnewprimitivecoordinatesindex. jt_gap_rectappendnewprimitivecoordinatesindex+S (jt_index_rectappendnewprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectappendnewprimitivecoordinatesat. fs_h_jt_rectappendnewprimitivecoordinatesat + S (jt_value_rectappendnewprimitivecoordinates) = S ((S (jt_index_rectappendnewprimitivecoordinates)) * jt_g_rectappendnew)) /\ exists fs_q_jt_rectappendnewprimitivecoordinatesat. jt_f_rectappendnew = fs_q_jt_rectappendnewprimitivecoordinatesat * S ((S (jt_index_rectappendnewprimitivecoordinates)) * jt_g_rectappendnew) + (jt_value_rectappendnewprimitivecoordinates))) -> (exists jt_factor_rectappendnewprimitivecoordinatesdivides. (jt_value_rectappendnewprimitivecoordinates)=(jt_divisor_rectappendnewprimitive)*jt_factor_rectappendnewprimitivecoordinatesdivides)) -> jt_divisor_rectappendnewprimitive=1))))))))))))))