matrix_integer_vector_equality_restrict

Exact expanded first-order arithmetic statement

forall ab ac bb bc eb ec fb fc L K. (exists mdr_gap_restriction_bound. mdr_gap_restriction_bound + (K) = (L)) -> (forall ics_index_equality_full ics_value0_equality_full ics_value1_equality_full ics_value2_equality_full ics_value3_equality_full. (exists ics_gap_equality_full_bound. ics_gap_equality_full_bound + S (ics_index_equality_full) = (L)) -> (((exists fs_h_ics_equality_full_at0. fs_h_ics_equality_full_at0 + S (ics_value0_equality_full) = S ((S (ics_index_equality_full)) * ac)) /\ exists fs_q_ics_equality_full_at0. ab = fs_q_ics_equality_full_at0 * S ((S (ics_index_equality_full)) * ac) + (ics_value0_equality_full))) -> (((exists fs_h_ics_equality_full_at1. fs_h_ics_equality_full_at1 + S (ics_value1_equality_full) = S ((S (ics_index_equality_full)) * bc)) /\ exists fs_q_ics_equality_full_at1. bb = fs_q_ics_equality_full_at1 * S ((S (ics_index_equality_full)) * bc) + (ics_value1_equality_full))) -> (((exists fs_h_ics_equality_full_at2. fs_h_ics_equality_full_at2 + S (ics_value2_equality_full) = S ((S (ics_index_equality_full)) * ec)) /\ exists fs_q_ics_equality_full_at2. eb = fs_q_ics_equality_full_at2 * S ((S (ics_index_equality_full)) * ec) + (ics_value2_equality_full))) -> (((exists fs_h_ics_equality_full_at3. fs_h_ics_equality_full_at3 + S (ics_value3_equality_full) = S ((S (ics_index_equality_full)) * fc)) /\ exists fs_q_ics_equality_full_at3. fb = fs_q_ics_equality_full_at3 * S ((S (ics_index_equality_full)) * fc) + (ics_value3_equality_full))) -> ics_value0_equality_full + ics_value3_equality_full = ics_value2_equality_full + ics_value1_equality_full) -> (forall ics_index_equality_prefix ics_value0_equality_prefix ics_value1_equality_prefix ics_value2_equality_prefix ics_value3_equality_prefix. (exists ics_gap_equality_prefix_bound. ics_gap_equality_prefix_bound + S (ics_index_equality_prefix) = (K)) -> (((exists fs_h_ics_equality_prefix_at0. fs_h_ics_equality_prefix_at0 + S (ics_value0_equality_prefix) = S ((S (ics_index_equality_prefix)) * ac)) /\ exists fs_q_ics_equality_prefix_at0. ab = fs_q_ics_equality_prefix_at0 * S ((S (ics_index_equality_prefix)) * ac) + (ics_value0_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at1. fs_h_ics_equality_prefix_at1 + S (ics_value1_equality_prefix) = S ((S (ics_index_equality_prefix)) * bc)) /\ exists fs_q_ics_equality_prefix_at1. bb = fs_q_ics_equality_prefix_at1 * S ((S (ics_index_equality_prefix)) * bc) + (ics_value1_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at2. fs_h_ics_equality_prefix_at2 + S (ics_value2_equality_prefix) = S ((S (ics_index_equality_prefix)) * ec)) /\ exists fs_q_ics_equality_prefix_at2. eb = fs_q_ics_equality_prefix_at2 * S ((S (ics_index_equality_prefix)) * ec) + (ics_value2_equality_prefix))) -> (((exists fs_h_ics_equality_prefix_at3. fs_h_ics_equality_prefix_at3 + S (ics_value3_equality_prefix) = S ((S (ics_index_equality_prefix)) * fc)) /\ exists fs_q_ics_equality_prefix_at3. fb = fs_q_ics_equality_prefix_at3 * S ((S (ics_index_equality_prefix)) * fc) + (ics_value3_equality_prefix))) -> ics_value0_equality_prefix + ics_value3_equality_prefix = ics_value2_equality_prefix + ics_value1_equality_prefix)