signed_table_scalar_extend

Exact expanded first-order arithmetic statement

forall a F G K l b c. (((exists dst_positive_code_scalar_extend_sourceinput_table dst_positive_scale_scalar_extend_sourceinput_table dst_negative_code_scalar_extend_sourceinput_table dst_negative_scale_scalar_extend_sourceinput_table. (((F) = (((((dst_positive_code_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table)) * S ((dst_positive_code_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table)) + ((dst_positive_scale_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table))) + (((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) * S ((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) + ((dst_negative_scale_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)))) * S ((((dst_positive_code_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table)) * S ((dst_positive_code_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table)) + ((dst_positive_scale_scalar_extend_sourceinput_table) + (dst_positive_scale_scalar_extend_sourceinput_table))) + (((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) * S ((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) + ((dst_negative_scale_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)))) + ((((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) * S ((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) + ((dst_negative_scale_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table))) + (((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) * S ((dst_negative_code_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)) + ((dst_negative_scale_scalar_extend_sourceinput_table) + (dst_negative_scale_scalar_extend_sourceinput_table)))))) /\ (forall dst_index_scalar_extend_sourceinput_table. (exists pvs_le_gap_scalar_extend_sourceinput_tabledomain. pvs_le_gap_scalar_extend_sourceinput_tabledomain + (dst_index_scalar_extend_sourceinput_table) = (l)) -> exists dst_positive_scalar_extend_sourceinput_table dst_negative_scalar_extend_sourceinput_table dst_value_scalar_extend_sourceinput_table. ((((exists ff_h_pvs_scalar_extend_sourceinput_tableentrypositive. ff_h_pvs_scalar_extend_sourceinput_tableentrypositive + S (dst_positive_scalar_extend_sourceinput_table) = S ((S (dst_index_scalar_extend_sourceinput_table)) * dst_positive_scale_scalar_extend_sourceinput_table)) /\ exists ff_q_pvs_scalar_extend_sourceinput_tableentrypositive. dst_positive_code_scalar_extend_sourceinput_table = ff_q_pvs_scalar_extend_sourceinput_tableentrypositive * S ((S (dst_index_scalar_extend_sourceinput_table)) * dst_positive_scale_scalar_extend_sourceinput_table) + (dst_positive_scalar_extend_sourceinput_table))) /\ (((((exists ff_h_pvs_scalar_extend_sourceinput_tableentrynegative. ff_h_pvs_scalar_extend_sourceinput_tableentrynegative + S (dst_negative_scalar_extend_sourceinput_table) = S ((S (dst_index_scalar_extend_sourceinput_table)) * dst_negative_scale_scalar_extend_sourceinput_table)) /\ exists ff_q_pvs_scalar_extend_sourceinput_tableentrynegative. dst_negative_code_scalar_extend_sourceinput_table = ff_q_pvs_scalar_extend_sourceinput_tableentrynegative * S ((S (dst_index_scalar_extend_sourceinput_table)) * dst_negative_scale_scalar_extend_sourceinput_table) + (dst_negative_scalar_extend_sourceinput_table))) /\ (exists ge_balance_positive_scalar_extend_sourceinput_tableentryvalue ge_balance_negative_scalar_extend_sourceinput_tableentryvalue. (((((dst_value_scalar_extend_sourceinput_table) = 2 * (ge_balance_positive_scalar_extend_sourceinput_tableentryvalue) /\ (ge_balance_negative_scalar_extend_sourceinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_extend_sourceinput_tableentryvaluedecode. (((dst_value_scalar_extend_sourceinput_table) = 2 * ge_signed_half_scalar_extend_sourceinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_sourceinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_extend_sourceinput_tableentryvalue) = S ge_signed_half_scalar_extend_sourceinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_extend_sourceinput_table) + ge_balance_negative_scalar_extend_sourceinput_tableentryvalue = (dst_negative_scalar_extend_sourceinput_table) + ge_balance_positive_scalar_extend_sourceinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_extend_sourceoutput_table dst_positive_scale_scalar_extend_sourceoutput_table dst_negative_code_scalar_extend_sourceoutput_table dst_negative_scale_scalar_extend_sourceoutput_table. (((G) = (((((dst_positive_code_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table)) * S ((dst_positive_code_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table)) + ((dst_positive_scale_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table))) + (((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) * S ((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) + ((dst_negative_scale_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)))) * S ((((dst_positive_code_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table)) * S ((dst_positive_code_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table)) + ((dst_positive_scale_scalar_extend_sourceoutput_table) + (dst_positive_scale_scalar_extend_sourceoutput_table))) + (((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) * S ((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) + ((dst_negative_scale_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)))) + ((((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) * S ((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) + ((dst_negative_scale_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table))) + (((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) * S ((dst_negative_code_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)) + ((dst_negative_scale_scalar_extend_sourceoutput_table) + (dst_negative_scale_scalar_extend_sourceoutput_table)))))) /\ (forall dst_index_scalar_extend_sourceoutput_table. (exists pvs_le_gap_scalar_extend_sourceoutput_tabledomain. pvs_le_gap_scalar_extend_sourceoutput_tabledomain + (dst_index_scalar_extend_sourceoutput_table) = (l)) -> exists dst_positive_scalar_extend_sourceoutput_table dst_negative_scalar_extend_sourceoutput_table dst_value_scalar_extend_sourceoutput_table. ((((exists ff_h_pvs_scalar_extend_sourceoutput_tableentrypositive. ff_h_pvs_scalar_extend_sourceoutput_tableentrypositive + S (dst_positive_scalar_extend_sourceoutput_table) = S ((S (dst_index_scalar_extend_sourceoutput_table)) * dst_positive_scale_scalar_extend_sourceoutput_table)) /\ exists ff_q_pvs_scalar_extend_sourceoutput_tableentrypositive. dst_positive_code_scalar_extend_sourceoutput_table = ff_q_pvs_scalar_extend_sourceoutput_tableentrypositive * S ((S (dst_index_scalar_extend_sourceoutput_table)) * dst_positive_scale_scalar_extend_sourceoutput_table) + (dst_positive_scalar_extend_sourceoutput_table))) /\ (((((exists ff_h_pvs_scalar_extend_sourceoutput_tableentrynegative. ff_h_pvs_scalar_extend_sourceoutput_tableentrynegative + S (dst_negative_scalar_extend_sourceoutput_table) = S ((S (dst_index_scalar_extend_sourceoutput_table)) * dst_negative_scale_scalar_extend_sourceoutput_table)) /\ exists ff_q_pvs_scalar_extend_sourceoutput_tableentrynegative. dst_negative_code_scalar_extend_sourceoutput_table = ff_q_pvs_scalar_extend_sourceoutput_tableentrynegative * S ((S (dst_index_scalar_extend_sourceoutput_table)) * dst_negative_scale_scalar_extend_sourceoutput_table) + (dst_negative_scalar_extend_sourceoutput_table))) /\ (exists ge_balance_positive_scalar_extend_sourceoutput_tableentryvalue ge_balance_negative_scalar_extend_sourceoutput_tableentryvalue. (((((dst_value_scalar_extend_sourceoutput_table) = 2 * (ge_balance_positive_scalar_extend_sourceoutput_tableentryvalue) /\ (ge_balance_negative_scalar_extend_sourceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_extend_sourceoutput_tableentryvaluedecode. (((dst_value_scalar_extend_sourceoutput_table) = 2 * ge_signed_half_scalar_extend_sourceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_sourceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_extend_sourceoutput_tableentryvalue) = S ge_signed_half_scalar_extend_sourceoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_extend_sourceoutput_table) + ge_balance_negative_scalar_extend_sourceoutput_tableentryvalue = (dst_negative_scalar_extend_sourceoutput_table) + ge_balance_positive_scalar_extend_sourceoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_extend_sourceentries. (exists pvs_gap_scalar_extend_sourceentriesbound. pvs_gap_scalar_extend_sourceentriesbound + S (sto_index_scalar_extend_sourceentries) = (l)) -> exists sto_input_scalar_extend_sourceentries sto_output_scalar_extend_sourceentries. ((exists dst_positive_code_scalar_extend_sourceentriesentryinput dst_positive_scale_scalar_extend_sourceentriesentryinput dst_negative_code_scalar_extend_sourceentriesentryinput dst_negative_scale_scalar_extend_sourceentriesentryinput dst_positive_scalar_extend_sourceentriesentryinput dst_negative_scalar_extend_sourceentriesentryinput. (((F) = (((((dst_positive_code_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_positive_code_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput)) + ((dst_positive_scale_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput))) + (((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)))) * S ((((dst_positive_code_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_positive_code_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput)) + ((dst_positive_scale_scalar_extend_sourceentriesentryinput) + (dst_positive_scale_scalar_extend_sourceentriesentryinput))) + (((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)))) + ((((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput))) + (((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryinput) + (dst_negative_scale_scalar_extend_sourceentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_extend_sourceentriesentryinputpositive. ff_h_pvs_scalar_extend_sourceentriesentryinputpositive + S (dst_positive_scalar_extend_sourceentriesentryinput) = S ((S (sto_index_scalar_extend_sourceentries)) * dst_positive_scale_scalar_extend_sourceentriesentryinput)) /\ exists ff_q_pvs_scalar_extend_sourceentriesentryinputpositive. dst_positive_code_scalar_extend_sourceentriesentryinput = ff_q_pvs_scalar_extend_sourceentriesentryinputpositive * S ((S (sto_index_scalar_extend_sourceentries)) * dst_positive_scale_scalar_extend_sourceentriesentryinput) + (dst_positive_scalar_extend_sourceentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_extend_sourceentriesentryinputnegative. ff_h_pvs_scalar_extend_sourceentriesentryinputnegative + S (dst_negative_scalar_extend_sourceentriesentryinput) = S ((S (sto_index_scalar_extend_sourceentries)) * dst_negative_scale_scalar_extend_sourceentriesentryinput)) /\ exists ff_q_pvs_scalar_extend_sourceentriesentryinputnegative. dst_negative_code_scalar_extend_sourceentriesentryinput = ff_q_pvs_scalar_extend_sourceentriesentryinputnegative * S ((S (sto_index_scalar_extend_sourceentries)) * dst_negative_scale_scalar_extend_sourceentriesentryinput) + (dst_negative_scalar_extend_sourceentriesentryinput))) /\ (exists ge_balance_positive_scalar_extend_sourceentriesentryinputvalue ge_balance_negative_scalar_extend_sourceentriesentryinputvalue. (((((sto_input_scalar_extend_sourceentries) = 2 * (ge_balance_positive_scalar_extend_sourceentriesentryinputvalue) /\ (ge_balance_negative_scalar_extend_sourceentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_extend_sourceentriesentryinputvaluedecode. (((sto_input_scalar_extend_sourceentries) = 2 * ge_signed_half_scalar_extend_sourceentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_sourceentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_extend_sourceentriesentryinputvalue) = S ge_signed_half_scalar_extend_sourceentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_extend_sourceentriesentryinput) + ge_balance_negative_scalar_extend_sourceentriesentryinputvalue = (dst_negative_scalar_extend_sourceentriesentryinput) + ge_balance_positive_scalar_extend_sourceentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_extend_sourceentriesentryoutput dst_positive_scale_scalar_extend_sourceentriesentryoutput dst_negative_code_scalar_extend_sourceentriesentryoutput dst_negative_scale_scalar_extend_sourceentriesentryoutput dst_positive_scalar_extend_sourceentriesentryoutput dst_negative_scalar_extend_sourceentriesentryoutput. (((G) = (((((dst_positive_code_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_positive_code_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_positive_scale_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput))) + (((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)))) * S ((((dst_positive_code_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_positive_code_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_positive_scale_scalar_extend_sourceentriesentryoutput) + (dst_positive_scale_scalar_extend_sourceentriesentryoutput))) + (((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)))) + ((((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput))) + (((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) * S ((dst_negative_code_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)) + ((dst_negative_scale_scalar_extend_sourceentriesentryoutput) + (dst_negative_scale_scalar_extend_sourceentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_extend_sourceentriesentryoutputpositive. ff_h_pvs_scalar_extend_sourceentriesentryoutputpositive + S (dst_positive_scalar_extend_sourceentriesentryoutput) = S ((S (sto_index_scalar_extend_sourceentries)) * dst_positive_scale_scalar_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_scalar_extend_sourceentriesentryoutputpositive. dst_positive_code_scalar_extend_sourceentriesentryoutput = ff_q_pvs_scalar_extend_sourceentriesentryoutputpositive * S ((S (sto_index_scalar_extend_sourceentries)) * dst_positive_scale_scalar_extend_sourceentriesentryoutput) + (dst_positive_scalar_extend_sourceentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_extend_sourceentriesentryoutputnegative. ff_h_pvs_scalar_extend_sourceentriesentryoutputnegative + S (dst_negative_scalar_extend_sourceentriesentryoutput) = S ((S (sto_index_scalar_extend_sourceentries)) * dst_negative_scale_scalar_extend_sourceentriesentryoutput)) /\ exists ff_q_pvs_scalar_extend_sourceentriesentryoutputnegative. dst_negative_code_scalar_extend_sourceentriesentryoutput = ff_q_pvs_scalar_extend_sourceentriesentryoutputnegative * S ((S (sto_index_scalar_extend_sourceentries)) * dst_negative_scale_scalar_extend_sourceentriesentryoutput) + (dst_negative_scalar_extend_sourceentriesentryoutput))) /\ (exists ge_balance_positive_scalar_extend_sourceentriesentryoutputvalue ge_balance_negative_scalar_extend_sourceentriesentryoutputvalue. (((((sto_output_scalar_extend_sourceentries) = 2 * (ge_balance_positive_scalar_extend_sourceentriesentryoutputvalue) /\ (ge_balance_negative_scalar_extend_sourceentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_extend_sourceentriesentryoutputvaluedecode. (((sto_output_scalar_extend_sourceentries) = 2 * ge_signed_half_scalar_extend_sourceentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_sourceentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_extend_sourceentriesentryoutputvalue) = S ge_signed_half_scalar_extend_sourceentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_extend_sourceentriesentryoutput) + ge_balance_negative_scalar_extend_sourceentriesentryoutputvalue = (dst_negative_scalar_extend_sourceentriesentryoutput) + ge_balance_positive_scalar_extend_sourceentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_extend_sourceentriesentryoperation sto_an_scalar_extend_sourceentriesentryoperation sto_bp_scalar_extend_sourceentriesentryoperation sto_bn_scalar_extend_sourceentriesentryoperation sto_cp_scalar_extend_sourceentriesentryoperation sto_cn_scalar_extend_sourceentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_extend_sourceentriesentryoperation) /\ (sto_an_scalar_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_sourceentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_extend_sourceentriesentryoperationleft + 1 /\ (sto_ap_scalar_extend_sourceentriesentryoperation) = 0) /\ (sto_an_scalar_extend_sourceentriesentryoperation) = S ge_signed_half_scalar_extend_sourceentriesentryoperationleft))) /\ ((((((sto_input_scalar_extend_sourceentries) = 2 * (sto_bp_scalar_extend_sourceentriesentryoperation) /\ (sto_bn_scalar_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_sourceentriesentryoperationright. (((sto_input_scalar_extend_sourceentries) = 2 * ge_signed_half_scalar_extend_sourceentriesentryoperationright + 1 /\ (sto_bp_scalar_extend_sourceentriesentryoperation) = 0) /\ (sto_bn_scalar_extend_sourceentriesentryoperation) = S ge_signed_half_scalar_extend_sourceentriesentryoperationright))) /\ ((((((sto_output_scalar_extend_sourceentries) = 2 * (sto_cp_scalar_extend_sourceentriesentryoperation) /\ (sto_cn_scalar_extend_sourceentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_sourceentriesentryoperationoutput. (((sto_output_scalar_extend_sourceentries) = 2 * ge_signed_half_scalar_extend_sourceentriesentryoperationoutput + 1 /\ (sto_cp_scalar_extend_sourceentriesentryoperation) = 0) /\ (sto_cn_scalar_extend_sourceentriesentryoperation) = S ge_signed_half_scalar_extend_sourceentriesentryoperationoutput))) /\ ((sto_ap_scalar_extend_sourceentriesentryoperation * sto_bp_scalar_extend_sourceentriesentryoperation + sto_an_scalar_extend_sourceentriesentryoperation * sto_bn_scalar_extend_sourceentriesentryoperation) + sto_cn_scalar_extend_sourceentriesentryoperation = (sto_ap_scalar_extend_sourceentriesentryoperation * sto_bn_scalar_extend_sourceentriesentryoperation + sto_an_scalar_extend_sourceentriesentryoperation * sto_bp_scalar_extend_sourceentriesentryoperation) + sto_cp_scalar_extend_sourceentriesentryoperation))))))))))))))) -> (exists dst_positive_code_scalar_extend_table dst_positive_scale_scalar_extend_table dst_negative_code_scalar_extend_table dst_negative_scale_scalar_extend_table. (((K) = (((((dst_positive_code_scalar_extend_table) + (dst_positive_scale_scalar_extend_table)) * S ((dst_positive_code_scalar_extend_table) + (dst_positive_scale_scalar_extend_table)) + ((dst_positive_scale_scalar_extend_table) + (dst_positive_scale_scalar_extend_table))) + (((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) * S ((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) + ((dst_negative_scale_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)))) * S ((((dst_positive_code_scalar_extend_table) + (dst_positive_scale_scalar_extend_table)) * S ((dst_positive_code_scalar_extend_table) + (dst_positive_scale_scalar_extend_table)) + ((dst_positive_scale_scalar_extend_table) + (dst_positive_scale_scalar_extend_table))) + (((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) * S ((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) + ((dst_negative_scale_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)))) + ((((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) * S ((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) + ((dst_negative_scale_scalar_extend_table) + (dst_negative_scale_scalar_extend_table))) + (((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) * S ((dst_negative_code_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)) + ((dst_negative_scale_scalar_extend_table) + (dst_negative_scale_scalar_extend_table)))))) /\ (forall dst_index_scalar_extend_table. (exists pvs_le_gap_scalar_extend_tabledomain. pvs_le_gap_scalar_extend_tabledomain + (dst_index_scalar_extend_table) = (l)) -> exists dst_positive_scalar_extend_table dst_negative_scalar_extend_table dst_value_scalar_extend_table. ((((exists ff_h_pvs_scalar_extend_tableentrypositive. ff_h_pvs_scalar_extend_tableentrypositive + S (dst_positive_scalar_extend_table) = S ((S (dst_index_scalar_extend_table)) * dst_positive_scale_scalar_extend_table)) /\ exists ff_q_pvs_scalar_extend_tableentrypositive. dst_positive_code_scalar_extend_table = ff_q_pvs_scalar_extend_tableentrypositive * S ((S (dst_index_scalar_extend_table)) * dst_positive_scale_scalar_extend_table) + (dst_positive_scalar_extend_table))) /\ (((((exists ff_h_pvs_scalar_extend_tableentrynegative. ff_h_pvs_scalar_extend_tableentrynegative + S (dst_negative_scalar_extend_table) = S ((S (dst_index_scalar_extend_table)) * dst_negative_scale_scalar_extend_table)) /\ exists ff_q_pvs_scalar_extend_tableentrynegative. dst_negative_code_scalar_extend_table = ff_q_pvs_scalar_extend_tableentrynegative * S ((S (dst_index_scalar_extend_table)) * dst_negative_scale_scalar_extend_table) + (dst_negative_scalar_extend_table))) /\ (exists ge_balance_positive_scalar_extend_tableentryvalue ge_balance_negative_scalar_extend_tableentryvalue. (((((dst_value_scalar_extend_table) = 2 * (ge_balance_positive_scalar_extend_tableentryvalue) /\ (ge_balance_negative_scalar_extend_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_extend_tableentryvaluedecode. (((dst_value_scalar_extend_table) = 2 * ge_signed_half_scalar_extend_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_extend_tableentryvalue) = S ge_signed_half_scalar_extend_tableentryvaluedecode))) /\ ((dst_positive_scalar_extend_table) + ge_balance_negative_scalar_extend_tableentryvalue = (dst_negative_scalar_extend_table) + ge_balance_positive_scalar_extend_tableentryvalue))))))))) -> (forall dst_index_scalar_extend_preservation dst_first_scalar_extend_preservation dst_second_scalar_extend_preservation. (exists pvs_gap_scalar_extend_preservationbound. pvs_gap_scalar_extend_preservationbound + S (dst_index_scalar_extend_preservation) = (l)) -> (exists dst_positive_code_scalar_extend_preservationfirst dst_positive_scale_scalar_extend_preservationfirst dst_negative_code_scalar_extend_preservationfirst dst_negative_scale_scalar_extend_preservationfirst dst_positive_scalar_extend_preservationfirst dst_negative_scalar_extend_preservationfirst. (((G) = (((((dst_positive_code_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst)) * S ((dst_positive_code_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst)) + ((dst_positive_scale_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst))) + (((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) * S ((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) + ((dst_negative_scale_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)))) * S ((((dst_positive_code_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst)) * S ((dst_positive_code_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst)) + ((dst_positive_scale_scalar_extend_preservationfirst) + (dst_positive_scale_scalar_extend_preservationfirst))) + (((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) * S ((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) + ((dst_negative_scale_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)))) + ((((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) * S ((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) + ((dst_negative_scale_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst))) + (((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) * S ((dst_negative_code_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)) + ((dst_negative_scale_scalar_extend_preservationfirst) + (dst_negative_scale_scalar_extend_preservationfirst)))))) /\ (((((exists ff_h_pvs_scalar_extend_preservationfirstpositive. ff_h_pvs_scalar_extend_preservationfirstpositive + S (dst_positive_scalar_extend_preservationfirst) = S ((S (dst_index_scalar_extend_preservation)) * dst_positive_scale_scalar_extend_preservationfirst)) /\ exists ff_q_pvs_scalar_extend_preservationfirstpositive. dst_positive_code_scalar_extend_preservationfirst = ff_q_pvs_scalar_extend_preservationfirstpositive * S ((S (dst_index_scalar_extend_preservation)) * dst_positive_scale_scalar_extend_preservationfirst) + (dst_positive_scalar_extend_preservationfirst))) /\ (((((exists ff_h_pvs_scalar_extend_preservationfirstnegative. ff_h_pvs_scalar_extend_preservationfirstnegative + S (dst_negative_scalar_extend_preservationfirst) = S ((S (dst_index_scalar_extend_preservation)) * dst_negative_scale_scalar_extend_preservationfirst)) /\ exists ff_q_pvs_scalar_extend_preservationfirstnegative. dst_negative_code_scalar_extend_preservationfirst = ff_q_pvs_scalar_extend_preservationfirstnegative * S ((S (dst_index_scalar_extend_preservation)) * dst_negative_scale_scalar_extend_preservationfirst) + (dst_negative_scalar_extend_preservationfirst))) /\ (exists ge_balance_positive_scalar_extend_preservationfirstvalue ge_balance_negative_scalar_extend_preservationfirstvalue. (((((dst_first_scalar_extend_preservation) = 2 * (ge_balance_positive_scalar_extend_preservationfirstvalue) /\ (ge_balance_negative_scalar_extend_preservationfirstvalue) = 0) \/ exists ge_signed_half_scalar_extend_preservationfirstvaluedecode. (((dst_first_scalar_extend_preservation) = 2 * ge_signed_half_scalar_extend_preservationfirstvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_preservationfirstvalue) = 0) /\ (ge_balance_negative_scalar_extend_preservationfirstvalue) = S ge_signed_half_scalar_extend_preservationfirstvaluedecode))) /\ ((dst_positive_scalar_extend_preservationfirst) + ge_balance_negative_scalar_extend_preservationfirstvalue = (dst_negative_scalar_extend_preservationfirst) + ge_balance_positive_scalar_extend_preservationfirstvalue))))))))) -> (exists dst_positive_code_scalar_extend_preservationsecond dst_positive_scale_scalar_extend_preservationsecond dst_negative_code_scalar_extend_preservationsecond dst_negative_scale_scalar_extend_preservationsecond dst_positive_scalar_extend_preservationsecond dst_negative_scalar_extend_preservationsecond. (((K) = (((((dst_positive_code_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond)) * S ((dst_positive_code_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond)) + ((dst_positive_scale_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond))) + (((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) * S ((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) + ((dst_negative_scale_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)))) * S ((((dst_positive_code_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond)) * S ((dst_positive_code_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond)) + ((dst_positive_scale_scalar_extend_preservationsecond) + (dst_positive_scale_scalar_extend_preservationsecond))) + (((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) * S ((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) + ((dst_negative_scale_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)))) + ((((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) * S ((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) + ((dst_negative_scale_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond))) + (((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) * S ((dst_negative_code_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)) + ((dst_negative_scale_scalar_extend_preservationsecond) + (dst_negative_scale_scalar_extend_preservationsecond)))))) /\ (((((exists ff_h_pvs_scalar_extend_preservationsecondpositive. ff_h_pvs_scalar_extend_preservationsecondpositive + S (dst_positive_scalar_extend_preservationsecond) = S ((S (dst_index_scalar_extend_preservation)) * dst_positive_scale_scalar_extend_preservationsecond)) /\ exists ff_q_pvs_scalar_extend_preservationsecondpositive. dst_positive_code_scalar_extend_preservationsecond = ff_q_pvs_scalar_extend_preservationsecondpositive * S ((S (dst_index_scalar_extend_preservation)) * dst_positive_scale_scalar_extend_preservationsecond) + (dst_positive_scalar_extend_preservationsecond))) /\ (((((exists ff_h_pvs_scalar_extend_preservationsecondnegative. ff_h_pvs_scalar_extend_preservationsecondnegative + S (dst_negative_scalar_extend_preservationsecond) = S ((S (dst_index_scalar_extend_preservation)) * dst_negative_scale_scalar_extend_preservationsecond)) /\ exists ff_q_pvs_scalar_extend_preservationsecondnegative. dst_negative_code_scalar_extend_preservationsecond = ff_q_pvs_scalar_extend_preservationsecondnegative * S ((S (dst_index_scalar_extend_preservation)) * dst_negative_scale_scalar_extend_preservationsecond) + (dst_negative_scalar_extend_preservationsecond))) /\ (exists ge_balance_positive_scalar_extend_preservationsecondvalue ge_balance_negative_scalar_extend_preservationsecondvalue. (((((dst_second_scalar_extend_preservation) = 2 * (ge_balance_positive_scalar_extend_preservationsecondvalue) /\ (ge_balance_negative_scalar_extend_preservationsecondvalue) = 0) \/ exists ge_signed_half_scalar_extend_preservationsecondvaluedecode. (((dst_second_scalar_extend_preservation) = 2 * ge_signed_half_scalar_extend_preservationsecondvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_preservationsecondvalue) = 0) /\ (ge_balance_negative_scalar_extend_preservationsecondvalue) = S ge_signed_half_scalar_extend_preservationsecondvaluedecode))) /\ ((dst_positive_scalar_extend_preservationsecond) + ge_balance_negative_scalar_extend_preservationsecondvalue = (dst_negative_scalar_extend_preservationsecond) + ge_balance_positive_scalar_extend_preservationsecondvalue))))))))) -> dst_first_scalar_extend_preservation = dst_second_scalar_extend_preservation) -> (exists dst_positive_code_scalar_extend_at_0 dst_positive_scale_scalar_extend_at_0 dst_negative_code_scalar_extend_at_0 dst_negative_scale_scalar_extend_at_0 dst_positive_scalar_extend_at_0 dst_negative_scalar_extend_at_0. (((F) = (((((dst_positive_code_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0)) * S ((dst_positive_code_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0)) + ((dst_positive_scale_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0))) + (((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) * S ((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) + ((dst_negative_scale_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)))) * S ((((dst_positive_code_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0)) * S ((dst_positive_code_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0)) + ((dst_positive_scale_scalar_extend_at_0) + (dst_positive_scale_scalar_extend_at_0))) + (((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) * S ((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) + ((dst_negative_scale_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)))) + ((((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) * S ((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) + ((dst_negative_scale_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0))) + (((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) * S ((dst_negative_code_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)) + ((dst_negative_scale_scalar_extend_at_0) + (dst_negative_scale_scalar_extend_at_0)))))) /\ (((((exists ff_h_pvs_scalar_extend_at_0positive. ff_h_pvs_scalar_extend_at_0positive + S (dst_positive_scalar_extend_at_0) = S ((S (l)) * dst_positive_scale_scalar_extend_at_0)) /\ exists ff_q_pvs_scalar_extend_at_0positive. dst_positive_code_scalar_extend_at_0 = ff_q_pvs_scalar_extend_at_0positive * S ((S (l)) * dst_positive_scale_scalar_extend_at_0) + (dst_positive_scalar_extend_at_0))) /\ (((((exists ff_h_pvs_scalar_extend_at_0negative. ff_h_pvs_scalar_extend_at_0negative + S (dst_negative_scalar_extend_at_0) = S ((S (l)) * dst_negative_scale_scalar_extend_at_0)) /\ exists ff_q_pvs_scalar_extend_at_0negative. dst_negative_code_scalar_extend_at_0 = ff_q_pvs_scalar_extend_at_0negative * S ((S (l)) * dst_negative_scale_scalar_extend_at_0) + (dst_negative_scalar_extend_at_0))) /\ (exists ge_balance_positive_scalar_extend_at_0value ge_balance_negative_scalar_extend_at_0value. (((((b) = 2 * (ge_balance_positive_scalar_extend_at_0value) /\ (ge_balance_negative_scalar_extend_at_0value) = 0) \/ exists ge_signed_half_scalar_extend_at_0valuedecode. (((b) = 2 * ge_signed_half_scalar_extend_at_0valuedecode + 1 /\ (ge_balance_positive_scalar_extend_at_0value) = 0) /\ (ge_balance_negative_scalar_extend_at_0value) = S ge_signed_half_scalar_extend_at_0valuedecode))) /\ ((dst_positive_scalar_extend_at_0) + ge_balance_negative_scalar_extend_at_0value = (dst_negative_scalar_extend_at_0) + ge_balance_positive_scalar_extend_at_0value))))))))) -> (exists dst_positive_code_scalar_extend_at_1 dst_positive_scale_scalar_extend_at_1 dst_negative_code_scalar_extend_at_1 dst_negative_scale_scalar_extend_at_1 dst_positive_scalar_extend_at_1 dst_negative_scalar_extend_at_1. (((K) = (((((dst_positive_code_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1)) * S ((dst_positive_code_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1)) + ((dst_positive_scale_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1))) + (((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) * S ((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) + ((dst_negative_scale_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)))) * S ((((dst_positive_code_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1)) * S ((dst_positive_code_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1)) + ((dst_positive_scale_scalar_extend_at_1) + (dst_positive_scale_scalar_extend_at_1))) + (((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) * S ((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) + ((dst_negative_scale_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)))) + ((((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) * S ((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) + ((dst_negative_scale_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1))) + (((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) * S ((dst_negative_code_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)) + ((dst_negative_scale_scalar_extend_at_1) + (dst_negative_scale_scalar_extend_at_1)))))) /\ (((((exists ff_h_pvs_scalar_extend_at_1positive. ff_h_pvs_scalar_extend_at_1positive + S (dst_positive_scalar_extend_at_1) = S ((S (l)) * dst_positive_scale_scalar_extend_at_1)) /\ exists ff_q_pvs_scalar_extend_at_1positive. dst_positive_code_scalar_extend_at_1 = ff_q_pvs_scalar_extend_at_1positive * S ((S (l)) * dst_positive_scale_scalar_extend_at_1) + (dst_positive_scalar_extend_at_1))) /\ (((((exists ff_h_pvs_scalar_extend_at_1negative. ff_h_pvs_scalar_extend_at_1negative + S (dst_negative_scalar_extend_at_1) = S ((S (l)) * dst_negative_scale_scalar_extend_at_1)) /\ exists ff_q_pvs_scalar_extend_at_1negative. dst_negative_code_scalar_extend_at_1 = ff_q_pvs_scalar_extend_at_1negative * S ((S (l)) * dst_negative_scale_scalar_extend_at_1) + (dst_negative_scalar_extend_at_1))) /\ (exists ge_balance_positive_scalar_extend_at_1value ge_balance_negative_scalar_extend_at_1value. (((((c) = 2 * (ge_balance_positive_scalar_extend_at_1value) /\ (ge_balance_negative_scalar_extend_at_1value) = 0) \/ exists ge_signed_half_scalar_extend_at_1valuedecode. (((c) = 2 * ge_signed_half_scalar_extend_at_1valuedecode + 1 /\ (ge_balance_positive_scalar_extend_at_1value) = 0) /\ (ge_balance_negative_scalar_extend_at_1value) = S ge_signed_half_scalar_extend_at_1valuedecode))) /\ ((dst_positive_scalar_extend_at_1) + ge_balance_negative_scalar_extend_at_1value = (dst_negative_scalar_extend_at_1) + ge_balance_positive_scalar_extend_at_1value))))))))) -> (exists sto_ap_scalar_extend_operation sto_an_scalar_extend_operation sto_bp_scalar_extend_operation sto_bn_scalar_extend_operation sto_cp_scalar_extend_operation sto_cn_scalar_extend_operation. (((((a) = 2 * (sto_ap_scalar_extend_operation) /\ (sto_an_scalar_extend_operation) = 0) \/ exists ge_signed_half_scalar_extend_operationleft. (((a) = 2 * ge_signed_half_scalar_extend_operationleft + 1 /\ (sto_ap_scalar_extend_operation) = 0) /\ (sto_an_scalar_extend_operation) = S ge_signed_half_scalar_extend_operationleft))) /\ ((((((b) = 2 * (sto_bp_scalar_extend_operation) /\ (sto_bn_scalar_extend_operation) = 0) \/ exists ge_signed_half_scalar_extend_operationright. (((b) = 2 * ge_signed_half_scalar_extend_operationright + 1 /\ (sto_bp_scalar_extend_operation) = 0) /\ (sto_bn_scalar_extend_operation) = S ge_signed_half_scalar_extend_operationright))) /\ ((((((c) = 2 * (sto_cp_scalar_extend_operation) /\ (sto_cn_scalar_extend_operation) = 0) \/ exists ge_signed_half_scalar_extend_operationoutput. (((c) = 2 * ge_signed_half_scalar_extend_operationoutput + 1 /\ (sto_cp_scalar_extend_operation) = 0) /\ (sto_cn_scalar_extend_operation) = S ge_signed_half_scalar_extend_operationoutput))) /\ ((sto_ap_scalar_extend_operation * sto_bp_scalar_extend_operation + sto_an_scalar_extend_operation * sto_bn_scalar_extend_operation) + sto_cn_scalar_extend_operation = (sto_ap_scalar_extend_operation * sto_bn_scalar_extend_operation + sto_an_scalar_extend_operation * sto_bp_scalar_extend_operation) + sto_cp_scalar_extend_operation))))))) -> (((exists dst_positive_code_scalar_extend_resultinput_table dst_positive_scale_scalar_extend_resultinput_table dst_negative_code_scalar_extend_resultinput_table dst_negative_scale_scalar_extend_resultinput_table. (((F) = (((((dst_positive_code_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table)) * S ((dst_positive_code_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table)) + ((dst_positive_scale_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table))) + (((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) * S ((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) + ((dst_negative_scale_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)))) * S ((((dst_positive_code_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table)) * S ((dst_positive_code_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table)) + ((dst_positive_scale_scalar_extend_resultinput_table) + (dst_positive_scale_scalar_extend_resultinput_table))) + (((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) * S ((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) + ((dst_negative_scale_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)))) + ((((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) * S ((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) + ((dst_negative_scale_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table))) + (((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) * S ((dst_negative_code_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)) + ((dst_negative_scale_scalar_extend_resultinput_table) + (dst_negative_scale_scalar_extend_resultinput_table)))))) /\ (forall dst_index_scalar_extend_resultinput_table. (exists pvs_le_gap_scalar_extend_resultinput_tabledomain. pvs_le_gap_scalar_extend_resultinput_tabledomain + (dst_index_scalar_extend_resultinput_table) = (S l)) -> exists dst_positive_scalar_extend_resultinput_table dst_negative_scalar_extend_resultinput_table dst_value_scalar_extend_resultinput_table. ((((exists ff_h_pvs_scalar_extend_resultinput_tableentrypositive. ff_h_pvs_scalar_extend_resultinput_tableentrypositive + S (dst_positive_scalar_extend_resultinput_table) = S ((S (dst_index_scalar_extend_resultinput_table)) * dst_positive_scale_scalar_extend_resultinput_table)) /\ exists ff_q_pvs_scalar_extend_resultinput_tableentrypositive. dst_positive_code_scalar_extend_resultinput_table = ff_q_pvs_scalar_extend_resultinput_tableentrypositive * S ((S (dst_index_scalar_extend_resultinput_table)) * dst_positive_scale_scalar_extend_resultinput_table) + (dst_positive_scalar_extend_resultinput_table))) /\ (((((exists ff_h_pvs_scalar_extend_resultinput_tableentrynegative. ff_h_pvs_scalar_extend_resultinput_tableentrynegative + S (dst_negative_scalar_extend_resultinput_table) = S ((S (dst_index_scalar_extend_resultinput_table)) * dst_negative_scale_scalar_extend_resultinput_table)) /\ exists ff_q_pvs_scalar_extend_resultinput_tableentrynegative. dst_negative_code_scalar_extend_resultinput_table = ff_q_pvs_scalar_extend_resultinput_tableentrynegative * S ((S (dst_index_scalar_extend_resultinput_table)) * dst_negative_scale_scalar_extend_resultinput_table) + (dst_negative_scalar_extend_resultinput_table))) /\ (exists ge_balance_positive_scalar_extend_resultinput_tableentryvalue ge_balance_negative_scalar_extend_resultinput_tableentryvalue. (((((dst_value_scalar_extend_resultinput_table) = 2 * (ge_balance_positive_scalar_extend_resultinput_tableentryvalue) /\ (ge_balance_negative_scalar_extend_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_extend_resultinput_tableentryvaluedecode. (((dst_value_scalar_extend_resultinput_table) = 2 * ge_signed_half_scalar_extend_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_extend_resultinput_tableentryvalue) = S ge_signed_half_scalar_extend_resultinput_tableentryvaluedecode))) /\ ((dst_positive_scalar_extend_resultinput_table) + ge_balance_negative_scalar_extend_resultinput_tableentryvalue = (dst_negative_scalar_extend_resultinput_table) + ge_balance_positive_scalar_extend_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_scalar_extend_resultoutput_table dst_positive_scale_scalar_extend_resultoutput_table dst_negative_code_scalar_extend_resultoutput_table dst_negative_scale_scalar_extend_resultoutput_table. (((K) = (((((dst_positive_code_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table)) * S ((dst_positive_code_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table)) + ((dst_positive_scale_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table))) + (((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) * S ((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) + ((dst_negative_scale_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)))) * S ((((dst_positive_code_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table)) * S ((dst_positive_code_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table)) + ((dst_positive_scale_scalar_extend_resultoutput_table) + (dst_positive_scale_scalar_extend_resultoutput_table))) + (((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) * S ((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) + ((dst_negative_scale_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)))) + ((((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) * S ((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) + ((dst_negative_scale_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table))) + (((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) * S ((dst_negative_code_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)) + ((dst_negative_scale_scalar_extend_resultoutput_table) + (dst_negative_scale_scalar_extend_resultoutput_table)))))) /\ (forall dst_index_scalar_extend_resultoutput_table. (exists pvs_le_gap_scalar_extend_resultoutput_tabledomain. pvs_le_gap_scalar_extend_resultoutput_tabledomain + (dst_index_scalar_extend_resultoutput_table) = (S l)) -> exists dst_positive_scalar_extend_resultoutput_table dst_negative_scalar_extend_resultoutput_table dst_value_scalar_extend_resultoutput_table. ((((exists ff_h_pvs_scalar_extend_resultoutput_tableentrypositive. ff_h_pvs_scalar_extend_resultoutput_tableentrypositive + S (dst_positive_scalar_extend_resultoutput_table) = S ((S (dst_index_scalar_extend_resultoutput_table)) * dst_positive_scale_scalar_extend_resultoutput_table)) /\ exists ff_q_pvs_scalar_extend_resultoutput_tableentrypositive. dst_positive_code_scalar_extend_resultoutput_table = ff_q_pvs_scalar_extend_resultoutput_tableentrypositive * S ((S (dst_index_scalar_extend_resultoutput_table)) * dst_positive_scale_scalar_extend_resultoutput_table) + (dst_positive_scalar_extend_resultoutput_table))) /\ (((((exists ff_h_pvs_scalar_extend_resultoutput_tableentrynegative. ff_h_pvs_scalar_extend_resultoutput_tableentrynegative + S (dst_negative_scalar_extend_resultoutput_table) = S ((S (dst_index_scalar_extend_resultoutput_table)) * dst_negative_scale_scalar_extend_resultoutput_table)) /\ exists ff_q_pvs_scalar_extend_resultoutput_tableentrynegative. dst_negative_code_scalar_extend_resultoutput_table = ff_q_pvs_scalar_extend_resultoutput_tableentrynegative * S ((S (dst_index_scalar_extend_resultoutput_table)) * dst_negative_scale_scalar_extend_resultoutput_table) + (dst_negative_scalar_extend_resultoutput_table))) /\ (exists ge_balance_positive_scalar_extend_resultoutput_tableentryvalue ge_balance_negative_scalar_extend_resultoutput_tableentryvalue. (((((dst_value_scalar_extend_resultoutput_table) = 2 * (ge_balance_positive_scalar_extend_resultoutput_tableentryvalue) /\ (ge_balance_negative_scalar_extend_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_scalar_extend_resultoutput_tableentryvaluedecode. (((dst_value_scalar_extend_resultoutput_table) = 2 * ge_signed_half_scalar_extend_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_scalar_extend_resultoutput_tableentryvalue) = S ge_signed_half_scalar_extend_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_scalar_extend_resultoutput_table) + ge_balance_negative_scalar_extend_resultoutput_tableentryvalue = (dst_negative_scalar_extend_resultoutput_table) + ge_balance_positive_scalar_extend_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_scalar_extend_resultentries. (exists pvs_gap_scalar_extend_resultentriesbound. pvs_gap_scalar_extend_resultentriesbound + S (sto_index_scalar_extend_resultentries) = (S l)) -> exists sto_input_scalar_extend_resultentries sto_output_scalar_extend_resultentries. ((exists dst_positive_code_scalar_extend_resultentriesentryinput dst_positive_scale_scalar_extend_resultentriesentryinput dst_negative_code_scalar_extend_resultentriesentryinput dst_negative_scale_scalar_extend_resultentriesentryinput dst_positive_scalar_extend_resultentriesentryinput dst_negative_scalar_extend_resultentriesentryinput. (((F) = (((((dst_positive_code_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput)) * S ((dst_positive_code_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput)) + ((dst_positive_scale_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput))) + (((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) * S ((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) + ((dst_negative_scale_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)))) * S ((((dst_positive_code_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput)) * S ((dst_positive_code_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput)) + ((dst_positive_scale_scalar_extend_resultentriesentryinput) + (dst_positive_scale_scalar_extend_resultentriesentryinput))) + (((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) * S ((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) + ((dst_negative_scale_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)))) + ((((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) * S ((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) + ((dst_negative_scale_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput))) + (((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) * S ((dst_negative_code_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)) + ((dst_negative_scale_scalar_extend_resultentriesentryinput) + (dst_negative_scale_scalar_extend_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_scalar_extend_resultentriesentryinputpositive. ff_h_pvs_scalar_extend_resultentriesentryinputpositive + S (dst_positive_scalar_extend_resultentriesentryinput) = S ((S (sto_index_scalar_extend_resultentries)) * dst_positive_scale_scalar_extend_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_extend_resultentriesentryinputpositive. dst_positive_code_scalar_extend_resultentriesentryinput = ff_q_pvs_scalar_extend_resultentriesentryinputpositive * S ((S (sto_index_scalar_extend_resultentries)) * dst_positive_scale_scalar_extend_resultentriesentryinput) + (dst_positive_scalar_extend_resultentriesentryinput))) /\ (((((exists ff_h_pvs_scalar_extend_resultentriesentryinputnegative. ff_h_pvs_scalar_extend_resultentriesentryinputnegative + S (dst_negative_scalar_extend_resultentriesentryinput) = S ((S (sto_index_scalar_extend_resultentries)) * dst_negative_scale_scalar_extend_resultentriesentryinput)) /\ exists ff_q_pvs_scalar_extend_resultentriesentryinputnegative. dst_negative_code_scalar_extend_resultentriesentryinput = ff_q_pvs_scalar_extend_resultentriesentryinputnegative * S ((S (sto_index_scalar_extend_resultentries)) * dst_negative_scale_scalar_extend_resultentriesentryinput) + (dst_negative_scalar_extend_resultentriesentryinput))) /\ (exists ge_balance_positive_scalar_extend_resultentriesentryinputvalue ge_balance_negative_scalar_extend_resultentriesentryinputvalue. (((((sto_input_scalar_extend_resultentries) = 2 * (ge_balance_positive_scalar_extend_resultentriesentryinputvalue) /\ (ge_balance_negative_scalar_extend_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_scalar_extend_resultentriesentryinputvaluedecode. (((sto_input_scalar_extend_resultentries) = 2 * ge_signed_half_scalar_extend_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_scalar_extend_resultentriesentryinputvalue) = S ge_signed_half_scalar_extend_resultentriesentryinputvaluedecode))) /\ ((dst_positive_scalar_extend_resultentriesentryinput) + ge_balance_negative_scalar_extend_resultentriesentryinputvalue = (dst_negative_scalar_extend_resultentriesentryinput) + ge_balance_positive_scalar_extend_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_scalar_extend_resultentriesentryoutput dst_positive_scale_scalar_extend_resultentriesentryoutput dst_negative_code_scalar_extend_resultentriesentryoutput dst_negative_scale_scalar_extend_resultentriesentryoutput dst_positive_scalar_extend_resultentriesentryoutput dst_negative_scalar_extend_resultentriesentryoutput. (((K) = (((((dst_positive_code_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_positive_code_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput)) + ((dst_positive_scale_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput))) + (((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) + ((dst_negative_scale_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)))) * S ((((dst_positive_code_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_positive_code_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput)) + ((dst_positive_scale_scalar_extend_resultentriesentryoutput) + (dst_positive_scale_scalar_extend_resultentriesentryoutput))) + (((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) + ((dst_negative_scale_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)))) + ((((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) + ((dst_negative_scale_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput))) + (((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) * S ((dst_negative_code_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)) + ((dst_negative_scale_scalar_extend_resultentriesentryoutput) + (dst_negative_scale_scalar_extend_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_scalar_extend_resultentriesentryoutputpositive. ff_h_pvs_scalar_extend_resultentriesentryoutputpositive + S (dst_positive_scalar_extend_resultentriesentryoutput) = S ((S (sto_index_scalar_extend_resultentries)) * dst_positive_scale_scalar_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_extend_resultentriesentryoutputpositive. dst_positive_code_scalar_extend_resultentriesentryoutput = ff_q_pvs_scalar_extend_resultentriesentryoutputpositive * S ((S (sto_index_scalar_extend_resultentries)) * dst_positive_scale_scalar_extend_resultentriesentryoutput) + (dst_positive_scalar_extend_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_scalar_extend_resultentriesentryoutputnegative. ff_h_pvs_scalar_extend_resultentriesentryoutputnegative + S (dst_negative_scalar_extend_resultentriesentryoutput) = S ((S (sto_index_scalar_extend_resultentries)) * dst_negative_scale_scalar_extend_resultentriesentryoutput)) /\ exists ff_q_pvs_scalar_extend_resultentriesentryoutputnegative. dst_negative_code_scalar_extend_resultentriesentryoutput = ff_q_pvs_scalar_extend_resultentriesentryoutputnegative * S ((S (sto_index_scalar_extend_resultentries)) * dst_negative_scale_scalar_extend_resultentriesentryoutput) + (dst_negative_scalar_extend_resultentriesentryoutput))) /\ (exists ge_balance_positive_scalar_extend_resultentriesentryoutputvalue ge_balance_negative_scalar_extend_resultentriesentryoutputvalue. (((((sto_output_scalar_extend_resultentries) = 2 * (ge_balance_positive_scalar_extend_resultentriesentryoutputvalue) /\ (ge_balance_negative_scalar_extend_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_scalar_extend_resultentriesentryoutputvaluedecode. (((sto_output_scalar_extend_resultentries) = 2 * ge_signed_half_scalar_extend_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_scalar_extend_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_scalar_extend_resultentriesentryoutputvalue) = S ge_signed_half_scalar_extend_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_scalar_extend_resultentriesentryoutput) + ge_balance_negative_scalar_extend_resultentriesentryoutputvalue = (dst_negative_scalar_extend_resultentriesentryoutput) + ge_balance_positive_scalar_extend_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_scalar_extend_resultentriesentryoperation sto_an_scalar_extend_resultentriesentryoperation sto_bp_scalar_extend_resultentriesentryoperation sto_bn_scalar_extend_resultentriesentryoperation sto_cp_scalar_extend_resultentriesentryoperation sto_cn_scalar_extend_resultentriesentryoperation. (((((a) = 2 * (sto_ap_scalar_extend_resultentriesentryoperation) /\ (sto_an_scalar_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_resultentriesentryoperationleft. (((a) = 2 * ge_signed_half_scalar_extend_resultentriesentryoperationleft + 1 /\ (sto_ap_scalar_extend_resultentriesentryoperation) = 0) /\ (sto_an_scalar_extend_resultentriesentryoperation) = S ge_signed_half_scalar_extend_resultentriesentryoperationleft))) /\ ((((((sto_input_scalar_extend_resultentries) = 2 * (sto_bp_scalar_extend_resultentriesentryoperation) /\ (sto_bn_scalar_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_resultentriesentryoperationright. (((sto_input_scalar_extend_resultentries) = 2 * ge_signed_half_scalar_extend_resultentriesentryoperationright + 1 /\ (sto_bp_scalar_extend_resultentriesentryoperation) = 0) /\ (sto_bn_scalar_extend_resultentriesentryoperation) = S ge_signed_half_scalar_extend_resultentriesentryoperationright))) /\ ((((((sto_output_scalar_extend_resultentries) = 2 * (sto_cp_scalar_extend_resultentriesentryoperation) /\ (sto_cn_scalar_extend_resultentriesentryoperation) = 0) \/ exists ge_signed_half_scalar_extend_resultentriesentryoperationoutput. (((sto_output_scalar_extend_resultentries) = 2 * ge_signed_half_scalar_extend_resultentriesentryoperationoutput + 1 /\ (sto_cp_scalar_extend_resultentriesentryoperation) = 0) /\ (sto_cn_scalar_extend_resultentriesentryoperation) = S ge_signed_half_scalar_extend_resultentriesentryoperationoutput))) /\ ((sto_ap_scalar_extend_resultentriesentryoperation * sto_bp_scalar_extend_resultentriesentryoperation + sto_an_scalar_extend_resultentriesentryoperation * sto_bn_scalar_extend_resultentriesentryoperation) + sto_cn_scalar_extend_resultentriesentryoperation = (sto_ap_scalar_extend_resultentriesentryoperation * sto_bn_scalar_extend_resultentriesentryoperation + sto_an_scalar_extend_resultentriesentryoperation * sto_bp_scalar_extend_resultentriesentryoperation) + sto_cp_scalar_extend_resultentriesentryoperation)))))))))))))))