integer_vector_add_from_component_sums

Exact expanded first-order arithmetic statement

forall ab ac db dc eb ec fb fc pb pc nb nc l. (forall ff_index_mcp_add_ics_add_components_p ff_left_mcp_add_ics_add_components_p ff_right_mcp_add_ics_add_components_p ff_target_mcp_add_ics_add_components_p. (exists mcp_gap_ics_add_components_p_bound. mcp_gap_ics_add_components_p_bound + S (ff_index_mcp_add_ics_add_components_p) = (l)) -> (((exists fs_h_mcp_ics_add_components_p_left. fs_h_mcp_ics_add_components_p_left + S (ff_left_mcp_add_ics_add_components_p) = S ((S (ff_index_mcp_add_ics_add_components_p)) * ac)) /\ exists fs_q_mcp_ics_add_components_p_left. ab = fs_q_mcp_ics_add_components_p_left * S ((S (ff_index_mcp_add_ics_add_components_p)) * ac) + (ff_left_mcp_add_ics_add_components_p))) -> (((exists fs_h_mcp_ics_add_components_p_right. fs_h_mcp_ics_add_components_p_right + S (ff_right_mcp_add_ics_add_components_p) = S ((S (ff_index_mcp_add_ics_add_components_p)) * ec)) /\ exists fs_q_mcp_ics_add_components_p_right. eb = fs_q_mcp_ics_add_components_p_right * S ((S (ff_index_mcp_add_ics_add_components_p)) * ec) + (ff_right_mcp_add_ics_add_components_p))) -> (((exists fs_h_mcp_ics_add_components_p_target. fs_h_mcp_ics_add_components_p_target + S (ff_target_mcp_add_ics_add_components_p) = S ((S (ff_index_mcp_add_ics_add_components_p)) * pc)) /\ exists fs_q_mcp_ics_add_components_p_target. pb = fs_q_mcp_ics_add_components_p_target * S ((S (ff_index_mcp_add_ics_add_components_p)) * pc) + (ff_target_mcp_add_ics_add_components_p))) -> ff_target_mcp_add_ics_add_components_p = ff_left_mcp_add_ics_add_components_p + ff_right_mcp_add_ics_add_components_p) -> (forall ff_index_mcp_add_ics_add_components_n ff_left_mcp_add_ics_add_components_n ff_right_mcp_add_ics_add_components_n ff_target_mcp_add_ics_add_components_n. (exists mcp_gap_ics_add_components_n_bound. mcp_gap_ics_add_components_n_bound + S (ff_index_mcp_add_ics_add_components_n) = (l)) -> (((exists fs_h_mcp_ics_add_components_n_left. fs_h_mcp_ics_add_components_n_left + S (ff_left_mcp_add_ics_add_components_n) = S ((S (ff_index_mcp_add_ics_add_components_n)) * dc)) /\ exists fs_q_mcp_ics_add_components_n_left. db = fs_q_mcp_ics_add_components_n_left * S ((S (ff_index_mcp_add_ics_add_components_n)) * dc) + (ff_left_mcp_add_ics_add_components_n))) -> (((exists fs_h_mcp_ics_add_components_n_right. fs_h_mcp_ics_add_components_n_right + S (ff_right_mcp_add_ics_add_components_n) = S ((S (ff_index_mcp_add_ics_add_components_n)) * fc)) /\ exists fs_q_mcp_ics_add_components_n_right. fb = fs_q_mcp_ics_add_components_n_right * S ((S (ff_index_mcp_add_ics_add_components_n)) * fc) + (ff_right_mcp_add_ics_add_components_n))) -> (((exists fs_h_mcp_ics_add_components_n_target. fs_h_mcp_ics_add_components_n_target + S (ff_target_mcp_add_ics_add_components_n) = S ((S (ff_index_mcp_add_ics_add_components_n)) * nc)) /\ exists fs_q_mcp_ics_add_components_n_target. nb = fs_q_mcp_ics_add_components_n_target * S ((S (ff_index_mcp_add_ics_add_components_n)) * nc) + (ff_target_mcp_add_ics_add_components_n))) -> ff_target_mcp_add_ics_add_components_n = ff_left_mcp_add_ics_add_components_n + ff_right_mcp_add_ics_add_components_n) -> (forall ics_index_add_components_result ics_value0_add_components_result ics_value1_add_components_result ics_value2_add_components_result ics_value3_add_components_result ics_value4_add_components_result ics_value5_add_components_result. (exists ics_gap_add_components_result_bound. ics_gap_add_components_result_bound + S (ics_index_add_components_result) = (l)) -> (((exists fs_h_ics_add_components_result_at0. fs_h_ics_add_components_result_at0 + S (ics_value0_add_components_result) = S ((S (ics_index_add_components_result)) * ac)) /\ exists fs_q_ics_add_components_result_at0. ab = fs_q_ics_add_components_result_at0 * S ((S (ics_index_add_components_result)) * ac) + (ics_value0_add_components_result))) -> (((exists fs_h_ics_add_components_result_at1. fs_h_ics_add_components_result_at1 + S (ics_value1_add_components_result) = S ((S (ics_index_add_components_result)) * dc)) /\ exists fs_q_ics_add_components_result_at1. db = fs_q_ics_add_components_result_at1 * S ((S (ics_index_add_components_result)) * dc) + (ics_value1_add_components_result))) -> (((exists fs_h_ics_add_components_result_at2. fs_h_ics_add_components_result_at2 + S (ics_value2_add_components_result) = S ((S (ics_index_add_components_result)) * ec)) /\ exists fs_q_ics_add_components_result_at2. eb = fs_q_ics_add_components_result_at2 * S ((S (ics_index_add_components_result)) * ec) + (ics_value2_add_components_result))) -> (((exists fs_h_ics_add_components_result_at3. fs_h_ics_add_components_result_at3 + S (ics_value3_add_components_result) = S ((S (ics_index_add_components_result)) * fc)) /\ exists fs_q_ics_add_components_result_at3. fb = fs_q_ics_add_components_result_at3 * S ((S (ics_index_add_components_result)) * fc) + (ics_value3_add_components_result))) -> (((exists fs_h_ics_add_components_result_at4. fs_h_ics_add_components_result_at4 + S (ics_value4_add_components_result) = S ((S (ics_index_add_components_result)) * pc)) /\ exists fs_q_ics_add_components_result_at4. pb = fs_q_ics_add_components_result_at4 * S ((S (ics_index_add_components_result)) * pc) + (ics_value4_add_components_result))) -> (((exists fs_h_ics_add_components_result_at5. fs_h_ics_add_components_result_at5 + S (ics_value5_add_components_result) = S ((S (ics_index_add_components_result)) * nc)) /\ exists fs_q_ics_add_components_result_at5. nb = fs_q_ics_add_components_result_at5 * S ((S (ics_index_add_components_result)) * nc) + (ics_value5_add_components_result))) -> ics_value4_add_components_result + (ics_value1_add_components_result + ics_value3_add_components_result) = (ics_value0_add_components_result + ics_value2_add_components_result) + ics_value5_add_components_result)