signed_slice_sum_unit_prefix_iff

Exact expanded first-order arithmetic statement

forall F l z. (exists dst_positive_code_unit_source dst_positive_scale_unit_source dst_negative_code_unit_source dst_negative_scale_unit_source. (((F) = (((((dst_positive_code_unit_source) + (dst_positive_scale_unit_source)) * S ((dst_positive_code_unit_source) + (dst_positive_scale_unit_source)) + ((dst_positive_scale_unit_source) + (dst_positive_scale_unit_source))) + (((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) * S ((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) + ((dst_negative_scale_unit_source) + (dst_negative_scale_unit_source)))) * S ((((dst_positive_code_unit_source) + (dst_positive_scale_unit_source)) * S ((dst_positive_code_unit_source) + (dst_positive_scale_unit_source)) + ((dst_positive_scale_unit_source) + (dst_positive_scale_unit_source))) + (((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) * S ((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) + ((dst_negative_scale_unit_source) + (dst_negative_scale_unit_source)))) + ((((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) * S ((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) + ((dst_negative_scale_unit_source) + (dst_negative_scale_unit_source))) + (((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) * S ((dst_negative_code_unit_source) + (dst_negative_scale_unit_source)) + ((dst_negative_scale_unit_source) + (dst_negative_scale_unit_source)))))) /\ (forall dst_index_unit_source. (exists pvs_le_gap_unit_sourcedomain. pvs_le_gap_unit_sourcedomain + (dst_index_unit_source) = (0)) -> exists dst_positive_unit_source dst_negative_unit_source dst_value_unit_source. ((((exists ff_h_pvs_unit_sourceentrypositive. ff_h_pvs_unit_sourceentrypositive + S (dst_positive_unit_source) = S ((S (dst_index_unit_source)) * dst_positive_scale_unit_source)) /\ exists ff_q_pvs_unit_sourceentrypositive. dst_positive_code_unit_source = ff_q_pvs_unit_sourceentrypositive * S ((S (dst_index_unit_source)) * dst_positive_scale_unit_source) + (dst_positive_unit_source))) /\ (((((exists ff_h_pvs_unit_sourceentrynegative. ff_h_pvs_unit_sourceentrynegative + S (dst_negative_unit_source) = S ((S (dst_index_unit_source)) * dst_negative_scale_unit_source)) /\ exists ff_q_pvs_unit_sourceentrynegative. dst_negative_code_unit_source = ff_q_pvs_unit_sourceentrynegative * S ((S (dst_index_unit_source)) * dst_negative_scale_unit_source) + (dst_negative_unit_source))) /\ (exists ge_balance_positive_unit_sourceentryvalue ge_balance_negative_unit_sourceentryvalue. (((((dst_value_unit_source) = 2 * (ge_balance_positive_unit_sourceentryvalue) /\ (ge_balance_negative_unit_sourceentryvalue) = 0) \/ exists ge_signed_half_unit_sourceentryvaluedecode. (((dst_value_unit_source) = 2 * ge_signed_half_unit_sourceentryvaluedecode + 1 /\ (ge_balance_positive_unit_sourceentryvalue) = 0) /\ (ge_balance_negative_unit_sourceentryvalue) = S ge_signed_half_unit_sourceentryvaluedecode))) /\ ((dst_positive_unit_source) + ge_balance_negative_unit_sourceentryvalue = (dst_negative_unit_source) + ge_balance_positive_unit_sourceentryvalue))))))))) -> (((exists srs_slice_unit_slice. ((((exists dst_positive_code_unit_sliceslicesource_table dst_positive_scale_unit_sliceslicesource_table dst_negative_code_unit_sliceslicesource_table dst_negative_scale_unit_sliceslicesource_table. (((F) = (((((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) * S ((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) + ((dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))) * S ((((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) * S ((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) + ((dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))) + ((((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))))) /\ (forall dst_index_unit_sliceslicesource_table. (exists pvs_le_gap_unit_sliceslicesource_tabledomain. pvs_le_gap_unit_sliceslicesource_tabledomain + (dst_index_unit_sliceslicesource_table) = (0)) -> exists dst_positive_unit_sliceslicesource_table dst_negative_unit_sliceslicesource_table dst_value_unit_sliceslicesource_table. ((((exists ff_h_pvs_unit_sliceslicesource_tableentrypositive. ff_h_pvs_unit_sliceslicesource_tableentrypositive + S (dst_positive_unit_sliceslicesource_table) = S ((S (dst_index_unit_sliceslicesource_table)) * dst_positive_scale_unit_sliceslicesource_table)) /\ exists ff_q_pvs_unit_sliceslicesource_tableentrypositive. dst_positive_code_unit_sliceslicesource_table = ff_q_pvs_unit_sliceslicesource_tableentrypositive * S ((S (dst_index_unit_sliceslicesource_table)) * dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_unit_sliceslicesource_table))) /\ (((((exists ff_h_pvs_unit_sliceslicesource_tableentrynegative. ff_h_pvs_unit_sliceslicesource_tableentrynegative + S (dst_negative_unit_sliceslicesource_table) = S ((S (dst_index_unit_sliceslicesource_table)) * dst_negative_scale_unit_sliceslicesource_table)) /\ exists ff_q_pvs_unit_sliceslicesource_tableentrynegative. dst_negative_code_unit_sliceslicesource_table = ff_q_pvs_unit_sliceslicesource_tableentrynegative * S ((S (dst_index_unit_sliceslicesource_table)) * dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_unit_sliceslicesource_table))) /\ (exists ge_balance_positive_unit_sliceslicesource_tableentryvalue ge_balance_negative_unit_sliceslicesource_tableentryvalue. (((((dst_value_unit_sliceslicesource_table) = 2 * (ge_balance_positive_unit_sliceslicesource_tableentryvalue) /\ (ge_balance_negative_unit_sliceslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_unit_sliceslicesource_tableentryvaluedecode. (((dst_value_unit_sliceslicesource_table) = 2 * ge_signed_half_unit_sliceslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_unit_sliceslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_unit_sliceslicesource_tableentryvalue) = S ge_signed_half_unit_sliceslicesource_tableentryvaluedecode))) /\ ((dst_positive_unit_sliceslicesource_table) + ge_balance_negative_unit_sliceslicesource_tableentryvalue = (dst_negative_unit_sliceslicesource_table) + ge_balance_positive_unit_sliceslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_unit_slicesliceoutput_table dst_positive_scale_unit_slicesliceoutput_table dst_negative_code_unit_slicesliceoutput_table dst_negative_scale_unit_slicesliceoutput_table. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) * S ((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) + ((dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))) * S ((((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) * S ((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) + ((dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))) + ((((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))))) /\ (forall dst_index_unit_slicesliceoutput_table. (exists pvs_le_gap_unit_slicesliceoutput_tabledomain. pvs_le_gap_unit_slicesliceoutput_tabledomain + (dst_index_unit_slicesliceoutput_table) = (l)) -> exists dst_positive_unit_slicesliceoutput_table dst_negative_unit_slicesliceoutput_table dst_value_unit_slicesliceoutput_table. ((((exists ff_h_pvs_unit_slicesliceoutput_tableentrypositive. ff_h_pvs_unit_slicesliceoutput_tableentrypositive + S (dst_positive_unit_slicesliceoutput_table) = S ((S (dst_index_unit_slicesliceoutput_table)) * dst_positive_scale_unit_slicesliceoutput_table)) /\ exists ff_q_pvs_unit_slicesliceoutput_tableentrypositive. dst_positive_code_unit_slicesliceoutput_table = ff_q_pvs_unit_slicesliceoutput_tableentrypositive * S ((S (dst_index_unit_slicesliceoutput_table)) * dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_unit_slicesliceoutput_table))) /\ (((((exists ff_h_pvs_unit_slicesliceoutput_tableentrynegative. ff_h_pvs_unit_slicesliceoutput_tableentrynegative + S (dst_negative_unit_slicesliceoutput_table) = S ((S (dst_index_unit_slicesliceoutput_table)) * dst_negative_scale_unit_slicesliceoutput_table)) /\ exists ff_q_pvs_unit_slicesliceoutput_tableentrynegative. dst_negative_code_unit_slicesliceoutput_table = ff_q_pvs_unit_slicesliceoutput_tableentrynegative * S ((S (dst_index_unit_slicesliceoutput_table)) * dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_unit_slicesliceoutput_table))) /\ (exists ge_balance_positive_unit_slicesliceoutput_tableentryvalue ge_balance_negative_unit_slicesliceoutput_tableentryvalue. (((((dst_value_unit_slicesliceoutput_table) = 2 * (ge_balance_positive_unit_slicesliceoutput_tableentryvalue) /\ (ge_balance_negative_unit_slicesliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode. (((dst_value_unit_slicesliceoutput_table) = 2 * ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_unit_slicesliceoutput_tableentryvalue) = S ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode))) /\ ((dst_positive_unit_slicesliceoutput_table) + ge_balance_negative_unit_slicesliceoutput_tableentryvalue = (dst_negative_unit_slicesliceoutput_table) + ge_balance_positive_unit_slicesliceoutput_tableentryvalue))))))))) /\ (forall srs_index_unit_sliceslice. (exists pvs_gap_unit_sliceslicebound. pvs_gap_unit_sliceslicebound + S (srs_index_unit_sliceslice) = (l)) -> exists srs_value_unit_sliceslice. (((exists dst_positive_code_unit_slicesliceentrysource dst_positive_scale_unit_slicesliceentrysource dst_negative_code_unit_slicesliceentrysource dst_negative_scale_unit_slicesliceentrysource dst_positive_unit_slicesliceentrysource dst_negative_unit_slicesliceentrysource. (((F) = (((((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) * S ((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) + ((dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))) * S ((((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) * S ((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) + ((dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))) + ((((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))))) /\ (((((exists ff_h_pvs_unit_slicesliceentrysourcepositive. ff_h_pvs_unit_slicesliceentrysourcepositive + S (dst_positive_unit_slicesliceentrysource) = S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_positive_scale_unit_slicesliceentrysource)) /\ exists ff_q_pvs_unit_slicesliceentrysourcepositive. dst_positive_code_unit_slicesliceentrysource = ff_q_pvs_unit_slicesliceentrysourcepositive * S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_unit_slicesliceentrysource))) /\ (((((exists ff_h_pvs_unit_slicesliceentrysourcenegative. ff_h_pvs_unit_slicesliceentrysourcenegative + S (dst_negative_unit_slicesliceentrysource) = S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_negative_scale_unit_slicesliceentrysource)) /\ exists ff_q_pvs_unit_slicesliceentrysourcenegative. dst_negative_code_unit_slicesliceentrysource = ff_q_pvs_unit_slicesliceentrysourcenegative * S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_unit_slicesliceentrysource))) /\ (exists ge_balance_positive_unit_slicesliceentrysourcevalue ge_balance_negative_unit_slicesliceentrysourcevalue. (((((srs_value_unit_sliceslice) = 2 * (ge_balance_positive_unit_slicesliceentrysourcevalue) /\ (ge_balance_negative_unit_slicesliceentrysourcevalue) = 0) \/ exists ge_signed_half_unit_slicesliceentrysourcevaluedecode. (((srs_value_unit_sliceslice) = 2 * ge_signed_half_unit_slicesliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceentrysourcevalue) = 0) /\ (ge_balance_negative_unit_slicesliceentrysourcevalue) = S ge_signed_half_unit_slicesliceentrysourcevaluedecode))) /\ ((dst_positive_unit_slicesliceentrysource) + ge_balance_negative_unit_slicesliceentrysourcevalue = (dst_negative_unit_slicesliceentrysource) + ge_balance_positive_unit_slicesliceentrysourcevalue))))))))) /\ (exists dst_positive_code_unit_slicesliceentryoutput dst_positive_scale_unit_slicesliceentryoutput dst_negative_code_unit_slicesliceentryoutput dst_negative_scale_unit_slicesliceentryoutput dst_positive_unit_slicesliceentryoutput dst_negative_unit_slicesliceentryoutput. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) * S ((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) + ((dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))) * S ((((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) * S ((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) + ((dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))) + ((((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))))) /\ (((((exists ff_h_pvs_unit_slicesliceentryoutputpositive. ff_h_pvs_unit_slicesliceentryoutputpositive + S (dst_positive_unit_slicesliceentryoutput) = S ((S (srs_index_unit_sliceslice)) * dst_positive_scale_unit_slicesliceentryoutput)) /\ exists ff_q_pvs_unit_slicesliceentryoutputpositive. dst_positive_code_unit_slicesliceentryoutput = ff_q_pvs_unit_slicesliceentryoutputpositive * S ((S (srs_index_unit_sliceslice)) * dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_unit_slicesliceentryoutput))) /\ (((((exists ff_h_pvs_unit_slicesliceentryoutputnegative. ff_h_pvs_unit_slicesliceentryoutputnegative + S (dst_negative_unit_slicesliceentryoutput) = S ((S (srs_index_unit_sliceslice)) * dst_negative_scale_unit_slicesliceentryoutput)) /\ exists ff_q_pvs_unit_slicesliceentryoutputnegative. dst_negative_code_unit_slicesliceentryoutput = ff_q_pvs_unit_slicesliceentryoutputnegative * S ((S (srs_index_unit_sliceslice)) * dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_unit_slicesliceentryoutput))) /\ (exists ge_balance_positive_unit_slicesliceentryoutputvalue ge_balance_negative_unit_slicesliceentryoutputvalue. (((((srs_value_unit_sliceslice) = 2 * (ge_balance_positive_unit_slicesliceentryoutputvalue) /\ (ge_balance_negative_unit_slicesliceentryoutputvalue) = 0) \/ exists ge_signed_half_unit_slicesliceentryoutputvaluedecode. (((srs_value_unit_sliceslice) = 2 * ge_signed_half_unit_slicesliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceentryoutputvalue) = 0) /\ (ge_balance_negative_unit_slicesliceentryoutputvalue) = S ge_signed_half_unit_slicesliceentryoutputvaluedecode))) /\ ((dst_positive_unit_slicesliceentryoutput) + ge_balance_negative_unit_slicesliceentryoutputvalue = (dst_negative_unit_slicesliceentryoutput) + ge_balance_positive_unit_slicesliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_unit_slicesum dst_positive_scale_unit_slicesum dst_negative_code_unit_slicesum dst_negative_scale_unit_slicesum dst_positive_sum_unit_slicesum dst_negative_sum_unit_slicesum. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) * S ((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) + ((dst_positive_scale_unit_slicesum) + (dst_positive_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))) * S ((((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) * S ((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) + ((dst_positive_scale_unit_slicesum) + (dst_positive_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))) + ((((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))))) /\ (((exists fs_u_dst_unit_slicesumpositive fs_v_dst_unit_slicesumpositive. ((((exists fs_h_dst_unit_slicesumpositive_body_start. fs_h_dst_unit_slicesumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_start. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_start * S ((S (0)) * fs_v_dst_unit_slicesumpositive) + (0))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_terminal. fs_h_dst_unit_slicesumpositive_body_terminal + S (dst_positive_sum_unit_slicesum) = S ((S (l)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_terminal. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_terminal * S ((S (l)) * fs_v_dst_unit_slicesumpositive) + (dst_positive_sum_unit_slicesum))) /\ forall fs_i_dst_unit_slicesumpositive_body_steps. (exists fs_lt_dst_unit_slicesumpositive_body_steps_bound. fs_lt_dst_unit_slicesumpositive_body_steps_bound + S fs_i_dst_unit_slicesumpositive_body_steps = l) -> exists fs_a_dst_unit_slicesumpositive_body_steps fs_r_dst_unit_slicesumpositive_body_steps fs_s_dst_unit_slicesumpositive_body_steps. ((((exists fs_h_dst_unit_slicesumpositive_body_steps_summand. fs_h_dst_unit_slicesumpositive_body_steps_summand + S (fs_a_dst_unit_slicesumpositive_body_steps) = S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * dst_positive_scale_unit_slicesum)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_summand. dst_positive_code_unit_slicesum = fs_q_dst_unit_slicesumpositive_body_steps_summand * S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * dst_positive_scale_unit_slicesum) + (fs_a_dst_unit_slicesumpositive_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_steps_partial. fs_h_dst_unit_slicesumpositive_body_steps_partial + S (fs_r_dst_unit_slicesumpositive_body_steps) = S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_partial. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_steps_partial * S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive) + (fs_r_dst_unit_slicesumpositive_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_steps_successor. fs_h_dst_unit_slicesumpositive_body_steps_successor + S (fs_s_dst_unit_slicesumpositive_body_steps) = S ((S (S fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_successor. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_steps_successor * S ((S (S fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive) + (fs_s_dst_unit_slicesumpositive_body_steps))) /\ fs_s_dst_unit_slicesumpositive_body_steps = fs_r_dst_unit_slicesumpositive_body_steps + fs_a_dst_unit_slicesumpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_slicesumnegative fs_v_dst_unit_slicesumnegative. ((((exists fs_h_dst_unit_slicesumnegative_body_start. fs_h_dst_unit_slicesumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_start. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_start * S ((S (0)) * fs_v_dst_unit_slicesumnegative) + (0))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_terminal. fs_h_dst_unit_slicesumnegative_body_terminal + S (dst_negative_sum_unit_slicesum) = S ((S (l)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_terminal. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_terminal * S ((S (l)) * fs_v_dst_unit_slicesumnegative) + (dst_negative_sum_unit_slicesum))) /\ forall fs_i_dst_unit_slicesumnegative_body_steps. (exists fs_lt_dst_unit_slicesumnegative_body_steps_bound. fs_lt_dst_unit_slicesumnegative_body_steps_bound + S fs_i_dst_unit_slicesumnegative_body_steps = l) -> exists fs_a_dst_unit_slicesumnegative_body_steps fs_r_dst_unit_slicesumnegative_body_steps fs_s_dst_unit_slicesumnegative_body_steps. ((((exists fs_h_dst_unit_slicesumnegative_body_steps_summand. fs_h_dst_unit_slicesumnegative_body_steps_summand + S (fs_a_dst_unit_slicesumnegative_body_steps) = S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * dst_negative_scale_unit_slicesum)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_summand. dst_negative_code_unit_slicesum = fs_q_dst_unit_slicesumnegative_body_steps_summand * S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * dst_negative_scale_unit_slicesum) + (fs_a_dst_unit_slicesumnegative_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_steps_partial. fs_h_dst_unit_slicesumnegative_body_steps_partial + S (fs_r_dst_unit_slicesumnegative_body_steps) = S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_partial. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_steps_partial * S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative) + (fs_r_dst_unit_slicesumnegative_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_steps_successor. fs_h_dst_unit_slicesumnegative_body_steps_successor + S (fs_s_dst_unit_slicesumnegative_body_steps) = S ((S (S fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_successor. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_steps_successor * S ((S (S fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative) + (fs_s_dst_unit_slicesumnegative_body_steps))) /\ fs_s_dst_unit_slicesumnegative_body_steps = fs_r_dst_unit_slicesumnegative_body_steps + fs_a_dst_unit_slicesumnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_slicesumresult ge_balance_negative_unit_slicesumresult. (((((z) = 2 * (ge_balance_positive_unit_slicesumresult) /\ (ge_balance_negative_unit_slicesumresult) = 0) \/ exists ge_signed_half_unit_slicesumresultdecode. (((z) = 2 * ge_signed_half_unit_slicesumresultdecode + 1 /\ (ge_balance_positive_unit_slicesumresult) = 0) /\ (ge_balance_negative_unit_slicesumresult) = S ge_signed_half_unit_slicesumresultdecode))) /\ ((dst_positive_sum_unit_slicesum) + ge_balance_negative_unit_slicesumresult = (dst_negative_sum_unit_slicesum) + ge_balance_positive_unit_slicesumresult))))))))))) -> (exists dst_positive_code_unit_prefix dst_positive_scale_unit_prefix dst_negative_code_unit_prefix dst_negative_scale_unit_prefix dst_positive_sum_unit_prefix dst_negative_sum_unit_prefix. (((F) = (((((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) * S ((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) + ((dst_positive_scale_unit_prefix) + (dst_positive_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))) * S ((((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) * S ((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) + ((dst_positive_scale_unit_prefix) + (dst_positive_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))) + ((((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))))) /\ (((exists fs_u_dst_unit_prefixpositive fs_v_dst_unit_prefixpositive. ((((exists fs_h_dst_unit_prefixpositive_body_start. fs_h_dst_unit_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_start. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_start * S ((S (0)) * fs_v_dst_unit_prefixpositive) + (0))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_terminal. fs_h_dst_unit_prefixpositive_body_terminal + S (dst_positive_sum_unit_prefix) = S ((S (l)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_terminal. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_unit_prefixpositive) + (dst_positive_sum_unit_prefix))) /\ forall fs_i_dst_unit_prefixpositive_body_steps. (exists fs_lt_dst_unit_prefixpositive_body_steps_bound. fs_lt_dst_unit_prefixpositive_body_steps_bound + S fs_i_dst_unit_prefixpositive_body_steps = l) -> exists fs_a_dst_unit_prefixpositive_body_steps fs_r_dst_unit_prefixpositive_body_steps fs_s_dst_unit_prefixpositive_body_steps. ((((exists fs_h_dst_unit_prefixpositive_body_steps_summand. fs_h_dst_unit_prefixpositive_body_steps_summand + S (fs_a_dst_unit_prefixpositive_body_steps) = S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * dst_positive_scale_unit_prefix)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_summand. dst_positive_code_unit_prefix = fs_q_dst_unit_prefixpositive_body_steps_summand * S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * dst_positive_scale_unit_prefix) + (fs_a_dst_unit_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_steps_partial. fs_h_dst_unit_prefixpositive_body_steps_partial + S (fs_r_dst_unit_prefixpositive_body_steps) = S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_partial. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_steps_partial * S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive) + (fs_r_dst_unit_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_steps_successor. fs_h_dst_unit_prefixpositive_body_steps_successor + S (fs_s_dst_unit_prefixpositive_body_steps) = S ((S (S fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_successor. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive) + (fs_s_dst_unit_prefixpositive_body_steps))) /\ fs_s_dst_unit_prefixpositive_body_steps = fs_r_dst_unit_prefixpositive_body_steps + fs_a_dst_unit_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_prefixnegative fs_v_dst_unit_prefixnegative. ((((exists fs_h_dst_unit_prefixnegative_body_start. fs_h_dst_unit_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_start. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_start * S ((S (0)) * fs_v_dst_unit_prefixnegative) + (0))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_terminal. fs_h_dst_unit_prefixnegative_body_terminal + S (dst_negative_sum_unit_prefix) = S ((S (l)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_terminal. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_unit_prefixnegative) + (dst_negative_sum_unit_prefix))) /\ forall fs_i_dst_unit_prefixnegative_body_steps. (exists fs_lt_dst_unit_prefixnegative_body_steps_bound. fs_lt_dst_unit_prefixnegative_body_steps_bound + S fs_i_dst_unit_prefixnegative_body_steps = l) -> exists fs_a_dst_unit_prefixnegative_body_steps fs_r_dst_unit_prefixnegative_body_steps fs_s_dst_unit_prefixnegative_body_steps. ((((exists fs_h_dst_unit_prefixnegative_body_steps_summand. fs_h_dst_unit_prefixnegative_body_steps_summand + S (fs_a_dst_unit_prefixnegative_body_steps) = S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * dst_negative_scale_unit_prefix)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_summand. dst_negative_code_unit_prefix = fs_q_dst_unit_prefixnegative_body_steps_summand * S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * dst_negative_scale_unit_prefix) + (fs_a_dst_unit_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_steps_partial. fs_h_dst_unit_prefixnegative_body_steps_partial + S (fs_r_dst_unit_prefixnegative_body_steps) = S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_partial. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_steps_partial * S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative) + (fs_r_dst_unit_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_steps_successor. fs_h_dst_unit_prefixnegative_body_steps_successor + S (fs_s_dst_unit_prefixnegative_body_steps) = S ((S (S fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_successor. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative) + (fs_s_dst_unit_prefixnegative_body_steps))) /\ fs_s_dst_unit_prefixnegative_body_steps = fs_r_dst_unit_prefixnegative_body_steps + fs_a_dst_unit_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_prefixresult ge_balance_negative_unit_prefixresult. (((((z) = 2 * (ge_balance_positive_unit_prefixresult) /\ (ge_balance_negative_unit_prefixresult) = 0) \/ exists ge_signed_half_unit_prefixresultdecode. (((z) = 2 * ge_signed_half_unit_prefixresultdecode + 1 /\ (ge_balance_positive_unit_prefixresult) = 0) /\ (ge_balance_negative_unit_prefixresult) = S ge_signed_half_unit_prefixresultdecode))) /\ ((dst_positive_sum_unit_prefix) + ge_balance_negative_unit_prefixresult = (dst_negative_sum_unit_prefix) + ge_balance_positive_unit_prefixresult)))))))))) /\ ((exists dst_positive_code_unit_prefix dst_positive_scale_unit_prefix dst_negative_code_unit_prefix dst_negative_scale_unit_prefix dst_positive_sum_unit_prefix dst_negative_sum_unit_prefix. (((F) = (((((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) * S ((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) + ((dst_positive_scale_unit_prefix) + (dst_positive_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))) * S ((((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) * S ((dst_positive_code_unit_prefix) + (dst_positive_scale_unit_prefix)) + ((dst_positive_scale_unit_prefix) + (dst_positive_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))) + ((((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix))) + (((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) * S ((dst_negative_code_unit_prefix) + (dst_negative_scale_unit_prefix)) + ((dst_negative_scale_unit_prefix) + (dst_negative_scale_unit_prefix)))))) /\ (((exists fs_u_dst_unit_prefixpositive fs_v_dst_unit_prefixpositive. ((((exists fs_h_dst_unit_prefixpositive_body_start. fs_h_dst_unit_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_start. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_start * S ((S (0)) * fs_v_dst_unit_prefixpositive) + (0))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_terminal. fs_h_dst_unit_prefixpositive_body_terminal + S (dst_positive_sum_unit_prefix) = S ((S (l)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_terminal. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_unit_prefixpositive) + (dst_positive_sum_unit_prefix))) /\ forall fs_i_dst_unit_prefixpositive_body_steps. (exists fs_lt_dst_unit_prefixpositive_body_steps_bound. fs_lt_dst_unit_prefixpositive_body_steps_bound + S fs_i_dst_unit_prefixpositive_body_steps = l) -> exists fs_a_dst_unit_prefixpositive_body_steps fs_r_dst_unit_prefixpositive_body_steps fs_s_dst_unit_prefixpositive_body_steps. ((((exists fs_h_dst_unit_prefixpositive_body_steps_summand. fs_h_dst_unit_prefixpositive_body_steps_summand + S (fs_a_dst_unit_prefixpositive_body_steps) = S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * dst_positive_scale_unit_prefix)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_summand. dst_positive_code_unit_prefix = fs_q_dst_unit_prefixpositive_body_steps_summand * S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * dst_positive_scale_unit_prefix) + (fs_a_dst_unit_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_steps_partial. fs_h_dst_unit_prefixpositive_body_steps_partial + S (fs_r_dst_unit_prefixpositive_body_steps) = S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_partial. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_steps_partial * S ((S (fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive) + (fs_r_dst_unit_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_unit_prefixpositive_body_steps_successor. fs_h_dst_unit_prefixpositive_body_steps_successor + S (fs_s_dst_unit_prefixpositive_body_steps) = S ((S (S fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive)) /\ exists fs_q_dst_unit_prefixpositive_body_steps_successor. fs_u_dst_unit_prefixpositive = fs_q_dst_unit_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_unit_prefixpositive_body_steps)) * fs_v_dst_unit_prefixpositive) + (fs_s_dst_unit_prefixpositive_body_steps))) /\ fs_s_dst_unit_prefixpositive_body_steps = fs_r_dst_unit_prefixpositive_body_steps + fs_a_dst_unit_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_prefixnegative fs_v_dst_unit_prefixnegative. ((((exists fs_h_dst_unit_prefixnegative_body_start. fs_h_dst_unit_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_start. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_start * S ((S (0)) * fs_v_dst_unit_prefixnegative) + (0))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_terminal. fs_h_dst_unit_prefixnegative_body_terminal + S (dst_negative_sum_unit_prefix) = S ((S (l)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_terminal. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_unit_prefixnegative) + (dst_negative_sum_unit_prefix))) /\ forall fs_i_dst_unit_prefixnegative_body_steps. (exists fs_lt_dst_unit_prefixnegative_body_steps_bound. fs_lt_dst_unit_prefixnegative_body_steps_bound + S fs_i_dst_unit_prefixnegative_body_steps = l) -> exists fs_a_dst_unit_prefixnegative_body_steps fs_r_dst_unit_prefixnegative_body_steps fs_s_dst_unit_prefixnegative_body_steps. ((((exists fs_h_dst_unit_prefixnegative_body_steps_summand. fs_h_dst_unit_prefixnegative_body_steps_summand + S (fs_a_dst_unit_prefixnegative_body_steps) = S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * dst_negative_scale_unit_prefix)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_summand. dst_negative_code_unit_prefix = fs_q_dst_unit_prefixnegative_body_steps_summand * S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * dst_negative_scale_unit_prefix) + (fs_a_dst_unit_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_steps_partial. fs_h_dst_unit_prefixnegative_body_steps_partial + S (fs_r_dst_unit_prefixnegative_body_steps) = S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_partial. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_steps_partial * S ((S (fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative) + (fs_r_dst_unit_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_unit_prefixnegative_body_steps_successor. fs_h_dst_unit_prefixnegative_body_steps_successor + S (fs_s_dst_unit_prefixnegative_body_steps) = S ((S (S fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative)) /\ exists fs_q_dst_unit_prefixnegative_body_steps_successor. fs_u_dst_unit_prefixnegative = fs_q_dst_unit_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_unit_prefixnegative_body_steps)) * fs_v_dst_unit_prefixnegative) + (fs_s_dst_unit_prefixnegative_body_steps))) /\ fs_s_dst_unit_prefixnegative_body_steps = fs_r_dst_unit_prefixnegative_body_steps + fs_a_dst_unit_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_prefixresult ge_balance_negative_unit_prefixresult. (((((z) = 2 * (ge_balance_positive_unit_prefixresult) /\ (ge_balance_negative_unit_prefixresult) = 0) \/ exists ge_signed_half_unit_prefixresultdecode. (((z) = 2 * ge_signed_half_unit_prefixresultdecode + 1 /\ (ge_balance_positive_unit_prefixresult) = 0) /\ (ge_balance_negative_unit_prefixresult) = S ge_signed_half_unit_prefixresultdecode))) /\ ((dst_positive_sum_unit_prefix) + ge_balance_negative_unit_prefixresult = (dst_negative_sum_unit_prefix) + ge_balance_positive_unit_prefixresult))))))))) -> (exists srs_slice_unit_slice. ((((exists dst_positive_code_unit_sliceslicesource_table dst_positive_scale_unit_sliceslicesource_table dst_negative_code_unit_sliceslicesource_table dst_negative_scale_unit_sliceslicesource_table. (((F) = (((((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) * S ((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) + ((dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))) * S ((((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) * S ((dst_positive_code_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table)) + ((dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))) + ((((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table))) + (((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) * S ((dst_negative_code_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)) + ((dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_scale_unit_sliceslicesource_table)))))) /\ (forall dst_index_unit_sliceslicesource_table. (exists pvs_le_gap_unit_sliceslicesource_tabledomain. pvs_le_gap_unit_sliceslicesource_tabledomain + (dst_index_unit_sliceslicesource_table) = (0)) -> exists dst_positive_unit_sliceslicesource_table dst_negative_unit_sliceslicesource_table dst_value_unit_sliceslicesource_table. ((((exists ff_h_pvs_unit_sliceslicesource_tableentrypositive. ff_h_pvs_unit_sliceslicesource_tableentrypositive + S (dst_positive_unit_sliceslicesource_table) = S ((S (dst_index_unit_sliceslicesource_table)) * dst_positive_scale_unit_sliceslicesource_table)) /\ exists ff_q_pvs_unit_sliceslicesource_tableentrypositive. dst_positive_code_unit_sliceslicesource_table = ff_q_pvs_unit_sliceslicesource_tableentrypositive * S ((S (dst_index_unit_sliceslicesource_table)) * dst_positive_scale_unit_sliceslicesource_table) + (dst_positive_unit_sliceslicesource_table))) /\ (((((exists ff_h_pvs_unit_sliceslicesource_tableentrynegative. ff_h_pvs_unit_sliceslicesource_tableentrynegative + S (dst_negative_unit_sliceslicesource_table) = S ((S (dst_index_unit_sliceslicesource_table)) * dst_negative_scale_unit_sliceslicesource_table)) /\ exists ff_q_pvs_unit_sliceslicesource_tableentrynegative. dst_negative_code_unit_sliceslicesource_table = ff_q_pvs_unit_sliceslicesource_tableentrynegative * S ((S (dst_index_unit_sliceslicesource_table)) * dst_negative_scale_unit_sliceslicesource_table) + (dst_negative_unit_sliceslicesource_table))) /\ (exists ge_balance_positive_unit_sliceslicesource_tableentryvalue ge_balance_negative_unit_sliceslicesource_tableentryvalue. (((((dst_value_unit_sliceslicesource_table) = 2 * (ge_balance_positive_unit_sliceslicesource_tableentryvalue) /\ (ge_balance_negative_unit_sliceslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_unit_sliceslicesource_tableentryvaluedecode. (((dst_value_unit_sliceslicesource_table) = 2 * ge_signed_half_unit_sliceslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_unit_sliceslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_unit_sliceslicesource_tableentryvalue) = S ge_signed_half_unit_sliceslicesource_tableentryvaluedecode))) /\ ((dst_positive_unit_sliceslicesource_table) + ge_balance_negative_unit_sliceslicesource_tableentryvalue = (dst_negative_unit_sliceslicesource_table) + ge_balance_positive_unit_sliceslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_unit_slicesliceoutput_table dst_positive_scale_unit_slicesliceoutput_table dst_negative_code_unit_slicesliceoutput_table dst_negative_scale_unit_slicesliceoutput_table. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) * S ((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) + ((dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))) * S ((((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) * S ((dst_positive_code_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table)) + ((dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))) + ((((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table))) + (((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) * S ((dst_negative_code_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)) + ((dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_scale_unit_slicesliceoutput_table)))))) /\ (forall dst_index_unit_slicesliceoutput_table. (exists pvs_le_gap_unit_slicesliceoutput_tabledomain. pvs_le_gap_unit_slicesliceoutput_tabledomain + (dst_index_unit_slicesliceoutput_table) = (l)) -> exists dst_positive_unit_slicesliceoutput_table dst_negative_unit_slicesliceoutput_table dst_value_unit_slicesliceoutput_table. ((((exists ff_h_pvs_unit_slicesliceoutput_tableentrypositive. ff_h_pvs_unit_slicesliceoutput_tableentrypositive + S (dst_positive_unit_slicesliceoutput_table) = S ((S (dst_index_unit_slicesliceoutput_table)) * dst_positive_scale_unit_slicesliceoutput_table)) /\ exists ff_q_pvs_unit_slicesliceoutput_tableentrypositive. dst_positive_code_unit_slicesliceoutput_table = ff_q_pvs_unit_slicesliceoutput_tableentrypositive * S ((S (dst_index_unit_slicesliceoutput_table)) * dst_positive_scale_unit_slicesliceoutput_table) + (dst_positive_unit_slicesliceoutput_table))) /\ (((((exists ff_h_pvs_unit_slicesliceoutput_tableentrynegative. ff_h_pvs_unit_slicesliceoutput_tableentrynegative + S (dst_negative_unit_slicesliceoutput_table) = S ((S (dst_index_unit_slicesliceoutput_table)) * dst_negative_scale_unit_slicesliceoutput_table)) /\ exists ff_q_pvs_unit_slicesliceoutput_tableentrynegative. dst_negative_code_unit_slicesliceoutput_table = ff_q_pvs_unit_slicesliceoutput_tableentrynegative * S ((S (dst_index_unit_slicesliceoutput_table)) * dst_negative_scale_unit_slicesliceoutput_table) + (dst_negative_unit_slicesliceoutput_table))) /\ (exists ge_balance_positive_unit_slicesliceoutput_tableentryvalue ge_balance_negative_unit_slicesliceoutput_tableentryvalue. (((((dst_value_unit_slicesliceoutput_table) = 2 * (ge_balance_positive_unit_slicesliceoutput_tableentryvalue) /\ (ge_balance_negative_unit_slicesliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode. (((dst_value_unit_slicesliceoutput_table) = 2 * ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_unit_slicesliceoutput_tableentryvalue) = S ge_signed_half_unit_slicesliceoutput_tableentryvaluedecode))) /\ ((dst_positive_unit_slicesliceoutput_table) + ge_balance_negative_unit_slicesliceoutput_tableentryvalue = (dst_negative_unit_slicesliceoutput_table) + ge_balance_positive_unit_slicesliceoutput_tableentryvalue))))))))) /\ (forall srs_index_unit_sliceslice. (exists pvs_gap_unit_sliceslicebound. pvs_gap_unit_sliceslicebound + S (srs_index_unit_sliceslice) = (l)) -> exists srs_value_unit_sliceslice. (((exists dst_positive_code_unit_slicesliceentrysource dst_positive_scale_unit_slicesliceentrysource dst_negative_code_unit_slicesliceentrysource dst_negative_scale_unit_slicesliceentrysource dst_positive_unit_slicesliceentrysource dst_negative_unit_slicesliceentrysource. (((F) = (((((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) * S ((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) + ((dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))) * S ((((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) * S ((dst_positive_code_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource)) + ((dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))) + ((((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource))) + (((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) * S ((dst_negative_code_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)) + ((dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_scale_unit_slicesliceentrysource)))))) /\ (((((exists ff_h_pvs_unit_slicesliceentrysourcepositive. ff_h_pvs_unit_slicesliceentrysourcepositive + S (dst_positive_unit_slicesliceentrysource) = S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_positive_scale_unit_slicesliceentrysource)) /\ exists ff_q_pvs_unit_slicesliceentrysourcepositive. dst_positive_code_unit_slicesliceentrysource = ff_q_pvs_unit_slicesliceentrysourcepositive * S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_positive_scale_unit_slicesliceentrysource) + (dst_positive_unit_slicesliceentrysource))) /\ (((((exists ff_h_pvs_unit_slicesliceentrysourcenegative. ff_h_pvs_unit_slicesliceentrysourcenegative + S (dst_negative_unit_slicesliceentrysource) = S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_negative_scale_unit_slicesliceentrysource)) /\ exists ff_q_pvs_unit_slicesliceentrysourcenegative. dst_negative_code_unit_slicesliceentrysource = ff_q_pvs_unit_slicesliceentrysourcenegative * S ((S (((0) + ((1) * (srs_index_unit_sliceslice))))) * dst_negative_scale_unit_slicesliceentrysource) + (dst_negative_unit_slicesliceentrysource))) /\ (exists ge_balance_positive_unit_slicesliceentrysourcevalue ge_balance_negative_unit_slicesliceentrysourcevalue. (((((srs_value_unit_sliceslice) = 2 * (ge_balance_positive_unit_slicesliceentrysourcevalue) /\ (ge_balance_negative_unit_slicesliceentrysourcevalue) = 0) \/ exists ge_signed_half_unit_slicesliceentrysourcevaluedecode. (((srs_value_unit_sliceslice) = 2 * ge_signed_half_unit_slicesliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceentrysourcevalue) = 0) /\ (ge_balance_negative_unit_slicesliceentrysourcevalue) = S ge_signed_half_unit_slicesliceentrysourcevaluedecode))) /\ ((dst_positive_unit_slicesliceentrysource) + ge_balance_negative_unit_slicesliceentrysourcevalue = (dst_negative_unit_slicesliceentrysource) + ge_balance_positive_unit_slicesliceentrysourcevalue))))))))) /\ (exists dst_positive_code_unit_slicesliceentryoutput dst_positive_scale_unit_slicesliceentryoutput dst_negative_code_unit_slicesliceentryoutput dst_negative_scale_unit_slicesliceentryoutput dst_positive_unit_slicesliceentryoutput dst_negative_unit_slicesliceentryoutput. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) * S ((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) + ((dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))) * S ((((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) * S ((dst_positive_code_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput)) + ((dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))) + ((((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput))) + (((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) * S ((dst_negative_code_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)) + ((dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_scale_unit_slicesliceentryoutput)))))) /\ (((((exists ff_h_pvs_unit_slicesliceentryoutputpositive. ff_h_pvs_unit_slicesliceentryoutputpositive + S (dst_positive_unit_slicesliceentryoutput) = S ((S (srs_index_unit_sliceslice)) * dst_positive_scale_unit_slicesliceentryoutput)) /\ exists ff_q_pvs_unit_slicesliceentryoutputpositive. dst_positive_code_unit_slicesliceentryoutput = ff_q_pvs_unit_slicesliceentryoutputpositive * S ((S (srs_index_unit_sliceslice)) * dst_positive_scale_unit_slicesliceentryoutput) + (dst_positive_unit_slicesliceentryoutput))) /\ (((((exists ff_h_pvs_unit_slicesliceentryoutputnegative. ff_h_pvs_unit_slicesliceentryoutputnegative + S (dst_negative_unit_slicesliceentryoutput) = S ((S (srs_index_unit_sliceslice)) * dst_negative_scale_unit_slicesliceentryoutput)) /\ exists ff_q_pvs_unit_slicesliceentryoutputnegative. dst_negative_code_unit_slicesliceentryoutput = ff_q_pvs_unit_slicesliceentryoutputnegative * S ((S (srs_index_unit_sliceslice)) * dst_negative_scale_unit_slicesliceentryoutput) + (dst_negative_unit_slicesliceentryoutput))) /\ (exists ge_balance_positive_unit_slicesliceentryoutputvalue ge_balance_negative_unit_slicesliceentryoutputvalue. (((((srs_value_unit_sliceslice) = 2 * (ge_balance_positive_unit_slicesliceentryoutputvalue) /\ (ge_balance_negative_unit_slicesliceentryoutputvalue) = 0) \/ exists ge_signed_half_unit_slicesliceentryoutputvaluedecode. (((srs_value_unit_sliceslice) = 2 * ge_signed_half_unit_slicesliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_unit_slicesliceentryoutputvalue) = 0) /\ (ge_balance_negative_unit_slicesliceentryoutputvalue) = S ge_signed_half_unit_slicesliceentryoutputvaluedecode))) /\ ((dst_positive_unit_slicesliceentryoutput) + ge_balance_negative_unit_slicesliceentryoutputvalue = (dst_negative_unit_slicesliceentryoutput) + ge_balance_positive_unit_slicesliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_unit_slicesum dst_positive_scale_unit_slicesum dst_negative_code_unit_slicesum dst_negative_scale_unit_slicesum dst_positive_sum_unit_slicesum dst_negative_sum_unit_slicesum. (((srs_slice_unit_slice) = (((((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) * S ((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) + ((dst_positive_scale_unit_slicesum) + (dst_positive_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))) * S ((((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) * S ((dst_positive_code_unit_slicesum) + (dst_positive_scale_unit_slicesum)) + ((dst_positive_scale_unit_slicesum) + (dst_positive_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))) + ((((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum))) + (((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) * S ((dst_negative_code_unit_slicesum) + (dst_negative_scale_unit_slicesum)) + ((dst_negative_scale_unit_slicesum) + (dst_negative_scale_unit_slicesum)))))) /\ (((exists fs_u_dst_unit_slicesumpositive fs_v_dst_unit_slicesumpositive. ((((exists fs_h_dst_unit_slicesumpositive_body_start. fs_h_dst_unit_slicesumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_start. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_start * S ((S (0)) * fs_v_dst_unit_slicesumpositive) + (0))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_terminal. fs_h_dst_unit_slicesumpositive_body_terminal + S (dst_positive_sum_unit_slicesum) = S ((S (l)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_terminal. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_terminal * S ((S (l)) * fs_v_dst_unit_slicesumpositive) + (dst_positive_sum_unit_slicesum))) /\ forall fs_i_dst_unit_slicesumpositive_body_steps. (exists fs_lt_dst_unit_slicesumpositive_body_steps_bound. fs_lt_dst_unit_slicesumpositive_body_steps_bound + S fs_i_dst_unit_slicesumpositive_body_steps = l) -> exists fs_a_dst_unit_slicesumpositive_body_steps fs_r_dst_unit_slicesumpositive_body_steps fs_s_dst_unit_slicesumpositive_body_steps. ((((exists fs_h_dst_unit_slicesumpositive_body_steps_summand. fs_h_dst_unit_slicesumpositive_body_steps_summand + S (fs_a_dst_unit_slicesumpositive_body_steps) = S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * dst_positive_scale_unit_slicesum)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_summand. dst_positive_code_unit_slicesum = fs_q_dst_unit_slicesumpositive_body_steps_summand * S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * dst_positive_scale_unit_slicesum) + (fs_a_dst_unit_slicesumpositive_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_steps_partial. fs_h_dst_unit_slicesumpositive_body_steps_partial + S (fs_r_dst_unit_slicesumpositive_body_steps) = S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_partial. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_steps_partial * S ((S (fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive) + (fs_r_dst_unit_slicesumpositive_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumpositive_body_steps_successor. fs_h_dst_unit_slicesumpositive_body_steps_successor + S (fs_s_dst_unit_slicesumpositive_body_steps) = S ((S (S fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive)) /\ exists fs_q_dst_unit_slicesumpositive_body_steps_successor. fs_u_dst_unit_slicesumpositive = fs_q_dst_unit_slicesumpositive_body_steps_successor * S ((S (S fs_i_dst_unit_slicesumpositive_body_steps)) * fs_v_dst_unit_slicesumpositive) + (fs_s_dst_unit_slicesumpositive_body_steps))) /\ fs_s_dst_unit_slicesumpositive_body_steps = fs_r_dst_unit_slicesumpositive_body_steps + fs_a_dst_unit_slicesumpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_slicesumnegative fs_v_dst_unit_slicesumnegative. ((((exists fs_h_dst_unit_slicesumnegative_body_start. fs_h_dst_unit_slicesumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_start. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_start * S ((S (0)) * fs_v_dst_unit_slicesumnegative) + (0))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_terminal. fs_h_dst_unit_slicesumnegative_body_terminal + S (dst_negative_sum_unit_slicesum) = S ((S (l)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_terminal. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_terminal * S ((S (l)) * fs_v_dst_unit_slicesumnegative) + (dst_negative_sum_unit_slicesum))) /\ forall fs_i_dst_unit_slicesumnegative_body_steps. (exists fs_lt_dst_unit_slicesumnegative_body_steps_bound. fs_lt_dst_unit_slicesumnegative_body_steps_bound + S fs_i_dst_unit_slicesumnegative_body_steps = l) -> exists fs_a_dst_unit_slicesumnegative_body_steps fs_r_dst_unit_slicesumnegative_body_steps fs_s_dst_unit_slicesumnegative_body_steps. ((((exists fs_h_dst_unit_slicesumnegative_body_steps_summand. fs_h_dst_unit_slicesumnegative_body_steps_summand + S (fs_a_dst_unit_slicesumnegative_body_steps) = S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * dst_negative_scale_unit_slicesum)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_summand. dst_negative_code_unit_slicesum = fs_q_dst_unit_slicesumnegative_body_steps_summand * S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * dst_negative_scale_unit_slicesum) + (fs_a_dst_unit_slicesumnegative_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_steps_partial. fs_h_dst_unit_slicesumnegative_body_steps_partial + S (fs_r_dst_unit_slicesumnegative_body_steps) = S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_partial. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_steps_partial * S ((S (fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative) + (fs_r_dst_unit_slicesumnegative_body_steps))) /\ ((((exists fs_h_dst_unit_slicesumnegative_body_steps_successor. fs_h_dst_unit_slicesumnegative_body_steps_successor + S (fs_s_dst_unit_slicesumnegative_body_steps) = S ((S (S fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative)) /\ exists fs_q_dst_unit_slicesumnegative_body_steps_successor. fs_u_dst_unit_slicesumnegative = fs_q_dst_unit_slicesumnegative_body_steps_successor * S ((S (S fs_i_dst_unit_slicesumnegative_body_steps)) * fs_v_dst_unit_slicesumnegative) + (fs_s_dst_unit_slicesumnegative_body_steps))) /\ fs_s_dst_unit_slicesumnegative_body_steps = fs_r_dst_unit_slicesumnegative_body_steps + fs_a_dst_unit_slicesumnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_slicesumresult ge_balance_negative_unit_slicesumresult. (((((z) = 2 * (ge_balance_positive_unit_slicesumresult) /\ (ge_balance_negative_unit_slicesumresult) = 0) \/ exists ge_signed_half_unit_slicesumresultdecode. (((z) = 2 * ge_signed_half_unit_slicesumresultdecode + 1 /\ (ge_balance_positive_unit_slicesumresult) = 0) /\ (ge_balance_negative_unit_slicesumresult) = S ge_signed_half_unit_slicesumresultdecode))) /\ ((dst_positive_sum_unit_slicesum) + ge_balance_negative_unit_slicesumresult = (dst_negative_sum_unit_slicesum) + ge_balance_positive_unit_slicesumresult)))))))))))))