signed_table_weighted_scalar_commute

Exact expanded first-order arithmetic statement

forall l a W F G P Q. (((exists dst_positive_code_weighted_scale_inputinput_table dst_positive_scale_weighted_scale_inputinput_table dst_negative_code_weighted_scale_inputinput_table dst_negative_scale_weighted_scale_inputinput_table. (((F) = (((((dst_positive_code_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table)) * S ((dst_positive_code_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table)) + ((dst_positive_scale_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table))) + (((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) * S ((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) + ((dst_negative_scale_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)))) * S ((((dst_positive_code_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table)) * S ((dst_positive_code_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table)) + ((dst_positive_scale_weighted_scale_inputinput_table) + (dst_positive_scale_weighted_scale_inputinput_table))) + (((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) * S ((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) + ((dst_negative_scale_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)))) + ((((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) * S ((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) + ((dst_negative_scale_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table))) + (((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) * S ((dst_negative_code_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)) + ((dst_negative_scale_weighted_scale_inputinput_table) + (dst_negative_scale_weighted_scale_inputinput_table)))))) /\ (forall dst_index_weighted_scale_inputinput_table. (exists pvs_le_gap_weighted_scale_inputinput_tabledomain. pvs_le_gap_weighted_scale_inputinput_tabledomain + (dst_index_weighted_scale_inputinput_table) = (l)) -> exists dst_positive_weighted_scale_inputinput_table dst_negative_weighted_scale_inputinput_table dst_value_weighted_scale_inputinput_table. ((((exists ff_h_pvs_weighted_scale_inputinput_tableentrypositive. ff_h_pvs_weighted_scale_inputinput_tableentrypositive + S (dst_positive_weighted_scale_inputinput_table) = S ((S (dst_index_weighted_scale_inputinput_table)) * dst_positive_scale_weighted_scale_inputinput_table)) /\ exists ff_q_pvs_weighted_scale_inputinput_tableentrypositive. dst_positive_code_weighted_scale_inputinput_table = ff_q_pvs_weighted_scale_inputinput_tableentrypositive * S ((S (dst_index_weighted_scale_inputinput_table)) * dst_positive_scale_weighted_scale_inputinput_table) + (dst_positive_weighted_scale_inputinput_table))) /\ (((((exists ff_h_pvs_weighted_scale_inputinput_tableentrynegative. ff_h_pvs_weighted_scale_inputinput_tableentrynegative + S (dst_negative_weighted_scale_inputinput_table) = S ((S (dst_index_weighted_scale_inputinput_table)) * dst_negative_scale_weighted_scale_inputinput_table)) /\ exists ff_q_pvs_weighted_scale_inputinput_tableentrynegative. dst_negative_code_weighted_scale_inputinput_table = ff_q_pvs_weighted_scale_inputinput_tableentrynegative * S ((S (dst_index_weighted_scale_inputinput_table)) * dst_negative_scale_weighted_scale_inputinput_table) + (dst_negative_weighted_scale_inputinput_table))) /\ (exists ge_balance_positive_weighted_scale_inputinput_tableentryvalue ge_balance_negative_weighted_scale_inputinput_tableentryvalue. (((((dst_value_weighted_scale_inputinput_table) = 2 * (ge_balance_positive_weighted_scale_inputinput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_inputinput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_inputinput_tableentryvaluedecode. (((dst_value_weighted_scale_inputinput_table) = 2 * ge_signed_half_weighted_scale_inputinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_inputinput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_inputinput_tableentryvalue) = S ge_signed_half_weighted_scale_inputinput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_inputinput_table) + ge_balance_negative_weighted_scale_inputinput_tableentryvalue = (dst_negative_weighted_scale_inputinput_table) + ge_balance_positive_weighted_scale_inputinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_inputoutput_table dst_positive_scale_weighted_scale_inputoutput_table dst_negative_code_weighted_scale_inputoutput_table dst_negative_scale_weighted_scale_inputoutput_table. (((G) = (((((dst_positive_code_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table)) * S ((dst_positive_code_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table)) + ((dst_positive_scale_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table))) + (((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) * S ((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) + ((dst_negative_scale_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)))) * S ((((dst_positive_code_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table)) * S ((dst_positive_code_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table)) + ((dst_positive_scale_weighted_scale_inputoutput_table) + (dst_positive_scale_weighted_scale_inputoutput_table))) + (((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) * S ((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) + ((dst_negative_scale_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)))) + ((((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) * S ((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) + ((dst_negative_scale_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table))) + (((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) * S ((dst_negative_code_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)) + ((dst_negative_scale_weighted_scale_inputoutput_table) + (dst_negative_scale_weighted_scale_inputoutput_table)))))) /\ (forall dst_index_weighted_scale_inputoutput_table. (exists pvs_le_gap_weighted_scale_inputoutput_tabledomain. pvs_le_gap_weighted_scale_inputoutput_tabledomain + (dst_index_weighted_scale_inputoutput_table) = (l)) -> exists dst_positive_weighted_scale_inputoutput_table dst_negative_weighted_scale_inputoutput_table dst_value_weighted_scale_inputoutput_table. ((((exists ff_h_pvs_weighted_scale_inputoutput_tableentrypositive. ff_h_pvs_weighted_scale_inputoutput_tableentrypositive + S (dst_positive_weighted_scale_inputoutput_table) = S ((S (dst_index_weighted_scale_inputoutput_table)) * dst_positive_scale_weighted_scale_inputoutput_table)) /\ exists ff_q_pvs_weighted_scale_inputoutput_tableentrypositive. dst_positive_code_weighted_scale_inputoutput_table = ff_q_pvs_weighted_scale_inputoutput_tableentrypositive * S ((S (dst_index_weighted_scale_inputoutput_table)) * dst_positive_scale_weighted_scale_inputoutput_table) + (dst_positive_weighted_scale_inputoutput_table))) /\ (((((exists ff_h_pvs_weighted_scale_inputoutput_tableentrynegative. ff_h_pvs_weighted_scale_inputoutput_tableentrynegative + S (dst_negative_weighted_scale_inputoutput_table) = S ((S (dst_index_weighted_scale_inputoutput_table)) * dst_negative_scale_weighted_scale_inputoutput_table)) /\ exists ff_q_pvs_weighted_scale_inputoutput_tableentrynegative. dst_negative_code_weighted_scale_inputoutput_table = ff_q_pvs_weighted_scale_inputoutput_tableentrynegative * S ((S (dst_index_weighted_scale_inputoutput_table)) * dst_negative_scale_weighted_scale_inputoutput_table) + (dst_negative_weighted_scale_inputoutput_table))) /\ (exists ge_balance_positive_weighted_scale_inputoutput_tableentryvalue ge_balance_negative_weighted_scale_inputoutput_tableentryvalue. (((((dst_value_weighted_scale_inputoutput_table) = 2 * (ge_balance_positive_weighted_scale_inputoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_inputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_inputoutput_tableentryvaluedecode. (((dst_value_weighted_scale_inputoutput_table) = 2 * ge_signed_half_weighted_scale_inputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_inputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_inputoutput_tableentryvalue) = S ge_signed_half_weighted_scale_inputoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_inputoutput_table) + ge_balance_negative_weighted_scale_inputoutput_tableentryvalue = (dst_negative_weighted_scale_inputoutput_table) + ge_balance_positive_weighted_scale_inputoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scale_inputentries. (exists pvs_gap_weighted_scale_inputentriesbound. pvs_gap_weighted_scale_inputentriesbound + S (sto_index_weighted_scale_inputentries) = (l)) -> exists sto_input_weighted_scale_inputentries sto_output_weighted_scale_inputentries. ((exists dst_positive_code_weighted_scale_inputentriesentryinput dst_positive_scale_weighted_scale_inputentriesentryinput dst_negative_code_weighted_scale_inputentriesentryinput dst_negative_scale_weighted_scale_inputentriesentryinput dst_positive_weighted_scale_inputentriesentryinput dst_negative_weighted_scale_inputentriesentryinput. (((F) = (((((dst_positive_code_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput)) * S ((dst_positive_code_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput)) + ((dst_positive_scale_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput))) + (((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) * S ((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) + ((dst_negative_scale_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)))) * S ((((dst_positive_code_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput)) * S ((dst_positive_code_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput)) + ((dst_positive_scale_weighted_scale_inputentriesentryinput) + (dst_positive_scale_weighted_scale_inputentriesentryinput))) + (((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) * S ((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) + ((dst_negative_scale_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)))) + ((((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) * S ((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) + ((dst_negative_scale_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput))) + (((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) * S ((dst_negative_code_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)) + ((dst_negative_scale_weighted_scale_inputentriesentryinput) + (dst_negative_scale_weighted_scale_inputentriesentryinput)))))) /\ (((((exists ff_h_pvs_weighted_scale_inputentriesentryinputpositive. ff_h_pvs_weighted_scale_inputentriesentryinputpositive + S (dst_positive_weighted_scale_inputentriesentryinput) = S ((S (sto_index_weighted_scale_inputentries)) * dst_positive_scale_weighted_scale_inputentriesentryinput)) /\ exists ff_q_pvs_weighted_scale_inputentriesentryinputpositive. dst_positive_code_weighted_scale_inputentriesentryinput = ff_q_pvs_weighted_scale_inputentriesentryinputpositive * S ((S (sto_index_weighted_scale_inputentries)) * dst_positive_scale_weighted_scale_inputentriesentryinput) + (dst_positive_weighted_scale_inputentriesentryinput))) /\ (((((exists ff_h_pvs_weighted_scale_inputentriesentryinputnegative. ff_h_pvs_weighted_scale_inputentriesentryinputnegative + S (dst_negative_weighted_scale_inputentriesentryinput) = S ((S (sto_index_weighted_scale_inputentries)) * dst_negative_scale_weighted_scale_inputentriesentryinput)) /\ exists ff_q_pvs_weighted_scale_inputentriesentryinputnegative. dst_negative_code_weighted_scale_inputentriesentryinput = ff_q_pvs_weighted_scale_inputentriesentryinputnegative * S ((S (sto_index_weighted_scale_inputentries)) * dst_negative_scale_weighted_scale_inputentriesentryinput) + (dst_negative_weighted_scale_inputentriesentryinput))) /\ (exists ge_balance_positive_weighted_scale_inputentriesentryinputvalue ge_balance_negative_weighted_scale_inputentriesentryinputvalue. (((((sto_input_weighted_scale_inputentries) = 2 * (ge_balance_positive_weighted_scale_inputentriesentryinputvalue) /\ (ge_balance_negative_weighted_scale_inputentriesentryinputvalue) = 0) \/ exists ge_signed_half_weighted_scale_inputentriesentryinputvaluedecode. (((sto_input_weighted_scale_inputentries) = 2 * ge_signed_half_weighted_scale_inputentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_inputentriesentryinputvalue) = 0) /\ (ge_balance_negative_weighted_scale_inputentriesentryinputvalue) = S ge_signed_half_weighted_scale_inputentriesentryinputvaluedecode))) /\ ((dst_positive_weighted_scale_inputentriesentryinput) + ge_balance_negative_weighted_scale_inputentriesentryinputvalue = (dst_negative_weighted_scale_inputentriesentryinput) + ge_balance_positive_weighted_scale_inputentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_inputentriesentryoutput dst_positive_scale_weighted_scale_inputentriesentryoutput dst_negative_code_weighted_scale_inputentriesentryoutput dst_negative_scale_weighted_scale_inputentriesentryoutput dst_positive_weighted_scale_inputentriesentryoutput dst_negative_weighted_scale_inputentriesentryoutput. (((G) = (((((dst_positive_code_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_positive_code_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput)) + ((dst_positive_scale_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput))) + (((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)))) * S ((((dst_positive_code_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_positive_code_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput)) + ((dst_positive_scale_weighted_scale_inputentriesentryoutput) + (dst_positive_scale_weighted_scale_inputentriesentryoutput))) + (((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)))) + ((((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput))) + (((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) * S ((dst_negative_code_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)) + ((dst_negative_scale_weighted_scale_inputentriesentryoutput) + (dst_negative_scale_weighted_scale_inputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scale_inputentriesentryoutputpositive. ff_h_pvs_weighted_scale_inputentriesentryoutputpositive + S (dst_positive_weighted_scale_inputentriesentryoutput) = S ((S (sto_index_weighted_scale_inputentries)) * dst_positive_scale_weighted_scale_inputentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_inputentriesentryoutputpositive. dst_positive_code_weighted_scale_inputentriesentryoutput = ff_q_pvs_weighted_scale_inputentriesentryoutputpositive * S ((S (sto_index_weighted_scale_inputentries)) * dst_positive_scale_weighted_scale_inputentriesentryoutput) + (dst_positive_weighted_scale_inputentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scale_inputentriesentryoutputnegative. ff_h_pvs_weighted_scale_inputentriesentryoutputnegative + S (dst_negative_weighted_scale_inputentriesentryoutput) = S ((S (sto_index_weighted_scale_inputentries)) * dst_negative_scale_weighted_scale_inputentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_inputentriesentryoutputnegative. dst_negative_code_weighted_scale_inputentriesentryoutput = ff_q_pvs_weighted_scale_inputentriesentryoutputnegative * S ((S (sto_index_weighted_scale_inputentries)) * dst_negative_scale_weighted_scale_inputentriesentryoutput) + (dst_negative_weighted_scale_inputentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scale_inputentriesentryoutputvalue ge_balance_negative_weighted_scale_inputentriesentryoutputvalue. (((((sto_output_weighted_scale_inputentries) = 2 * (ge_balance_positive_weighted_scale_inputentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scale_inputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scale_inputentriesentryoutputvaluedecode. (((sto_output_weighted_scale_inputentries) = 2 * ge_signed_half_weighted_scale_inputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_inputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scale_inputentriesentryoutputvalue) = S ge_signed_half_weighted_scale_inputentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scale_inputentriesentryoutput) + ge_balance_negative_weighted_scale_inputentriesentryoutputvalue = (dst_negative_weighted_scale_inputentriesentryoutput) + ge_balance_positive_weighted_scale_inputentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scale_inputentriesentryoperation sto_an_weighted_scale_inputentriesentryoperation sto_bp_weighted_scale_inputentriesentryoperation sto_bn_weighted_scale_inputentriesentryoperation sto_cp_weighted_scale_inputentriesentryoperation sto_cn_weighted_scale_inputentriesentryoperation. (((((a) = 2 * (sto_ap_weighted_scale_inputentriesentryoperation) /\ (sto_an_weighted_scale_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_inputentriesentryoperationleft. (((a) = 2 * ge_signed_half_weighted_scale_inputentriesentryoperationleft + 1 /\ (sto_ap_weighted_scale_inputentriesentryoperation) = 0) /\ (sto_an_weighted_scale_inputentriesentryoperation) = S ge_signed_half_weighted_scale_inputentriesentryoperationleft))) /\ ((((((sto_input_weighted_scale_inputentries) = 2 * (sto_bp_weighted_scale_inputentriesentryoperation) /\ (sto_bn_weighted_scale_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_inputentriesentryoperationright. (((sto_input_weighted_scale_inputentries) = 2 * ge_signed_half_weighted_scale_inputentriesentryoperationright + 1 /\ (sto_bp_weighted_scale_inputentriesentryoperation) = 0) /\ (sto_bn_weighted_scale_inputentriesentryoperation) = S ge_signed_half_weighted_scale_inputentriesentryoperationright))) /\ ((((((sto_output_weighted_scale_inputentries) = 2 * (sto_cp_weighted_scale_inputentriesentryoperation) /\ (sto_cn_weighted_scale_inputentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_inputentriesentryoperationoutput. (((sto_output_weighted_scale_inputentries) = 2 * ge_signed_half_weighted_scale_inputentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scale_inputentriesentryoperation) = 0) /\ (sto_cn_weighted_scale_inputentriesentryoperation) = S ge_signed_half_weighted_scale_inputentriesentryoperationoutput))) /\ ((sto_ap_weighted_scale_inputentriesentryoperation * sto_bp_weighted_scale_inputentriesentryoperation + sto_an_weighted_scale_inputentriesentryoperation * sto_bn_weighted_scale_inputentriesentryoperation) + sto_cn_weighted_scale_inputentriesentryoperation = (sto_ap_weighted_scale_inputentriesentryoperation * sto_bn_weighted_scale_inputentriesentryoperation + sto_an_weighted_scale_inputentriesentryoperation * sto_bp_weighted_scale_inputentriesentryoperation) + sto_cp_weighted_scale_inputentriesentryoperation))))))))))))))) -> (((exists dst_positive_code_weighted_scale_firstleft_table dst_positive_scale_weighted_scale_firstleft_table dst_negative_code_weighted_scale_firstleft_table dst_negative_scale_weighted_scale_firstleft_table. (((W) = (((((dst_positive_code_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table)) * S ((dst_positive_code_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table)) + ((dst_positive_scale_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table))) + (((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) * S ((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) + ((dst_negative_scale_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)))) * S ((((dst_positive_code_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table)) * S ((dst_positive_code_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table)) + ((dst_positive_scale_weighted_scale_firstleft_table) + (dst_positive_scale_weighted_scale_firstleft_table))) + (((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) * S ((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) + ((dst_negative_scale_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)))) + ((((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) * S ((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) + ((dst_negative_scale_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table))) + (((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) * S ((dst_negative_code_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)) + ((dst_negative_scale_weighted_scale_firstleft_table) + (dst_negative_scale_weighted_scale_firstleft_table)))))) /\ (forall dst_index_weighted_scale_firstleft_table. (exists pvs_le_gap_weighted_scale_firstleft_tabledomain. pvs_le_gap_weighted_scale_firstleft_tabledomain + (dst_index_weighted_scale_firstleft_table) = (l)) -> exists dst_positive_weighted_scale_firstleft_table dst_negative_weighted_scale_firstleft_table dst_value_weighted_scale_firstleft_table. ((((exists ff_h_pvs_weighted_scale_firstleft_tableentrypositive. ff_h_pvs_weighted_scale_firstleft_tableentrypositive + S (dst_positive_weighted_scale_firstleft_table) = S ((S (dst_index_weighted_scale_firstleft_table)) * dst_positive_scale_weighted_scale_firstleft_table)) /\ exists ff_q_pvs_weighted_scale_firstleft_tableentrypositive. dst_positive_code_weighted_scale_firstleft_table = ff_q_pvs_weighted_scale_firstleft_tableentrypositive * S ((S (dst_index_weighted_scale_firstleft_table)) * dst_positive_scale_weighted_scale_firstleft_table) + (dst_positive_weighted_scale_firstleft_table))) /\ (((((exists ff_h_pvs_weighted_scale_firstleft_tableentrynegative. ff_h_pvs_weighted_scale_firstleft_tableentrynegative + S (dst_negative_weighted_scale_firstleft_table) = S ((S (dst_index_weighted_scale_firstleft_table)) * dst_negative_scale_weighted_scale_firstleft_table)) /\ exists ff_q_pvs_weighted_scale_firstleft_tableentrynegative. dst_negative_code_weighted_scale_firstleft_table = ff_q_pvs_weighted_scale_firstleft_tableentrynegative * S ((S (dst_index_weighted_scale_firstleft_table)) * dst_negative_scale_weighted_scale_firstleft_table) + (dst_negative_weighted_scale_firstleft_table))) /\ (exists ge_balance_positive_weighted_scale_firstleft_tableentryvalue ge_balance_negative_weighted_scale_firstleft_tableentryvalue. (((((dst_value_weighted_scale_firstleft_table) = 2 * (ge_balance_positive_weighted_scale_firstleft_tableentryvalue) /\ (ge_balance_negative_weighted_scale_firstleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstleft_tableentryvaluedecode. (((dst_value_weighted_scale_firstleft_table) = 2 * ge_signed_half_weighted_scale_firstleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstleft_tableentryvalue) = S ge_signed_half_weighted_scale_firstleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_firstleft_table) + ge_balance_negative_weighted_scale_firstleft_tableentryvalue = (dst_negative_weighted_scale_firstleft_table) + ge_balance_positive_weighted_scale_firstleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_firstright_table dst_positive_scale_weighted_scale_firstright_table dst_negative_code_weighted_scale_firstright_table dst_negative_scale_weighted_scale_firstright_table. (((F) = (((((dst_positive_code_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table)) * S ((dst_positive_code_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table)) + ((dst_positive_scale_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table))) + (((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) * S ((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) + ((dst_negative_scale_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)))) * S ((((dst_positive_code_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table)) * S ((dst_positive_code_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table)) + ((dst_positive_scale_weighted_scale_firstright_table) + (dst_positive_scale_weighted_scale_firstright_table))) + (((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) * S ((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) + ((dst_negative_scale_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)))) + ((((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) * S ((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) + ((dst_negative_scale_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table))) + (((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) * S ((dst_negative_code_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)) + ((dst_negative_scale_weighted_scale_firstright_table) + (dst_negative_scale_weighted_scale_firstright_table)))))) /\ (forall dst_index_weighted_scale_firstright_table. (exists pvs_le_gap_weighted_scale_firstright_tabledomain. pvs_le_gap_weighted_scale_firstright_tabledomain + (dst_index_weighted_scale_firstright_table) = (l)) -> exists dst_positive_weighted_scale_firstright_table dst_negative_weighted_scale_firstright_table dst_value_weighted_scale_firstright_table. ((((exists ff_h_pvs_weighted_scale_firstright_tableentrypositive. ff_h_pvs_weighted_scale_firstright_tableentrypositive + S (dst_positive_weighted_scale_firstright_table) = S ((S (dst_index_weighted_scale_firstright_table)) * dst_positive_scale_weighted_scale_firstright_table)) /\ exists ff_q_pvs_weighted_scale_firstright_tableentrypositive. dst_positive_code_weighted_scale_firstright_table = ff_q_pvs_weighted_scale_firstright_tableentrypositive * S ((S (dst_index_weighted_scale_firstright_table)) * dst_positive_scale_weighted_scale_firstright_table) + (dst_positive_weighted_scale_firstright_table))) /\ (((((exists ff_h_pvs_weighted_scale_firstright_tableentrynegative. ff_h_pvs_weighted_scale_firstright_tableentrynegative + S (dst_negative_weighted_scale_firstright_table) = S ((S (dst_index_weighted_scale_firstright_table)) * dst_negative_scale_weighted_scale_firstright_table)) /\ exists ff_q_pvs_weighted_scale_firstright_tableentrynegative. dst_negative_code_weighted_scale_firstright_table = ff_q_pvs_weighted_scale_firstright_tableentrynegative * S ((S (dst_index_weighted_scale_firstright_table)) * dst_negative_scale_weighted_scale_firstright_table) + (dst_negative_weighted_scale_firstright_table))) /\ (exists ge_balance_positive_weighted_scale_firstright_tableentryvalue ge_balance_negative_weighted_scale_firstright_tableentryvalue. (((((dst_value_weighted_scale_firstright_table) = 2 * (ge_balance_positive_weighted_scale_firstright_tableentryvalue) /\ (ge_balance_negative_weighted_scale_firstright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstright_tableentryvaluedecode. (((dst_value_weighted_scale_firstright_table) = 2 * ge_signed_half_weighted_scale_firstright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstright_tableentryvalue) = S ge_signed_half_weighted_scale_firstright_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_firstright_table) + ge_balance_negative_weighted_scale_firstright_tableentryvalue = (dst_negative_weighted_scale_firstright_table) + ge_balance_positive_weighted_scale_firstright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_firstoutput_table dst_positive_scale_weighted_scale_firstoutput_table dst_negative_code_weighted_scale_firstoutput_table dst_negative_scale_weighted_scale_firstoutput_table. (((P) = (((((dst_positive_code_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table)) * S ((dst_positive_code_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table)) + ((dst_positive_scale_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table))) + (((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) * S ((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) + ((dst_negative_scale_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)))) * S ((((dst_positive_code_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table)) * S ((dst_positive_code_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table)) + ((dst_positive_scale_weighted_scale_firstoutput_table) + (dst_positive_scale_weighted_scale_firstoutput_table))) + (((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) * S ((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) + ((dst_negative_scale_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)))) + ((((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) * S ((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) + ((dst_negative_scale_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table))) + (((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) * S ((dst_negative_code_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)) + ((dst_negative_scale_weighted_scale_firstoutput_table) + (dst_negative_scale_weighted_scale_firstoutput_table)))))) /\ (forall dst_index_weighted_scale_firstoutput_table. (exists pvs_le_gap_weighted_scale_firstoutput_tabledomain. pvs_le_gap_weighted_scale_firstoutput_tabledomain + (dst_index_weighted_scale_firstoutput_table) = (l)) -> exists dst_positive_weighted_scale_firstoutput_table dst_negative_weighted_scale_firstoutput_table dst_value_weighted_scale_firstoutput_table. ((((exists ff_h_pvs_weighted_scale_firstoutput_tableentrypositive. ff_h_pvs_weighted_scale_firstoutput_tableentrypositive + S (dst_positive_weighted_scale_firstoutput_table) = S ((S (dst_index_weighted_scale_firstoutput_table)) * dst_positive_scale_weighted_scale_firstoutput_table)) /\ exists ff_q_pvs_weighted_scale_firstoutput_tableentrypositive. dst_positive_code_weighted_scale_firstoutput_table = ff_q_pvs_weighted_scale_firstoutput_tableentrypositive * S ((S (dst_index_weighted_scale_firstoutput_table)) * dst_positive_scale_weighted_scale_firstoutput_table) + (dst_positive_weighted_scale_firstoutput_table))) /\ (((((exists ff_h_pvs_weighted_scale_firstoutput_tableentrynegative. ff_h_pvs_weighted_scale_firstoutput_tableentrynegative + S (dst_negative_weighted_scale_firstoutput_table) = S ((S (dst_index_weighted_scale_firstoutput_table)) * dst_negative_scale_weighted_scale_firstoutput_table)) /\ exists ff_q_pvs_weighted_scale_firstoutput_tableentrynegative. dst_negative_code_weighted_scale_firstoutput_table = ff_q_pvs_weighted_scale_firstoutput_tableentrynegative * S ((S (dst_index_weighted_scale_firstoutput_table)) * dst_negative_scale_weighted_scale_firstoutput_table) + (dst_negative_weighted_scale_firstoutput_table))) /\ (exists ge_balance_positive_weighted_scale_firstoutput_tableentryvalue ge_balance_negative_weighted_scale_firstoutput_tableentryvalue. (((((dst_value_weighted_scale_firstoutput_table) = 2 * (ge_balance_positive_weighted_scale_firstoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_firstoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstoutput_tableentryvaluedecode. (((dst_value_weighted_scale_firstoutput_table) = 2 * ge_signed_half_weighted_scale_firstoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstoutput_tableentryvalue) = S ge_signed_half_weighted_scale_firstoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_firstoutput_table) + ge_balance_negative_weighted_scale_firstoutput_tableentryvalue = (dst_negative_weighted_scale_firstoutput_table) + ge_balance_positive_weighted_scale_firstoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scale_firstentries. (exists pvs_gap_weighted_scale_firstentriesbound. pvs_gap_weighted_scale_firstentriesbound + S (sto_index_weighted_scale_firstentries) = (l)) -> exists sto_left_weighted_scale_firstentries sto_right_weighted_scale_firstentries sto_output_weighted_scale_firstentries. ((exists dst_positive_code_weighted_scale_firstentriesentryleft dst_positive_scale_weighted_scale_firstentriesentryleft dst_negative_code_weighted_scale_firstentriesentryleft dst_negative_scale_weighted_scale_firstentriesentryleft dst_positive_weighted_scale_firstentriesentryleft dst_negative_weighted_scale_firstentriesentryleft. (((W) = (((((dst_positive_code_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft)) * S ((dst_positive_code_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft)) + ((dst_positive_scale_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft))) + (((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) * S ((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) + ((dst_negative_scale_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)))) * S ((((dst_positive_code_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft)) * S ((dst_positive_code_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft)) + ((dst_positive_scale_weighted_scale_firstentriesentryleft) + (dst_positive_scale_weighted_scale_firstentriesentryleft))) + (((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) * S ((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) + ((dst_negative_scale_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)))) + ((((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) * S ((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) + ((dst_negative_scale_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft))) + (((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) * S ((dst_negative_code_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)) + ((dst_negative_scale_weighted_scale_firstentriesentryleft) + (dst_negative_scale_weighted_scale_firstentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryleftpositive. ff_h_pvs_weighted_scale_firstentriesentryleftpositive + S (dst_positive_weighted_scale_firstentriesentryleft) = S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryleft)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryleftpositive. dst_positive_code_weighted_scale_firstentriesentryleft = ff_q_pvs_weighted_scale_firstentriesentryleftpositive * S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryleft) + (dst_positive_weighted_scale_firstentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryleftnegative. ff_h_pvs_weighted_scale_firstentriesentryleftnegative + S (dst_negative_weighted_scale_firstentriesentryleft) = S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryleft)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryleftnegative. dst_negative_code_weighted_scale_firstentriesentryleft = ff_q_pvs_weighted_scale_firstentriesentryleftnegative * S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryleft) + (dst_negative_weighted_scale_firstentriesentryleft))) /\ (exists ge_balance_positive_weighted_scale_firstentriesentryleftvalue ge_balance_negative_weighted_scale_firstentriesentryleftvalue. (((((sto_left_weighted_scale_firstentries) = 2 * (ge_balance_positive_weighted_scale_firstentriesentryleftvalue) /\ (ge_balance_negative_weighted_scale_firstentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryleftvaluedecode. (((sto_left_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstentriesentryleftvalue) = S ge_signed_half_weighted_scale_firstentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_scale_firstentriesentryleft) + ge_balance_negative_weighted_scale_firstentriesentryleftvalue = (dst_negative_weighted_scale_firstentriesentryleft) + ge_balance_positive_weighted_scale_firstentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_firstentriesentryright dst_positive_scale_weighted_scale_firstentriesentryright dst_negative_code_weighted_scale_firstentriesentryright dst_negative_scale_weighted_scale_firstentriesentryright dst_positive_weighted_scale_firstentriesentryright dst_negative_weighted_scale_firstentriesentryright. (((F) = (((((dst_positive_code_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright)) * S ((dst_positive_code_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright)) + ((dst_positive_scale_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright))) + (((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) * S ((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) + ((dst_negative_scale_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)))) * S ((((dst_positive_code_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright)) * S ((dst_positive_code_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright)) + ((dst_positive_scale_weighted_scale_firstentriesentryright) + (dst_positive_scale_weighted_scale_firstentriesentryright))) + (((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) * S ((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) + ((dst_negative_scale_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)))) + ((((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) * S ((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) + ((dst_negative_scale_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright))) + (((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) * S ((dst_negative_code_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)) + ((dst_negative_scale_weighted_scale_firstentriesentryright) + (dst_negative_scale_weighted_scale_firstentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryrightpositive. ff_h_pvs_weighted_scale_firstentriesentryrightpositive + S (dst_positive_weighted_scale_firstentriesentryright) = S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryright)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryrightpositive. dst_positive_code_weighted_scale_firstentriesentryright = ff_q_pvs_weighted_scale_firstentriesentryrightpositive * S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryright) + (dst_positive_weighted_scale_firstentriesentryright))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryrightnegative. ff_h_pvs_weighted_scale_firstentriesentryrightnegative + S (dst_negative_weighted_scale_firstentriesentryright) = S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryright)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryrightnegative. dst_negative_code_weighted_scale_firstentriesentryright = ff_q_pvs_weighted_scale_firstentriesentryrightnegative * S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryright) + (dst_negative_weighted_scale_firstentriesentryright))) /\ (exists ge_balance_positive_weighted_scale_firstentriesentryrightvalue ge_balance_negative_weighted_scale_firstentriesentryrightvalue. (((((sto_right_weighted_scale_firstentries) = 2 * (ge_balance_positive_weighted_scale_firstentriesentryrightvalue) /\ (ge_balance_negative_weighted_scale_firstentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryrightvaluedecode. (((sto_right_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstentriesentryrightvalue) = S ge_signed_half_weighted_scale_firstentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_scale_firstentriesentryright) + ge_balance_negative_weighted_scale_firstentriesentryrightvalue = (dst_negative_weighted_scale_firstentriesentryright) + ge_balance_positive_weighted_scale_firstentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_firstentriesentryoutput dst_positive_scale_weighted_scale_firstentriesentryoutput dst_negative_code_weighted_scale_firstentriesentryoutput dst_negative_scale_weighted_scale_firstentriesentryoutput dst_positive_weighted_scale_firstentriesentryoutput dst_negative_weighted_scale_firstentriesentryoutput. (((P) = (((((dst_positive_code_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_positive_code_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput)) + ((dst_positive_scale_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput))) + (((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) + ((dst_negative_scale_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)))) * S ((((dst_positive_code_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_positive_code_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput)) + ((dst_positive_scale_weighted_scale_firstentriesentryoutput) + (dst_positive_scale_weighted_scale_firstentriesentryoutput))) + (((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) + ((dst_negative_scale_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)))) + ((((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) + ((dst_negative_scale_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput))) + (((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) * S ((dst_negative_code_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)) + ((dst_negative_scale_weighted_scale_firstentriesentryoutput) + (dst_negative_scale_weighted_scale_firstentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryoutputpositive. ff_h_pvs_weighted_scale_firstentriesentryoutputpositive + S (dst_positive_weighted_scale_firstentriesentryoutput) = S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryoutputpositive. dst_positive_code_weighted_scale_firstentriesentryoutput = ff_q_pvs_weighted_scale_firstentriesentryoutputpositive * S ((S (sto_index_weighted_scale_firstentries)) * dst_positive_scale_weighted_scale_firstentriesentryoutput) + (dst_positive_weighted_scale_firstentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scale_firstentriesentryoutputnegative. ff_h_pvs_weighted_scale_firstentriesentryoutputnegative + S (dst_negative_weighted_scale_firstentriesentryoutput) = S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_firstentriesentryoutputnegative. dst_negative_code_weighted_scale_firstentriesentryoutput = ff_q_pvs_weighted_scale_firstentriesentryoutputnegative * S ((S (sto_index_weighted_scale_firstentries)) * dst_negative_scale_weighted_scale_firstentriesentryoutput) + (dst_negative_weighted_scale_firstentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scale_firstentriesentryoutputvalue ge_balance_negative_weighted_scale_firstentriesentryoutputvalue. (((((sto_output_weighted_scale_firstentries) = 2 * (ge_balance_positive_weighted_scale_firstentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scale_firstentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryoutputvaluedecode. (((sto_output_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_firstentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scale_firstentriesentryoutputvalue) = S ge_signed_half_weighted_scale_firstentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scale_firstentriesentryoutput) + ge_balance_negative_weighted_scale_firstentriesentryoutputvalue = (dst_negative_weighted_scale_firstentriesentryoutput) + ge_balance_positive_weighted_scale_firstentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scale_firstentriesentryoperation sto_an_weighted_scale_firstentriesentryoperation sto_bp_weighted_scale_firstentriesentryoperation sto_bn_weighted_scale_firstentriesentryoperation sto_cp_weighted_scale_firstentriesentryoperation sto_cn_weighted_scale_firstentriesentryoperation. (((((sto_left_weighted_scale_firstentries) = 2 * (sto_ap_weighted_scale_firstentriesentryoperation) /\ (sto_an_weighted_scale_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryoperationleft. (((sto_left_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryoperationleft + 1 /\ (sto_ap_weighted_scale_firstentriesentryoperation) = 0) /\ (sto_an_weighted_scale_firstentriesentryoperation) = S ge_signed_half_weighted_scale_firstentriesentryoperationleft))) /\ ((((((sto_right_weighted_scale_firstentries) = 2 * (sto_bp_weighted_scale_firstentriesentryoperation) /\ (sto_bn_weighted_scale_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryoperationright. (((sto_right_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryoperationright + 1 /\ (sto_bp_weighted_scale_firstentriesentryoperation) = 0) /\ (sto_bn_weighted_scale_firstentriesentryoperation) = S ge_signed_half_weighted_scale_firstentriesentryoperationright))) /\ ((((((sto_output_weighted_scale_firstentries) = 2 * (sto_cp_weighted_scale_firstentriesentryoperation) /\ (sto_cn_weighted_scale_firstentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_firstentriesentryoperationoutput. (((sto_output_weighted_scale_firstentries) = 2 * ge_signed_half_weighted_scale_firstentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scale_firstentriesentryoperation) = 0) /\ (sto_cn_weighted_scale_firstentriesentryoperation) = S ge_signed_half_weighted_scale_firstentriesentryoperationoutput))) /\ ((sto_ap_weighted_scale_firstentriesentryoperation * sto_bp_weighted_scale_firstentriesentryoperation + sto_an_weighted_scale_firstentriesentryoperation * sto_bn_weighted_scale_firstentriesentryoperation) + sto_cn_weighted_scale_firstentriesentryoperation = (sto_ap_weighted_scale_firstentriesentryoperation * sto_bn_weighted_scale_firstentriesentryoperation + sto_an_weighted_scale_firstentriesentryoperation * sto_bp_weighted_scale_firstentriesentryoperation) + sto_cp_weighted_scale_firstentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_scale_secondleft_table dst_positive_scale_weighted_scale_secondleft_table dst_negative_code_weighted_scale_secondleft_table dst_negative_scale_weighted_scale_secondleft_table. (((W) = (((((dst_positive_code_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table)) * S ((dst_positive_code_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table)) + ((dst_positive_scale_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table))) + (((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) * S ((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) + ((dst_negative_scale_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)))) * S ((((dst_positive_code_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table)) * S ((dst_positive_code_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table)) + ((dst_positive_scale_weighted_scale_secondleft_table) + (dst_positive_scale_weighted_scale_secondleft_table))) + (((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) * S ((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) + ((dst_negative_scale_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)))) + ((((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) * S ((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) + ((dst_negative_scale_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table))) + (((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) * S ((dst_negative_code_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)) + ((dst_negative_scale_weighted_scale_secondleft_table) + (dst_negative_scale_weighted_scale_secondleft_table)))))) /\ (forall dst_index_weighted_scale_secondleft_table. (exists pvs_le_gap_weighted_scale_secondleft_tabledomain. pvs_le_gap_weighted_scale_secondleft_tabledomain + (dst_index_weighted_scale_secondleft_table) = (l)) -> exists dst_positive_weighted_scale_secondleft_table dst_negative_weighted_scale_secondleft_table dst_value_weighted_scale_secondleft_table. ((((exists ff_h_pvs_weighted_scale_secondleft_tableentrypositive. ff_h_pvs_weighted_scale_secondleft_tableentrypositive + S (dst_positive_weighted_scale_secondleft_table) = S ((S (dst_index_weighted_scale_secondleft_table)) * dst_positive_scale_weighted_scale_secondleft_table)) /\ exists ff_q_pvs_weighted_scale_secondleft_tableentrypositive. dst_positive_code_weighted_scale_secondleft_table = ff_q_pvs_weighted_scale_secondleft_tableentrypositive * S ((S (dst_index_weighted_scale_secondleft_table)) * dst_positive_scale_weighted_scale_secondleft_table) + (dst_positive_weighted_scale_secondleft_table))) /\ (((((exists ff_h_pvs_weighted_scale_secondleft_tableentrynegative. ff_h_pvs_weighted_scale_secondleft_tableentrynegative + S (dst_negative_weighted_scale_secondleft_table) = S ((S (dst_index_weighted_scale_secondleft_table)) * dst_negative_scale_weighted_scale_secondleft_table)) /\ exists ff_q_pvs_weighted_scale_secondleft_tableentrynegative. dst_negative_code_weighted_scale_secondleft_table = ff_q_pvs_weighted_scale_secondleft_tableentrynegative * S ((S (dst_index_weighted_scale_secondleft_table)) * dst_negative_scale_weighted_scale_secondleft_table) + (dst_negative_weighted_scale_secondleft_table))) /\ (exists ge_balance_positive_weighted_scale_secondleft_tableentryvalue ge_balance_negative_weighted_scale_secondleft_tableentryvalue. (((((dst_value_weighted_scale_secondleft_table) = 2 * (ge_balance_positive_weighted_scale_secondleft_tableentryvalue) /\ (ge_balance_negative_weighted_scale_secondleft_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondleft_tableentryvaluedecode. (((dst_value_weighted_scale_secondleft_table) = 2 * ge_signed_half_weighted_scale_secondleft_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondleft_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondleft_tableentryvalue) = S ge_signed_half_weighted_scale_secondleft_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_secondleft_table) + ge_balance_negative_weighted_scale_secondleft_tableentryvalue = (dst_negative_weighted_scale_secondleft_table) + ge_balance_positive_weighted_scale_secondleft_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_secondright_table dst_positive_scale_weighted_scale_secondright_table dst_negative_code_weighted_scale_secondright_table dst_negative_scale_weighted_scale_secondright_table. (((G) = (((((dst_positive_code_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table)) * S ((dst_positive_code_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table)) + ((dst_positive_scale_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table))) + (((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) * S ((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) + ((dst_negative_scale_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)))) * S ((((dst_positive_code_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table)) * S ((dst_positive_code_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table)) + ((dst_positive_scale_weighted_scale_secondright_table) + (dst_positive_scale_weighted_scale_secondright_table))) + (((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) * S ((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) + ((dst_negative_scale_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)))) + ((((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) * S ((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) + ((dst_negative_scale_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table))) + (((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) * S ((dst_negative_code_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)) + ((dst_negative_scale_weighted_scale_secondright_table) + (dst_negative_scale_weighted_scale_secondright_table)))))) /\ (forall dst_index_weighted_scale_secondright_table. (exists pvs_le_gap_weighted_scale_secondright_tabledomain. pvs_le_gap_weighted_scale_secondright_tabledomain + (dst_index_weighted_scale_secondright_table) = (l)) -> exists dst_positive_weighted_scale_secondright_table dst_negative_weighted_scale_secondright_table dst_value_weighted_scale_secondright_table. ((((exists ff_h_pvs_weighted_scale_secondright_tableentrypositive. ff_h_pvs_weighted_scale_secondright_tableentrypositive + S (dst_positive_weighted_scale_secondright_table) = S ((S (dst_index_weighted_scale_secondright_table)) * dst_positive_scale_weighted_scale_secondright_table)) /\ exists ff_q_pvs_weighted_scale_secondright_tableentrypositive. dst_positive_code_weighted_scale_secondright_table = ff_q_pvs_weighted_scale_secondright_tableentrypositive * S ((S (dst_index_weighted_scale_secondright_table)) * dst_positive_scale_weighted_scale_secondright_table) + (dst_positive_weighted_scale_secondright_table))) /\ (((((exists ff_h_pvs_weighted_scale_secondright_tableentrynegative. ff_h_pvs_weighted_scale_secondright_tableentrynegative + S (dst_negative_weighted_scale_secondright_table) = S ((S (dst_index_weighted_scale_secondright_table)) * dst_negative_scale_weighted_scale_secondright_table)) /\ exists ff_q_pvs_weighted_scale_secondright_tableentrynegative. dst_negative_code_weighted_scale_secondright_table = ff_q_pvs_weighted_scale_secondright_tableentrynegative * S ((S (dst_index_weighted_scale_secondright_table)) * dst_negative_scale_weighted_scale_secondright_table) + (dst_negative_weighted_scale_secondright_table))) /\ (exists ge_balance_positive_weighted_scale_secondright_tableentryvalue ge_balance_negative_weighted_scale_secondright_tableentryvalue. (((((dst_value_weighted_scale_secondright_table) = 2 * (ge_balance_positive_weighted_scale_secondright_tableentryvalue) /\ (ge_balance_negative_weighted_scale_secondright_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondright_tableentryvaluedecode. (((dst_value_weighted_scale_secondright_table) = 2 * ge_signed_half_weighted_scale_secondright_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondright_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondright_tableentryvalue) = S ge_signed_half_weighted_scale_secondright_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_secondright_table) + ge_balance_negative_weighted_scale_secondright_tableentryvalue = (dst_negative_weighted_scale_secondright_table) + ge_balance_positive_weighted_scale_secondright_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_secondoutput_table dst_positive_scale_weighted_scale_secondoutput_table dst_negative_code_weighted_scale_secondoutput_table dst_negative_scale_weighted_scale_secondoutput_table. (((Q) = (((((dst_positive_code_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table)) * S ((dst_positive_code_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table)) + ((dst_positive_scale_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table))) + (((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) * S ((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) + ((dst_negative_scale_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)))) * S ((((dst_positive_code_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table)) * S ((dst_positive_code_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table)) + ((dst_positive_scale_weighted_scale_secondoutput_table) + (dst_positive_scale_weighted_scale_secondoutput_table))) + (((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) * S ((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) + ((dst_negative_scale_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)))) + ((((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) * S ((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) + ((dst_negative_scale_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table))) + (((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) * S ((dst_negative_code_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)) + ((dst_negative_scale_weighted_scale_secondoutput_table) + (dst_negative_scale_weighted_scale_secondoutput_table)))))) /\ (forall dst_index_weighted_scale_secondoutput_table. (exists pvs_le_gap_weighted_scale_secondoutput_tabledomain. pvs_le_gap_weighted_scale_secondoutput_tabledomain + (dst_index_weighted_scale_secondoutput_table) = (l)) -> exists dst_positive_weighted_scale_secondoutput_table dst_negative_weighted_scale_secondoutput_table dst_value_weighted_scale_secondoutput_table. ((((exists ff_h_pvs_weighted_scale_secondoutput_tableentrypositive. ff_h_pvs_weighted_scale_secondoutput_tableentrypositive + S (dst_positive_weighted_scale_secondoutput_table) = S ((S (dst_index_weighted_scale_secondoutput_table)) * dst_positive_scale_weighted_scale_secondoutput_table)) /\ exists ff_q_pvs_weighted_scale_secondoutput_tableentrypositive. dst_positive_code_weighted_scale_secondoutput_table = ff_q_pvs_weighted_scale_secondoutput_tableentrypositive * S ((S (dst_index_weighted_scale_secondoutput_table)) * dst_positive_scale_weighted_scale_secondoutput_table) + (dst_positive_weighted_scale_secondoutput_table))) /\ (((((exists ff_h_pvs_weighted_scale_secondoutput_tableentrynegative. ff_h_pvs_weighted_scale_secondoutput_tableentrynegative + S (dst_negative_weighted_scale_secondoutput_table) = S ((S (dst_index_weighted_scale_secondoutput_table)) * dst_negative_scale_weighted_scale_secondoutput_table)) /\ exists ff_q_pvs_weighted_scale_secondoutput_tableentrynegative. dst_negative_code_weighted_scale_secondoutput_table = ff_q_pvs_weighted_scale_secondoutput_tableentrynegative * S ((S (dst_index_weighted_scale_secondoutput_table)) * dst_negative_scale_weighted_scale_secondoutput_table) + (dst_negative_weighted_scale_secondoutput_table))) /\ (exists ge_balance_positive_weighted_scale_secondoutput_tableentryvalue ge_balance_negative_weighted_scale_secondoutput_tableentryvalue. (((((dst_value_weighted_scale_secondoutput_table) = 2 * (ge_balance_positive_weighted_scale_secondoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_secondoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondoutput_tableentryvaluedecode. (((dst_value_weighted_scale_secondoutput_table) = 2 * ge_signed_half_weighted_scale_secondoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondoutput_tableentryvalue) = S ge_signed_half_weighted_scale_secondoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_secondoutput_table) + ge_balance_negative_weighted_scale_secondoutput_tableentryvalue = (dst_negative_weighted_scale_secondoutput_table) + ge_balance_positive_weighted_scale_secondoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scale_secondentries. (exists pvs_gap_weighted_scale_secondentriesbound. pvs_gap_weighted_scale_secondentriesbound + S (sto_index_weighted_scale_secondentries) = (l)) -> exists sto_left_weighted_scale_secondentries sto_right_weighted_scale_secondentries sto_output_weighted_scale_secondentries. ((exists dst_positive_code_weighted_scale_secondentriesentryleft dst_positive_scale_weighted_scale_secondentriesentryleft dst_negative_code_weighted_scale_secondentriesentryleft dst_negative_scale_weighted_scale_secondentriesentryleft dst_positive_weighted_scale_secondentriesentryleft dst_negative_weighted_scale_secondentriesentryleft. (((W) = (((((dst_positive_code_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft)) * S ((dst_positive_code_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft)) + ((dst_positive_scale_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft))) + (((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) * S ((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) + ((dst_negative_scale_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)))) * S ((((dst_positive_code_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft)) * S ((dst_positive_code_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft)) + ((dst_positive_scale_weighted_scale_secondentriesentryleft) + (dst_positive_scale_weighted_scale_secondentriesentryleft))) + (((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) * S ((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) + ((dst_negative_scale_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)))) + ((((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) * S ((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) + ((dst_negative_scale_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft))) + (((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) * S ((dst_negative_code_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)) + ((dst_negative_scale_weighted_scale_secondentriesentryleft) + (dst_negative_scale_weighted_scale_secondentriesentryleft)))))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryleftpositive. ff_h_pvs_weighted_scale_secondentriesentryleftpositive + S (dst_positive_weighted_scale_secondentriesentryleft) = S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryleft)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryleftpositive. dst_positive_code_weighted_scale_secondentriesentryleft = ff_q_pvs_weighted_scale_secondentriesentryleftpositive * S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryleft) + (dst_positive_weighted_scale_secondentriesentryleft))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryleftnegative. ff_h_pvs_weighted_scale_secondentriesentryleftnegative + S (dst_negative_weighted_scale_secondentriesentryleft) = S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryleft)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryleftnegative. dst_negative_code_weighted_scale_secondentriesentryleft = ff_q_pvs_weighted_scale_secondentriesentryleftnegative * S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryleft) + (dst_negative_weighted_scale_secondentriesentryleft))) /\ (exists ge_balance_positive_weighted_scale_secondentriesentryleftvalue ge_balance_negative_weighted_scale_secondentriesentryleftvalue. (((((sto_left_weighted_scale_secondentries) = 2 * (ge_balance_positive_weighted_scale_secondentriesentryleftvalue) /\ (ge_balance_negative_weighted_scale_secondentriesentryleftvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryleftvaluedecode. (((sto_left_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryleftvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondentriesentryleftvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondentriesentryleftvalue) = S ge_signed_half_weighted_scale_secondentriesentryleftvaluedecode))) /\ ((dst_positive_weighted_scale_secondentriesentryleft) + ge_balance_negative_weighted_scale_secondentriesentryleftvalue = (dst_negative_weighted_scale_secondentriesentryleft) + ge_balance_positive_weighted_scale_secondentriesentryleftvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_secondentriesentryright dst_positive_scale_weighted_scale_secondentriesentryright dst_negative_code_weighted_scale_secondentriesentryright dst_negative_scale_weighted_scale_secondentriesentryright dst_positive_weighted_scale_secondentriesentryright dst_negative_weighted_scale_secondentriesentryright. (((G) = (((((dst_positive_code_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright)) * S ((dst_positive_code_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright)) + ((dst_positive_scale_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright))) + (((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) * S ((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) + ((dst_negative_scale_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)))) * S ((((dst_positive_code_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright)) * S ((dst_positive_code_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright)) + ((dst_positive_scale_weighted_scale_secondentriesentryright) + (dst_positive_scale_weighted_scale_secondentriesentryright))) + (((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) * S ((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) + ((dst_negative_scale_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)))) + ((((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) * S ((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) + ((dst_negative_scale_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright))) + (((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) * S ((dst_negative_code_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)) + ((dst_negative_scale_weighted_scale_secondentriesentryright) + (dst_negative_scale_weighted_scale_secondentriesentryright)))))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryrightpositive. ff_h_pvs_weighted_scale_secondentriesentryrightpositive + S (dst_positive_weighted_scale_secondentriesentryright) = S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryright)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryrightpositive. dst_positive_code_weighted_scale_secondentriesentryright = ff_q_pvs_weighted_scale_secondentriesentryrightpositive * S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryright) + (dst_positive_weighted_scale_secondentriesentryright))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryrightnegative. ff_h_pvs_weighted_scale_secondentriesentryrightnegative + S (dst_negative_weighted_scale_secondentriesentryright) = S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryright)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryrightnegative. dst_negative_code_weighted_scale_secondentriesentryright = ff_q_pvs_weighted_scale_secondentriesentryrightnegative * S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryright) + (dst_negative_weighted_scale_secondentriesentryright))) /\ (exists ge_balance_positive_weighted_scale_secondentriesentryrightvalue ge_balance_negative_weighted_scale_secondentriesentryrightvalue. (((((sto_right_weighted_scale_secondentries) = 2 * (ge_balance_positive_weighted_scale_secondentriesentryrightvalue) /\ (ge_balance_negative_weighted_scale_secondentriesentryrightvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryrightvaluedecode. (((sto_right_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryrightvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondentriesentryrightvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondentriesentryrightvalue) = S ge_signed_half_weighted_scale_secondentriesentryrightvaluedecode))) /\ ((dst_positive_weighted_scale_secondentriesentryright) + ge_balance_negative_weighted_scale_secondentriesentryrightvalue = (dst_negative_weighted_scale_secondentriesentryright) + ge_balance_positive_weighted_scale_secondentriesentryrightvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_secondentriesentryoutput dst_positive_scale_weighted_scale_secondentriesentryoutput dst_negative_code_weighted_scale_secondentriesentryoutput dst_negative_scale_weighted_scale_secondentriesentryoutput dst_positive_weighted_scale_secondentriesentryoutput dst_negative_weighted_scale_secondentriesentryoutput. (((Q) = (((((dst_positive_code_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_positive_code_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput)) + ((dst_positive_scale_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput))) + (((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) + ((dst_negative_scale_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)))) * S ((((dst_positive_code_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_positive_code_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput)) + ((dst_positive_scale_weighted_scale_secondentriesentryoutput) + (dst_positive_scale_weighted_scale_secondentriesentryoutput))) + (((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) + ((dst_negative_scale_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)))) + ((((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) + ((dst_negative_scale_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput))) + (((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) * S ((dst_negative_code_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)) + ((dst_negative_scale_weighted_scale_secondentriesentryoutput) + (dst_negative_scale_weighted_scale_secondentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryoutputpositive. ff_h_pvs_weighted_scale_secondentriesentryoutputpositive + S (dst_positive_weighted_scale_secondentriesentryoutput) = S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryoutputpositive. dst_positive_code_weighted_scale_secondentriesentryoutput = ff_q_pvs_weighted_scale_secondentriesentryoutputpositive * S ((S (sto_index_weighted_scale_secondentries)) * dst_positive_scale_weighted_scale_secondentriesentryoutput) + (dst_positive_weighted_scale_secondentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scale_secondentriesentryoutputnegative. ff_h_pvs_weighted_scale_secondentriesentryoutputnegative + S (dst_negative_weighted_scale_secondentriesentryoutput) = S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_secondentriesentryoutputnegative. dst_negative_code_weighted_scale_secondentriesentryoutput = ff_q_pvs_weighted_scale_secondentriesentryoutputnegative * S ((S (sto_index_weighted_scale_secondentries)) * dst_negative_scale_weighted_scale_secondentriesentryoutput) + (dst_negative_weighted_scale_secondentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scale_secondentriesentryoutputvalue ge_balance_negative_weighted_scale_secondentriesentryoutputvalue. (((((sto_output_weighted_scale_secondentries) = 2 * (ge_balance_positive_weighted_scale_secondentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scale_secondentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryoutputvaluedecode. (((sto_output_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_secondentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scale_secondentriesentryoutputvalue) = S ge_signed_half_weighted_scale_secondentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scale_secondentriesentryoutput) + ge_balance_negative_weighted_scale_secondentriesentryoutputvalue = (dst_negative_weighted_scale_secondentriesentryoutput) + ge_balance_positive_weighted_scale_secondentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scale_secondentriesentryoperation sto_an_weighted_scale_secondentriesentryoperation sto_bp_weighted_scale_secondentriesentryoperation sto_bn_weighted_scale_secondentriesentryoperation sto_cp_weighted_scale_secondentriesentryoperation sto_cn_weighted_scale_secondentriesentryoperation. (((((sto_left_weighted_scale_secondentries) = 2 * (sto_ap_weighted_scale_secondentriesentryoperation) /\ (sto_an_weighted_scale_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryoperationleft. (((sto_left_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryoperationleft + 1 /\ (sto_ap_weighted_scale_secondentriesentryoperation) = 0) /\ (sto_an_weighted_scale_secondentriesentryoperation) = S ge_signed_half_weighted_scale_secondentriesentryoperationleft))) /\ ((((((sto_right_weighted_scale_secondentries) = 2 * (sto_bp_weighted_scale_secondentriesentryoperation) /\ (sto_bn_weighted_scale_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryoperationright. (((sto_right_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryoperationright + 1 /\ (sto_bp_weighted_scale_secondentriesentryoperation) = 0) /\ (sto_bn_weighted_scale_secondentriesentryoperation) = S ge_signed_half_weighted_scale_secondentriesentryoperationright))) /\ ((((((sto_output_weighted_scale_secondentries) = 2 * (sto_cp_weighted_scale_secondentriesentryoperation) /\ (sto_cn_weighted_scale_secondentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_secondentriesentryoperationoutput. (((sto_output_weighted_scale_secondentries) = 2 * ge_signed_half_weighted_scale_secondentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scale_secondentriesentryoperation) = 0) /\ (sto_cn_weighted_scale_secondentriesentryoperation) = S ge_signed_half_weighted_scale_secondentriesentryoperationoutput))) /\ ((sto_ap_weighted_scale_secondentriesentryoperation * sto_bp_weighted_scale_secondentriesentryoperation + sto_an_weighted_scale_secondentriesentryoperation * sto_bn_weighted_scale_secondentriesentryoperation) + sto_cn_weighted_scale_secondentriesentryoperation = (sto_ap_weighted_scale_secondentriesentryoperation * sto_bn_weighted_scale_secondentriesentryoperation + sto_an_weighted_scale_secondentriesentryoperation * sto_bp_weighted_scale_secondentriesentryoperation) + sto_cp_weighted_scale_secondentriesentryoperation))))))))))))))))))) -> (((exists dst_positive_code_weighted_scale_resultinput_table dst_positive_scale_weighted_scale_resultinput_table dst_negative_code_weighted_scale_resultinput_table dst_negative_scale_weighted_scale_resultinput_table. (((P) = (((((dst_positive_code_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table)) * S ((dst_positive_code_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table)) + ((dst_positive_scale_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table))) + (((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) * S ((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) + ((dst_negative_scale_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)))) * S ((((dst_positive_code_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table)) * S ((dst_positive_code_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table)) + ((dst_positive_scale_weighted_scale_resultinput_table) + (dst_positive_scale_weighted_scale_resultinput_table))) + (((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) * S ((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) + ((dst_negative_scale_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)))) + ((((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) * S ((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) + ((dst_negative_scale_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table))) + (((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) * S ((dst_negative_code_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)) + ((dst_negative_scale_weighted_scale_resultinput_table) + (dst_negative_scale_weighted_scale_resultinput_table)))))) /\ (forall dst_index_weighted_scale_resultinput_table. (exists pvs_le_gap_weighted_scale_resultinput_tabledomain. pvs_le_gap_weighted_scale_resultinput_tabledomain + (dst_index_weighted_scale_resultinput_table) = (l)) -> exists dst_positive_weighted_scale_resultinput_table dst_negative_weighted_scale_resultinput_table dst_value_weighted_scale_resultinput_table. ((((exists ff_h_pvs_weighted_scale_resultinput_tableentrypositive. ff_h_pvs_weighted_scale_resultinput_tableentrypositive + S (dst_positive_weighted_scale_resultinput_table) = S ((S (dst_index_weighted_scale_resultinput_table)) * dst_positive_scale_weighted_scale_resultinput_table)) /\ exists ff_q_pvs_weighted_scale_resultinput_tableentrypositive. dst_positive_code_weighted_scale_resultinput_table = ff_q_pvs_weighted_scale_resultinput_tableentrypositive * S ((S (dst_index_weighted_scale_resultinput_table)) * dst_positive_scale_weighted_scale_resultinput_table) + (dst_positive_weighted_scale_resultinput_table))) /\ (((((exists ff_h_pvs_weighted_scale_resultinput_tableentrynegative. ff_h_pvs_weighted_scale_resultinput_tableentrynegative + S (dst_negative_weighted_scale_resultinput_table) = S ((S (dst_index_weighted_scale_resultinput_table)) * dst_negative_scale_weighted_scale_resultinput_table)) /\ exists ff_q_pvs_weighted_scale_resultinput_tableentrynegative. dst_negative_code_weighted_scale_resultinput_table = ff_q_pvs_weighted_scale_resultinput_tableentrynegative * S ((S (dst_index_weighted_scale_resultinput_table)) * dst_negative_scale_weighted_scale_resultinput_table) + (dst_negative_weighted_scale_resultinput_table))) /\ (exists ge_balance_positive_weighted_scale_resultinput_tableentryvalue ge_balance_negative_weighted_scale_resultinput_tableentryvalue. (((((dst_value_weighted_scale_resultinput_table) = 2 * (ge_balance_positive_weighted_scale_resultinput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_resultinput_tableentryvaluedecode. (((dst_value_weighted_scale_resultinput_table) = 2 * ge_signed_half_weighted_scale_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_resultinput_tableentryvalue) = S ge_signed_half_weighted_scale_resultinput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_resultinput_table) + ge_balance_negative_weighted_scale_resultinput_tableentryvalue = (dst_negative_weighted_scale_resultinput_table) + ge_balance_positive_weighted_scale_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_resultoutput_table dst_positive_scale_weighted_scale_resultoutput_table dst_negative_code_weighted_scale_resultoutput_table dst_negative_scale_weighted_scale_resultoutput_table. (((Q) = (((((dst_positive_code_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table)) * S ((dst_positive_code_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table)) + ((dst_positive_scale_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table))) + (((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) * S ((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) + ((dst_negative_scale_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)))) * S ((((dst_positive_code_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table)) * S ((dst_positive_code_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table)) + ((dst_positive_scale_weighted_scale_resultoutput_table) + (dst_positive_scale_weighted_scale_resultoutput_table))) + (((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) * S ((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) + ((dst_negative_scale_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)))) + ((((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) * S ((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) + ((dst_negative_scale_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table))) + (((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) * S ((dst_negative_code_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)) + ((dst_negative_scale_weighted_scale_resultoutput_table) + (dst_negative_scale_weighted_scale_resultoutput_table)))))) /\ (forall dst_index_weighted_scale_resultoutput_table. (exists pvs_le_gap_weighted_scale_resultoutput_tabledomain. pvs_le_gap_weighted_scale_resultoutput_tabledomain + (dst_index_weighted_scale_resultoutput_table) = (l)) -> exists dst_positive_weighted_scale_resultoutput_table dst_negative_weighted_scale_resultoutput_table dst_value_weighted_scale_resultoutput_table. ((((exists ff_h_pvs_weighted_scale_resultoutput_tableentrypositive. ff_h_pvs_weighted_scale_resultoutput_tableentrypositive + S (dst_positive_weighted_scale_resultoutput_table) = S ((S (dst_index_weighted_scale_resultoutput_table)) * dst_positive_scale_weighted_scale_resultoutput_table)) /\ exists ff_q_pvs_weighted_scale_resultoutput_tableentrypositive. dst_positive_code_weighted_scale_resultoutput_table = ff_q_pvs_weighted_scale_resultoutput_tableentrypositive * S ((S (dst_index_weighted_scale_resultoutput_table)) * dst_positive_scale_weighted_scale_resultoutput_table) + (dst_positive_weighted_scale_resultoutput_table))) /\ (((((exists ff_h_pvs_weighted_scale_resultoutput_tableentrynegative. ff_h_pvs_weighted_scale_resultoutput_tableentrynegative + S (dst_negative_weighted_scale_resultoutput_table) = S ((S (dst_index_weighted_scale_resultoutput_table)) * dst_negative_scale_weighted_scale_resultoutput_table)) /\ exists ff_q_pvs_weighted_scale_resultoutput_tableentrynegative. dst_negative_code_weighted_scale_resultoutput_table = ff_q_pvs_weighted_scale_resultoutput_tableentrynegative * S ((S (dst_index_weighted_scale_resultoutput_table)) * dst_negative_scale_weighted_scale_resultoutput_table) + (dst_negative_weighted_scale_resultoutput_table))) /\ (exists ge_balance_positive_weighted_scale_resultoutput_tableentryvalue ge_balance_negative_weighted_scale_resultoutput_tableentryvalue. (((((dst_value_weighted_scale_resultoutput_table) = 2 * (ge_balance_positive_weighted_scale_resultoutput_tableentryvalue) /\ (ge_balance_negative_weighted_scale_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_weighted_scale_resultoutput_tableentryvaluedecode. (((dst_value_weighted_scale_resultoutput_table) = 2 * ge_signed_half_weighted_scale_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_weighted_scale_resultoutput_tableentryvalue) = S ge_signed_half_weighted_scale_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_weighted_scale_resultoutput_table) + ge_balance_negative_weighted_scale_resultoutput_tableentryvalue = (dst_negative_weighted_scale_resultoutput_table) + ge_balance_positive_weighted_scale_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_weighted_scale_resultentries. (exists pvs_gap_weighted_scale_resultentriesbound. pvs_gap_weighted_scale_resultentriesbound + S (sto_index_weighted_scale_resultentries) = (l)) -> exists sto_input_weighted_scale_resultentries sto_output_weighted_scale_resultentries. ((exists dst_positive_code_weighted_scale_resultentriesentryinput dst_positive_scale_weighted_scale_resultentriesentryinput dst_negative_code_weighted_scale_resultentriesentryinput dst_negative_scale_weighted_scale_resultentriesentryinput dst_positive_weighted_scale_resultentriesentryinput dst_negative_weighted_scale_resultentriesentryinput. (((P) = (((((dst_positive_code_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput)) * S ((dst_positive_code_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput)) + ((dst_positive_scale_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput))) + (((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) * S ((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) + ((dst_negative_scale_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)))) * S ((((dst_positive_code_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput)) * S ((dst_positive_code_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput)) + ((dst_positive_scale_weighted_scale_resultentriesentryinput) + (dst_positive_scale_weighted_scale_resultentriesentryinput))) + (((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) * S ((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) + ((dst_negative_scale_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)))) + ((((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) * S ((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) + ((dst_negative_scale_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput))) + (((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) * S ((dst_negative_code_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)) + ((dst_negative_scale_weighted_scale_resultentriesentryinput) + (dst_negative_scale_weighted_scale_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_weighted_scale_resultentriesentryinputpositive. ff_h_pvs_weighted_scale_resultentriesentryinputpositive + S (dst_positive_weighted_scale_resultentriesentryinput) = S ((S (sto_index_weighted_scale_resultentries)) * dst_positive_scale_weighted_scale_resultentriesentryinput)) /\ exists ff_q_pvs_weighted_scale_resultentriesentryinputpositive. dst_positive_code_weighted_scale_resultentriesentryinput = ff_q_pvs_weighted_scale_resultentriesentryinputpositive * S ((S (sto_index_weighted_scale_resultentries)) * dst_positive_scale_weighted_scale_resultentriesentryinput) + (dst_positive_weighted_scale_resultentriesentryinput))) /\ (((((exists ff_h_pvs_weighted_scale_resultentriesentryinputnegative. ff_h_pvs_weighted_scale_resultentriesentryinputnegative + S (dst_negative_weighted_scale_resultentriesentryinput) = S ((S (sto_index_weighted_scale_resultentries)) * dst_negative_scale_weighted_scale_resultentriesentryinput)) /\ exists ff_q_pvs_weighted_scale_resultentriesentryinputnegative. dst_negative_code_weighted_scale_resultentriesentryinput = ff_q_pvs_weighted_scale_resultentriesentryinputnegative * S ((S (sto_index_weighted_scale_resultentries)) * dst_negative_scale_weighted_scale_resultentriesentryinput) + (dst_negative_weighted_scale_resultentriesentryinput))) /\ (exists ge_balance_positive_weighted_scale_resultentriesentryinputvalue ge_balance_negative_weighted_scale_resultentriesentryinputvalue. (((((sto_input_weighted_scale_resultentries) = 2 * (ge_balance_positive_weighted_scale_resultentriesentryinputvalue) /\ (ge_balance_negative_weighted_scale_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_weighted_scale_resultentriesentryinputvaluedecode. (((sto_input_weighted_scale_resultentries) = 2 * ge_signed_half_weighted_scale_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_weighted_scale_resultentriesentryinputvalue) = S ge_signed_half_weighted_scale_resultentriesentryinputvaluedecode))) /\ ((dst_positive_weighted_scale_resultentriesentryinput) + ge_balance_negative_weighted_scale_resultentriesentryinputvalue = (dst_negative_weighted_scale_resultentriesentryinput) + ge_balance_positive_weighted_scale_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_weighted_scale_resultentriesentryoutput dst_positive_scale_weighted_scale_resultentriesentryoutput dst_negative_code_weighted_scale_resultentriesentryoutput dst_negative_scale_weighted_scale_resultentriesentryoutput dst_positive_weighted_scale_resultentriesentryoutput dst_negative_weighted_scale_resultentriesentryoutput. (((Q) = (((((dst_positive_code_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_positive_code_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput)) + ((dst_positive_scale_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput))) + (((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) + ((dst_negative_scale_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)))) * S ((((dst_positive_code_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_positive_code_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput)) + ((dst_positive_scale_weighted_scale_resultentriesentryoutput) + (dst_positive_scale_weighted_scale_resultentriesentryoutput))) + (((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) + ((dst_negative_scale_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)))) + ((((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) + ((dst_negative_scale_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput))) + (((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) * S ((dst_negative_code_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)) + ((dst_negative_scale_weighted_scale_resultentriesentryoutput) + (dst_negative_scale_weighted_scale_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_weighted_scale_resultentriesentryoutputpositive. ff_h_pvs_weighted_scale_resultentriesentryoutputpositive + S (dst_positive_weighted_scale_resultentriesentryoutput) = S ((S (sto_index_weighted_scale_resultentries)) * dst_positive_scale_weighted_scale_resultentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_resultentriesentryoutputpositive. dst_positive_code_weighted_scale_resultentriesentryoutput = ff_q_pvs_weighted_scale_resultentriesentryoutputpositive * S ((S (sto_index_weighted_scale_resultentries)) * dst_positive_scale_weighted_scale_resultentriesentryoutput) + (dst_positive_weighted_scale_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_weighted_scale_resultentriesentryoutputnegative. ff_h_pvs_weighted_scale_resultentriesentryoutputnegative + S (dst_negative_weighted_scale_resultentriesentryoutput) = S ((S (sto_index_weighted_scale_resultentries)) * dst_negative_scale_weighted_scale_resultentriesentryoutput)) /\ exists ff_q_pvs_weighted_scale_resultentriesentryoutputnegative. dst_negative_code_weighted_scale_resultentriesentryoutput = ff_q_pvs_weighted_scale_resultentriesentryoutputnegative * S ((S (sto_index_weighted_scale_resultentries)) * dst_negative_scale_weighted_scale_resultentriesentryoutput) + (dst_negative_weighted_scale_resultentriesentryoutput))) /\ (exists ge_balance_positive_weighted_scale_resultentriesentryoutputvalue ge_balance_negative_weighted_scale_resultentriesentryoutputvalue. (((((sto_output_weighted_scale_resultentries) = 2 * (ge_balance_positive_weighted_scale_resultentriesentryoutputvalue) /\ (ge_balance_negative_weighted_scale_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_weighted_scale_resultentriesentryoutputvaluedecode. (((sto_output_weighted_scale_resultentries) = 2 * ge_signed_half_weighted_scale_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_weighted_scale_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_weighted_scale_resultentriesentryoutputvalue) = S ge_signed_half_weighted_scale_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_weighted_scale_resultentriesentryoutput) + ge_balance_negative_weighted_scale_resultentriesentryoutputvalue = (dst_negative_weighted_scale_resultentriesentryoutput) + ge_balance_positive_weighted_scale_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_weighted_scale_resultentriesentryoperation sto_an_weighted_scale_resultentriesentryoperation sto_bp_weighted_scale_resultentriesentryoperation sto_bn_weighted_scale_resultentriesentryoperation sto_cp_weighted_scale_resultentriesentryoperation sto_cn_weighted_scale_resultentriesentryoperation. (((((a) = 2 * (sto_ap_weighted_scale_resultentriesentryoperation) /\ (sto_an_weighted_scale_resultentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_weighted_scale_resultentriesentryoperationleft + 1 /\ (sto_ap_weighted_scale_resultentriesentryoperation) = 0) /\ (sto_an_weighted_scale_resultentriesentryoperation) = S ge_signed_half_weighted_scale_resultentriesentryoperationleft))) /\ ((((((sto_input_weighted_scale_resultentries) = 2 * (sto_bp_weighted_scale_resultentriesentryoperation) /\ (sto_bn_weighted_scale_resultentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_resultentriesentryoperationright. (((sto_input_weighted_scale_resultentries) = 2 * ge_signed_half_weighted_scale_resultentriesentryoperationright + 1 /\ (sto_bp_weighted_scale_resultentriesentryoperation) = 0) /\ (sto_bn_weighted_scale_resultentriesentryoperation) = S ge_signed_half_weighted_scale_resultentriesentryoperationright))) /\ ((((((sto_output_weighted_scale_resultentries) = 2 * (sto_cp_weighted_scale_resultentriesentryoperation) /\ (sto_cn_weighted_scale_resultentriesentryoperation) = 0) \/ exists ge_signed_half_weighted_scale_resultentriesentryoperationoutput. (((sto_output_weighted_scale_resultentries) = 2 * ge_signed_half_weighted_scale_resultentriesentryoperationoutput + 1 /\ (sto_cp_weighted_scale_resultentriesentryoperation) = 0) /\ (sto_cn_weighted_scale_resultentriesentryoperation) = S ge_signed_half_weighted_scale_resultentriesentryoperationoutput))) /\ ((sto_ap_weighted_scale_resultentriesentryoperation * sto_bp_weighted_scale_resultentriesentryoperation + sto_an_weighted_scale_resultentriesentryoperation * sto_bn_weighted_scale_resultentriesentryoperation) + sto_cn_weighted_scale_resultentriesentryoperation = (sto_ap_weighted_scale_resultentriesentryoperation * sto_bn_weighted_scale_resultentriesentryoperation + sto_an_weighted_scale_resultentriesentryoperation * sto_bp_weighted_scale_resultentriesentryoperation) + sto_cp_weighted_scale_resultentriesentryoperation)))))))))))))))