jordan_tuple_scan_skip

Exact expanded first-order arithmetic statement

forall k n c t B C D E j. (((forall jt_i_skipsource. (exists jt_gap_skipsourcesoundindex. jt_gap_skipsourcesoundindex+S (jt_i_skipsource)=(j)) -> exists jt_b_skipsource jt_e_skipsource. ((((((exists fs_h_jt_skipsourcesoundcode. fs_h_jt_skipsourcesoundcode + S (jt_b_skipsource) = S ((S (jt_i_skipsource)) * C)) /\ exists fs_q_jt_skipsourcesoundcode. B = fs_q_jt_skipsourcesoundcode * S ((S (jt_i_skipsource)) * C) + (jt_b_skipsource))) /\ (((exists fs_h_jt_skipsourcesoundscale. fs_h_jt_skipsourcesoundscale + S (jt_e_skipsource) = S ((S (jt_i_skipsource)) * E)) /\ exists fs_q_jt_skipsourcesoundscale. D = fs_q_jt_skipsourcesoundscale * S ((S (jt_i_skipsource)) * E) + (jt_e_skipsource))))) /\ (((forall jt_index_skipsourcebound. (exists jt_gap_skipsourceboundindex. jt_gap_skipsourceboundindex+S (jt_index_skipsourcebound)=(k)) -> exists jt_value_skipsourcebound. ((((exists fs_h_jt_skipsourceboundat. fs_h_jt_skipsourceboundat + S (jt_value_skipsourcebound) = S ((S (jt_index_skipsourcebound)) * jt_e_skipsource)) /\ exists fs_q_jt_skipsourceboundat. jt_b_skipsource = fs_q_jt_skipsourceboundat * S ((S (jt_index_skipsourcebound)) * jt_e_skipsource) + (jt_value_skipsourcebound))) /\ (exists jt_gap_skipsourceboundvalue. jt_gap_skipsourceboundvalue+S (jt_value_skipsourcebound)=(n)))) /\ (forall jt_divisor_skipsourceprimitive. (exists jt_factor_skipsourceprimitivemodulus. (n)=(jt_divisor_skipsourceprimitive)*jt_factor_skipsourceprimitivemodulus) -> (forall jt_index_skipsourceprimitivecoordinates jt_value_skipsourceprimitivecoordinates. (exists jt_gap_skipsourceprimitivecoordinatesindex. jt_gap_skipsourceprimitivecoordinatesindex+S (jt_index_skipsourceprimitivecoordinates)=(k)) -> (((exists fs_h_jt_skipsourceprimitivecoordinatesat. fs_h_jt_skipsourceprimitivecoordinatesat + S (jt_value_skipsourceprimitivecoordinates) = S ((S (jt_index_skipsourceprimitivecoordinates)) * jt_e_skipsource)) /\ exists fs_q_jt_skipsourceprimitivecoordinatesat. jt_b_skipsource = fs_q_jt_skipsourceprimitivecoordinatesat * S ((S (jt_index_skipsourceprimitivecoordinates)) * jt_e_skipsource) + (jt_value_skipsourceprimitivecoordinates))) -> (exists jt_factor_skipsourceprimitivecoordinatesdivides. (jt_value_skipsourceprimitivecoordinates)=(jt_divisor_skipsourceprimitive)*jt_factor_skipsourceprimitivecoordinatesdivides)) -> jt_divisor_skipsourceprimitive=1))))) /\ (((forall jt_i_skipsource jt_h_skipsource jt_b_skipsource jt_e_skipsource jt_d_skipsource jt_f_skipsource. (exists jt_gap_skipsourcefirstindex. jt_gap_skipsourcefirstindex+S (jt_i_skipsource)=(j)) -> (exists jt_gap_skipsourcesecondindex. jt_gap_skipsourcesecondindex+S (jt_h_skipsource)=(j)) -> (((((exists fs_h_jt_skipsourcefirstcode. fs_h_jt_skipsourcefirstcode + S (jt_b_skipsource) = S ((S (jt_i_skipsource)) * C)) /\ exists fs_q_jt_skipsourcefirstcode. B = fs_q_jt_skipsourcefirstcode * S ((S (jt_i_skipsource)) * C) + (jt_b_skipsource))) /\ (((exists fs_h_jt_skipsourcefirstscale. fs_h_jt_skipsourcefirstscale + S (jt_e_skipsource) = S ((S (jt_i_skipsource)) * E)) /\ exists fs_q_jt_skipsourcefirstscale. D = fs_q_jt_skipsourcefirstscale * S ((S (jt_i_skipsource)) * E) + (jt_e_skipsource))))) -> (((((exists fs_h_jt_skipsourcesecondcode. fs_h_jt_skipsourcesecondcode + S (jt_d_skipsource) = S ((S (jt_h_skipsource)) * C)) /\ exists fs_q_jt_skipsourcesecondcode. B = fs_q_jt_skipsourcesecondcode * S ((S (jt_h_skipsource)) * C) + (jt_d_skipsource))) /\ (((exists fs_h_jt_skipsourcesecondscale. fs_h_jt_skipsourcesecondscale + S (jt_f_skipsource) = S ((S (jt_h_skipsource)) * E)) /\ exists fs_q_jt_skipsourcesecondscale. D = fs_q_jt_skipsourcesecondscale * S ((S (jt_h_skipsource)) * E) + (jt_f_skipsource))))) -> (forall jt_index_skipsourcesame jt_left_skipsourcesame jt_right_skipsourcesame. (exists jt_gap_skipsourcesameindex. jt_gap_skipsourcesameindex+S (jt_index_skipsourcesame)=(k)) -> (((exists fs_h_jt_skipsourcesameleft. fs_h_jt_skipsourcesameleft + S (jt_left_skipsourcesame) = S ((S (jt_index_skipsourcesame)) * jt_e_skipsource)) /\ exists fs_q_jt_skipsourcesameleft. jt_b_skipsource = fs_q_jt_skipsourcesameleft * S ((S (jt_index_skipsourcesame)) * jt_e_skipsource) + (jt_left_skipsourcesame))) -> (((exists fs_h_jt_skipsourcesameright. fs_h_jt_skipsourcesameright + S (jt_right_skipsourcesame) = S ((S (jt_index_skipsourcesame)) * jt_f_skipsource)) /\ exists fs_q_jt_skipsourcesameright. jt_d_skipsource = fs_q_jt_skipsourcesameright * S ((S (jt_index_skipsourcesame)) * jt_f_skipsource) + (jt_right_skipsourcesame))) -> jt_left_skipsourcesame=jt_right_skipsourcesame) -> jt_i_skipsource=jt_h_skipsource) /\ (forall jt_z_skipsource. (exists jt_gap_skipsourcecodeindex. jt_gap_skipsourcecodeindex+S (jt_z_skipsource)=(t)) -> (forall jt_index_skipsourceinputbound. (exists jt_gap_skipsourceinputboundindex. jt_gap_skipsourceinputboundindex+S (jt_index_skipsourceinputbound)=(k)) -> exists jt_value_skipsourceinputbound. ((((exists fs_h_jt_skipsourceinputboundat. fs_h_jt_skipsourceinputboundat + S (jt_value_skipsourceinputbound) = S ((S (jt_index_skipsourceinputbound)) * c)) /\ exists fs_q_jt_skipsourceinputboundat. jt_z_skipsource = fs_q_jt_skipsourceinputboundat * S ((S (jt_index_skipsourceinputbound)) * c) + (jt_value_skipsourceinputbound))) /\ (exists jt_gap_skipsourceinputboundvalue. jt_gap_skipsourceinputboundvalue+S (jt_value_skipsourceinputbound)=(n)))) -> (forall jt_divisor_skipsourceinputprimitive. (exists jt_factor_skipsourceinputprimitivemodulus. (n)=(jt_divisor_skipsourceinputprimitive)*jt_factor_skipsourceinputprimitivemodulus) -> (forall jt_index_skipsourceinputprimitivecoordinates jt_value_skipsourceinputprimitivecoordinates. (exists jt_gap_skipsourceinputprimitivecoordinatesindex. jt_gap_skipsourceinputprimitivecoordinatesindex+S (jt_index_skipsourceinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_skipsourceinputprimitivecoordinatesat. fs_h_jt_skipsourceinputprimitivecoordinatesat + S (jt_value_skipsourceinputprimitivecoordinates) = S ((S (jt_index_skipsourceinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_skipsourceinputprimitivecoordinatesat. jt_z_skipsource = fs_q_jt_skipsourceinputprimitivecoordinatesat * S ((S (jt_index_skipsourceinputprimitivecoordinates)) * c) + (jt_value_skipsourceinputprimitivecoordinates))) -> (exists jt_factor_skipsourceinputprimitivecoordinatesdivides. (jt_value_skipsourceinputprimitivecoordinates)=(jt_divisor_skipsourceinputprimitive)*jt_factor_skipsourceinputprimitivecoordinatesdivides)) -> jt_divisor_skipsourceinputprimitive=1) -> (exists jt_index_skipsourcelisted jt_code_skipsourcelisted jt_scale_skipsourcelisted. ((exists jt_gap_skipsourcelistedindex. jt_gap_skipsourcelistedindex+S (jt_index_skipsourcelisted)=(j)) /\ (((((((exists fs_h_jt_skipsourcelistedcode. fs_h_jt_skipsourcelistedcode + S (jt_code_skipsourcelisted) = S ((S (jt_index_skipsourcelisted)) * C)) /\ exists fs_q_jt_skipsourcelistedcode. B = fs_q_jt_skipsourcelistedcode * S ((S (jt_index_skipsourcelisted)) * C) + (jt_code_skipsourcelisted))) /\ (((exists fs_h_jt_skipsourcelistedscale. fs_h_jt_skipsourcelistedscale + S (jt_scale_skipsourcelisted) = S ((S (jt_index_skipsourcelisted)) * E)) /\ exists fs_q_jt_skipsourcelistedscale. D = fs_q_jt_skipsourcelistedscale * S ((S (jt_index_skipsourcelisted)) * E) + (jt_scale_skipsourcelisted))))) /\ (forall jt_index_skipsourcelistedequal jt_left_skipsourcelistedequal jt_right_skipsourcelistedequal. (exists jt_gap_skipsourcelistedequalindex. jt_gap_skipsourcelistedequalindex+S (jt_index_skipsourcelistedequal)=(k)) -> (((exists fs_h_jt_skipsourcelistedequalleft. fs_h_jt_skipsourcelistedequalleft + S (jt_left_skipsourcelistedequal) = S ((S (jt_index_skipsourcelistedequal)) * c)) /\ exists fs_q_jt_skipsourcelistedequalleft. jt_z_skipsource = fs_q_jt_skipsourcelistedequalleft * S ((S (jt_index_skipsourcelistedequal)) * c) + (jt_left_skipsourcelistedequal))) -> (((exists fs_h_jt_skipsourcelistedequalright. fs_h_jt_skipsourcelistedequalright + S (jt_right_skipsourcelistedequal) = S ((S (jt_index_skipsourcelistedequal)) * jt_scale_skipsourcelisted)) /\ exists fs_q_jt_skipsourcelistedequalright. jt_code_skipsourcelisted = fs_q_jt_skipsourcelistedequalright * S ((S (jt_index_skipsourcelistedequal)) * jt_scale_skipsourcelisted) + (jt_right_skipsourcelistedequal))) -> jt_left_skipsourcelistedequal=jt_right_skipsourcelistedequal)))))))))) -> ((forall jt_index_skipcurrentbound. (exists jt_gap_skipcurrentboundindex. jt_gap_skipcurrentboundindex+S (jt_index_skipcurrentbound)=(k)) -> exists jt_value_skipcurrentbound. ((((exists fs_h_jt_skipcurrentboundat. fs_h_jt_skipcurrentboundat + S (jt_value_skipcurrentbound) = S ((S (jt_index_skipcurrentbound)) * c)) /\ exists fs_q_jt_skipcurrentboundat. t = fs_q_jt_skipcurrentboundat * S ((S (jt_index_skipcurrentbound)) * c) + (jt_value_skipcurrentbound))) /\ (exists jt_gap_skipcurrentboundvalue. jt_gap_skipcurrentboundvalue+S (jt_value_skipcurrentbound)=(n)))) -> (forall jt_divisor_skipcurrentprimitive. (exists jt_factor_skipcurrentprimitivemodulus. (n)=(jt_divisor_skipcurrentprimitive)*jt_factor_skipcurrentprimitivemodulus) -> (forall jt_index_skipcurrentprimitivecoordinates jt_value_skipcurrentprimitivecoordinates. (exists jt_gap_skipcurrentprimitivecoordinatesindex. jt_gap_skipcurrentprimitivecoordinatesindex+S (jt_index_skipcurrentprimitivecoordinates)=(k)) -> (((exists fs_h_jt_skipcurrentprimitivecoordinatesat. fs_h_jt_skipcurrentprimitivecoordinatesat + S (jt_value_skipcurrentprimitivecoordinates) = S ((S (jt_index_skipcurrentprimitivecoordinates)) * c)) /\ exists fs_q_jt_skipcurrentprimitivecoordinatesat. t = fs_q_jt_skipcurrentprimitivecoordinatesat * S ((S (jt_index_skipcurrentprimitivecoordinates)) * c) + (jt_value_skipcurrentprimitivecoordinates))) -> (exists jt_factor_skipcurrentprimitivecoordinatesdivides. (jt_value_skipcurrentprimitivecoordinates)=(jt_divisor_skipcurrentprimitive)*jt_factor_skipcurrentprimitivecoordinatesdivides)) -> jt_divisor_skipcurrentprimitive=1) -> (exists jt_index_skipcurrentlisted jt_code_skipcurrentlisted jt_scale_skipcurrentlisted. ((exists jt_gap_skipcurrentlistedindex. jt_gap_skipcurrentlistedindex+S (jt_index_skipcurrentlisted)=(j)) /\ (((((((exists fs_h_jt_skipcurrentlistedcode. fs_h_jt_skipcurrentlistedcode + S (jt_code_skipcurrentlisted) = S ((S (jt_index_skipcurrentlisted)) * C)) /\ exists fs_q_jt_skipcurrentlistedcode. B = fs_q_jt_skipcurrentlistedcode * S ((S (jt_index_skipcurrentlisted)) * C) + (jt_code_skipcurrentlisted))) /\ (((exists fs_h_jt_skipcurrentlistedscale. fs_h_jt_skipcurrentlistedscale + S (jt_scale_skipcurrentlisted) = S ((S (jt_index_skipcurrentlisted)) * E)) /\ exists fs_q_jt_skipcurrentlistedscale. D = fs_q_jt_skipcurrentlistedscale * S ((S (jt_index_skipcurrentlisted)) * E) + (jt_scale_skipcurrentlisted))))) /\ (forall jt_index_skipcurrentlistedequal jt_left_skipcurrentlistedequal jt_right_skipcurrentlistedequal. (exists jt_gap_skipcurrentlistedequalindex. jt_gap_skipcurrentlistedequalindex+S (jt_index_skipcurrentlistedequal)=(k)) -> (((exists fs_h_jt_skipcurrentlistedequalleft. fs_h_jt_skipcurrentlistedequalleft + S (jt_left_skipcurrentlistedequal) = S ((S (jt_index_skipcurrentlistedequal)) * c)) /\ exists fs_q_jt_skipcurrentlistedequalleft. t = fs_q_jt_skipcurrentlistedequalleft * S ((S (jt_index_skipcurrentlistedequal)) * c) + (jt_left_skipcurrentlistedequal))) -> (((exists fs_h_jt_skipcurrentlistedequalright. fs_h_jt_skipcurrentlistedequalright + S (jt_right_skipcurrentlistedequal) = S ((S (jt_index_skipcurrentlistedequal)) * jt_scale_skipcurrentlisted)) /\ exists fs_q_jt_skipcurrentlistedequalright. jt_code_skipcurrentlisted = fs_q_jt_skipcurrentlistedequalright * S ((S (jt_index_skipcurrentlistedequal)) * jt_scale_skipcurrentlisted) + (jt_right_skipcurrentlistedequal))) -> jt_left_skipcurrentlistedequal=jt_right_skipcurrentlistedequal)))))) -> (((forall jt_i_skiptarget. (exists jt_gap_skiptargetsoundindex. jt_gap_skiptargetsoundindex+S (jt_i_skiptarget)=(j)) -> exists jt_b_skiptarget jt_e_skiptarget. ((((((exists fs_h_jt_skiptargetsoundcode. fs_h_jt_skiptargetsoundcode + S (jt_b_skiptarget) = S ((S (jt_i_skiptarget)) * C)) /\ exists fs_q_jt_skiptargetsoundcode. B = fs_q_jt_skiptargetsoundcode * S ((S (jt_i_skiptarget)) * C) + (jt_b_skiptarget))) /\ (((exists fs_h_jt_skiptargetsoundscale. fs_h_jt_skiptargetsoundscale + S (jt_e_skiptarget) = S ((S (jt_i_skiptarget)) * E)) /\ exists fs_q_jt_skiptargetsoundscale. D = fs_q_jt_skiptargetsoundscale * S ((S (jt_i_skiptarget)) * E) + (jt_e_skiptarget))))) /\ (((forall jt_index_skiptargetbound. (exists jt_gap_skiptargetboundindex. jt_gap_skiptargetboundindex+S (jt_index_skiptargetbound)=(k)) -> exists jt_value_skiptargetbound. ((((exists fs_h_jt_skiptargetboundat. fs_h_jt_skiptargetboundat + S (jt_value_skiptargetbound) = S ((S (jt_index_skiptargetbound)) * jt_e_skiptarget)) /\ exists fs_q_jt_skiptargetboundat. jt_b_skiptarget = fs_q_jt_skiptargetboundat * S ((S (jt_index_skiptargetbound)) * jt_e_skiptarget) + (jt_value_skiptargetbound))) /\ (exists jt_gap_skiptargetboundvalue. jt_gap_skiptargetboundvalue+S (jt_value_skiptargetbound)=(n)))) /\ (forall jt_divisor_skiptargetprimitive. (exists jt_factor_skiptargetprimitivemodulus. (n)=(jt_divisor_skiptargetprimitive)*jt_factor_skiptargetprimitivemodulus) -> (forall jt_index_skiptargetprimitivecoordinates jt_value_skiptargetprimitivecoordinates. (exists jt_gap_skiptargetprimitivecoordinatesindex. jt_gap_skiptargetprimitivecoordinatesindex+S (jt_index_skiptargetprimitivecoordinates)=(k)) -> (((exists fs_h_jt_skiptargetprimitivecoordinatesat. fs_h_jt_skiptargetprimitivecoordinatesat + S (jt_value_skiptargetprimitivecoordinates) = S ((S (jt_index_skiptargetprimitivecoordinates)) * jt_e_skiptarget)) /\ exists fs_q_jt_skiptargetprimitivecoordinatesat. jt_b_skiptarget = fs_q_jt_skiptargetprimitivecoordinatesat * S ((S (jt_index_skiptargetprimitivecoordinates)) * jt_e_skiptarget) + (jt_value_skiptargetprimitivecoordinates))) -> (exists jt_factor_skiptargetprimitivecoordinatesdivides. (jt_value_skiptargetprimitivecoordinates)=(jt_divisor_skiptargetprimitive)*jt_factor_skiptargetprimitivecoordinatesdivides)) -> jt_divisor_skiptargetprimitive=1))))) /\ (((forall jt_i_skiptarget jt_h_skiptarget jt_b_skiptarget jt_e_skiptarget jt_d_skiptarget jt_f_skiptarget. (exists jt_gap_skiptargetfirstindex. jt_gap_skiptargetfirstindex+S (jt_i_skiptarget)=(j)) -> (exists jt_gap_skiptargetsecondindex. jt_gap_skiptargetsecondindex+S (jt_h_skiptarget)=(j)) -> (((((exists fs_h_jt_skiptargetfirstcode. fs_h_jt_skiptargetfirstcode + S (jt_b_skiptarget) = S ((S (jt_i_skiptarget)) * C)) /\ exists fs_q_jt_skiptargetfirstcode. B = fs_q_jt_skiptargetfirstcode * S ((S (jt_i_skiptarget)) * C) + (jt_b_skiptarget))) /\ (((exists fs_h_jt_skiptargetfirstscale. fs_h_jt_skiptargetfirstscale + S (jt_e_skiptarget) = S ((S (jt_i_skiptarget)) * E)) /\ exists fs_q_jt_skiptargetfirstscale. D = fs_q_jt_skiptargetfirstscale * S ((S (jt_i_skiptarget)) * E) + (jt_e_skiptarget))))) -> (((((exists fs_h_jt_skiptargetsecondcode. fs_h_jt_skiptargetsecondcode + S (jt_d_skiptarget) = S ((S (jt_h_skiptarget)) * C)) /\ exists fs_q_jt_skiptargetsecondcode. B = fs_q_jt_skiptargetsecondcode * S ((S (jt_h_skiptarget)) * C) + (jt_d_skiptarget))) /\ (((exists fs_h_jt_skiptargetsecondscale. fs_h_jt_skiptargetsecondscale + S (jt_f_skiptarget) = S ((S (jt_h_skiptarget)) * E)) /\ exists fs_q_jt_skiptargetsecondscale. D = fs_q_jt_skiptargetsecondscale * S ((S (jt_h_skiptarget)) * E) + (jt_f_skiptarget))))) -> (forall jt_index_skiptargetsame jt_left_skiptargetsame jt_right_skiptargetsame. (exists jt_gap_skiptargetsameindex. jt_gap_skiptargetsameindex+S (jt_index_skiptargetsame)=(k)) -> (((exists fs_h_jt_skiptargetsameleft. fs_h_jt_skiptargetsameleft + S (jt_left_skiptargetsame) = S ((S (jt_index_skiptargetsame)) * jt_e_skiptarget)) /\ exists fs_q_jt_skiptargetsameleft. jt_b_skiptarget = fs_q_jt_skiptargetsameleft * S ((S (jt_index_skiptargetsame)) * jt_e_skiptarget) + (jt_left_skiptargetsame))) -> (((exists fs_h_jt_skiptargetsameright. fs_h_jt_skiptargetsameright + S (jt_right_skiptargetsame) = S ((S (jt_index_skiptargetsame)) * jt_f_skiptarget)) /\ exists fs_q_jt_skiptargetsameright. jt_d_skiptarget = fs_q_jt_skiptargetsameright * S ((S (jt_index_skiptargetsame)) * jt_f_skiptarget) + (jt_right_skiptargetsame))) -> jt_left_skiptargetsame=jt_right_skiptargetsame) -> jt_i_skiptarget=jt_h_skiptarget) /\ (forall jt_z_skiptarget. (exists jt_gap_skiptargetcodeindex. jt_gap_skiptargetcodeindex+S (jt_z_skiptarget)=(S t)) -> (forall jt_index_skiptargetinputbound. (exists jt_gap_skiptargetinputboundindex. jt_gap_skiptargetinputboundindex+S (jt_index_skiptargetinputbound)=(k)) -> exists jt_value_skiptargetinputbound. ((((exists fs_h_jt_skiptargetinputboundat. fs_h_jt_skiptargetinputboundat + S (jt_value_skiptargetinputbound) = S ((S (jt_index_skiptargetinputbound)) * c)) /\ exists fs_q_jt_skiptargetinputboundat. jt_z_skiptarget = fs_q_jt_skiptargetinputboundat * S ((S (jt_index_skiptargetinputbound)) * c) + (jt_value_skiptargetinputbound))) /\ (exists jt_gap_skiptargetinputboundvalue. jt_gap_skiptargetinputboundvalue+S (jt_value_skiptargetinputbound)=(n)))) -> (forall jt_divisor_skiptargetinputprimitive. (exists jt_factor_skiptargetinputprimitivemodulus. (n)=(jt_divisor_skiptargetinputprimitive)*jt_factor_skiptargetinputprimitivemodulus) -> (forall jt_index_skiptargetinputprimitivecoordinates jt_value_skiptargetinputprimitivecoordinates. (exists jt_gap_skiptargetinputprimitivecoordinatesindex. jt_gap_skiptargetinputprimitivecoordinatesindex+S (jt_index_skiptargetinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_skiptargetinputprimitivecoordinatesat. fs_h_jt_skiptargetinputprimitivecoordinatesat + S (jt_value_skiptargetinputprimitivecoordinates) = S ((S (jt_index_skiptargetinputprimitivecoordinates)) * c)) /\ exists fs_q_jt_skiptargetinputprimitivecoordinatesat. jt_z_skiptarget = fs_q_jt_skiptargetinputprimitivecoordinatesat * S ((S (jt_index_skiptargetinputprimitivecoordinates)) * c) + (jt_value_skiptargetinputprimitivecoordinates))) -> (exists jt_factor_skiptargetinputprimitivecoordinatesdivides. (jt_value_skiptargetinputprimitivecoordinates)=(jt_divisor_skiptargetinputprimitive)*jt_factor_skiptargetinputprimitivecoordinatesdivides)) -> jt_divisor_skiptargetinputprimitive=1) -> (exists jt_index_skiptargetlisted jt_code_skiptargetlisted jt_scale_skiptargetlisted. ((exists jt_gap_skiptargetlistedindex. jt_gap_skiptargetlistedindex+S (jt_index_skiptargetlisted)=(j)) /\ (((((((exists fs_h_jt_skiptargetlistedcode. fs_h_jt_skiptargetlistedcode + S (jt_code_skiptargetlisted) = S ((S (jt_index_skiptargetlisted)) * C)) /\ exists fs_q_jt_skiptargetlistedcode. B = fs_q_jt_skiptargetlistedcode * S ((S (jt_index_skiptargetlisted)) * C) + (jt_code_skiptargetlisted))) /\ (((exists fs_h_jt_skiptargetlistedscale. fs_h_jt_skiptargetlistedscale + S (jt_scale_skiptargetlisted) = S ((S (jt_index_skiptargetlisted)) * E)) /\ exists fs_q_jt_skiptargetlistedscale. D = fs_q_jt_skiptargetlistedscale * S ((S (jt_index_skiptargetlisted)) * E) + (jt_scale_skiptargetlisted))))) /\ (forall jt_index_skiptargetlistedequal jt_left_skiptargetlistedequal jt_right_skiptargetlistedequal. (exists jt_gap_skiptargetlistedequalindex. jt_gap_skiptargetlistedequalindex+S (jt_index_skiptargetlistedequal)=(k)) -> (((exists fs_h_jt_skiptargetlistedequalleft. fs_h_jt_skiptargetlistedequalleft + S (jt_left_skiptargetlistedequal) = S ((S (jt_index_skiptargetlistedequal)) * c)) /\ exists fs_q_jt_skiptargetlistedequalleft. jt_z_skiptarget = fs_q_jt_skiptargetlistedequalleft * S ((S (jt_index_skiptargetlistedequal)) * c) + (jt_left_skiptargetlistedequal))) -> (((exists fs_h_jt_skiptargetlistedequalright. fs_h_jt_skiptargetlistedequalright + S (jt_right_skiptargetlistedequal) = S ((S (jt_index_skiptargetlistedequal)) * jt_scale_skiptargetlisted)) /\ exists fs_q_jt_skiptargetlistedequalright. jt_code_skiptargetlisted = fs_q_jt_skiptargetlistedequalright * S ((S (jt_index_skiptargetlistedequal)) * jt_scale_skiptargetlisted) + (jt_right_skiptargetlistedequal))) -> jt_left_skiptargetlistedequal=jt_right_skiptargetlistedequal))))))))))