ArithPositiveEqual(F,G,N)

forall dm_index_lowertier dm_first_value_lowertier dm_second_value_lowertier. ~(dm_index_lowertier=0) -> (exists pvs_le_gap_lowertierdomain. pvs_le_gap_lowertierdomain + (dm_index_lowertier) = ((N))) -> (exists dst_positive_code_lowertierfirst dst_positive_scale_lowertierfirst dst_negative_code_lowertierfirst dst_negative_scale_lowertierfirst dst_positive_lowertierfirst dst_negative_lowertierfirst. ((((F)) = (((((dst_positive_code_lowertierfirst) + (dst_positive_scale_lowertierfirst)) * S ((dst_positive_code_lowertierfirst) + (dst_positive_scale_lowertierfirst)) + ((dst_positive_scale_lowertierfirst) + (dst_positive_scale_lowertierfirst))) + (((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) * S ((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) + ((dst_negative_scale_lowertierfirst) + (dst_negative_scale_lowertierfirst)))) * S ((((dst_positive_code_lowertierfirst) + (dst_positive_scale_lowertierfirst)) * S ((dst_positive_code_lowertierfirst) + (dst_positive_scale_lowertierfirst)) + ((dst_positive_scale_lowertierfirst) + (dst_positive_scale_lowertierfirst))) + (((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) * S ((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) + ((dst_negative_scale_lowertierfirst) + (dst_negative_scale_lowertierfirst)))) + ((((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) * S ((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) + ((dst_negative_scale_lowertierfirst) + (dst_negative_scale_lowertierfirst))) + (((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) * S ((dst_negative_code_lowertierfirst) + (dst_negative_scale_lowertierfirst)) + ((dst_negative_scale_lowertierfirst) + (dst_negative_scale_lowertierfirst)))))) /\ (((((exists ff_h_pvs_lowertierfirstpositive. ff_h_pvs_lowertierfirstpositive + S (dst_positive_lowertierfirst) = S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierfirst)) /\ exists ff_q_pvs_lowertierfirstpositive. dst_positive_code_lowertierfirst = ff_q_pvs_lowertierfirstpositive * S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierfirst) + (dst_positive_lowertierfirst))) /\ (((((exists ff_h_pvs_lowertierfirstnegative. ff_h_pvs_lowertierfirstnegative + S (dst_negative_lowertierfirst) = S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierfirst)) /\ exists ff_q_pvs_lowertierfirstnegative. dst_negative_code_lowertierfirst = ff_q_pvs_lowertierfirstnegative * S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierfirst) + (dst_negative_lowertierfirst))) /\ (exists ge_balance_positive_lowertierfirstvalue ge_balance_negative_lowertierfirstvalue. (((((dm_first_value_lowertier) = 2 * (ge_balance_positive_lowertierfirstvalue) /\ (ge_balance_negative_lowertierfirstvalue) = 0) \/ exists ge_signed_half_lowertierfirstvaluedecode. (((dm_first_value_lowertier) = 2 * ge_signed_half_lowertierfirstvaluedecode + 1 /\ (ge_balance_positive_lowertierfirstvalue) = 0) /\ (ge_balance_negative_lowertierfirstvalue) = S ge_signed_half_lowertierfirstvaluedecode))) /\ ((dst_positive_lowertierfirst) + ge_balance_negative_lowertierfirstvalue = (dst_negative_lowertierfirst) + ge_balance_positive_lowertierfirstvalue))))))))) -> (exists dst_positive_code_lowertiersecond dst_positive_scale_lowertiersecond dst_negative_code_lowertiersecond dst_negative_scale_lowertiersecond dst_positive_lowertiersecond dst_negative_lowertiersecond. ((((G)) = (((((dst_positive_code_lowertiersecond) + (dst_positive_scale_lowertiersecond)) * S ((dst_positive_code_lowertiersecond) + (dst_positive_scale_lowertiersecond)) + ((dst_positive_scale_lowertiersecond) + (dst_positive_scale_lowertiersecond))) + (((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) * S ((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) + ((dst_negative_scale_lowertiersecond) + (dst_negative_scale_lowertiersecond)))) * S ((((dst_positive_code_lowertiersecond) + (dst_positive_scale_lowertiersecond)) * S ((dst_positive_code_lowertiersecond) + (dst_positive_scale_lowertiersecond)) + ((dst_positive_scale_lowertiersecond) + (dst_positive_scale_lowertiersecond))) + (((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) * S ((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) + ((dst_negative_scale_lowertiersecond) + (dst_negative_scale_lowertiersecond)))) + ((((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) * S ((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) + ((dst_negative_scale_lowertiersecond) + (dst_negative_scale_lowertiersecond))) + (((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) * S ((dst_negative_code_lowertiersecond) + (dst_negative_scale_lowertiersecond)) + ((dst_negative_scale_lowertiersecond) + (dst_negative_scale_lowertiersecond)))))) /\ (((((exists ff_h_pvs_lowertiersecondpositive. ff_h_pvs_lowertiersecondpositive + S (dst_positive_lowertiersecond) = S ((S (dm_index_lowertier)) * dst_positive_scale_lowertiersecond)) /\ exists ff_q_pvs_lowertiersecondpositive. dst_positive_code_lowertiersecond = ff_q_pvs_lowertiersecondpositive * S ((S (dm_index_lowertier)) * dst_positive_scale_lowertiersecond) + (dst_positive_lowertiersecond))) /\ (((((exists ff_h_pvs_lowertiersecondnegative. ff_h_pvs_lowertiersecondnegative + S (dst_negative_lowertiersecond) = S ((S (dm_index_lowertier)) * dst_negative_scale_lowertiersecond)) /\ exists ff_q_pvs_lowertiersecondnegative. dst_negative_code_lowertiersecond = ff_q_pvs_lowertiersecondnegative * S ((S (dm_index_lowertier)) * dst_negative_scale_lowertiersecond) + (dst_negative_lowertiersecond))) /\ (exists ge_balance_positive_lowertiersecondvalue ge_balance_negative_lowertiersecondvalue. (((((dm_second_value_lowertier) = 2 * (ge_balance_positive_lowertiersecondvalue) /\ (ge_balance_negative_lowertiersecondvalue) = 0) \/ exists ge_signed_half_lowertiersecondvaluedecode. (((dm_second_value_lowertier) = 2 * ge_signed_half_lowertiersecondvaluedecode + 1 /\ (ge_balance_positive_lowertiersecondvalue) = 0) /\ (ge_balance_negative_lowertiersecondvalue) = S ge_signed_half_lowertiersecondvaluedecode))) /\ ((dst_positive_lowertiersecond) + ge_balance_negative_lowertiersecondvalue = (dst_negative_lowertiersecond) + ge_balance_positive_lowertiersecondvalue))))))))) -> dm_first_value_lowertier=dm_second_value_lowertier

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