signed_prefix_sum_scalar_multiply_values_exist

Exact expanded first-order arithmetic statement

forall l a F G. (((exists dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table. (((F) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)))))) /\ (forall dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table. (exists pvs_le_gap_signed_prefix_sum_scalar_multiply_construct_graphinput_tabledomain. pvs_le_gap_signed_prefix_sum_scalar_multiply_construct_graphinput_tabledomain + (dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table) = (l)) -> exists dst_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_table dst_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_table dst_value_signed_prefix_sum_scalar_multiply_construct_graphinput_table. ((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrypositive. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrypositive + S (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_table) = S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrypositive. dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrypositive * S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_table))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrynegative. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrynegative + S (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_table) = S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrynegative. dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphinput_table = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentrynegative * S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphinput_table)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_table))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue. (((((dst_value_signed_prefix_sum_scalar_multiply_construct_graphinput_table) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvaluedecode. (((dst_value_signed_prefix_sum_scalar_multiply_construct_graphinput_table) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvaluedecode))) /\ ((dst_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue = (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphinput_table) + ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table. (((G) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)))))) /\ (forall dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table. (exists pvs_le_gap_signed_prefix_sum_scalar_multiply_construct_graphoutput_tabledomain. pvs_le_gap_signed_prefix_sum_scalar_multiply_construct_graphoutput_tabledomain + (dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) = (l)) -> exists dst_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_table dst_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_table dst_value_signed_prefix_sum_scalar_multiply_construct_graphoutput_table. ((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrypositive. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrypositive + S (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) = S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrypositive. dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrypositive * S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_table))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrynegative. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrynegative + S (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) = S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrynegative. dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphoutput_table = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentrynegative * S ((S (dst_index_signed_prefix_sum_scalar_multiply_construct_graphoutput_table)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_table))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue. (((((dst_value_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvaluedecode. (((dst_value_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvaluedecode))) /\ ((dst_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue = (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphoutput_table) + ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphoutput_tableentryvalue))))))))) /\ (forall sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries. (exists pvs_gap_signed_prefix_sum_scalar_multiply_construct_graphentriesbound. pvs_gap_signed_prefix_sum_scalar_multiply_construct_graphentriesbound + S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries) = (l)) -> exists sto_input_signed_prefix_sum_scalar_multiply_construct_graphentries sto_output_signed_prefix_sum_scalar_multiply_construct_graphentries. ((exists dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput. (((F) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)))))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputpositive. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputpositive + S (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) = S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputpositive. dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputpositive * S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputnegative. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputnegative + S (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) = S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputnegative. dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputnegative * S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue. (((((sto_input_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvaluedecode. (((sto_input_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvaluedecode))) /\ ((dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue = (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinput) + ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput. (((G) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)))))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputpositive. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputpositive + S (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) = S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputpositive. dst_positive_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputpositive * S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput))) /\ (((((exists ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputnegative. ff_h_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputnegative + S (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) = S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput)) /\ exists ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputnegative. dst_negative_code_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput = ff_q_pvs_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputnegative * S ((S (sto_index_signed_prefix_sum_scalar_multiply_construct_graphentries)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue. (((((sto_output_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvaluedecode. (((sto_output_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvaluedecode))) /\ ((dst_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + ge_balance_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue = (dst_negative_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutput) + ge_balance_positive_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoutputvalue))))))))) /\ (exists sto_ap_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation sto_an_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation sto_bp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation sto_bn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation sto_cp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation sto_cn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation. (((((a) = 2 * (sto_ap_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) /\ (sto_an_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationleft. (((a) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationleft + 1 /\ (sto_ap_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) /\ (sto_an_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationleft))) /\ ((((((sto_input_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * (sto_bp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) /\ (sto_bn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationright. (((sto_input_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationright + 1 /\ (sto_bp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) /\ (sto_bn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationright))) /\ ((((((sto_output_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * (sto_cp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) /\ (sto_cn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationoutput. (((sto_output_signed_prefix_sum_scalar_multiply_construct_graphentries) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationoutput + 1 /\ (sto_cp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = 0) /\ (sto_cn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperationoutput))) /\ ((sto_ap_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation * sto_bp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation + sto_an_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation * sto_bn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) + sto_cn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation = (sto_ap_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation * sto_bn_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation + sto_an_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation * sto_bp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation) + sto_cp_signed_prefix_sum_scalar_multiply_construct_graphentriesentryoperation))))))))))))))) -> exists b c. ((exists dst_positive_code_signed_prefix_sum_scalar_multiply_result0 dst_positive_scale_signed_prefix_sum_scalar_multiply_result0 dst_negative_code_signed_prefix_sum_scalar_multiply_result0 dst_negative_scale_signed_prefix_sum_scalar_multiply_result0 dst_positive_sum_signed_prefix_sum_scalar_multiply_result0 dst_negative_sum_signed_prefix_sum_scalar_multiply_result0. (((F) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result0))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result0) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)))))) /\ (((exists fs_u_dst_signed_prefix_sum_scalar_multiply_result0positive fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_start. fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_start + S (0) = S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_start. fs_u_dst_signed_prefix_sum_scalar_multiply_result0positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_start * S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive) + (0))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_terminal. fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_terminal + S (dst_positive_sum_signed_prefix_sum_scalar_multiply_result0) = S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_terminal. fs_u_dst_signed_prefix_sum_scalar_multiply_result0positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_terminal * S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive) + (dst_positive_sum_signed_prefix_sum_scalar_multiply_result0))) /\ forall fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps. (exists fs_lt_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_bound. fs_lt_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_bound + S fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps = l) -> exists fs_a_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps fs_r_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps fs_s_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_summand. fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_summand + S (fs_a_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_result0)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_summand. dst_positive_code_signed_prefix_sum_scalar_multiply_result0 = fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_summand * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_result0) + (fs_a_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_partial. fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_partial + S (fs_r_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_partial. fs_u_dst_signed_prefix_sum_scalar_multiply_result0positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_partial * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive) + (fs_r_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_successor. fs_h_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_successor + S (fs_s_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps) = S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_successor. fs_u_dst_signed_prefix_sum_scalar_multiply_result0positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps_successor * S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0positive) + (fs_s_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps))) /\ fs_s_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps = fs_r_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps + fs_a_dst_signed_prefix_sum_scalar_multiply_result0positive_body_steps)))))) /\ (((exists fs_u_dst_signed_prefix_sum_scalar_multiply_result0negative fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_start. fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_start + S (0) = S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_start. fs_u_dst_signed_prefix_sum_scalar_multiply_result0negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_start * S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative) + (0))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_terminal. fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_terminal + S (dst_negative_sum_signed_prefix_sum_scalar_multiply_result0) = S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_terminal. fs_u_dst_signed_prefix_sum_scalar_multiply_result0negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_terminal * S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative) + (dst_negative_sum_signed_prefix_sum_scalar_multiply_result0))) /\ forall fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps. (exists fs_lt_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_bound. fs_lt_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_bound + S fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps = l) -> exists fs_a_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps fs_r_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps fs_s_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_summand. fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_summand + S (fs_a_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_result0)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_summand. dst_negative_code_signed_prefix_sum_scalar_multiply_result0 = fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_summand * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_result0) + (fs_a_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_partial. fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_partial + S (fs_r_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_partial. fs_u_dst_signed_prefix_sum_scalar_multiply_result0negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_partial * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative) + (fs_r_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_successor. fs_h_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_successor + S (fs_s_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps) = S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_successor. fs_u_dst_signed_prefix_sum_scalar_multiply_result0negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps_successor * S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result0negative) + (fs_s_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps))) /\ fs_s_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps = fs_r_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps + fs_a_dst_signed_prefix_sum_scalar_multiply_result0negative_body_steps)))))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_result0result ge_balance_negative_signed_prefix_sum_scalar_multiply_result0result. (((((b) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_result0result) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_result0result) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_result0resultdecode. (((b) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_result0resultdecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_result0result) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_result0result) = S ge_signed_half_signed_prefix_sum_scalar_multiply_result0resultdecode))) /\ ((dst_positive_sum_signed_prefix_sum_scalar_multiply_result0) + ge_balance_negative_signed_prefix_sum_scalar_multiply_result0result = (dst_negative_sum_signed_prefix_sum_scalar_multiply_result0) + ge_balance_positive_signed_prefix_sum_scalar_multiply_result0result))))))))) /\ (((exists dst_positive_code_signed_prefix_sum_scalar_multiply_result1 dst_positive_scale_signed_prefix_sum_scalar_multiply_result1 dst_negative_code_signed_prefix_sum_scalar_multiply_result1 dst_negative_scale_signed_prefix_sum_scalar_multiply_result1 dst_positive_sum_signed_prefix_sum_scalar_multiply_result1 dst_negative_sum_signed_prefix_sum_scalar_multiply_result1. (((G) = (((((dst_positive_code_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)))) * S ((((dst_positive_code_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_positive_code_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_positive_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_positive_scale_signed_prefix_sum_scalar_multiply_result1))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)))) + ((((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1))) + (((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) * S ((dst_negative_code_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) + ((dst_negative_scale_signed_prefix_sum_scalar_multiply_result1) + (dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)))))) /\ (((exists fs_u_dst_signed_prefix_sum_scalar_multiply_result1positive fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_start. fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_start + S (0) = S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_start. fs_u_dst_signed_prefix_sum_scalar_multiply_result1positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_start * S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive) + (0))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_terminal. fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_terminal + S (dst_positive_sum_signed_prefix_sum_scalar_multiply_result1) = S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_terminal. fs_u_dst_signed_prefix_sum_scalar_multiply_result1positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_terminal * S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive) + (dst_positive_sum_signed_prefix_sum_scalar_multiply_result1))) /\ forall fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps. (exists fs_lt_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_bound. fs_lt_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_bound + S fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps = l) -> exists fs_a_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps fs_r_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps fs_s_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_summand. fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_summand + S (fs_a_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_result1)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_summand. dst_positive_code_signed_prefix_sum_scalar_multiply_result1 = fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_summand * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * dst_positive_scale_signed_prefix_sum_scalar_multiply_result1) + (fs_a_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_partial. fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_partial + S (fs_r_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_partial. fs_u_dst_signed_prefix_sum_scalar_multiply_result1positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_partial * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive) + (fs_r_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_successor. fs_h_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_successor + S (fs_s_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps) = S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_successor. fs_u_dst_signed_prefix_sum_scalar_multiply_result1positive = fs_q_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps_successor * S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1positive) + (fs_s_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps))) /\ fs_s_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps = fs_r_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps + fs_a_dst_signed_prefix_sum_scalar_multiply_result1positive_body_steps)))))) /\ (((exists fs_u_dst_signed_prefix_sum_scalar_multiply_result1negative fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_start. fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_start + S (0) = S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_start. fs_u_dst_signed_prefix_sum_scalar_multiply_result1negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_start * S ((S (0)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative) + (0))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_terminal. fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_terminal + S (dst_negative_sum_signed_prefix_sum_scalar_multiply_result1) = S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_terminal. fs_u_dst_signed_prefix_sum_scalar_multiply_result1negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_terminal * S ((S (l)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative) + (dst_negative_sum_signed_prefix_sum_scalar_multiply_result1))) /\ forall fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps. (exists fs_lt_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_bound. fs_lt_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_bound + S fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps = l) -> exists fs_a_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps fs_r_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps fs_s_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps. ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_summand. fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_summand + S (fs_a_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_result1)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_summand. dst_negative_code_signed_prefix_sum_scalar_multiply_result1 = fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_summand * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * dst_negative_scale_signed_prefix_sum_scalar_multiply_result1) + (fs_a_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_partial. fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_partial + S (fs_r_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps) = S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_partial. fs_u_dst_signed_prefix_sum_scalar_multiply_result1negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_partial * S ((S (fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative) + (fs_r_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps))) /\ ((((exists fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_successor. fs_h_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_successor + S (fs_s_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps) = S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative)) /\ exists fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_successor. fs_u_dst_signed_prefix_sum_scalar_multiply_result1negative = fs_q_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps_successor * S ((S (S fs_i_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)) * fs_v_dst_signed_prefix_sum_scalar_multiply_result1negative) + (fs_s_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps))) /\ fs_s_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps = fs_r_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps + fs_a_dst_signed_prefix_sum_scalar_multiply_result1negative_body_steps)))))) /\ (exists ge_balance_positive_signed_prefix_sum_scalar_multiply_result1result ge_balance_negative_signed_prefix_sum_scalar_multiply_result1result. (((((c) = 2 * (ge_balance_positive_signed_prefix_sum_scalar_multiply_result1result) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_result1result) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_result1resultdecode. (((c) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_result1resultdecode + 1 /\ (ge_balance_positive_signed_prefix_sum_scalar_multiply_result1result) = 0) /\ (ge_balance_negative_signed_prefix_sum_scalar_multiply_result1result) = S ge_signed_half_signed_prefix_sum_scalar_multiply_result1resultdecode))) /\ ((dst_positive_sum_signed_prefix_sum_scalar_multiply_result1) + ge_balance_negative_signed_prefix_sum_scalar_multiply_result1result = (dst_negative_sum_signed_prefix_sum_scalar_multiply_result1) + ge_balance_positive_signed_prefix_sum_scalar_multiply_result1result))))))))) /\ (exists sto_ap_signed_prefix_sum_scalar_multiply_result_operation sto_an_signed_prefix_sum_scalar_multiply_result_operation sto_bp_signed_prefix_sum_scalar_multiply_result_operation sto_bn_signed_prefix_sum_scalar_multiply_result_operation sto_cp_signed_prefix_sum_scalar_multiply_result_operation sto_cn_signed_prefix_sum_scalar_multiply_result_operation. (((((a) = 2 * (sto_ap_signed_prefix_sum_scalar_multiply_result_operation) /\ (sto_an_signed_prefix_sum_scalar_multiply_result_operation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationleft. (((a) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationleft + 1 /\ (sto_ap_signed_prefix_sum_scalar_multiply_result_operation) = 0) /\ (sto_an_signed_prefix_sum_scalar_multiply_result_operation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationleft))) /\ ((((((b) = 2 * (sto_bp_signed_prefix_sum_scalar_multiply_result_operation) /\ (sto_bn_signed_prefix_sum_scalar_multiply_result_operation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationright. (((b) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationright + 1 /\ (sto_bp_signed_prefix_sum_scalar_multiply_result_operation) = 0) /\ (sto_bn_signed_prefix_sum_scalar_multiply_result_operation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationright))) /\ ((((((c) = 2 * (sto_cp_signed_prefix_sum_scalar_multiply_result_operation) /\ (sto_cn_signed_prefix_sum_scalar_multiply_result_operation) = 0) \/ exists ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationoutput. (((c) = 2 * ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationoutput + 1 /\ (sto_cp_signed_prefix_sum_scalar_multiply_result_operation) = 0) /\ (sto_cn_signed_prefix_sum_scalar_multiply_result_operation) = S ge_signed_half_signed_prefix_sum_scalar_multiply_result_operationoutput))) /\ ((sto_ap_signed_prefix_sum_scalar_multiply_result_operation * sto_bp_signed_prefix_sum_scalar_multiply_result_operation + sto_an_signed_prefix_sum_scalar_multiply_result_operation * sto_bn_signed_prefix_sum_scalar_multiply_result_operation) + sto_cn_signed_prefix_sum_scalar_multiply_result_operation = (sto_ap_signed_prefix_sum_scalar_multiply_result_operation * sto_bn_signed_prefix_sum_scalar_multiply_result_operation + sto_an_signed_prefix_sum_scalar_multiply_result_operation * sto_bp_signed_prefix_sum_scalar_multiply_result_operation) + sto_cp_signed_prefix_sum_scalar_multiply_result_operation))))))))))