matrix_integer_vector_equality_symmetric

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc l. (forall ics_index_equal_source ics_value0_equal_source ics_value1_equal_source ics_value2_equal_source ics_value3_equal_source. (exists ics_gap_equal_source_bound. ics_gap_equal_source_bound + S (ics_index_equal_source) = (l)) -> (((exists fs_h_ics_equal_source_at0. fs_h_ics_equal_source_at0 + S (ics_value0_equal_source) = S ((S (ics_index_equal_source)) * ac)) /\ exists fs_q_ics_equal_source_at0. ab = fs_q_ics_equal_source_at0 * S ((S (ics_index_equal_source)) * ac) + (ics_value0_equal_source))) -> (((exists fs_h_ics_equal_source_at1. fs_h_ics_equal_source_at1 + S (ics_value1_equal_source) = S ((S (ics_index_equal_source)) * bc)) /\ exists fs_q_ics_equal_source_at1. bb = fs_q_ics_equal_source_at1 * S ((S (ics_index_equal_source)) * bc) + (ics_value1_equal_source))) -> (((exists fs_h_ics_equal_source_at2. fs_h_ics_equal_source_at2 + S (ics_value2_equal_source) = S ((S (ics_index_equal_source)) * ec)) /\ exists fs_q_ics_equal_source_at2. eb = fs_q_ics_equal_source_at2 * S ((S (ics_index_equal_source)) * ec) + (ics_value2_equal_source))) -> (((exists fs_h_ics_equal_source_at3. fs_h_ics_equal_source_at3 + S (ics_value3_equal_source) = S ((S (ics_index_equal_source)) * fc)) /\ exists fs_q_ics_equal_source_at3. fb = fs_q_ics_equal_source_at3 * S ((S (ics_index_equal_source)) * fc) + (ics_value3_equal_source))) -> ics_value0_equal_source + ics_value3_equal_source = ics_value2_equal_source + ics_value1_equal_source) -> (forall ics_index_equal_reverse ics_value0_equal_reverse ics_value1_equal_reverse ics_value2_equal_reverse ics_value3_equal_reverse. (exists ics_gap_equal_reverse_bound. ics_gap_equal_reverse_bound + S (ics_index_equal_reverse) = (l)) -> (((exists fs_h_ics_equal_reverse_at0. fs_h_ics_equal_reverse_at0 + S (ics_value0_equal_reverse) = S ((S (ics_index_equal_reverse)) * ec)) /\ exists fs_q_ics_equal_reverse_at0. eb = fs_q_ics_equal_reverse_at0 * S ((S (ics_index_equal_reverse)) * ec) + (ics_value0_equal_reverse))) -> (((exists fs_h_ics_equal_reverse_at1. fs_h_ics_equal_reverse_at1 + S (ics_value1_equal_reverse) = S ((S (ics_index_equal_reverse)) * fc)) /\ exists fs_q_ics_equal_reverse_at1. fb = fs_q_ics_equal_reverse_at1 * S ((S (ics_index_equal_reverse)) * fc) + (ics_value1_equal_reverse))) -> (((exists fs_h_ics_equal_reverse_at2. fs_h_ics_equal_reverse_at2 + S (ics_value2_equal_reverse) = S ((S (ics_index_equal_reverse)) * ac)) /\ exists fs_q_ics_equal_reverse_at2. ab = fs_q_ics_equal_reverse_at2 * S ((S (ics_index_equal_reverse)) * ac) + (ics_value2_equal_reverse))) -> (((exists fs_h_ics_equal_reverse_at3. fs_h_ics_equal_reverse_at3 + S (ics_value3_equal_reverse) = S ((S (ics_index_equal_reverse)) * bc)) /\ exists fs_q_ics_equal_reverse_at3. bb = fs_q_ics_equal_reverse_at3 * S ((S (ics_index_equal_reverse)) * bc) + (ics_value3_equal_reverse))) -> ics_value0_equal_reverse + ics_value3_equal_reverse = ics_value2_equal_reverse + ics_value1_equal_reverse)