signed_table_scalar_empty

Exact expanded first-order arithmetic statement

forall a F G. (exists dst_positive_code_scalar_empty_0 dst_positive_scale_scalar_empty_0 dst_negative_code_scalar_empty_0 dst_negative_scale_scalar_empty_0. (((F) = (((((dst_positive_code_scalar_empty_0) + (dst_positive_scale_scalar_empty_0)) * S ((dst_positive_code_scalar_empty_0) + (dst_positive_scale_scalar_empty_0)) + ((dst_positive_scale_scalar_empty_0) + (dst_positive_scale_scalar_empty_0))) + (((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) * S ((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) + ((dst_negative_scale_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)))) * S ((((dst_positive_code_scalar_empty_0) + (dst_positive_scale_scalar_empty_0)) * S ((dst_positive_code_scalar_empty_0) + (dst_positive_scale_scalar_empty_0)) + ((dst_positive_scale_scalar_empty_0) + (dst_positive_scale_scalar_empty_0))) + (((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) * S ((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) + ((dst_negative_scale_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)))) + ((((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) * S ((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) + ((dst_negative_scale_scalar_empty_0) + (dst_negative_scale_scalar_empty_0))) + (((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) * S ((dst_negative_code_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)) + ((dst_negative_scale_scalar_empty_0) + (dst_negative_scale_scalar_empty_0)))))) /\ (forall dst_index_scalar_empty_0. (exists pvs_le_gap_scalar_empty_0domain. pvs_le_gap_scalar_empty_0domain + (dst_index_scalar_empty_0) = (0)) -> exists dst_positive_scalar_empty_0 dst_negative_scalar_empty_0 dst_value_scalar_empty_0. ((((exists ff_h_pvs_scalar_empty_0entrypositive. ff_h_pvs_scalar_empty_0entrypositive + S (dst_positive_scalar_empty_0) = S ((S (dst_index_scalar_empty_0)) * dst_positive_scale_scalar_empty_0)) /\ exists ff_q_pvs_scalar_empty_0entrypositive. dst_positive_code_scalar_empty_0 = ff_q_pvs_scalar_empty_0entrypositive * S ((S (dst_index_scalar_empty_0)) * dst_positive_scale_scalar_empty_0) + (dst_positive_scalar_empty_0))) /\ (((((exists ff_h_pvs_scalar_empty_0entrynegative. ff_h_pvs_scalar_empty_0entrynegative + S (dst_negative_scalar_empty_0) = S ((S (dst_index_scalar_empty_0)) * dst_negative_scale_scalar_empty_0)) /\ exists ff_q_pvs_scalar_empty_0entrynegative. dst_negative_code_scalar_empty_0 = ff_q_pvs_scalar_empty_0entrynegative * S ((S (dst_index_scalar_empty_0)) * dst_negative_scale_scalar_empty_0) + (dst_negative_scalar_empty_0))) /\ (exists ge_balance_positive_scalar_empty_0entryvalue ge_balance_negative_scalar_empty_0entryvalue. (((((dst_value_scalar_empty_0) = 2 * (ge_balance_positive_scalar_empty_0entryvalue) /\ (ge_balance_negative_scalar_empty_0entryvalue) = 0) \/ exists ge_signed_half_scalar_empty_0entryvaluedecode. (((dst_value_scalar_empty_0) = 2 * ge_signed_half_scalar_empty_0entryvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_0entryvalue) = 0) /\ (ge_balance_negative_scalar_empty_0entryvalue) = S ge_signed_half_scalar_empty_0entryvaluedecode))) /\ ((dst_positive_scalar_empty_0) + ge_balance_negative_scalar_empty_0entryvalue = (dst_negative_scalar_empty_0) + ge_balance_positive_scalar_empty_0entryvalue))))))))) -> (exists dst_positive_code_scalar_empty_1 dst_positive_scale_scalar_empty_1 dst_negative_code_scalar_empty_1 dst_negative_scale_scalar_empty_1. (((G) = (((((dst_positive_code_scalar_empty_1) + (dst_positive_scale_scalar_empty_1)) * S ((dst_positive_code_scalar_empty_1) + (dst_positive_scale_scalar_empty_1)) + ((dst_positive_scale_scalar_empty_1) + (dst_positive_scale_scalar_empty_1))) + (((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) * S ((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) + ((dst_negative_scale_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)))) * S ((((dst_positive_code_scalar_empty_1) + (dst_positive_scale_scalar_empty_1)) * S ((dst_positive_code_scalar_empty_1) + (dst_positive_scale_scalar_empty_1)) + ((dst_positive_scale_scalar_empty_1) + (dst_positive_scale_scalar_empty_1))) + (((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) * S ((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) + ((dst_negative_scale_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)))) + ((((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) * S ((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) + ((dst_negative_scale_scalar_empty_1) + (dst_negative_scale_scalar_empty_1))) + (((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) * S ((dst_negative_code_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)) + ((dst_negative_scale_scalar_empty_1) + (dst_negative_scale_scalar_empty_1)))))) /\ (forall dst_index_scalar_empty_1. (exists pvs_le_gap_scalar_empty_1domain. pvs_le_gap_scalar_empty_1domain + (dst_index_scalar_empty_1) = (0)) -> exists dst_positive_scalar_empty_1 dst_negative_scalar_empty_1 dst_value_scalar_empty_1. ((((exists ff_h_pvs_scalar_empty_1entrypositive. ff_h_pvs_scalar_empty_1entrypositive + S (dst_positive_scalar_empty_1) = S ((S (dst_index_scalar_empty_1)) * dst_positive_scale_scalar_empty_1)) /\ exists ff_q_pvs_scalar_empty_1entrypositive. dst_positive_code_scalar_empty_1 = ff_q_pvs_scalar_empty_1entrypositive * S ((S (dst_index_scalar_empty_1)) * dst_positive_scale_scalar_empty_1) + (dst_positive_scalar_empty_1))) /\ (((((exists ff_h_pvs_scalar_empty_1entrynegative. ff_h_pvs_scalar_empty_1entrynegative + S (dst_negative_scalar_empty_1) = S ((S (dst_index_scalar_empty_1)) * dst_negative_scale_scalar_empty_1)) /\ exists ff_q_pvs_scalar_empty_1entrynegative. dst_negative_code_scalar_empty_1 = ff_q_pvs_scalar_empty_1entrynegative * S ((S (dst_index_scalar_empty_1)) * dst_negative_scale_scalar_empty_1) + (dst_negative_scalar_empty_1))) /\ (exists ge_balance_positive_scalar_empty_1entryvalue ge_balance_negative_scalar_empty_1entryvalue. (((((dst_value_scalar_empty_1) = 2 * (ge_balance_positive_scalar_empty_1entryvalue) /\ (ge_balance_negative_scalar_empty_1entryvalue) = 0) \/ exists ge_signed_half_scalar_empty_1entryvaluedecode. (((dst_value_scalar_empty_1) = 2 * ge_signed_half_scalar_empty_1entryvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_1entryvalue) = 0) /\ (ge_balance_negative_scalar_empty_1entryvalue) = S ge_signed_half_scalar_empty_1entryvaluedecode))) /\ ((dst_positive_scalar_empty_1) + ge_balance_negative_scalar_empty_1entryvalue = (dst_negative_scalar_empty_1) + ge_balance_positive_scalar_empty_1entryvalue))))))))) -> (((exists dst_positive_code_scalar_empty_resultinput_table dst_positive_scale_scalar_empty_resultinput_table dst_negative_code_scalar_empty_resultinput_table dst_negative_scale_scalar_empty_resultinput_table. (((F) = (((((dst_positive_code_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table)) * S ((dst_positive_code_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table)) + ((dst_positive_scale_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table))) + (((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) * S ((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) + ((dst_negative_scale_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)))) * S ((((dst_positive_code_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table)) * S ((dst_positive_code_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table)) + ((dst_positive_scale_scalar_empty_resultinput_table) + (dst_positive_scale_scalar_empty_resultinput_table))) + (((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) * S ((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) + ((dst_negative_scale_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)))) + ((((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) * S ((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) + ((dst_negative_scale_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table))) + (((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) * S ((dst_negative_code_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)) + ((dst_negative_scale_scalar_empty_resultinput_table) + (dst_negative_scale_scalar_empty_resultinput_table)))))) /\ (forall dst_index_scalar_empty_resultinput_table. (exists pvs_le_gap_scalar_empty_resultinput_tabledomain. pvs_le_gap_scalar_empty_resultinput_tabledomain + (dst_index_scalar_empty_resultinput_table) = (0)) -> exists dst_positive_scalar_empty_resultinput_table dst_negative_scalar_empty_resultinput_table dst_value_scalar_empty_resultinput_table. ((((exists ff_h_pvs_scalar_empty_resultinput_tableentrypositive. ff_h_pvs_scalar_empty_resultinput_tableentrypositive + S (dst_positive_scalar_empty_resultinput_table) = S ((S (dst_index_scalar_empty_resultinput_table)) * dst_positive_scale_scalar_empty_resultinput_table)) /\ exists ff_q_pvs_scalar_empty_resultinput_tableentrypositive. dst_positive_code_scalar_empty_resultinput_table = ff_q_pvs_scalar_empty_resultinput_tableentrypositive * S ((S (dst_index_scalar_empty_resultinput_table)) * dst_positive_scale_scalar_empty_resultinput_table) + (dst_positive_scalar_empty_resultinput_table))) /\ (((((exists ff_h_pvs_scalar_empty_resultinput_tableentrynegative. ff_h_pvs_scalar_empty_resultinput_tableentrynegative + S (dst_negative_scalar_empty_resultinput_table) = S ((S (dst_index_scalar_empty_resultinput_table)) * dst_negative_scale_scalar_empty_resultinput_table)) /\ exists ff_q_pvs_scalar_empty_resultinput_tableentrynegative. dst_negative_code_scalar_empty_resultinput_table = ff_q_pvs_scalar_empty_resultinput_tableentrynegative * S ((S (dst_index_scalar_empty_resultinput_table)) * dst_negative_scale_scalar_empty_resultinput_table) + (dst_negative_scalar_empty_resultinput_table))) /\ (exists ge_balance_positive_scalar_empty_resultinput_tableentryvalue ge_balance_negative_scalar_empty_resultinput_tableentryvalue. (((((dst_value_scalar_empty_resultinput_table) = 2 * (ge_balance_positive_scalar_empty_resultinput_tableentryvalue) /\ (ge_balance_negative_scalar_empty_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_empty_resultinput_tableentryvaluedecode. (((dst_value_scalar_empty_resultinput_table) = 2 * ge_signed_half_scalar_empty_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_empty_resultinput_tableentryvalue) = S ge_signed_half_scalar_empty_resultinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_empty_resultinput_table) + ge_balance_negative_scalar_empty_resultinput_tableentryvalue = (dst_negative_scalar_empty_resultinput_table) + ge_balance_positive_scalar_empty_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_empty_resultoutput_table dst_positive_scale_scalar_empty_resultoutput_table dst_negative_code_scalar_empty_resultoutput_table dst_negative_scale_scalar_empty_resultoutput_table. (((G) = (((((dst_positive_code_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table)) * S ((dst_positive_code_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table)) + ((dst_positive_scale_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table))) + (((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) * S ((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) + ((dst_negative_scale_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)))) * S ((((dst_positive_code_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table)) * S ((dst_positive_code_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table)) + ((dst_positive_scale_scalar_empty_resultoutput_table) + (dst_positive_scale_scalar_empty_resultoutput_table))) + (((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) * S ((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) + ((dst_negative_scale_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)))) + ((((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) * S ((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) + ((dst_negative_scale_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table))) + (((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) * S ((dst_negative_code_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)) + ((dst_negative_scale_scalar_empty_resultoutput_table) + (dst_negative_scale_scalar_empty_resultoutput_table)))))) /\ (forall dst_index_scalar_empty_resultoutput_table. (exists pvs_le_gap_scalar_empty_resultoutput_tabledomain. pvs_le_gap_scalar_empty_resultoutput_tabledomain + (dst_index_scalar_empty_resultoutput_table) = (0)) -> exists dst_positive_scalar_empty_resultoutput_table dst_negative_scalar_empty_resultoutput_table dst_value_scalar_empty_resultoutput_table. ((((exists ff_h_pvs_scalar_empty_resultoutput_tableentrypositive. ff_h_pvs_scalar_empty_resultoutput_tableentrypositive + S (dst_positive_scalar_empty_resultoutput_table) = S ((S (dst_index_scalar_empty_resultoutput_table)) * dst_positive_scale_scalar_empty_resultoutput_table)) /\ exists ff_q_pvs_scalar_empty_resultoutput_tableentrypositive. dst_positive_code_scalar_empty_resultoutput_table = ff_q_pvs_scalar_empty_resultoutput_tableentrypositive * S ((S (dst_index_scalar_empty_resultoutput_table)) * dst_positive_scale_scalar_empty_resultoutput_table) + (dst_positive_scalar_empty_resultoutput_table))) /\ (((((exists ff_h_pvs_scalar_empty_resultoutput_tableentrynegative. ff_h_pvs_scalar_empty_resultoutput_tableentrynegative + S (dst_negative_scalar_empty_resultoutput_table) = S ((S (dst_index_scalar_empty_resultoutput_table)) * dst_negative_scale_scalar_empty_resultoutput_table)) /\ exists ff_q_pvs_scalar_empty_resultoutput_tableentrynegative. dst_negative_code_scalar_empty_resultoutput_table = ff_q_pvs_scalar_empty_resultoutput_tableentrynegative * S ((S (dst_index_scalar_empty_resultoutput_table)) * dst_negative_scale_scalar_empty_resultoutput_table) + (dst_negative_scalar_empty_resultoutput_table))) /\ (exists ge_balance_positive_scalar_empty_resultoutput_tableentryvalue ge_balance_negative_scalar_empty_resultoutput_tableentryvalue. (((((dst_value_scalar_empty_resultoutput_table) = 2 * (ge_balance_positive_scalar_empty_resultoutput_tableentryvalue) /\ (ge_balance_negative_scalar_empty_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_empty_resultoutput_tableentryvaluedecode. (((dst_value_scalar_empty_resultoutput_table) = 2 * ge_signed_half_scalar_empty_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_empty_resultoutput_tableentryvalue) = S ge_signed_half_scalar_empty_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_empty_resultoutput_table) + ge_balance_negative_scalar_empty_resultoutput_tableentryvalue = (dst_negative_scalar_empty_resultoutput_table) + ge_balance_positive_scalar_empty_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_empty_resultentries. (exists pvs_gap_scalar_empty_resultentriesbound. pvs_gap_scalar_empty_resultentriesbound + S (sto_index_scalar_empty_resultentries) = (0)) -> exists sto_input_scalar_empty_resultentries sto_output_scalar_empty_resultentries. ((exists dst_positive_code_scalar_empty_resultentriesentryinput dst_positive_scale_scalar_empty_resultentriesentryinput dst_negative_code_scalar_empty_resultentriesentryinput dst_negative_scale_scalar_empty_resultentriesentryinput dst_positive_scalar_empty_resultentriesentryinput dst_negative_scalar_empty_resultentriesentryinput. (((F) = (((((dst_positive_code_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput)) * S ((dst_positive_code_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput)) + ((dst_positive_scale_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput))) + (((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) * S ((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) + ((dst_negative_scale_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)))) * S ((((dst_positive_code_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput)) * S ((dst_positive_code_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput)) + ((dst_positive_scale_scalar_empty_resultentriesentryinput) + (dst_positive_scale_scalar_empty_resultentriesentryinput))) + (((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) * S ((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) + ((dst_negative_scale_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)))) + ((((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) * S ((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) + ((dst_negative_scale_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput))) + (((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) * S ((dst_negative_code_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)) + ((dst_negative_scale_scalar_empty_resultentriesentryinput) + (dst_negative_scale_scalar_empty_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_empty_resultentriesentryinputpositive. ff_h_pvs_scalar_empty_resultentriesentryinputpositive + S (dst_positive_scalar_empty_resultentriesentryinput) = S ((S (sto_index_scalar_empty_resultentries)) * dst_positive_scale_scalar_empty_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_empty_resultentriesentryinputpositive. dst_positive_code_scalar_empty_resultentriesentryinput = ff_q_pvs_scalar_empty_resultentriesentryinputpositive * S ((S (sto_index_scalar_empty_resultentries)) * dst_positive_scale_scalar_empty_resultentriesentryinput) + (dst_positive_scalar_empty_resultentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_empty_resultentriesentryinputnegative. ff_h_pvs_scalar_empty_resultentriesentryinputnegative + S (dst_negative_scalar_empty_resultentriesentryinput) = S ((S (sto_index_scalar_empty_resultentries)) * dst_negative_scale_scalar_empty_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_empty_resultentriesentryinputnegative. dst_negative_code_scalar_empty_resultentriesentryinput = ff_q_pvs_scalar_empty_resultentriesentryinputnegative * S ((S (sto_index_scalar_empty_resultentries)) * dst_negative_scale_scalar_empty_resultentriesentryinput) + (dst_negative_scalar_empty_resultentriesentryinput))) /\ (exists ge_balance_positive_scalar_empty_resultentriesentryinputvalue ge_balance_negative_scalar_empty_resultentriesentryinputvalue. (((((sto_input_scalar_empty_resultentries) = 2 * (ge_balance_positive_scalar_empty_resultentriesentryinputvalue) /\ (ge_balance_negative_scalar_empty_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_empty_resultentriesentryinputvaluedecode. (((sto_input_scalar_empty_resultentries) = 2 * ge_signed_half_scalar_empty_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_empty_resultentriesentryinputvalue) = S ge_signed_half_scalar_empty_resultentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_empty_resultentriesentryinput) + ge_balance_negative_scalar_empty_resultentriesentryinputvalue = (dst_negative_scalar_empty_resultentriesentryinput) + ge_balance_positive_scalar_empty_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_empty_resultentriesentryoutput dst_positive_scale_scalar_empty_resultentriesentryoutput dst_negative_code_scalar_empty_resultentriesentryoutput dst_negative_scale_scalar_empty_resultentriesentryoutput dst_positive_scalar_empty_resultentriesentryoutput dst_negative_scalar_empty_resultentriesentryoutput. (((G) = (((((dst_positive_code_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_positive_code_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput)) + ((dst_positive_scale_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput))) + (((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) + ((dst_negative_scale_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)))) * S ((((dst_positive_code_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_positive_code_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput)) + ((dst_positive_scale_scalar_empty_resultentriesentryoutput) + (dst_positive_scale_scalar_empty_resultentriesentryoutput))) + (((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) + ((dst_negative_scale_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)))) + ((((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) + ((dst_negative_scale_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput))) + (((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) * S ((dst_negative_code_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)) + ((dst_negative_scale_scalar_empty_resultentriesentryoutput) + (dst_negative_scale_scalar_empty_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_empty_resultentriesentryoutputpositive. ff_h_pvs_scalar_empty_resultentriesentryoutputpositive + S (dst_positive_scalar_empty_resultentriesentryoutput) = S ((S (sto_index_scalar_empty_resultentries)) * dst_positive_scale_scalar_empty_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_empty_resultentriesentryoutputpositive. dst_positive_code_scalar_empty_resultentriesentryoutput = ff_q_pvs_scalar_empty_resultentriesentryoutputpositive * S ((S (sto_index_scalar_empty_resultentries)) * dst_positive_scale_scalar_empty_resultentriesentryoutput) + (dst_positive_scalar_empty_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_empty_resultentriesentryoutputnegative. ff_h_pvs_scalar_empty_resultentriesentryoutputnegative + S (dst_negative_scalar_empty_resultentriesentryoutput) = S ((S (sto_index_scalar_empty_resultentries)) * dst_negative_scale_scalar_empty_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_empty_resultentriesentryoutputnegative. dst_negative_code_scalar_empty_resultentriesentryoutput = ff_q_pvs_scalar_empty_resultentriesentryoutputnegative * S ((S (sto_index_scalar_empty_resultentries)) * dst_negative_scale_scalar_empty_resultentriesentryoutput) + (dst_negative_scalar_empty_resultentriesentryoutput))) /\ (exists ge_balance_positive_scalar_empty_resultentriesentryoutputvalue ge_balance_negative_scalar_empty_resultentriesentryoutputvalue. (((((sto_output_scalar_empty_resultentries) = 2 * (ge_balance_positive_scalar_empty_resultentriesentryoutputvalue) /\ (ge_balance_negative_scalar_empty_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_empty_resultentriesentryoutputvaluedecode. (((sto_output_scalar_empty_resultentries) = 2 * ge_signed_half_scalar_empty_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_empty_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_empty_resultentriesentryoutputvalue) = S ge_signed_half_scalar_empty_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_empty_resultentriesentryoutput) + ge_balance_negative_scalar_empty_resultentriesentryoutputvalue = (dst_negative_scalar_empty_resultentriesentryoutput) + ge_balance_positive_scalar_empty_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_empty_resultentriesentryoperation sto_an_scalar_empty_resultentriesentryoperation sto_bp_scalar_empty_resultentriesentryoperation sto_bn_scalar_empty_resultentriesentryoperation sto_cp_scalar_empty_resultentriesentryoperation sto_cn_scalar_empty_resultentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_empty_resultentriesentryoperation) /\ (sto_an_scalar_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_empty_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_empty_resultentriesentryoperationleft + 1 /\ (sto_ap_scalar_empty_resultentriesentryoperation) = 0) /\ (sto_an_scalar_empty_resultentriesentryoperation) = S ge_signed_half_scalar_empty_resultentriesentryoperationleft))) /\ ((((((sto_input_scalar_empty_resultentries) = 2 * (sto_bp_scalar_empty_resultentriesentryoperation) /\ (sto_bn_scalar_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_empty_resultentriesentryoperationright. (((sto_input_scalar_empty_resultentries) = 2 * ge_signed_half_scalar_empty_resultentriesentryoperationright + 1 /\ (sto_bp_scalar_empty_resultentriesentryoperation) = 0) /\ (sto_bn_scalar_empty_resultentriesentryoperation) = S ge_signed_half_scalar_empty_resultentriesentryoperationright))) /\ ((((((sto_output_scalar_empty_resultentries) = 2 * (sto_cp_scalar_empty_resultentriesentryoperation) /\ (sto_cn_scalar_empty_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_empty_resultentriesentryoperationoutput. (((sto_output_scalar_empty_resultentries) = 2 * ge_signed_half_scalar_empty_resultentriesentryoperationoutput + 1 /\ (sto_cp_scalar_empty_resultentriesentryoperation) = 0) /\ (sto_cn_scalar_empty_resultentriesentryoperation) = S ge_signed_half_scalar_empty_resultentriesentryoperationoutput))) /\ ((sto_ap_scalar_empty_resultentriesentryoperation * sto_bp_scalar_empty_resultentriesentryoperation + sto_an_scalar_empty_resultentriesentryoperation * sto_bn_scalar_empty_resultentriesentryoperation) + sto_cn_scalar_empty_resultentriesentryoperation = (sto_ap_scalar_empty_resultentriesentryoperation * sto_bn_scalar_empty_resultentriesentryoperation + sto_an_scalar_empty_resultentriesentryoperation * sto_bp_scalar_empty_resultentriesentryoperation) + sto_cp_scalar_empty_resultentriesentryoperation)))))))))))))))