signed_rectangular_slice_restrict

forall F G o s l. (((exists dst_positive_code_restrict_sourcesource_table dst_positive_scale_restrict_sourcesource_table dst_negative_code_restrict_sourcesource_table dst_negative_scale_restrict_sourcesource_table. (((F) = (((((dst_positive_code_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table)) * S ((dst_positive_code_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table)) + ((dst_positive_scale_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table))) + (((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) * S ((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) + ((dst_negative_scale_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)))) * S ((((dst_positive_code_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table)) * S ((dst_positive_code_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table)) + ((dst_positive_scale_restrict_sourcesource_table) + (dst_positive_scale_restrict_sourcesource_table))) + (((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) * S ((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) + ((dst_negative_scale_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)))) + ((((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) * S ((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) + ((dst_negative_scale_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table))) + (((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) * S ((dst_negative_code_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)) + ((dst_negative_scale_restrict_sourcesource_table) + (dst_negative_scale_restrict_sourcesource_table)))))) /\ (forall dst_index_restrict_sourcesource_table. (exists pvs_le_gap_restrict_sourcesource_tabledomain. pvs_le_gap_restrict_sourcesource_tabledomain + (dst_index_restrict_sourcesource_table) = (0)) -> exists dst_positive_restrict_sourcesource_table dst_negative_restrict_sourcesource_table dst_value_restrict_sourcesource_table. ((((exists ff_h_pvs_restrict_sourcesource_tableentrypositive. ff_h_pvs_restrict_sourcesource_tableentrypositive + S (dst_positive_restrict_sourcesource_table) = S ((S (dst_index_restrict_sourcesource_table)) * dst_positive_scale_restrict_sourcesource_table)) /\ exists ff_q_pvs_restrict_sourcesource_tableentrypositive. dst_positive_code_restrict_sourcesource_table = ff_q_pvs_restrict_sourcesource_tableentrypositive * S ((S (dst_index_restrict_sourcesource_table)) * dst_positive_scale_restrict_sourcesource_table) + (dst_positive_restrict_sourcesource_table))) /\ (((((exists ff_h_pvs_restrict_sourcesource_tableentrynegative. ff_h_pvs_restrict_sourcesource_tableentrynegative + S (dst_negative_restrict_sourcesource_table) = S ((S (dst_index_restrict_sourcesource_table)) * dst_negative_scale_restrict_sourcesource_table)) /\ exists ff_q_pvs_restrict_sourcesource_tableentrynegative. dst_negative_code_restrict_sourcesource_table = ff_q_pvs_restrict_sourcesource_tableentrynegative * S ((S (dst_index_restrict_sourcesource_table)) * dst_negative_scale_restrict_sourcesource_table) + (dst_negative_restrict_sourcesource_table))) /\ (exists ge_balance_positive_restrict_sourcesource_tableentryvalue ge_balance_negative_restrict_sourcesource_tableentryvalue. (((((dst_value_restrict_sourcesource_table) = 2 * (ge_balance_positive_restrict_sourcesource_tableentryvalue) /\ (ge_balance_negative_restrict_sourcesource_tableentryvalue) = 0) \/ exists ge_signed_half_restrict_sourcesource_tableentryvaluedecode. (((dst_value_restrict_sourcesource_table) = 2 * ge_signed_half_restrict_sourcesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcesource_tableentryvalue) = 0) /\ (ge_balance_negative_restrict_sourcesource_tableentryvalue) = S ge_signed_half_restrict_sourcesource_tableentryvaluedecode))) /\ ((dst_positive_restrict_sourcesource_table) + ge_balance_negative_restrict_sourcesource_tableentryvalue = (dst_negative_restrict_sourcesource_table) + ge_balance_positive_restrict_sourcesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_sourceoutput_table dst_positive_scale_restrict_sourceoutput_table dst_negative_code_restrict_sourceoutput_table dst_negative_scale_restrict_sourceoutput_table. (((G) = (((((dst_positive_code_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table)) * S ((dst_positive_code_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table)) + ((dst_positive_scale_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table))) + (((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) * S ((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) + ((dst_negative_scale_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)))) * S ((((dst_positive_code_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table)) * S ((dst_positive_code_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table)) + ((dst_positive_scale_restrict_sourceoutput_table) + (dst_positive_scale_restrict_sourceoutput_table))) + (((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) * S ((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) + ((dst_negative_scale_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)))) + ((((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) * S ((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) + ((dst_negative_scale_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table))) + (((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) * S ((dst_negative_code_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)) + ((dst_negative_scale_restrict_sourceoutput_table) + (dst_negative_scale_restrict_sourceoutput_table)))))) /\ (forall dst_index_restrict_sourceoutput_table. (exists pvs_le_gap_restrict_sourceoutput_tabledomain. pvs_le_gap_restrict_sourceoutput_tabledomain + (dst_index_restrict_sourceoutput_table) = (S l)) -> exists dst_positive_restrict_sourceoutput_table dst_negative_restrict_sourceoutput_table dst_value_restrict_sourceoutput_table. ((((exists ff_h_pvs_restrict_sourceoutput_tableentrypositive. ff_h_pvs_restrict_sourceoutput_tableentrypositive + S (dst_positive_restrict_sourceoutput_table) = S ((S (dst_index_restrict_sourceoutput_table)) * dst_positive_scale_restrict_sourceoutput_table)) /\ exists ff_q_pvs_restrict_sourceoutput_tableentrypositive. dst_positive_code_restrict_sourceoutput_table = ff_q_pvs_restrict_sourceoutput_tableentrypositive * S ((S (dst_index_restrict_sourceoutput_table)) * dst_positive_scale_restrict_sourceoutput_table) + (dst_positive_restrict_sourceoutput_table))) /\ (((((exists ff_h_pvs_restrict_sourceoutput_tableentrynegative. ff_h_pvs_restrict_sourceoutput_tableentrynegative + S (dst_negative_restrict_sourceoutput_table) = S ((S (dst_index_restrict_sourceoutput_table)) * dst_negative_scale_restrict_sourceoutput_table)) /\ exists ff_q_pvs_restrict_sourceoutput_tableentrynegative. dst_negative_code_restrict_sourceoutput_table = ff_q_pvs_restrict_sourceoutput_tableentrynegative * S ((S (dst_index_restrict_sourceoutput_table)) * dst_negative_scale_restrict_sourceoutput_table) + (dst_negative_restrict_sourceoutput_table))) /\ (exists ge_balance_positive_restrict_sourceoutput_tableentryvalue ge_balance_negative_restrict_sourceoutput_tableentryvalue. (((((dst_value_restrict_sourceoutput_table) = 2 * (ge_balance_positive_restrict_sourceoutput_tableentryvalue) /\ (ge_balance_negative_restrict_sourceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_restrict_sourceoutput_tableentryvaluedecode. (((dst_value_restrict_sourceoutput_table) = 2 * ge_signed_half_restrict_sourceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_restrict_sourceoutput_tableentryvalue) = S ge_signed_half_restrict_sourceoutput_tableentryvaluedecode))) /\ ((dst_positive_restrict_sourceoutput_table) + ge_balance_negative_restrict_sourceoutput_tableentryvalue = (dst_negative_restrict_sourceoutput_table) + ge_balance_positive_restrict_sourceoutput_tableentryvalue))))))))) /\ (forall srs_index_restrict_source. (exists pvs_gap_restrict_sourcebound. pvs_gap_restrict_sourcebound + S (srs_index_restrict_source) = (S l)) -> exists srs_value_restrict_source. (((exists dst_positive_code_restrict_sourceentrysource dst_positive_scale_restrict_sourceentrysource dst_negative_code_restrict_sourceentrysource dst_negative_scale_restrict_sourceentrysource dst_positive_restrict_sourceentrysource dst_negative_restrict_sourceentrysource. (((F) = (((((dst_positive_code_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource)) * S ((dst_positive_code_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource)) + ((dst_positive_scale_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource))) + (((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) * S ((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) + ((dst_negative_scale_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)))) * S ((((dst_positive_code_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource)) * S ((dst_positive_code_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource)) + ((dst_positive_scale_restrict_sourceentrysource) + (dst_positive_scale_restrict_sourceentrysource))) + (((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) * S ((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) + ((dst_negative_scale_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)))) + ((((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) * S ((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) + ((dst_negative_scale_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource))) + (((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) * S ((dst_negative_code_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)) + ((dst_negative_scale_restrict_sourceentrysource) + (dst_negative_scale_restrict_sourceentrysource)))))) /\ (((((exists ff_h_pvs_restrict_sourceentrysourcepositive. ff_h_pvs_restrict_sourceentrysourcepositive + S (dst_positive_restrict_sourceentrysource) = S ((S (((o) + ((s) * (srs_index_restrict_source))))) * dst_positive_scale_restrict_sourceentrysource)) /\ exists ff_q_pvs_restrict_sourceentrysourcepositive. dst_positive_code_restrict_sourceentrysource = ff_q_pvs_restrict_sourceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_restrict_source))))) * dst_positive_scale_restrict_sourceentrysource) + (dst_positive_restrict_sourceentrysource))) /\ (((((exists ff_h_pvs_restrict_sourceentrysourcenegative. ff_h_pvs_restrict_sourceentrysourcenegative + S (dst_negative_restrict_sourceentrysource) = S ((S (((o) + ((s) * (srs_index_restrict_source))))) * dst_negative_scale_restrict_sourceentrysource)) /\ exists ff_q_pvs_restrict_sourceentrysourcenegative. dst_negative_code_restrict_sourceentrysource = ff_q_pvs_restrict_sourceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_restrict_source))))) * dst_negative_scale_restrict_sourceentrysource) + (dst_negative_restrict_sourceentrysource))) /\ (exists ge_balance_positive_restrict_sourceentrysourcevalue ge_balance_negative_restrict_sourceentrysourcevalue. (((((srs_value_restrict_source) = 2 * (ge_balance_positive_restrict_sourceentrysourcevalue) /\ (ge_balance_negative_restrict_sourceentrysourcevalue) = 0) \/ exists ge_signed_half_restrict_sourceentrysourcevaluedecode. (((srs_value_restrict_source) = 2 * ge_signed_half_restrict_sourceentrysourcevaluedecode + 1 /\ (ge_balance_positive_restrict_sourceentrysourcevalue) = 0) /\ (ge_balance_negative_restrict_sourceentrysourcevalue) = S ge_signed_half_restrict_sourceentrysourcevaluedecode))) /\ ((dst_positive_restrict_sourceentrysource) + ge_balance_negative_restrict_sourceentrysourcevalue = (dst_negative_restrict_sourceentrysource) + ge_balance_positive_restrict_sourceentrysourcevalue))))))))) /\ (exists dst_positive_code_restrict_sourceentryoutput dst_positive_scale_restrict_sourceentryoutput dst_negative_code_restrict_sourceentryoutput dst_negative_scale_restrict_sourceentryoutput dst_positive_restrict_sourceentryoutput dst_negative_restrict_sourceentryoutput. (((G) = (((((dst_positive_code_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput)) * S ((dst_positive_code_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput)) + ((dst_positive_scale_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput))) + (((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) * S ((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) + ((dst_negative_scale_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)))) * S ((((dst_positive_code_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput)) * S ((dst_positive_code_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput)) + ((dst_positive_scale_restrict_sourceentryoutput) + (dst_positive_scale_restrict_sourceentryoutput))) + (((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) * S ((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) + ((dst_negative_scale_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)))) + ((((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) * S ((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) + ((dst_negative_scale_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput))) + (((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) * S ((dst_negative_code_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)) + ((dst_negative_scale_restrict_sourceentryoutput) + (dst_negative_scale_restrict_sourceentryoutput)))))) /\ (((((exists ff_h_pvs_restrict_sourceentryoutputpositive. ff_h_pvs_restrict_sourceentryoutputpositive + S (dst_positive_restrict_sourceentryoutput) = S ((S (srs_index_restrict_source)) * dst_positive_scale_restrict_sourceentryoutput)) /\ exists ff_q_pvs_restrict_sourceentryoutputpositive. dst_positive_code_restrict_sourceentryoutput = ff_q_pvs_restrict_sourceentryoutputpositive * S ((S (srs_index_restrict_source)) * dst_positive_scale_restrict_sourceentryoutput) + (dst_positive_restrict_sourceentryoutput))) /\ (((((exists ff_h_pvs_restrict_sourceentryoutputnegative. ff_h_pvs_restrict_sourceentryoutputnegative + S (dst_negative_restrict_sourceentryoutput) = S ((S (srs_index_restrict_source)) * dst_negative_scale_restrict_sourceentryoutput)) /\ exists ff_q_pvs_restrict_sourceentryoutputnegative. dst_negative_code_restrict_sourceentryoutput = ff_q_pvs_restrict_sourceentryoutputnegative * S ((S (srs_index_restrict_source)) * dst_negative_scale_restrict_sourceentryoutput) + (dst_negative_restrict_sourceentryoutput))) /\ (exists ge_balance_positive_restrict_sourceentryoutputvalue ge_balance_negative_restrict_sourceentryoutputvalue. (((((srs_value_restrict_source) = 2 * (ge_balance_positive_restrict_sourceentryoutputvalue) /\ (ge_balance_negative_restrict_sourceentryoutputvalue) = 0) \/ exists ge_signed_half_restrict_sourceentryoutputvaluedecode. (((srs_value_restrict_source) = 2 * ge_signed_half_restrict_sourceentryoutputvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceentryoutputvalue) = 0) /\ (ge_balance_negative_restrict_sourceentryoutputvalue) = S ge_signed_half_restrict_sourceentryoutputvaluedecode))) /\ ((dst_positive_restrict_sourceentryoutput) + ge_balance_negative_restrict_sourceentryoutputvalue = (dst_negative_restrict_sourceentryoutput) + ge_balance_positive_restrict_sourceentryoutputvalue)))))))))))))))) -> (((exists dst_positive_code_restrict_resultsource_table dst_positive_scale_restrict_resultsource_table dst_negative_code_restrict_resultsource_table dst_negative_scale_restrict_resultsource_table. (((F) = (((((dst_positive_code_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table)) * S ((dst_positive_code_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table)) + ((dst_positive_scale_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table))) + (((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) * S ((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) + ((dst_negative_scale_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)))) * S ((((dst_positive_code_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table)) * S ((dst_positive_code_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table)) + ((dst_positive_scale_restrict_resultsource_table) + (dst_positive_scale_restrict_resultsource_table))) + (((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) * S ((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) + ((dst_negative_scale_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)))) + ((((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) * S ((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) + ((dst_negative_scale_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table))) + (((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) * S ((dst_negative_code_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)) + ((dst_negative_scale_restrict_resultsource_table) + (dst_negative_scale_restrict_resultsource_table)))))) /\ (forall dst_index_restrict_resultsource_table. (exists pvs_le_gap_restrict_resultsource_tabledomain. pvs_le_gap_restrict_resultsource_tabledomain + (dst_index_restrict_resultsource_table) = (0)) -> exists dst_positive_restrict_resultsource_table dst_negative_restrict_resultsource_table dst_value_restrict_resultsource_table. ((((exists ff_h_pvs_restrict_resultsource_tableentrypositive. ff_h_pvs_restrict_resultsource_tableentrypositive + S (dst_positive_restrict_resultsource_table) = S ((S (dst_index_restrict_resultsource_table)) * dst_positive_scale_restrict_resultsource_table)) /\ exists ff_q_pvs_restrict_resultsource_tableentrypositive. dst_positive_code_restrict_resultsource_table = ff_q_pvs_restrict_resultsource_tableentrypositive * S ((S (dst_index_restrict_resultsource_table)) * dst_positive_scale_restrict_resultsource_table) + (dst_positive_restrict_resultsource_table))) /\ (((((exists ff_h_pvs_restrict_resultsource_tableentrynegative. ff_h_pvs_restrict_resultsource_tableentrynegative + S (dst_negative_restrict_resultsource_table) = S ((S (dst_index_restrict_resultsource_table)) * dst_negative_scale_restrict_resultsource_table)) /\ exists ff_q_pvs_restrict_resultsource_tableentrynegative. dst_negative_code_restrict_resultsource_table = ff_q_pvs_restrict_resultsource_tableentrynegative * S ((S (dst_index_restrict_resultsource_table)) * dst_negative_scale_restrict_resultsource_table) + (dst_negative_restrict_resultsource_table))) /\ (exists ge_balance_positive_restrict_resultsource_tableentryvalue ge_balance_negative_restrict_resultsource_tableentryvalue. (((((dst_value_restrict_resultsource_table) = 2 * (ge_balance_positive_restrict_resultsource_tableentryvalue) /\ (ge_balance_negative_restrict_resultsource_tableentryvalue) = 0) \/ exists ge_signed_half_restrict_resultsource_tableentryvaluedecode. (((dst_value_restrict_resultsource_table) = 2 * ge_signed_half_restrict_resultsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_resultsource_tableentryvalue) = 0) /\ (ge_balance_negative_restrict_resultsource_tableentryvalue) = S ge_signed_half_restrict_resultsource_tableentryvaluedecode))) /\ ((dst_positive_restrict_resultsource_table) + ge_balance_negative_restrict_resultsource_tableentryvalue = (dst_negative_restrict_resultsource_table) + ge_balance_positive_restrict_resultsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_resultoutput_table dst_positive_scale_restrict_resultoutput_table dst_negative_code_restrict_resultoutput_table dst_negative_scale_restrict_resultoutput_table. (((G) = (((((dst_positive_code_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table)) * S ((dst_positive_code_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table)) + ((dst_positive_scale_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table))) + (((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) * S ((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) + ((dst_negative_scale_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)))) * S ((((dst_positive_code_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table)) * S ((dst_positive_code_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table)) + ((dst_positive_scale_restrict_resultoutput_table) + (dst_positive_scale_restrict_resultoutput_table))) + (((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) * S ((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) + ((dst_negative_scale_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)))) + ((((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) * S ((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) + ((dst_negative_scale_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table))) + (((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) * S ((dst_negative_code_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)) + ((dst_negative_scale_restrict_resultoutput_table) + (dst_negative_scale_restrict_resultoutput_table)))))) /\ (forall dst_index_restrict_resultoutput_table. (exists pvs_le_gap_restrict_resultoutput_tabledomain. pvs_le_gap_restrict_resultoutput_tabledomain + (dst_index_restrict_resultoutput_table) = (l)) -> exists dst_positive_restrict_resultoutput_table dst_negative_restrict_resultoutput_table dst_value_restrict_resultoutput_table. ((((exists ff_h_pvs_restrict_resultoutput_tableentrypositive. ff_h_pvs_restrict_resultoutput_tableentrypositive + S (dst_positive_restrict_resultoutput_table) = S ((S (dst_index_restrict_resultoutput_table)) * dst_positive_scale_restrict_resultoutput_table)) /\ exists ff_q_pvs_restrict_resultoutput_tableentrypositive. dst_positive_code_restrict_resultoutput_table = ff_q_pvs_restrict_resultoutput_tableentrypositive * S ((S (dst_index_restrict_resultoutput_table)) * dst_positive_scale_restrict_resultoutput_table) + (dst_positive_restrict_resultoutput_table))) /\ (((((exists ff_h_pvs_restrict_resultoutput_tableentrynegative. ff_h_pvs_restrict_resultoutput_tableentrynegative + S (dst_negative_restrict_resultoutput_table) = S ((S (dst_index_restrict_resultoutput_table)) * dst_negative_scale_restrict_resultoutput_table)) /\ exists ff_q_pvs_restrict_resultoutput_tableentrynegative. dst_negative_code_restrict_resultoutput_table = ff_q_pvs_restrict_resultoutput_tableentrynegative * S ((S (dst_index_restrict_resultoutput_table)) * dst_negative_scale_restrict_resultoutput_table) + (dst_negative_restrict_resultoutput_table))) /\ (exists ge_balance_positive_restrict_resultoutput_tableentryvalue ge_balance_negative_restrict_resultoutput_tableentryvalue. (((((dst_value_restrict_resultoutput_table) = 2 * (ge_balance_positive_restrict_resultoutput_tableentryvalue) /\ (ge_balance_negative_restrict_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_restrict_resultoutput_tableentryvaluedecode. (((dst_value_restrict_resultoutput_table) = 2 * ge_signed_half_restrict_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_restrict_resultoutput_tableentryvalue) = S ge_signed_half_restrict_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_restrict_resultoutput_table) + ge_balance_negative_restrict_resultoutput_tableentryvalue = (dst_negative_restrict_resultoutput_table) + ge_balance_positive_restrict_resultoutput_tableentryvalue))))))))) /\ (forall srs_index_restrict_result. (exists pvs_gap_restrict_resultbound. pvs_gap_restrict_resultbound + S (srs_index_restrict_result) = (l)) -> exists srs_value_restrict_result. (((exists dst_positive_code_restrict_resultentrysource dst_positive_scale_restrict_resultentrysource dst_negative_code_restrict_resultentrysource dst_negative_scale_restrict_resultentrysource dst_positive_restrict_resultentrysource dst_negative_restrict_resultentrysource. (((F) = (((((dst_positive_code_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource)) * S ((dst_positive_code_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource)) + ((dst_positive_scale_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource))) + (((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) * S ((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) + ((dst_negative_scale_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)))) * S ((((dst_positive_code_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource)) * S ((dst_positive_code_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource)) + ((dst_positive_scale_restrict_resultentrysource) + (dst_positive_scale_restrict_resultentrysource))) + (((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) * S ((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) + ((dst_negative_scale_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)))) + ((((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) * S ((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) + ((dst_negative_scale_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource))) + (((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) * S ((dst_negative_code_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)) + ((dst_negative_scale_restrict_resultentrysource) + (dst_negative_scale_restrict_resultentrysource)))))) /\ (((((exists ff_h_pvs_restrict_resultentrysourcepositive. ff_h_pvs_restrict_resultentrysourcepositive + S (dst_positive_restrict_resultentrysource) = S ((S (((o) + ((s) * (srs_index_restrict_result))))) * dst_positive_scale_restrict_resultentrysource)) /\ exists ff_q_pvs_restrict_resultentrysourcepositive. dst_positive_code_restrict_resultentrysource = ff_q_pvs_restrict_resultentrysourcepositive * S ((S (((o) + ((s) * (srs_index_restrict_result))))) * dst_positive_scale_restrict_resultentrysource) + (dst_positive_restrict_resultentrysource))) /\ (((((exists ff_h_pvs_restrict_resultentrysourcenegative. ff_h_pvs_restrict_resultentrysourcenegative + S (dst_negative_restrict_resultentrysource) = S ((S (((o) + ((s) * (srs_index_restrict_result))))) * dst_negative_scale_restrict_resultentrysource)) /\ exists ff_q_pvs_restrict_resultentrysourcenegative. dst_negative_code_restrict_resultentrysource = ff_q_pvs_restrict_resultentrysourcenegative * S ((S (((o) + ((s) * (srs_index_restrict_result))))) * dst_negative_scale_restrict_resultentrysource) + (dst_negative_restrict_resultentrysource))) /\ (exists ge_balance_positive_restrict_resultentrysourcevalue ge_balance_negative_restrict_resultentrysourcevalue. (((((srs_value_restrict_result) = 2 * (ge_balance_positive_restrict_resultentrysourcevalue) /\ (ge_balance_negative_restrict_resultentrysourcevalue) = 0) \/ exists ge_signed_half_restrict_resultentrysourcevaluedecode. (((srs_value_restrict_result) = 2 * ge_signed_half_restrict_resultentrysourcevaluedecode + 1 /\ (ge_balance_positive_restrict_resultentrysourcevalue) = 0) /\ (ge_balance_negative_restrict_resultentrysourcevalue) = S ge_signed_half_restrict_resultentrysourcevaluedecode))) /\ ((dst_positive_restrict_resultentrysource) + ge_balance_negative_restrict_resultentrysourcevalue = (dst_negative_restrict_resultentrysource) + ge_balance_positive_restrict_resultentrysourcevalue))))))))) /\ (exists dst_positive_code_restrict_resultentryoutput dst_positive_scale_restrict_resultentryoutput dst_negative_code_restrict_resultentryoutput dst_negative_scale_restrict_resultentryoutput dst_positive_restrict_resultentryoutput dst_negative_restrict_resultentryoutput. (((G) = (((((dst_positive_code_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput)) * S ((dst_positive_code_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput)) + ((dst_positive_scale_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput))) + (((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) * S ((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) + ((dst_negative_scale_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)))) * S ((((dst_positive_code_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput)) * S ((dst_positive_code_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput)) + ((dst_positive_scale_restrict_resultentryoutput) + (dst_positive_scale_restrict_resultentryoutput))) + (((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) * S ((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) + ((dst_negative_scale_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)))) + ((((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) * S ((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) + ((dst_negative_scale_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput))) + (((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) * S ((dst_negative_code_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)) + ((dst_negative_scale_restrict_resultentryoutput) + (dst_negative_scale_restrict_resultentryoutput)))))) /\ (((((exists ff_h_pvs_restrict_resultentryoutputpositive. ff_h_pvs_restrict_resultentryoutputpositive + S (dst_positive_restrict_resultentryoutput) = S ((S (srs_index_restrict_result)) * dst_positive_scale_restrict_resultentryoutput)) /\ exists ff_q_pvs_restrict_resultentryoutputpositive. dst_positive_code_restrict_resultentryoutput = ff_q_pvs_restrict_resultentryoutputpositive * S ((S (srs_index_restrict_result)) * dst_positive_scale_restrict_resultentryoutput) + (dst_positive_restrict_resultentryoutput))) /\ (((((exists ff_h_pvs_restrict_resultentryoutputnegative. ff_h_pvs_restrict_resultentryoutputnegative + S (dst_negative_restrict_resultentryoutput) = S ((S (srs_index_restrict_result)) * dst_negative_scale_restrict_resultentryoutput)) /\ exists ff_q_pvs_restrict_resultentryoutputnegative. dst_negative_code_restrict_resultentryoutput = ff_q_pvs_restrict_resultentryoutputnegative * S ((S (srs_index_restrict_result)) * dst_negative_scale_restrict_resultentryoutput) + (dst_negative_restrict_resultentryoutput))) /\ (exists ge_balance_positive_restrict_resultentryoutputvalue ge_balance_negative_restrict_resultentryoutputvalue. (((((srs_value_restrict_result) = 2 * (ge_balance_positive_restrict_resultentryoutputvalue) /\ (ge_balance_negative_restrict_resultentryoutputvalue) = 0) \/ exists ge_signed_half_restrict_resultentryoutputvaluedecode. (((srs_value_restrict_result) = 2 * ge_signed_half_restrict_resultentryoutputvaluedecode + 1 /\ (ge_balance_positive_restrict_resultentryoutputvalue) = 0) /\ (ge_balance_negative_restrict_resultentryoutputvalue) = S ge_signed_half_restrict_resultentryoutputvaluedecode))) /\ ((dst_positive_restrict_resultentryoutput) + ge_balance_negative_restrict_resultentryoutputvalue = (dst_negative_restrict_resultentryoutput) + ge_balance_positive_restrict_resultentryoutputvalue))))))))))))))))