signed_table_scalar_exists_extensionally_unique

Exact expanded first-order arithmetic statement

forall l a F. (exists dst_positive_code_scalar_exists_unique_input0 dst_positive_scale_scalar_exists_unique_input0 dst_negative_code_scalar_exists_unique_input0 dst_negative_scale_scalar_exists_unique_input0. (((F) = (((((dst_positive_code_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0)) * S ((dst_positive_code_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0)) + ((dst_positive_scale_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0))) + (((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) * S ((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) + ((dst_negative_scale_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)))) * S ((((dst_positive_code_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0)) * S ((dst_positive_code_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0)) + ((dst_positive_scale_scalar_exists_unique_input0) + (dst_positive_scale_scalar_exists_unique_input0))) + (((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) * S ((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) + ((dst_negative_scale_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)))) + ((((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) * S ((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) + ((dst_negative_scale_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0))) + (((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) * S ((dst_negative_code_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)) + ((dst_negative_scale_scalar_exists_unique_input0) + (dst_negative_scale_scalar_exists_unique_input0)))))) /\ (forall dst_index_scalar_exists_unique_input0. (exists pvs_le_gap_scalar_exists_unique_input0domain. pvs_le_gap_scalar_exists_unique_input0domain + (dst_index_scalar_exists_unique_input0) = (l)) -> exists dst_positive_scalar_exists_unique_input0 dst_negative_scalar_exists_unique_input0 dst_value_scalar_exists_unique_input0. ((((exists ff_h_pvs_scalar_exists_unique_input0entrypositive. ff_h_pvs_scalar_exists_unique_input0entrypositive + S (dst_positive_scalar_exists_unique_input0) = S ((S (dst_index_scalar_exists_unique_input0)) * dst_positive_scale_scalar_exists_unique_input0)) /\ exists ff_q_pvs_scalar_exists_unique_input0entrypositive. dst_positive_code_scalar_exists_unique_input0 = ff_q_pvs_scalar_exists_unique_input0entrypositive * S ((S (dst_index_scalar_exists_unique_input0)) * dst_positive_scale_scalar_exists_unique_input0) + (dst_positive_scalar_exists_unique_input0))) /\ (((((exists ff_h_pvs_scalar_exists_unique_input0entrynegative. ff_h_pvs_scalar_exists_unique_input0entrynegative + S (dst_negative_scalar_exists_unique_input0) = S ((S (dst_index_scalar_exists_unique_input0)) * dst_negative_scale_scalar_exists_unique_input0)) /\ exists ff_q_pvs_scalar_exists_unique_input0entrynegative. dst_negative_code_scalar_exists_unique_input0 = ff_q_pvs_scalar_exists_unique_input0entrynegative * S ((S (dst_index_scalar_exists_unique_input0)) * dst_negative_scale_scalar_exists_unique_input0) + (dst_negative_scalar_exists_unique_input0))) /\ (exists ge_balance_positive_scalar_exists_unique_input0entryvalue ge_balance_negative_scalar_exists_unique_input0entryvalue. (((((dst_value_scalar_exists_unique_input0) = 2 * (ge_balance_positive_scalar_exists_unique_input0entryvalue) /\ (ge_balance_negative_scalar_exists_unique_input0entryvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_input0entryvaluedecode. (((dst_value_scalar_exists_unique_input0) = 2 * ge_signed_half_scalar_exists_unique_input0entryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_input0entryvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_input0entryvalue) = S ge_signed_half_scalar_exists_unique_input0entryvaluedecode))) /\ ((dst_positive_scalar_exists_unique_input0) + ge_balance_negative_scalar_exists_unique_input0entryvalue = (dst_negative_scalar_exists_unique_input0) + ge_balance_positive_scalar_exists_unique_input0entryvalue))))))))) -> exists G. ((((exists dst_positive_code_scalar_exists_unique_resultinput_table dst_positive_scale_scalar_exists_unique_resultinput_table dst_negative_code_scalar_exists_unique_resultinput_table dst_negative_scale_scalar_exists_unique_resultinput_table. (((F) = (((((dst_positive_code_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table)) * S ((dst_positive_code_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table)) + ((dst_positive_scale_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table))) + (((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) * S ((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) + ((dst_negative_scale_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)))) * S ((((dst_positive_code_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table)) * S ((dst_positive_code_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table)) + ((dst_positive_scale_scalar_exists_unique_resultinput_table) + (dst_positive_scale_scalar_exists_unique_resultinput_table))) + (((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) * S ((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) + ((dst_negative_scale_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)))) + ((((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) * S ((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) + ((dst_negative_scale_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table))) + (((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) * S ((dst_negative_code_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)) + ((dst_negative_scale_scalar_exists_unique_resultinput_table) + (dst_negative_scale_scalar_exists_unique_resultinput_table)))))) /\ (forall dst_index_scalar_exists_unique_resultinput_table. (exists pvs_le_gap_scalar_exists_unique_resultinput_tabledomain. pvs_le_gap_scalar_exists_unique_resultinput_tabledomain + (dst_index_scalar_exists_unique_resultinput_table) = (l)) -> exists dst_positive_scalar_exists_unique_resultinput_table dst_negative_scalar_exists_unique_resultinput_table dst_value_scalar_exists_unique_resultinput_table. ((((exists ff_h_pvs_scalar_exists_unique_resultinput_tableentrypositive. ff_h_pvs_scalar_exists_unique_resultinput_tableentrypositive + S (dst_positive_scalar_exists_unique_resultinput_table) = S ((S (dst_index_scalar_exists_unique_resultinput_table)) * dst_positive_scale_scalar_exists_unique_resultinput_table)) /\ exists ff_q_pvs_scalar_exists_unique_resultinput_tableentrypositive. dst_positive_code_scalar_exists_unique_resultinput_table = ff_q_pvs_scalar_exists_unique_resultinput_tableentrypositive * S ((S (dst_index_scalar_exists_unique_resultinput_table)) * dst_positive_scale_scalar_exists_unique_resultinput_table) + (dst_positive_scalar_exists_unique_resultinput_table))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultinput_tableentrynegative. ff_h_pvs_scalar_exists_unique_resultinput_tableentrynegative + S (dst_negative_scalar_exists_unique_resultinput_table) = S ((S (dst_index_scalar_exists_unique_resultinput_table)) * dst_negative_scale_scalar_exists_unique_resultinput_table)) /\ exists ff_q_pvs_scalar_exists_unique_resultinput_tableentrynegative. dst_negative_code_scalar_exists_unique_resultinput_table = ff_q_pvs_scalar_exists_unique_resultinput_tableentrynegative * S ((S (dst_index_scalar_exists_unique_resultinput_table)) * dst_negative_scale_scalar_exists_unique_resultinput_table) + (dst_negative_scalar_exists_unique_resultinput_table))) /\ (exists ge_balance_positive_scalar_exists_unique_resultinput_tableentryvalue ge_balance_negative_scalar_exists_unique_resultinput_tableentryvalue. (((((dst_value_scalar_exists_unique_resultinput_table) = 2 * (ge_balance_positive_scalar_exists_unique_resultinput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_unique_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultinput_tableentryvaluedecode. (((dst_value_scalar_exists_unique_resultinput_table) = 2 * ge_signed_half_scalar_exists_unique_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_resultinput_tableentryvalue) = S ge_signed_half_scalar_exists_unique_resultinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_unique_resultinput_table) + ge_balance_negative_scalar_exists_unique_resultinput_tableentryvalue = (dst_negative_scalar_exists_unique_resultinput_table) + ge_balance_positive_scalar_exists_unique_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_unique_resultoutput_table dst_positive_scale_scalar_exists_unique_resultoutput_table dst_negative_code_scalar_exists_unique_resultoutput_table dst_negative_scale_scalar_exists_unique_resultoutput_table. (((G) = (((((dst_positive_code_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_positive_code_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table)) + ((dst_positive_scale_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table))) + (((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) + ((dst_negative_scale_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)))) * S ((((dst_positive_code_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_positive_code_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table)) + ((dst_positive_scale_scalar_exists_unique_resultoutput_table) + (dst_positive_scale_scalar_exists_unique_resultoutput_table))) + (((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) + ((dst_negative_scale_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)))) + ((((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) + ((dst_negative_scale_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table))) + (((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) * S ((dst_negative_code_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)) + ((dst_negative_scale_scalar_exists_unique_resultoutput_table) + (dst_negative_scale_scalar_exists_unique_resultoutput_table)))))) /\ (forall dst_index_scalar_exists_unique_resultoutput_table. (exists pvs_le_gap_scalar_exists_unique_resultoutput_tabledomain. pvs_le_gap_scalar_exists_unique_resultoutput_tabledomain + (dst_index_scalar_exists_unique_resultoutput_table) = (l)) -> exists dst_positive_scalar_exists_unique_resultoutput_table dst_negative_scalar_exists_unique_resultoutput_table dst_value_scalar_exists_unique_resultoutput_table. ((((exists ff_h_pvs_scalar_exists_unique_resultoutput_tableentrypositive. ff_h_pvs_scalar_exists_unique_resultoutput_tableentrypositive + S (dst_positive_scalar_exists_unique_resultoutput_table) = S ((S (dst_index_scalar_exists_unique_resultoutput_table)) * dst_positive_scale_scalar_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_scalar_exists_unique_resultoutput_tableentrypositive. dst_positive_code_scalar_exists_unique_resultoutput_table = ff_q_pvs_scalar_exists_unique_resultoutput_tableentrypositive * S ((S (dst_index_scalar_exists_unique_resultoutput_table)) * dst_positive_scale_scalar_exists_unique_resultoutput_table) + (dst_positive_scalar_exists_unique_resultoutput_table))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultoutput_tableentrynegative. ff_h_pvs_scalar_exists_unique_resultoutput_tableentrynegative + S (dst_negative_scalar_exists_unique_resultoutput_table) = S ((S (dst_index_scalar_exists_unique_resultoutput_table)) * dst_negative_scale_scalar_exists_unique_resultoutput_table)) /\ exists ff_q_pvs_scalar_exists_unique_resultoutput_tableentrynegative. dst_negative_code_scalar_exists_unique_resultoutput_table = ff_q_pvs_scalar_exists_unique_resultoutput_tableentrynegative * S ((S (dst_index_scalar_exists_unique_resultoutput_table)) * dst_negative_scale_scalar_exists_unique_resultoutput_table) + (dst_negative_scalar_exists_unique_resultoutput_table))) /\ (exists ge_balance_positive_scalar_exists_unique_resultoutput_tableentryvalue ge_balance_negative_scalar_exists_unique_resultoutput_tableentryvalue. (((((dst_value_scalar_exists_unique_resultoutput_table) = 2 * (ge_balance_positive_scalar_exists_unique_resultoutput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_unique_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultoutput_tableentryvaluedecode. (((dst_value_scalar_exists_unique_resultoutput_table) = 2 * ge_signed_half_scalar_exists_unique_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_resultoutput_tableentryvalue) = S ge_signed_half_scalar_exists_unique_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_unique_resultoutput_table) + ge_balance_negative_scalar_exists_unique_resultoutput_tableentryvalue = (dst_negative_scalar_exists_unique_resultoutput_table) + ge_balance_positive_scalar_exists_unique_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_exists_unique_resultentries. (exists pvs_gap_scalar_exists_unique_resultentriesbound. pvs_gap_scalar_exists_unique_resultentriesbound + S (sto_index_scalar_exists_unique_resultentries) = (l)) -> exists sto_input_scalar_exists_unique_resultentries sto_output_scalar_exists_unique_resultentries. ((exists dst_positive_code_scalar_exists_unique_resultentriesentryinput dst_positive_scale_scalar_exists_unique_resultentriesentryinput dst_negative_code_scalar_exists_unique_resultentriesentryinput dst_negative_scale_scalar_exists_unique_resultentriesentryinput dst_positive_scalar_exists_unique_resultentriesentryinput dst_negative_scalar_exists_unique_resultentriesentryinput. (((F) = (((((dst_positive_code_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_positive_code_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_positive_scale_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)))) * S ((((dst_positive_code_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_positive_code_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_positive_scale_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)))) + ((((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultentriesentryinputpositive. ff_h_pvs_scalar_exists_unique_resultentriesentryinputpositive + S (dst_positive_scalar_exists_unique_resultentriesentryinput) = S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_positive_scale_scalar_exists_unique_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_unique_resultentriesentryinputpositive. dst_positive_code_scalar_exists_unique_resultentriesentryinput = ff_q_pvs_scalar_exists_unique_resultentriesentryinputpositive * S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_positive_scale_scalar_exists_unique_resultentriesentryinput) + (dst_positive_scalar_exists_unique_resultentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultentriesentryinputnegative. ff_h_pvs_scalar_exists_unique_resultentriesentryinputnegative + S (dst_negative_scalar_exists_unique_resultentriesentryinput) = S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_negative_scale_scalar_exists_unique_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_unique_resultentriesentryinputnegative. dst_negative_code_scalar_exists_unique_resultentriesentryinput = ff_q_pvs_scalar_exists_unique_resultentriesentryinputnegative * S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_negative_scale_scalar_exists_unique_resultentriesentryinput) + (dst_negative_scalar_exists_unique_resultentriesentryinput))) /\ (exists ge_balance_positive_scalar_exists_unique_resultentriesentryinputvalue ge_balance_negative_scalar_exists_unique_resultentriesentryinputvalue. (((((sto_input_scalar_exists_unique_resultentries) = 2 * (ge_balance_positive_scalar_exists_unique_resultentriesentryinputvalue) /\ (ge_balance_negative_scalar_exists_unique_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultentriesentryinputvaluedecode. (((sto_input_scalar_exists_unique_resultentries) = 2 * ge_signed_half_scalar_exists_unique_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_resultentriesentryinputvalue) = S ge_signed_half_scalar_exists_unique_resultentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_exists_unique_resultentriesentryinput) + ge_balance_negative_scalar_exists_unique_resultentriesentryinputvalue = (dst_negative_scalar_exists_unique_resultentriesentryinput) + ge_balance_positive_scalar_exists_unique_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_unique_resultentriesentryoutput dst_positive_scale_scalar_exists_unique_resultentriesentryoutput dst_negative_code_scalar_exists_unique_resultentriesentryoutput dst_negative_scale_scalar_exists_unique_resultentriesentryoutput dst_positive_scalar_exists_unique_resultentriesentryoutput dst_negative_scalar_exists_unique_resultentriesentryoutput. (((G) = (((((dst_positive_code_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_positive_code_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_positive_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)))) * S ((((dst_positive_code_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_positive_code_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_positive_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)))) + ((((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultentriesentryoutputpositive. ff_h_pvs_scalar_exists_unique_resultentriesentryoutputpositive + S (dst_positive_scalar_exists_unique_resultentriesentryoutput) = S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_positive_scale_scalar_exists_unique_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_unique_resultentriesentryoutputpositive. dst_positive_code_scalar_exists_unique_resultentriesentryoutput = ff_q_pvs_scalar_exists_unique_resultentriesentryoutputpositive * S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_positive_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_positive_scalar_exists_unique_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_exists_unique_resultentriesentryoutputnegative. ff_h_pvs_scalar_exists_unique_resultentriesentryoutputnegative + S (dst_negative_scalar_exists_unique_resultentriesentryoutput) = S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_negative_scale_scalar_exists_unique_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_unique_resultentriesentryoutputnegative. dst_negative_code_scalar_exists_unique_resultentriesentryoutput = ff_q_pvs_scalar_exists_unique_resultentriesentryoutputnegative * S ((S (sto_index_scalar_exists_unique_resultentries)) * dst_negative_scale_scalar_exists_unique_resultentriesentryoutput) + (dst_negative_scalar_exists_unique_resultentriesentryoutput))) /\ (exists ge_balance_positive_scalar_exists_unique_resultentriesentryoutputvalue ge_balance_negative_scalar_exists_unique_resultentriesentryoutputvalue. (((((sto_output_scalar_exists_unique_resultentries) = 2 * (ge_balance_positive_scalar_exists_unique_resultentriesentryoutputvalue) /\ (ge_balance_negative_scalar_exists_unique_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultentriesentryoutputvaluedecode. (((sto_output_scalar_exists_unique_resultentries) = 2 * ge_signed_half_scalar_exists_unique_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_resultentriesentryoutputvalue) = S ge_signed_half_scalar_exists_unique_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_exists_unique_resultentriesentryoutput) + ge_balance_negative_scalar_exists_unique_resultentriesentryoutputvalue = (dst_negative_scalar_exists_unique_resultentriesentryoutput) + ge_balance_positive_scalar_exists_unique_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_exists_unique_resultentriesentryoperation sto_an_scalar_exists_unique_resultentriesentryoperation sto_bp_scalar_exists_unique_resultentriesentryoperation sto_bn_scalar_exists_unique_resultentriesentryoperation sto_cp_scalar_exists_unique_resultentriesentryoperation sto_cn_scalar_exists_unique_resultentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_exists_unique_resultentriesentryoperation) /\ (sto_an_scalar_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_exists_unique_resultentriesentryoperationleft + 1 /\ (sto_ap_scalar_exists_unique_resultentriesentryoperation) = 0) /\ (sto_an_scalar_exists_unique_resultentriesentryoperation) = S ge_signed_half_scalar_exists_unique_resultentriesentryoperationleft))) /\ ((((((sto_input_scalar_exists_unique_resultentries) = 2 * (sto_bp_scalar_exists_unique_resultentriesentryoperation) /\ (sto_bn_scalar_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultentriesentryoperationright. (((sto_input_scalar_exists_unique_resultentries) = 2 * ge_signed_half_scalar_exists_unique_resultentriesentryoperationright + 1 /\ (sto_bp_scalar_exists_unique_resultentriesentryoperation) = 0) /\ (sto_bn_scalar_exists_unique_resultentriesentryoperation) = S ge_signed_half_scalar_exists_unique_resultentriesentryoperationright))) /\ ((((((sto_output_scalar_exists_unique_resultentries) = 2 * (sto_cp_scalar_exists_unique_resultentriesentryoperation) /\ (sto_cn_scalar_exists_unique_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_resultentriesentryoperationoutput. (((sto_output_scalar_exists_unique_resultentries) = 2 * ge_signed_half_scalar_exists_unique_resultentriesentryoperationoutput + 1 /\ (sto_cp_scalar_exists_unique_resultentriesentryoperation) = 0) /\ (sto_cn_scalar_exists_unique_resultentriesentryoperation) = S ge_signed_half_scalar_exists_unique_resultentriesentryoperationoutput))) /\ ((sto_ap_scalar_exists_unique_resultentriesentryoperation * sto_bp_scalar_exists_unique_resultentriesentryoperation + sto_an_scalar_exists_unique_resultentriesentryoperation * sto_bn_scalar_exists_unique_resultentriesentryoperation) + sto_cn_scalar_exists_unique_resultentriesentryoperation = (sto_ap_scalar_exists_unique_resultentriesentryoperation * sto_bn_scalar_exists_unique_resultentriesentryoperation + sto_an_scalar_exists_unique_resultentriesentryoperation * sto_bp_scalar_exists_unique_resultentriesentryoperation) + sto_cp_scalar_exists_unique_resultentriesentryoperation))))))))))))))) /\ (forall K. (((exists dst_positive_code_scalar_exists_unique_otherinput_table dst_positive_scale_scalar_exists_unique_otherinput_table dst_negative_code_scalar_exists_unique_otherinput_table dst_negative_scale_scalar_exists_unique_otherinput_table. (((F) = (((((dst_positive_code_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table)) * S ((dst_positive_code_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table)) + ((dst_positive_scale_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table))) + (((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) * S ((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) + ((dst_negative_scale_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)))) * S ((((dst_positive_code_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table)) * S ((dst_positive_code_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table)) + ((dst_positive_scale_scalar_exists_unique_otherinput_table) + (dst_positive_scale_scalar_exists_unique_otherinput_table))) + (((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) * S ((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) + ((dst_negative_scale_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)))) + ((((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) * S ((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) + ((dst_negative_scale_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table))) + (((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) * S ((dst_negative_code_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)) + ((dst_negative_scale_scalar_exists_unique_otherinput_table) + (dst_negative_scale_scalar_exists_unique_otherinput_table)))))) /\ (forall dst_index_scalar_exists_unique_otherinput_table. (exists pvs_le_gap_scalar_exists_unique_otherinput_tabledomain. pvs_le_gap_scalar_exists_unique_otherinput_tabledomain + (dst_index_scalar_exists_unique_otherinput_table) = (l)) -> exists dst_positive_scalar_exists_unique_otherinput_table dst_negative_scalar_exists_unique_otherinput_table dst_value_scalar_exists_unique_otherinput_table. ((((exists ff_h_pvs_scalar_exists_unique_otherinput_tableentrypositive. ff_h_pvs_scalar_exists_unique_otherinput_tableentrypositive + S (dst_positive_scalar_exists_unique_otherinput_table) = S ((S (dst_index_scalar_exists_unique_otherinput_table)) * dst_positive_scale_scalar_exists_unique_otherinput_table)) /\ exists ff_q_pvs_scalar_exists_unique_otherinput_tableentrypositive. dst_positive_code_scalar_exists_unique_otherinput_table = ff_q_pvs_scalar_exists_unique_otherinput_tableentrypositive * S ((S (dst_index_scalar_exists_unique_otherinput_table)) * dst_positive_scale_scalar_exists_unique_otherinput_table) + (dst_positive_scalar_exists_unique_otherinput_table))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otherinput_tableentrynegative. ff_h_pvs_scalar_exists_unique_otherinput_tableentrynegative + S (dst_negative_scalar_exists_unique_otherinput_table) = S ((S (dst_index_scalar_exists_unique_otherinput_table)) * dst_negative_scale_scalar_exists_unique_otherinput_table)) /\ exists ff_q_pvs_scalar_exists_unique_otherinput_tableentrynegative. dst_negative_code_scalar_exists_unique_otherinput_table = ff_q_pvs_scalar_exists_unique_otherinput_tableentrynegative * S ((S (dst_index_scalar_exists_unique_otherinput_table)) * dst_negative_scale_scalar_exists_unique_otherinput_table) + (dst_negative_scalar_exists_unique_otherinput_table))) /\ (exists ge_balance_positive_scalar_exists_unique_otherinput_tableentryvalue ge_balance_negative_scalar_exists_unique_otherinput_tableentryvalue. (((((dst_value_scalar_exists_unique_otherinput_table) = 2 * (ge_balance_positive_scalar_exists_unique_otherinput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_unique_otherinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherinput_tableentryvaluedecode. (((dst_value_scalar_exists_unique_otherinput_table) = 2 * ge_signed_half_scalar_exists_unique_otherinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_otherinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_otherinput_tableentryvalue) = S ge_signed_half_scalar_exists_unique_otherinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_unique_otherinput_table) + ge_balance_negative_scalar_exists_unique_otherinput_tableentryvalue = (dst_negative_scalar_exists_unique_otherinput_table) + ge_balance_positive_scalar_exists_unique_otherinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_unique_otheroutput_table dst_positive_scale_scalar_exists_unique_otheroutput_table dst_negative_code_scalar_exists_unique_otheroutput_table dst_negative_scale_scalar_exists_unique_otheroutput_table. (((K) = (((((dst_positive_code_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_positive_code_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table)) + ((dst_positive_scale_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table))) + (((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) + ((dst_negative_scale_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)))) * S ((((dst_positive_code_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_positive_code_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table)) + ((dst_positive_scale_scalar_exists_unique_otheroutput_table) + (dst_positive_scale_scalar_exists_unique_otheroutput_table))) + (((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) + ((dst_negative_scale_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)))) + ((((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) + ((dst_negative_scale_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table))) + (((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) * S ((dst_negative_code_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)) + ((dst_negative_scale_scalar_exists_unique_otheroutput_table) + (dst_negative_scale_scalar_exists_unique_otheroutput_table)))))) /\ (forall dst_index_scalar_exists_unique_otheroutput_table. (exists pvs_le_gap_scalar_exists_unique_otheroutput_tabledomain. pvs_le_gap_scalar_exists_unique_otheroutput_tabledomain + (dst_index_scalar_exists_unique_otheroutput_table) = (l)) -> exists dst_positive_scalar_exists_unique_otheroutput_table dst_negative_scalar_exists_unique_otheroutput_table dst_value_scalar_exists_unique_otheroutput_table. ((((exists ff_h_pvs_scalar_exists_unique_otheroutput_tableentrypositive. ff_h_pvs_scalar_exists_unique_otheroutput_tableentrypositive + S (dst_positive_scalar_exists_unique_otheroutput_table) = S ((S (dst_index_scalar_exists_unique_otheroutput_table)) * dst_positive_scale_scalar_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_scalar_exists_unique_otheroutput_tableentrypositive. dst_positive_code_scalar_exists_unique_otheroutput_table = ff_q_pvs_scalar_exists_unique_otheroutput_tableentrypositive * S ((S (dst_index_scalar_exists_unique_otheroutput_table)) * dst_positive_scale_scalar_exists_unique_otheroutput_table) + (dst_positive_scalar_exists_unique_otheroutput_table))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otheroutput_tableentrynegative. ff_h_pvs_scalar_exists_unique_otheroutput_tableentrynegative + S (dst_negative_scalar_exists_unique_otheroutput_table) = S ((S (dst_index_scalar_exists_unique_otheroutput_table)) * dst_negative_scale_scalar_exists_unique_otheroutput_table)) /\ exists ff_q_pvs_scalar_exists_unique_otheroutput_tableentrynegative. dst_negative_code_scalar_exists_unique_otheroutput_table = ff_q_pvs_scalar_exists_unique_otheroutput_tableentrynegative * S ((S (dst_index_scalar_exists_unique_otheroutput_table)) * dst_negative_scale_scalar_exists_unique_otheroutput_table) + (dst_negative_scalar_exists_unique_otheroutput_table))) /\ (exists ge_balance_positive_scalar_exists_unique_otheroutput_tableentryvalue ge_balance_negative_scalar_exists_unique_otheroutput_tableentryvalue. (((((dst_value_scalar_exists_unique_otheroutput_table) = 2 * (ge_balance_positive_scalar_exists_unique_otheroutput_tableentryvalue) /\ (ge_balance_negative_scalar_exists_unique_otheroutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_otheroutput_tableentryvaluedecode. (((dst_value_scalar_exists_unique_otheroutput_table) = 2 * ge_signed_half_scalar_exists_unique_otheroutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_otheroutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_otheroutput_tableentryvalue) = S ge_signed_half_scalar_exists_unique_otheroutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_exists_unique_otheroutput_table) + ge_balance_negative_scalar_exists_unique_otheroutput_tableentryvalue = (dst_negative_scalar_exists_unique_otheroutput_table) + ge_balance_positive_scalar_exists_unique_otheroutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_exists_unique_otherentries. (exists pvs_gap_scalar_exists_unique_otherentriesbound. pvs_gap_scalar_exists_unique_otherentriesbound + S (sto_index_scalar_exists_unique_otherentries) = (l)) -> exists sto_input_scalar_exists_unique_otherentries sto_output_scalar_exists_unique_otherentries. ((exists dst_positive_code_scalar_exists_unique_otherentriesentryinput dst_positive_scale_scalar_exists_unique_otherentriesentryinput dst_negative_code_scalar_exists_unique_otherentriesentryinput dst_negative_scale_scalar_exists_unique_otherentriesentryinput dst_positive_scalar_exists_unique_otherentriesentryinput dst_negative_scalar_exists_unique_otherentriesentryinput. (((F) = (((((dst_positive_code_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_positive_code_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_positive_scale_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)))) * S ((((dst_positive_code_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_positive_code_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_positive_scale_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)))) + ((((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otherentriesentryinputpositive. ff_h_pvs_scalar_exists_unique_otherentriesentryinputpositive + S (dst_positive_scalar_exists_unique_otherentriesentryinput) = S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_positive_scale_scalar_exists_unique_otherentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_unique_otherentriesentryinputpositive. dst_positive_code_scalar_exists_unique_otherentriesentryinput = ff_q_pvs_scalar_exists_unique_otherentriesentryinputpositive * S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_positive_scale_scalar_exists_unique_otherentriesentryinput) + (dst_positive_scalar_exists_unique_otherentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otherentriesentryinputnegative. ff_h_pvs_scalar_exists_unique_otherentriesentryinputnegative + S (dst_negative_scalar_exists_unique_otherentriesentryinput) = S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_negative_scale_scalar_exists_unique_otherentriesentryinput)) /\ exists ff_q_pvs_scalar_exists_unique_otherentriesentryinputnegative. dst_negative_code_scalar_exists_unique_otherentriesentryinput = ff_q_pvs_scalar_exists_unique_otherentriesentryinputnegative * S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_negative_scale_scalar_exists_unique_otherentriesentryinput) + (dst_negative_scalar_exists_unique_otherentriesentryinput))) /\ (exists ge_balance_positive_scalar_exists_unique_otherentriesentryinputvalue ge_balance_negative_scalar_exists_unique_otherentriesentryinputvalue. (((((sto_input_scalar_exists_unique_otherentries) = 2 * (ge_balance_positive_scalar_exists_unique_otherentriesentryinputvalue) /\ (ge_balance_negative_scalar_exists_unique_otherentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherentriesentryinputvaluedecode. (((sto_input_scalar_exists_unique_otherentries) = 2 * ge_signed_half_scalar_exists_unique_otherentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_otherentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_otherentriesentryinputvalue) = S ge_signed_half_scalar_exists_unique_otherentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_exists_unique_otherentriesentryinput) + ge_balance_negative_scalar_exists_unique_otherentriesentryinputvalue = (dst_negative_scalar_exists_unique_otherentriesentryinput) + ge_balance_positive_scalar_exists_unique_otherentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_exists_unique_otherentriesentryoutput dst_positive_scale_scalar_exists_unique_otherentriesentryoutput dst_negative_code_scalar_exists_unique_otherentriesentryoutput dst_negative_scale_scalar_exists_unique_otherentriesentryoutput dst_positive_scalar_exists_unique_otherentriesentryoutput dst_negative_scalar_exists_unique_otherentriesentryoutput. (((K) = (((((dst_positive_code_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_positive_code_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_positive_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)))) * S ((((dst_positive_code_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_positive_code_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_positive_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scale_scalar_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)))) + ((((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput))) + (((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) * S ((dst_negative_code_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) + ((dst_negative_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otherentriesentryoutputpositive. ff_h_pvs_scalar_exists_unique_otherentriesentryoutputpositive + S (dst_positive_scalar_exists_unique_otherentriesentryoutput) = S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_positive_scale_scalar_exists_unique_otherentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_unique_otherentriesentryoutputpositive. dst_positive_code_scalar_exists_unique_otherentriesentryoutput = ff_q_pvs_scalar_exists_unique_otherentriesentryoutputpositive * S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_positive_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_positive_scalar_exists_unique_otherentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_exists_unique_otherentriesentryoutputnegative. ff_h_pvs_scalar_exists_unique_otherentriesentryoutputnegative + S (dst_negative_scalar_exists_unique_otherentriesentryoutput) = S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_negative_scale_scalar_exists_unique_otherentriesentryoutput)) /\ exists ff_q_pvs_scalar_exists_unique_otherentriesentryoutputnegative. dst_negative_code_scalar_exists_unique_otherentriesentryoutput = ff_q_pvs_scalar_exists_unique_otherentriesentryoutputnegative * S ((S (sto_index_scalar_exists_unique_otherentries)) * dst_negative_scale_scalar_exists_unique_otherentriesentryoutput) + (dst_negative_scalar_exists_unique_otherentriesentryoutput))) /\ (exists ge_balance_positive_scalar_exists_unique_otherentriesentryoutputvalue ge_balance_negative_scalar_exists_unique_otherentriesentryoutputvalue. (((((sto_output_scalar_exists_unique_otherentries) = 2 * (ge_balance_positive_scalar_exists_unique_otherentriesentryoutputvalue) /\ (ge_balance_negative_scalar_exists_unique_otherentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherentriesentryoutputvaluedecode. (((sto_output_scalar_exists_unique_otherentries) = 2 * ge_signed_half_scalar_exists_unique_otherentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_otherentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_otherentriesentryoutputvalue) = S ge_signed_half_scalar_exists_unique_otherentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_exists_unique_otherentriesentryoutput) + ge_balance_negative_scalar_exists_unique_otherentriesentryoutputvalue = (dst_negative_scalar_exists_unique_otherentriesentryoutput) + ge_balance_positive_scalar_exists_unique_otherentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_exists_unique_otherentriesentryoperation sto_an_scalar_exists_unique_otherentriesentryoperation sto_bp_scalar_exists_unique_otherentriesentryoperation sto_bn_scalar_exists_unique_otherentriesentryoperation sto_cp_scalar_exists_unique_otherentriesentryoperation sto_cn_scalar_exists_unique_otherentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_exists_unique_otherentriesentryoperation) /\ (sto_an_scalar_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_exists_unique_otherentriesentryoperationleft + 1 /\ (sto_ap_scalar_exists_unique_otherentriesentryoperation) = 0) /\ (sto_an_scalar_exists_unique_otherentriesentryoperation) = S ge_signed_half_scalar_exists_unique_otherentriesentryoperationleft))) /\ ((((((sto_input_scalar_exists_unique_otherentries) = 2 * (sto_bp_scalar_exists_unique_otherentriesentryoperation) /\ (sto_bn_scalar_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherentriesentryoperationright. (((sto_input_scalar_exists_unique_otherentries) = 2 * ge_signed_half_scalar_exists_unique_otherentriesentryoperationright + 1 /\ (sto_bp_scalar_exists_unique_otherentriesentryoperation) = 0) /\ (sto_bn_scalar_exists_unique_otherentriesentryoperation) = S ge_signed_half_scalar_exists_unique_otherentriesentryoperationright))) /\ ((((((sto_output_scalar_exists_unique_otherentries) = 2 * (sto_cp_scalar_exists_unique_otherentriesentryoperation) /\ (sto_cn_scalar_exists_unique_otherentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_exists_unique_otherentriesentryoperationoutput. (((sto_output_scalar_exists_unique_otherentries) = 2 * ge_signed_half_scalar_exists_unique_otherentriesentryoperationoutput + 1 /\ (sto_cp_scalar_exists_unique_otherentriesentryoperation) = 0) /\ (sto_cn_scalar_exists_unique_otherentriesentryoperation) = S ge_signed_half_scalar_exists_unique_otherentriesentryoperationoutput))) /\ ((sto_ap_scalar_exists_unique_otherentriesentryoperation * sto_bp_scalar_exists_unique_otherentriesentryoperation + sto_an_scalar_exists_unique_otherentriesentryoperation * sto_bn_scalar_exists_unique_otherentriesentryoperation) + sto_cn_scalar_exists_unique_otherentriesentryoperation = (sto_ap_scalar_exists_unique_otherentriesentryoperation * sto_bn_scalar_exists_unique_otherentriesentryoperation + sto_an_scalar_exists_unique_otherentriesentryoperation * sto_bp_scalar_exists_unique_otherentriesentryoperation) + sto_cp_scalar_exists_unique_otherentriesentryoperation))))))))))))))) -> (forall dst_index_scalar_exists_unique_equal dst_first_scalar_exists_unique_equal dst_second_scalar_exists_unique_equal. (exists pvs_gap_scalar_exists_unique_equalbound. pvs_gap_scalar_exists_unique_equalbound + S (dst_index_scalar_exists_unique_equal) = (l)) -> (exists dst_positive_code_scalar_exists_unique_equalfirst dst_positive_scale_scalar_exists_unique_equalfirst dst_negative_code_scalar_exists_unique_equalfirst dst_negative_scale_scalar_exists_unique_equalfirst dst_positive_scalar_exists_unique_equalfirst dst_negative_scalar_exists_unique_equalfirst. (((G) = (((((dst_positive_code_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst)) * S ((dst_positive_code_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst)) + ((dst_positive_scale_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst))) + (((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) * S ((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) + ((dst_negative_scale_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)))) * S ((((dst_positive_code_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst)) * S ((dst_positive_code_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst)) + ((dst_positive_scale_scalar_exists_unique_equalfirst) + (dst_positive_scale_scalar_exists_unique_equalfirst))) + (((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) * S ((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) + ((dst_negative_scale_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)))) + ((((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) * S ((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) + ((dst_negative_scale_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst))) + (((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) * S ((dst_negative_code_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)) + ((dst_negative_scale_scalar_exists_unique_equalfirst) + (dst_negative_scale_scalar_exists_unique_equalfirst)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_equalfirstpositive. ff_h_pvs_scalar_exists_unique_equalfirstpositive + S (dst_positive_scalar_exists_unique_equalfirst) = S ((S (dst_index_scalar_exists_unique_equal)) * dst_positive_scale_scalar_exists_unique_equalfirst)) /\ exists ff_q_pvs_scalar_exists_unique_equalfirstpositive. dst_positive_code_scalar_exists_unique_equalfirst = ff_q_pvs_scalar_exists_unique_equalfirstpositive * S ((S (dst_index_scalar_exists_unique_equal)) * dst_positive_scale_scalar_exists_unique_equalfirst) + (dst_positive_scalar_exists_unique_equalfirst))) /\ (((((exists ff_h_pvs_scalar_exists_unique_equalfirstnegative. ff_h_pvs_scalar_exists_unique_equalfirstnegative + S (dst_negative_scalar_exists_unique_equalfirst) = S ((S (dst_index_scalar_exists_unique_equal)) * dst_negative_scale_scalar_exists_unique_equalfirst)) /\ exists ff_q_pvs_scalar_exists_unique_equalfirstnegative. dst_negative_code_scalar_exists_unique_equalfirst = ff_q_pvs_scalar_exists_unique_equalfirstnegative * S ((S (dst_index_scalar_exists_unique_equal)) * dst_negative_scale_scalar_exists_unique_equalfirst) + (dst_negative_scalar_exists_unique_equalfirst))) /\ (exists ge_balance_positive_scalar_exists_unique_equalfirstvalue ge_balance_negative_scalar_exists_unique_equalfirstvalue. (((((dst_first_scalar_exists_unique_equal) = 2 * (ge_balance_positive_scalar_exists_unique_equalfirstvalue) /\ (ge_balance_negative_scalar_exists_unique_equalfirstvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_equalfirstvaluedecode. (((dst_first_scalar_exists_unique_equal) = 2 * ge_signed_half_scalar_exists_unique_equalfirstvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_equalfirstvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_equalfirstvalue) = S ge_signed_half_scalar_exists_unique_equalfirstvaluedecode))) /\ ((dst_positive_scalar_exists_unique_equalfirst) + ge_balance_negative_scalar_exists_unique_equalfirstvalue = (dst_negative_scalar_exists_unique_equalfirst) + ge_balance_positive_scalar_exists_unique_equalfirstvalue))))))))) -> (exists dst_positive_code_scalar_exists_unique_equalsecond dst_positive_scale_scalar_exists_unique_equalsecond dst_negative_code_scalar_exists_unique_equalsecond dst_negative_scale_scalar_exists_unique_equalsecond dst_positive_scalar_exists_unique_equalsecond dst_negative_scalar_exists_unique_equalsecond. (((K) = (((((dst_positive_code_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond)) * S ((dst_positive_code_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond)) + ((dst_positive_scale_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond))) + (((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) * S ((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) + ((dst_negative_scale_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)))) * S ((((dst_positive_code_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond)) * S ((dst_positive_code_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond)) + ((dst_positive_scale_scalar_exists_unique_equalsecond) + (dst_positive_scale_scalar_exists_unique_equalsecond))) + (((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) * S ((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) + ((dst_negative_scale_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)))) + ((((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) * S ((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) + ((dst_negative_scale_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond))) + (((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) * S ((dst_negative_code_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)) + ((dst_negative_scale_scalar_exists_unique_equalsecond) + (dst_negative_scale_scalar_exists_unique_equalsecond)))))) /\ (((((exists ff_h_pvs_scalar_exists_unique_equalsecondpositive. ff_h_pvs_scalar_exists_unique_equalsecondpositive + S (dst_positive_scalar_exists_unique_equalsecond) = S ((S (dst_index_scalar_exists_unique_equal)) * dst_positive_scale_scalar_exists_unique_equalsecond)) /\ exists ff_q_pvs_scalar_exists_unique_equalsecondpositive. dst_positive_code_scalar_exists_unique_equalsecond = ff_q_pvs_scalar_exists_unique_equalsecondpositive * S ((S (dst_index_scalar_exists_unique_equal)) * dst_positive_scale_scalar_exists_unique_equalsecond) + (dst_positive_scalar_exists_unique_equalsecond))) /\ (((((exists ff_h_pvs_scalar_exists_unique_equalsecondnegative. ff_h_pvs_scalar_exists_unique_equalsecondnegative + S (dst_negative_scalar_exists_unique_equalsecond) = S ((S (dst_index_scalar_exists_unique_equal)) * dst_negative_scale_scalar_exists_unique_equalsecond)) /\ exists ff_q_pvs_scalar_exists_unique_equalsecondnegative. dst_negative_code_scalar_exists_unique_equalsecond = ff_q_pvs_scalar_exists_unique_equalsecondnegative * S ((S (dst_index_scalar_exists_unique_equal)) * dst_negative_scale_scalar_exists_unique_equalsecond) + (dst_negative_scalar_exists_unique_equalsecond))) /\ (exists ge_balance_positive_scalar_exists_unique_equalsecondvalue ge_balance_negative_scalar_exists_unique_equalsecondvalue. (((((dst_second_scalar_exists_unique_equal) = 2 * (ge_balance_positive_scalar_exists_unique_equalsecondvalue) /\ (ge_balance_negative_scalar_exists_unique_equalsecondvalue) = 0) \/ exists ge_signed_half_scalar_exists_unique_equalsecondvaluedecode. (((dst_second_scalar_exists_unique_equal) = 2 * ge_signed_half_scalar_exists_unique_equalsecondvaluedecode + 1 /\ (ge_balance_positive_scalar_exists_unique_equalsecondvalue) = 0) /\ (ge_balance_negative_scalar_exists_unique_equalsecondvalue) = S ge_signed_half_scalar_exists_unique_equalsecondvaluedecode))) /\ ((dst_positive_scalar_exists_unique_equalsecond) + ge_balance_negative_scalar_exists_unique_equalsecondvalue = (dst_negative_scalar_exists_unique_equalsecond) + ge_balance_positive_scalar_exists_unique_equalsecondvalue))))))))) -> dst_first_scalar_exists_unique_equal = dst_second_scalar_exists_unique_equal)))