signed_weighted_sum_scalar_linearity

forall l a W F G b c. (((exists dst_positive_code_weighted_scalar_inputinput_table dst_positive_scale_weighted_scalar_inputinput_table dst_negative_code_weighted_scalar_inputinput_table dst_negative_scale_weighted_scalar_inputinput_table. (((F) = (((((dst_positive_code_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table)) * S ((dst_positive_code_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table)) + ((dst_positive_scale_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table))) + (((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) * S ((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) + ((dst_negative_scale_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)))) * S ((((dst_positive_code_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table)) * S ((dst_positive_code_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table)) + ((dst_positive_scale_weighted_scalar_inputinput_table) + (dst_positive_scale_weighted_scalar_inputinput_table))) + (((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) * S ((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) + ((dst_negative_scale_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)))) + ((((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) * S ((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) + ((dst_negative_scale_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table))) + (((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) * S ((dst_negative_code_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)) + ((dst_negative_scale_weighted_scalar_inputinput_table) + (dst_negative_scale_weighted_scalar_inputinput_table)))))) /\ (forall dst_index_weighted_scalar_inputinput_table. (exists pvs_le_gap_weighted_scalar_inputinput_tabledomain. pvs_le_gap_weighted_scalar_inputinput_tabledomain + (dst_index_weighted_scalar_inputinput_table) = (l)) -> exists dst_positive_weighted_scalar_inputinput_table dst_negative_weighted_scalar_inputinput_table dst_value_weighted_scalar_inputinput_table. ((((exists ff_h_pvs_weighted_scalar_inputinput_tableentrypositive. ff_h_pvs_weighted_scalar_inputinput_tableentrypositive + S (dst_positive_weighted_scalar_inputinput_table) = S ((S (dst_index_weighted_scalar_inputinput_table)) * dst_positive_scale_weighted_scalar_inputinput_table)) /\ exists ff_q_pvs_weighted_scalar_inputinput_tableentrypositive. dst_positive_code_weighted_scalar_inputinput_table = ff_q_pvs_weighted_scalar_inputinput_tableentrypositive * S ((S (dst_index_weighted_scalar_inputinput_table)) * dst_positive_scale_weighted_scalar_inputinput_table) + (dst_positive_weighted_scalar_inputinput_table))) /\ (((((exists ff_h_pvs_weighted_scalar_inputinput_tableentrynegative. ff_h_pvs_weighted_scalar_inputinput_tableentrynegative + S (dst_negative_weighted_scalar_inputinput_table) = S ((S (dst_index_weighted_scalar_inputinput_table)) * dst_negative_scale_weighted_scalar_inputinput_table)) /\ exists ff_q_pvs_weighted_scalar_inputinput_tableentrynegative. dst_negative_code_weighted_scalar_inputinput_table = ff_q_pvs_weighted_scalar_inputinput_tableentrynegative * S ((S (dst_index_weighted_scalar_inputinput_table)) * dst_negative_scale_weighted_scalar_inputinput_table) + (dst_negative_weighted_scalar_inputinput_table))) /\ (exists ge_balance_positive_weighted_scalar_inputinput_tableentryvalue ge_balance_negative_weighted_scalar_inputinput_tableentryvalue. (((((dst_value_weighted_scalar_inputinput_table) = 2 * (ge_balance_positive_weighted_scalar_inputinput_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_inputinput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_inputinput_tableentryvaluedecode. (((dst_value_weighted_scalar_inputinput_table) = 2 * ge_signed_half_weighted_scalar_inputinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_inputinput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_inputinput_tableentryvalue) = S ge_signed_half_weighted_scalar_inputinput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_inputinput_table) + ge_balance_negative_weighted_scalar_inputinput_tableentryvalue = (dst_negative_weighted_scalar_inputinput_table) + ge_balance_positive_weighted_scalar_inputinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_inputoutput_table dst_positive_scale_weighted_scalar_inputoutput_table dst_negative_code_weighted_scalar_inputoutput_table dst_negative_scale_weighted_scalar_inputoutput_table. (((G) = (((((dst_positive_code_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table)) * S ((dst_positive_code_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table)) + ((dst_positive_scale_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table))) + (((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) * S ((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) + ((dst_negative_scale_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)))) * S ((((dst_positive_code_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table)) * S ((dst_positive_code_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table)) + ((dst_positive_scale_weighted_scalar_inputoutput_table) + (dst_positive_scale_weighted_scalar_inputoutput_table))) + (((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) * S ((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) + ((dst_negative_scale_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)))) + ((((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) * S ((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) + ((dst_negative_scale_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table))) + (((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) * S ((dst_negative_code_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)) + ((dst_negative_scale_weighted_scalar_inputoutput_table) + (dst_negative_scale_weighted_scalar_inputoutput_table)))))) /\ (forall dst_index_weighted_scalar_inputoutput_table. (exists pvs_le_gap_weighted_scalar_inputoutput_tabledomain. pvs_le_gap_weighted_scalar_inputoutput_tabledomain + (dst_index_weighted_scalar_inputoutput_table) = (l)) -> exists dst_positive_weighted_scalar_inputoutput_table dst_negative_weighted_scalar_inputoutput_table dst_value_weighted_scalar_inputoutput_table. ((((exists ff_h_pvs_weighted_scalar_inputoutput_tableentrypositive. ff_h_pvs_weighted_scalar_inputoutput_tableentrypositive + S (dst_positive_weighted_scalar_inputoutput_table) = S ((S (dst_index_weighted_scalar_inputoutput_table)) * dst_positive_scale_weighted_scalar_inputoutput_table)) /\ exists ff_q_pvs_weighted_scalar_inputoutput_tableentrypositive. dst_positive_code_weighted_scalar_inputoutput_table = ff_q_pvs_weighted_scalar_inputoutput_tableentrypositive * S ((S (dst_index_weighted_scalar_inputoutput_table)) * dst_positive_scale_weighted_scalar_inputoutput_table) + (dst_positive_weighted_scalar_inputoutput_table))) /\ (((((exists ff_h_pvs_weighted_scalar_inputoutput_tableentrynegative. ff_h_pvs_weighted_scalar_inputoutput_tableentrynegative + S (dst_negative_weighted_scalar_inputoutput_table) = S ((S (dst_index_weighted_scalar_inputoutput_table)) * dst_negative_scale_weighted_scalar_inputoutput_table)) /\ exists ff_q_pvs_weighted_scalar_inputoutput_tableentrynegative. dst_negative_code_weighted_scalar_inputoutput_table = ff_q_pvs_weighted_scalar_inputoutput_tableentrynegative * S ((S (dst_index_weighted_scalar_inputoutput_table)) * dst_negative_scale_weighted_scalar_inputoutput_table) + (dst_negative_weighted_scalar_inputoutput_table))) /\ (exists ge_balance_positive_weighted_scalar_inputoutput_tableentryvalue ge_balance_negative_weighted_scalar_inputoutput_tableentryvalue. (((((dst_value_weighted_scalar_inputoutput_table) = 2 * (ge_balance_positive_weighted_scalar_inputoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_inputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_inputoutput_tableentryvaluedecode. (((dst_value_weighted_scalar_inputoutput_table) = 2 * ge_signed_half_weighted_scalar_inputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_inputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_inputoutput_tableentryvalue) = S ge_signed_half_weighted_scalar_inputoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_inputoutput_table) + ge_balance_negative_weighted_scalar_inputoutput_tableentryvalue = (dst_negative_weighted_scalar_inputoutput_table) + ge_balance_positive_weighted_scalar_inputoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scalar_inputentries. (exists pvs_gap_weighted_scalar_inputentriesbound. pvs_gap_weighted_scalar_inputentriesbound + S (sto_index_weighted_scalar_inputentries) = (l)) -> exists sto_input_weighted_scalar_inputentries sto_output_weighted_scalar_inputentries. ((exists dst_positive_code_weighted_scalar_inputentriesentryinput dst_positive_scale_weighted_scalar_inputentriesentryinput dst_negative_code_weighted_scalar_inputentriesentryinput dst_negative_scale_weighted_scalar_inputentriesentryinput dst_positive_weighted_scalar_inputentriesentryinput dst_negative_weighted_scalar_inputentriesentryinput. (((F) = (((((dst_positive_code_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_positive_code_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput)) + ((dst_positive_scale_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput))) + (((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)))) * S ((((dst_positive_code_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_positive_code_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput)) + ((dst_positive_scale_weighted_scalar_inputentriesentryinput) + (dst_positive_scale_weighted_scalar_inputentriesentryinput))) + (((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)))) + ((((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput))) + (((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryinput) + (dst_negative_scale_weighted_scalar_inputentriesentryinput)))))) /\ (((((exists ff_h_pvs_weighted_scalar_inputentriesentryinputpositive. ff_h_pvs_weighted_scalar_inputentriesentryinputpositive + S (dst_positive_weighted_scalar_inputentriesentryinput) = S ((S (sto_index_weighted_scalar_inputentries)) * dst_positive_scale_weighted_scalar_inputentriesentryinput)) /\ exists ff_q_pvs_weighted_scalar_inputentriesentryinputpositive. dst_positive_code_weighted_scalar_inputentriesentryinput = ff_q_pvs_weighted_scalar_inputentriesentryinputpositive * S ((S (sto_index_weighted_scalar_inputentries)) * dst_positive_scale_weighted_scalar_inputentriesentryinput) + (dst_positive_weighted_scalar_inputentriesentryinput))) /\ (((((exists ff_h_pvs_weighted_scalar_inputentriesentryinputnegative. ff_h_pvs_weighted_scalar_inputentriesentryinputnegative + S (dst_negative_weighted_scalar_inputentriesentryinput) = S ((S (sto_index_weighted_scalar_inputentries)) * dst_negative_scale_weighted_scalar_inputentriesentryinput)) /\ exists ff_q_pvs_weighted_scalar_inputentriesentryinputnegative. dst_negative_code_weighted_scalar_inputentriesentryinput = ff_q_pvs_weighted_scalar_inputentriesentryinputnegative * S ((S (sto_index_weighted_scalar_inputentries)) * dst_negative_scale_weighted_scalar_inputentriesentryinput) + (dst_negative_weighted_scalar_inputentriesentryinput))) /\ (exists ge_balance_positive_weighted_scalar_inputentriesentryinputvalue ge_balance_negative_weighted_scalar_inputentriesentryinputvalue. (((((sto_input_weighted_scalar_inputentries) = 2 * (ge_balance_positive_weighted_scalar_inputentriesentryinputvalue) /\ (ge_balance_negative_weighted_scalar_inputentriesentryinputvalue) = 0) \/ exists ge_signed_half_weighted_scalar_inputentriesentryinputvaluedecode. (((sto_input_weighted_scalar_inputentries) = 2 * ge_signed_half_weighted_scalar_inputentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_inputentriesentryinputvalue) = 0) /\ (ge_balance_negative_weighted_scalar_inputentriesentryinputvalue) = S ge_signed_half_weighted_scalar_inputentriesentryinputvaluedecode))) /\ ((dst_positive_weighted_scalar_inputentriesentryinput) + ge_balance_negative_weighted_scalar_inputentriesentryinputvalue = (dst_negative_weighted_scalar_inputentriesentryinput) + ge_balance_positive_weighted_scalar_inputentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_inputentriesentryoutput dst_positive_scale_weighted_scalar_inputentriesentryoutput dst_negative_code_weighted_scalar_inputentriesentryoutput dst_negative_scale_weighted_scalar_inputentriesentryoutput dst_positive_weighted_scalar_inputentriesentryoutput dst_negative_weighted_scalar_inputentriesentryoutput. (((G) = (((((dst_positive_code_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput))) + (((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)))) * S ((((dst_positive_code_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_inputentriesentryoutput) + (dst_positive_scale_weighted_scalar_inputentriesentryoutput))) + (((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)))) + ((((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput))) + (((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_inputentriesentryoutput) + (dst_negative_scale_weighted_scalar_inputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scalar_inputentriesentryoutputpositive. ff_h_pvs_weighted_scalar_inputentriesentryoutputpositive + S (dst_positive_weighted_scalar_inputentriesentryoutput) = S ((S (sto_index_weighted_scalar_inputentries)) * dst_positive_scale_weighted_scalar_inputentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_inputentriesentryoutputpositive. dst_positive_code_weighted_scalar_inputentriesentryoutput = ff_q_pvs_weighted_scalar_inputentriesentryoutputpositive * S ((S (sto_index_weighted_scalar_inputentries)) * dst_positive_scale_weighted_scalar_inputentriesentryoutput) + (dst_positive_weighted_scalar_inputentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scalar_inputentriesentryoutputnegative. ff_h_pvs_weighted_scalar_inputentriesentryoutputnegative + S (dst_negative_weighted_scalar_inputentriesentryoutput) = S ((S (sto_index_weighted_scalar_inputentries)) * dst_negative_scale_weighted_scalar_inputentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_inputentriesentryoutputnegative. dst_negative_code_weighted_scalar_inputentriesentryoutput = ff_q_pvs_weighted_scalar_inputentriesentryoutputnegative * S ((S (sto_index_weighted_scalar_inputentries)) * dst_negative_scale_weighted_scalar_inputentriesentryoutput) + (dst_negative_weighted_scalar_inputentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scalar_inputentriesentryoutputvalue ge_balance_negative_weighted_scalar_inputentriesentryoutputvalue. (((((sto_output_weighted_scalar_inputentries) = 2 * (ge_balance_positive_weighted_scalar_inputentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scalar_inputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scalar_inputentriesentryoutputvaluedecode. (((sto_output_weighted_scalar_inputentries) = 2 * ge_signed_half_weighted_scalar_inputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_inputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scalar_inputentriesentryoutputvalue) = S ge_signed_half_weighted_scalar_inputentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scalar_inputentriesentryoutput) + ge_balance_negative_weighted_scalar_inputentriesentryoutputvalue = (dst_negative_weighted_scalar_inputentriesentryoutput) + ge_balance_positive_weighted_scalar_inputentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scalar_inputentriesentryoperation sto_an_weighted_scalar_inputentriesentryoperation sto_bp_weighted_scalar_inputentriesentryoperation sto_bn_weighted_scalar_inputentriesentryoperation sto_cp_weighted_scalar_inputentriesentryoperation sto_cn_weighted_scalar_inputentriesentryoperation. (((((a) = 2 * (sto_ap_weighted_scalar_inputentriesentryoperation) /\ (sto_an_weighted_scalar_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_inputentriesentryoperationleft. (((a) = 2 * ge_signed_half_weighted_scalar_inputentriesentryoperationleft + 1 /\ (sto_ap_weighted_scalar_inputentriesentryoperation) = 0) /\ (sto_an_weighted_scalar_inputentriesentryoperation) = S ge_signed_half_weighted_scalar_inputentriesentryoperationleft))) /\ ((((((sto_input_weighted_scalar_inputentries) = 2 * (sto_bp_weighted_scalar_inputentriesentryoperation) /\ (sto_bn_weighted_scalar_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_inputentriesentryoperationright. (((sto_input_weighted_scalar_inputentries) = 2 * ge_signed_half_weighted_scalar_inputentriesentryoperationright + 1 /\ (sto_bp_weighted_scalar_inputentriesentryoperation) = 0) /\ (sto_bn_weighted_scalar_inputentriesentryoperation) = S ge_signed_half_weighted_scalar_inputentriesentryoperationright))) /\ ((((((sto_output_weighted_scalar_inputentries) = 2 * (sto_cp_weighted_scalar_inputentriesentryoperation) /\ (sto_cn_weighted_scalar_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_inputentriesentryoperationoutput. (((sto_output_weighted_scalar_inputentries) = 2 * ge_signed_half_weighted_scalar_inputentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scalar_inputentriesentryoperation) = 0) /\ (sto_cn_weighted_scalar_inputentriesentryoperation) = S ge_signed_half_weighted_scalar_inputentriesentryoperationoutput))) /\ ((sto_ap_weighted_scalar_inputentriesentryoperation * sto_bp_weighted_scalar_inputentriesentryoperation + sto_an_weighted_scalar_inputentriesentryoperation * sto_bn_weighted_scalar_inputentriesentryoperation) + sto_cn_weighted_scalar_inputentriesentryoperation = (sto_ap_weighted_scalar_inputentriesentryoperation * sto_bn_weighted_scalar_inputentriesentryoperation + sto_an_weighted_scalar_inputentriesentryoperation * sto_bp_weighted_scalar_inputentriesentryoperation) + sto_cp_weighted_scalar_inputentriesentryoperation))))))))))))))) -> (exists sws_product_table_weighted_scalar_first. ((((exists dst_positive_code_weighted_scalar_firstproductsleft_table dst_positive_scale_weighted_scalar_firstproductsleft_table dst_negative_code_weighted_scalar_firstproductsleft_table dst_negative_scale_weighted_scalar_firstproductsleft_table. (((W) = (((((dst_positive_code_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_positive_code_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table)) + ((dst_positive_scale_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table))) + (((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) + ((dst_negative_scale_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)))) * S ((((dst_positive_code_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_positive_code_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table)) + ((dst_positive_scale_weighted_scalar_firstproductsleft_table) + (dst_positive_scale_weighted_scalar_firstproductsleft_table))) + (((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) + ((dst_negative_scale_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)))) + ((((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) + ((dst_negative_scale_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table))) + (((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) * S ((dst_negative_code_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)) + ((dst_negative_scale_weighted_scalar_firstproductsleft_table) + (dst_negative_scale_weighted_scalar_firstproductsleft_table)))))) /\ (forall dst_index_weighted_scalar_firstproductsleft_table. (exists pvs_le_gap_weighted_scalar_firstproductsleft_tabledomain. pvs_le_gap_weighted_scalar_firstproductsleft_tabledomain + (dst_index_weighted_scalar_firstproductsleft_table) = (l)) -> exists dst_positive_weighted_scalar_firstproductsleft_table dst_negative_weighted_scalar_firstproductsleft_table dst_value_weighted_scalar_firstproductsleft_table. ((((exists ff_h_pvs_weighted_scalar_firstproductsleft_tableentrypositive. ff_h_pvs_weighted_scalar_firstproductsleft_tableentrypositive + S (dst_positive_weighted_scalar_firstproductsleft_table) = S ((S (dst_index_weighted_scalar_firstproductsleft_table)) * dst_positive_scale_weighted_scalar_firstproductsleft_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsleft_tableentrypositive. dst_positive_code_weighted_scalar_firstproductsleft_table = ff_q_pvs_weighted_scalar_firstproductsleft_tableentrypositive * S ((S (dst_index_weighted_scalar_firstproductsleft_table)) * dst_positive_scale_weighted_scalar_firstproductsleft_table) + (dst_positive_weighted_scalar_firstproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsleft_tableentrynegative. ff_h_pvs_weighted_scalar_firstproductsleft_tableentrynegative + S (dst_negative_weighted_scalar_firstproductsleft_table) = S ((S (dst_index_weighted_scalar_firstproductsleft_table)) * dst_negative_scale_weighted_scalar_firstproductsleft_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsleft_tableentrynegative. dst_negative_code_weighted_scalar_firstproductsleft_table = ff_q_pvs_weighted_scalar_firstproductsleft_tableentrynegative * S ((S (dst_index_weighted_scalar_firstproductsleft_table)) * dst_negative_scale_weighted_scalar_firstproductsleft_table) + (dst_negative_weighted_scalar_firstproductsleft_table))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsleft_tableentryvalue ge_balance_negative_weighted_scalar_firstproductsleft_tableentryvalue. (((((dst_value_weighted_scalar_firstproductsleft_table) = 2 * (ge_balance_positive_weighted_scalar_firstproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsleft_tableentryvaluedecode. (((dst_value_weighted_scalar_firstproductsleft_table) = 2 * ge_signed_half_weighted_scalar_firstproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsleft_tableentryvalue) = S ge_signed_half_weighted_scalar_firstproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsleft_table) + ge_balance_negative_weighted_scalar_firstproductsleft_tableentryvalue = (dst_negative_weighted_scalar_firstproductsleft_table) + ge_balance_positive_weighted_scalar_firstproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_firstproductsright_table dst_positive_scale_weighted_scalar_firstproductsright_table dst_negative_code_weighted_scalar_firstproductsright_table dst_negative_scale_weighted_scalar_firstproductsright_table. (((F) = (((((dst_positive_code_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table)) * S ((dst_positive_code_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table)) + ((dst_positive_scale_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table))) + (((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) * S ((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) + ((dst_negative_scale_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)))) * S ((((dst_positive_code_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table)) * S ((dst_positive_code_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table)) + ((dst_positive_scale_weighted_scalar_firstproductsright_table) + (dst_positive_scale_weighted_scalar_firstproductsright_table))) + (((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) * S ((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) + ((dst_negative_scale_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)))) + ((((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) * S ((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) + ((dst_negative_scale_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table))) + (((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) * S ((dst_negative_code_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)) + ((dst_negative_scale_weighted_scalar_firstproductsright_table) + (dst_negative_scale_weighted_scalar_firstproductsright_table)))))) /\ (forall dst_index_weighted_scalar_firstproductsright_table. (exists pvs_le_gap_weighted_scalar_firstproductsright_tabledomain. pvs_le_gap_weighted_scalar_firstproductsright_tabledomain + (dst_index_weighted_scalar_firstproductsright_table) = (l)) -> exists dst_positive_weighted_scalar_firstproductsright_table dst_negative_weighted_scalar_firstproductsright_table dst_value_weighted_scalar_firstproductsright_table. ((((exists ff_h_pvs_weighted_scalar_firstproductsright_tableentrypositive. ff_h_pvs_weighted_scalar_firstproductsright_tableentrypositive + S (dst_positive_weighted_scalar_firstproductsright_table) = S ((S (dst_index_weighted_scalar_firstproductsright_table)) * dst_positive_scale_weighted_scalar_firstproductsright_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsright_tableentrypositive. dst_positive_code_weighted_scalar_firstproductsright_table = ff_q_pvs_weighted_scalar_firstproductsright_tableentrypositive * S ((S (dst_index_weighted_scalar_firstproductsright_table)) * dst_positive_scale_weighted_scalar_firstproductsright_table) + (dst_positive_weighted_scalar_firstproductsright_table))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsright_tableentrynegative. ff_h_pvs_weighted_scalar_firstproductsright_tableentrynegative + S (dst_negative_weighted_scalar_firstproductsright_table) = S ((S (dst_index_weighted_scalar_firstproductsright_table)) * dst_negative_scale_weighted_scalar_firstproductsright_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsright_tableentrynegative. dst_negative_code_weighted_scalar_firstproductsright_table = ff_q_pvs_weighted_scalar_firstproductsright_tableentrynegative * S ((S (dst_index_weighted_scalar_firstproductsright_table)) * dst_negative_scale_weighted_scalar_firstproductsright_table) + (dst_negative_weighted_scalar_firstproductsright_table))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsright_tableentryvalue ge_balance_negative_weighted_scalar_firstproductsright_tableentryvalue. (((((dst_value_weighted_scalar_firstproductsright_table) = 2 * (ge_balance_positive_weighted_scalar_firstproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsright_tableentryvaluedecode. (((dst_value_weighted_scalar_firstproductsright_table) = 2 * ge_signed_half_weighted_scalar_firstproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsright_tableentryvalue) = S ge_signed_half_weighted_scalar_firstproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsright_table) + ge_balance_negative_weighted_scalar_firstproductsright_tableentryvalue = (dst_negative_weighted_scalar_firstproductsright_table) + ge_balance_positive_weighted_scalar_firstproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_firstproductsoutput_table dst_positive_scale_weighted_scalar_firstproductsoutput_table dst_negative_code_weighted_scalar_firstproductsoutput_table dst_negative_scale_weighted_scalar_firstproductsoutput_table. (((sws_product_table_weighted_scalar_first) = (((((dst_positive_code_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_positive_code_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_positive_scale_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table))) + (((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)))) * S ((((dst_positive_code_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_positive_code_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_positive_scale_weighted_scalar_firstproductsoutput_table) + (dst_positive_scale_weighted_scalar_firstproductsoutput_table))) + (((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)))) + ((((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table))) + (((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_firstproductsoutput_table) + (dst_negative_scale_weighted_scalar_firstproductsoutput_table)))))) /\ (forall dst_index_weighted_scalar_firstproductsoutput_table. (exists pvs_le_gap_weighted_scalar_firstproductsoutput_tabledomain. pvs_le_gap_weighted_scalar_firstproductsoutput_tabledomain + (dst_index_weighted_scalar_firstproductsoutput_table) = (l)) -> exists dst_positive_weighted_scalar_firstproductsoutput_table dst_negative_weighted_scalar_firstproductsoutput_table dst_value_weighted_scalar_firstproductsoutput_table. ((((exists ff_h_pvs_weighted_scalar_firstproductsoutput_tableentrypositive. ff_h_pvs_weighted_scalar_firstproductsoutput_tableentrypositive + S (dst_positive_weighted_scalar_firstproductsoutput_table) = S ((S (dst_index_weighted_scalar_firstproductsoutput_table)) * dst_positive_scale_weighted_scalar_firstproductsoutput_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsoutput_tableentrypositive. dst_positive_code_weighted_scalar_firstproductsoutput_table = ff_q_pvs_weighted_scalar_firstproductsoutput_tableentrypositive * S ((S (dst_index_weighted_scalar_firstproductsoutput_table)) * dst_positive_scale_weighted_scalar_firstproductsoutput_table) + (dst_positive_weighted_scalar_firstproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsoutput_tableentrynegative. ff_h_pvs_weighted_scalar_firstproductsoutput_tableentrynegative + S (dst_negative_weighted_scalar_firstproductsoutput_table) = S ((S (dst_index_weighted_scalar_firstproductsoutput_table)) * dst_negative_scale_weighted_scalar_firstproductsoutput_table)) /\ exists ff_q_pvs_weighted_scalar_firstproductsoutput_tableentrynegative. dst_negative_code_weighted_scalar_firstproductsoutput_table = ff_q_pvs_weighted_scalar_firstproductsoutput_tableentrynegative * S ((S (dst_index_weighted_scalar_firstproductsoutput_table)) * dst_negative_scale_weighted_scalar_firstproductsoutput_table) + (dst_negative_weighted_scalar_firstproductsoutput_table))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsoutput_tableentryvalue ge_balance_negative_weighted_scalar_firstproductsoutput_tableentryvalue. (((((dst_value_weighted_scalar_firstproductsoutput_table) = 2 * (ge_balance_positive_weighted_scalar_firstproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsoutput_tableentryvaluedecode. (((dst_value_weighted_scalar_firstproductsoutput_table) = 2 * ge_signed_half_weighted_scalar_firstproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsoutput_tableentryvalue) = S ge_signed_half_weighted_scalar_firstproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsoutput_table) + ge_balance_negative_weighted_scalar_firstproductsoutput_tableentryvalue = (dst_negative_weighted_scalar_firstproductsoutput_table) + ge_balance_positive_weighted_scalar_firstproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scalar_firstproductsentries. (exists pvs_gap_weighted_scalar_firstproductsentriesbound. pvs_gap_weighted_scalar_firstproductsentriesbound + S (sto_index_weighted_scalar_firstproductsentries) = (l)) -> exists sto_left_weighted_scalar_firstproductsentries sto_right_weighted_scalar_firstproductsentries sto_output_weighted_scalar_firstproductsentries. ((exists dst_positive_code_weighted_scalar_firstproductsentriesentryleft dst_positive_scale_weighted_scalar_firstproductsentriesentryleft dst_negative_code_weighted_scalar_firstproductsentriesentryleft dst_negative_scale_weighted_scalar_firstproductsentriesentryleft dst_positive_weighted_scalar_firstproductsentriesentryleft dst_negative_weighted_scalar_firstproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)))) + ((((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryleftpositive. ff_h_pvs_weighted_scalar_firstproductsentriesentryleftpositive + S (dst_positive_weighted_scalar_firstproductsentriesentryleft) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryleftpositive. dst_positive_code_weighted_scalar_firstproductsentriesentryleft = ff_q_pvs_weighted_scalar_firstproductsentriesentryleftpositive * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_positive_weighted_scalar_firstproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryleftnegative. ff_h_pvs_weighted_scalar_firstproductsentriesentryleftnegative + S (dst_negative_weighted_scalar_firstproductsentriesentryleft) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryleftnegative. dst_negative_code_weighted_scalar_firstproductsentriesentryleft = ff_q_pvs_weighted_scalar_firstproductsentriesentryleftnegative * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryleft) + (dst_negative_weighted_scalar_firstproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsentriesentryleftvalue ge_balance_negative_weighted_scalar_firstproductsentriesentryleftvalue. (((((sto_left_weighted_scalar_firstproductsentries) = 2 * (ge_balance_positive_weighted_scalar_firstproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryleftvaluedecode. (((sto_left_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryleftvalue) = S ge_signed_half_weighted_scalar_firstproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsentriesentryleft) + ge_balance_negative_weighted_scalar_firstproductsentriesentryleftvalue = (dst_negative_weighted_scalar_firstproductsentriesentryleft) + ge_balance_positive_weighted_scalar_firstproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_firstproductsentriesentryright dst_positive_scale_weighted_scalar_firstproductsentriesentryright dst_negative_code_weighted_scalar_firstproductsentriesentryright dst_negative_scale_weighted_scalar_firstproductsentriesentryright dst_positive_weighted_scalar_firstproductsentriesentryright dst_negative_weighted_scalar_firstproductsentriesentryright. (((F) = (((((dst_positive_code_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)))) * S ((((dst_positive_code_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryright) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)))) + ((((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryright) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryrightpositive. ff_h_pvs_weighted_scalar_firstproductsentriesentryrightpositive + S (dst_positive_weighted_scalar_firstproductsentriesentryright) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryright)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryrightpositive. dst_positive_code_weighted_scalar_firstproductsentriesentryright = ff_q_pvs_weighted_scalar_firstproductsentriesentryrightpositive * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryright) + (dst_positive_weighted_scalar_firstproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryrightnegative. ff_h_pvs_weighted_scalar_firstproductsentriesentryrightnegative + S (dst_negative_weighted_scalar_firstproductsentriesentryright) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryright)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryrightnegative. dst_negative_code_weighted_scalar_firstproductsentriesentryright = ff_q_pvs_weighted_scalar_firstproductsentriesentryrightnegative * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryright) + (dst_negative_weighted_scalar_firstproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsentriesentryrightvalue ge_balance_negative_weighted_scalar_firstproductsentriesentryrightvalue. (((((sto_right_weighted_scalar_firstproductsentries) = 2 * (ge_balance_positive_weighted_scalar_firstproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryrightvaluedecode. (((sto_right_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryrightvalue) = S ge_signed_half_weighted_scalar_firstproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsentriesentryright) + ge_balance_negative_weighted_scalar_firstproductsentriesentryrightvalue = (dst_negative_weighted_scalar_firstproductsentriesentryright) + ge_balance_positive_weighted_scalar_firstproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_firstproductsentriesentryoutput dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput dst_negative_code_weighted_scalar_firstproductsentriesentryoutput dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput dst_positive_weighted_scalar_firstproductsentriesentryoutput dst_negative_weighted_scalar_firstproductsentriesentryoutput. (((sws_product_table_weighted_scalar_first) = (((((dst_positive_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryoutputpositive. ff_h_pvs_weighted_scalar_firstproductsentriesentryoutputpositive + S (dst_positive_weighted_scalar_firstproductsentriesentryoutput) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryoutputpositive. dst_positive_code_weighted_scalar_firstproductsentriesentryoutput = ff_q_pvs_weighted_scalar_firstproductsentriesentryoutputpositive * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_positive_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_positive_weighted_scalar_firstproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scalar_firstproductsentriesentryoutputnegative. ff_h_pvs_weighted_scalar_firstproductsentriesentryoutputnegative + S (dst_negative_weighted_scalar_firstproductsentriesentryoutput) = S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_firstproductsentriesentryoutputnegative. dst_negative_code_weighted_scalar_firstproductsentriesentryoutput = ff_q_pvs_weighted_scalar_firstproductsentriesentryoutputnegative * S ((S (sto_index_weighted_scalar_firstproductsentries)) * dst_negative_scale_weighted_scalar_firstproductsentriesentryoutput) + (dst_negative_weighted_scalar_firstproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scalar_firstproductsentriesentryoutputvalue ge_balance_negative_weighted_scalar_firstproductsentriesentryoutputvalue. (((((sto_output_weighted_scalar_firstproductsentries) = 2 * (ge_balance_positive_weighted_scalar_firstproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryoutputvaluedecode. (((sto_output_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_firstproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scalar_firstproductsentriesentryoutputvalue) = S ge_signed_half_weighted_scalar_firstproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scalar_firstproductsentriesentryoutput) + ge_balance_negative_weighted_scalar_firstproductsentriesentryoutputvalue = (dst_negative_weighted_scalar_firstproductsentriesentryoutput) + ge_balance_positive_weighted_scalar_firstproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scalar_firstproductsentriesentryoperation sto_an_weighted_scalar_firstproductsentriesentryoperation sto_bp_weighted_scalar_firstproductsentriesentryoperation sto_bn_weighted_scalar_firstproductsentriesentryoperation sto_cp_weighted_scalar_firstproductsentriesentryoperation sto_cn_weighted_scalar_firstproductsentriesentryoperation. (((((sto_left_weighted_scalar_firstproductsentries) = 2 * (sto_ap_weighted_scalar_firstproductsentriesentryoperation) /\ (sto_an_weighted_scalar_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryoperationleft. (((sto_left_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_scalar_firstproductsentriesentryoperation) = 0) /\ (sto_an_weighted_scalar_firstproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_firstproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_scalar_firstproductsentries) = 2 * (sto_bp_weighted_scalar_firstproductsentriesentryoperation) /\ (sto_bn_weighted_scalar_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryoperationright. (((sto_right_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_scalar_firstproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_scalar_firstproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_firstproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_scalar_firstproductsentries) = 2 * (sto_cp_weighted_scalar_firstproductsentriesentryoperation) /\ (sto_cn_weighted_scalar_firstproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_firstproductsentriesentryoperationoutput. (((sto_output_weighted_scalar_firstproductsentries) = 2 * ge_signed_half_weighted_scalar_firstproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scalar_firstproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_scalar_firstproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_firstproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_scalar_firstproductsentriesentryoperation * sto_bp_weighted_scalar_firstproductsentriesentryoperation + sto_an_weighted_scalar_firstproductsentriesentryoperation * sto_bn_weighted_scalar_firstproductsentriesentryoperation) + sto_cn_weighted_scalar_firstproductsentriesentryoperation = (sto_ap_weighted_scalar_firstproductsentriesentryoperation * sto_bn_weighted_scalar_firstproductsentriesentryoperation + sto_an_weighted_scalar_firstproductsentriesentryoperation * sto_bp_weighted_scalar_firstproductsentriesentryoperation) + sto_cp_weighted_scalar_firstproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_scalar_firstsum dst_positive_scale_weighted_scalar_firstsum dst_negative_code_weighted_scalar_firstsum dst_negative_scale_weighted_scalar_firstsum dst_positive_sum_weighted_scalar_firstsum dst_negative_sum_weighted_scalar_firstsum. (((sws_product_table_weighted_scalar_first) = (((((dst_positive_code_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum)) * S ((dst_positive_code_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum)) + ((dst_positive_scale_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum))) + (((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) * S ((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) + ((dst_negative_scale_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)))) * S ((((dst_positive_code_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum)) * S ((dst_positive_code_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum)) + ((dst_positive_scale_weighted_scalar_firstsum) + (dst_positive_scale_weighted_scalar_firstsum))) + (((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) * S ((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) + ((dst_negative_scale_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)))) + ((((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) * S ((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) + ((dst_negative_scale_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum))) + (((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) * S ((dst_negative_code_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)) + ((dst_negative_scale_weighted_scalar_firstsum) + (dst_negative_scale_weighted_scalar_firstsum)))))) /\ (((exists fs_u_dst_weighted_scalar_firstsumpositive fs_v_dst_weighted_scalar_firstsumpositive. ((((exists fs_h_dst_weighted_scalar_firstsumpositive_body_start. fs_h_dst_weighted_scalar_firstsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_scalar_firstsumpositive)) /\ exists fs_q_dst_weighted_scalar_firstsumpositive_body_start. fs_u_dst_weighted_scalar_firstsumpositive = fs_q_dst_weighted_scalar_firstsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_scalar_firstsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumpositive_body_terminal. fs_h_dst_weighted_scalar_firstsumpositive_body_terminal + S (dst_positive_sum_weighted_scalar_firstsum) = S ((S (l)) * fs_v_dst_weighted_scalar_firstsumpositive)) /\ exists fs_q_dst_weighted_scalar_firstsumpositive_body_terminal. fs_u_dst_weighted_scalar_firstsumpositive = fs_q_dst_weighted_scalar_firstsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_scalar_firstsumpositive) + (dst_positive_sum_weighted_scalar_firstsum))) /\ forall fs_i_dst_weighted_scalar_firstsumpositive_body_steps. (exists fs_lt_dst_weighted_scalar_firstsumpositive_body_steps_bound. fs_lt_dst_weighted_scalar_firstsumpositive_body_steps_bound + S fs_i_dst_weighted_scalar_firstsumpositive_body_steps = l) -> exists fs_a_dst_weighted_scalar_firstsumpositive_body_steps fs_r_dst_weighted_scalar_firstsumpositive_body_steps fs_s_dst_weighted_scalar_firstsumpositive_body_steps. ((((exists fs_h_dst_weighted_scalar_firstsumpositive_body_steps_summand. fs_h_dst_weighted_scalar_firstsumpositive_body_steps_summand + S (fs_a_dst_weighted_scalar_firstsumpositive_body_steps) = S ((S (fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * dst_positive_scale_weighted_scalar_firstsum)) /\ exists fs_q_dst_weighted_scalar_firstsumpositive_body_steps_summand. dst_positive_code_weighted_scalar_firstsum = fs_q_dst_weighted_scalar_firstsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * dst_positive_scale_weighted_scalar_firstsum) + (fs_a_dst_weighted_scalar_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumpositive_body_steps_partial. fs_h_dst_weighted_scalar_firstsumpositive_body_steps_partial + S (fs_r_dst_weighted_scalar_firstsumpositive_body_steps) = S ((S (fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * fs_v_dst_weighted_scalar_firstsumpositive)) /\ exists fs_q_dst_weighted_scalar_firstsumpositive_body_steps_partial. fs_u_dst_weighted_scalar_firstsumpositive = fs_q_dst_weighted_scalar_firstsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * fs_v_dst_weighted_scalar_firstsumpositive) + (fs_r_dst_weighted_scalar_firstsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumpositive_body_steps_successor. fs_h_dst_weighted_scalar_firstsumpositive_body_steps_successor + S (fs_s_dst_weighted_scalar_firstsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * fs_v_dst_weighted_scalar_firstsumpositive)) /\ exists fs_q_dst_weighted_scalar_firstsumpositive_body_steps_successor. fs_u_dst_weighted_scalar_firstsumpositive = fs_q_dst_weighted_scalar_firstsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_scalar_firstsumpositive_body_steps)) * fs_v_dst_weighted_scalar_firstsumpositive) + (fs_s_dst_weighted_scalar_firstsumpositive_body_steps))) /\ fs_s_dst_weighted_scalar_firstsumpositive_body_steps = fs_r_dst_weighted_scalar_firstsumpositive_body_steps + fs_a_dst_weighted_scalar_firstsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_scalar_firstsumnegative fs_v_dst_weighted_scalar_firstsumnegative. ((((exists fs_h_dst_weighted_scalar_firstsumnegative_body_start. fs_h_dst_weighted_scalar_firstsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_scalar_firstsumnegative)) /\ exists fs_q_dst_weighted_scalar_firstsumnegative_body_start. fs_u_dst_weighted_scalar_firstsumnegative = fs_q_dst_weighted_scalar_firstsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_scalar_firstsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumnegative_body_terminal. fs_h_dst_weighted_scalar_firstsumnegative_body_terminal + S (dst_negative_sum_weighted_scalar_firstsum) = S ((S (l)) * fs_v_dst_weighted_scalar_firstsumnegative)) /\ exists fs_q_dst_weighted_scalar_firstsumnegative_body_terminal. fs_u_dst_weighted_scalar_firstsumnegative = fs_q_dst_weighted_scalar_firstsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_scalar_firstsumnegative) + (dst_negative_sum_weighted_scalar_firstsum))) /\ forall fs_i_dst_weighted_scalar_firstsumnegative_body_steps. (exists fs_lt_dst_weighted_scalar_firstsumnegative_body_steps_bound. fs_lt_dst_weighted_scalar_firstsumnegative_body_steps_bound + S fs_i_dst_weighted_scalar_firstsumnegative_body_steps = l) -> exists fs_a_dst_weighted_scalar_firstsumnegative_body_steps fs_r_dst_weighted_scalar_firstsumnegative_body_steps fs_s_dst_weighted_scalar_firstsumnegative_body_steps. ((((exists fs_h_dst_weighted_scalar_firstsumnegative_body_steps_summand. fs_h_dst_weighted_scalar_firstsumnegative_body_steps_summand + S (fs_a_dst_weighted_scalar_firstsumnegative_body_steps) = S ((S (fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * dst_negative_scale_weighted_scalar_firstsum)) /\ exists fs_q_dst_weighted_scalar_firstsumnegative_body_steps_summand. dst_negative_code_weighted_scalar_firstsum = fs_q_dst_weighted_scalar_firstsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * dst_negative_scale_weighted_scalar_firstsum) + (fs_a_dst_weighted_scalar_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumnegative_body_steps_partial. fs_h_dst_weighted_scalar_firstsumnegative_body_steps_partial + S (fs_r_dst_weighted_scalar_firstsumnegative_body_steps) = S ((S (fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * fs_v_dst_weighted_scalar_firstsumnegative)) /\ exists fs_q_dst_weighted_scalar_firstsumnegative_body_steps_partial. fs_u_dst_weighted_scalar_firstsumnegative = fs_q_dst_weighted_scalar_firstsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * fs_v_dst_weighted_scalar_firstsumnegative) + (fs_r_dst_weighted_scalar_firstsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_firstsumnegative_body_steps_successor. fs_h_dst_weighted_scalar_firstsumnegative_body_steps_successor + S (fs_s_dst_weighted_scalar_firstsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * fs_v_dst_weighted_scalar_firstsumnegative)) /\ exists fs_q_dst_weighted_scalar_firstsumnegative_body_steps_successor. fs_u_dst_weighted_scalar_firstsumnegative = fs_q_dst_weighted_scalar_firstsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_scalar_firstsumnegative_body_steps)) * fs_v_dst_weighted_scalar_firstsumnegative) + (fs_s_dst_weighted_scalar_firstsumnegative_body_steps))) /\ fs_s_dst_weighted_scalar_firstsumnegative_body_steps = fs_r_dst_weighted_scalar_firstsumnegative_body_steps + fs_a_dst_weighted_scalar_firstsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_scalar_firstsumresult ge_balance_negative_weighted_scalar_firstsumresult. (((((b) = 2 * (ge_balance_positive_weighted_scalar_firstsumresult) /\ (ge_balance_negative_weighted_scalar_firstsumresult) = 0) \/ exists ge_signed_half_weighted_scalar_firstsumresultdecode. (((b) = 2 * ge_signed_half_weighted_scalar_firstsumresultdecode + 1 /\ (ge_balance_positive_weighted_scalar_firstsumresult) = 0) /\ (ge_balance_negative_weighted_scalar_firstsumresult) = S ge_signed_half_weighted_scalar_firstsumresultdecode))) /\ ((dst_positive_sum_weighted_scalar_firstsum) + ge_balance_negative_weighted_scalar_firstsumresult = (dst_negative_sum_weighted_scalar_firstsum) + ge_balance_positive_weighted_scalar_firstsumresult))))))))))) -> (exists sws_product_table_weighted_scalar_output. ((((exists dst_positive_code_weighted_scalar_outputproductsleft_table dst_positive_scale_weighted_scalar_outputproductsleft_table dst_negative_code_weighted_scalar_outputproductsleft_table dst_negative_scale_weighted_scalar_outputproductsleft_table. (((W) = (((((dst_positive_code_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_positive_code_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table)) + ((dst_positive_scale_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table))) + (((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) + ((dst_negative_scale_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)))) * S ((((dst_positive_code_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_positive_code_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table)) + ((dst_positive_scale_weighted_scalar_outputproductsleft_table) + (dst_positive_scale_weighted_scalar_outputproductsleft_table))) + (((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) + ((dst_negative_scale_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)))) + ((((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) + ((dst_negative_scale_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table))) + (((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) * S ((dst_negative_code_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)) + ((dst_negative_scale_weighted_scalar_outputproductsleft_table) + (dst_negative_scale_weighted_scalar_outputproductsleft_table)))))) /\ (forall dst_index_weighted_scalar_outputproductsleft_table. (exists pvs_le_gap_weighted_scalar_outputproductsleft_tabledomain. pvs_le_gap_weighted_scalar_outputproductsleft_tabledomain + (dst_index_weighted_scalar_outputproductsleft_table) = (l)) -> exists dst_positive_weighted_scalar_outputproductsleft_table dst_negative_weighted_scalar_outputproductsleft_table dst_value_weighted_scalar_outputproductsleft_table. ((((exists ff_h_pvs_weighted_scalar_outputproductsleft_tableentrypositive. ff_h_pvs_weighted_scalar_outputproductsleft_tableentrypositive + S (dst_positive_weighted_scalar_outputproductsleft_table) = S ((S (dst_index_weighted_scalar_outputproductsleft_table)) * dst_positive_scale_weighted_scalar_outputproductsleft_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsleft_tableentrypositive. dst_positive_code_weighted_scalar_outputproductsleft_table = ff_q_pvs_weighted_scalar_outputproductsleft_tableentrypositive * S ((S (dst_index_weighted_scalar_outputproductsleft_table)) * dst_positive_scale_weighted_scalar_outputproductsleft_table) + (dst_positive_weighted_scalar_outputproductsleft_table))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsleft_tableentrynegative. ff_h_pvs_weighted_scalar_outputproductsleft_tableentrynegative + S (dst_negative_weighted_scalar_outputproductsleft_table) = S ((S (dst_index_weighted_scalar_outputproductsleft_table)) * dst_negative_scale_weighted_scalar_outputproductsleft_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsleft_tableentrynegative. dst_negative_code_weighted_scalar_outputproductsleft_table = ff_q_pvs_weighted_scalar_outputproductsleft_tableentrynegative * S ((S (dst_index_weighted_scalar_outputproductsleft_table)) * dst_negative_scale_weighted_scalar_outputproductsleft_table) + (dst_negative_weighted_scalar_outputproductsleft_table))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsleft_tableentryvalue ge_balance_negative_weighted_scalar_outputproductsleft_tableentryvalue. (((((dst_value_weighted_scalar_outputproductsleft_table) = 2 * (ge_balance_positive_weighted_scalar_outputproductsleft_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsleft_tableentryvaluedecode. (((dst_value_weighted_scalar_outputproductsleft_table) = 2 * ge_signed_half_weighted_scalar_outputproductsleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsleft_tableentryvalue) = S ge_signed_half_weighted_scalar_outputproductsleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsleft_table) + ge_balance_negative_weighted_scalar_outputproductsleft_tableentryvalue = (dst_negative_weighted_scalar_outputproductsleft_table) + ge_balance_positive_weighted_scalar_outputproductsleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_outputproductsright_table dst_positive_scale_weighted_scalar_outputproductsright_table dst_negative_code_weighted_scalar_outputproductsright_table dst_negative_scale_weighted_scalar_outputproductsright_table. (((G) = (((((dst_positive_code_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table)) * S ((dst_positive_code_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table)) + ((dst_positive_scale_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table))) + (((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) * S ((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) + ((dst_negative_scale_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)))) * S ((((dst_positive_code_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table)) * S ((dst_positive_code_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table)) + ((dst_positive_scale_weighted_scalar_outputproductsright_table) + (dst_positive_scale_weighted_scalar_outputproductsright_table))) + (((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) * S ((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) + ((dst_negative_scale_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)))) + ((((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) * S ((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) + ((dst_negative_scale_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table))) + (((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) * S ((dst_negative_code_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)) + ((dst_negative_scale_weighted_scalar_outputproductsright_table) + (dst_negative_scale_weighted_scalar_outputproductsright_table)))))) /\ (forall dst_index_weighted_scalar_outputproductsright_table. (exists pvs_le_gap_weighted_scalar_outputproductsright_tabledomain. pvs_le_gap_weighted_scalar_outputproductsright_tabledomain + (dst_index_weighted_scalar_outputproductsright_table) = (l)) -> exists dst_positive_weighted_scalar_outputproductsright_table dst_negative_weighted_scalar_outputproductsright_table dst_value_weighted_scalar_outputproductsright_table. ((((exists ff_h_pvs_weighted_scalar_outputproductsright_tableentrypositive. ff_h_pvs_weighted_scalar_outputproductsright_tableentrypositive + S (dst_positive_weighted_scalar_outputproductsright_table) = S ((S (dst_index_weighted_scalar_outputproductsright_table)) * dst_positive_scale_weighted_scalar_outputproductsright_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsright_tableentrypositive. dst_positive_code_weighted_scalar_outputproductsright_table = ff_q_pvs_weighted_scalar_outputproductsright_tableentrypositive * S ((S (dst_index_weighted_scalar_outputproductsright_table)) * dst_positive_scale_weighted_scalar_outputproductsright_table) + (dst_positive_weighted_scalar_outputproductsright_table))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsright_tableentrynegative. ff_h_pvs_weighted_scalar_outputproductsright_tableentrynegative + S (dst_negative_weighted_scalar_outputproductsright_table) = S ((S (dst_index_weighted_scalar_outputproductsright_table)) * dst_negative_scale_weighted_scalar_outputproductsright_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsright_tableentrynegative. dst_negative_code_weighted_scalar_outputproductsright_table = ff_q_pvs_weighted_scalar_outputproductsright_tableentrynegative * S ((S (dst_index_weighted_scalar_outputproductsright_table)) * dst_negative_scale_weighted_scalar_outputproductsright_table) + (dst_negative_weighted_scalar_outputproductsright_table))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsright_tableentryvalue ge_balance_negative_weighted_scalar_outputproductsright_tableentryvalue. (((((dst_value_weighted_scalar_outputproductsright_table) = 2 * (ge_balance_positive_weighted_scalar_outputproductsright_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsright_tableentryvaluedecode. (((dst_value_weighted_scalar_outputproductsright_table) = 2 * ge_signed_half_weighted_scalar_outputproductsright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsright_tableentryvalue) = S ge_signed_half_weighted_scalar_outputproductsright_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsright_table) + ge_balance_negative_weighted_scalar_outputproductsright_tableentryvalue = (dst_negative_weighted_scalar_outputproductsright_table) + ge_balance_positive_weighted_scalar_outputproductsright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_outputproductsoutput_table dst_positive_scale_weighted_scalar_outputproductsoutput_table dst_negative_code_weighted_scalar_outputproductsoutput_table dst_negative_scale_weighted_scalar_outputproductsoutput_table. (((sws_product_table_weighted_scalar_output) = (((((dst_positive_code_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_positive_code_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_positive_scale_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table))) + (((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)))) * S ((((dst_positive_code_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_positive_code_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_positive_scale_weighted_scalar_outputproductsoutput_table) + (dst_positive_scale_weighted_scalar_outputproductsoutput_table))) + (((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)))) + ((((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table))) + (((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) * S ((dst_negative_code_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)) + ((dst_negative_scale_weighted_scalar_outputproductsoutput_table) + (dst_negative_scale_weighted_scalar_outputproductsoutput_table)))))) /\ (forall dst_index_weighted_scalar_outputproductsoutput_table. (exists pvs_le_gap_weighted_scalar_outputproductsoutput_tabledomain. pvs_le_gap_weighted_scalar_outputproductsoutput_tabledomain + (dst_index_weighted_scalar_outputproductsoutput_table) = (l)) -> exists dst_positive_weighted_scalar_outputproductsoutput_table dst_negative_weighted_scalar_outputproductsoutput_table dst_value_weighted_scalar_outputproductsoutput_table. ((((exists ff_h_pvs_weighted_scalar_outputproductsoutput_tableentrypositive. ff_h_pvs_weighted_scalar_outputproductsoutput_tableentrypositive + S (dst_positive_weighted_scalar_outputproductsoutput_table) = S ((S (dst_index_weighted_scalar_outputproductsoutput_table)) * dst_positive_scale_weighted_scalar_outputproductsoutput_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsoutput_tableentrypositive. dst_positive_code_weighted_scalar_outputproductsoutput_table = ff_q_pvs_weighted_scalar_outputproductsoutput_tableentrypositive * S ((S (dst_index_weighted_scalar_outputproductsoutput_table)) * dst_positive_scale_weighted_scalar_outputproductsoutput_table) + (dst_positive_weighted_scalar_outputproductsoutput_table))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsoutput_tableentrynegative. ff_h_pvs_weighted_scalar_outputproductsoutput_tableentrynegative + S (dst_negative_weighted_scalar_outputproductsoutput_table) = S ((S (dst_index_weighted_scalar_outputproductsoutput_table)) * dst_negative_scale_weighted_scalar_outputproductsoutput_table)) /\ exists ff_q_pvs_weighted_scalar_outputproductsoutput_tableentrynegative. dst_negative_code_weighted_scalar_outputproductsoutput_table = ff_q_pvs_weighted_scalar_outputproductsoutput_tableentrynegative * S ((S (dst_index_weighted_scalar_outputproductsoutput_table)) * dst_negative_scale_weighted_scalar_outputproductsoutput_table) + (dst_negative_weighted_scalar_outputproductsoutput_table))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsoutput_tableentryvalue ge_balance_negative_weighted_scalar_outputproductsoutput_tableentryvalue. (((((dst_value_weighted_scalar_outputproductsoutput_table) = 2 * (ge_balance_positive_weighted_scalar_outputproductsoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsoutput_tableentryvaluedecode. (((dst_value_weighted_scalar_outputproductsoutput_table) = 2 * ge_signed_half_weighted_scalar_outputproductsoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsoutput_tableentryvalue) = S ge_signed_half_weighted_scalar_outputproductsoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsoutput_table) + ge_balance_negative_weighted_scalar_outputproductsoutput_tableentryvalue = (dst_negative_weighted_scalar_outputproductsoutput_table) + ge_balance_positive_weighted_scalar_outputproductsoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scalar_outputproductsentries. (exists pvs_gap_weighted_scalar_outputproductsentriesbound. pvs_gap_weighted_scalar_outputproductsentriesbound + S (sto_index_weighted_scalar_outputproductsentries) = (l)) -> exists sto_left_weighted_scalar_outputproductsentries sto_right_weighted_scalar_outputproductsentries sto_output_weighted_scalar_outputproductsentries. ((exists dst_positive_code_weighted_scalar_outputproductsentriesentryleft dst_positive_scale_weighted_scalar_outputproductsentriesentryleft dst_negative_code_weighted_scalar_outputproductsentriesentryleft dst_negative_scale_weighted_scalar_outputproductsentriesentryleft dst_positive_weighted_scalar_outputproductsentriesentryleft dst_negative_weighted_scalar_outputproductsentriesentryleft. (((W) = (((((dst_positive_code_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)))) * S ((((dst_positive_code_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)))) + ((((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryleftpositive. ff_h_pvs_weighted_scalar_outputproductsentriesentryleftpositive + S (dst_positive_weighted_scalar_outputproductsentriesentryleft) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryleftpositive. dst_positive_code_weighted_scalar_outputproductsentriesentryleft = ff_q_pvs_weighted_scalar_outputproductsentriesentryleftpositive * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_positive_weighted_scalar_outputproductsentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryleftnegative. ff_h_pvs_weighted_scalar_outputproductsentriesentryleftnegative + S (dst_negative_weighted_scalar_outputproductsentriesentryleft) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryleft)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryleftnegative. dst_negative_code_weighted_scalar_outputproductsentriesentryleft = ff_q_pvs_weighted_scalar_outputproductsentriesentryleftnegative * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryleft) + (dst_negative_weighted_scalar_outputproductsentriesentryleft))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsentriesentryleftvalue ge_balance_negative_weighted_scalar_outputproductsentriesentryleftvalue. (((((sto_left_weighted_scalar_outputproductsentries) = 2 * (ge_balance_positive_weighted_scalar_outputproductsentriesentryleftvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryleftvaluedecode. (((sto_left_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryleftvalue) = S ge_signed_half_weighted_scalar_outputproductsentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsentriesentryleft) + ge_balance_negative_weighted_scalar_outputproductsentriesentryleftvalue = (dst_negative_weighted_scalar_outputproductsentriesentryleft) + ge_balance_positive_weighted_scalar_outputproductsentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_outputproductsentriesentryright dst_positive_scale_weighted_scalar_outputproductsentriesentryright dst_negative_code_weighted_scalar_outputproductsentriesentryright dst_negative_scale_weighted_scalar_outputproductsentriesentryright dst_positive_weighted_scalar_outputproductsentriesentryright dst_negative_weighted_scalar_outputproductsentriesentryright. (((G) = (((((dst_positive_code_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)))) * S ((((dst_positive_code_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryright) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)))) + ((((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryright) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryrightpositive. ff_h_pvs_weighted_scalar_outputproductsentriesentryrightpositive + S (dst_positive_weighted_scalar_outputproductsentriesentryright) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryright)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryrightpositive. dst_positive_code_weighted_scalar_outputproductsentriesentryright = ff_q_pvs_weighted_scalar_outputproductsentriesentryrightpositive * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryright) + (dst_positive_weighted_scalar_outputproductsentriesentryright))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryrightnegative. ff_h_pvs_weighted_scalar_outputproductsentriesentryrightnegative + S (dst_negative_weighted_scalar_outputproductsentriesentryright) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryright)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryrightnegative. dst_negative_code_weighted_scalar_outputproductsentriesentryright = ff_q_pvs_weighted_scalar_outputproductsentriesentryrightnegative * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryright) + (dst_negative_weighted_scalar_outputproductsentriesentryright))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsentriesentryrightvalue ge_balance_negative_weighted_scalar_outputproductsentriesentryrightvalue. (((((sto_right_weighted_scalar_outputproductsentries) = 2 * (ge_balance_positive_weighted_scalar_outputproductsentriesentryrightvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryrightvaluedecode. (((sto_right_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryrightvalue) = S ge_signed_half_weighted_scalar_outputproductsentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsentriesentryright) + ge_balance_negative_weighted_scalar_outputproductsentriesentryrightvalue = (dst_negative_weighted_scalar_outputproductsentriesentryright) + ge_balance_positive_weighted_scalar_outputproductsentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_scalar_outputproductsentriesentryoutput dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput dst_negative_code_weighted_scalar_outputproductsentriesentryoutput dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput dst_positive_weighted_scalar_outputproductsentriesentryoutput dst_negative_weighted_scalar_outputproductsentriesentryoutput. (((sws_product_table_weighted_scalar_output) = (((((dst_positive_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)))) * S ((((dst_positive_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_positive_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)))) + ((((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput))) + (((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) * S ((dst_negative_code_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) + ((dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryoutputpositive. ff_h_pvs_weighted_scalar_outputproductsentriesentryoutputpositive + S (dst_positive_weighted_scalar_outputproductsentriesentryoutput) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryoutputpositive. dst_positive_code_weighted_scalar_outputproductsentriesentryoutput = ff_q_pvs_weighted_scalar_outputproductsentriesentryoutputpositive * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_positive_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_positive_weighted_scalar_outputproductsentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scalar_outputproductsentriesentryoutputnegative. ff_h_pvs_weighted_scalar_outputproductsentriesentryoutputnegative + S (dst_negative_weighted_scalar_outputproductsentriesentryoutput) = S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput)) /\ exists ff_q_pvs_weighted_scalar_outputproductsentriesentryoutputnegative. dst_negative_code_weighted_scalar_outputproductsentriesentryoutput = ff_q_pvs_weighted_scalar_outputproductsentriesentryoutputnegative * S ((S (sto_index_weighted_scalar_outputproductsentries)) * dst_negative_scale_weighted_scalar_outputproductsentriesentryoutput) + (dst_negative_weighted_scalar_outputproductsentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scalar_outputproductsentriesentryoutputvalue ge_balance_negative_weighted_scalar_outputproductsentriesentryoutputvalue. (((((sto_output_weighted_scalar_outputproductsentries) = 2 * (ge_balance_positive_weighted_scalar_outputproductsentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryoutputvaluedecode. (((sto_output_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scalar_outputproductsentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scalar_outputproductsentriesentryoutputvalue) = S ge_signed_half_weighted_scalar_outputproductsentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scalar_outputproductsentriesentryoutput) + ge_balance_negative_weighted_scalar_outputproductsentriesentryoutputvalue = (dst_negative_weighted_scalar_outputproductsentriesentryoutput) + ge_balance_positive_weighted_scalar_outputproductsentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scalar_outputproductsentriesentryoperation sto_an_weighted_scalar_outputproductsentriesentryoperation sto_bp_weighted_scalar_outputproductsentriesentryoperation sto_bn_weighted_scalar_outputproductsentriesentryoperation sto_cp_weighted_scalar_outputproductsentriesentryoperation sto_cn_weighted_scalar_outputproductsentriesentryoperation. (((((sto_left_weighted_scalar_outputproductsentries) = 2 * (sto_ap_weighted_scalar_outputproductsentriesentryoperation) /\ (sto_an_weighted_scalar_outputproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryoperationleft. (((sto_left_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryoperationleft + 1 /\ (sto_ap_weighted_scalar_outputproductsentriesentryoperation) = 0) /\ (sto_an_weighted_scalar_outputproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_outputproductsentriesentryoperationleft))) /\ ((((((sto_right_weighted_scalar_outputproductsentries) = 2 * (sto_bp_weighted_scalar_outputproductsentriesentryoperation) /\ (sto_bn_weighted_scalar_outputproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryoperationright. (((sto_right_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryoperationright + 1 /\ (sto_bp_weighted_scalar_outputproductsentriesentryoperation) = 0) /\ (sto_bn_weighted_scalar_outputproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_outputproductsentriesentryoperationright))) /\ ((((((sto_output_weighted_scalar_outputproductsentries) = 2 * (sto_cp_weighted_scalar_outputproductsentriesentryoperation) /\ (sto_cn_weighted_scalar_outputproductsentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scalar_outputproductsentriesentryoperationoutput. (((sto_output_weighted_scalar_outputproductsentries) = 2 * ge_signed_half_weighted_scalar_outputproductsentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scalar_outputproductsentriesentryoperation) = 0) /\ (sto_cn_weighted_scalar_outputproductsentriesentryoperation) = S ge_signed_half_weighted_scalar_outputproductsentriesentryoperationoutput))) /\ ((sto_ap_weighted_scalar_outputproductsentriesentryoperation * sto_bp_weighted_scalar_outputproductsentriesentryoperation + sto_an_weighted_scalar_outputproductsentriesentryoperation * sto_bn_weighted_scalar_outputproductsentriesentryoperation) + sto_cn_weighted_scalar_outputproductsentriesentryoperation = (sto_ap_weighted_scalar_outputproductsentriesentryoperation * sto_bn_weighted_scalar_outputproductsentriesentryoperation + sto_an_weighted_scalar_outputproductsentriesentryoperation * sto_bp_weighted_scalar_outputproductsentriesentryoperation) + sto_cp_weighted_scalar_outputproductsentriesentryoperation))))))))))))))))))) /\ (exists dst_positive_code_weighted_scalar_outputsum dst_positive_scale_weighted_scalar_outputsum dst_negative_code_weighted_scalar_outputsum dst_negative_scale_weighted_scalar_outputsum dst_positive_sum_weighted_scalar_outputsum dst_negative_sum_weighted_scalar_outputsum. (((sws_product_table_weighted_scalar_output) = (((((dst_positive_code_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum)) * S ((dst_positive_code_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum)) + ((dst_positive_scale_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum))) + (((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) * S ((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) + ((dst_negative_scale_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)))) * S ((((dst_positive_code_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum)) * S ((dst_positive_code_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum)) + ((dst_positive_scale_weighted_scalar_outputsum) + (dst_positive_scale_weighted_scalar_outputsum))) + (((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) * S ((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) + ((dst_negative_scale_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)))) + ((((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) * S ((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) + ((dst_negative_scale_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum))) + (((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) * S ((dst_negative_code_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)) + ((dst_negative_scale_weighted_scalar_outputsum) + (dst_negative_scale_weighted_scalar_outputsum)))))) /\ (((exists fs_u_dst_weighted_scalar_outputsumpositive fs_v_dst_weighted_scalar_outputsumpositive. ((((exists fs_h_dst_weighted_scalar_outputsumpositive_body_start. fs_h_dst_weighted_scalar_outputsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_scalar_outputsumpositive)) /\ exists fs_q_dst_weighted_scalar_outputsumpositive_body_start. fs_u_dst_weighted_scalar_outputsumpositive = fs_q_dst_weighted_scalar_outputsumpositive_body_start * S ((S (0)) * fs_v_dst_weighted_scalar_outputsumpositive) + (0))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumpositive_body_terminal. fs_h_dst_weighted_scalar_outputsumpositive_body_terminal + S (dst_positive_sum_weighted_scalar_outputsum) = S ((S (l)) * fs_v_dst_weighted_scalar_outputsumpositive)) /\ exists fs_q_dst_weighted_scalar_outputsumpositive_body_terminal. fs_u_dst_weighted_scalar_outputsumpositive = fs_q_dst_weighted_scalar_outputsumpositive_body_terminal * S ((S (l)) * fs_v_dst_weighted_scalar_outputsumpositive) + (dst_positive_sum_weighted_scalar_outputsum))) /\ forall fs_i_dst_weighted_scalar_outputsumpositive_body_steps. (exists fs_lt_dst_weighted_scalar_outputsumpositive_body_steps_bound. fs_lt_dst_weighted_scalar_outputsumpositive_body_steps_bound + S fs_i_dst_weighted_scalar_outputsumpositive_body_steps = l) -> exists fs_a_dst_weighted_scalar_outputsumpositive_body_steps fs_r_dst_weighted_scalar_outputsumpositive_body_steps fs_s_dst_weighted_scalar_outputsumpositive_body_steps. ((((exists fs_h_dst_weighted_scalar_outputsumpositive_body_steps_summand. fs_h_dst_weighted_scalar_outputsumpositive_body_steps_summand + S (fs_a_dst_weighted_scalar_outputsumpositive_body_steps) = S ((S (fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * dst_positive_scale_weighted_scalar_outputsum)) /\ exists fs_q_dst_weighted_scalar_outputsumpositive_body_steps_summand. dst_positive_code_weighted_scalar_outputsum = fs_q_dst_weighted_scalar_outputsumpositive_body_steps_summand * S ((S (fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * dst_positive_scale_weighted_scalar_outputsum) + (fs_a_dst_weighted_scalar_outputsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumpositive_body_steps_partial. fs_h_dst_weighted_scalar_outputsumpositive_body_steps_partial + S (fs_r_dst_weighted_scalar_outputsumpositive_body_steps) = S ((S (fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * fs_v_dst_weighted_scalar_outputsumpositive)) /\ exists fs_q_dst_weighted_scalar_outputsumpositive_body_steps_partial. fs_u_dst_weighted_scalar_outputsumpositive = fs_q_dst_weighted_scalar_outputsumpositive_body_steps_partial * S ((S (fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * fs_v_dst_weighted_scalar_outputsumpositive) + (fs_r_dst_weighted_scalar_outputsumpositive_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumpositive_body_steps_successor. fs_h_dst_weighted_scalar_outputsumpositive_body_steps_successor + S (fs_s_dst_weighted_scalar_outputsumpositive_body_steps) = S ((S (S fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * fs_v_dst_weighted_scalar_outputsumpositive)) /\ exists fs_q_dst_weighted_scalar_outputsumpositive_body_steps_successor. fs_u_dst_weighted_scalar_outputsumpositive = fs_q_dst_weighted_scalar_outputsumpositive_body_steps_successor * S ((S (S fs_i_dst_weighted_scalar_outputsumpositive_body_steps)) * fs_v_dst_weighted_scalar_outputsumpositive) + (fs_s_dst_weighted_scalar_outputsumpositive_body_steps))) /\ fs_s_dst_weighted_scalar_outputsumpositive_body_steps = fs_r_dst_weighted_scalar_outputsumpositive_body_steps + fs_a_dst_weighted_scalar_outputsumpositive_body_steps)))))) /\ (((exists fs_u_dst_weighted_scalar_outputsumnegative fs_v_dst_weighted_scalar_outputsumnegative. ((((exists fs_h_dst_weighted_scalar_outputsumnegative_body_start. fs_h_dst_weighted_scalar_outputsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_weighted_scalar_outputsumnegative)) /\ exists fs_q_dst_weighted_scalar_outputsumnegative_body_start. fs_u_dst_weighted_scalar_outputsumnegative = fs_q_dst_weighted_scalar_outputsumnegative_body_start * S ((S (0)) * fs_v_dst_weighted_scalar_outputsumnegative) + (0))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumnegative_body_terminal. fs_h_dst_weighted_scalar_outputsumnegative_body_terminal + S (dst_negative_sum_weighted_scalar_outputsum) = S ((S (l)) * fs_v_dst_weighted_scalar_outputsumnegative)) /\ exists fs_q_dst_weighted_scalar_outputsumnegative_body_terminal. fs_u_dst_weighted_scalar_outputsumnegative = fs_q_dst_weighted_scalar_outputsumnegative_body_terminal * S ((S (l)) * fs_v_dst_weighted_scalar_outputsumnegative) + (dst_negative_sum_weighted_scalar_outputsum))) /\ forall fs_i_dst_weighted_scalar_outputsumnegative_body_steps. (exists fs_lt_dst_weighted_scalar_outputsumnegative_body_steps_bound. fs_lt_dst_weighted_scalar_outputsumnegative_body_steps_bound + S fs_i_dst_weighted_scalar_outputsumnegative_body_steps = l) -> exists fs_a_dst_weighted_scalar_outputsumnegative_body_steps fs_r_dst_weighted_scalar_outputsumnegative_body_steps fs_s_dst_weighted_scalar_outputsumnegative_body_steps. ((((exists fs_h_dst_weighted_scalar_outputsumnegative_body_steps_summand. fs_h_dst_weighted_scalar_outputsumnegative_body_steps_summand + S (fs_a_dst_weighted_scalar_outputsumnegative_body_steps) = S ((S (fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * dst_negative_scale_weighted_scalar_outputsum)) /\ exists fs_q_dst_weighted_scalar_outputsumnegative_body_steps_summand. dst_negative_code_weighted_scalar_outputsum = fs_q_dst_weighted_scalar_outputsumnegative_body_steps_summand * S ((S (fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * dst_negative_scale_weighted_scalar_outputsum) + (fs_a_dst_weighted_scalar_outputsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumnegative_body_steps_partial. fs_h_dst_weighted_scalar_outputsumnegative_body_steps_partial + S (fs_r_dst_weighted_scalar_outputsumnegative_body_steps) = S ((S (fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * fs_v_dst_weighted_scalar_outputsumnegative)) /\ exists fs_q_dst_weighted_scalar_outputsumnegative_body_steps_partial. fs_u_dst_weighted_scalar_outputsumnegative = fs_q_dst_weighted_scalar_outputsumnegative_body_steps_partial * S ((S (fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * fs_v_dst_weighted_scalar_outputsumnegative) + (fs_r_dst_weighted_scalar_outputsumnegative_body_steps))) /\ ((((exists fs_h_dst_weighted_scalar_outputsumnegative_body_steps_successor. fs_h_dst_weighted_scalar_outputsumnegative_body_steps_successor + S (fs_s_dst_weighted_scalar_outputsumnegative_body_steps) = S ((S (S fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * fs_v_dst_weighted_scalar_outputsumnegative)) /\ exists fs_q_dst_weighted_scalar_outputsumnegative_body_steps_successor. fs_u_dst_weighted_scalar_outputsumnegative = fs_q_dst_weighted_scalar_outputsumnegative_body_steps_successor * S ((S (S fs_i_dst_weighted_scalar_outputsumnegative_body_steps)) * fs_v_dst_weighted_scalar_outputsumnegative) + (fs_s_dst_weighted_scalar_outputsumnegative_body_steps))) /\ fs_s_dst_weighted_scalar_outputsumnegative_body_steps = fs_r_dst_weighted_scalar_outputsumnegative_body_steps + fs_a_dst_weighted_scalar_outputsumnegative_body_steps)))))) /\ (exists ge_balance_positive_weighted_scalar_outputsumresult ge_balance_negative_weighted_scalar_outputsumresult. (((((c) = 2 * (ge_balance_positive_weighted_scalar_outputsumresult) /\ (ge_balance_negative_weighted_scalar_outputsumresult) = 0) \/ exists ge_signed_half_weighted_scalar_outputsumresultdecode. (((c) = 2 * ge_signed_half_weighted_scalar_outputsumresultdecode + 1 /\ (ge_balance_positive_weighted_scalar_outputsumresult) = 0) /\ (ge_balance_negative_weighted_scalar_outputsumresult) = S ge_signed_half_weighted_scalar_outputsumresultdecode))) /\ ((dst_positive_sum_weighted_scalar_outputsum) + ge_balance_negative_weighted_scalar_outputsumresult = (dst_negative_sum_weighted_scalar_outputsum) + ge_balance_positive_weighted_scalar_outputsumresult))))))))))) -> (exists sto_ap_weighted_scalar_result sto_an_weighted_scalar_result sto_bp_weighted_scalar_result sto_bn_weighted_scalar_result sto_cp_weighted_scalar_result sto_cn_weighted_scalar_result. (((((a) = 2 * (sto_ap_weighted_scalar_result) /\ (sto_an_weighted_scalar_result) = 0) \/ exists ge_signed_half_weighted_scalar_resultleft. (((a) = 2 * ge_signed_half_weighted_scalar_resultleft + 1 /\ (sto_ap_weighted_scalar_result) = 0) /\ (sto_an_weighted_scalar_result) = S ge_signed_half_weighted_scalar_resultleft))) /\ ((((((b) = 2 * (sto_bp_weighted_scalar_result) /\ (sto_bn_weighted_scalar_result) = 0) \/ exists ge_signed_half_weighted_scalar_resultright. (((b) = 2 * ge_signed_half_weighted_scalar_resultright + 1 /\ (sto_bp_weighted_scalar_result) = 0) /\ (sto_bn_weighted_scalar_result) = S ge_signed_half_weighted_scalar_resultright))) /\ ((((((c) = 2 * (sto_cp_weighted_scalar_result) /\ (sto_cn_weighted_scalar_result) = 0) \/ exists ge_signed_half_weighted_scalar_resultoutput. (((c) = 2 * ge_signed_half_weighted_scalar_resultoutput + 1 /\ (sto_cp_weighted_scalar_result) = 0) /\ (sto_cn_weighted_scalar_result) = S ge_signed_half_weighted_scalar_resultoutput))) /\ ((sto_ap_weighted_scalar_result * sto_bp_weighted_scalar_result + sto_an_weighted_scalar_result * sto_bn_weighted_scalar_result) + sto_cn_weighted_scalar_result = (sto_ap_weighted_scalar_result * sto_bn_weighted_scalar_result + sto_an_weighted_scalar_result * sto_bp_weighted_scalar_result) + sto_cp_weighted_scalar_result)))))))