signed_rectangular_slice_extend

Exact expanded first-order arithmetic statement

forall F G H o s l a. (((exists dst_positive_code_extend_prefixsource_table dst_positive_scale_extend_prefixsource_table dst_negative_code_extend_prefixsource_table dst_negative_scale_extend_prefixsource_table. (((F) = (((((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) * S ((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) + ((dst_positive_scale_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))) * S ((((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) * S ((dst_positive_code_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table)) + ((dst_positive_scale_extend_prefixsource_table) + (dst_positive_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))) + ((((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table))) + (((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) * S ((dst_negative_code_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)) + ((dst_negative_scale_extend_prefixsource_table) + (dst_negative_scale_extend_prefixsource_table)))))) /\ (forall dst_index_extend_prefixsource_table. (exists pvs_le_gap_extend_prefixsource_tabledomain. pvs_le_gap_extend_prefixsource_tabledomain + (dst_index_extend_prefixsource_table) = (0)) -> exists dst_positive_extend_prefixsource_table dst_negative_extend_prefixsource_table dst_value_extend_prefixsource_table. ((((exists ff_h_pvs_extend_prefixsource_tableentrypositive. ff_h_pvs_extend_prefixsource_tableentrypositive + S (dst_positive_extend_prefixsource_table) = S ((S (dst_index_extend_prefixsource_table)) * dst_positive_scale_extend_prefixsource_table)) /\ exists ff_q_pvs_extend_prefixsource_tableentrypositive. dst_positive_code_extend_prefixsource_table = ff_q_pvs_extend_prefixsource_tableentrypositive * S ((S (dst_index_extend_prefixsource_table)) * dst_positive_scale_extend_prefixsource_table) + (dst_positive_extend_prefixsource_table))) /\ (((((exists ff_h_pvs_extend_prefixsource_tableentrynegative. ff_h_pvs_extend_prefixsource_tableentrynegative + S (dst_negative_extend_prefixsource_table) = S ((S (dst_index_extend_prefixsource_table)) * dst_negative_scale_extend_prefixsource_table)) /\ exists ff_q_pvs_extend_prefixsource_tableentrynegative. dst_negative_code_extend_prefixsource_table = ff_q_pvs_extend_prefixsource_tableentrynegative * S ((S (dst_index_extend_prefixsource_table)) * dst_negative_scale_extend_prefixsource_table) + (dst_negative_extend_prefixsource_table))) /\ (exists ge_balance_positive_extend_prefixsource_tableentryvalue ge_balance_negative_extend_prefixsource_tableentryvalue. (((((dst_value_extend_prefixsource_table) = 2 * (ge_balance_positive_extend_prefixsource_tableentryvalue) /\ (ge_balance_negative_extend_prefixsource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixsource_tableentryvaluedecode. (((dst_value_extend_prefixsource_table) = 2 * ge_signed_half_extend_prefixsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixsource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixsource_tableentryvalue) = S ge_signed_half_extend_prefixsource_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixsource_table) + ge_balance_negative_extend_prefixsource_tableentryvalue = (dst_negative_extend_prefixsource_table) + ge_balance_positive_extend_prefixsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_prefixoutput_table dst_positive_scale_extend_prefixoutput_table dst_negative_code_extend_prefixoutput_table dst_negative_scale_extend_prefixoutput_table. (((G) = (((((dst_positive_code_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table)) * S ((dst_positive_code_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table)) + ((dst_positive_scale_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table))) + (((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) * S ((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) + ((dst_negative_scale_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)))) * S ((((dst_positive_code_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table)) * S ((dst_positive_code_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table)) + ((dst_positive_scale_extend_prefixoutput_table) + (dst_positive_scale_extend_prefixoutput_table))) + (((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) * S ((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) + ((dst_negative_scale_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)))) + ((((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) * S ((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) + ((dst_negative_scale_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table))) + (((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) * S ((dst_negative_code_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)) + ((dst_negative_scale_extend_prefixoutput_table) + (dst_negative_scale_extend_prefixoutput_table)))))) /\ (forall dst_index_extend_prefixoutput_table. (exists pvs_le_gap_extend_prefixoutput_tabledomain. pvs_le_gap_extend_prefixoutput_tabledomain + (dst_index_extend_prefixoutput_table) = (l)) -> exists dst_positive_extend_prefixoutput_table dst_negative_extend_prefixoutput_table dst_value_extend_prefixoutput_table. ((((exists ff_h_pvs_extend_prefixoutput_tableentrypositive. ff_h_pvs_extend_prefixoutput_tableentrypositive + S (dst_positive_extend_prefixoutput_table) = S ((S (dst_index_extend_prefixoutput_table)) * dst_positive_scale_extend_prefixoutput_table)) /\ exists ff_q_pvs_extend_prefixoutput_tableentrypositive. dst_positive_code_extend_prefixoutput_table = ff_q_pvs_extend_prefixoutput_tableentrypositive * S ((S (dst_index_extend_prefixoutput_table)) * dst_positive_scale_extend_prefixoutput_table) + (dst_positive_extend_prefixoutput_table))) /\ (((((exists ff_h_pvs_extend_prefixoutput_tableentrynegative. ff_h_pvs_extend_prefixoutput_tableentrynegative + S (dst_negative_extend_prefixoutput_table) = S ((S (dst_index_extend_prefixoutput_table)) * dst_negative_scale_extend_prefixoutput_table)) /\ exists ff_q_pvs_extend_prefixoutput_tableentrynegative. dst_negative_code_extend_prefixoutput_table = ff_q_pvs_extend_prefixoutput_tableentrynegative * S ((S (dst_index_extend_prefixoutput_table)) * dst_negative_scale_extend_prefixoutput_table) + (dst_negative_extend_prefixoutput_table))) /\ (exists ge_balance_positive_extend_prefixoutput_tableentryvalue ge_balance_negative_extend_prefixoutput_tableentryvalue. (((((dst_value_extend_prefixoutput_table) = 2 * (ge_balance_positive_extend_prefixoutput_tableentryvalue) /\ (ge_balance_negative_extend_prefixoutput_tableentryvalue) = 0) \/ exists ge_signed_half_extend_prefixoutput_tableentryvaluedecode. (((dst_value_extend_prefixoutput_table) = 2 * ge_signed_half_extend_prefixoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_prefixoutput_tableentryvalue) = 0) /\ (ge_balance_negative_extend_prefixoutput_tableentryvalue) = S ge_signed_half_extend_prefixoutput_tableentryvaluedecode))) /\ ((dst_positive_extend_prefixoutput_table) + ge_balance_negative_extend_prefixoutput_tableentryvalue = (dst_negative_extend_prefixoutput_table) + ge_balance_positive_extend_prefixoutput_tableentryvalue))))))))) /\ (forall srs_index_extend_prefix. (exists pvs_gap_extend_prefixbound. pvs_gap_extend_prefixbound + S (srs_index_extend_prefix) = (l)) -> exists srs_value_extend_prefix. (((exists dst_positive_code_extend_prefixentrysource dst_positive_scale_extend_prefixentrysource dst_negative_code_extend_prefixentrysource dst_negative_scale_extend_prefixentrysource dst_positive_extend_prefixentrysource dst_negative_extend_prefixentrysource. (((F) = (((((dst_positive_code_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource)) * S ((dst_positive_code_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource)) + ((dst_positive_scale_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource))) + (((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) * S ((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) + ((dst_negative_scale_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)))) * S ((((dst_positive_code_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource)) * S ((dst_positive_code_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource)) + ((dst_positive_scale_extend_prefixentrysource) + (dst_positive_scale_extend_prefixentrysource))) + (((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) * S ((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) + ((dst_negative_scale_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)))) + ((((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) * S ((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) + ((dst_negative_scale_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource))) + (((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) * S ((dst_negative_code_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)) + ((dst_negative_scale_extend_prefixentrysource) + (dst_negative_scale_extend_prefixentrysource)))))) /\ (((((exists ff_h_pvs_extend_prefixentrysourcepositive. ff_h_pvs_extend_prefixentrysourcepositive + S (dst_positive_extend_prefixentrysource) = S ((S (((o) + ((s) * (srs_index_extend_prefix))))) * dst_positive_scale_extend_prefixentrysource)) /\ exists ff_q_pvs_extend_prefixentrysourcepositive. dst_positive_code_extend_prefixentrysource = ff_q_pvs_extend_prefixentrysourcepositive * S ((S (((o) + ((s) * (srs_index_extend_prefix))))) * dst_positive_scale_extend_prefixentrysource) + (dst_positive_extend_prefixentrysource))) /\ (((((exists ff_h_pvs_extend_prefixentrysourcenegative. ff_h_pvs_extend_prefixentrysourcenegative + S (dst_negative_extend_prefixentrysource) = S ((S (((o) + ((s) * (srs_index_extend_prefix))))) * dst_negative_scale_extend_prefixentrysource)) /\ exists ff_q_pvs_extend_prefixentrysourcenegative. dst_negative_code_extend_prefixentrysource = ff_q_pvs_extend_prefixentrysourcenegative * S ((S (((o) + ((s) * (srs_index_extend_prefix))))) * dst_negative_scale_extend_prefixentrysource) + (dst_negative_extend_prefixentrysource))) /\ (exists ge_balance_positive_extend_prefixentrysourcevalue ge_balance_negative_extend_prefixentrysourcevalue. (((((srs_value_extend_prefix) = 2 * (ge_balance_positive_extend_prefixentrysourcevalue) /\ (ge_balance_negative_extend_prefixentrysourcevalue) = 0) \/ exists ge_signed_half_extend_prefixentrysourcevaluedecode. (((srs_value_extend_prefix) = 2 * ge_signed_half_extend_prefixentrysourcevaluedecode + 1 /\ (ge_balance_positive_extend_prefixentrysourcevalue) = 0) /\ (ge_balance_negative_extend_prefixentrysourcevalue) = S ge_signed_half_extend_prefixentrysourcevaluedecode))) /\ ((dst_positive_extend_prefixentrysource) + ge_balance_negative_extend_prefixentrysourcevalue = (dst_negative_extend_prefixentrysource) + ge_balance_positive_extend_prefixentrysourcevalue))))))))) /\ (exists dst_positive_code_extend_prefixentryoutput dst_positive_scale_extend_prefixentryoutput dst_negative_code_extend_prefixentryoutput dst_negative_scale_extend_prefixentryoutput dst_positive_extend_prefixentryoutput dst_negative_extend_prefixentryoutput. (((G) = (((((dst_positive_code_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput)) * S ((dst_positive_code_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput)) + ((dst_positive_scale_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput))) + (((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) * S ((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) + ((dst_negative_scale_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)))) * S ((((dst_positive_code_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput)) * S ((dst_positive_code_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput)) + ((dst_positive_scale_extend_prefixentryoutput) + (dst_positive_scale_extend_prefixentryoutput))) + (((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) * S ((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) + ((dst_negative_scale_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)))) + ((((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) * S ((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) + ((dst_negative_scale_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput))) + (((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) * S ((dst_negative_code_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)) + ((dst_negative_scale_extend_prefixentryoutput) + (dst_negative_scale_extend_prefixentryoutput)))))) /\ (((((exists ff_h_pvs_extend_prefixentryoutputpositive. ff_h_pvs_extend_prefixentryoutputpositive + S (dst_positive_extend_prefixentryoutput) = S ((S (srs_index_extend_prefix)) * dst_positive_scale_extend_prefixentryoutput)) /\ exists ff_q_pvs_extend_prefixentryoutputpositive. dst_positive_code_extend_prefixentryoutput = ff_q_pvs_extend_prefixentryoutputpositive * S ((S (srs_index_extend_prefix)) * dst_positive_scale_extend_prefixentryoutput) + (dst_positive_extend_prefixentryoutput))) /\ (((((exists ff_h_pvs_extend_prefixentryoutputnegative. ff_h_pvs_extend_prefixentryoutputnegative + S (dst_negative_extend_prefixentryoutput) = S ((S (srs_index_extend_prefix)) * dst_negative_scale_extend_prefixentryoutput)) /\ exists ff_q_pvs_extend_prefixentryoutputnegative. dst_negative_code_extend_prefixentryoutput = ff_q_pvs_extend_prefixentryoutputnegative * S ((S (srs_index_extend_prefix)) * dst_negative_scale_extend_prefixentryoutput) + (dst_negative_extend_prefixentryoutput))) /\ (exists ge_balance_positive_extend_prefixentryoutputvalue ge_balance_negative_extend_prefixentryoutputvalue. (((((srs_value_extend_prefix) = 2 * (ge_balance_positive_extend_prefixentryoutputvalue) /\ (ge_balance_negative_extend_prefixentryoutputvalue) = 0) \/ exists ge_signed_half_extend_prefixentryoutputvaluedecode. (((srs_value_extend_prefix) = 2 * ge_signed_half_extend_prefixentryoutputvaluedecode + 1 /\ (ge_balance_positive_extend_prefixentryoutputvalue) = 0) /\ (ge_balance_negative_extend_prefixentryoutputvalue) = S ge_signed_half_extend_prefixentryoutputvaluedecode))) /\ ((dst_positive_extend_prefixentryoutput) + ge_balance_negative_extend_prefixentryoutputvalue = (dst_negative_extend_prefixentryoutput) + ge_balance_positive_extend_prefixentryoutputvalue)))))))))))))))) -> (exists dst_positive_code_extend_table dst_positive_scale_extend_table dst_negative_code_extend_table dst_negative_scale_extend_table. (((H) = (((((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) * S ((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) + ((dst_positive_scale_extend_table) + (dst_positive_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))) * S ((((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) * S ((dst_positive_code_extend_table) + (dst_positive_scale_extend_table)) + ((dst_positive_scale_extend_table) + (dst_positive_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))) + ((((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table))) + (((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) * S ((dst_negative_code_extend_table) + (dst_negative_scale_extend_table)) + ((dst_negative_scale_extend_table) + (dst_negative_scale_extend_table)))))) /\ (forall dst_index_extend_table. (exists pvs_le_gap_extend_tabledomain. pvs_le_gap_extend_tabledomain + (dst_index_extend_table) = (l)) -> exists dst_positive_extend_table dst_negative_extend_table dst_value_extend_table. ((((exists ff_h_pvs_extend_tableentrypositive. ff_h_pvs_extend_tableentrypositive + S (dst_positive_extend_table) = S ((S (dst_index_extend_table)) * dst_positive_scale_extend_table)) /\ exists ff_q_pvs_extend_tableentrypositive. dst_positive_code_extend_table = ff_q_pvs_extend_tableentrypositive * S ((S (dst_index_extend_table)) * dst_positive_scale_extend_table) + (dst_positive_extend_table))) /\ (((((exists ff_h_pvs_extend_tableentrynegative. ff_h_pvs_extend_tableentrynegative + S (dst_negative_extend_table) = S ((S (dst_index_extend_table)) * dst_negative_scale_extend_table)) /\ exists ff_q_pvs_extend_tableentrynegative. dst_negative_code_extend_table = ff_q_pvs_extend_tableentrynegative * S ((S (dst_index_extend_table)) * dst_negative_scale_extend_table) + (dst_negative_extend_table))) /\ (exists ge_balance_positive_extend_tableentryvalue ge_balance_negative_extend_tableentryvalue. (((((dst_value_extend_table) = 2 * (ge_balance_positive_extend_tableentryvalue) /\ (ge_balance_negative_extend_tableentryvalue) = 0) \/ exists ge_signed_half_extend_tableentryvaluedecode. (((dst_value_extend_table) = 2 * ge_signed_half_extend_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_tableentryvalue) = 0) /\ (ge_balance_negative_extend_tableentryvalue) = S ge_signed_half_extend_tableentryvaluedecode))) /\ ((dst_positive_extend_table) + ge_balance_negative_extend_tableentryvalue = (dst_negative_extend_table) + ge_balance_positive_extend_tableentryvalue))))))))) -> (forall dst_index_extend_preserved dst_first_extend_preserved dst_second_extend_preserved. (exists pvs_gap_extend_preservedbound. pvs_gap_extend_preservedbound + S (dst_index_extend_preserved) = (l)) -> (exists dst_positive_code_extend_preservedfirst dst_positive_scale_extend_preservedfirst dst_negative_code_extend_preservedfirst dst_negative_scale_extend_preservedfirst dst_positive_extend_preservedfirst dst_negative_extend_preservedfirst. (((G) = (((((dst_positive_code_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst)) * S ((dst_positive_code_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst)) + ((dst_positive_scale_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst))) + (((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) * S ((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) + ((dst_negative_scale_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)))) * S ((((dst_positive_code_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst)) * S ((dst_positive_code_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst)) + ((dst_positive_scale_extend_preservedfirst) + (dst_positive_scale_extend_preservedfirst))) + (((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) * S ((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) + ((dst_negative_scale_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)))) + ((((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) * S ((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) + ((dst_negative_scale_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst))) + (((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) * S ((dst_negative_code_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)) + ((dst_negative_scale_extend_preservedfirst) + (dst_negative_scale_extend_preservedfirst)))))) /\ (((((exists ff_h_pvs_extend_preservedfirstpositive. ff_h_pvs_extend_preservedfirstpositive + S (dst_positive_extend_preservedfirst) = S ((S (dst_index_extend_preserved)) * dst_positive_scale_extend_preservedfirst)) /\ exists ff_q_pvs_extend_preservedfirstpositive. dst_positive_code_extend_preservedfirst = ff_q_pvs_extend_preservedfirstpositive * S ((S (dst_index_extend_preserved)) * dst_positive_scale_extend_preservedfirst) + (dst_positive_extend_preservedfirst))) /\ (((((exists ff_h_pvs_extend_preservedfirstnegative. ff_h_pvs_extend_preservedfirstnegative + S (dst_negative_extend_preservedfirst) = S ((S (dst_index_extend_preserved)) * dst_negative_scale_extend_preservedfirst)) /\ exists ff_q_pvs_extend_preservedfirstnegative. dst_negative_code_extend_preservedfirst = ff_q_pvs_extend_preservedfirstnegative * S ((S (dst_index_extend_preserved)) * dst_negative_scale_extend_preservedfirst) + (dst_negative_extend_preservedfirst))) /\ (exists ge_balance_positive_extend_preservedfirstvalue ge_balance_negative_extend_preservedfirstvalue. (((((dst_first_extend_preserved) = 2 * (ge_balance_positive_extend_preservedfirstvalue) /\ (ge_balance_negative_extend_preservedfirstvalue) = 0) \/ exists ge_signed_half_extend_preservedfirstvaluedecode. (((dst_first_extend_preserved) = 2 * ge_signed_half_extend_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_extend_preservedfirstvalue) = 0) /\ (ge_balance_negative_extend_preservedfirstvalue) = S ge_signed_half_extend_preservedfirstvaluedecode))) /\ ((dst_positive_extend_preservedfirst) + ge_balance_negative_extend_preservedfirstvalue = (dst_negative_extend_preservedfirst) + ge_balance_positive_extend_preservedfirstvalue))))))))) -> (exists dst_positive_code_extend_preservedsecond dst_positive_scale_extend_preservedsecond dst_negative_code_extend_preservedsecond dst_negative_scale_extend_preservedsecond dst_positive_extend_preservedsecond dst_negative_extend_preservedsecond. (((H) = (((((dst_positive_code_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond)) * S ((dst_positive_code_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond)) + ((dst_positive_scale_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond))) + (((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) * S ((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) + ((dst_negative_scale_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)))) * S ((((dst_positive_code_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond)) * S ((dst_positive_code_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond)) + ((dst_positive_scale_extend_preservedsecond) + (dst_positive_scale_extend_preservedsecond))) + (((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) * S ((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) + ((dst_negative_scale_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)))) + ((((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) * S ((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) + ((dst_negative_scale_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond))) + (((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) * S ((dst_negative_code_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)) + ((dst_negative_scale_extend_preservedsecond) + (dst_negative_scale_extend_preservedsecond)))))) /\ (((((exists ff_h_pvs_extend_preservedsecondpositive. ff_h_pvs_extend_preservedsecondpositive + S (dst_positive_extend_preservedsecond) = S ((S (dst_index_extend_preserved)) * dst_positive_scale_extend_preservedsecond)) /\ exists ff_q_pvs_extend_preservedsecondpositive. dst_positive_code_extend_preservedsecond = ff_q_pvs_extend_preservedsecondpositive * S ((S (dst_index_extend_preserved)) * dst_positive_scale_extend_preservedsecond) + (dst_positive_extend_preservedsecond))) /\ (((((exists ff_h_pvs_extend_preservedsecondnegative. ff_h_pvs_extend_preservedsecondnegative + S (dst_negative_extend_preservedsecond) = S ((S (dst_index_extend_preserved)) * dst_negative_scale_extend_preservedsecond)) /\ exists ff_q_pvs_extend_preservedsecondnegative. dst_negative_code_extend_preservedsecond = ff_q_pvs_extend_preservedsecondnegative * S ((S (dst_index_extend_preserved)) * dst_negative_scale_extend_preservedsecond) + (dst_negative_extend_preservedsecond))) /\ (exists ge_balance_positive_extend_preservedsecondvalue ge_balance_negative_extend_preservedsecondvalue. (((((dst_second_extend_preserved) = 2 * (ge_balance_positive_extend_preservedsecondvalue) /\ (ge_balance_negative_extend_preservedsecondvalue) = 0) \/ exists ge_signed_half_extend_preservedsecondvaluedecode. (((dst_second_extend_preserved) = 2 * ge_signed_half_extend_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_extend_preservedsecondvalue) = 0) /\ (ge_balance_negative_extend_preservedsecondvalue) = S ge_signed_half_extend_preservedsecondvaluedecode))) /\ ((dst_positive_extend_preservedsecond) + ge_balance_negative_extend_preservedsecondvalue = (dst_negative_extend_preservedsecond) + ge_balance_positive_extend_preservedsecondvalue))))))))) -> dst_first_extend_preserved = dst_second_extend_preserved) -> (exists dst_positive_code_extend_source dst_positive_scale_extend_source dst_negative_code_extend_source dst_negative_scale_extend_source dst_positive_extend_source dst_negative_extend_source. (((F) = (((((dst_positive_code_extend_source) + (dst_positive_scale_extend_source)) * S ((dst_positive_code_extend_source) + (dst_positive_scale_extend_source)) + ((dst_positive_scale_extend_source) + (dst_positive_scale_extend_source))) + (((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) * S ((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) + ((dst_negative_scale_extend_source) + (dst_negative_scale_extend_source)))) * S ((((dst_positive_code_extend_source) + (dst_positive_scale_extend_source)) * S ((dst_positive_code_extend_source) + (dst_positive_scale_extend_source)) + ((dst_positive_scale_extend_source) + (dst_positive_scale_extend_source))) + (((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) * S ((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) + ((dst_negative_scale_extend_source) + (dst_negative_scale_extend_source)))) + ((((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) * S ((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) + ((dst_negative_scale_extend_source) + (dst_negative_scale_extend_source))) + (((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) * S ((dst_negative_code_extend_source) + (dst_negative_scale_extend_source)) + ((dst_negative_scale_extend_source) + (dst_negative_scale_extend_source)))))) /\ (((((exists ff_h_pvs_extend_sourcepositive. ff_h_pvs_extend_sourcepositive + S (dst_positive_extend_source) = S ((S (((o) + ((s) * (l))))) * dst_positive_scale_extend_source)) /\ exists ff_q_pvs_extend_sourcepositive. dst_positive_code_extend_source = ff_q_pvs_extend_sourcepositive * S ((S (((o) + ((s) * (l))))) * dst_positive_scale_extend_source) + (dst_positive_extend_source))) /\ (((((exists ff_h_pvs_extend_sourcenegative. ff_h_pvs_extend_sourcenegative + S (dst_negative_extend_source) = S ((S (((o) + ((s) * (l))))) * dst_negative_scale_extend_source)) /\ exists ff_q_pvs_extend_sourcenegative. dst_negative_code_extend_source = ff_q_pvs_extend_sourcenegative * S ((S (((o) + ((s) * (l))))) * dst_negative_scale_extend_source) + (dst_negative_extend_source))) /\ (exists ge_balance_positive_extend_sourcevalue ge_balance_negative_extend_sourcevalue. (((((a) = 2 * (ge_balance_positive_extend_sourcevalue) /\ (ge_balance_negative_extend_sourcevalue) = 0) \/ exists ge_signed_half_extend_sourcevaluedecode. (((a) = 2 * ge_signed_half_extend_sourcevaluedecode + 1 /\ (ge_balance_positive_extend_sourcevalue) = 0) /\ (ge_balance_negative_extend_sourcevalue) = S ge_signed_half_extend_sourcevaluedecode))) /\ ((dst_positive_extend_source) + ge_balance_negative_extend_sourcevalue = (dst_negative_extend_source) + ge_balance_positive_extend_sourcevalue))))))))) -> (exists dst_positive_code_extend_value dst_positive_scale_extend_value dst_negative_code_extend_value dst_negative_scale_extend_value dst_positive_extend_value dst_negative_extend_value. (((H) = (((((dst_positive_code_extend_value) + (dst_positive_scale_extend_value)) * S ((dst_positive_code_extend_value) + (dst_positive_scale_extend_value)) + ((dst_positive_scale_extend_value) + (dst_positive_scale_extend_value))) + (((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) * S ((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) + ((dst_negative_scale_extend_value) + (dst_negative_scale_extend_value)))) * S ((((dst_positive_code_extend_value) + (dst_positive_scale_extend_value)) * S ((dst_positive_code_extend_value) + (dst_positive_scale_extend_value)) + ((dst_positive_scale_extend_value) + (dst_positive_scale_extend_value))) + (((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) * S ((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) + ((dst_negative_scale_extend_value) + (dst_negative_scale_extend_value)))) + ((((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) * S ((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) + ((dst_negative_scale_extend_value) + (dst_negative_scale_extend_value))) + (((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) * S ((dst_negative_code_extend_value) + (dst_negative_scale_extend_value)) + ((dst_negative_scale_extend_value) + (dst_negative_scale_extend_value)))))) /\ (((((exists ff_h_pvs_extend_valuepositive. ff_h_pvs_extend_valuepositive + S (dst_positive_extend_value) = S ((S (l)) * dst_positive_scale_extend_value)) /\ exists ff_q_pvs_extend_valuepositive. dst_positive_code_extend_value = ff_q_pvs_extend_valuepositive * S ((S (l)) * dst_positive_scale_extend_value) + (dst_positive_extend_value))) /\ (((((exists ff_h_pvs_extend_valuenegative. ff_h_pvs_extend_valuenegative + S (dst_negative_extend_value) = S ((S (l)) * dst_negative_scale_extend_value)) /\ exists ff_q_pvs_extend_valuenegative. dst_negative_code_extend_value = ff_q_pvs_extend_valuenegative * S ((S (l)) * dst_negative_scale_extend_value) + (dst_negative_extend_value))) /\ (exists ge_balance_positive_extend_valuevalue ge_balance_negative_extend_valuevalue. (((((a) = 2 * (ge_balance_positive_extend_valuevalue) /\ (ge_balance_negative_extend_valuevalue) = 0) \/ exists ge_signed_half_extend_valuevaluedecode. (((a) = 2 * ge_signed_half_extend_valuevaluedecode + 1 /\ (ge_balance_positive_extend_valuevalue) = 0) /\ (ge_balance_negative_extend_valuevalue) = S ge_signed_half_extend_valuevaluedecode))) /\ ((dst_positive_extend_value) + ge_balance_negative_extend_valuevalue = (dst_negative_extend_value) + ge_balance_positive_extend_valuevalue))))))))) -> (((exists dst_positive_code_extend_resultsource_table dst_positive_scale_extend_resultsource_table dst_negative_code_extend_resultsource_table dst_negative_scale_extend_resultsource_table. (((F) = (((((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) * S ((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) + ((dst_positive_scale_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))) * S ((((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) * S ((dst_positive_code_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table)) + ((dst_positive_scale_extend_resultsource_table) + (dst_positive_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))) + ((((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table))) + (((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) * S ((dst_negative_code_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)) + ((dst_negative_scale_extend_resultsource_table) + (dst_negative_scale_extend_resultsource_table)))))) /\ (forall dst_index_extend_resultsource_table. (exists pvs_le_gap_extend_resultsource_tabledomain. pvs_le_gap_extend_resultsource_tabledomain + (dst_index_extend_resultsource_table) = (0)) -> exists dst_positive_extend_resultsource_table dst_negative_extend_resultsource_table dst_value_extend_resultsource_table. ((((exists ff_h_pvs_extend_resultsource_tableentrypositive. ff_h_pvs_extend_resultsource_tableentrypositive + S (dst_positive_extend_resultsource_table) = S ((S (dst_index_extend_resultsource_table)) * dst_positive_scale_extend_resultsource_table)) /\ exists ff_q_pvs_extend_resultsource_tableentrypositive. dst_positive_code_extend_resultsource_table = ff_q_pvs_extend_resultsource_tableentrypositive * S ((S (dst_index_extend_resultsource_table)) * dst_positive_scale_extend_resultsource_table) + (dst_positive_extend_resultsource_table))) /\ (((((exists ff_h_pvs_extend_resultsource_tableentrynegative. ff_h_pvs_extend_resultsource_tableentrynegative + S (dst_negative_extend_resultsource_table) = S ((S (dst_index_extend_resultsource_table)) * dst_negative_scale_extend_resultsource_table)) /\ exists ff_q_pvs_extend_resultsource_tableentrynegative. dst_negative_code_extend_resultsource_table = ff_q_pvs_extend_resultsource_tableentrynegative * S ((S (dst_index_extend_resultsource_table)) * dst_negative_scale_extend_resultsource_table) + (dst_negative_extend_resultsource_table))) /\ (exists ge_balance_positive_extend_resultsource_tableentryvalue ge_balance_negative_extend_resultsource_tableentryvalue. (((((dst_value_extend_resultsource_table) = 2 * (ge_balance_positive_extend_resultsource_tableentryvalue) /\ (ge_balance_negative_extend_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultsource_tableentryvaluedecode. (((dst_value_extend_resultsource_table) = 2 * ge_signed_half_extend_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultsource_tableentryvalue) = S ge_signed_half_extend_resultsource_tableentryvaluedecode))) /\ ((dst_positive_extend_resultsource_table) + ge_balance_negative_extend_resultsource_tableentryvalue = (dst_negative_extend_resultsource_table) + ge_balance_positive_extend_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_extend_resultoutput_table dst_positive_scale_extend_resultoutput_table dst_negative_code_extend_resultoutput_table dst_negative_scale_extend_resultoutput_table. (((H) = (((((dst_positive_code_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table)) * S ((dst_positive_code_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table)) + ((dst_positive_scale_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table))) + (((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) * S ((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) + ((dst_negative_scale_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)))) * S ((((dst_positive_code_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table)) * S ((dst_positive_code_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table)) + ((dst_positive_scale_extend_resultoutput_table) + (dst_positive_scale_extend_resultoutput_table))) + (((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) * S ((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) + ((dst_negative_scale_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)))) + ((((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) * S ((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) + ((dst_negative_scale_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table))) + (((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) * S ((dst_negative_code_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)) + ((dst_negative_scale_extend_resultoutput_table) + (dst_negative_scale_extend_resultoutput_table)))))) /\ (forall dst_index_extend_resultoutput_table. (exists pvs_le_gap_extend_resultoutput_tabledomain. pvs_le_gap_extend_resultoutput_tabledomain + (dst_index_extend_resultoutput_table) = (S l)) -> exists dst_positive_extend_resultoutput_table dst_negative_extend_resultoutput_table dst_value_extend_resultoutput_table. ((((exists ff_h_pvs_extend_resultoutput_tableentrypositive. ff_h_pvs_extend_resultoutput_tableentrypositive + S (dst_positive_extend_resultoutput_table) = S ((S (dst_index_extend_resultoutput_table)) * dst_positive_scale_extend_resultoutput_table)) /\ exists ff_q_pvs_extend_resultoutput_tableentrypositive. dst_positive_code_extend_resultoutput_table = ff_q_pvs_extend_resultoutput_tableentrypositive * S ((S (dst_index_extend_resultoutput_table)) * dst_positive_scale_extend_resultoutput_table) + (dst_positive_extend_resultoutput_table))) /\ (((((exists ff_h_pvs_extend_resultoutput_tableentrynegative. ff_h_pvs_extend_resultoutput_tableentrynegative + S (dst_negative_extend_resultoutput_table) = S ((S (dst_index_extend_resultoutput_table)) * dst_negative_scale_extend_resultoutput_table)) /\ exists ff_q_pvs_extend_resultoutput_tableentrynegative. dst_negative_code_extend_resultoutput_table = ff_q_pvs_extend_resultoutput_tableentrynegative * S ((S (dst_index_extend_resultoutput_table)) * dst_negative_scale_extend_resultoutput_table) + (dst_negative_extend_resultoutput_table))) /\ (exists ge_balance_positive_extend_resultoutput_tableentryvalue ge_balance_negative_extend_resultoutput_tableentryvalue. (((((dst_value_extend_resultoutput_table) = 2 * (ge_balance_positive_extend_resultoutput_tableentryvalue) /\ (ge_balance_negative_extend_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_extend_resultoutput_tableentryvaluedecode. (((dst_value_extend_resultoutput_table) = 2 * ge_signed_half_extend_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_extend_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_extend_resultoutput_tableentryvalue) = S ge_signed_half_extend_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_extend_resultoutput_table) + ge_balance_negative_extend_resultoutput_tableentryvalue = (dst_negative_extend_resultoutput_table) + ge_balance_positive_extend_resultoutput_tableentryvalue))))))))) /\ (forall srs_index_extend_result. (exists pvs_gap_extend_resultbound. pvs_gap_extend_resultbound + S (srs_index_extend_result) = (S l)) -> exists srs_value_extend_result. (((exists dst_positive_code_extend_resultentrysource dst_positive_scale_extend_resultentrysource dst_negative_code_extend_resultentrysource dst_negative_scale_extend_resultentrysource dst_positive_extend_resultentrysource dst_negative_extend_resultentrysource. (((F) = (((((dst_positive_code_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource)) * S ((dst_positive_code_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource)) + ((dst_positive_scale_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource))) + (((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) * S ((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) + ((dst_negative_scale_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)))) * S ((((dst_positive_code_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource)) * S ((dst_positive_code_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource)) + ((dst_positive_scale_extend_resultentrysource) + (dst_positive_scale_extend_resultentrysource))) + (((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) * S ((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) + ((dst_negative_scale_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)))) + ((((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) * S ((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) + ((dst_negative_scale_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource))) + (((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) * S ((dst_negative_code_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)) + ((dst_negative_scale_extend_resultentrysource) + (dst_negative_scale_extend_resultentrysource)))))) /\ (((((exists ff_h_pvs_extend_resultentrysourcepositive. ff_h_pvs_extend_resultentrysourcepositive + S (dst_positive_extend_resultentrysource) = S ((S (((o) + ((s) * (srs_index_extend_result))))) * dst_positive_scale_extend_resultentrysource)) /\ exists ff_q_pvs_extend_resultentrysourcepositive. dst_positive_code_extend_resultentrysource = ff_q_pvs_extend_resultentrysourcepositive * S ((S (((o) + ((s) * (srs_index_extend_result))))) * dst_positive_scale_extend_resultentrysource) + (dst_positive_extend_resultentrysource))) /\ (((((exists ff_h_pvs_extend_resultentrysourcenegative. ff_h_pvs_extend_resultentrysourcenegative + S (dst_negative_extend_resultentrysource) = S ((S (((o) + ((s) * (srs_index_extend_result))))) * dst_negative_scale_extend_resultentrysource)) /\ exists ff_q_pvs_extend_resultentrysourcenegative. dst_negative_code_extend_resultentrysource = ff_q_pvs_extend_resultentrysourcenegative * S ((S (((o) + ((s) * (srs_index_extend_result))))) * dst_negative_scale_extend_resultentrysource) + (dst_negative_extend_resultentrysource))) /\ (exists ge_balance_positive_extend_resultentrysourcevalue ge_balance_negative_extend_resultentrysourcevalue. (((((srs_value_extend_result) = 2 * (ge_balance_positive_extend_resultentrysourcevalue) /\ (ge_balance_negative_extend_resultentrysourcevalue) = 0) \/ exists ge_signed_half_extend_resultentrysourcevaluedecode. (((srs_value_extend_result) = 2 * ge_signed_half_extend_resultentrysourcevaluedecode + 1 /\ (ge_balance_positive_extend_resultentrysourcevalue) = 0) /\ (ge_balance_negative_extend_resultentrysourcevalue) = S ge_signed_half_extend_resultentrysourcevaluedecode))) /\ ((dst_positive_extend_resultentrysource) + ge_balance_negative_extend_resultentrysourcevalue = (dst_negative_extend_resultentrysource) + ge_balance_positive_extend_resultentrysourcevalue))))))))) /\ (exists dst_positive_code_extend_resultentryoutput dst_positive_scale_extend_resultentryoutput dst_negative_code_extend_resultentryoutput dst_negative_scale_extend_resultentryoutput dst_positive_extend_resultentryoutput dst_negative_extend_resultentryoutput. (((H) = (((((dst_positive_code_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput)) * S ((dst_positive_code_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput)) + ((dst_positive_scale_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput))) + (((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) * S ((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) + ((dst_negative_scale_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)))) * S ((((dst_positive_code_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput)) * S ((dst_positive_code_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput)) + ((dst_positive_scale_extend_resultentryoutput) + (dst_positive_scale_extend_resultentryoutput))) + (((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) * S ((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) + ((dst_negative_scale_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)))) + ((((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) * S ((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) + ((dst_negative_scale_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput))) + (((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) * S ((dst_negative_code_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)) + ((dst_negative_scale_extend_resultentryoutput) + (dst_negative_scale_extend_resultentryoutput)))))) /\ (((((exists ff_h_pvs_extend_resultentryoutputpositive. ff_h_pvs_extend_resultentryoutputpositive + S (dst_positive_extend_resultentryoutput) = S ((S (srs_index_extend_result)) * dst_positive_scale_extend_resultentryoutput)) /\ exists ff_q_pvs_extend_resultentryoutputpositive. dst_positive_code_extend_resultentryoutput = ff_q_pvs_extend_resultentryoutputpositive * S ((S (srs_index_extend_result)) * dst_positive_scale_extend_resultentryoutput) + (dst_positive_extend_resultentryoutput))) /\ (((((exists ff_h_pvs_extend_resultentryoutputnegative. ff_h_pvs_extend_resultentryoutputnegative + S (dst_negative_extend_resultentryoutput) = S ((S (srs_index_extend_result)) * dst_negative_scale_extend_resultentryoutput)) /\ exists ff_q_pvs_extend_resultentryoutputnegative. dst_negative_code_extend_resultentryoutput = ff_q_pvs_extend_resultentryoutputnegative * S ((S (srs_index_extend_result)) * dst_negative_scale_extend_resultentryoutput) + (dst_negative_extend_resultentryoutput))) /\ (exists ge_balance_positive_extend_resultentryoutputvalue ge_balance_negative_extend_resultentryoutputvalue. (((((srs_value_extend_result) = 2 * (ge_balance_positive_extend_resultentryoutputvalue) /\ (ge_balance_negative_extend_resultentryoutputvalue) = 0) \/ exists ge_signed_half_extend_resultentryoutputvaluedecode. (((srs_value_extend_result) = 2 * ge_signed_half_extend_resultentryoutputvaluedecode + 1 /\ (ge_balance_positive_extend_resultentryoutputvalue) = 0) /\ (ge_balance_negative_extend_resultentryoutputvalue) = S ge_signed_half_extend_resultentryoutputvaluedecode))) /\ ((dst_positive_extend_resultentryoutput) + ge_balance_negative_extend_resultentryoutputvalue = (dst_negative_extend_resultentryoutput) + ge_balance_positive_extend_resultentryoutputvalue))))))))))))))))