ArithNegate(F,G,l)

forall mdc_index_lowercontinuation mdc_source_lowercontinuation mdc_target_lowercontinuation. (exists pvs_gap_lowercontinuationbound. pvs_gap_lowercontinuationbound + S (mdc_index_lowercontinuation) = ((l))) -> (exists dst_positive_code_lowercontinuationfirst dst_positive_scale_lowercontinuationfirst dst_negative_code_lowercontinuationfirst dst_negative_scale_lowercontinuationfirst dst_positive_lowercontinuationfirst dst_negative_lowercontinuationfirst. ((((F)) = (((((dst_positive_code_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst)) * S ((dst_positive_code_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst)) + ((dst_positive_scale_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst))) + (((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) * S ((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) + ((dst_negative_scale_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)))) * S ((((dst_positive_code_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst)) * S ((dst_positive_code_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst)) + ((dst_positive_scale_lowercontinuationfirst) + (dst_positive_scale_lowercontinuationfirst))) + (((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) * S ((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) + ((dst_negative_scale_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)))) + ((((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) * S ((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) + ((dst_negative_scale_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst))) + (((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) * S ((dst_negative_code_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)) + ((dst_negative_scale_lowercontinuationfirst) + (dst_negative_scale_lowercontinuationfirst)))))) /\ (((((exists ff_h_pvs_lowercontinuationfirstpositive. ff_h_pvs_lowercontinuationfirstpositive + S (dst_positive_lowercontinuationfirst) = S ((S (mdc_index_lowercontinuation)) * dst_positive_scale_lowercontinuationfirst)) /\ exists ff_q_pvs_lowercontinuationfirstpositive. dst_positive_code_lowercontinuationfirst = ff_q_pvs_lowercontinuationfirstpositive * S ((S (mdc_index_lowercontinuation)) * dst_positive_scale_lowercontinuationfirst) + (dst_positive_lowercontinuationfirst))) /\ (((((exists ff_h_pvs_lowercontinuationfirstnegative. ff_h_pvs_lowercontinuationfirstnegative + S (dst_negative_lowercontinuationfirst) = S ((S (mdc_index_lowercontinuation)) * dst_negative_scale_lowercontinuationfirst)) /\ exists ff_q_pvs_lowercontinuationfirstnegative. dst_negative_code_lowercontinuationfirst = ff_q_pvs_lowercontinuationfirstnegative * S ((S (mdc_index_lowercontinuation)) * dst_negative_scale_lowercontinuationfirst) + (dst_negative_lowercontinuationfirst))) /\ (exists ge_balance_positive_lowercontinuationfirstvalue ge_balance_negative_lowercontinuationfirstvalue. (((((mdc_source_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationfirstvalue) /\ (ge_balance_negative_lowercontinuationfirstvalue) = 0) \/ exists ge_signed_half_lowercontinuationfirstvaluedecode. (((mdc_source_lowercontinuation) = 2 * ge_signed_half_lowercontinuationfirstvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationfirstvalue) = 0) /\ (ge_balance_negative_lowercontinuationfirstvalue) = S ge_signed_half_lowercontinuationfirstvaluedecode))) /\ ((dst_positive_lowercontinuationfirst) + ge_balance_negative_lowercontinuationfirstvalue = (dst_negative_lowercontinuationfirst) + ge_balance_positive_lowercontinuationfirstvalue))))))))) -> (exists dst_positive_code_lowercontinuationsecond dst_positive_scale_lowercontinuationsecond dst_negative_code_lowercontinuationsecond dst_negative_scale_lowercontinuationsecond dst_positive_lowercontinuationsecond dst_negative_lowercontinuationsecond. ((((G)) = (((((dst_positive_code_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond)) * S ((dst_positive_code_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond)) + ((dst_positive_scale_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond))) + (((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) * S ((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) + ((dst_negative_scale_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)))) * S ((((dst_positive_code_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond)) * S ((dst_positive_code_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond)) + ((dst_positive_scale_lowercontinuationsecond) + (dst_positive_scale_lowercontinuationsecond))) + (((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) * S ((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) + ((dst_negative_scale_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)))) + ((((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) * S ((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) + ((dst_negative_scale_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond))) + (((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) * S ((dst_negative_code_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)) + ((dst_negative_scale_lowercontinuationsecond) + (dst_negative_scale_lowercontinuationsecond)))))) /\ (((((exists ff_h_pvs_lowercontinuationsecondpositive. ff_h_pvs_lowercontinuationsecondpositive + S (dst_positive_lowercontinuationsecond) = S ((S (mdc_index_lowercontinuation)) * dst_positive_scale_lowercontinuationsecond)) /\ exists ff_q_pvs_lowercontinuationsecondpositive. dst_positive_code_lowercontinuationsecond = ff_q_pvs_lowercontinuationsecondpositive * S ((S (mdc_index_lowercontinuation)) * dst_positive_scale_lowercontinuationsecond) + (dst_positive_lowercontinuationsecond))) /\ (((((exists ff_h_pvs_lowercontinuationsecondnegative. ff_h_pvs_lowercontinuationsecondnegative + S (dst_negative_lowercontinuationsecond) = S ((S (mdc_index_lowercontinuation)) * dst_negative_scale_lowercontinuationsecond)) /\ exists ff_q_pvs_lowercontinuationsecondnegative. dst_negative_code_lowercontinuationsecond = ff_q_pvs_lowercontinuationsecondnegative * S ((S (mdc_index_lowercontinuation)) * dst_negative_scale_lowercontinuationsecond) + (dst_negative_lowercontinuationsecond))) /\ (exists ge_balance_positive_lowercontinuationsecondvalue ge_balance_negative_lowercontinuationsecondvalue. (((((mdc_target_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationsecondvalue) /\ (ge_balance_negative_lowercontinuationsecondvalue) = 0) \/ exists ge_signed_half_lowercontinuationsecondvaluedecode. (((mdc_target_lowercontinuation) = 2 * ge_signed_half_lowercontinuationsecondvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsecondvalue) = 0) /\ (ge_balance_negative_lowercontinuationsecondvalue) = S ge_signed_half_lowercontinuationsecondvaluedecode))) /\ ((dst_positive_lowercontinuationsecond) + ge_balance_negative_lowercontinuationsecondvalue = (dst_negative_lowercontinuationsecond) + ge_balance_positive_lowercontinuationsecondvalue))))))))) -> (exists mps_positive_lowercontinuationnegation mps_negative_lowercontinuationnegation. (((((mdc_source_lowercontinuation) = 2 * (mps_positive_lowercontinuationnegation) /\ (mps_negative_lowercontinuationnegation) = 0) \/ exists ge_signed_half_lowercontinuationnegationsource. (((mdc_source_lowercontinuation) = 2 * ge_signed_half_lowercontinuationnegationsource + 1 /\ (mps_positive_lowercontinuationnegation) = 0) /\ (mps_negative_lowercontinuationnegation) = S ge_signed_half_lowercontinuationnegationsource))) /\ ((((mdc_target_lowercontinuation) = 2 * (mps_negative_lowercontinuationnegation) /\ (mps_positive_lowercontinuationnegation) = 0) \/ exists ge_signed_half_lowercontinuationnegationtarget. (((mdc_target_lowercontinuation) = 2 * ge_signed_half_lowercontinuationnegationtarget + 1 /\ (mps_negative_lowercontinuationnegation) = 0) /\ (mps_positive_lowercontinuationnegation) = S ge_signed_half_lowercontinuationnegationtarget)))))

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