jordan_enumeration_position_match_from_entries

Exact expanded first-order arithmetic statement

forall k A B C D E F G H i j b c d e. (((((exists fs_h_jt_position_leftcode. fs_h_jt_position_leftcode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_position_leftcode. A = fs_q_jt_position_leftcode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_position_leftscale. fs_h_jt_position_leftscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_position_leftscale. C = fs_q_jt_position_leftscale * S ((S (i)) * D) + (c))))) -> (((((exists fs_h_jt_position_rightcode. fs_h_jt_position_rightcode + S (d) = S ((S (j)) * F)) /\ exists fs_q_jt_position_rightcode. E = fs_q_jt_position_rightcode * S ((S (j)) * F) + (d))) /\ (((exists fs_h_jt_position_rightscale. fs_h_jt_position_rightscale + S (e) = S ((S (j)) * H)) /\ exists fs_q_jt_position_rightscale. G = fs_q_jt_position_rightscale * S ((S (j)) * H) + (e))))) -> (forall jt_index_position_equal jt_left_position_equal jt_right_position_equal. (exists jt_gap_position_equalindex. jt_gap_position_equalindex+S (jt_index_position_equal)=(k)) -> (((exists fs_h_jt_position_equalleft. fs_h_jt_position_equalleft + S (jt_left_position_equal) = S ((S (jt_index_position_equal)) * c)) /\ exists fs_q_jt_position_equalleft. b = fs_q_jt_position_equalleft * S ((S (jt_index_position_equal)) * c) + (jt_left_position_equal))) -> (((exists fs_h_jt_position_equalright. fs_h_jt_position_equalright + S (jt_right_position_equal) = S ((S (jt_index_position_equal)) * e)) /\ exists fs_q_jt_position_equalright. d = fs_q_jt_position_equalright * S ((S (jt_index_position_equal)) * e) + (jt_right_position_equal))) -> jt_left_position_equal=jt_right_position_equal) -> (forall jt_b_position_result jt_c_position_result jt_d_position_result jt_e_position_result. (((((exists fs_h_jt_position_resultleftcode. fs_h_jt_position_resultleftcode + S (jt_b_position_result) = S ((S (i)) * B)) /\ exists fs_q_jt_position_resultleftcode. A = fs_q_jt_position_resultleftcode * S ((S (i)) * B) + (jt_b_position_result))) /\ (((exists fs_h_jt_position_resultleftscale. fs_h_jt_position_resultleftscale + S (jt_c_position_result) = S ((S (i)) * D)) /\ exists fs_q_jt_position_resultleftscale. C = fs_q_jt_position_resultleftscale * S ((S (i)) * D) + (jt_c_position_result))))) -> (((((exists fs_h_jt_position_resultrightcode. fs_h_jt_position_resultrightcode + S (jt_d_position_result) = S ((S (j)) * F)) /\ exists fs_q_jt_position_resultrightcode. E = fs_q_jt_position_resultrightcode * S ((S (j)) * F) + (jt_d_position_result))) /\ (((exists fs_h_jt_position_resultrightscale. fs_h_jt_position_resultrightscale + S (jt_e_position_result) = S ((S (j)) * H)) /\ exists fs_q_jt_position_resultrightscale. G = fs_q_jt_position_resultrightscale * S ((S (j)) * H) + (jt_e_position_result))))) -> (forall jt_index_position_resultequal jt_left_position_resultequal jt_right_position_resultequal. (exists jt_gap_position_resultequalindex. jt_gap_position_resultequalindex+S (jt_index_position_resultequal)=(k)) -> (((exists fs_h_jt_position_resultequalleft. fs_h_jt_position_resultequalleft + S (jt_left_position_resultequal) = S ((S (jt_index_position_resultequal)) * jt_c_position_result)) /\ exists fs_q_jt_position_resultequalleft. jt_b_position_result = fs_q_jt_position_resultequalleft * S ((S (jt_index_position_resultequal)) * jt_c_position_result) + (jt_left_position_resultequal))) -> (((exists fs_h_jt_position_resultequalright. fs_h_jt_position_resultequalright + S (jt_right_position_resultequal) = S ((S (jt_index_position_resultequal)) * jt_e_position_result)) /\ exists fs_q_jt_position_resultequalright. jt_d_position_result = fs_q_jt_position_resultequalright * S ((S (jt_index_position_resultequal)) * jt_e_position_result) + (jt_right_position_resultequal))) -> jt_left_position_resultequal=jt_right_position_resultequal))