jordan_rectangle_crt_successor

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v q. ~(m=0) -> ~(n=0) -> (forall jt_divisor_rectsuccessorcop. (exists jt_factor_rectsuccessorcopa. (m)=(jt_divisor_rectsuccessorcop)*jt_factor_rectsuccessorcopa) -> (exists jt_factor_rectsuccessorcopb. (n)=(jt_divisor_rectsuccessorcop)*jt_factor_rectsuccessorcopb) -> jt_divisor_rectsuccessorcop=1) -> (((forall jt_i_rectsuccessorleft. (exists jt_gap_rectsuccessorleftsoundindex. jt_gap_rectsuccessorleftsoundindex+S (jt_i_rectsuccessorleft)=(u)) -> exists jt_b_rectsuccessorleft jt_c_rectsuccessorleft. ((((((exists fs_h_jt_rectsuccessorleftsoundcode. fs_h_jt_rectsuccessorleftsoundcode + S (jt_b_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * B)) /\ exists fs_q_jt_rectsuccessorleftsoundcode. A = fs_q_jt_rectsuccessorleftsoundcode * S ((S (jt_i_rectsuccessorleft)) * B) + (jt_b_rectsuccessorleft))) /\ (((exists fs_h_jt_rectsuccessorleftsoundscale. fs_h_jt_rectsuccessorleftsoundscale + S (jt_c_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * D)) /\ exists fs_q_jt_rectsuccessorleftsoundscale. C = fs_q_jt_rectsuccessorleftsoundscale * S ((S (jt_i_rectsuccessorleft)) * D) + (jt_c_rectsuccessorleft))))) /\ (((forall jt_index_rectsuccessorleftbound. (exists jt_gap_rectsuccessorleftboundindex. jt_gap_rectsuccessorleftboundindex+S (jt_index_rectsuccessorleftbound)=(k)) -> exists jt_value_rectsuccessorleftbound. ((((exists fs_h_jt_rectsuccessorleftboundat. fs_h_jt_rectsuccessorleftboundat + S (jt_value_rectsuccessorleftbound) = S ((S (jt_index_rectsuccessorleftbound)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftboundat. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftboundat * S ((S (jt_index_rectsuccessorleftbound)) * jt_c_rectsuccessorleft) + (jt_value_rectsuccessorleftbound))) /\ (exists jt_gap_rectsuccessorleftboundvalue. jt_gap_rectsuccessorleftboundvalue+S (jt_value_rectsuccessorleftbound)=(m)))) /\ (forall jt_divisor_rectsuccessorleftprimitive. (exists jt_factor_rectsuccessorleftprimitivemodulus. (m)=(jt_divisor_rectsuccessorleftprimitive)*jt_factor_rectsuccessorleftprimitivemodulus) -> (forall jt_index_rectsuccessorleftprimitivecoordinates jt_value_rectsuccessorleftprimitivecoordinates. (exists jt_gap_rectsuccessorleftprimitivecoordinatesindex. jt_gap_rectsuccessorleftprimitivecoordinatesindex+S (jt_index_rectsuccessorleftprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessorleftprimitivecoordinatesat. fs_h_jt_rectsuccessorleftprimitivecoordinatesat + S (jt_value_rectsuccessorleftprimitivecoordinates) = S ((S (jt_index_rectsuccessorleftprimitivecoordinates)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftprimitivecoordinatesat. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftprimitivecoordinatesat * S ((S (jt_index_rectsuccessorleftprimitivecoordinates)) * jt_c_rectsuccessorleft) + (jt_value_rectsuccessorleftprimitivecoordinates))) -> (exists jt_factor_rectsuccessorleftprimitivecoordinatesdivides. (jt_value_rectsuccessorleftprimitivecoordinates)=(jt_divisor_rectsuccessorleftprimitive)*jt_factor_rectsuccessorleftprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessorleftprimitive=1))))) /\ (((forall jt_b_rectsuccessorleft jt_c_rectsuccessorleft. (forall jt_index_rectsuccessorleftinputbound. (exists jt_gap_rectsuccessorleftinputboundindex. jt_gap_rectsuccessorleftinputboundindex+S (jt_index_rectsuccessorleftinputbound)=(k)) -> exists jt_value_rectsuccessorleftinputbound. ((((exists fs_h_jt_rectsuccessorleftinputboundat. fs_h_jt_rectsuccessorleftinputboundat + S (jt_value_rectsuccessorleftinputbound) = S ((S (jt_index_rectsuccessorleftinputbound)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftinputboundat. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftinputboundat * S ((S (jt_index_rectsuccessorleftinputbound)) * jt_c_rectsuccessorleft) + (jt_value_rectsuccessorleftinputbound))) /\ (exists jt_gap_rectsuccessorleftinputboundvalue. jt_gap_rectsuccessorleftinputboundvalue+S (jt_value_rectsuccessorleftinputbound)=(m)))) -> (forall jt_divisor_rectsuccessorleftinputprimitive. (exists jt_factor_rectsuccessorleftinputprimitivemodulus. (m)=(jt_divisor_rectsuccessorleftinputprimitive)*jt_factor_rectsuccessorleftinputprimitivemodulus) -> (forall jt_index_rectsuccessorleftinputprimitivecoordinates jt_value_rectsuccessorleftinputprimitivecoordinates. (exists jt_gap_rectsuccessorleftinputprimitivecoordinatesindex. jt_gap_rectsuccessorleftinputprimitivecoordinatesindex+S (jt_index_rectsuccessorleftinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessorleftinputprimitivecoordinatesat. fs_h_jt_rectsuccessorleftinputprimitivecoordinatesat + S (jt_value_rectsuccessorleftinputprimitivecoordinates) = S ((S (jt_index_rectsuccessorleftinputprimitivecoordinates)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftinputprimitivecoordinatesat. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftinputprimitivecoordinatesat * S ((S (jt_index_rectsuccessorleftinputprimitivecoordinates)) * jt_c_rectsuccessorleft) + (jt_value_rectsuccessorleftinputprimitivecoordinates))) -> (exists jt_factor_rectsuccessorleftinputprimitivecoordinatesdivides. (jt_value_rectsuccessorleftinputprimitivecoordinates)=(jt_divisor_rectsuccessorleftinputprimitive)*jt_factor_rectsuccessorleftinputprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessorleftinputprimitive=1) -> exists jt_i_rectsuccessorleft jt_d_rectsuccessorleft jt_e_rectsuccessorleft. ((exists jt_gap_rectsuccessorleftcompleteindex. jt_gap_rectsuccessorleftcompleteindex+S (jt_i_rectsuccessorleft)=(u)) /\ (((((((exists fs_h_jt_rectsuccessorleftcompletecode. fs_h_jt_rectsuccessorleftcompletecode + S (jt_d_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * B)) /\ exists fs_q_jt_rectsuccessorleftcompletecode. A = fs_q_jt_rectsuccessorleftcompletecode * S ((S (jt_i_rectsuccessorleft)) * B) + (jt_d_rectsuccessorleft))) /\ (((exists fs_h_jt_rectsuccessorleftcompletescale. fs_h_jt_rectsuccessorleftcompletescale + S (jt_e_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * D)) /\ exists fs_q_jt_rectsuccessorleftcompletescale. C = fs_q_jt_rectsuccessorleftcompletescale * S ((S (jt_i_rectsuccessorleft)) * D) + (jt_e_rectsuccessorleft))))) /\ (forall jt_index_rectsuccessorleftrepresented jt_left_rectsuccessorleftrepresented jt_right_rectsuccessorleftrepresented. (exists jt_gap_rectsuccessorleftrepresentedindex. jt_gap_rectsuccessorleftrepresentedindex+S (jt_index_rectsuccessorleftrepresented)=(k)) -> (((exists fs_h_jt_rectsuccessorleftrepresentedleft. fs_h_jt_rectsuccessorleftrepresentedleft + S (jt_left_rectsuccessorleftrepresented) = S ((S (jt_index_rectsuccessorleftrepresented)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftrepresentedleft. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftrepresentedleft * S ((S (jt_index_rectsuccessorleftrepresented)) * jt_c_rectsuccessorleft) + (jt_left_rectsuccessorleftrepresented))) -> (((exists fs_h_jt_rectsuccessorleftrepresentedright. fs_h_jt_rectsuccessorleftrepresentedright + S (jt_right_rectsuccessorleftrepresented) = S ((S (jt_index_rectsuccessorleftrepresented)) * jt_e_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftrepresentedright. jt_d_rectsuccessorleft = fs_q_jt_rectsuccessorleftrepresentedright * S ((S (jt_index_rectsuccessorleftrepresented)) * jt_e_rectsuccessorleft) + (jt_right_rectsuccessorleftrepresented))) -> jt_left_rectsuccessorleftrepresented=jt_right_rectsuccessorleftrepresented))))) /\ (forall jt_i_rectsuccessorleft jt_h_rectsuccessorleft jt_b_rectsuccessorleft jt_c_rectsuccessorleft jt_d_rectsuccessorleft jt_e_rectsuccessorleft. (exists jt_gap_rectsuccessorleftfirstindex. jt_gap_rectsuccessorleftfirstindex+S (jt_i_rectsuccessorleft)=(u)) -> (exists jt_gap_rectsuccessorleftsecondindex. jt_gap_rectsuccessorleftsecondindex+S (jt_h_rectsuccessorleft)=(u)) -> (((((exists fs_h_jt_rectsuccessorleftfirstcode. fs_h_jt_rectsuccessorleftfirstcode + S (jt_b_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * B)) /\ exists fs_q_jt_rectsuccessorleftfirstcode. A = fs_q_jt_rectsuccessorleftfirstcode * S ((S (jt_i_rectsuccessorleft)) * B) + (jt_b_rectsuccessorleft))) /\ (((exists fs_h_jt_rectsuccessorleftfirstscale. fs_h_jt_rectsuccessorleftfirstscale + S (jt_c_rectsuccessorleft) = S ((S (jt_i_rectsuccessorleft)) * D)) /\ exists fs_q_jt_rectsuccessorleftfirstscale. C = fs_q_jt_rectsuccessorleftfirstscale * S ((S (jt_i_rectsuccessorleft)) * D) + (jt_c_rectsuccessorleft))))) -> (((((exists fs_h_jt_rectsuccessorleftsecondcode. fs_h_jt_rectsuccessorleftsecondcode + S (jt_d_rectsuccessorleft) = S ((S (jt_h_rectsuccessorleft)) * B)) /\ exists fs_q_jt_rectsuccessorleftsecondcode. A = fs_q_jt_rectsuccessorleftsecondcode * S ((S (jt_h_rectsuccessorleft)) * B) + (jt_d_rectsuccessorleft))) /\ (((exists fs_h_jt_rectsuccessorleftsecondscale. fs_h_jt_rectsuccessorleftsecondscale + S (jt_e_rectsuccessorleft) = S ((S (jt_h_rectsuccessorleft)) * D)) /\ exists fs_q_jt_rectsuccessorleftsecondscale. C = fs_q_jt_rectsuccessorleftsecondscale * S ((S (jt_h_rectsuccessorleft)) * D) + (jt_e_rectsuccessorleft))))) -> (forall jt_index_rectsuccessorleftsame jt_left_rectsuccessorleftsame jt_right_rectsuccessorleftsame. (exists jt_gap_rectsuccessorleftsameindex. jt_gap_rectsuccessorleftsameindex+S (jt_index_rectsuccessorleftsame)=(k)) -> (((exists fs_h_jt_rectsuccessorleftsameleft. fs_h_jt_rectsuccessorleftsameleft + S (jt_left_rectsuccessorleftsame) = S ((S (jt_index_rectsuccessorleftsame)) * jt_c_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftsameleft. jt_b_rectsuccessorleft = fs_q_jt_rectsuccessorleftsameleft * S ((S (jt_index_rectsuccessorleftsame)) * jt_c_rectsuccessorleft) + (jt_left_rectsuccessorleftsame))) -> (((exists fs_h_jt_rectsuccessorleftsameright. fs_h_jt_rectsuccessorleftsameright + S (jt_right_rectsuccessorleftsame) = S ((S (jt_index_rectsuccessorleftsame)) * jt_e_rectsuccessorleft)) /\ exists fs_q_jt_rectsuccessorleftsameright. jt_d_rectsuccessorleft = fs_q_jt_rectsuccessorleftsameright * S ((S (jt_index_rectsuccessorleftsame)) * jt_e_rectsuccessorleft) + (jt_right_rectsuccessorleftsame))) -> jt_left_rectsuccessorleftsame=jt_right_rectsuccessorleftsame) -> jt_i_rectsuccessorleft=jt_h_rectsuccessorleft))))) -> (((forall jt_i_rectsuccessorright. (exists jt_gap_rectsuccessorrightsoundindex. jt_gap_rectsuccessorrightsoundindex+S (jt_i_rectsuccessorright)=(v)) -> exists jt_b_rectsuccessorright jt_c_rectsuccessorright. ((((((exists fs_h_jt_rectsuccessorrightsoundcode. fs_h_jt_rectsuccessorrightsoundcode + S (jt_b_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * F)) /\ exists fs_q_jt_rectsuccessorrightsoundcode. E = fs_q_jt_rectsuccessorrightsoundcode * S ((S (jt_i_rectsuccessorright)) * F) + (jt_b_rectsuccessorright))) /\ (((exists fs_h_jt_rectsuccessorrightsoundscale. fs_h_jt_rectsuccessorrightsoundscale + S (jt_c_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * H)) /\ exists fs_q_jt_rectsuccessorrightsoundscale. G = fs_q_jt_rectsuccessorrightsoundscale * S ((S (jt_i_rectsuccessorright)) * H) + (jt_c_rectsuccessorright))))) /\ (((forall jt_index_rectsuccessorrightbound. (exists jt_gap_rectsuccessorrightboundindex. jt_gap_rectsuccessorrightboundindex+S (jt_index_rectsuccessorrightbound)=(k)) -> exists jt_value_rectsuccessorrightbound. ((((exists fs_h_jt_rectsuccessorrightboundat. fs_h_jt_rectsuccessorrightboundat + S (jt_value_rectsuccessorrightbound) = S ((S (jt_index_rectsuccessorrightbound)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightboundat. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightboundat * S ((S (jt_index_rectsuccessorrightbound)) * jt_c_rectsuccessorright) + (jt_value_rectsuccessorrightbound))) /\ (exists jt_gap_rectsuccessorrightboundvalue. jt_gap_rectsuccessorrightboundvalue+S (jt_value_rectsuccessorrightbound)=(n)))) /\ (forall jt_divisor_rectsuccessorrightprimitive. (exists jt_factor_rectsuccessorrightprimitivemodulus. (n)=(jt_divisor_rectsuccessorrightprimitive)*jt_factor_rectsuccessorrightprimitivemodulus) -> (forall jt_index_rectsuccessorrightprimitivecoordinates jt_value_rectsuccessorrightprimitivecoordinates. (exists jt_gap_rectsuccessorrightprimitivecoordinatesindex. jt_gap_rectsuccessorrightprimitivecoordinatesindex+S (jt_index_rectsuccessorrightprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessorrightprimitivecoordinatesat. fs_h_jt_rectsuccessorrightprimitivecoordinatesat + S (jt_value_rectsuccessorrightprimitivecoordinates) = S ((S (jt_index_rectsuccessorrightprimitivecoordinates)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightprimitivecoordinatesat. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightprimitivecoordinatesat * S ((S (jt_index_rectsuccessorrightprimitivecoordinates)) * jt_c_rectsuccessorright) + (jt_value_rectsuccessorrightprimitivecoordinates))) -> (exists jt_factor_rectsuccessorrightprimitivecoordinatesdivides. (jt_value_rectsuccessorrightprimitivecoordinates)=(jt_divisor_rectsuccessorrightprimitive)*jt_factor_rectsuccessorrightprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessorrightprimitive=1))))) /\ (((forall jt_b_rectsuccessorright jt_c_rectsuccessorright. (forall jt_index_rectsuccessorrightinputbound. (exists jt_gap_rectsuccessorrightinputboundindex. jt_gap_rectsuccessorrightinputboundindex+S (jt_index_rectsuccessorrightinputbound)=(k)) -> exists jt_value_rectsuccessorrightinputbound. ((((exists fs_h_jt_rectsuccessorrightinputboundat. fs_h_jt_rectsuccessorrightinputboundat + S (jt_value_rectsuccessorrightinputbound) = S ((S (jt_index_rectsuccessorrightinputbound)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightinputboundat. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightinputboundat * S ((S (jt_index_rectsuccessorrightinputbound)) * jt_c_rectsuccessorright) + (jt_value_rectsuccessorrightinputbound))) /\ (exists jt_gap_rectsuccessorrightinputboundvalue. jt_gap_rectsuccessorrightinputboundvalue+S (jt_value_rectsuccessorrightinputbound)=(n)))) -> (forall jt_divisor_rectsuccessorrightinputprimitive. (exists jt_factor_rectsuccessorrightinputprimitivemodulus. (n)=(jt_divisor_rectsuccessorrightinputprimitive)*jt_factor_rectsuccessorrightinputprimitivemodulus) -> (forall jt_index_rectsuccessorrightinputprimitivecoordinates jt_value_rectsuccessorrightinputprimitivecoordinates. (exists jt_gap_rectsuccessorrightinputprimitivecoordinatesindex. jt_gap_rectsuccessorrightinputprimitivecoordinatesindex+S (jt_index_rectsuccessorrightinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessorrightinputprimitivecoordinatesat. fs_h_jt_rectsuccessorrightinputprimitivecoordinatesat + S (jt_value_rectsuccessorrightinputprimitivecoordinates) = S ((S (jt_index_rectsuccessorrightinputprimitivecoordinates)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightinputprimitivecoordinatesat. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightinputprimitivecoordinatesat * S ((S (jt_index_rectsuccessorrightinputprimitivecoordinates)) * jt_c_rectsuccessorright) + (jt_value_rectsuccessorrightinputprimitivecoordinates))) -> (exists jt_factor_rectsuccessorrightinputprimitivecoordinatesdivides. (jt_value_rectsuccessorrightinputprimitivecoordinates)=(jt_divisor_rectsuccessorrightinputprimitive)*jt_factor_rectsuccessorrightinputprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessorrightinputprimitive=1) -> exists jt_i_rectsuccessorright jt_d_rectsuccessorright jt_e_rectsuccessorright. ((exists jt_gap_rectsuccessorrightcompleteindex. jt_gap_rectsuccessorrightcompleteindex+S (jt_i_rectsuccessorright)=(v)) /\ (((((((exists fs_h_jt_rectsuccessorrightcompletecode. fs_h_jt_rectsuccessorrightcompletecode + S (jt_d_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * F)) /\ exists fs_q_jt_rectsuccessorrightcompletecode. E = fs_q_jt_rectsuccessorrightcompletecode * S ((S (jt_i_rectsuccessorright)) * F) + (jt_d_rectsuccessorright))) /\ (((exists fs_h_jt_rectsuccessorrightcompletescale. fs_h_jt_rectsuccessorrightcompletescale + S (jt_e_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * H)) /\ exists fs_q_jt_rectsuccessorrightcompletescale. G = fs_q_jt_rectsuccessorrightcompletescale * S ((S (jt_i_rectsuccessorright)) * H) + (jt_e_rectsuccessorright))))) /\ (forall jt_index_rectsuccessorrightrepresented jt_left_rectsuccessorrightrepresented jt_right_rectsuccessorrightrepresented. (exists jt_gap_rectsuccessorrightrepresentedindex. jt_gap_rectsuccessorrightrepresentedindex+S (jt_index_rectsuccessorrightrepresented)=(k)) -> (((exists fs_h_jt_rectsuccessorrightrepresentedleft. fs_h_jt_rectsuccessorrightrepresentedleft + S (jt_left_rectsuccessorrightrepresented) = S ((S (jt_index_rectsuccessorrightrepresented)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightrepresentedleft. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightrepresentedleft * S ((S (jt_index_rectsuccessorrightrepresented)) * jt_c_rectsuccessorright) + (jt_left_rectsuccessorrightrepresented))) -> (((exists fs_h_jt_rectsuccessorrightrepresentedright. fs_h_jt_rectsuccessorrightrepresentedright + S (jt_right_rectsuccessorrightrepresented) = S ((S (jt_index_rectsuccessorrightrepresented)) * jt_e_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightrepresentedright. jt_d_rectsuccessorright = fs_q_jt_rectsuccessorrightrepresentedright * S ((S (jt_index_rectsuccessorrightrepresented)) * jt_e_rectsuccessorright) + (jt_right_rectsuccessorrightrepresented))) -> jt_left_rectsuccessorrightrepresented=jt_right_rectsuccessorrightrepresented))))) /\ (forall jt_i_rectsuccessorright jt_h_rectsuccessorright jt_b_rectsuccessorright jt_c_rectsuccessorright jt_d_rectsuccessorright jt_e_rectsuccessorright. (exists jt_gap_rectsuccessorrightfirstindex. jt_gap_rectsuccessorrightfirstindex+S (jt_i_rectsuccessorright)=(v)) -> (exists jt_gap_rectsuccessorrightsecondindex. jt_gap_rectsuccessorrightsecondindex+S (jt_h_rectsuccessorright)=(v)) -> (((((exists fs_h_jt_rectsuccessorrightfirstcode. fs_h_jt_rectsuccessorrightfirstcode + S (jt_b_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * F)) /\ exists fs_q_jt_rectsuccessorrightfirstcode. E = fs_q_jt_rectsuccessorrightfirstcode * S ((S (jt_i_rectsuccessorright)) * F) + (jt_b_rectsuccessorright))) /\ (((exists fs_h_jt_rectsuccessorrightfirstscale. fs_h_jt_rectsuccessorrightfirstscale + S (jt_c_rectsuccessorright) = S ((S (jt_i_rectsuccessorright)) * H)) /\ exists fs_q_jt_rectsuccessorrightfirstscale. G = fs_q_jt_rectsuccessorrightfirstscale * S ((S (jt_i_rectsuccessorright)) * H) + (jt_c_rectsuccessorright))))) -> (((((exists fs_h_jt_rectsuccessorrightsecondcode. fs_h_jt_rectsuccessorrightsecondcode + S (jt_d_rectsuccessorright) = S ((S (jt_h_rectsuccessorright)) * F)) /\ exists fs_q_jt_rectsuccessorrightsecondcode. E = fs_q_jt_rectsuccessorrightsecondcode * S ((S (jt_h_rectsuccessorright)) * F) + (jt_d_rectsuccessorright))) /\ (((exists fs_h_jt_rectsuccessorrightsecondscale. fs_h_jt_rectsuccessorrightsecondscale + S (jt_e_rectsuccessorright) = S ((S (jt_h_rectsuccessorright)) * H)) /\ exists fs_q_jt_rectsuccessorrightsecondscale. G = fs_q_jt_rectsuccessorrightsecondscale * S ((S (jt_h_rectsuccessorright)) * H) + (jt_e_rectsuccessorright))))) -> (forall jt_index_rectsuccessorrightsame jt_left_rectsuccessorrightsame jt_right_rectsuccessorrightsame. (exists jt_gap_rectsuccessorrightsameindex. jt_gap_rectsuccessorrightsameindex+S (jt_index_rectsuccessorrightsame)=(k)) -> (((exists fs_h_jt_rectsuccessorrightsameleft. fs_h_jt_rectsuccessorrightsameleft + S (jt_left_rectsuccessorrightsame) = S ((S (jt_index_rectsuccessorrightsame)) * jt_c_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightsameleft. jt_b_rectsuccessorright = fs_q_jt_rectsuccessorrightsameleft * S ((S (jt_index_rectsuccessorrightsame)) * jt_c_rectsuccessorright) + (jt_left_rectsuccessorrightsame))) -> (((exists fs_h_jt_rectsuccessorrightsameright. fs_h_jt_rectsuccessorrightsameright + S (jt_right_rectsuccessorrightsame) = S ((S (jt_index_rectsuccessorrightsame)) * jt_e_rectsuccessorright)) /\ exists fs_q_jt_rectsuccessorrightsameright. jt_d_rectsuccessorright = fs_q_jt_rectsuccessorrightsameright * S ((S (jt_index_rectsuccessorrightsame)) * jt_e_rectsuccessorright) + (jt_right_rectsuccessorrightsame))) -> jt_left_rectsuccessorrightsame=jt_right_rectsuccessorrightsame) -> jt_i_rectsuccessorright=jt_h_rectsuccessorright))))) -> (exists P Q R T. forall jt_index_rectsuccessorold. (exists jt_gap_rectsuccessoroldindex. jt_gap_rectsuccessoroldindex+S (jt_index_rectsuccessorold)=(q)) -> exists jt_row_rectsuccessorold jt_column_rectsuccessorold jt_b_rectsuccessorold jt_c_rectsuccessorold jt_d_rectsuccessorold jt_e_rectsuccessorold jt_f_rectsuccessorold jt_g_rectsuccessorold. ((exists jt_gap_rectsuccessoroldrow. jt_gap_rectsuccessoroldrow+S (jt_row_rectsuccessorold)=(u)) /\ (((exists jt_gap_rectsuccessoroldcolumn. jt_gap_rectsuccessoroldcolumn+S (jt_column_rectsuccessorold)=(v)) /\ (((jt_index_rectsuccessorold=(v)*jt_row_rectsuccessorold+jt_column_rectsuccessorold) /\ (((((((exists fs_h_jt_rectsuccessoroldleftcode. fs_h_jt_rectsuccessoroldleftcode + S (jt_b_rectsuccessorold) = S ((S (jt_row_rectsuccessorold)) * B)) /\ exists fs_q_jt_rectsuccessoroldleftcode. A = fs_q_jt_rectsuccessoroldleftcode * S ((S (jt_row_rectsuccessorold)) * B) + (jt_b_rectsuccessorold))) /\ (((exists fs_h_jt_rectsuccessoroldleftscale. fs_h_jt_rectsuccessoroldleftscale + S (jt_c_rectsuccessorold) = S ((S (jt_row_rectsuccessorold)) * D)) /\ exists fs_q_jt_rectsuccessoroldleftscale. C = fs_q_jt_rectsuccessoroldleftscale * S ((S (jt_row_rectsuccessorold)) * D) + (jt_c_rectsuccessorold))))) /\ (((((((exists fs_h_jt_rectsuccessoroldrightcode. fs_h_jt_rectsuccessoroldrightcode + S (jt_d_rectsuccessorold) = S ((S (jt_column_rectsuccessorold)) * F)) /\ exists fs_q_jt_rectsuccessoroldrightcode. E = fs_q_jt_rectsuccessoroldrightcode * S ((S (jt_column_rectsuccessorold)) * F) + (jt_d_rectsuccessorold))) /\ (((exists fs_h_jt_rectsuccessoroldrightscale. fs_h_jt_rectsuccessoroldrightscale + S (jt_e_rectsuccessorold) = S ((S (jt_column_rectsuccessorold)) * H)) /\ exists fs_q_jt_rectsuccessoroldrightscale. G = fs_q_jt_rectsuccessoroldrightscale * S ((S (jt_column_rectsuccessorold)) * H) + (jt_e_rectsuccessorold))))) /\ (((((((exists fs_h_jt_rectsuccessoroldoutputcode. fs_h_jt_rectsuccessoroldoutputcode + S (jt_f_rectsuccessorold) = S ((S (jt_index_rectsuccessorold)) * Q)) /\ exists fs_q_jt_rectsuccessoroldoutputcode. P = fs_q_jt_rectsuccessoroldoutputcode * S ((S (jt_index_rectsuccessorold)) * Q) + (jt_f_rectsuccessorold))) /\ (((exists fs_h_jt_rectsuccessoroldoutputscale. fs_h_jt_rectsuccessoroldoutputscale + S (jt_g_rectsuccessorold) = S ((S (jt_index_rectsuccessorold)) * T)) /\ exists fs_q_jt_rectsuccessoroldoutputscale. R = fs_q_jt_rectsuccessoroldoutputscale * S ((S (jt_index_rectsuccessorold)) * T) + (jt_g_rectsuccessorold))))) /\ (((((forall jt_index_rectsuccessoroldcrtbound. (exists jt_gap_rectsuccessoroldcrtboundindex. jt_gap_rectsuccessoroldcrtboundindex+S (jt_index_rectsuccessoroldcrtbound)=(k)) -> exists jt_value_rectsuccessoroldcrtbound. ((((exists fs_h_jt_rectsuccessoroldcrtboundat. fs_h_jt_rectsuccessoroldcrtboundat + S (jt_value_rectsuccessoroldcrtbound) = S ((S (jt_index_rectsuccessoroldcrtbound)) * jt_g_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldcrtboundat. jt_f_rectsuccessorold = fs_q_jt_rectsuccessoroldcrtboundat * S ((S (jt_index_rectsuccessoroldcrtbound)) * jt_g_rectsuccessorold) + (jt_value_rectsuccessoroldcrtbound))) /\ (exists jt_gap_rectsuccessoroldcrtboundvalue. jt_gap_rectsuccessoroldcrtboundvalue+S (jt_value_rectsuccessoroldcrtbound)=(m*n)))) /\ (((forall jt_index_rectsuccessoroldcrtleft jt_left_rectsuccessoroldcrtleft jt_right_rectsuccessoroldcrtleft. (exists jt_gap_rectsuccessoroldcrtleftindex. jt_gap_rectsuccessoroldcrtleftindex+S (jt_index_rectsuccessoroldcrtleft)=(k)) -> (((exists fs_h_jt_rectsuccessoroldcrtleftleft. fs_h_jt_rectsuccessoroldcrtleftleft + S (jt_left_rectsuccessoroldcrtleft) = S ((S (jt_index_rectsuccessoroldcrtleft)) * jt_g_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldcrtleftleft. jt_f_rectsuccessorold = fs_q_jt_rectsuccessoroldcrtleftleft * S ((S (jt_index_rectsuccessoroldcrtleft)) * jt_g_rectsuccessorold) + (jt_left_rectsuccessoroldcrtleft))) -> (((exists fs_h_jt_rectsuccessoroldcrtleftright. fs_h_jt_rectsuccessoroldcrtleftright + S (jt_right_rectsuccessoroldcrtleft) = S ((S (jt_index_rectsuccessoroldcrtleft)) * jt_c_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldcrtleftright. jt_b_rectsuccessorold = fs_q_jt_rectsuccessoroldcrtleftright * S ((S (jt_index_rectsuccessoroldcrtleft)) * jt_c_rectsuccessorold) + (jt_right_rectsuccessoroldcrtleft))) -> (exists jt_left_rectsuccessoroldcrtleftmod jt_right_rectsuccessoroldcrtleftmod. (jt_left_rectsuccessoroldcrtleft)+(m)*jt_left_rectsuccessoroldcrtleftmod=(jt_right_rectsuccessoroldcrtleft)+(m)*jt_right_rectsuccessoroldcrtleftmod)) /\ (forall jt_index_rectsuccessoroldcrtright jt_left_rectsuccessoroldcrtright jt_right_rectsuccessoroldcrtright. (exists jt_gap_rectsuccessoroldcrtrightindex. jt_gap_rectsuccessoroldcrtrightindex+S (jt_index_rectsuccessoroldcrtright)=(k)) -> (((exists fs_h_jt_rectsuccessoroldcrtrightleft. fs_h_jt_rectsuccessoroldcrtrightleft + S (jt_left_rectsuccessoroldcrtright) = S ((S (jt_index_rectsuccessoroldcrtright)) * jt_g_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldcrtrightleft. jt_f_rectsuccessorold = fs_q_jt_rectsuccessoroldcrtrightleft * S ((S (jt_index_rectsuccessoroldcrtright)) * jt_g_rectsuccessorold) + (jt_left_rectsuccessoroldcrtright))) -> (((exists fs_h_jt_rectsuccessoroldcrtrightright. fs_h_jt_rectsuccessoroldcrtrightright + S (jt_right_rectsuccessoroldcrtright) = S ((S (jt_index_rectsuccessoroldcrtright)) * jt_e_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldcrtrightright. jt_d_rectsuccessorold = fs_q_jt_rectsuccessoroldcrtrightright * S ((S (jt_index_rectsuccessoroldcrtright)) * jt_e_rectsuccessorold) + (jt_right_rectsuccessoroldcrtright))) -> (exists jt_left_rectsuccessoroldcrtrightmod jt_right_rectsuccessoroldcrtrightmod. (jt_left_rectsuccessoroldcrtright)+(n)*jt_left_rectsuccessoroldcrtrightmod=(jt_right_rectsuccessoroldcrtright)+(n)*jt_right_rectsuccessoroldcrtrightmod)))))) /\ (forall jt_divisor_rectsuccessoroldprimitive. (exists jt_factor_rectsuccessoroldprimitivemodulus. (m*n)=(jt_divisor_rectsuccessoroldprimitive)*jt_factor_rectsuccessoroldprimitivemodulus) -> (forall jt_index_rectsuccessoroldprimitivecoordinates jt_value_rectsuccessoroldprimitivecoordinates. (exists jt_gap_rectsuccessoroldprimitivecoordinatesindex. jt_gap_rectsuccessoroldprimitivecoordinatesindex+S (jt_index_rectsuccessoroldprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessoroldprimitivecoordinatesat. fs_h_jt_rectsuccessoroldprimitivecoordinatesat + S (jt_value_rectsuccessoroldprimitivecoordinates) = S ((S (jt_index_rectsuccessoroldprimitivecoordinates)) * jt_g_rectsuccessorold)) /\ exists fs_q_jt_rectsuccessoroldprimitivecoordinatesat. jt_f_rectsuccessorold = fs_q_jt_rectsuccessoroldprimitivecoordinatesat * S ((S (jt_index_rectsuccessoroldprimitivecoordinates)) * jt_g_rectsuccessorold) + (jt_value_rectsuccessoroldprimitivecoordinates))) -> (exists jt_factor_rectsuccessoroldprimitivecoordinatesdivides. (jt_value_rectsuccessoroldprimitivecoordinates)=(jt_divisor_rectsuccessoroldprimitive)*jt_factor_rectsuccessoroldprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessoroldprimitive=1))))))))))))))) -> (exists jt_gap_rectsuccessorbound. jt_gap_rectsuccessorbound+S (q)=(u*v)) -> exists P Q R T. forall jt_index_rectsuccessornew. (exists jt_gap_rectsuccessornewindex. jt_gap_rectsuccessornewindex+S (jt_index_rectsuccessornew)=(S q)) -> exists jt_row_rectsuccessornew jt_column_rectsuccessornew jt_b_rectsuccessornew jt_c_rectsuccessornew jt_d_rectsuccessornew jt_e_rectsuccessornew jt_f_rectsuccessornew jt_g_rectsuccessornew. ((exists jt_gap_rectsuccessornewrow. jt_gap_rectsuccessornewrow+S (jt_row_rectsuccessornew)=(u)) /\ (((exists jt_gap_rectsuccessornewcolumn. jt_gap_rectsuccessornewcolumn+S (jt_column_rectsuccessornew)=(v)) /\ (((jt_index_rectsuccessornew=(v)*jt_row_rectsuccessornew+jt_column_rectsuccessornew) /\ (((((((exists fs_h_jt_rectsuccessornewleftcode. fs_h_jt_rectsuccessornewleftcode + S (jt_b_rectsuccessornew) = S ((S (jt_row_rectsuccessornew)) * B)) /\ exists fs_q_jt_rectsuccessornewleftcode. A = fs_q_jt_rectsuccessornewleftcode * S ((S (jt_row_rectsuccessornew)) * B) + (jt_b_rectsuccessornew))) /\ (((exists fs_h_jt_rectsuccessornewleftscale. fs_h_jt_rectsuccessornewleftscale + S (jt_c_rectsuccessornew) = S ((S (jt_row_rectsuccessornew)) * D)) /\ exists fs_q_jt_rectsuccessornewleftscale. C = fs_q_jt_rectsuccessornewleftscale * S ((S (jt_row_rectsuccessornew)) * D) + (jt_c_rectsuccessornew))))) /\ (((((((exists fs_h_jt_rectsuccessornewrightcode. fs_h_jt_rectsuccessornewrightcode + S (jt_d_rectsuccessornew) = S ((S (jt_column_rectsuccessornew)) * F)) /\ exists fs_q_jt_rectsuccessornewrightcode. E = fs_q_jt_rectsuccessornewrightcode * S ((S (jt_column_rectsuccessornew)) * F) + (jt_d_rectsuccessornew))) /\ (((exists fs_h_jt_rectsuccessornewrightscale. fs_h_jt_rectsuccessornewrightscale + S (jt_e_rectsuccessornew) = S ((S (jt_column_rectsuccessornew)) * H)) /\ exists fs_q_jt_rectsuccessornewrightscale. G = fs_q_jt_rectsuccessornewrightscale * S ((S (jt_column_rectsuccessornew)) * H) + (jt_e_rectsuccessornew))))) /\ (((((((exists fs_h_jt_rectsuccessornewoutputcode. fs_h_jt_rectsuccessornewoutputcode + S (jt_f_rectsuccessornew) = S ((S (jt_index_rectsuccessornew)) * Q)) /\ exists fs_q_jt_rectsuccessornewoutputcode. P = fs_q_jt_rectsuccessornewoutputcode * S ((S (jt_index_rectsuccessornew)) * Q) + (jt_f_rectsuccessornew))) /\ (((exists fs_h_jt_rectsuccessornewoutputscale. fs_h_jt_rectsuccessornewoutputscale + S (jt_g_rectsuccessornew) = S ((S (jt_index_rectsuccessornew)) * T)) /\ exists fs_q_jt_rectsuccessornewoutputscale. R = fs_q_jt_rectsuccessornewoutputscale * S ((S (jt_index_rectsuccessornew)) * T) + (jt_g_rectsuccessornew))))) /\ (((((forall jt_index_rectsuccessornewcrtbound. (exists jt_gap_rectsuccessornewcrtboundindex. jt_gap_rectsuccessornewcrtboundindex+S (jt_index_rectsuccessornewcrtbound)=(k)) -> exists jt_value_rectsuccessornewcrtbound. ((((exists fs_h_jt_rectsuccessornewcrtboundat. fs_h_jt_rectsuccessornewcrtboundat + S (jt_value_rectsuccessornewcrtbound) = S ((S (jt_index_rectsuccessornewcrtbound)) * jt_g_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewcrtboundat. jt_f_rectsuccessornew = fs_q_jt_rectsuccessornewcrtboundat * S ((S (jt_index_rectsuccessornewcrtbound)) * jt_g_rectsuccessornew) + (jt_value_rectsuccessornewcrtbound))) /\ (exists jt_gap_rectsuccessornewcrtboundvalue. jt_gap_rectsuccessornewcrtboundvalue+S (jt_value_rectsuccessornewcrtbound)=(m*n)))) /\ (((forall jt_index_rectsuccessornewcrtleft jt_left_rectsuccessornewcrtleft jt_right_rectsuccessornewcrtleft. (exists jt_gap_rectsuccessornewcrtleftindex. jt_gap_rectsuccessornewcrtleftindex+S (jt_index_rectsuccessornewcrtleft)=(k)) -> (((exists fs_h_jt_rectsuccessornewcrtleftleft. fs_h_jt_rectsuccessornewcrtleftleft + S (jt_left_rectsuccessornewcrtleft) = S ((S (jt_index_rectsuccessornewcrtleft)) * jt_g_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewcrtleftleft. jt_f_rectsuccessornew = fs_q_jt_rectsuccessornewcrtleftleft * S ((S (jt_index_rectsuccessornewcrtleft)) * jt_g_rectsuccessornew) + (jt_left_rectsuccessornewcrtleft))) -> (((exists fs_h_jt_rectsuccessornewcrtleftright. fs_h_jt_rectsuccessornewcrtleftright + S (jt_right_rectsuccessornewcrtleft) = S ((S (jt_index_rectsuccessornewcrtleft)) * jt_c_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewcrtleftright. jt_b_rectsuccessornew = fs_q_jt_rectsuccessornewcrtleftright * S ((S (jt_index_rectsuccessornewcrtleft)) * jt_c_rectsuccessornew) + (jt_right_rectsuccessornewcrtleft))) -> (exists jt_left_rectsuccessornewcrtleftmod jt_right_rectsuccessornewcrtleftmod. (jt_left_rectsuccessornewcrtleft)+(m)*jt_left_rectsuccessornewcrtleftmod=(jt_right_rectsuccessornewcrtleft)+(m)*jt_right_rectsuccessornewcrtleftmod)) /\ (forall jt_index_rectsuccessornewcrtright jt_left_rectsuccessornewcrtright jt_right_rectsuccessornewcrtright. (exists jt_gap_rectsuccessornewcrtrightindex. jt_gap_rectsuccessornewcrtrightindex+S (jt_index_rectsuccessornewcrtright)=(k)) -> (((exists fs_h_jt_rectsuccessornewcrtrightleft. fs_h_jt_rectsuccessornewcrtrightleft + S (jt_left_rectsuccessornewcrtright) = S ((S (jt_index_rectsuccessornewcrtright)) * jt_g_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewcrtrightleft. jt_f_rectsuccessornew = fs_q_jt_rectsuccessornewcrtrightleft * S ((S (jt_index_rectsuccessornewcrtright)) * jt_g_rectsuccessornew) + (jt_left_rectsuccessornewcrtright))) -> (((exists fs_h_jt_rectsuccessornewcrtrightright. fs_h_jt_rectsuccessornewcrtrightright + S (jt_right_rectsuccessornewcrtright) = S ((S (jt_index_rectsuccessornewcrtright)) * jt_e_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewcrtrightright. jt_d_rectsuccessornew = fs_q_jt_rectsuccessornewcrtrightright * S ((S (jt_index_rectsuccessornewcrtright)) * jt_e_rectsuccessornew) + (jt_right_rectsuccessornewcrtright))) -> (exists jt_left_rectsuccessornewcrtrightmod jt_right_rectsuccessornewcrtrightmod. (jt_left_rectsuccessornewcrtright)+(n)*jt_left_rectsuccessornewcrtrightmod=(jt_right_rectsuccessornewcrtright)+(n)*jt_right_rectsuccessornewcrtrightmod)))))) /\ (forall jt_divisor_rectsuccessornewprimitive. (exists jt_factor_rectsuccessornewprimitivemodulus. (m*n)=(jt_divisor_rectsuccessornewprimitive)*jt_factor_rectsuccessornewprimitivemodulus) -> (forall jt_index_rectsuccessornewprimitivecoordinates jt_value_rectsuccessornewprimitivecoordinates. (exists jt_gap_rectsuccessornewprimitivecoordinatesindex. jt_gap_rectsuccessornewprimitivecoordinatesindex+S (jt_index_rectsuccessornewprimitivecoordinates)=(k)) -> (((exists fs_h_jt_rectsuccessornewprimitivecoordinatesat. fs_h_jt_rectsuccessornewprimitivecoordinatesat + S (jt_value_rectsuccessornewprimitivecoordinates) = S ((S (jt_index_rectsuccessornewprimitivecoordinates)) * jt_g_rectsuccessornew)) /\ exists fs_q_jt_rectsuccessornewprimitivecoordinatesat. jt_f_rectsuccessornew = fs_q_jt_rectsuccessornewprimitivecoordinatesat * S ((S (jt_index_rectsuccessornewprimitivecoordinates)) * jt_g_rectsuccessornew) + (jt_value_rectsuccessornewprimitivecoordinates))) -> (exists jt_factor_rectsuccessornewprimitivecoordinatesdivides. (jt_value_rectsuccessornewprimitivecoordinates)=(jt_divisor_rectsuccessornewprimitive)*jt_factor_rectsuccessornewprimitivecoordinatesdivides)) -> jt_divisor_rectsuccessornewprimitive=1))))))))))))))