signed_table_scalar_extensional_unique

Exact expanded first-order arithmetic statement

forall a F G H l. (((exists dst_positive_code_scalar_unique_firstinput_table dst_positive_scale_scalar_unique_firstinput_table dst_negative_code_scalar_unique_firstinput_table dst_negative_scale_scalar_unique_firstinput_table. (((F) = (((((dst_positive_code_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table)) * S ((dst_positive_code_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table)) + ((dst_positive_scale_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table))) + (((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) * S ((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) + ((dst_negative_scale_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)))) * S ((((dst_positive_code_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table)) * S ((dst_positive_code_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table)) + ((dst_positive_scale_scalar_unique_firstinput_table) + (dst_positive_scale_scalar_unique_firstinput_table))) + (((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) * S ((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) + ((dst_negative_scale_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)))) + ((((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) * S ((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) + ((dst_negative_scale_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table))) + (((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) * S ((dst_negative_code_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)) + ((dst_negative_scale_scalar_unique_firstinput_table) + (dst_negative_scale_scalar_unique_firstinput_table)))))) /\ (forall dst_index_scalar_unique_firstinput_table. (exists pvs_le_gap_scalar_unique_firstinput_tabledomain. pvs_le_gap_scalar_unique_firstinput_tabledomain + (dst_index_scalar_unique_firstinput_table) = (l)) -> exists dst_positive_scalar_unique_firstinput_table dst_negative_scalar_unique_firstinput_table dst_value_scalar_unique_firstinput_table. ((((exists ff_h_pvs_scalar_unique_firstinput_tableentrypositive. ff_h_pvs_scalar_unique_firstinput_tableentrypositive + S (dst_positive_scalar_unique_firstinput_table) = S ((S (dst_index_scalar_unique_firstinput_table)) * dst_positive_scale_scalar_unique_firstinput_table)) /\ exists ff_q_pvs_scalar_unique_firstinput_tableentrypositive. dst_positive_code_scalar_unique_firstinput_table = ff_q_pvs_scalar_unique_firstinput_tableentrypositive * S ((S (dst_index_scalar_unique_firstinput_table)) * dst_positive_scale_scalar_unique_firstinput_table) + (dst_positive_scalar_unique_firstinput_table))) /\ (((((exists ff_h_pvs_scalar_unique_firstinput_tableentrynegative. ff_h_pvs_scalar_unique_firstinput_tableentrynegative + S (dst_negative_scalar_unique_firstinput_table) = S ((S (dst_index_scalar_unique_firstinput_table)) * dst_negative_scale_scalar_unique_firstinput_table)) /\ exists ff_q_pvs_scalar_unique_firstinput_tableentrynegative. dst_negative_code_scalar_unique_firstinput_table = ff_q_pvs_scalar_unique_firstinput_tableentrynegative * S ((S (dst_index_scalar_unique_firstinput_table)) * dst_negative_scale_scalar_unique_firstinput_table) + (dst_negative_scalar_unique_firstinput_table))) /\ (exists ge_balance_positive_scalar_unique_firstinput_tableentryvalue ge_balance_negative_scalar_unique_firstinput_tableentryvalue. (((((dst_value_scalar_unique_firstinput_table) = 2 * (ge_balance_positive_scalar_unique_firstinput_tableentryvalue) /\ (ge_balance_negative_scalar_unique_firstinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_unique_firstinput_tableentryvaluedecode. (((dst_value_scalar_unique_firstinput_table) = 2 * ge_signed_half_scalar_unique_firstinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_firstinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_unique_firstinput_tableentryvalue) = S ge_signed_half_scalar_unique_firstinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_unique_firstinput_table) + ge_balance_negative_scalar_unique_firstinput_tableentryvalue = (dst_negative_scalar_unique_firstinput_table) + ge_balance_positive_scalar_unique_firstinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_unique_firstoutput_table dst_positive_scale_scalar_unique_firstoutput_table dst_negative_code_scalar_unique_firstoutput_table dst_negative_scale_scalar_unique_firstoutput_table. (((G) = (((((dst_positive_code_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table)) * S ((dst_positive_code_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table)) + ((dst_positive_scale_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table))) + (((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) * S ((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) + ((dst_negative_scale_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)))) * S ((((dst_positive_code_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table)) * S ((dst_positive_code_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table)) + ((dst_positive_scale_scalar_unique_firstoutput_table) + (dst_positive_scale_scalar_unique_firstoutput_table))) + (((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) * S ((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) + ((dst_negative_scale_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)))) + ((((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) * S ((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) + ((dst_negative_scale_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table))) + (((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) * S ((dst_negative_code_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)) + ((dst_negative_scale_scalar_unique_firstoutput_table) + (dst_negative_scale_scalar_unique_firstoutput_table)))))) /\ (forall dst_index_scalar_unique_firstoutput_table. (exists pvs_le_gap_scalar_unique_firstoutput_tabledomain. pvs_le_gap_scalar_unique_firstoutput_tabledomain + (dst_index_scalar_unique_firstoutput_table) = (l)) -> exists dst_positive_scalar_unique_firstoutput_table dst_negative_scalar_unique_firstoutput_table dst_value_scalar_unique_firstoutput_table. ((((exists ff_h_pvs_scalar_unique_firstoutput_tableentrypositive. ff_h_pvs_scalar_unique_firstoutput_tableentrypositive + S (dst_positive_scalar_unique_firstoutput_table) = S ((S (dst_index_scalar_unique_firstoutput_table)) * dst_positive_scale_scalar_unique_firstoutput_table)) /\ exists ff_q_pvs_scalar_unique_firstoutput_tableentrypositive. dst_positive_code_scalar_unique_firstoutput_table = ff_q_pvs_scalar_unique_firstoutput_tableentrypositive * S ((S (dst_index_scalar_unique_firstoutput_table)) * dst_positive_scale_scalar_unique_firstoutput_table) + (dst_positive_scalar_unique_firstoutput_table))) /\ (((((exists ff_h_pvs_scalar_unique_firstoutput_tableentrynegative. ff_h_pvs_scalar_unique_firstoutput_tableentrynegative + S (dst_negative_scalar_unique_firstoutput_table) = S ((S (dst_index_scalar_unique_firstoutput_table)) * dst_negative_scale_scalar_unique_firstoutput_table)) /\ exists ff_q_pvs_scalar_unique_firstoutput_tableentrynegative. dst_negative_code_scalar_unique_firstoutput_table = ff_q_pvs_scalar_unique_firstoutput_tableentrynegative * S ((S (dst_index_scalar_unique_firstoutput_table)) * dst_negative_scale_scalar_unique_firstoutput_table) + (dst_negative_scalar_unique_firstoutput_table))) /\ (exists ge_balance_positive_scalar_unique_firstoutput_tableentryvalue ge_balance_negative_scalar_unique_firstoutput_tableentryvalue. (((((dst_value_scalar_unique_firstoutput_table) = 2 * (ge_balance_positive_scalar_unique_firstoutput_tableentryvalue) /\ (ge_balance_negative_scalar_unique_firstoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_unique_firstoutput_tableentryvaluedecode. (((dst_value_scalar_unique_firstoutput_table) = 2 * ge_signed_half_scalar_unique_firstoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_firstoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_unique_firstoutput_tableentryvalue) = S ge_signed_half_scalar_unique_firstoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_unique_firstoutput_table) + ge_balance_negative_scalar_unique_firstoutput_tableentryvalue = (dst_negative_scalar_unique_firstoutput_table) + ge_balance_positive_scalar_unique_firstoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_unique_firstentries. (exists pvs_gap_scalar_unique_firstentriesbound. pvs_gap_scalar_unique_firstentriesbound + S (sto_index_scalar_unique_firstentries) = (l)) -> exists sto_input_scalar_unique_firstentries sto_output_scalar_unique_firstentries. ((exists dst_positive_code_scalar_unique_firstentriesentryinput dst_positive_scale_scalar_unique_firstentriesentryinput dst_negative_code_scalar_unique_firstentriesentryinput dst_negative_scale_scalar_unique_firstentriesentryinput dst_positive_scalar_unique_firstentriesentryinput dst_negative_scalar_unique_firstentriesentryinput. (((F) = (((((dst_positive_code_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput)) * S ((dst_positive_code_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput)) + ((dst_positive_scale_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput))) + (((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) * S ((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) + ((dst_negative_scale_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)))) * S ((((dst_positive_code_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput)) * S ((dst_positive_code_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput)) + ((dst_positive_scale_scalar_unique_firstentriesentryinput) + (dst_positive_scale_scalar_unique_firstentriesentryinput))) + (((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) * S ((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) + ((dst_negative_scale_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)))) + ((((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) * S ((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) + ((dst_negative_scale_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput))) + (((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) * S ((dst_negative_code_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)) + ((dst_negative_scale_scalar_unique_firstentriesentryinput) + (dst_negative_scale_scalar_unique_firstentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_unique_firstentriesentryinputpositive. ff_h_pvs_scalar_unique_firstentriesentryinputpositive + S (dst_positive_scalar_unique_firstentriesentryinput) = S ((S (sto_index_scalar_unique_firstentries)) * dst_positive_scale_scalar_unique_firstentriesentryinput)) /\ exists ff_q_pvs_scalar_unique_firstentriesentryinputpositive. dst_positive_code_scalar_unique_firstentriesentryinput = ff_q_pvs_scalar_unique_firstentriesentryinputpositive * S ((S (sto_index_scalar_unique_firstentries)) * dst_positive_scale_scalar_unique_firstentriesentryinput) + (dst_positive_scalar_unique_firstentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_unique_firstentriesentryinputnegative. ff_h_pvs_scalar_unique_firstentriesentryinputnegative + S (dst_negative_scalar_unique_firstentriesentryinput) = S ((S (sto_index_scalar_unique_firstentries)) * dst_negative_scale_scalar_unique_firstentriesentryinput)) /\ exists ff_q_pvs_scalar_unique_firstentriesentryinputnegative. dst_negative_code_scalar_unique_firstentriesentryinput = ff_q_pvs_scalar_unique_firstentriesentryinputnegative * S ((S (sto_index_scalar_unique_firstentries)) * dst_negative_scale_scalar_unique_firstentriesentryinput) + (dst_negative_scalar_unique_firstentriesentryinput))) /\ (exists ge_balance_positive_scalar_unique_firstentriesentryinputvalue ge_balance_negative_scalar_unique_firstentriesentryinputvalue. (((((sto_input_scalar_unique_firstentries) = 2 * (ge_balance_positive_scalar_unique_firstentriesentryinputvalue) /\ (ge_balance_negative_scalar_unique_firstentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_unique_firstentriesentryinputvaluedecode. (((sto_input_scalar_unique_firstentries) = 2 * ge_signed_half_scalar_unique_firstentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_firstentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_unique_firstentriesentryinputvalue) = S ge_signed_half_scalar_unique_firstentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_unique_firstentriesentryinput) + ge_balance_negative_scalar_unique_firstentriesentryinputvalue = (dst_negative_scalar_unique_firstentriesentryinput) + ge_balance_positive_scalar_unique_firstentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_unique_firstentriesentryoutput dst_positive_scale_scalar_unique_firstentriesentryoutput dst_negative_code_scalar_unique_firstentriesentryoutput dst_negative_scale_scalar_unique_firstentriesentryoutput dst_positive_scalar_unique_firstentriesentryoutput dst_negative_scalar_unique_firstentriesentryoutput. (((G) = (((((dst_positive_code_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_positive_code_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput)) + ((dst_positive_scale_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput))) + (((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) + ((dst_negative_scale_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)))) * S ((((dst_positive_code_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_positive_code_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput)) + ((dst_positive_scale_scalar_unique_firstentriesentryoutput) + (dst_positive_scale_scalar_unique_firstentriesentryoutput))) + (((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) + ((dst_negative_scale_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)))) + ((((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) + ((dst_negative_scale_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput))) + (((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) * S ((dst_negative_code_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)) + ((dst_negative_scale_scalar_unique_firstentriesentryoutput) + (dst_negative_scale_scalar_unique_firstentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_unique_firstentriesentryoutputpositive. ff_h_pvs_scalar_unique_firstentriesentryoutputpositive + S (dst_positive_scalar_unique_firstentriesentryoutput) = S ((S (sto_index_scalar_unique_firstentries)) * dst_positive_scale_scalar_unique_firstentriesentryoutput)) /\ exists ff_q_pvs_scalar_unique_firstentriesentryoutputpositive. dst_positive_code_scalar_unique_firstentriesentryoutput = ff_q_pvs_scalar_unique_firstentriesentryoutputpositive * S ((S (sto_index_scalar_unique_firstentries)) * dst_positive_scale_scalar_unique_firstentriesentryoutput) + (dst_positive_scalar_unique_firstentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_unique_firstentriesentryoutputnegative. ff_h_pvs_scalar_unique_firstentriesentryoutputnegative + S (dst_negative_scalar_unique_firstentriesentryoutput) = S ((S (sto_index_scalar_unique_firstentries)) * dst_negative_scale_scalar_unique_firstentriesentryoutput)) /\ exists ff_q_pvs_scalar_unique_firstentriesentryoutputnegative. dst_negative_code_scalar_unique_firstentriesentryoutput = ff_q_pvs_scalar_unique_firstentriesentryoutputnegative * S ((S (sto_index_scalar_unique_firstentries)) * dst_negative_scale_scalar_unique_firstentriesentryoutput) + (dst_negative_scalar_unique_firstentriesentryoutput))) /\ (exists ge_balance_positive_scalar_unique_firstentriesentryoutputvalue ge_balance_negative_scalar_unique_firstentriesentryoutputvalue. (((((sto_output_scalar_unique_firstentries) = 2 * (ge_balance_positive_scalar_unique_firstentriesentryoutputvalue) /\ (ge_balance_negative_scalar_unique_firstentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_unique_firstentriesentryoutputvaluedecode. (((sto_output_scalar_unique_firstentries) = 2 * ge_signed_half_scalar_unique_firstentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_firstentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_unique_firstentriesentryoutputvalue) = S ge_signed_half_scalar_unique_firstentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_unique_firstentriesentryoutput) + ge_balance_negative_scalar_unique_firstentriesentryoutputvalue = (dst_negative_scalar_unique_firstentriesentryoutput) + ge_balance_positive_scalar_unique_firstentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_unique_firstentriesentryoperation sto_an_scalar_unique_firstentriesentryoperation sto_bp_scalar_unique_firstentriesentryoperation sto_bn_scalar_unique_firstentriesentryoperation sto_cp_scalar_unique_firstentriesentryoperation sto_cn_scalar_unique_firstentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_unique_firstentriesentryoperation) /\ (sto_an_scalar_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_firstentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_unique_firstentriesentryoperationleft + 1 /\ (sto_ap_scalar_unique_firstentriesentryoperation) = 0) /\ (sto_an_scalar_unique_firstentriesentryoperation) = S ge_signed_half_scalar_unique_firstentriesentryoperationleft))) /\ ((((((sto_input_scalar_unique_firstentries) = 2 * (sto_bp_scalar_unique_firstentriesentryoperation) /\ (sto_bn_scalar_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_firstentriesentryoperationright. (((sto_input_scalar_unique_firstentries) = 2 * ge_signed_half_scalar_unique_firstentriesentryoperationright + 1 /\ (sto_bp_scalar_unique_firstentriesentryoperation) = 0) /\ (sto_bn_scalar_unique_firstentriesentryoperation) = S ge_signed_half_scalar_unique_firstentriesentryoperationright))) /\ ((((((sto_output_scalar_unique_firstentries) = 2 * (sto_cp_scalar_unique_firstentriesentryoperation) /\ (sto_cn_scalar_unique_firstentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_firstentriesentryoperationoutput. (((sto_output_scalar_unique_firstentries) = 2 * ge_signed_half_scalar_unique_firstentriesentryoperationoutput + 1 /\ (sto_cp_scalar_unique_firstentriesentryoperation) = 0) /\ (sto_cn_scalar_unique_firstentriesentryoperation) = S ge_signed_half_scalar_unique_firstentriesentryoperationoutput))) /\ ((sto_ap_scalar_unique_firstentriesentryoperation * sto_bp_scalar_unique_firstentriesentryoperation + sto_an_scalar_unique_firstentriesentryoperation * sto_bn_scalar_unique_firstentriesentryoperation) + sto_cn_scalar_unique_firstentriesentryoperation = (sto_ap_scalar_unique_firstentriesentryoperation * sto_bn_scalar_unique_firstentriesentryoperation + sto_an_scalar_unique_firstentriesentryoperation * sto_bp_scalar_unique_firstentriesentryoperation) + sto_cp_scalar_unique_firstentriesentryoperation))))))))))))))) -> (((exists dst_positive_code_scalar_unique_secondinput_table dst_positive_scale_scalar_unique_secondinput_table dst_negative_code_scalar_unique_secondinput_table dst_negative_scale_scalar_unique_secondinput_table. (((F) = (((((dst_positive_code_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table)) * S ((dst_positive_code_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table)) + ((dst_positive_scale_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table))) + (((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) * S ((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) + ((dst_negative_scale_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)))) * S ((((dst_positive_code_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table)) * S ((dst_positive_code_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table)) + ((dst_positive_scale_scalar_unique_secondinput_table) + (dst_positive_scale_scalar_unique_secondinput_table))) + (((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) * S ((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) + ((dst_negative_scale_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)))) + ((((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) * S ((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) + ((dst_negative_scale_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table))) + (((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) * S ((dst_negative_code_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)) + ((dst_negative_scale_scalar_unique_secondinput_table) + (dst_negative_scale_scalar_unique_secondinput_table)))))) /\ (forall dst_index_scalar_unique_secondinput_table. (exists pvs_le_gap_scalar_unique_secondinput_tabledomain. pvs_le_gap_scalar_unique_secondinput_tabledomain + (dst_index_scalar_unique_secondinput_table) = (l)) -> exists dst_positive_scalar_unique_secondinput_table dst_negative_scalar_unique_secondinput_table dst_value_scalar_unique_secondinput_table. ((((exists ff_h_pvs_scalar_unique_secondinput_tableentrypositive. ff_h_pvs_scalar_unique_secondinput_tableentrypositive + S (dst_positive_scalar_unique_secondinput_table) = S ((S (dst_index_scalar_unique_secondinput_table)) * dst_positive_scale_scalar_unique_secondinput_table)) /\ exists ff_q_pvs_scalar_unique_secondinput_tableentrypositive. dst_positive_code_scalar_unique_secondinput_table = ff_q_pvs_scalar_unique_secondinput_tableentrypositive * S ((S (dst_index_scalar_unique_secondinput_table)) * dst_positive_scale_scalar_unique_secondinput_table) + (dst_positive_scalar_unique_secondinput_table))) /\ (((((exists ff_h_pvs_scalar_unique_secondinput_tableentrynegative. ff_h_pvs_scalar_unique_secondinput_tableentrynegative + S (dst_negative_scalar_unique_secondinput_table) = S ((S (dst_index_scalar_unique_secondinput_table)) * dst_negative_scale_scalar_unique_secondinput_table)) /\ exists ff_q_pvs_scalar_unique_secondinput_tableentrynegative. dst_negative_code_scalar_unique_secondinput_table = ff_q_pvs_scalar_unique_secondinput_tableentrynegative * S ((S (dst_index_scalar_unique_secondinput_table)) * dst_negative_scale_scalar_unique_secondinput_table) + (dst_negative_scalar_unique_secondinput_table))) /\ (exists ge_balance_positive_scalar_unique_secondinput_tableentryvalue ge_balance_negative_scalar_unique_secondinput_tableentryvalue. (((((dst_value_scalar_unique_secondinput_table) = 2 * (ge_balance_positive_scalar_unique_secondinput_tableentryvalue) /\ (ge_balance_negative_scalar_unique_secondinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_unique_secondinput_tableentryvaluedecode. (((dst_value_scalar_unique_secondinput_table) = 2 * ge_signed_half_scalar_unique_secondinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_secondinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_unique_secondinput_tableentryvalue) = S ge_signed_half_scalar_unique_secondinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_unique_secondinput_table) + ge_balance_negative_scalar_unique_secondinput_tableentryvalue = (dst_negative_scalar_unique_secondinput_table) + ge_balance_positive_scalar_unique_secondinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_unique_secondoutput_table dst_positive_scale_scalar_unique_secondoutput_table dst_negative_code_scalar_unique_secondoutput_table dst_negative_scale_scalar_unique_secondoutput_table. (((H) = (((((dst_positive_code_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table)) * S ((dst_positive_code_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table)) + ((dst_positive_scale_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table))) + (((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) * S ((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) + ((dst_negative_scale_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)))) * S ((((dst_positive_code_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table)) * S ((dst_positive_code_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table)) + ((dst_positive_scale_scalar_unique_secondoutput_table) + (dst_positive_scale_scalar_unique_secondoutput_table))) + (((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) * S ((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) + ((dst_negative_scale_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)))) + ((((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) * S ((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) + ((dst_negative_scale_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table))) + (((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) * S ((dst_negative_code_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)) + ((dst_negative_scale_scalar_unique_secondoutput_table) + (dst_negative_scale_scalar_unique_secondoutput_table)))))) /\ (forall dst_index_scalar_unique_secondoutput_table. (exists pvs_le_gap_scalar_unique_secondoutput_tabledomain. pvs_le_gap_scalar_unique_secondoutput_tabledomain + (dst_index_scalar_unique_secondoutput_table) = (l)) -> exists dst_positive_scalar_unique_secondoutput_table dst_negative_scalar_unique_secondoutput_table dst_value_scalar_unique_secondoutput_table. ((((exists ff_h_pvs_scalar_unique_secondoutput_tableentrypositive. ff_h_pvs_scalar_unique_secondoutput_tableentrypositive + S (dst_positive_scalar_unique_secondoutput_table) = S ((S (dst_index_scalar_unique_secondoutput_table)) * dst_positive_scale_scalar_unique_secondoutput_table)) /\ exists ff_q_pvs_scalar_unique_secondoutput_tableentrypositive. dst_positive_code_scalar_unique_secondoutput_table = ff_q_pvs_scalar_unique_secondoutput_tableentrypositive * S ((S (dst_index_scalar_unique_secondoutput_table)) * dst_positive_scale_scalar_unique_secondoutput_table) + (dst_positive_scalar_unique_secondoutput_table))) /\ (((((exists ff_h_pvs_scalar_unique_secondoutput_tableentrynegative. ff_h_pvs_scalar_unique_secondoutput_tableentrynegative + S (dst_negative_scalar_unique_secondoutput_table) = S ((S (dst_index_scalar_unique_secondoutput_table)) * dst_negative_scale_scalar_unique_secondoutput_table)) /\ exists ff_q_pvs_scalar_unique_secondoutput_tableentrynegative. dst_negative_code_scalar_unique_secondoutput_table = ff_q_pvs_scalar_unique_secondoutput_tableentrynegative * S ((S (dst_index_scalar_unique_secondoutput_table)) * dst_negative_scale_scalar_unique_secondoutput_table) + (dst_negative_scalar_unique_secondoutput_table))) /\ (exists ge_balance_positive_scalar_unique_secondoutput_tableentryvalue ge_balance_negative_scalar_unique_secondoutput_tableentryvalue. (((((dst_value_scalar_unique_secondoutput_table) = 2 * (ge_balance_positive_scalar_unique_secondoutput_tableentryvalue) /\ (ge_balance_negative_scalar_unique_secondoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_unique_secondoutput_tableentryvaluedecode. (((dst_value_scalar_unique_secondoutput_table) = 2 * ge_signed_half_scalar_unique_secondoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_secondoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_unique_secondoutput_tableentryvalue) = S ge_signed_half_scalar_unique_secondoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_unique_secondoutput_table) + ge_balance_negative_scalar_unique_secondoutput_tableentryvalue = (dst_negative_scalar_unique_secondoutput_table) + ge_balance_positive_scalar_unique_secondoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_unique_secondentries. (exists pvs_gap_scalar_unique_secondentriesbound. pvs_gap_scalar_unique_secondentriesbound + S (sto_index_scalar_unique_secondentries) = (l)) -> exists sto_input_scalar_unique_secondentries sto_output_scalar_unique_secondentries. ((exists dst_positive_code_scalar_unique_secondentriesentryinput dst_positive_scale_scalar_unique_secondentriesentryinput dst_negative_code_scalar_unique_secondentriesentryinput dst_negative_scale_scalar_unique_secondentriesentryinput dst_positive_scalar_unique_secondentriesentryinput dst_negative_scalar_unique_secondentriesentryinput. (((F) = (((((dst_positive_code_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput)) * S ((dst_positive_code_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput)) + ((dst_positive_scale_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput))) + (((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) * S ((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) + ((dst_negative_scale_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)))) * S ((((dst_positive_code_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput)) * S ((dst_positive_code_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput)) + ((dst_positive_scale_scalar_unique_secondentriesentryinput) + (dst_positive_scale_scalar_unique_secondentriesentryinput))) + (((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) * S ((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) + ((dst_negative_scale_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)))) + ((((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) * S ((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) + ((dst_negative_scale_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput))) + (((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) * S ((dst_negative_code_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)) + ((dst_negative_scale_scalar_unique_secondentriesentryinput) + (dst_negative_scale_scalar_unique_secondentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_unique_secondentriesentryinputpositive. ff_h_pvs_scalar_unique_secondentriesentryinputpositive + S (dst_positive_scalar_unique_secondentriesentryinput) = S ((S (sto_index_scalar_unique_secondentries)) * dst_positive_scale_scalar_unique_secondentriesentryinput)) /\ exists ff_q_pvs_scalar_unique_secondentriesentryinputpositive. dst_positive_code_scalar_unique_secondentriesentryinput = ff_q_pvs_scalar_unique_secondentriesentryinputpositive * S ((S (sto_index_scalar_unique_secondentries)) * dst_positive_scale_scalar_unique_secondentriesentryinput) + (dst_positive_scalar_unique_secondentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_unique_secondentriesentryinputnegative. ff_h_pvs_scalar_unique_secondentriesentryinputnegative + S (dst_negative_scalar_unique_secondentriesentryinput) = S ((S (sto_index_scalar_unique_secondentries)) * dst_negative_scale_scalar_unique_secondentriesentryinput)) /\ exists ff_q_pvs_scalar_unique_secondentriesentryinputnegative. dst_negative_code_scalar_unique_secondentriesentryinput = ff_q_pvs_scalar_unique_secondentriesentryinputnegative * S ((S (sto_index_scalar_unique_secondentries)) * dst_negative_scale_scalar_unique_secondentriesentryinput) + (dst_negative_scalar_unique_secondentriesentryinput))) /\ (exists ge_balance_positive_scalar_unique_secondentriesentryinputvalue ge_balance_negative_scalar_unique_secondentriesentryinputvalue. (((((sto_input_scalar_unique_secondentries) = 2 * (ge_balance_positive_scalar_unique_secondentriesentryinputvalue) /\ (ge_balance_negative_scalar_unique_secondentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_unique_secondentriesentryinputvaluedecode. (((sto_input_scalar_unique_secondentries) = 2 * ge_signed_half_scalar_unique_secondentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_secondentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_unique_secondentriesentryinputvalue) = S ge_signed_half_scalar_unique_secondentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_unique_secondentriesentryinput) + ge_balance_negative_scalar_unique_secondentriesentryinputvalue = (dst_negative_scalar_unique_secondentriesentryinput) + ge_balance_positive_scalar_unique_secondentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_unique_secondentriesentryoutput dst_positive_scale_scalar_unique_secondentriesentryoutput dst_negative_code_scalar_unique_secondentriesentryoutput dst_negative_scale_scalar_unique_secondentriesentryoutput dst_positive_scalar_unique_secondentriesentryoutput dst_negative_scalar_unique_secondentriesentryoutput. (((H) = (((((dst_positive_code_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_positive_code_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput)) + ((dst_positive_scale_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput))) + (((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) + ((dst_negative_scale_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)))) * S ((((dst_positive_code_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_positive_code_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput)) + ((dst_positive_scale_scalar_unique_secondentriesentryoutput) + (dst_positive_scale_scalar_unique_secondentriesentryoutput))) + (((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) + ((dst_negative_scale_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)))) + ((((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) + ((dst_negative_scale_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput))) + (((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) * S ((dst_negative_code_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)) + ((dst_negative_scale_scalar_unique_secondentriesentryoutput) + (dst_negative_scale_scalar_unique_secondentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_unique_secondentriesentryoutputpositive. ff_h_pvs_scalar_unique_secondentriesentryoutputpositive + S (dst_positive_scalar_unique_secondentriesentryoutput) = S ((S (sto_index_scalar_unique_secondentries)) * dst_positive_scale_scalar_unique_secondentriesentryoutput)) /\ exists ff_q_pvs_scalar_unique_secondentriesentryoutputpositive. dst_positive_code_scalar_unique_secondentriesentryoutput = ff_q_pvs_scalar_unique_secondentriesentryoutputpositive * S ((S (sto_index_scalar_unique_secondentries)) * dst_positive_scale_scalar_unique_secondentriesentryoutput) + (dst_positive_scalar_unique_secondentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_unique_secondentriesentryoutputnegative. ff_h_pvs_scalar_unique_secondentriesentryoutputnegative + S (dst_negative_scalar_unique_secondentriesentryoutput) = S ((S (sto_index_scalar_unique_secondentries)) * dst_negative_scale_scalar_unique_secondentriesentryoutput)) /\ exists ff_q_pvs_scalar_unique_secondentriesentryoutputnegative. dst_negative_code_scalar_unique_secondentriesentryoutput = ff_q_pvs_scalar_unique_secondentriesentryoutputnegative * S ((S (sto_index_scalar_unique_secondentries)) * dst_negative_scale_scalar_unique_secondentriesentryoutput) + (dst_negative_scalar_unique_secondentriesentryoutput))) /\ (exists ge_balance_positive_scalar_unique_secondentriesentryoutputvalue ge_balance_negative_scalar_unique_secondentriesentryoutputvalue. (((((sto_output_scalar_unique_secondentries) = 2 * (ge_balance_positive_scalar_unique_secondentriesentryoutputvalue) /\ (ge_balance_negative_scalar_unique_secondentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_unique_secondentriesentryoutputvaluedecode. (((sto_output_scalar_unique_secondentries) = 2 * ge_signed_half_scalar_unique_secondentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_secondentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_unique_secondentriesentryoutputvalue) = S ge_signed_half_scalar_unique_secondentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_unique_secondentriesentryoutput) + ge_balance_negative_scalar_unique_secondentriesentryoutputvalue = (dst_negative_scalar_unique_secondentriesentryoutput) + ge_balance_positive_scalar_unique_secondentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_unique_secondentriesentryoperation sto_an_scalar_unique_secondentriesentryoperation sto_bp_scalar_unique_secondentriesentryoperation sto_bn_scalar_unique_secondentriesentryoperation sto_cp_scalar_unique_secondentriesentryoperation sto_cn_scalar_unique_secondentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_unique_secondentriesentryoperation) /\ (sto_an_scalar_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_secondentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_unique_secondentriesentryoperationleft + 1 /\ (sto_ap_scalar_unique_secondentriesentryoperation) = 0) /\ (sto_an_scalar_unique_secondentriesentryoperation) = S ge_signed_half_scalar_unique_secondentriesentryoperationleft))) /\ ((((((sto_input_scalar_unique_secondentries) = 2 * (sto_bp_scalar_unique_secondentriesentryoperation) /\ (sto_bn_scalar_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_secondentriesentryoperationright. (((sto_input_scalar_unique_secondentries) = 2 * ge_signed_half_scalar_unique_secondentriesentryoperationright + 1 /\ (sto_bp_scalar_unique_secondentriesentryoperation) = 0) /\ (sto_bn_scalar_unique_secondentriesentryoperation) = S ge_signed_half_scalar_unique_secondentriesentryoperationright))) /\ ((((((sto_output_scalar_unique_secondentries) = 2 * (sto_cp_scalar_unique_secondentriesentryoperation) /\ (sto_cn_scalar_unique_secondentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_unique_secondentriesentryoperationoutput. (((sto_output_scalar_unique_secondentries) = 2 * ge_signed_half_scalar_unique_secondentriesentryoperationoutput + 1 /\ (sto_cp_scalar_unique_secondentriesentryoperation) = 0) /\ (sto_cn_scalar_unique_secondentriesentryoperation) = S ge_signed_half_scalar_unique_secondentriesentryoperationoutput))) /\ ((sto_ap_scalar_unique_secondentriesentryoperation * sto_bp_scalar_unique_secondentriesentryoperation + sto_an_scalar_unique_secondentriesentryoperation * sto_bn_scalar_unique_secondentriesentryoperation) + sto_cn_scalar_unique_secondentriesentryoperation = (sto_ap_scalar_unique_secondentriesentryoperation * sto_bn_scalar_unique_secondentriesentryoperation + sto_an_scalar_unique_secondentriesentryoperation * sto_bp_scalar_unique_secondentriesentryoperation) + sto_cp_scalar_unique_secondentriesentryoperation))))))))))))))) -> (forall dst_index_scalar_unique_result dst_first_scalar_unique_result dst_second_scalar_unique_result. (exists pvs_gap_scalar_unique_resultbound. pvs_gap_scalar_unique_resultbound + S (dst_index_scalar_unique_result) = (l)) -> (exists dst_positive_code_scalar_unique_resultfirst dst_positive_scale_scalar_unique_resultfirst dst_negative_code_scalar_unique_resultfirst dst_negative_scale_scalar_unique_resultfirst dst_positive_scalar_unique_resultfirst dst_negative_scalar_unique_resultfirst. (((G) = (((((dst_positive_code_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst)) * S ((dst_positive_code_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst)) + ((dst_positive_scale_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst))) + (((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) * S ((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) + ((dst_negative_scale_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)))) * S ((((dst_positive_code_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst)) * S ((dst_positive_code_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst)) + ((dst_positive_scale_scalar_unique_resultfirst) + (dst_positive_scale_scalar_unique_resultfirst))) + (((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) * S ((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) + ((dst_negative_scale_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)))) + ((((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) * S ((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) + ((dst_negative_scale_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst))) + (((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) * S ((dst_negative_code_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)) + ((dst_negative_scale_scalar_unique_resultfirst) + (dst_negative_scale_scalar_unique_resultfirst)))))) /\ (((((exists ff_h_pvs_scalar_unique_resultfirstpositive. ff_h_pvs_scalar_unique_resultfirstpositive + S (dst_positive_scalar_unique_resultfirst) = S ((S (dst_index_scalar_unique_result)) * dst_positive_scale_scalar_unique_resultfirst)) /\ exists ff_q_pvs_scalar_unique_resultfirstpositive. dst_positive_code_scalar_unique_resultfirst = ff_q_pvs_scalar_unique_resultfirstpositive * S ((S (dst_index_scalar_unique_result)) * dst_positive_scale_scalar_unique_resultfirst) + (dst_positive_scalar_unique_resultfirst))) /\ (((((exists ff_h_pvs_scalar_unique_resultfirstnegative. ff_h_pvs_scalar_unique_resultfirstnegative + S (dst_negative_scalar_unique_resultfirst) = S ((S (dst_index_scalar_unique_result)) * dst_negative_scale_scalar_unique_resultfirst)) /\ exists ff_q_pvs_scalar_unique_resultfirstnegative. dst_negative_code_scalar_unique_resultfirst = ff_q_pvs_scalar_unique_resultfirstnegative * S ((S (dst_index_scalar_unique_result)) * dst_negative_scale_scalar_unique_resultfirst) + (dst_negative_scalar_unique_resultfirst))) /\ (exists ge_balance_positive_scalar_unique_resultfirstvalue ge_balance_negative_scalar_unique_resultfirstvalue. (((((dst_first_scalar_unique_result) = 2 * (ge_balance_positive_scalar_unique_resultfirstvalue) /\ (ge_balance_negative_scalar_unique_resultfirstvalue) = 0) \/ exists ge_signed_half_scalar_unique_resultfirstvaluedecode. (((dst_first_scalar_unique_result) = 2 * ge_signed_half_scalar_unique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_resultfirstvalue) = 0) /\ (ge_balance_negative_scalar_unique_resultfirstvalue) = S ge_signed_half_scalar_unique_resultfirstvaluedecode))) /\ ((dst_positive_scalar_unique_resultfirst) + ge_balance_negative_scalar_unique_resultfirstvalue = (dst_negative_scalar_unique_resultfirst) + ge_balance_positive_scalar_unique_resultfirstvalue))))))))) -> (exists dst_positive_code_scalar_unique_resultsecond dst_positive_scale_scalar_unique_resultsecond dst_negative_code_scalar_unique_resultsecond dst_negative_scale_scalar_unique_resultsecond dst_positive_scalar_unique_resultsecond dst_negative_scalar_unique_resultsecond. (((H) = (((((dst_positive_code_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond)) * S ((dst_positive_code_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond)) + ((dst_positive_scale_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond))) + (((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) * S ((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) + ((dst_negative_scale_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)))) * S ((((dst_positive_code_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond)) * S ((dst_positive_code_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond)) + ((dst_positive_scale_scalar_unique_resultsecond) + (dst_positive_scale_scalar_unique_resultsecond))) + (((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) * S ((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) + ((dst_negative_scale_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)))) + ((((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) * S ((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) + ((dst_negative_scale_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond))) + (((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) * S ((dst_negative_code_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)) + ((dst_negative_scale_scalar_unique_resultsecond) + (dst_negative_scale_scalar_unique_resultsecond)))))) /\ (((((exists ff_h_pvs_scalar_unique_resultsecondpositive. ff_h_pvs_scalar_unique_resultsecondpositive + S (dst_positive_scalar_unique_resultsecond) = S ((S (dst_index_scalar_unique_result)) * dst_positive_scale_scalar_unique_resultsecond)) /\ exists ff_q_pvs_scalar_unique_resultsecondpositive. dst_positive_code_scalar_unique_resultsecond = ff_q_pvs_scalar_unique_resultsecondpositive * S ((S (dst_index_scalar_unique_result)) * dst_positive_scale_scalar_unique_resultsecond) + (dst_positive_scalar_unique_resultsecond))) /\ (((((exists ff_h_pvs_scalar_unique_resultsecondnegative. ff_h_pvs_scalar_unique_resultsecondnegative + S (dst_negative_scalar_unique_resultsecond) = S ((S (dst_index_scalar_unique_result)) * dst_negative_scale_scalar_unique_resultsecond)) /\ exists ff_q_pvs_scalar_unique_resultsecondnegative. dst_negative_code_scalar_unique_resultsecond = ff_q_pvs_scalar_unique_resultsecondnegative * S ((S (dst_index_scalar_unique_result)) * dst_negative_scale_scalar_unique_resultsecond) + (dst_negative_scalar_unique_resultsecond))) /\ (exists ge_balance_positive_scalar_unique_resultsecondvalue ge_balance_negative_scalar_unique_resultsecondvalue. (((((dst_second_scalar_unique_result) = 2 * (ge_balance_positive_scalar_unique_resultsecondvalue) /\ (ge_balance_negative_scalar_unique_resultsecondvalue) = 0) \/ exists ge_signed_half_scalar_unique_resultsecondvaluedecode. (((dst_second_scalar_unique_result) = 2 * ge_signed_half_scalar_unique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_scalar_unique_resultsecondvalue) = 0) /\ (ge_balance_negative_scalar_unique_resultsecondvalue) = S ge_signed_half_scalar_unique_resultsecondvaluedecode))) /\ ((dst_positive_scalar_unique_resultsecond) + ge_balance_negative_scalar_unique_resultsecondvalue = (dst_negative_scalar_unique_resultsecond) + ge_balance_positive_scalar_unique_resultsecondvalue))))))))) -> dst_first_scalar_unique_result = dst_second_scalar_unique_result)