jordan_enumeration_index_map_entry

forall k A B C D E F G H Z W q v i j. (forall jt_index_actual_given_map. (exists jt_gap_actual_given_mapindex. jt_gap_actual_given_mapindex+S (jt_index_actual_given_map)=(q)) -> exists jt_image_actual_given_map. ((((exists fs_h_jt_actual_given_mapat. fs_h_jt_actual_given_mapat + S (jt_image_actual_given_map) = S ((S (jt_index_actual_given_map)) * W)) /\ exists fs_q_jt_actual_given_mapat. Z = fs_q_jt_actual_given_mapat * S ((S (jt_index_actual_given_map)) * W) + (jt_image_actual_given_map))) /\ (((exists jt_gap_actual_given_mapbound. jt_gap_actual_given_mapbound+S (jt_image_actual_given_map)=(v)) /\ (forall jt_b_actual_given_mapmatch jt_c_actual_given_mapmatch jt_d_actual_given_mapmatch jt_e_actual_given_mapmatch. (((((exists fs_h_jt_actual_given_mapmatchleftcode. fs_h_jt_actual_given_mapmatchleftcode + S (jt_b_actual_given_mapmatch) = S ((S (jt_index_actual_given_map)) * B)) /\ exists fs_q_jt_actual_given_mapmatchleftcode. A = fs_q_jt_actual_given_mapmatchleftcode * S ((S (jt_index_actual_given_map)) * B) + (jt_b_actual_given_mapmatch))) /\ (((exists fs_h_jt_actual_given_mapmatchleftscale. fs_h_jt_actual_given_mapmatchleftscale + S (jt_c_actual_given_mapmatch) = S ((S (jt_index_actual_given_map)) * D)) /\ exists fs_q_jt_actual_given_mapmatchleftscale. C = fs_q_jt_actual_given_mapmatchleftscale * S ((S (jt_index_actual_given_map)) * D) + (jt_c_actual_given_mapmatch))))) -> (((((exists fs_h_jt_actual_given_mapmatchrightcode. fs_h_jt_actual_given_mapmatchrightcode + S (jt_d_actual_given_mapmatch) = S ((S (jt_image_actual_given_map)) * F)) /\ exists fs_q_jt_actual_given_mapmatchrightcode. E = fs_q_jt_actual_given_mapmatchrightcode * S ((S (jt_image_actual_given_map)) * F) + (jt_d_actual_given_mapmatch))) /\ (((exists fs_h_jt_actual_given_mapmatchrightscale. fs_h_jt_actual_given_mapmatchrightscale + S (jt_e_actual_given_mapmatch) = S ((S (jt_image_actual_given_map)) * H)) /\ exists fs_q_jt_actual_given_mapmatchrightscale. G = fs_q_jt_actual_given_mapmatchrightscale * S ((S (jt_image_actual_given_map)) * H) + (jt_e_actual_given_mapmatch))))) -> (forall jt_index_actual_given_mapmatchequal jt_left_actual_given_mapmatchequal jt_right_actual_given_mapmatchequal. (exists jt_gap_actual_given_mapmatchequalindex. jt_gap_actual_given_mapmatchequalindex+S (jt_index_actual_given_mapmatchequal)=(k)) -> (((exists fs_h_jt_actual_given_mapmatchequalleft. fs_h_jt_actual_given_mapmatchequalleft + S (jt_left_actual_given_mapmatchequal) = S ((S (jt_index_actual_given_mapmatchequal)) * jt_c_actual_given_mapmatch)) /\ exists fs_q_jt_actual_given_mapmatchequalleft. jt_b_actual_given_mapmatch = fs_q_jt_actual_given_mapmatchequalleft * S ((S (jt_index_actual_given_mapmatchequal)) * jt_c_actual_given_mapmatch) + (jt_left_actual_given_mapmatchequal))) -> (((exists fs_h_jt_actual_given_mapmatchequalright. fs_h_jt_actual_given_mapmatchequalright + S (jt_right_actual_given_mapmatchequal) = S ((S (jt_index_actual_given_mapmatchequal)) * jt_e_actual_given_mapmatch)) /\ exists fs_q_jt_actual_given_mapmatchequalright. jt_d_actual_given_mapmatch = fs_q_jt_actual_given_mapmatchequalright * S ((S (jt_index_actual_given_mapmatchequal)) * jt_e_actual_given_mapmatch) + (jt_right_actual_given_mapmatchequal))) -> jt_left_actual_given_mapmatchequal=jt_right_actual_given_mapmatchequal)))))) -> (exists jt_gap_actual_index. jt_gap_actual_index+S (i)=(q)) -> (((exists fs_h_jt_actual_value. fs_h_jt_actual_value + S (j) = S ((S (i)) * W)) /\ exists fs_q_jt_actual_value. Z = fs_q_jt_actual_value * S ((S (i)) * W) + (j))) -> (((exists jt_gap_actual_result_bound. jt_gap_actual_result_bound+S (j)=(v)) /\ (forall jt_b_actual_result_match jt_c_actual_result_match jt_d_actual_result_match jt_e_actual_result_match. (((((exists fs_h_jt_actual_result_matchleftcode. fs_h_jt_actual_result_matchleftcode + S (jt_b_actual_result_match) = S ((S (i)) * B)) /\ exists fs_q_jt_actual_result_matchleftcode. A = fs_q_jt_actual_result_matchleftcode * S ((S (i)) * B) + (jt_b_actual_result_match))) /\ (((exists fs_h_jt_actual_result_matchleftscale. fs_h_jt_actual_result_matchleftscale + S (jt_c_actual_result_match) = S ((S (i)) * D)) /\ exists fs_q_jt_actual_result_matchleftscale. C = fs_q_jt_actual_result_matchleftscale * S ((S (i)) * D) + (jt_c_actual_result_match))))) -> (((((exists fs_h_jt_actual_result_matchrightcode. fs_h_jt_actual_result_matchrightcode + S (jt_d_actual_result_match) = S ((S (j)) * F)) /\ exists fs_q_jt_actual_result_matchrightcode. E = fs_q_jt_actual_result_matchrightcode * S ((S (j)) * F) + (jt_d_actual_result_match))) /\ (((exists fs_h_jt_actual_result_matchrightscale. fs_h_jt_actual_result_matchrightscale + S (jt_e_actual_result_match) = S ((S (j)) * H)) /\ exists fs_q_jt_actual_result_matchrightscale. G = fs_q_jt_actual_result_matchrightscale * S ((S (j)) * H) + (jt_e_actual_result_match))))) -> (forall jt_index_actual_result_matchequal jt_left_actual_result_matchequal jt_right_actual_result_matchequal. (exists jt_gap_actual_result_matchequalindex. jt_gap_actual_result_matchequalindex+S (jt_index_actual_result_matchequal)=(k)) -> (((exists fs_h_jt_actual_result_matchequalleft. fs_h_jt_actual_result_matchequalleft + S (jt_left_actual_result_matchequal) = S ((S (jt_index_actual_result_matchequal)) * jt_c_actual_result_match)) /\ exists fs_q_jt_actual_result_matchequalleft. jt_b_actual_result_match = fs_q_jt_actual_result_matchequalleft * S ((S (jt_index_actual_result_matchequal)) * jt_c_actual_result_match) + (jt_left_actual_result_matchequal))) -> (((exists fs_h_jt_actual_result_matchequalright. fs_h_jt_actual_result_matchequalright + S (jt_right_actual_result_matchequal) = S ((S (jt_index_actual_result_matchequal)) * jt_e_actual_result_match)) /\ exists fs_q_jt_actual_result_matchequalright. jt_d_actual_result_match = fs_q_jt_actual_result_matchequalright * S ((S (jt_index_actual_result_matchequal)) * jt_e_actual_result_match) + (jt_right_actual_result_matchequal))) -> jt_left_actual_result_matchequal=jt_right_actual_result_matchequal))))