ArithSlice(F,G,o,s,l)

((exists dst_positive_code_lowercontinuationsource_table dst_positive_scale_lowercontinuationsource_table dst_negative_code_lowercontinuationsource_table dst_negative_scale_lowercontinuationsource_table. ((((F)) = (((((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) * S ((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) + ((dst_positive_scale_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))) * S ((((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) * S ((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) + ((dst_positive_scale_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))) + ((((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))))) /\ (forall dst_index_lowercontinuationsource_table. (exists pvs_le_gap_lowercontinuationsource_tabledomain. pvs_le_gap_lowercontinuationsource_tabledomain + (dst_index_lowercontinuationsource_table) = (0)) -> exists dst_positive_lowercontinuationsource_table dst_negative_lowercontinuationsource_table dst_value_lowercontinuationsource_table. ((((exists ff_h_pvs_lowercontinuationsource_tableentrypositive. ff_h_pvs_lowercontinuationsource_tableentrypositive + S (dst_positive_lowercontinuationsource_table) = S ((S (dst_index_lowercontinuationsource_table)) * dst_positive_scale_lowercontinuationsource_table)) /\ exists ff_q_pvs_lowercontinuationsource_tableentrypositive. dst_positive_code_lowercontinuationsource_table = ff_q_pvs_lowercontinuationsource_tableentrypositive * S ((S (dst_index_lowercontinuationsource_table)) * dst_positive_scale_lowercontinuationsource_table) + (dst_positive_lowercontinuationsource_table))) /\ (((((exists ff_h_pvs_lowercontinuationsource_tableentrynegative. ff_h_pvs_lowercontinuationsource_tableentrynegative + S (dst_negative_lowercontinuationsource_table) = S ((S (dst_index_lowercontinuationsource_table)) * dst_negative_scale_lowercontinuationsource_table)) /\ exists ff_q_pvs_lowercontinuationsource_tableentrynegative. dst_negative_code_lowercontinuationsource_table = ff_q_pvs_lowercontinuationsource_tableentrynegative * S ((S (dst_index_lowercontinuationsource_table)) * dst_negative_scale_lowercontinuationsource_table) + (dst_negative_lowercontinuationsource_table))) /\ (exists ge_balance_positive_lowercontinuationsource_tableentryvalue ge_balance_negative_lowercontinuationsource_tableentryvalue. (((((dst_value_lowercontinuationsource_table) = 2 * (ge_balance_positive_lowercontinuationsource_tableentryvalue) /\ (ge_balance_negative_lowercontinuationsource_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationsource_tableentryvaluedecode. (((dst_value_lowercontinuationsource_table) = 2 * ge_signed_half_lowercontinuationsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsource_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationsource_tableentryvalue) = S ge_signed_half_lowercontinuationsource_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationsource_table) + ge_balance_negative_lowercontinuationsource_tableentryvalue = (dst_negative_lowercontinuationsource_table) + ge_balance_positive_lowercontinuationsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowercontinuationoutput_table dst_positive_scale_lowercontinuationoutput_table dst_negative_code_lowercontinuationoutput_table dst_negative_scale_lowercontinuationoutput_table. ((((G)) = (((((dst_positive_code_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table)) * S ((dst_positive_code_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table)) + ((dst_positive_scale_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table))) + (((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) * S ((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) + ((dst_negative_scale_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)))) * S ((((dst_positive_code_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table)) * S ((dst_positive_code_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table)) + ((dst_positive_scale_lowercontinuationoutput_table) + (dst_positive_scale_lowercontinuationoutput_table))) + (((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) * S ((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) + ((dst_negative_scale_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)))) + ((((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) * S ((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) + ((dst_negative_scale_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table))) + (((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) * S ((dst_negative_code_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)) + ((dst_negative_scale_lowercontinuationoutput_table) + (dst_negative_scale_lowercontinuationoutput_table)))))) /\ (forall dst_index_lowercontinuationoutput_table. (exists pvs_le_gap_lowercontinuationoutput_tabledomain. pvs_le_gap_lowercontinuationoutput_tabledomain + (dst_index_lowercontinuationoutput_table) = ((l))) -> exists dst_positive_lowercontinuationoutput_table dst_negative_lowercontinuationoutput_table dst_value_lowercontinuationoutput_table. ((((exists ff_h_pvs_lowercontinuationoutput_tableentrypositive. ff_h_pvs_lowercontinuationoutput_tableentrypositive + S (dst_positive_lowercontinuationoutput_table) = S ((S (dst_index_lowercontinuationoutput_table)) * dst_positive_scale_lowercontinuationoutput_table)) /\ exists ff_q_pvs_lowercontinuationoutput_tableentrypositive. dst_positive_code_lowercontinuationoutput_table = ff_q_pvs_lowercontinuationoutput_tableentrypositive * S ((S (dst_index_lowercontinuationoutput_table)) * dst_positive_scale_lowercontinuationoutput_table) + (dst_positive_lowercontinuationoutput_table))) /\ (((((exists ff_h_pvs_lowercontinuationoutput_tableentrynegative. ff_h_pvs_lowercontinuationoutput_tableentrynegative + S (dst_negative_lowercontinuationoutput_table) = S ((S (dst_index_lowercontinuationoutput_table)) * dst_negative_scale_lowercontinuationoutput_table)) /\ exists ff_q_pvs_lowercontinuationoutput_tableentrynegative. dst_negative_code_lowercontinuationoutput_table = ff_q_pvs_lowercontinuationoutput_tableentrynegative * S ((S (dst_index_lowercontinuationoutput_table)) * dst_negative_scale_lowercontinuationoutput_table) + (dst_negative_lowercontinuationoutput_table))) /\ (exists ge_balance_positive_lowercontinuationoutput_tableentryvalue ge_balance_negative_lowercontinuationoutput_tableentryvalue. (((((dst_value_lowercontinuationoutput_table) = 2 * (ge_balance_positive_lowercontinuationoutput_tableentryvalue) /\ (ge_balance_negative_lowercontinuationoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationoutput_tableentryvaluedecode. (((dst_value_lowercontinuationoutput_table) = 2 * ge_signed_half_lowercontinuationoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationoutput_tableentryvalue) = S ge_signed_half_lowercontinuationoutput_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationoutput_table) + ge_balance_negative_lowercontinuationoutput_tableentryvalue = (dst_negative_lowercontinuationoutput_table) + ge_balance_positive_lowercontinuationoutput_tableentryvalue))))))))) /\ (forall srs_index_lowercontinuation. (exists pvs_gap_lowercontinuationbound. pvs_gap_lowercontinuationbound + S (srs_index_lowercontinuation) = ((l))) -> exists srs_value_lowercontinuation. (((exists dst_positive_code_lowercontinuationentrysource dst_positive_scale_lowercontinuationentrysource dst_negative_code_lowercontinuationentrysource dst_negative_scale_lowercontinuationentrysource dst_positive_lowercontinuationentrysource dst_negative_lowercontinuationentrysource. ((((F)) = (((((dst_positive_code_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource)) * S ((dst_positive_code_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource)) + ((dst_positive_scale_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource))) + (((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) * S ((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) + ((dst_negative_scale_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)))) * S ((((dst_positive_code_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource)) * S ((dst_positive_code_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource)) + ((dst_positive_scale_lowercontinuationentrysource) + (dst_positive_scale_lowercontinuationentrysource))) + (((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) * S ((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) + ((dst_negative_scale_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)))) + ((((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) * S ((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) + ((dst_negative_scale_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource))) + (((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) * S ((dst_negative_code_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)) + ((dst_negative_scale_lowercontinuationentrysource) + (dst_negative_scale_lowercontinuationentrysource)))))) /\ (((((exists ff_h_pvs_lowercontinuationentrysourcepositive. ff_h_pvs_lowercontinuationentrysourcepositive + S (dst_positive_lowercontinuationentrysource) = S ((S ((((o)) + (((s)) * (srs_index_lowercontinuation))))) * dst_positive_scale_lowercontinuationentrysource)) /\ exists ff_q_pvs_lowercontinuationentrysourcepositive. dst_positive_code_lowercontinuationentrysource = ff_q_pvs_lowercontinuationentrysourcepositive * S ((S ((((o)) + (((s)) * (srs_index_lowercontinuation))))) * dst_positive_scale_lowercontinuationentrysource) + (dst_positive_lowercontinuationentrysource))) /\ (((((exists ff_h_pvs_lowercontinuationentrysourcenegative. ff_h_pvs_lowercontinuationentrysourcenegative + S (dst_negative_lowercontinuationentrysource) = S ((S ((((o)) + (((s)) * (srs_index_lowercontinuation))))) * dst_negative_scale_lowercontinuationentrysource)) /\ exists ff_q_pvs_lowercontinuationentrysourcenegative. dst_negative_code_lowercontinuationentrysource = ff_q_pvs_lowercontinuationentrysourcenegative * S ((S ((((o)) + (((s)) * (srs_index_lowercontinuation))))) * dst_negative_scale_lowercontinuationentrysource) + (dst_negative_lowercontinuationentrysource))) /\ (exists ge_balance_positive_lowercontinuationentrysourcevalue ge_balance_negative_lowercontinuationentrysourcevalue. (((((srs_value_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationentrysourcevalue) /\ (ge_balance_negative_lowercontinuationentrysourcevalue) = 0) \/ exists ge_signed_half_lowercontinuationentrysourcevaluedecode. (((srs_value_lowercontinuation) = 2 * ge_signed_half_lowercontinuationentrysourcevaluedecode + 1 /\ (ge_balance_positive_lowercontinuationentrysourcevalue) = 0) /\ (ge_balance_negative_lowercontinuationentrysourcevalue) = S ge_signed_half_lowercontinuationentrysourcevaluedecode))) /\ ((dst_positive_lowercontinuationentrysource) + ge_balance_negative_lowercontinuationentrysourcevalue = (dst_negative_lowercontinuationentrysource) + ge_balance_positive_lowercontinuationentrysourcevalue))))))))) /\ (exists dst_positive_code_lowercontinuationentryoutput dst_positive_scale_lowercontinuationentryoutput dst_negative_code_lowercontinuationentryoutput dst_negative_scale_lowercontinuationentryoutput dst_positive_lowercontinuationentryoutput dst_negative_lowercontinuationentryoutput. ((((G)) = (((((dst_positive_code_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput)) * S ((dst_positive_code_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput)) + ((dst_positive_scale_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput))) + (((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) * S ((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) + ((dst_negative_scale_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)))) * S ((((dst_positive_code_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput)) * S ((dst_positive_code_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput)) + ((dst_positive_scale_lowercontinuationentryoutput) + (dst_positive_scale_lowercontinuationentryoutput))) + (((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) * S ((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) + ((dst_negative_scale_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)))) + ((((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) * S ((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) + ((dst_negative_scale_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput))) + (((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) * S ((dst_negative_code_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)) + ((dst_negative_scale_lowercontinuationentryoutput) + (dst_negative_scale_lowercontinuationentryoutput)))))) /\ (((((exists ff_h_pvs_lowercontinuationentryoutputpositive. ff_h_pvs_lowercontinuationentryoutputpositive + S (dst_positive_lowercontinuationentryoutput) = S ((S (srs_index_lowercontinuation)) * dst_positive_scale_lowercontinuationentryoutput)) /\ exists ff_q_pvs_lowercontinuationentryoutputpositive. dst_positive_code_lowercontinuationentryoutput = ff_q_pvs_lowercontinuationentryoutputpositive * S ((S (srs_index_lowercontinuation)) * dst_positive_scale_lowercontinuationentryoutput) + (dst_positive_lowercontinuationentryoutput))) /\ (((((exists ff_h_pvs_lowercontinuationentryoutputnegative. ff_h_pvs_lowercontinuationentryoutputnegative + S (dst_negative_lowercontinuationentryoutput) = S ((S (srs_index_lowercontinuation)) * dst_negative_scale_lowercontinuationentryoutput)) /\ exists ff_q_pvs_lowercontinuationentryoutputnegative. dst_negative_code_lowercontinuationentryoutput = ff_q_pvs_lowercontinuationentryoutputnegative * S ((S (srs_index_lowercontinuation)) * dst_negative_scale_lowercontinuationentryoutput) + (dst_negative_lowercontinuationentryoutput))) /\ (exists ge_balance_positive_lowercontinuationentryoutputvalue ge_balance_negative_lowercontinuationentryoutputvalue. (((((srs_value_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationentryoutputvalue) /\ (ge_balance_negative_lowercontinuationentryoutputvalue) = 0) \/ exists ge_signed_half_lowercontinuationentryoutputvaluedecode. (((srs_value_lowercontinuation) = 2 * ge_signed_half_lowercontinuationentryoutputvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationentryoutputvalue) = 0) /\ (ge_balance_negative_lowercontinuationentryoutputvalue) = S ge_signed_half_lowercontinuationentryoutputvaluedecode))) /\ ((dst_positive_lowercontinuationentryoutput) + ge_balance_negative_lowercontinuationentryoutputvalue = (dst_negative_lowercontinuationentryoutput) + ge_balance_positive_lowercontinuationentryoutputvalue)))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.