signed_rectangular_slice_lookup

forall F G o s l i z. (((exists dst_positive_code_lookup_slicesource_table dst_positive_scale_lookup_slicesource_table dst_negative_code_lookup_slicesource_table dst_negative_scale_lookup_slicesource_table. (((F) = (((((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) * S ((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) + ((dst_positive_scale_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))) * S ((((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) * S ((dst_positive_code_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table)) + ((dst_positive_scale_lookup_slicesource_table) + (dst_positive_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))) + ((((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table))) + (((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) * S ((dst_negative_code_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)) + ((dst_negative_scale_lookup_slicesource_table) + (dst_negative_scale_lookup_slicesource_table)))))) /\ (forall dst_index_lookup_slicesource_table. (exists pvs_le_gap_lookup_slicesource_tabledomain. pvs_le_gap_lookup_slicesource_tabledomain + (dst_index_lookup_slicesource_table) = (0)) -> exists dst_positive_lookup_slicesource_table dst_negative_lookup_slicesource_table dst_value_lookup_slicesource_table. ((((exists ff_h_pvs_lookup_slicesource_tableentrypositive. ff_h_pvs_lookup_slicesource_tableentrypositive + S (dst_positive_lookup_slicesource_table) = S ((S (dst_index_lookup_slicesource_table)) * dst_positive_scale_lookup_slicesource_table)) /\ exists ff_q_pvs_lookup_slicesource_tableentrypositive. dst_positive_code_lookup_slicesource_table = ff_q_pvs_lookup_slicesource_tableentrypositive * S ((S (dst_index_lookup_slicesource_table)) * dst_positive_scale_lookup_slicesource_table) + (dst_positive_lookup_slicesource_table))) /\ (((((exists ff_h_pvs_lookup_slicesource_tableentrynegative. ff_h_pvs_lookup_slicesource_tableentrynegative + S (dst_negative_lookup_slicesource_table) = S ((S (dst_index_lookup_slicesource_table)) * dst_negative_scale_lookup_slicesource_table)) /\ exists ff_q_pvs_lookup_slicesource_tableentrynegative. dst_negative_code_lookup_slicesource_table = ff_q_pvs_lookup_slicesource_tableentrynegative * S ((S (dst_index_lookup_slicesource_table)) * dst_negative_scale_lookup_slicesource_table) + (dst_negative_lookup_slicesource_table))) /\ (exists ge_balance_positive_lookup_slicesource_tableentryvalue ge_balance_negative_lookup_slicesource_tableentryvalue. (((((dst_value_lookup_slicesource_table) = 2 * (ge_balance_positive_lookup_slicesource_tableentryvalue) /\ (ge_balance_negative_lookup_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_slicesource_tableentryvaluedecode. (((dst_value_lookup_slicesource_table) = 2 * ge_signed_half_lookup_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_slicesource_tableentryvalue) = S ge_signed_half_lookup_slicesource_tableentryvaluedecode))) /\ ((dst_positive_lookup_slicesource_table) + ge_balance_negative_lookup_slicesource_tableentryvalue = (dst_negative_lookup_slicesource_table) + ge_balance_positive_lookup_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lookup_sliceoutput_table dst_positive_scale_lookup_sliceoutput_table dst_negative_code_lookup_sliceoutput_table dst_negative_scale_lookup_sliceoutput_table. (((G) = (((((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) * S ((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) + ((dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))) * S ((((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) * S ((dst_positive_code_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table)) + ((dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))) + ((((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table))) + (((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) * S ((dst_negative_code_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)) + ((dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_scale_lookup_sliceoutput_table)))))) /\ (forall dst_index_lookup_sliceoutput_table. (exists pvs_le_gap_lookup_sliceoutput_tabledomain. pvs_le_gap_lookup_sliceoutput_tabledomain + (dst_index_lookup_sliceoutput_table) = (l)) -> exists dst_positive_lookup_sliceoutput_table dst_negative_lookup_sliceoutput_table dst_value_lookup_sliceoutput_table. ((((exists ff_h_pvs_lookup_sliceoutput_tableentrypositive. ff_h_pvs_lookup_sliceoutput_tableentrypositive + S (dst_positive_lookup_sliceoutput_table) = S ((S (dst_index_lookup_sliceoutput_table)) * dst_positive_scale_lookup_sliceoutput_table)) /\ exists ff_q_pvs_lookup_sliceoutput_tableentrypositive. dst_positive_code_lookup_sliceoutput_table = ff_q_pvs_lookup_sliceoutput_tableentrypositive * S ((S (dst_index_lookup_sliceoutput_table)) * dst_positive_scale_lookup_sliceoutput_table) + (dst_positive_lookup_sliceoutput_table))) /\ (((((exists ff_h_pvs_lookup_sliceoutput_tableentrynegative. ff_h_pvs_lookup_sliceoutput_tableentrynegative + S (dst_negative_lookup_sliceoutput_table) = S ((S (dst_index_lookup_sliceoutput_table)) * dst_negative_scale_lookup_sliceoutput_table)) /\ exists ff_q_pvs_lookup_sliceoutput_tableentrynegative. dst_negative_code_lookup_sliceoutput_table = ff_q_pvs_lookup_sliceoutput_tableentrynegative * S ((S (dst_index_lookup_sliceoutput_table)) * dst_negative_scale_lookup_sliceoutput_table) + (dst_negative_lookup_sliceoutput_table))) /\ (exists ge_balance_positive_lookup_sliceoutput_tableentryvalue ge_balance_negative_lookup_sliceoutput_tableentryvalue. (((((dst_value_lookup_sliceoutput_table) = 2 * (ge_balance_positive_lookup_sliceoutput_tableentryvalue) /\ (ge_balance_negative_lookup_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lookup_sliceoutput_tableentryvaluedecode. (((dst_value_lookup_sliceoutput_table) = 2 * ge_signed_half_lookup_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lookup_sliceoutput_tableentryvalue) = S ge_signed_half_lookup_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_lookup_sliceoutput_table) + ge_balance_negative_lookup_sliceoutput_tableentryvalue = (dst_negative_lookup_sliceoutput_table) + ge_balance_positive_lookup_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_lookup_slice. (exists pvs_gap_lookup_slicebound. pvs_gap_lookup_slicebound + S (srs_index_lookup_slice) = (l)) -> exists srs_value_lookup_slice. (((exists dst_positive_code_lookup_sliceentrysource dst_positive_scale_lookup_sliceentrysource dst_negative_code_lookup_sliceentrysource dst_negative_scale_lookup_sliceentrysource dst_positive_lookup_sliceentrysource dst_negative_lookup_sliceentrysource. (((F) = (((((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) * S ((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) + ((dst_positive_scale_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))) * S ((((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) * S ((dst_positive_code_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource)) + ((dst_positive_scale_lookup_sliceentrysource) + (dst_positive_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))) + ((((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource))) + (((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) * S ((dst_negative_code_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)) + ((dst_negative_scale_lookup_sliceentrysource) + (dst_negative_scale_lookup_sliceentrysource)))))) /\ (((((exists ff_h_pvs_lookup_sliceentrysourcepositive. ff_h_pvs_lookup_sliceentrysourcepositive + S (dst_positive_lookup_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_positive_scale_lookup_sliceentrysource)) /\ exists ff_q_pvs_lookup_sliceentrysourcepositive. dst_positive_code_lookup_sliceentrysource = ff_q_pvs_lookup_sliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_positive_scale_lookup_sliceentrysource) + (dst_positive_lookup_sliceentrysource))) /\ (((((exists ff_h_pvs_lookup_sliceentrysourcenegative. ff_h_pvs_lookup_sliceentrysourcenegative + S (dst_negative_lookup_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_negative_scale_lookup_sliceentrysource)) /\ exists ff_q_pvs_lookup_sliceentrysourcenegative. dst_negative_code_lookup_sliceentrysource = ff_q_pvs_lookup_sliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_lookup_slice))))) * dst_negative_scale_lookup_sliceentrysource) + (dst_negative_lookup_sliceentrysource))) /\ (exists ge_balance_positive_lookup_sliceentrysourcevalue ge_balance_negative_lookup_sliceentrysourcevalue. (((((srs_value_lookup_slice) = 2 * (ge_balance_positive_lookup_sliceentrysourcevalue) /\ (ge_balance_negative_lookup_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_lookup_sliceentrysourcevaluedecode. (((srs_value_lookup_slice) = 2 * ge_signed_half_lookup_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_lookup_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_lookup_sliceentrysourcevalue) = S ge_signed_half_lookup_sliceentrysourcevaluedecode))) /\ ((dst_positive_lookup_sliceentrysource) + ge_balance_negative_lookup_sliceentrysourcevalue = (dst_negative_lookup_sliceentrysource) + ge_balance_positive_lookup_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_lookup_sliceentryoutput dst_positive_scale_lookup_sliceentryoutput dst_negative_code_lookup_sliceentryoutput dst_negative_scale_lookup_sliceentryoutput dst_positive_lookup_sliceentryoutput dst_negative_lookup_sliceentryoutput. (((G) = (((((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) * S ((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) + ((dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))) * S ((((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) * S ((dst_positive_code_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput)) + ((dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))) + ((((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput))) + (((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) * S ((dst_negative_code_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)) + ((dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_scale_lookup_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_lookup_sliceentryoutputpositive. ff_h_pvs_lookup_sliceentryoutputpositive + S (dst_positive_lookup_sliceentryoutput) = S ((S (srs_index_lookup_slice)) * dst_positive_scale_lookup_sliceentryoutput)) /\ exists ff_q_pvs_lookup_sliceentryoutputpositive. dst_positive_code_lookup_sliceentryoutput = ff_q_pvs_lookup_sliceentryoutputpositive * S ((S (srs_index_lookup_slice)) * dst_positive_scale_lookup_sliceentryoutput) + (dst_positive_lookup_sliceentryoutput))) /\ (((((exists ff_h_pvs_lookup_sliceentryoutputnegative. ff_h_pvs_lookup_sliceentryoutputnegative + S (dst_negative_lookup_sliceentryoutput) = S ((S (srs_index_lookup_slice)) * dst_negative_scale_lookup_sliceentryoutput)) /\ exists ff_q_pvs_lookup_sliceentryoutputnegative. dst_negative_code_lookup_sliceentryoutput = ff_q_pvs_lookup_sliceentryoutputnegative * S ((S (srs_index_lookup_slice)) * dst_negative_scale_lookup_sliceentryoutput) + (dst_negative_lookup_sliceentryoutput))) /\ (exists ge_balance_positive_lookup_sliceentryoutputvalue ge_balance_negative_lookup_sliceentryoutputvalue. (((((srs_value_lookup_slice) = 2 * (ge_balance_positive_lookup_sliceentryoutputvalue) /\ (ge_balance_negative_lookup_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_lookup_sliceentryoutputvaluedecode. (((srs_value_lookup_slice) = 2 * ge_signed_half_lookup_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_lookup_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_lookup_sliceentryoutputvalue) = S ge_signed_half_lookup_sliceentryoutputvaluedecode))) /\ ((dst_positive_lookup_sliceentryoutput) + ge_balance_negative_lookup_sliceentryoutputvalue = (dst_negative_lookup_sliceentryoutput) + ge_balance_positive_lookup_sliceentryoutputvalue)))))))))))))))) -> (exists pvs_gap_lookup_bound. pvs_gap_lookup_bound + S (i) = (l)) -> (exists dst_positive_code_lookup_value dst_positive_scale_lookup_value dst_negative_code_lookup_value dst_negative_scale_lookup_value dst_positive_lookup_value dst_negative_lookup_value. (((G) = (((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) * S ((((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) * S ((dst_positive_code_lookup_value) + (dst_positive_scale_lookup_value)) + ((dst_positive_scale_lookup_value) + (dst_positive_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))) + ((((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value))) + (((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) * S ((dst_negative_code_lookup_value) + (dst_negative_scale_lookup_value)) + ((dst_negative_scale_lookup_value) + (dst_negative_scale_lookup_value)))))) /\ (((((exists ff_h_pvs_lookup_valuepositive. ff_h_pvs_lookup_valuepositive + S (dst_positive_lookup_value) = S ((S (i)) * dst_positive_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuepositive. dst_positive_code_lookup_value = ff_q_pvs_lookup_valuepositive * S ((S (i)) * dst_positive_scale_lookup_value) + (dst_positive_lookup_value))) /\ (((((exists ff_h_pvs_lookup_valuenegative. ff_h_pvs_lookup_valuenegative + S (dst_negative_lookup_value) = S ((S (i)) * dst_negative_scale_lookup_value)) /\ exists ff_q_pvs_lookup_valuenegative. dst_negative_code_lookup_value = ff_q_pvs_lookup_valuenegative * S ((S (i)) * dst_negative_scale_lookup_value) + (dst_negative_lookup_value))) /\ (exists ge_balance_positive_lookup_valuevalue ge_balance_negative_lookup_valuevalue. (((((z) = 2 * (ge_balance_positive_lookup_valuevalue) /\ (ge_balance_negative_lookup_valuevalue) = 0) \/ exists ge_signed_half_lookup_valuevaluedecode. (((z) = 2 * ge_signed_half_lookup_valuevaluedecode + 1 /\ (ge_balance_positive_lookup_valuevalue) = 0) /\ (ge_balance_negative_lookup_valuevalue) = S ge_signed_half_lookup_valuevaluedecode))) /\ ((dst_positive_lookup_value) + ge_balance_negative_lookup_valuevalue = (dst_negative_lookup_value) + ge_balance_positive_lookup_valuevalue))))))))) -> (exists dst_positive_code_lookup_source dst_positive_scale_lookup_source dst_negative_code_lookup_source dst_negative_scale_lookup_source dst_positive_lookup_source dst_negative_lookup_source. (((F) = (((((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) * S ((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) + ((dst_positive_scale_lookup_source) + (dst_positive_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))) * S ((((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) * S ((dst_positive_code_lookup_source) + (dst_positive_scale_lookup_source)) + ((dst_positive_scale_lookup_source) + (dst_positive_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))) + ((((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source))) + (((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) * S ((dst_negative_code_lookup_source) + (dst_negative_scale_lookup_source)) + ((dst_negative_scale_lookup_source) + (dst_negative_scale_lookup_source)))))) /\ (((((exists ff_h_pvs_lookup_sourcepositive. ff_h_pvs_lookup_sourcepositive + S (dst_positive_lookup_source) = S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_source)) /\ exists ff_q_pvs_lookup_sourcepositive. dst_positive_code_lookup_source = ff_q_pvs_lookup_sourcepositive * S ((S (((o) + ((s) * (i))))) * dst_positive_scale_lookup_source) + (dst_positive_lookup_source))) /\ (((((exists ff_h_pvs_lookup_sourcenegative. ff_h_pvs_lookup_sourcenegative + S (dst_negative_lookup_source) = S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_source)) /\ exists ff_q_pvs_lookup_sourcenegative. dst_negative_code_lookup_source = ff_q_pvs_lookup_sourcenegative * S ((S (((o) + ((s) * (i))))) * dst_negative_scale_lookup_source) + (dst_negative_lookup_source))) /\ (exists ge_balance_positive_lookup_sourcevalue ge_balance_negative_lookup_sourcevalue. (((((z) = 2 * (ge_balance_positive_lookup_sourcevalue) /\ (ge_balance_negative_lookup_sourcevalue) = 0) \/ exists ge_signed_half_lookup_sourcevaluedecode. (((z) = 2 * ge_signed_half_lookup_sourcevaluedecode + 1 /\ (ge_balance_positive_lookup_sourcevalue) = 0) /\ (ge_balance_negative_lookup_sourcevalue) = S ge_signed_half_lookup_sourcevaluedecode))) /\ ((dst_positive_lookup_source) + ge_balance_negative_lookup_sourcevalue = (dst_negative_lookup_source) + ge_balance_positive_lookup_sourcevalue)))))))))