jordan_enumeration_position_match_exists

forall k n A B C D u E F G H v i. (((forall jt_i_source_enum. (exists jt_gap_source_enumsoundindex. jt_gap_source_enumsoundindex+S (jt_i_source_enum)=(u)) -> exists jt_b_source_enum jt_c_source_enum. ((((((exists fs_h_jt_source_enumsoundcode. fs_h_jt_source_enumsoundcode + S (jt_b_source_enum) = S ((S (jt_i_source_enum)) * B)) /\ exists fs_q_jt_source_enumsoundcode. A = fs_q_jt_source_enumsoundcode * S ((S (jt_i_source_enum)) * B) + (jt_b_source_enum))) /\ (((exists fs_h_jt_source_enumsoundscale. fs_h_jt_source_enumsoundscale + S (jt_c_source_enum) = S ((S (jt_i_source_enum)) * D)) /\ exists fs_q_jt_source_enumsoundscale. C = fs_q_jt_source_enumsoundscale * S ((S (jt_i_source_enum)) * D) + (jt_c_source_enum))))) /\ (((forall jt_index_source_enumbound. (exists jt_gap_source_enumboundindex. jt_gap_source_enumboundindex+S (jt_index_source_enumbound)=(k)) -> exists jt_value_source_enumbound. ((((exists fs_h_jt_source_enumboundat. fs_h_jt_source_enumboundat + S (jt_value_source_enumbound) = S ((S (jt_index_source_enumbound)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enumboundat. jt_b_source_enum = fs_q_jt_source_enumboundat * S ((S (jt_index_source_enumbound)) * jt_c_source_enum) + (jt_value_source_enumbound))) /\ (exists jt_gap_source_enumboundvalue. jt_gap_source_enumboundvalue+S (jt_value_source_enumbound)=(n)))) /\ (forall jt_divisor_source_enumprimitive. (exists jt_factor_source_enumprimitivemodulus. (n)=(jt_divisor_source_enumprimitive)*jt_factor_source_enumprimitivemodulus) -> (forall jt_index_source_enumprimitivecoordinates jt_value_source_enumprimitivecoordinates. (exists jt_gap_source_enumprimitivecoordinatesindex. jt_gap_source_enumprimitivecoordinatesindex+S (jt_index_source_enumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_source_enumprimitivecoordinatesat. fs_h_jt_source_enumprimitivecoordinatesat + S (jt_value_source_enumprimitivecoordinates) = S ((S (jt_index_source_enumprimitivecoordinates)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enumprimitivecoordinatesat. jt_b_source_enum = fs_q_jt_source_enumprimitivecoordinatesat * S ((S (jt_index_source_enumprimitivecoordinates)) * jt_c_source_enum) + (jt_value_source_enumprimitivecoordinates))) -> (exists jt_factor_source_enumprimitivecoordinatesdivides. (jt_value_source_enumprimitivecoordinates)=(jt_divisor_source_enumprimitive)*jt_factor_source_enumprimitivecoordinatesdivides)) -> jt_divisor_source_enumprimitive=1))))) /\ (((forall jt_b_source_enum jt_c_source_enum. (forall jt_index_source_enuminputbound. (exists jt_gap_source_enuminputboundindex. jt_gap_source_enuminputboundindex+S (jt_index_source_enuminputbound)=(k)) -> exists jt_value_source_enuminputbound. ((((exists fs_h_jt_source_enuminputboundat. fs_h_jt_source_enuminputboundat + S (jt_value_source_enuminputbound) = S ((S (jt_index_source_enuminputbound)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enuminputboundat. jt_b_source_enum = fs_q_jt_source_enuminputboundat * S ((S (jt_index_source_enuminputbound)) * jt_c_source_enum) + (jt_value_source_enuminputbound))) /\ (exists jt_gap_source_enuminputboundvalue. jt_gap_source_enuminputboundvalue+S (jt_value_source_enuminputbound)=(n)))) -> (forall jt_divisor_source_enuminputprimitive. (exists jt_factor_source_enuminputprimitivemodulus. (n)=(jt_divisor_source_enuminputprimitive)*jt_factor_source_enuminputprimitivemodulus) -> (forall jt_index_source_enuminputprimitivecoordinates jt_value_source_enuminputprimitivecoordinates. (exists jt_gap_source_enuminputprimitivecoordinatesindex. jt_gap_source_enuminputprimitivecoordinatesindex+S (jt_index_source_enuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_source_enuminputprimitivecoordinatesat. fs_h_jt_source_enuminputprimitivecoordinatesat + S (jt_value_source_enuminputprimitivecoordinates) = S ((S (jt_index_source_enuminputprimitivecoordinates)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enuminputprimitivecoordinatesat. jt_b_source_enum = fs_q_jt_source_enuminputprimitivecoordinatesat * S ((S (jt_index_source_enuminputprimitivecoordinates)) * jt_c_source_enum) + (jt_value_source_enuminputprimitivecoordinates))) -> (exists jt_factor_source_enuminputprimitivecoordinatesdivides. (jt_value_source_enuminputprimitivecoordinates)=(jt_divisor_source_enuminputprimitive)*jt_factor_source_enuminputprimitivecoordinatesdivides)) -> jt_divisor_source_enuminputprimitive=1) -> exists jt_i_source_enum jt_d_source_enum jt_e_source_enum. ((exists jt_gap_source_enumcompleteindex. jt_gap_source_enumcompleteindex+S (jt_i_source_enum)=(u)) /\ (((((((exists fs_h_jt_source_enumcompletecode. fs_h_jt_source_enumcompletecode + S (jt_d_source_enum) = S ((S (jt_i_source_enum)) * B)) /\ exists fs_q_jt_source_enumcompletecode. A = fs_q_jt_source_enumcompletecode * S ((S (jt_i_source_enum)) * B) + (jt_d_source_enum))) /\ (((exists fs_h_jt_source_enumcompletescale. fs_h_jt_source_enumcompletescale + S (jt_e_source_enum) = S ((S (jt_i_source_enum)) * D)) /\ exists fs_q_jt_source_enumcompletescale. C = fs_q_jt_source_enumcompletescale * S ((S (jt_i_source_enum)) * D) + (jt_e_source_enum))))) /\ (forall jt_index_source_enumrepresented jt_left_source_enumrepresented jt_right_source_enumrepresented. (exists jt_gap_source_enumrepresentedindex. jt_gap_source_enumrepresentedindex+S (jt_index_source_enumrepresented)=(k)) -> (((exists fs_h_jt_source_enumrepresentedleft. fs_h_jt_source_enumrepresentedleft + S (jt_left_source_enumrepresented) = S ((S (jt_index_source_enumrepresented)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enumrepresentedleft. jt_b_source_enum = fs_q_jt_source_enumrepresentedleft * S ((S (jt_index_source_enumrepresented)) * jt_c_source_enum) + (jt_left_source_enumrepresented))) -> (((exists fs_h_jt_source_enumrepresentedright. fs_h_jt_source_enumrepresentedright + S (jt_right_source_enumrepresented) = S ((S (jt_index_source_enumrepresented)) * jt_e_source_enum)) /\ exists fs_q_jt_source_enumrepresentedright. jt_d_source_enum = fs_q_jt_source_enumrepresentedright * S ((S (jt_index_source_enumrepresented)) * jt_e_source_enum) + (jt_right_source_enumrepresented))) -> jt_left_source_enumrepresented=jt_right_source_enumrepresented))))) /\ (forall jt_i_source_enum jt_h_source_enum jt_b_source_enum jt_c_source_enum jt_d_source_enum jt_e_source_enum. (exists jt_gap_source_enumfirstindex. jt_gap_source_enumfirstindex+S (jt_i_source_enum)=(u)) -> (exists jt_gap_source_enumsecondindex. jt_gap_source_enumsecondindex+S (jt_h_source_enum)=(u)) -> (((((exists fs_h_jt_source_enumfirstcode. fs_h_jt_source_enumfirstcode + S (jt_b_source_enum) = S ((S (jt_i_source_enum)) * B)) /\ exists fs_q_jt_source_enumfirstcode. A = fs_q_jt_source_enumfirstcode * S ((S (jt_i_source_enum)) * B) + (jt_b_source_enum))) /\ (((exists fs_h_jt_source_enumfirstscale. fs_h_jt_source_enumfirstscale + S (jt_c_source_enum) = S ((S (jt_i_source_enum)) * D)) /\ exists fs_q_jt_source_enumfirstscale. C = fs_q_jt_source_enumfirstscale * S ((S (jt_i_source_enum)) * D) + (jt_c_source_enum))))) -> (((((exists fs_h_jt_source_enumsecondcode. fs_h_jt_source_enumsecondcode + S (jt_d_source_enum) = S ((S (jt_h_source_enum)) * B)) /\ exists fs_q_jt_source_enumsecondcode. A = fs_q_jt_source_enumsecondcode * S ((S (jt_h_source_enum)) * B) + (jt_d_source_enum))) /\ (((exists fs_h_jt_source_enumsecondscale. fs_h_jt_source_enumsecondscale + S (jt_e_source_enum) = S ((S (jt_h_source_enum)) * D)) /\ exists fs_q_jt_source_enumsecondscale. C = fs_q_jt_source_enumsecondscale * S ((S (jt_h_source_enum)) * D) + (jt_e_source_enum))))) -> (forall jt_index_source_enumsame jt_left_source_enumsame jt_right_source_enumsame. (exists jt_gap_source_enumsameindex. jt_gap_source_enumsameindex+S (jt_index_source_enumsame)=(k)) -> (((exists fs_h_jt_source_enumsameleft. fs_h_jt_source_enumsameleft + S (jt_left_source_enumsame) = S ((S (jt_index_source_enumsame)) * jt_c_source_enum)) /\ exists fs_q_jt_source_enumsameleft. jt_b_source_enum = fs_q_jt_source_enumsameleft * S ((S (jt_index_source_enumsame)) * jt_c_source_enum) + (jt_left_source_enumsame))) -> (((exists fs_h_jt_source_enumsameright. fs_h_jt_source_enumsameright + S (jt_right_source_enumsame) = S ((S (jt_index_source_enumsame)) * jt_e_source_enum)) /\ exists fs_q_jt_source_enumsameright. jt_d_source_enum = fs_q_jt_source_enumsameright * S ((S (jt_index_source_enumsame)) * jt_e_source_enum) + (jt_right_source_enumsame))) -> jt_left_source_enumsame=jt_right_source_enumsame) -> jt_i_source_enum=jt_h_source_enum))))) -> (((forall jt_i_target_enum. (exists jt_gap_target_enumsoundindex. jt_gap_target_enumsoundindex+S (jt_i_target_enum)=(v)) -> exists jt_b_target_enum jt_c_target_enum. ((((((exists fs_h_jt_target_enumsoundcode. fs_h_jt_target_enumsoundcode + S (jt_b_target_enum) = S ((S (jt_i_target_enum)) * F)) /\ exists fs_q_jt_target_enumsoundcode. E = fs_q_jt_target_enumsoundcode * S ((S (jt_i_target_enum)) * F) + (jt_b_target_enum))) /\ (((exists fs_h_jt_target_enumsoundscale. fs_h_jt_target_enumsoundscale + S (jt_c_target_enum) = S ((S (jt_i_target_enum)) * H)) /\ exists fs_q_jt_target_enumsoundscale. G = fs_q_jt_target_enumsoundscale * S ((S (jt_i_target_enum)) * H) + (jt_c_target_enum))))) /\ (((forall jt_index_target_enumbound. (exists jt_gap_target_enumboundindex. jt_gap_target_enumboundindex+S (jt_index_target_enumbound)=(k)) -> exists jt_value_target_enumbound. ((((exists fs_h_jt_target_enumboundat. fs_h_jt_target_enumboundat + S (jt_value_target_enumbound) = S ((S (jt_index_target_enumbound)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enumboundat. jt_b_target_enum = fs_q_jt_target_enumboundat * S ((S (jt_index_target_enumbound)) * jt_c_target_enum) + (jt_value_target_enumbound))) /\ (exists jt_gap_target_enumboundvalue. jt_gap_target_enumboundvalue+S (jt_value_target_enumbound)=(n)))) /\ (forall jt_divisor_target_enumprimitive. (exists jt_factor_target_enumprimitivemodulus. (n)=(jt_divisor_target_enumprimitive)*jt_factor_target_enumprimitivemodulus) -> (forall jt_index_target_enumprimitivecoordinates jt_value_target_enumprimitivecoordinates. (exists jt_gap_target_enumprimitivecoordinatesindex. jt_gap_target_enumprimitivecoordinatesindex+S (jt_index_target_enumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_target_enumprimitivecoordinatesat. fs_h_jt_target_enumprimitivecoordinatesat + S (jt_value_target_enumprimitivecoordinates) = S ((S (jt_index_target_enumprimitivecoordinates)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enumprimitivecoordinatesat. jt_b_target_enum = fs_q_jt_target_enumprimitivecoordinatesat * S ((S (jt_index_target_enumprimitivecoordinates)) * jt_c_target_enum) + (jt_value_target_enumprimitivecoordinates))) -> (exists jt_factor_target_enumprimitivecoordinatesdivides. (jt_value_target_enumprimitivecoordinates)=(jt_divisor_target_enumprimitive)*jt_factor_target_enumprimitivecoordinatesdivides)) -> jt_divisor_target_enumprimitive=1))))) /\ (((forall jt_b_target_enum jt_c_target_enum. (forall jt_index_target_enuminputbound. (exists jt_gap_target_enuminputboundindex. jt_gap_target_enuminputboundindex+S (jt_index_target_enuminputbound)=(k)) -> exists jt_value_target_enuminputbound. ((((exists fs_h_jt_target_enuminputboundat. fs_h_jt_target_enuminputboundat + S (jt_value_target_enuminputbound) = S ((S (jt_index_target_enuminputbound)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enuminputboundat. jt_b_target_enum = fs_q_jt_target_enuminputboundat * S ((S (jt_index_target_enuminputbound)) * jt_c_target_enum) + (jt_value_target_enuminputbound))) /\ (exists jt_gap_target_enuminputboundvalue. jt_gap_target_enuminputboundvalue+S (jt_value_target_enuminputbound)=(n)))) -> (forall jt_divisor_target_enuminputprimitive. (exists jt_factor_target_enuminputprimitivemodulus. (n)=(jt_divisor_target_enuminputprimitive)*jt_factor_target_enuminputprimitivemodulus) -> (forall jt_index_target_enuminputprimitivecoordinates jt_value_target_enuminputprimitivecoordinates. (exists jt_gap_target_enuminputprimitivecoordinatesindex. jt_gap_target_enuminputprimitivecoordinatesindex+S (jt_index_target_enuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_target_enuminputprimitivecoordinatesat. fs_h_jt_target_enuminputprimitivecoordinatesat + S (jt_value_target_enuminputprimitivecoordinates) = S ((S (jt_index_target_enuminputprimitivecoordinates)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enuminputprimitivecoordinatesat. jt_b_target_enum = fs_q_jt_target_enuminputprimitivecoordinatesat * S ((S (jt_index_target_enuminputprimitivecoordinates)) * jt_c_target_enum) + (jt_value_target_enuminputprimitivecoordinates))) -> (exists jt_factor_target_enuminputprimitivecoordinatesdivides. (jt_value_target_enuminputprimitivecoordinates)=(jt_divisor_target_enuminputprimitive)*jt_factor_target_enuminputprimitivecoordinatesdivides)) -> jt_divisor_target_enuminputprimitive=1) -> exists jt_i_target_enum jt_d_target_enum jt_e_target_enum. ((exists jt_gap_target_enumcompleteindex. jt_gap_target_enumcompleteindex+S (jt_i_target_enum)=(v)) /\ (((((((exists fs_h_jt_target_enumcompletecode. fs_h_jt_target_enumcompletecode + S (jt_d_target_enum) = S ((S (jt_i_target_enum)) * F)) /\ exists fs_q_jt_target_enumcompletecode. E = fs_q_jt_target_enumcompletecode * S ((S (jt_i_target_enum)) * F) + (jt_d_target_enum))) /\ (((exists fs_h_jt_target_enumcompletescale. fs_h_jt_target_enumcompletescale + S (jt_e_target_enum) = S ((S (jt_i_target_enum)) * H)) /\ exists fs_q_jt_target_enumcompletescale. G = fs_q_jt_target_enumcompletescale * S ((S (jt_i_target_enum)) * H) + (jt_e_target_enum))))) /\ (forall jt_index_target_enumrepresented jt_left_target_enumrepresented jt_right_target_enumrepresented. (exists jt_gap_target_enumrepresentedindex. jt_gap_target_enumrepresentedindex+S (jt_index_target_enumrepresented)=(k)) -> (((exists fs_h_jt_target_enumrepresentedleft. fs_h_jt_target_enumrepresentedleft + S (jt_left_target_enumrepresented) = S ((S (jt_index_target_enumrepresented)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enumrepresentedleft. jt_b_target_enum = fs_q_jt_target_enumrepresentedleft * S ((S (jt_index_target_enumrepresented)) * jt_c_target_enum) + (jt_left_target_enumrepresented))) -> (((exists fs_h_jt_target_enumrepresentedright. fs_h_jt_target_enumrepresentedright + S (jt_right_target_enumrepresented) = S ((S (jt_index_target_enumrepresented)) * jt_e_target_enum)) /\ exists fs_q_jt_target_enumrepresentedright. jt_d_target_enum = fs_q_jt_target_enumrepresentedright * S ((S (jt_index_target_enumrepresented)) * jt_e_target_enum) + (jt_right_target_enumrepresented))) -> jt_left_target_enumrepresented=jt_right_target_enumrepresented))))) /\ (forall jt_i_target_enum jt_h_target_enum jt_b_target_enum jt_c_target_enum jt_d_target_enum jt_e_target_enum. (exists jt_gap_target_enumfirstindex. jt_gap_target_enumfirstindex+S (jt_i_target_enum)=(v)) -> (exists jt_gap_target_enumsecondindex. jt_gap_target_enumsecondindex+S (jt_h_target_enum)=(v)) -> (((((exists fs_h_jt_target_enumfirstcode. fs_h_jt_target_enumfirstcode + S (jt_b_target_enum) = S ((S (jt_i_target_enum)) * F)) /\ exists fs_q_jt_target_enumfirstcode. E = fs_q_jt_target_enumfirstcode * S ((S (jt_i_target_enum)) * F) + (jt_b_target_enum))) /\ (((exists fs_h_jt_target_enumfirstscale. fs_h_jt_target_enumfirstscale + S (jt_c_target_enum) = S ((S (jt_i_target_enum)) * H)) /\ exists fs_q_jt_target_enumfirstscale. G = fs_q_jt_target_enumfirstscale * S ((S (jt_i_target_enum)) * H) + (jt_c_target_enum))))) -> (((((exists fs_h_jt_target_enumsecondcode. fs_h_jt_target_enumsecondcode + S (jt_d_target_enum) = S ((S (jt_h_target_enum)) * F)) /\ exists fs_q_jt_target_enumsecondcode. E = fs_q_jt_target_enumsecondcode * S ((S (jt_h_target_enum)) * F) + (jt_d_target_enum))) /\ (((exists fs_h_jt_target_enumsecondscale. fs_h_jt_target_enumsecondscale + S (jt_e_target_enum) = S ((S (jt_h_target_enum)) * H)) /\ exists fs_q_jt_target_enumsecondscale. G = fs_q_jt_target_enumsecondscale * S ((S (jt_h_target_enum)) * H) + (jt_e_target_enum))))) -> (forall jt_index_target_enumsame jt_left_target_enumsame jt_right_target_enumsame. (exists jt_gap_target_enumsameindex. jt_gap_target_enumsameindex+S (jt_index_target_enumsame)=(k)) -> (((exists fs_h_jt_target_enumsameleft. fs_h_jt_target_enumsameleft + S (jt_left_target_enumsame) = S ((S (jt_index_target_enumsame)) * jt_c_target_enum)) /\ exists fs_q_jt_target_enumsameleft. jt_b_target_enum = fs_q_jt_target_enumsameleft * S ((S (jt_index_target_enumsame)) * jt_c_target_enum) + (jt_left_target_enumsame))) -> (((exists fs_h_jt_target_enumsameright. fs_h_jt_target_enumsameright + S (jt_right_target_enumsame) = S ((S (jt_index_target_enumsame)) * jt_e_target_enum)) /\ exists fs_q_jt_target_enumsameright. jt_d_target_enum = fs_q_jt_target_enumsameright * S ((S (jt_index_target_enumsame)) * jt_e_target_enum) + (jt_right_target_enumsame))) -> jt_left_target_enumsame=jt_right_target_enumsame) -> jt_i_target_enum=jt_h_target_enum))))) -> (exists jt_gap_source_index. jt_gap_source_index+S (i)=(u)) -> (exists j. ((exists jt_gap_chosen_image_bound. jt_gap_chosen_image_bound+S (j)=(v)) /\ (forall jt_b_chosen_image_match jt_c_chosen_image_match jt_d_chosen_image_match jt_e_chosen_image_match. (((((exists fs_h_jt_chosen_image_matchleftcode. fs_h_jt_chosen_image_matchleftcode + S (jt_b_chosen_image_match) = S ((S (i)) * B)) /\ exists fs_q_jt_chosen_image_matchleftcode. A = fs_q_jt_chosen_image_matchleftcode * S ((S (i)) * B) + (jt_b_chosen_image_match))) /\ (((exists fs_h_jt_chosen_image_matchleftscale. fs_h_jt_chosen_image_matchleftscale + S (jt_c_chosen_image_match) = S ((S (i)) * D)) /\ exists fs_q_jt_chosen_image_matchleftscale. C = fs_q_jt_chosen_image_matchleftscale * S ((S (i)) * D) + (jt_c_chosen_image_match))))) -> (((((exists fs_h_jt_chosen_image_matchrightcode. fs_h_jt_chosen_image_matchrightcode + S (jt_d_chosen_image_match) = S ((S (j)) * F)) /\ exists fs_q_jt_chosen_image_matchrightcode. E = fs_q_jt_chosen_image_matchrightcode * S ((S (j)) * F) + (jt_d_chosen_image_match))) /\ (((exists fs_h_jt_chosen_image_matchrightscale. fs_h_jt_chosen_image_matchrightscale + S (jt_e_chosen_image_match) = S ((S (j)) * H)) /\ exists fs_q_jt_chosen_image_matchrightscale. G = fs_q_jt_chosen_image_matchrightscale * S ((S (j)) * H) + (jt_e_chosen_image_match))))) -> (forall jt_index_chosen_image_matchequal jt_left_chosen_image_matchequal jt_right_chosen_image_matchequal. (exists jt_gap_chosen_image_matchequalindex. jt_gap_chosen_image_matchequalindex+S (jt_index_chosen_image_matchequal)=(k)) -> (((exists fs_h_jt_chosen_image_matchequalleft. fs_h_jt_chosen_image_matchequalleft + S (jt_left_chosen_image_matchequal) = S ((S (jt_index_chosen_image_matchequal)) * jt_c_chosen_image_match)) /\ exists fs_q_jt_chosen_image_matchequalleft. jt_b_chosen_image_match = fs_q_jt_chosen_image_matchequalleft * S ((S (jt_index_chosen_image_matchequal)) * jt_c_chosen_image_match) + (jt_left_chosen_image_matchequal))) -> (((exists fs_h_jt_chosen_image_matchequalright. fs_h_jt_chosen_image_matchequalright + S (jt_right_chosen_image_matchequal) = S ((S (jt_index_chosen_image_matchequal)) * jt_e_chosen_image_match)) /\ exists fs_q_jt_chosen_image_matchequalright. jt_d_chosen_image_match = fs_q_jt_chosen_image_matchequalright * S ((S (jt_index_chosen_image_matchequal)) * jt_e_chosen_image_match) + (jt_right_chosen_image_matchequal))) -> jt_left_chosen_image_matchequal=jt_right_chosen_image_matchequal))))