signed_prefix_sum_scalar_multiply

forall l a F G b c. (((exists dst_positive_code_scalar_pointwiseinput_table dst_positive_scale_scalar_pointwiseinput_table dst_negative_code_scalar_pointwiseinput_table dst_negative_scale_scalar_pointwiseinput_table. (((F) = (((((dst_positive_code_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table)) * S ((dst_positive_code_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table)) + ((dst_positive_scale_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table))) + (((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) * S ((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) + ((dst_negative_scale_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)))) * S ((((dst_positive_code_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table)) * S ((dst_positive_code_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table)) + ((dst_positive_scale_scalar_pointwiseinput_table) + (dst_positive_scale_scalar_pointwiseinput_table))) + (((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) * S ((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) + ((dst_negative_scale_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)))) + ((((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) * S ((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) + ((dst_negative_scale_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table))) + (((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) * S ((dst_negative_code_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)) + ((dst_negative_scale_scalar_pointwiseinput_table) + (dst_negative_scale_scalar_pointwiseinput_table)))))) /\ (forall dst_index_scalar_pointwiseinput_table. (exists pvs_le_gap_scalar_pointwiseinput_tabledomain. pvs_le_gap_scalar_pointwiseinput_tabledomain + (dst_index_scalar_pointwiseinput_table) = (l)) -> exists dst_positive_scalar_pointwiseinput_table dst_negative_scalar_pointwiseinput_table dst_value_scalar_pointwiseinput_table. ((((exists ff_h_pvs_scalar_pointwiseinput_tableentrypositive. ff_h_pvs_scalar_pointwiseinput_tableentrypositive + S (dst_positive_scalar_pointwiseinput_table) = S ((S (dst_index_scalar_pointwiseinput_table)) * dst_positive_scale_scalar_pointwiseinput_table)) /\ exists ff_q_pvs_scalar_pointwiseinput_tableentrypositive. dst_positive_code_scalar_pointwiseinput_table = ff_q_pvs_scalar_pointwiseinput_tableentrypositive * S ((S (dst_index_scalar_pointwiseinput_table)) * dst_positive_scale_scalar_pointwiseinput_table) + (dst_positive_scalar_pointwiseinput_table))) /\ (((((exists ff_h_pvs_scalar_pointwiseinput_tableentrynegative. ff_h_pvs_scalar_pointwiseinput_tableentrynegative + S (dst_negative_scalar_pointwiseinput_table) = S ((S (dst_index_scalar_pointwiseinput_table)) * dst_negative_scale_scalar_pointwiseinput_table)) /\ exists ff_q_pvs_scalar_pointwiseinput_tableentrynegative. dst_negative_code_scalar_pointwiseinput_table = ff_q_pvs_scalar_pointwiseinput_tableentrynegative * S ((S (dst_index_scalar_pointwiseinput_table)) * dst_negative_scale_scalar_pointwiseinput_table) + (dst_negative_scalar_pointwiseinput_table))) /\ (exists ge_balance_positive_scalar_pointwiseinput_tableentryvalue ge_balance_negative_scalar_pointwiseinput_tableentryvalue. (((((dst_value_scalar_pointwiseinput_table) = 2 * (ge_balance_positive_scalar_pointwiseinput_tableentryvalue) /\ (ge_balance_negative_scalar_pointwiseinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_pointwiseinput_tableentryvaluedecode. (((dst_value_scalar_pointwiseinput_table) = 2 * ge_signed_half_scalar_pointwiseinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_pointwiseinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_pointwiseinput_tableentryvalue) = S ge_signed_half_scalar_pointwiseinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_pointwiseinput_table) + ge_balance_negative_scalar_pointwiseinput_tableentryvalue = (dst_negative_scalar_pointwiseinput_table) + ge_balance_positive_scalar_pointwiseinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_pointwiseoutput_table dst_positive_scale_scalar_pointwiseoutput_table dst_negative_code_scalar_pointwiseoutput_table dst_negative_scale_scalar_pointwiseoutput_table. (((G) = (((((dst_positive_code_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table)) * S ((dst_positive_code_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table)) + ((dst_positive_scale_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table))) + (((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) * S ((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) + ((dst_negative_scale_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)))) * S ((((dst_positive_code_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table)) * S ((dst_positive_code_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table)) + ((dst_positive_scale_scalar_pointwiseoutput_table) + (dst_positive_scale_scalar_pointwiseoutput_table))) + (((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) * S ((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) + ((dst_negative_scale_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)))) + ((((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) * S ((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) + ((dst_negative_scale_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table))) + (((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) * S ((dst_negative_code_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)) + ((dst_negative_scale_scalar_pointwiseoutput_table) + (dst_negative_scale_scalar_pointwiseoutput_table)))))) /\ (forall dst_index_scalar_pointwiseoutput_table. (exists pvs_le_gap_scalar_pointwiseoutput_tabledomain. pvs_le_gap_scalar_pointwiseoutput_tabledomain + (dst_index_scalar_pointwiseoutput_table) = (l)) -> exists dst_positive_scalar_pointwiseoutput_table dst_negative_scalar_pointwiseoutput_table dst_value_scalar_pointwiseoutput_table. ((((exists ff_h_pvs_scalar_pointwiseoutput_tableentrypositive. ff_h_pvs_scalar_pointwiseoutput_tableentrypositive + S (dst_positive_scalar_pointwiseoutput_table) = S ((S (dst_index_scalar_pointwiseoutput_table)) * dst_positive_scale_scalar_pointwiseoutput_table)) /\ exists ff_q_pvs_scalar_pointwiseoutput_tableentrypositive. dst_positive_code_scalar_pointwiseoutput_table = ff_q_pvs_scalar_pointwiseoutput_tableentrypositive * S ((S (dst_index_scalar_pointwiseoutput_table)) * dst_positive_scale_scalar_pointwiseoutput_table) + (dst_positive_scalar_pointwiseoutput_table))) /\ (((((exists ff_h_pvs_scalar_pointwiseoutput_tableentrynegative. ff_h_pvs_scalar_pointwiseoutput_tableentrynegative + S (dst_negative_scalar_pointwiseoutput_table) = S ((S (dst_index_scalar_pointwiseoutput_table)) * dst_negative_scale_scalar_pointwiseoutput_table)) /\ exists ff_q_pvs_scalar_pointwiseoutput_tableentrynegative. dst_negative_code_scalar_pointwiseoutput_table = ff_q_pvs_scalar_pointwiseoutput_tableentrynegative * S ((S (dst_index_scalar_pointwiseoutput_table)) * dst_negative_scale_scalar_pointwiseoutput_table) + (dst_negative_scalar_pointwiseoutput_table))) /\ (exists ge_balance_positive_scalar_pointwiseoutput_tableentryvalue ge_balance_negative_scalar_pointwiseoutput_tableentryvalue. (((((dst_value_scalar_pointwiseoutput_table) = 2 * (ge_balance_positive_scalar_pointwiseoutput_tableentryvalue) /\ (ge_balance_negative_scalar_pointwiseoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_pointwiseoutput_tableentryvaluedecode. (((dst_value_scalar_pointwiseoutput_table) = 2 * ge_signed_half_scalar_pointwiseoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_pointwiseoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_pointwiseoutput_tableentryvalue) = S ge_signed_half_scalar_pointwiseoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_pointwiseoutput_table) + ge_balance_negative_scalar_pointwiseoutput_tableentryvalue = (dst_negative_scalar_pointwiseoutput_table) + ge_balance_positive_scalar_pointwiseoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_pointwiseentries. (exists pvs_gap_scalar_pointwiseentriesbound. pvs_gap_scalar_pointwiseentriesbound + S (sto_index_scalar_pointwiseentries) = (l)) -> exists sto_input_scalar_pointwiseentries sto_output_scalar_pointwiseentries. ((exists dst_positive_code_scalar_pointwiseentriesentryinput dst_positive_scale_scalar_pointwiseentriesentryinput dst_negative_code_scalar_pointwiseentriesentryinput dst_negative_scale_scalar_pointwiseentriesentryinput dst_positive_scalar_pointwiseentriesentryinput dst_negative_scalar_pointwiseentriesentryinput. (((F) = (((((dst_positive_code_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput)) * S ((dst_positive_code_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput)) + ((dst_positive_scale_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput))) + (((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) * S ((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) + ((dst_negative_scale_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)))) * S ((((dst_positive_code_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput)) * S ((dst_positive_code_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput)) + ((dst_positive_scale_scalar_pointwiseentriesentryinput) + (dst_positive_scale_scalar_pointwiseentriesentryinput))) + (((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) * S ((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) + ((dst_negative_scale_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)))) + ((((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) * S ((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) + ((dst_negative_scale_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput))) + (((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) * S ((dst_negative_code_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)) + ((dst_negative_scale_scalar_pointwiseentriesentryinput) + (dst_negative_scale_scalar_pointwiseentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_pointwiseentriesentryinputpositive. ff_h_pvs_scalar_pointwiseentriesentryinputpositive + S (dst_positive_scalar_pointwiseentriesentryinput) = S ((S (sto_index_scalar_pointwiseentries)) * dst_positive_scale_scalar_pointwiseentriesentryinput)) /\ exists ff_q_pvs_scalar_pointwiseentriesentryinputpositive. dst_positive_code_scalar_pointwiseentriesentryinput = ff_q_pvs_scalar_pointwiseentriesentryinputpositive * S ((S (sto_index_scalar_pointwiseentries)) * dst_positive_scale_scalar_pointwiseentriesentryinput) + (dst_positive_scalar_pointwiseentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_pointwiseentriesentryinputnegative. ff_h_pvs_scalar_pointwiseentriesentryinputnegative + S (dst_negative_scalar_pointwiseentriesentryinput) = S ((S (sto_index_scalar_pointwiseentries)) * dst_negative_scale_scalar_pointwiseentriesentryinput)) /\ exists ff_q_pvs_scalar_pointwiseentriesentryinputnegative. dst_negative_code_scalar_pointwiseentriesentryinput = ff_q_pvs_scalar_pointwiseentriesentryinputnegative * S ((S (sto_index_scalar_pointwiseentries)) * dst_negative_scale_scalar_pointwiseentriesentryinput) + (dst_negative_scalar_pointwiseentriesentryinput))) /\ (exists ge_balance_positive_scalar_pointwiseentriesentryinputvalue ge_balance_negative_scalar_pointwiseentriesentryinputvalue. (((((sto_input_scalar_pointwiseentries) = 2 * (ge_balance_positive_scalar_pointwiseentriesentryinputvalue) /\ (ge_balance_negative_scalar_pointwiseentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_pointwiseentriesentryinputvaluedecode. (((sto_input_scalar_pointwiseentries) = 2 * ge_signed_half_scalar_pointwiseentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_pointwiseentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_pointwiseentriesentryinputvalue) = S ge_signed_half_scalar_pointwiseentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_pointwiseentriesentryinput) + ge_balance_negative_scalar_pointwiseentriesentryinputvalue = (dst_negative_scalar_pointwiseentriesentryinput) + ge_balance_positive_scalar_pointwiseentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_pointwiseentriesentryoutput dst_positive_scale_scalar_pointwiseentriesentryoutput dst_negative_code_scalar_pointwiseentriesentryoutput dst_negative_scale_scalar_pointwiseentriesentryoutput dst_positive_scalar_pointwiseentriesentryoutput dst_negative_scalar_pointwiseentriesentryoutput. (((G) = (((((dst_positive_code_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_positive_code_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput)) + ((dst_positive_scale_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput))) + (((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) + ((dst_negative_scale_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)))) * S ((((dst_positive_code_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_positive_code_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput)) + ((dst_positive_scale_scalar_pointwiseentriesentryoutput) + (dst_positive_scale_scalar_pointwiseentriesentryoutput))) + (((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) + ((dst_negative_scale_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)))) + ((((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) + ((dst_negative_scale_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput))) + (((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) * S ((dst_negative_code_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)) + ((dst_negative_scale_scalar_pointwiseentriesentryoutput) + (dst_negative_scale_scalar_pointwiseentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_pointwiseentriesentryoutputpositive. ff_h_pvs_scalar_pointwiseentriesentryoutputpositive + S (dst_positive_scalar_pointwiseentriesentryoutput) = S ((S (sto_index_scalar_pointwiseentries)) * dst_positive_scale_scalar_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_scalar_pointwiseentriesentryoutputpositive. dst_positive_code_scalar_pointwiseentriesentryoutput = ff_q_pvs_scalar_pointwiseentriesentryoutputpositive * S ((S (sto_index_scalar_pointwiseentries)) * dst_positive_scale_scalar_pointwiseentriesentryoutput) + (dst_positive_scalar_pointwiseentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_pointwiseentriesentryoutputnegative. ff_h_pvs_scalar_pointwiseentriesentryoutputnegative + S (dst_negative_scalar_pointwiseentriesentryoutput) = S ((S (sto_index_scalar_pointwiseentries)) * dst_negative_scale_scalar_pointwiseentriesentryoutput)) /\ exists ff_q_pvs_scalar_pointwiseentriesentryoutputnegative. dst_negative_code_scalar_pointwiseentriesentryoutput = ff_q_pvs_scalar_pointwiseentriesentryoutputnegative * S ((S (sto_index_scalar_pointwiseentries)) * dst_negative_scale_scalar_pointwiseentriesentryoutput) + (dst_negative_scalar_pointwiseentriesentryoutput))) /\ (exists ge_balance_positive_scalar_pointwiseentriesentryoutputvalue ge_balance_negative_scalar_pointwiseentriesentryoutputvalue. (((((sto_output_scalar_pointwiseentries) = 2 * (ge_balance_positive_scalar_pointwiseentriesentryoutputvalue) /\ (ge_balance_negative_scalar_pointwiseentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_pointwiseentriesentryoutputvaluedecode. (((sto_output_scalar_pointwiseentries) = 2 * ge_signed_half_scalar_pointwiseentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_pointwiseentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_pointwiseentriesentryoutputvalue) = S ge_signed_half_scalar_pointwiseentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_pointwiseentriesentryoutput) + ge_balance_negative_scalar_pointwiseentriesentryoutputvalue = (dst_negative_scalar_pointwiseentriesentryoutput) + ge_balance_positive_scalar_pointwiseentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_pointwiseentriesentryoperation sto_an_scalar_pointwiseentriesentryoperation sto_bp_scalar_pointwiseentriesentryoperation sto_bn_scalar_pointwiseentriesentryoperation sto_cp_scalar_pointwiseentriesentryoperation sto_cn_scalar_pointwiseentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_pointwiseentriesentryoperation) /\ (sto_an_scalar_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_pointwiseentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_pointwiseentriesentryoperationleft + 1 /\ (sto_ap_scalar_pointwiseentriesentryoperation) = 0) /\ (sto_an_scalar_pointwiseentriesentryoperation) = S ge_signed_half_scalar_pointwiseentriesentryoperationleft))) /\ ((((((sto_input_scalar_pointwiseentries) = 2 * (sto_bp_scalar_pointwiseentriesentryoperation) /\ (sto_bn_scalar_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_pointwiseentriesentryoperationright. (((sto_input_scalar_pointwiseentries) = 2 * ge_signed_half_scalar_pointwiseentriesentryoperationright + 1 /\ (sto_bp_scalar_pointwiseentriesentryoperation) = 0) /\ (sto_bn_scalar_pointwiseentriesentryoperation) = S ge_signed_half_scalar_pointwiseentriesentryoperationright))) /\ ((((((sto_output_scalar_pointwiseentries) = 2 * (sto_cp_scalar_pointwiseentriesentryoperation) /\ (sto_cn_scalar_pointwiseentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_pointwiseentriesentryoperationoutput. (((sto_output_scalar_pointwiseentries) = 2 * ge_signed_half_scalar_pointwiseentriesentryoperationoutput + 1 /\ (sto_cp_scalar_pointwiseentriesentryoperation) = 0) /\ (sto_cn_scalar_pointwiseentriesentryoperation) = S ge_signed_half_scalar_pointwiseentriesentryoperationoutput))) /\ ((sto_ap_scalar_pointwiseentriesentryoperation * sto_bp_scalar_pointwiseentriesentryoperation + sto_an_scalar_pointwiseentriesentryoperation * sto_bn_scalar_pointwiseentriesentryoperation) + sto_cn_scalar_pointwiseentriesentryoperation = (sto_ap_scalar_pointwiseentriesentryoperation * sto_bn_scalar_pointwiseentriesentryoperation + sto_an_scalar_pointwiseentriesentryoperation * sto_bp_scalar_pointwiseentriesentryoperation) + sto_cp_scalar_pointwiseentriesentryoperation))))))))))))))) -> (exists dst_positive_code_scalar_source_sum dst_positive_scale_scalar_source_sum dst_negative_code_scalar_source_sum dst_negative_scale_scalar_source_sum dst_positive_sum_scalar_source_sum dst_negative_sum_scalar_source_sum. (((F) = (((((dst_positive_code_scalar_source_sum) + (dst_positive_scale_scalar_source_sum)) * S ((dst_positive_code_scalar_source_sum) + (dst_positive_scale_scalar_source_sum)) + ((dst_positive_scale_scalar_source_sum) + (dst_positive_scale_scalar_source_sum))) + (((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) * S ((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) + ((dst_negative_scale_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)))) * S ((((dst_positive_code_scalar_source_sum) + (dst_positive_scale_scalar_source_sum)) * S ((dst_positive_code_scalar_source_sum) + (dst_positive_scale_scalar_source_sum)) + ((dst_positive_scale_scalar_source_sum) + (dst_positive_scale_scalar_source_sum))) + (((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) * S ((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) + ((dst_negative_scale_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)))) + ((((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) * S ((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) + ((dst_negative_scale_scalar_source_sum) + (dst_negative_scale_scalar_source_sum))) + (((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) * S ((dst_negative_code_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)) + ((dst_negative_scale_scalar_source_sum) + (dst_negative_scale_scalar_source_sum)))))) /\ (((exists fs_u_dst_scalar_source_sumpositive fs_v_dst_scalar_source_sumpositive. ((((exists fs_h_dst_scalar_source_sumpositive_body_start. fs_h_dst_scalar_source_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_scalar_source_sumpositive)) /\ exists fs_q_dst_scalar_source_sumpositive_body_start. fs_u_dst_scalar_source_sumpositive = fs_q_dst_scalar_source_sumpositive_body_start * S ((S (0)) * fs_v_dst_scalar_source_sumpositive) + (0))) /\ ((((exists fs_h_dst_scalar_source_sumpositive_body_terminal. fs_h_dst_scalar_source_sumpositive_body_terminal + S (dst_positive_sum_scalar_source_sum) = S ((S (l)) * fs_v_dst_scalar_source_sumpositive)) /\ exists fs_q_dst_scalar_source_sumpositive_body_terminal. fs_u_dst_scalar_source_sumpositive = fs_q_dst_scalar_source_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_scalar_source_sumpositive) + (dst_positive_sum_scalar_source_sum))) /\ forall fs_i_dst_scalar_source_sumpositive_body_steps. (exists fs_lt_dst_scalar_source_sumpositive_body_steps_bound. fs_lt_dst_scalar_source_sumpositive_body_steps_bound + S fs_i_dst_scalar_source_sumpositive_body_steps = l) -> exists fs_a_dst_scalar_source_sumpositive_body_steps fs_r_dst_scalar_source_sumpositive_body_steps fs_s_dst_scalar_source_sumpositive_body_steps. ((((exists fs_h_dst_scalar_source_sumpositive_body_steps_summand. fs_h_dst_scalar_source_sumpositive_body_steps_summand + S (fs_a_dst_scalar_source_sumpositive_body_steps) = S ((S (fs_i_dst_scalar_source_sumpositive_body_steps)) * dst_positive_scale_scalar_source_sum)) /\ exists fs_q_dst_scalar_source_sumpositive_body_steps_summand. dst_positive_code_scalar_source_sum = fs_q_dst_scalar_source_sumpositive_body_steps_summand * S ((S (fs_i_dst_scalar_source_sumpositive_body_steps)) * dst_positive_scale_scalar_source_sum) + (fs_a_dst_scalar_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_scalar_source_sumpositive_body_steps_partial. fs_h_dst_scalar_source_sumpositive_body_steps_partial + S (fs_r_dst_scalar_source_sumpositive_body_steps) = S ((S (fs_i_dst_scalar_source_sumpositive_body_steps)) * fs_v_dst_scalar_source_sumpositive)) /\ exists fs_q_dst_scalar_source_sumpositive_body_steps_partial. fs_u_dst_scalar_source_sumpositive = fs_q_dst_scalar_source_sumpositive_body_steps_partial * S ((S (fs_i_dst_scalar_source_sumpositive_body_steps)) * fs_v_dst_scalar_source_sumpositive) + (fs_r_dst_scalar_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_scalar_source_sumpositive_body_steps_successor. fs_h_dst_scalar_source_sumpositive_body_steps_successor + S (fs_s_dst_scalar_source_sumpositive_body_steps) = S ((S (S fs_i_dst_scalar_source_sumpositive_body_steps)) * fs_v_dst_scalar_source_sumpositive)) /\ exists fs_q_dst_scalar_source_sumpositive_body_steps_successor. fs_u_dst_scalar_source_sumpositive = fs_q_dst_scalar_source_sumpositive_body_steps_successor * S ((S (S fs_i_dst_scalar_source_sumpositive_body_steps)) * fs_v_dst_scalar_source_sumpositive) + (fs_s_dst_scalar_source_sumpositive_body_steps))) /\ fs_s_dst_scalar_source_sumpositive_body_steps = fs_r_dst_scalar_source_sumpositive_body_steps + fs_a_dst_scalar_source_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_scalar_source_sumnegative fs_v_dst_scalar_source_sumnegative. ((((exists fs_h_dst_scalar_source_sumnegative_body_start. fs_h_dst_scalar_source_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_scalar_source_sumnegative)) /\ exists fs_q_dst_scalar_source_sumnegative_body_start. fs_u_dst_scalar_source_sumnegative = fs_q_dst_scalar_source_sumnegative_body_start * S ((S (0)) * fs_v_dst_scalar_source_sumnegative) + (0))) /\ ((((exists fs_h_dst_scalar_source_sumnegative_body_terminal. fs_h_dst_scalar_source_sumnegative_body_terminal + S (dst_negative_sum_scalar_source_sum) = S ((S (l)) * fs_v_dst_scalar_source_sumnegative)) /\ exists fs_q_dst_scalar_source_sumnegative_body_terminal. fs_u_dst_scalar_source_sumnegative = fs_q_dst_scalar_source_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_scalar_source_sumnegative) + (dst_negative_sum_scalar_source_sum))) /\ forall fs_i_dst_scalar_source_sumnegative_body_steps. (exists fs_lt_dst_scalar_source_sumnegative_body_steps_bound. fs_lt_dst_scalar_source_sumnegative_body_steps_bound + S fs_i_dst_scalar_source_sumnegative_body_steps = l) -> exists fs_a_dst_scalar_source_sumnegative_body_steps fs_r_dst_scalar_source_sumnegative_body_steps fs_s_dst_scalar_source_sumnegative_body_steps. ((((exists fs_h_dst_scalar_source_sumnegative_body_steps_summand. fs_h_dst_scalar_source_sumnegative_body_steps_summand + S (fs_a_dst_scalar_source_sumnegative_body_steps) = S ((S (fs_i_dst_scalar_source_sumnegative_body_steps)) * dst_negative_scale_scalar_source_sum)) /\ exists fs_q_dst_scalar_source_sumnegative_body_steps_summand. dst_negative_code_scalar_source_sum = fs_q_dst_scalar_source_sumnegative_body_steps_summand * S ((S (fs_i_dst_scalar_source_sumnegative_body_steps)) * dst_negative_scale_scalar_source_sum) + (fs_a_dst_scalar_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_scalar_source_sumnegative_body_steps_partial. fs_h_dst_scalar_source_sumnegative_body_steps_partial + S (fs_r_dst_scalar_source_sumnegative_body_steps) = S ((S (fs_i_dst_scalar_source_sumnegative_body_steps)) * fs_v_dst_scalar_source_sumnegative)) /\ exists fs_q_dst_scalar_source_sumnegative_body_steps_partial. fs_u_dst_scalar_source_sumnegative = fs_q_dst_scalar_source_sumnegative_body_steps_partial * S ((S (fs_i_dst_scalar_source_sumnegative_body_steps)) * fs_v_dst_scalar_source_sumnegative) + (fs_r_dst_scalar_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_scalar_source_sumnegative_body_steps_successor. fs_h_dst_scalar_source_sumnegative_body_steps_successor + S (fs_s_dst_scalar_source_sumnegative_body_steps) = S ((S (S fs_i_dst_scalar_source_sumnegative_body_steps)) * fs_v_dst_scalar_source_sumnegative)) /\ exists fs_q_dst_scalar_source_sumnegative_body_steps_successor. fs_u_dst_scalar_source_sumnegative = fs_q_dst_scalar_source_sumnegative_body_steps_successor * S ((S (S fs_i_dst_scalar_source_sumnegative_body_steps)) * fs_v_dst_scalar_source_sumnegative) + (fs_s_dst_scalar_source_sumnegative_body_steps))) /\ fs_s_dst_scalar_source_sumnegative_body_steps = fs_r_dst_scalar_source_sumnegative_body_steps + fs_a_dst_scalar_source_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_scalar_source_sumresult ge_balance_negative_scalar_source_sumresult. (((((b) = 2 * (ge_balance_positive_scalar_source_sumresult) /\ (ge_balance_negative_scalar_source_sumresult) = 0) \/ exists ge_signed_half_scalar_source_sumresultdecode. (((b) = 2 * ge_signed_half_scalar_source_sumresultdecode + 1 /\ (ge_balance_positive_scalar_source_sumresult) = 0) /\ (ge_balance_negative_scalar_source_sumresult) = S ge_signed_half_scalar_source_sumresultdecode))) /\ ((dst_positive_sum_scalar_source_sum) + ge_balance_negative_scalar_source_sumresult = (dst_negative_sum_scalar_source_sum) + ge_balance_positive_scalar_source_sumresult))))))))) -> (exists dst_positive_code_scalar_output_sum dst_positive_scale_scalar_output_sum dst_negative_code_scalar_output_sum dst_negative_scale_scalar_output_sum dst_positive_sum_scalar_output_sum dst_negative_sum_scalar_output_sum. (((G) = (((((dst_positive_code_scalar_output_sum) + (dst_positive_scale_scalar_output_sum)) * S ((dst_positive_code_scalar_output_sum) + (dst_positive_scale_scalar_output_sum)) + ((dst_positive_scale_scalar_output_sum) + (dst_positive_scale_scalar_output_sum))) + (((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) * S ((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) + ((dst_negative_scale_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)))) * S ((((dst_positive_code_scalar_output_sum) + (dst_positive_scale_scalar_output_sum)) * S ((dst_positive_code_scalar_output_sum) + (dst_positive_scale_scalar_output_sum)) + ((dst_positive_scale_scalar_output_sum) + (dst_positive_scale_scalar_output_sum))) + (((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) * S ((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) + ((dst_negative_scale_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)))) + ((((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) * S ((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) + ((dst_negative_scale_scalar_output_sum) + (dst_negative_scale_scalar_output_sum))) + (((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) * S ((dst_negative_code_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)) + ((dst_negative_scale_scalar_output_sum) + (dst_negative_scale_scalar_output_sum)))))) /\ (((exists fs_u_dst_scalar_output_sumpositive fs_v_dst_scalar_output_sumpositive. ((((exists fs_h_dst_scalar_output_sumpositive_body_start. fs_h_dst_scalar_output_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_scalar_output_sumpositive)) /\ exists fs_q_dst_scalar_output_sumpositive_body_start. fs_u_dst_scalar_output_sumpositive = fs_q_dst_scalar_output_sumpositive_body_start * S ((S (0)) * fs_v_dst_scalar_output_sumpositive) + (0))) /\ ((((exists fs_h_dst_scalar_output_sumpositive_body_terminal. fs_h_dst_scalar_output_sumpositive_body_terminal + S (dst_positive_sum_scalar_output_sum) = S ((S (l)) * fs_v_dst_scalar_output_sumpositive)) /\ exists fs_q_dst_scalar_output_sumpositive_body_terminal. fs_u_dst_scalar_output_sumpositive = fs_q_dst_scalar_output_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_scalar_output_sumpositive) + (dst_positive_sum_scalar_output_sum))) /\ forall fs_i_dst_scalar_output_sumpositive_body_steps. (exists fs_lt_dst_scalar_output_sumpositive_body_steps_bound. fs_lt_dst_scalar_output_sumpositive_body_steps_bound + S fs_i_dst_scalar_output_sumpositive_body_steps = l) -> exists fs_a_dst_scalar_output_sumpositive_body_steps fs_r_dst_scalar_output_sumpositive_body_steps fs_s_dst_scalar_output_sumpositive_body_steps. ((((exists fs_h_dst_scalar_output_sumpositive_body_steps_summand. fs_h_dst_scalar_output_sumpositive_body_steps_summand + S (fs_a_dst_scalar_output_sumpositive_body_steps) = S ((S (fs_i_dst_scalar_output_sumpositive_body_steps)) * dst_positive_scale_scalar_output_sum)) /\ exists fs_q_dst_scalar_output_sumpositive_body_steps_summand. dst_positive_code_scalar_output_sum = fs_q_dst_scalar_output_sumpositive_body_steps_summand * S ((S (fs_i_dst_scalar_output_sumpositive_body_steps)) * dst_positive_scale_scalar_output_sum) + (fs_a_dst_scalar_output_sumpositive_body_steps))) /\ ((((exists fs_h_dst_scalar_output_sumpositive_body_steps_partial. fs_h_dst_scalar_output_sumpositive_body_steps_partial + S (fs_r_dst_scalar_output_sumpositive_body_steps) = S ((S (fs_i_dst_scalar_output_sumpositive_body_steps)) * fs_v_dst_scalar_output_sumpositive)) /\ exists fs_q_dst_scalar_output_sumpositive_body_steps_partial. fs_u_dst_scalar_output_sumpositive = fs_q_dst_scalar_output_sumpositive_body_steps_partial * S ((S (fs_i_dst_scalar_output_sumpositive_body_steps)) * fs_v_dst_scalar_output_sumpositive) + (fs_r_dst_scalar_output_sumpositive_body_steps))) /\ ((((exists fs_h_dst_scalar_output_sumpositive_body_steps_successor. fs_h_dst_scalar_output_sumpositive_body_steps_successor + S (fs_s_dst_scalar_output_sumpositive_body_steps) = S ((S (S fs_i_dst_scalar_output_sumpositive_body_steps)) * fs_v_dst_scalar_output_sumpositive)) /\ exists fs_q_dst_scalar_output_sumpositive_body_steps_successor. fs_u_dst_scalar_output_sumpositive = fs_q_dst_scalar_output_sumpositive_body_steps_successor * S ((S (S fs_i_dst_scalar_output_sumpositive_body_steps)) * fs_v_dst_scalar_output_sumpositive) + (fs_s_dst_scalar_output_sumpositive_body_steps))) /\ fs_s_dst_scalar_output_sumpositive_body_steps = fs_r_dst_scalar_output_sumpositive_body_steps + fs_a_dst_scalar_output_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_scalar_output_sumnegative fs_v_dst_scalar_output_sumnegative. ((((exists fs_h_dst_scalar_output_sumnegative_body_start. fs_h_dst_scalar_output_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_scalar_output_sumnegative)) /\ exists fs_q_dst_scalar_output_sumnegative_body_start. fs_u_dst_scalar_output_sumnegative = fs_q_dst_scalar_output_sumnegative_body_start * S ((S (0)) * fs_v_dst_scalar_output_sumnegative) + (0))) /\ ((((exists fs_h_dst_scalar_output_sumnegative_body_terminal. fs_h_dst_scalar_output_sumnegative_body_terminal + S (dst_negative_sum_scalar_output_sum) = S ((S (l)) * fs_v_dst_scalar_output_sumnegative)) /\ exists fs_q_dst_scalar_output_sumnegative_body_terminal. fs_u_dst_scalar_output_sumnegative = fs_q_dst_scalar_output_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_scalar_output_sumnegative) + (dst_negative_sum_scalar_output_sum))) /\ forall fs_i_dst_scalar_output_sumnegative_body_steps. (exists fs_lt_dst_scalar_output_sumnegative_body_steps_bound. fs_lt_dst_scalar_output_sumnegative_body_steps_bound + S fs_i_dst_scalar_output_sumnegative_body_steps = l) -> exists fs_a_dst_scalar_output_sumnegative_body_steps fs_r_dst_scalar_output_sumnegative_body_steps fs_s_dst_scalar_output_sumnegative_body_steps. ((((exists fs_h_dst_scalar_output_sumnegative_body_steps_summand. fs_h_dst_scalar_output_sumnegative_body_steps_summand + S (fs_a_dst_scalar_output_sumnegative_body_steps) = S ((S (fs_i_dst_scalar_output_sumnegative_body_steps)) * dst_negative_scale_scalar_output_sum)) /\ exists fs_q_dst_scalar_output_sumnegative_body_steps_summand. dst_negative_code_scalar_output_sum = fs_q_dst_scalar_output_sumnegative_body_steps_summand * S ((S (fs_i_dst_scalar_output_sumnegative_body_steps)) * dst_negative_scale_scalar_output_sum) + (fs_a_dst_scalar_output_sumnegative_body_steps))) /\ ((((exists fs_h_dst_scalar_output_sumnegative_body_steps_partial. fs_h_dst_scalar_output_sumnegative_body_steps_partial + S (fs_r_dst_scalar_output_sumnegative_body_steps) = S ((S (fs_i_dst_scalar_output_sumnegative_body_steps)) * fs_v_dst_scalar_output_sumnegative)) /\ exists fs_q_dst_scalar_output_sumnegative_body_steps_partial. fs_u_dst_scalar_output_sumnegative = fs_q_dst_scalar_output_sumnegative_body_steps_partial * S ((S (fs_i_dst_scalar_output_sumnegative_body_steps)) * fs_v_dst_scalar_output_sumnegative) + (fs_r_dst_scalar_output_sumnegative_body_steps))) /\ ((((exists fs_h_dst_scalar_output_sumnegative_body_steps_successor. fs_h_dst_scalar_output_sumnegative_body_steps_successor + S (fs_s_dst_scalar_output_sumnegative_body_steps) = S ((S (S fs_i_dst_scalar_output_sumnegative_body_steps)) * fs_v_dst_scalar_output_sumnegative)) /\ exists fs_q_dst_scalar_output_sumnegative_body_steps_successor. fs_u_dst_scalar_output_sumnegative = fs_q_dst_scalar_output_sumnegative_body_steps_successor * S ((S (S fs_i_dst_scalar_output_sumnegative_body_steps)) * fs_v_dst_scalar_output_sumnegative) + (fs_s_dst_scalar_output_sumnegative_body_steps))) /\ fs_s_dst_scalar_output_sumnegative_body_steps = fs_r_dst_scalar_output_sumnegative_body_steps + fs_a_dst_scalar_output_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_scalar_output_sumresult ge_balance_negative_scalar_output_sumresult. (((((c) = 2 * (ge_balance_positive_scalar_output_sumresult) /\ (ge_balance_negative_scalar_output_sumresult) = 0) \/ exists ge_signed_half_scalar_output_sumresultdecode. (((c) = 2 * ge_signed_half_scalar_output_sumresultdecode + 1 /\ (ge_balance_positive_scalar_output_sumresult) = 0) /\ (ge_balance_negative_scalar_output_sumresult) = S ge_signed_half_scalar_output_sumresultdecode))) /\ ((dst_positive_sum_scalar_output_sum) + ge_balance_negative_scalar_output_sumresult = (dst_negative_sum_scalar_output_sum) + ge_balance_positive_scalar_output_sumresult))))))))) -> (exists sto_ap_scalar_sum_result sto_an_scalar_sum_result sto_bp_scalar_sum_result sto_bn_scalar_sum_result sto_cp_scalar_sum_result sto_cn_scalar_sum_result. (((((a) = 2 * (sto_ap_scalar_sum_result) /\ (sto_an_scalar_sum_result) = 0) \/ exists ge_signed_half_scalar_sum_resultleft. (((a) = 2 * ge_signed_half_scalar_sum_resultleft + 1 /\ (sto_ap_scalar_sum_result) = 0) /\ (sto_an_scalar_sum_result) = S ge_signed_half_scalar_sum_resultleft))) /\ ((((((b) = 2 * (sto_bp_scalar_sum_result) /\ (sto_bn_scalar_sum_result) = 0) \/ exists ge_signed_half_scalar_sum_resultright. (((b) = 2 * ge_signed_half_scalar_sum_resultright + 1 /\ (sto_bp_scalar_sum_result) = 0) /\ (sto_bn_scalar_sum_result) = S ge_signed_half_scalar_sum_resultright))) /\ ((((((c) = 2 * (sto_cp_scalar_sum_result) /\ (sto_cn_scalar_sum_result) = 0) \/ exists ge_signed_half_scalar_sum_resultoutput. (((c) = 2 * ge_signed_half_scalar_sum_resultoutput + 1 /\ (sto_cp_scalar_sum_result) = 0) /\ (sto_cn_scalar_sum_result) = S ge_signed_half_scalar_sum_resultoutput))) /\ ((sto_ap_scalar_sum_result * sto_bp_scalar_sum_result + sto_an_scalar_sum_result * sto_bn_scalar_sum_result) + sto_cn_scalar_sum_result = (sto_ap_scalar_sum_result * sto_bn_scalar_sum_result + sto_an_scalar_sum_result * sto_bp_scalar_sum_result) + sto_cp_scalar_sum_result)))))))