signed_rectangular_slice_empty

Exact expanded first-order arithmetic statement

forall F G o s. (exists dst_positive_code_empty_source dst_positive_scale_empty_source dst_negative_code_empty_source dst_negative_scale_empty_source. (((F) = (((((dst_positive_code_empty_source) + (dst_positive_scale_empty_source)) * S ((dst_positive_code_empty_source) + (dst_positive_scale_empty_source)) + ((dst_positive_scale_empty_source) + (dst_positive_scale_empty_source))) + (((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) * S ((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) + ((dst_negative_scale_empty_source) + (dst_negative_scale_empty_source)))) * S ((((dst_positive_code_empty_source) + (dst_positive_scale_empty_source)) * S ((dst_positive_code_empty_source) + (dst_positive_scale_empty_source)) + ((dst_positive_scale_empty_source) + (dst_positive_scale_empty_source))) + (((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) * S ((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) + ((dst_negative_scale_empty_source) + (dst_negative_scale_empty_source)))) + ((((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) * S ((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) + ((dst_negative_scale_empty_source) + (dst_negative_scale_empty_source))) + (((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) * S ((dst_negative_code_empty_source) + (dst_negative_scale_empty_source)) + ((dst_negative_scale_empty_source) + (dst_negative_scale_empty_source)))))) /\ (forall dst_index_empty_source. (exists pvs_le_gap_empty_sourcedomain. pvs_le_gap_empty_sourcedomain + (dst_index_empty_source) = (0)) -> exists dst_positive_empty_source dst_negative_empty_source dst_value_empty_source. ((((exists ff_h_pvs_empty_sourceentrypositive. ff_h_pvs_empty_sourceentrypositive + S (dst_positive_empty_source) = S ((S (dst_index_empty_source)) * dst_positive_scale_empty_source)) /\ exists ff_q_pvs_empty_sourceentrypositive. dst_positive_code_empty_source = ff_q_pvs_empty_sourceentrypositive * S ((S (dst_index_empty_source)) * dst_positive_scale_empty_source) + (dst_positive_empty_source))) /\ (((((exists ff_h_pvs_empty_sourceentrynegative. ff_h_pvs_empty_sourceentrynegative + S (dst_negative_empty_source) = S ((S (dst_index_empty_source)) * dst_negative_scale_empty_source)) /\ exists ff_q_pvs_empty_sourceentrynegative. dst_negative_code_empty_source = ff_q_pvs_empty_sourceentrynegative * S ((S (dst_index_empty_source)) * dst_negative_scale_empty_source) + (dst_negative_empty_source))) /\ (exists ge_balance_positive_empty_sourceentryvalue ge_balance_negative_empty_sourceentryvalue. (((((dst_value_empty_source) = 2 * (ge_balance_positive_empty_sourceentryvalue) /\ (ge_balance_negative_empty_sourceentryvalue) = 0) \/ exists ge_signed_half_empty_sourceentryvaluedecode. (((dst_value_empty_source) = 2 * ge_signed_half_empty_sourceentryvaluedecode + 1 /\ (ge_balance_positive_empty_sourceentryvalue) = 0) /\ (ge_balance_negative_empty_sourceentryvalue) = S ge_signed_half_empty_sourceentryvaluedecode))) /\ ((dst_positive_empty_source) + ge_balance_negative_empty_sourceentryvalue = (dst_negative_empty_source) + ge_balance_positive_empty_sourceentryvalue))))))))) -> (exists dst_positive_code_empty_output dst_positive_scale_empty_output dst_negative_code_empty_output dst_negative_scale_empty_output. (((G) = (((((dst_positive_code_empty_output) + (dst_positive_scale_empty_output)) * S ((dst_positive_code_empty_output) + (dst_positive_scale_empty_output)) + ((dst_positive_scale_empty_output) + (dst_positive_scale_empty_output))) + (((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) * S ((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) + ((dst_negative_scale_empty_output) + (dst_negative_scale_empty_output)))) * S ((((dst_positive_code_empty_output) + (dst_positive_scale_empty_output)) * S ((dst_positive_code_empty_output) + (dst_positive_scale_empty_output)) + ((dst_positive_scale_empty_output) + (dst_positive_scale_empty_output))) + (((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) * S ((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) + ((dst_negative_scale_empty_output) + (dst_negative_scale_empty_output)))) + ((((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) * S ((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) + ((dst_negative_scale_empty_output) + (dst_negative_scale_empty_output))) + (((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) * S ((dst_negative_code_empty_output) + (dst_negative_scale_empty_output)) + ((dst_negative_scale_empty_output) + (dst_negative_scale_empty_output)))))) /\ (forall dst_index_empty_output. (exists pvs_le_gap_empty_outputdomain. pvs_le_gap_empty_outputdomain + (dst_index_empty_output) = (0)) -> exists dst_positive_empty_output dst_negative_empty_output dst_value_empty_output. ((((exists ff_h_pvs_empty_outputentrypositive. ff_h_pvs_empty_outputentrypositive + S (dst_positive_empty_output) = S ((S (dst_index_empty_output)) * dst_positive_scale_empty_output)) /\ exists ff_q_pvs_empty_outputentrypositive. dst_positive_code_empty_output = ff_q_pvs_empty_outputentrypositive * S ((S (dst_index_empty_output)) * dst_positive_scale_empty_output) + (dst_positive_empty_output))) /\ (((((exists ff_h_pvs_empty_outputentrynegative. ff_h_pvs_empty_outputentrynegative + S (dst_negative_empty_output) = S ((S (dst_index_empty_output)) * dst_negative_scale_empty_output)) /\ exists ff_q_pvs_empty_outputentrynegative. dst_negative_code_empty_output = ff_q_pvs_empty_outputentrynegative * S ((S (dst_index_empty_output)) * dst_negative_scale_empty_output) + (dst_negative_empty_output))) /\ (exists ge_balance_positive_empty_outputentryvalue ge_balance_negative_empty_outputentryvalue. (((((dst_value_empty_output) = 2 * (ge_balance_positive_empty_outputentryvalue) /\ (ge_balance_negative_empty_outputentryvalue) = 0) \/ exists ge_signed_half_empty_outputentryvaluedecode. (((dst_value_empty_output) = 2 * ge_signed_half_empty_outputentryvaluedecode + 1 /\ (ge_balance_positive_empty_outputentryvalue) = 0) /\ (ge_balance_negative_empty_outputentryvalue) = S ge_signed_half_empty_outputentryvaluedecode))) /\ ((dst_positive_empty_output) + ge_balance_negative_empty_outputentryvalue = (dst_negative_empty_output) + ge_balance_positive_empty_outputentryvalue))))))))) -> (((exists dst_positive_code_empty_resultsource_table dst_positive_scale_empty_resultsource_table dst_negative_code_empty_resultsource_table dst_negative_scale_empty_resultsource_table. (((F) = (((((dst_positive_code_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table)) * S ((dst_positive_code_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table)) + ((dst_positive_scale_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table))) + (((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) * S ((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) + ((dst_negative_scale_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)))) * S ((((dst_positive_code_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table)) * S ((dst_positive_code_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table)) + ((dst_positive_scale_empty_resultsource_table) + (dst_positive_scale_empty_resultsource_table))) + (((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) * S ((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) + ((dst_negative_scale_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)))) + ((((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) * S ((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) + ((dst_negative_scale_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table))) + (((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) * S ((dst_negative_code_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)) + ((dst_negative_scale_empty_resultsource_table) + (dst_negative_scale_empty_resultsource_table)))))) /\ (forall dst_index_empty_resultsource_table. (exists pvs_le_gap_empty_resultsource_tabledomain. pvs_le_gap_empty_resultsource_tabledomain + (dst_index_empty_resultsource_table) = (0)) -> exists dst_positive_empty_resultsource_table dst_negative_empty_resultsource_table dst_value_empty_resultsource_table. ((((exists ff_h_pvs_empty_resultsource_tableentrypositive. ff_h_pvs_empty_resultsource_tableentrypositive + S (dst_positive_empty_resultsource_table) = S ((S (dst_index_empty_resultsource_table)) * dst_positive_scale_empty_resultsource_table)) /\ exists ff_q_pvs_empty_resultsource_tableentrypositive. dst_positive_code_empty_resultsource_table = ff_q_pvs_empty_resultsource_tableentrypositive * S ((S (dst_index_empty_resultsource_table)) * dst_positive_scale_empty_resultsource_table) + (dst_positive_empty_resultsource_table))) /\ (((((exists ff_h_pvs_empty_resultsource_tableentrynegative. ff_h_pvs_empty_resultsource_tableentrynegative + S (dst_negative_empty_resultsource_table) = S ((S (dst_index_empty_resultsource_table)) * dst_negative_scale_empty_resultsource_table)) /\ exists ff_q_pvs_empty_resultsource_tableentrynegative. dst_negative_code_empty_resultsource_table = ff_q_pvs_empty_resultsource_tableentrynegative * S ((S (dst_index_empty_resultsource_table)) * dst_negative_scale_empty_resultsource_table) + (dst_negative_empty_resultsource_table))) /\ (exists ge_balance_positive_empty_resultsource_tableentryvalue ge_balance_negative_empty_resultsource_tableentryvalue. (((((dst_value_empty_resultsource_table) = 2 * (ge_balance_positive_empty_resultsource_tableentryvalue) /\ (ge_balance_negative_empty_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_empty_resultsource_tableentryvaluedecode. (((dst_value_empty_resultsource_table) = 2 * ge_signed_half_empty_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_empty_resultsource_tableentryvalue) = S ge_signed_half_empty_resultsource_tableentryvaluedecode))) /\ ((dst_positive_empty_resultsource_table) + ge_balance_negative_empty_resultsource_tableentryvalue = (dst_negative_empty_resultsource_table) + ge_balance_positive_empty_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_empty_resultoutput_table dst_positive_scale_empty_resultoutput_table dst_negative_code_empty_resultoutput_table dst_negative_scale_empty_resultoutput_table. (((G) = (((((dst_positive_code_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table)) * S ((dst_positive_code_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table)) + ((dst_positive_scale_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table))) + (((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) * S ((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) + ((dst_negative_scale_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)))) * S ((((dst_positive_code_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table)) * S ((dst_positive_code_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table)) + ((dst_positive_scale_empty_resultoutput_table) + (dst_positive_scale_empty_resultoutput_table))) + (((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) * S ((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) + ((dst_negative_scale_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)))) + ((((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) * S ((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) + ((dst_negative_scale_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table))) + (((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) * S ((dst_negative_code_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)) + ((dst_negative_scale_empty_resultoutput_table) + (dst_negative_scale_empty_resultoutput_table)))))) /\ (forall dst_index_empty_resultoutput_table. (exists pvs_le_gap_empty_resultoutput_tabledomain. pvs_le_gap_empty_resultoutput_tabledomain + (dst_index_empty_resultoutput_table) = (0)) -> exists dst_positive_empty_resultoutput_table dst_negative_empty_resultoutput_table dst_value_empty_resultoutput_table. ((((exists ff_h_pvs_empty_resultoutput_tableentrypositive. ff_h_pvs_empty_resultoutput_tableentrypositive + S (dst_positive_empty_resultoutput_table) = S ((S (dst_index_empty_resultoutput_table)) * dst_positive_scale_empty_resultoutput_table)) /\ exists ff_q_pvs_empty_resultoutput_tableentrypositive. dst_positive_code_empty_resultoutput_table = ff_q_pvs_empty_resultoutput_tableentrypositive * S ((S (dst_index_empty_resultoutput_table)) * dst_positive_scale_empty_resultoutput_table) + (dst_positive_empty_resultoutput_table))) /\ (((((exists ff_h_pvs_empty_resultoutput_tableentrynegative. ff_h_pvs_empty_resultoutput_tableentrynegative + S (dst_negative_empty_resultoutput_table) = S ((S (dst_index_empty_resultoutput_table)) * dst_negative_scale_empty_resultoutput_table)) /\ exists ff_q_pvs_empty_resultoutput_tableentrynegative. dst_negative_code_empty_resultoutput_table = ff_q_pvs_empty_resultoutput_tableentrynegative * S ((S (dst_index_empty_resultoutput_table)) * dst_negative_scale_empty_resultoutput_table) + (dst_negative_empty_resultoutput_table))) /\ (exists ge_balance_positive_empty_resultoutput_tableentryvalue ge_balance_negative_empty_resultoutput_tableentryvalue. (((((dst_value_empty_resultoutput_table) = 2 * (ge_balance_positive_empty_resultoutput_tableentryvalue) /\ (ge_balance_negative_empty_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_empty_resultoutput_tableentryvaluedecode. (((dst_value_empty_resultoutput_table) = 2 * ge_signed_half_empty_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_empty_resultoutput_tableentryvalue) = S ge_signed_half_empty_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_empty_resultoutput_table) + ge_balance_negative_empty_resultoutput_tableentryvalue = (dst_negative_empty_resultoutput_table) + ge_balance_positive_empty_resultoutput_tableentryvalue))))))))) /\ (forall srs_index_empty_result. (exists pvs_gap_empty_resultbound. pvs_gap_empty_resultbound + S (srs_index_empty_result) = (0)) -> exists srs_value_empty_result. (((exists dst_positive_code_empty_resultentrysource dst_positive_scale_empty_resultentrysource dst_negative_code_empty_resultentrysource dst_negative_scale_empty_resultentrysource dst_positive_empty_resultentrysource dst_negative_empty_resultentrysource. (((F) = (((((dst_positive_code_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource)) * S ((dst_positive_code_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource)) + ((dst_positive_scale_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource))) + (((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) * S ((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) + ((dst_negative_scale_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)))) * S ((((dst_positive_code_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource)) * S ((dst_positive_code_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource)) + ((dst_positive_scale_empty_resultentrysource) + (dst_positive_scale_empty_resultentrysource))) + (((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) * S ((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) + ((dst_negative_scale_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)))) + ((((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) * S ((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) + ((dst_negative_scale_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource))) + (((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) * S ((dst_negative_code_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)) + ((dst_negative_scale_empty_resultentrysource) + (dst_negative_scale_empty_resultentrysource)))))) /\ (((((exists ff_h_pvs_empty_resultentrysourcepositive. ff_h_pvs_empty_resultentrysourcepositive + S (dst_positive_empty_resultentrysource) = S ((S (((o) + ((s) * (srs_index_empty_result))))) * dst_positive_scale_empty_resultentrysource)) /\ exists ff_q_pvs_empty_resultentrysourcepositive. dst_positive_code_empty_resultentrysource = ff_q_pvs_empty_resultentrysourcepositive * S ((S (((o) + ((s) * (srs_index_empty_result))))) * dst_positive_scale_empty_resultentrysource) + (dst_positive_empty_resultentrysource))) /\ (((((exists ff_h_pvs_empty_resultentrysourcenegative. ff_h_pvs_empty_resultentrysourcenegative + S (dst_negative_empty_resultentrysource) = S ((S (((o) + ((s) * (srs_index_empty_result))))) * dst_negative_scale_empty_resultentrysource)) /\ exists ff_q_pvs_empty_resultentrysourcenegative. dst_negative_code_empty_resultentrysource = ff_q_pvs_empty_resultentrysourcenegative * S ((S (((o) + ((s) * (srs_index_empty_result))))) * dst_negative_scale_empty_resultentrysource) + (dst_negative_empty_resultentrysource))) /\ (exists ge_balance_positive_empty_resultentrysourcevalue ge_balance_negative_empty_resultentrysourcevalue. (((((srs_value_empty_result) = 2 * (ge_balance_positive_empty_resultentrysourcevalue) /\ (ge_balance_negative_empty_resultentrysourcevalue) = 0) \/ exists ge_signed_half_empty_resultentrysourcevaluedecode. (((srs_value_empty_result) = 2 * ge_signed_half_empty_resultentrysourcevaluedecode + 1 /\ (ge_balance_positive_empty_resultentrysourcevalue) = 0) /\ (ge_balance_negative_empty_resultentrysourcevalue) = S ge_signed_half_empty_resultentrysourcevaluedecode))) /\ ((dst_positive_empty_resultentrysource) + ge_balance_negative_empty_resultentrysourcevalue = (dst_negative_empty_resultentrysource) + ge_balance_positive_empty_resultentrysourcevalue))))))))) /\ (exists dst_positive_code_empty_resultentryoutput dst_positive_scale_empty_resultentryoutput dst_negative_code_empty_resultentryoutput dst_negative_scale_empty_resultentryoutput dst_positive_empty_resultentryoutput dst_negative_empty_resultentryoutput. (((G) = (((((dst_positive_code_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput)) * S ((dst_positive_code_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput)) + ((dst_positive_scale_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput))) + (((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) * S ((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) + ((dst_negative_scale_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)))) * S ((((dst_positive_code_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput)) * S ((dst_positive_code_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput)) + ((dst_positive_scale_empty_resultentryoutput) + (dst_positive_scale_empty_resultentryoutput))) + (((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) * S ((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) + ((dst_negative_scale_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)))) + ((((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) * S ((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) + ((dst_negative_scale_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput))) + (((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) * S ((dst_negative_code_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)) + ((dst_negative_scale_empty_resultentryoutput) + (dst_negative_scale_empty_resultentryoutput)))))) /\ (((((exists ff_h_pvs_empty_resultentryoutputpositive. ff_h_pvs_empty_resultentryoutputpositive + S (dst_positive_empty_resultentryoutput) = S ((S (srs_index_empty_result)) * dst_positive_scale_empty_resultentryoutput)) /\ exists ff_q_pvs_empty_resultentryoutputpositive. dst_positive_code_empty_resultentryoutput = ff_q_pvs_empty_resultentryoutputpositive * S ((S (srs_index_empty_result)) * dst_positive_scale_empty_resultentryoutput) + (dst_positive_empty_resultentryoutput))) /\ (((((exists ff_h_pvs_empty_resultentryoutputnegative. ff_h_pvs_empty_resultentryoutputnegative + S (dst_negative_empty_resultentryoutput) = S ((S (srs_index_empty_result)) * dst_negative_scale_empty_resultentryoutput)) /\ exists ff_q_pvs_empty_resultentryoutputnegative. dst_negative_code_empty_resultentryoutput = ff_q_pvs_empty_resultentryoutputnegative * S ((S (srs_index_empty_result)) * dst_negative_scale_empty_resultentryoutput) + (dst_negative_empty_resultentryoutput))) /\ (exists ge_balance_positive_empty_resultentryoutputvalue ge_balance_negative_empty_resultentryoutputvalue. (((((srs_value_empty_result) = 2 * (ge_balance_positive_empty_resultentryoutputvalue) /\ (ge_balance_negative_empty_resultentryoutputvalue) = 0) \/ exists ge_signed_half_empty_resultentryoutputvaluedecode. (((srs_value_empty_result) = 2 * ge_signed_half_empty_resultentryoutputvaluedecode + 1 /\ (ge_balance_positive_empty_resultentryoutputvalue) = 0) /\ (ge_balance_negative_empty_resultentryoutputvalue) = S ge_signed_half_empty_resultentryoutputvaluedecode))) /\ ((dst_positive_empty_resultentryoutput) + ge_balance_negative_empty_resultentryoutputvalue = (dst_negative_empty_resultentryoutput) + ge_balance_positive_empty_resultentryoutputvalue))))))))))))))))