signed_table_scalar_restrict

Exact expanded first-order arithmetic statement

forall a F G l. (((exists dst_positive_code_scalar_restrict_inputinput_table dst_positive_scale_scalar_restrict_inputinput_table dst_negative_code_scalar_restrict_inputinput_table dst_negative_scale_scalar_restrict_inputinput_table. (((F) = (((((dst_positive_code_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table)) * S ((dst_positive_code_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table)) + ((dst_positive_scale_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table))) + (((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) * S ((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) + ((dst_negative_scale_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)))) * S ((((dst_positive_code_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table)) * S ((dst_positive_code_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table)) + ((dst_positive_scale_scalar_restrict_inputinput_table) + (dst_positive_scale_scalar_restrict_inputinput_table))) + (((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) * S ((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) + ((dst_negative_scale_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)))) + ((((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) * S ((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) + ((dst_negative_scale_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table))) + (((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) * S ((dst_negative_code_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)) + ((dst_negative_scale_scalar_restrict_inputinput_table) + (dst_negative_scale_scalar_restrict_inputinput_table)))))) /\ (forall dst_index_scalar_restrict_inputinput_table. (exists pvs_le_gap_scalar_restrict_inputinput_tabledomain. pvs_le_gap_scalar_restrict_inputinput_tabledomain + (dst_index_scalar_restrict_inputinput_table) = (S l)) -> exists dst_positive_scalar_restrict_inputinput_table dst_negative_scalar_restrict_inputinput_table dst_value_scalar_restrict_inputinput_table. ((((exists ff_h_pvs_scalar_restrict_inputinput_tableentrypositive. ff_h_pvs_scalar_restrict_inputinput_tableentrypositive + S (dst_positive_scalar_restrict_inputinput_table) = S ((S (dst_index_scalar_restrict_inputinput_table)) * dst_positive_scale_scalar_restrict_inputinput_table)) /\ exists ff_q_pvs_scalar_restrict_inputinput_tableentrypositive. dst_positive_code_scalar_restrict_inputinput_table = ff_q_pvs_scalar_restrict_inputinput_tableentrypositive * S ((S (dst_index_scalar_restrict_inputinput_table)) * dst_positive_scale_scalar_restrict_inputinput_table) + (dst_positive_scalar_restrict_inputinput_table))) /\ (((((exists ff_h_pvs_scalar_restrict_inputinput_tableentrynegative. ff_h_pvs_scalar_restrict_inputinput_tableentrynegative + S (dst_negative_scalar_restrict_inputinput_table) = S ((S (dst_index_scalar_restrict_inputinput_table)) * dst_negative_scale_scalar_restrict_inputinput_table)) /\ exists ff_q_pvs_scalar_restrict_inputinput_tableentrynegative. dst_negative_code_scalar_restrict_inputinput_table = ff_q_pvs_scalar_restrict_inputinput_tableentrynegative * S ((S (dst_index_scalar_restrict_inputinput_table)) * dst_negative_scale_scalar_restrict_inputinput_table) + (dst_negative_scalar_restrict_inputinput_table))) /\ (exists ge_balance_positive_scalar_restrict_inputinput_tableentryvalue ge_balance_negative_scalar_restrict_inputinput_tableentryvalue. (((((dst_value_scalar_restrict_inputinput_table) = 2 * (ge_balance_positive_scalar_restrict_inputinput_tableentryvalue) /\ (ge_balance_negative_scalar_restrict_inputinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_restrict_inputinput_tableentryvaluedecode. (((dst_value_scalar_restrict_inputinput_table) = 2 * ge_signed_half_scalar_restrict_inputinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_inputinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_restrict_inputinput_tableentryvalue) = S ge_signed_half_scalar_restrict_inputinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_restrict_inputinput_table) + ge_balance_negative_scalar_restrict_inputinput_tableentryvalue = (dst_negative_scalar_restrict_inputinput_table) + ge_balance_positive_scalar_restrict_inputinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_restrict_inputoutput_table dst_positive_scale_scalar_restrict_inputoutput_table dst_negative_code_scalar_restrict_inputoutput_table dst_negative_scale_scalar_restrict_inputoutput_table. (((G) = (((((dst_positive_code_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table)) * S ((dst_positive_code_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table)) + ((dst_positive_scale_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table))) + (((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) * S ((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) + ((dst_negative_scale_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)))) * S ((((dst_positive_code_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table)) * S ((dst_positive_code_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table)) + ((dst_positive_scale_scalar_restrict_inputoutput_table) + (dst_positive_scale_scalar_restrict_inputoutput_table))) + (((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) * S ((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) + ((dst_negative_scale_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)))) + ((((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) * S ((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) + ((dst_negative_scale_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table))) + (((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) * S ((dst_negative_code_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)) + ((dst_negative_scale_scalar_restrict_inputoutput_table) + (dst_negative_scale_scalar_restrict_inputoutput_table)))))) /\ (forall dst_index_scalar_restrict_inputoutput_table. (exists pvs_le_gap_scalar_restrict_inputoutput_tabledomain. pvs_le_gap_scalar_restrict_inputoutput_tabledomain + (dst_index_scalar_restrict_inputoutput_table) = (S l)) -> exists dst_positive_scalar_restrict_inputoutput_table dst_negative_scalar_restrict_inputoutput_table dst_value_scalar_restrict_inputoutput_table. ((((exists ff_h_pvs_scalar_restrict_inputoutput_tableentrypositive. ff_h_pvs_scalar_restrict_inputoutput_tableentrypositive + S (dst_positive_scalar_restrict_inputoutput_table) = S ((S (dst_index_scalar_restrict_inputoutput_table)) * dst_positive_scale_scalar_restrict_inputoutput_table)) /\ exists ff_q_pvs_scalar_restrict_inputoutput_tableentrypositive. dst_positive_code_scalar_restrict_inputoutput_table = ff_q_pvs_scalar_restrict_inputoutput_tableentrypositive * S ((S (dst_index_scalar_restrict_inputoutput_table)) * dst_positive_scale_scalar_restrict_inputoutput_table) + (dst_positive_scalar_restrict_inputoutput_table))) /\ (((((exists ff_h_pvs_scalar_restrict_inputoutput_tableentrynegative. ff_h_pvs_scalar_restrict_inputoutput_tableentrynegative + S (dst_negative_scalar_restrict_inputoutput_table) = S ((S (dst_index_scalar_restrict_inputoutput_table)) * dst_negative_scale_scalar_restrict_inputoutput_table)) /\ exists ff_q_pvs_scalar_restrict_inputoutput_tableentrynegative. dst_negative_code_scalar_restrict_inputoutput_table = ff_q_pvs_scalar_restrict_inputoutput_tableentrynegative * S ((S (dst_index_scalar_restrict_inputoutput_table)) * dst_negative_scale_scalar_restrict_inputoutput_table) + (dst_negative_scalar_restrict_inputoutput_table))) /\ (exists ge_balance_positive_scalar_restrict_inputoutput_tableentryvalue ge_balance_negative_scalar_restrict_inputoutput_tableentryvalue. (((((dst_value_scalar_restrict_inputoutput_table) = 2 * (ge_balance_positive_scalar_restrict_inputoutput_tableentryvalue) /\ (ge_balance_negative_scalar_restrict_inputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_restrict_inputoutput_tableentryvaluedecode. (((dst_value_scalar_restrict_inputoutput_table) = 2 * ge_signed_half_scalar_restrict_inputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_inputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_restrict_inputoutput_tableentryvalue) = S ge_signed_half_scalar_restrict_inputoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_restrict_inputoutput_table) + ge_balance_negative_scalar_restrict_inputoutput_tableentryvalue = (dst_negative_scalar_restrict_inputoutput_table) + ge_balance_positive_scalar_restrict_inputoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_restrict_inputentries. (exists pvs_gap_scalar_restrict_inputentriesbound. pvs_gap_scalar_restrict_inputentriesbound + S (sto_index_scalar_restrict_inputentries) = (S l)) -> exists sto_input_scalar_restrict_inputentries sto_output_scalar_restrict_inputentries. ((exists dst_positive_code_scalar_restrict_inputentriesentryinput dst_positive_scale_scalar_restrict_inputentriesentryinput dst_negative_code_scalar_restrict_inputentriesentryinput dst_negative_scale_scalar_restrict_inputentriesentryinput dst_positive_scalar_restrict_inputentriesentryinput dst_negative_scalar_restrict_inputentriesentryinput. (((F) = (((((dst_positive_code_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_positive_code_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput)) + ((dst_positive_scale_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput))) + (((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)))) * S ((((dst_positive_code_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_positive_code_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput)) + ((dst_positive_scale_scalar_restrict_inputentriesentryinput) + (dst_positive_scale_scalar_restrict_inputentriesentryinput))) + (((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)))) + ((((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput))) + (((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryinput) + (dst_negative_scale_scalar_restrict_inputentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_restrict_inputentriesentryinputpositive. ff_h_pvs_scalar_restrict_inputentriesentryinputpositive + S (dst_positive_scalar_restrict_inputentriesentryinput) = S ((S (sto_index_scalar_restrict_inputentries)) * dst_positive_scale_scalar_restrict_inputentriesentryinput)) /\ exists ff_q_pvs_scalar_restrict_inputentriesentryinputpositive. dst_positive_code_scalar_restrict_inputentriesentryinput = ff_q_pvs_scalar_restrict_inputentriesentryinputpositive * S ((S (sto_index_scalar_restrict_inputentries)) * dst_positive_scale_scalar_restrict_inputentriesentryinput) + (dst_positive_scalar_restrict_inputentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_restrict_inputentriesentryinputnegative. ff_h_pvs_scalar_restrict_inputentriesentryinputnegative + S (dst_negative_scalar_restrict_inputentriesentryinput) = S ((S (sto_index_scalar_restrict_inputentries)) * dst_negative_scale_scalar_restrict_inputentriesentryinput)) /\ exists ff_q_pvs_scalar_restrict_inputentriesentryinputnegative. dst_negative_code_scalar_restrict_inputentriesentryinput = ff_q_pvs_scalar_restrict_inputentriesentryinputnegative * S ((S (sto_index_scalar_restrict_inputentries)) * dst_negative_scale_scalar_restrict_inputentriesentryinput) + (dst_negative_scalar_restrict_inputentriesentryinput))) /\ (exists ge_balance_positive_scalar_restrict_inputentriesentryinputvalue ge_balance_negative_scalar_restrict_inputentriesentryinputvalue. (((((sto_input_scalar_restrict_inputentries) = 2 * (ge_balance_positive_scalar_restrict_inputentriesentryinputvalue) /\ (ge_balance_negative_scalar_restrict_inputentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_restrict_inputentriesentryinputvaluedecode. (((sto_input_scalar_restrict_inputentries) = 2 * ge_signed_half_scalar_restrict_inputentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_inputentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_restrict_inputentriesentryinputvalue) = S ge_signed_half_scalar_restrict_inputentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_restrict_inputentriesentryinput) + ge_balance_negative_scalar_restrict_inputentriesentryinputvalue = (dst_negative_scalar_restrict_inputentriesentryinput) + ge_balance_positive_scalar_restrict_inputentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_restrict_inputentriesentryoutput dst_positive_scale_scalar_restrict_inputentriesentryoutput dst_negative_code_scalar_restrict_inputentriesentryoutput dst_negative_scale_scalar_restrict_inputentriesentryoutput dst_positive_scalar_restrict_inputentriesentryoutput dst_negative_scalar_restrict_inputentriesentryoutput. (((G) = (((((dst_positive_code_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_positive_code_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_positive_scale_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)))) * S ((((dst_positive_code_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_positive_code_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_positive_scale_scalar_restrict_inputentriesentryoutput) + (dst_positive_scale_scalar_restrict_inputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)))) + ((((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_inputentriesentryoutput) + (dst_negative_scale_scalar_restrict_inputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_restrict_inputentriesentryoutputpositive. ff_h_pvs_scalar_restrict_inputentriesentryoutputpositive + S (dst_positive_scalar_restrict_inputentriesentryoutput) = S ((S (sto_index_scalar_restrict_inputentries)) * dst_positive_scale_scalar_restrict_inputentriesentryoutput)) /\ exists ff_q_pvs_scalar_restrict_inputentriesentryoutputpositive. dst_positive_code_scalar_restrict_inputentriesentryoutput = ff_q_pvs_scalar_restrict_inputentriesentryoutputpositive * S ((S (sto_index_scalar_restrict_inputentries)) * dst_positive_scale_scalar_restrict_inputentriesentryoutput) + (dst_positive_scalar_restrict_inputentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_restrict_inputentriesentryoutputnegative. ff_h_pvs_scalar_restrict_inputentriesentryoutputnegative + S (dst_negative_scalar_restrict_inputentriesentryoutput) = S ((S (sto_index_scalar_restrict_inputentries)) * dst_negative_scale_scalar_restrict_inputentriesentryoutput)) /\ exists ff_q_pvs_scalar_restrict_inputentriesentryoutputnegative. dst_negative_code_scalar_restrict_inputentriesentryoutput = ff_q_pvs_scalar_restrict_inputentriesentryoutputnegative * S ((S (sto_index_scalar_restrict_inputentries)) * dst_negative_scale_scalar_restrict_inputentriesentryoutput) + (dst_negative_scalar_restrict_inputentriesentryoutput))) /\ (exists ge_balance_positive_scalar_restrict_inputentriesentryoutputvalue ge_balance_negative_scalar_restrict_inputentriesentryoutputvalue. (((((sto_output_scalar_restrict_inputentries) = 2 * (ge_balance_positive_scalar_restrict_inputentriesentryoutputvalue) /\ (ge_balance_negative_scalar_restrict_inputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_restrict_inputentriesentryoutputvaluedecode. (((sto_output_scalar_restrict_inputentries) = 2 * ge_signed_half_scalar_restrict_inputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_inputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_restrict_inputentriesentryoutputvalue) = S ge_signed_half_scalar_restrict_inputentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_restrict_inputentriesentryoutput) + ge_balance_negative_scalar_restrict_inputentriesentryoutputvalue = (dst_negative_scalar_restrict_inputentriesentryoutput) + ge_balance_positive_scalar_restrict_inputentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_restrict_inputentriesentryoperation sto_an_scalar_restrict_inputentriesentryoperation sto_bp_scalar_restrict_inputentriesentryoperation sto_bn_scalar_restrict_inputentriesentryoperation sto_cp_scalar_restrict_inputentriesentryoperation sto_cn_scalar_restrict_inputentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_restrict_inputentriesentryoperation) /\ (sto_an_scalar_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_inputentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_restrict_inputentriesentryoperationleft + 1 /\ (sto_ap_scalar_restrict_inputentriesentryoperation) = 0) /\ (sto_an_scalar_restrict_inputentriesentryoperation) = S ge_signed_half_scalar_restrict_inputentriesentryoperationleft))) /\ ((((((sto_input_scalar_restrict_inputentries) = 2 * (sto_bp_scalar_restrict_inputentriesentryoperation) /\ (sto_bn_scalar_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_inputentriesentryoperationright. (((sto_input_scalar_restrict_inputentries) = 2 * ge_signed_half_scalar_restrict_inputentriesentryoperationright + 1 /\ (sto_bp_scalar_restrict_inputentriesentryoperation) = 0) /\ (sto_bn_scalar_restrict_inputentriesentryoperation) = S ge_signed_half_scalar_restrict_inputentriesentryoperationright))) /\ ((((((sto_output_scalar_restrict_inputentries) = 2 * (sto_cp_scalar_restrict_inputentriesentryoperation) /\ (sto_cn_scalar_restrict_inputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_inputentriesentryoperationoutput. (((sto_output_scalar_restrict_inputentries) = 2 * ge_signed_half_scalar_restrict_inputentriesentryoperationoutput + 1 /\ (sto_cp_scalar_restrict_inputentriesentryoperation) = 0) /\ (sto_cn_scalar_restrict_inputentriesentryoperation) = S ge_signed_half_scalar_restrict_inputentriesentryoperationoutput))) /\ ((sto_ap_scalar_restrict_inputentriesentryoperation * sto_bp_scalar_restrict_inputentriesentryoperation + sto_an_scalar_restrict_inputentriesentryoperation * sto_bn_scalar_restrict_inputentriesentryoperation) + sto_cn_scalar_restrict_inputentriesentryoperation = (sto_ap_scalar_restrict_inputentriesentryoperation * sto_bn_scalar_restrict_inputentriesentryoperation + sto_an_scalar_restrict_inputentriesentryoperation * sto_bp_scalar_restrict_inputentriesentryoperation) + sto_cp_scalar_restrict_inputentriesentryoperation))))))))))))))) -> (((exists dst_positive_code_scalar_restrict_outputinput_table dst_positive_scale_scalar_restrict_outputinput_table dst_negative_code_scalar_restrict_outputinput_table dst_negative_scale_scalar_restrict_outputinput_table. (((F) = (((((dst_positive_code_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table)) * S ((dst_positive_code_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table)) + ((dst_positive_scale_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table))) + (((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) * S ((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) + ((dst_negative_scale_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)))) * S ((((dst_positive_code_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table)) * S ((dst_positive_code_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table)) + ((dst_positive_scale_scalar_restrict_outputinput_table) + (dst_positive_scale_scalar_restrict_outputinput_table))) + (((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) * S ((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) + ((dst_negative_scale_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)))) + ((((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) * S ((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) + ((dst_negative_scale_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table))) + (((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) * S ((dst_negative_code_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)) + ((dst_negative_scale_scalar_restrict_outputinput_table) + (dst_negative_scale_scalar_restrict_outputinput_table)))))) /\ (forall dst_index_scalar_restrict_outputinput_table. (exists pvs_le_gap_scalar_restrict_outputinput_tabledomain. pvs_le_gap_scalar_restrict_outputinput_tabledomain + (dst_index_scalar_restrict_outputinput_table) = (l)) -> exists dst_positive_scalar_restrict_outputinput_table dst_negative_scalar_restrict_outputinput_table dst_value_scalar_restrict_outputinput_table. ((((exists ff_h_pvs_scalar_restrict_outputinput_tableentrypositive. ff_h_pvs_scalar_restrict_outputinput_tableentrypositive + S (dst_positive_scalar_restrict_outputinput_table) = S ((S (dst_index_scalar_restrict_outputinput_table)) * dst_positive_scale_scalar_restrict_outputinput_table)) /\ exists ff_q_pvs_scalar_restrict_outputinput_tableentrypositive. dst_positive_code_scalar_restrict_outputinput_table = ff_q_pvs_scalar_restrict_outputinput_tableentrypositive * S ((S (dst_index_scalar_restrict_outputinput_table)) * dst_positive_scale_scalar_restrict_outputinput_table) + (dst_positive_scalar_restrict_outputinput_table))) /\ (((((exists ff_h_pvs_scalar_restrict_outputinput_tableentrynegative. ff_h_pvs_scalar_restrict_outputinput_tableentrynegative + S (dst_negative_scalar_restrict_outputinput_table) = S ((S (dst_index_scalar_restrict_outputinput_table)) * dst_negative_scale_scalar_restrict_outputinput_table)) /\ exists ff_q_pvs_scalar_restrict_outputinput_tableentrynegative. dst_negative_code_scalar_restrict_outputinput_table = ff_q_pvs_scalar_restrict_outputinput_tableentrynegative * S ((S (dst_index_scalar_restrict_outputinput_table)) * dst_negative_scale_scalar_restrict_outputinput_table) + (dst_negative_scalar_restrict_outputinput_table))) /\ (exists ge_balance_positive_scalar_restrict_outputinput_tableentryvalue ge_balance_negative_scalar_restrict_outputinput_tableentryvalue. (((((dst_value_scalar_restrict_outputinput_table) = 2 * (ge_balance_positive_scalar_restrict_outputinput_tableentryvalue) /\ (ge_balance_negative_scalar_restrict_outputinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_restrict_outputinput_tableentryvaluedecode. (((dst_value_scalar_restrict_outputinput_table) = 2 * ge_signed_half_scalar_restrict_outputinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_outputinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_restrict_outputinput_tableentryvalue) = S ge_signed_half_scalar_restrict_outputinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_restrict_outputinput_table) + ge_balance_negative_scalar_restrict_outputinput_tableentryvalue = (dst_negative_scalar_restrict_outputinput_table) + ge_balance_positive_scalar_restrict_outputinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_restrict_outputoutput_table dst_positive_scale_scalar_restrict_outputoutput_table dst_negative_code_scalar_restrict_outputoutput_table dst_negative_scale_scalar_restrict_outputoutput_table. (((G) = (((((dst_positive_code_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table)) * S ((dst_positive_code_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table)) + ((dst_positive_scale_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table))) + (((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) * S ((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) + ((dst_negative_scale_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)))) * S ((((dst_positive_code_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table)) * S ((dst_positive_code_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table)) + ((dst_positive_scale_scalar_restrict_outputoutput_table) + (dst_positive_scale_scalar_restrict_outputoutput_table))) + (((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) * S ((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) + ((dst_negative_scale_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)))) + ((((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) * S ((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) + ((dst_negative_scale_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table))) + (((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) * S ((dst_negative_code_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)) + ((dst_negative_scale_scalar_restrict_outputoutput_table) + (dst_negative_scale_scalar_restrict_outputoutput_table)))))) /\ (forall dst_index_scalar_restrict_outputoutput_table. (exists pvs_le_gap_scalar_restrict_outputoutput_tabledomain. pvs_le_gap_scalar_restrict_outputoutput_tabledomain + (dst_index_scalar_restrict_outputoutput_table) = (l)) -> exists dst_positive_scalar_restrict_outputoutput_table dst_negative_scalar_restrict_outputoutput_table dst_value_scalar_restrict_outputoutput_table. ((((exists ff_h_pvs_scalar_restrict_outputoutput_tableentrypositive. ff_h_pvs_scalar_restrict_outputoutput_tableentrypositive + S (dst_positive_scalar_restrict_outputoutput_table) = S ((S (dst_index_scalar_restrict_outputoutput_table)) * dst_positive_scale_scalar_restrict_outputoutput_table)) /\ exists ff_q_pvs_scalar_restrict_outputoutput_tableentrypositive. dst_positive_code_scalar_restrict_outputoutput_table = ff_q_pvs_scalar_restrict_outputoutput_tableentrypositive * S ((S (dst_index_scalar_restrict_outputoutput_table)) * dst_positive_scale_scalar_restrict_outputoutput_table) + (dst_positive_scalar_restrict_outputoutput_table))) /\ (((((exists ff_h_pvs_scalar_restrict_outputoutput_tableentrynegative. ff_h_pvs_scalar_restrict_outputoutput_tableentrynegative + S (dst_negative_scalar_restrict_outputoutput_table) = S ((S (dst_index_scalar_restrict_outputoutput_table)) * dst_negative_scale_scalar_restrict_outputoutput_table)) /\ exists ff_q_pvs_scalar_restrict_outputoutput_tableentrynegative. dst_negative_code_scalar_restrict_outputoutput_table = ff_q_pvs_scalar_restrict_outputoutput_tableentrynegative * S ((S (dst_index_scalar_restrict_outputoutput_table)) * dst_negative_scale_scalar_restrict_outputoutput_table) + (dst_negative_scalar_restrict_outputoutput_table))) /\ (exists ge_balance_positive_scalar_restrict_outputoutput_tableentryvalue ge_balance_negative_scalar_restrict_outputoutput_tableentryvalue. (((((dst_value_scalar_restrict_outputoutput_table) = 2 * (ge_balance_positive_scalar_restrict_outputoutput_tableentryvalue) /\ (ge_balance_negative_scalar_restrict_outputoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_restrict_outputoutput_tableentryvaluedecode. (((dst_value_scalar_restrict_outputoutput_table) = 2 * ge_signed_half_scalar_restrict_outputoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_outputoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_restrict_outputoutput_tableentryvalue) = S ge_signed_half_scalar_restrict_outputoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_restrict_outputoutput_table) + ge_balance_negative_scalar_restrict_outputoutput_tableentryvalue = (dst_negative_scalar_restrict_outputoutput_table) + ge_balance_positive_scalar_restrict_outputoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_restrict_outputentries. (exists pvs_gap_scalar_restrict_outputentriesbound. pvs_gap_scalar_restrict_outputentriesbound + S (sto_index_scalar_restrict_outputentries) = (l)) -> exists sto_input_scalar_restrict_outputentries sto_output_scalar_restrict_outputentries. ((exists dst_positive_code_scalar_restrict_outputentriesentryinput dst_positive_scale_scalar_restrict_outputentriesentryinput dst_negative_code_scalar_restrict_outputentriesentryinput dst_negative_scale_scalar_restrict_outputentriesentryinput dst_positive_scalar_restrict_outputentriesentryinput dst_negative_scalar_restrict_outputentriesentryinput. (((F) = (((((dst_positive_code_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_positive_code_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput)) + ((dst_positive_scale_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput))) + (((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)))) * S ((((dst_positive_code_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_positive_code_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput)) + ((dst_positive_scale_scalar_restrict_outputentriesentryinput) + (dst_positive_scale_scalar_restrict_outputentriesentryinput))) + (((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)))) + ((((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput))) + (((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryinput) + (dst_negative_scale_scalar_restrict_outputentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_restrict_outputentriesentryinputpositive. ff_h_pvs_scalar_restrict_outputentriesentryinputpositive + S (dst_positive_scalar_restrict_outputentriesentryinput) = S ((S (sto_index_scalar_restrict_outputentries)) * dst_positive_scale_scalar_restrict_outputentriesentryinput)) /\ exists ff_q_pvs_scalar_restrict_outputentriesentryinputpositive. dst_positive_code_scalar_restrict_outputentriesentryinput = ff_q_pvs_scalar_restrict_outputentriesentryinputpositive * S ((S (sto_index_scalar_restrict_outputentries)) * dst_positive_scale_scalar_restrict_outputentriesentryinput) + (dst_positive_scalar_restrict_outputentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_restrict_outputentriesentryinputnegative. ff_h_pvs_scalar_restrict_outputentriesentryinputnegative + S (dst_negative_scalar_restrict_outputentriesentryinput) = S ((S (sto_index_scalar_restrict_outputentries)) * dst_negative_scale_scalar_restrict_outputentriesentryinput)) /\ exists ff_q_pvs_scalar_restrict_outputentriesentryinputnegative. dst_negative_code_scalar_restrict_outputentriesentryinput = ff_q_pvs_scalar_restrict_outputentriesentryinputnegative * S ((S (sto_index_scalar_restrict_outputentries)) * dst_negative_scale_scalar_restrict_outputentriesentryinput) + (dst_negative_scalar_restrict_outputentriesentryinput))) /\ (exists ge_balance_positive_scalar_restrict_outputentriesentryinputvalue ge_balance_negative_scalar_restrict_outputentriesentryinputvalue. (((((sto_input_scalar_restrict_outputentries) = 2 * (ge_balance_positive_scalar_restrict_outputentriesentryinputvalue) /\ (ge_balance_negative_scalar_restrict_outputentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_restrict_outputentriesentryinputvaluedecode. (((sto_input_scalar_restrict_outputentries) = 2 * ge_signed_half_scalar_restrict_outputentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_outputentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_restrict_outputentriesentryinputvalue) = S ge_signed_half_scalar_restrict_outputentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_restrict_outputentriesentryinput) + ge_balance_negative_scalar_restrict_outputentriesentryinputvalue = (dst_negative_scalar_restrict_outputentriesentryinput) + ge_balance_positive_scalar_restrict_outputentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_restrict_outputentriesentryoutput dst_positive_scale_scalar_restrict_outputentriesentryoutput dst_negative_code_scalar_restrict_outputentriesentryoutput dst_negative_scale_scalar_restrict_outputentriesentryoutput dst_positive_scalar_restrict_outputentriesentryoutput dst_negative_scalar_restrict_outputentriesentryoutput. (((G) = (((((dst_positive_code_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_positive_code_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_positive_scale_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)))) * S ((((dst_positive_code_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_positive_code_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_positive_scale_scalar_restrict_outputentriesentryoutput) + (dst_positive_scale_scalar_restrict_outputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)))) + ((((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput))) + (((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) * S ((dst_negative_code_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)) + ((dst_negative_scale_scalar_restrict_outputentriesentryoutput) + (dst_negative_scale_scalar_restrict_outputentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_restrict_outputentriesentryoutputpositive. ff_h_pvs_scalar_restrict_outputentriesentryoutputpositive + S (dst_positive_scalar_restrict_outputentriesentryoutput) = S ((S (sto_index_scalar_restrict_outputentries)) * dst_positive_scale_scalar_restrict_outputentriesentryoutput)) /\ exists ff_q_pvs_scalar_restrict_outputentriesentryoutputpositive. dst_positive_code_scalar_restrict_outputentriesentryoutput = ff_q_pvs_scalar_restrict_outputentriesentryoutputpositive * S ((S (sto_index_scalar_restrict_outputentries)) * dst_positive_scale_scalar_restrict_outputentriesentryoutput) + (dst_positive_scalar_restrict_outputentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_restrict_outputentriesentryoutputnegative. ff_h_pvs_scalar_restrict_outputentriesentryoutputnegative + S (dst_negative_scalar_restrict_outputentriesentryoutput) = S ((S (sto_index_scalar_restrict_outputentries)) * dst_negative_scale_scalar_restrict_outputentriesentryoutput)) /\ exists ff_q_pvs_scalar_restrict_outputentriesentryoutputnegative. dst_negative_code_scalar_restrict_outputentriesentryoutput = ff_q_pvs_scalar_restrict_outputentriesentryoutputnegative * S ((S (sto_index_scalar_restrict_outputentries)) * dst_negative_scale_scalar_restrict_outputentriesentryoutput) + (dst_negative_scalar_restrict_outputentriesentryoutput))) /\ (exists ge_balance_positive_scalar_restrict_outputentriesentryoutputvalue ge_balance_negative_scalar_restrict_outputentriesentryoutputvalue. (((((sto_output_scalar_restrict_outputentries) = 2 * (ge_balance_positive_scalar_restrict_outputentriesentryoutputvalue) /\ (ge_balance_negative_scalar_restrict_outputentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_restrict_outputentriesentryoutputvaluedecode. (((sto_output_scalar_restrict_outputentries) = 2 * ge_signed_half_scalar_restrict_outputentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_restrict_outputentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_restrict_outputentriesentryoutputvalue) = S ge_signed_half_scalar_restrict_outputentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_restrict_outputentriesentryoutput) + ge_balance_negative_scalar_restrict_outputentriesentryoutputvalue = (dst_negative_scalar_restrict_outputentriesentryoutput) + ge_balance_positive_scalar_restrict_outputentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_restrict_outputentriesentryoperation sto_an_scalar_restrict_outputentriesentryoperation sto_bp_scalar_restrict_outputentriesentryoperation sto_bn_scalar_restrict_outputentriesentryoperation sto_cp_scalar_restrict_outputentriesentryoperation sto_cn_scalar_restrict_outputentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_restrict_outputentriesentryoperation) /\ (sto_an_scalar_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_outputentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_restrict_outputentriesentryoperationleft + 1 /\ (sto_ap_scalar_restrict_outputentriesentryoperation) = 0) /\ (sto_an_scalar_restrict_outputentriesentryoperation) = S ge_signed_half_scalar_restrict_outputentriesentryoperationleft))) /\ ((((((sto_input_scalar_restrict_outputentries) = 2 * (sto_bp_scalar_restrict_outputentriesentryoperation) /\ (sto_bn_scalar_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_outputentriesentryoperationright. (((sto_input_scalar_restrict_outputentries) = 2 * ge_signed_half_scalar_restrict_outputentriesentryoperationright + 1 /\ (sto_bp_scalar_restrict_outputentriesentryoperation) = 0) /\ (sto_bn_scalar_restrict_outputentriesentryoperation) = S ge_signed_half_scalar_restrict_outputentriesentryoperationright))) /\ ((((((sto_output_scalar_restrict_outputentries) = 2 * (sto_cp_scalar_restrict_outputentriesentryoperation) /\ (sto_cn_scalar_restrict_outputentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_restrict_outputentriesentryoperationoutput. (((sto_output_scalar_restrict_outputentries) = 2 * ge_signed_half_scalar_restrict_outputentriesentryoperationoutput + 1 /\ (sto_cp_scalar_restrict_outputentriesentryoperation) = 0) /\ (sto_cn_scalar_restrict_outputentriesentryoperation) = S ge_signed_half_scalar_restrict_outputentriesentryoperationoutput))) /\ ((sto_ap_scalar_restrict_outputentriesentryoperation * sto_bp_scalar_restrict_outputentriesentryoperation + sto_an_scalar_restrict_outputentriesentryoperation * sto_bn_scalar_restrict_outputentriesentryoperation) + sto_cn_scalar_restrict_outputentriesentryoperation = (sto_ap_scalar_restrict_outputentriesentryoperation * sto_bn_scalar_restrict_outputentriesentryoperation + sto_an_scalar_restrict_outputentriesentryoperation * sto_bp_scalar_restrict_outputentriesentryoperation) + sto_cp_scalar_restrict_outputentriesentryoperation)))))))))))))))