ArithTableEqual(F,G,l)

forall dst_index_bottomlayer dst_first_bottomlayer dst_second_bottomlayer. (exists pvs_gap_bottomlayerbound. pvs_gap_bottomlayerbound + S (dst_index_bottomlayer) = ((l))) -> (exists dst_positive_code_bottomlayerfirst dst_positive_scale_bottomlayerfirst dst_negative_code_bottomlayerfirst dst_negative_scale_bottomlayerfirst dst_positive_bottomlayerfirst dst_negative_bottomlayerfirst. ((((F)) = (((((dst_positive_code_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst)) * S ((dst_positive_code_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst)) + ((dst_positive_scale_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst))) + (((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) * S ((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) + ((dst_negative_scale_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)))) * S ((((dst_positive_code_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst)) * S ((dst_positive_code_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst)) + ((dst_positive_scale_bottomlayerfirst) + (dst_positive_scale_bottomlayerfirst))) + (((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) * S ((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) + ((dst_negative_scale_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)))) + ((((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) * S ((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) + ((dst_negative_scale_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst))) + (((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) * S ((dst_negative_code_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)) + ((dst_negative_scale_bottomlayerfirst) + (dst_negative_scale_bottomlayerfirst)))))) /\ (((((exists ff_h_pvs_bottomlayerfirstpositive. ff_h_pvs_bottomlayerfirstpositive + S (dst_positive_bottomlayerfirst) = S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayerfirst)) /\ exists ff_q_pvs_bottomlayerfirstpositive. dst_positive_code_bottomlayerfirst = ff_q_pvs_bottomlayerfirstpositive * S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayerfirst) + (dst_positive_bottomlayerfirst))) /\ (((((exists ff_h_pvs_bottomlayerfirstnegative. ff_h_pvs_bottomlayerfirstnegative + S (dst_negative_bottomlayerfirst) = S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayerfirst)) /\ exists ff_q_pvs_bottomlayerfirstnegative. dst_negative_code_bottomlayerfirst = ff_q_pvs_bottomlayerfirstnegative * S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayerfirst) + (dst_negative_bottomlayerfirst))) /\ (exists ge_balance_positive_bottomlayerfirstvalue ge_balance_negative_bottomlayerfirstvalue. (((((dst_first_bottomlayer) = 2 * (ge_balance_positive_bottomlayerfirstvalue) /\ (ge_balance_negative_bottomlayerfirstvalue) = 0) \/ exists ge_signed_half_bottomlayerfirstvaluedecode. (((dst_first_bottomlayer) = 2 * ge_signed_half_bottomlayerfirstvaluedecode + 1 /\ (ge_balance_positive_bottomlayerfirstvalue) = 0) /\ (ge_balance_negative_bottomlayerfirstvalue) = S ge_signed_half_bottomlayerfirstvaluedecode))) /\ ((dst_positive_bottomlayerfirst) + ge_balance_negative_bottomlayerfirstvalue = (dst_negative_bottomlayerfirst) + ge_balance_positive_bottomlayerfirstvalue))))))))) -> (exists dst_positive_code_bottomlayersecond dst_positive_scale_bottomlayersecond dst_negative_code_bottomlayersecond dst_negative_scale_bottomlayersecond dst_positive_bottomlayersecond dst_negative_bottomlayersecond. ((((G)) = (((((dst_positive_code_bottomlayersecond) + (dst_positive_scale_bottomlayersecond)) * S ((dst_positive_code_bottomlayersecond) + (dst_positive_scale_bottomlayersecond)) + ((dst_positive_scale_bottomlayersecond) + (dst_positive_scale_bottomlayersecond))) + (((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) * S ((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) + ((dst_negative_scale_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)))) * S ((((dst_positive_code_bottomlayersecond) + (dst_positive_scale_bottomlayersecond)) * S ((dst_positive_code_bottomlayersecond) + (dst_positive_scale_bottomlayersecond)) + ((dst_positive_scale_bottomlayersecond) + (dst_positive_scale_bottomlayersecond))) + (((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) * S ((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) + ((dst_negative_scale_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)))) + ((((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) * S ((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) + ((dst_negative_scale_bottomlayersecond) + (dst_negative_scale_bottomlayersecond))) + (((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) * S ((dst_negative_code_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)) + ((dst_negative_scale_bottomlayersecond) + (dst_negative_scale_bottomlayersecond)))))) /\ (((((exists ff_h_pvs_bottomlayersecondpositive. ff_h_pvs_bottomlayersecondpositive + S (dst_positive_bottomlayersecond) = S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayersecond)) /\ exists ff_q_pvs_bottomlayersecondpositive. dst_positive_code_bottomlayersecond = ff_q_pvs_bottomlayersecondpositive * S ((S (dst_index_bottomlayer)) * dst_positive_scale_bottomlayersecond) + (dst_positive_bottomlayersecond))) /\ (((((exists ff_h_pvs_bottomlayersecondnegative. ff_h_pvs_bottomlayersecondnegative + S (dst_negative_bottomlayersecond) = S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayersecond)) /\ exists ff_q_pvs_bottomlayersecondnegative. dst_negative_code_bottomlayersecond = ff_q_pvs_bottomlayersecondnegative * S ((S (dst_index_bottomlayer)) * dst_negative_scale_bottomlayersecond) + (dst_negative_bottomlayersecond))) /\ (exists ge_balance_positive_bottomlayersecondvalue ge_balance_negative_bottomlayersecondvalue. (((((dst_second_bottomlayer) = 2 * (ge_balance_positive_bottomlayersecondvalue) /\ (ge_balance_negative_bottomlayersecondvalue) = 0) \/ exists ge_signed_half_bottomlayersecondvaluedecode. (((dst_second_bottomlayer) = 2 * ge_signed_half_bottomlayersecondvaluedecode + 1 /\ (ge_balance_positive_bottomlayersecondvalue) = 0) /\ (ge_balance_negative_bottomlayersecondvalue) = S ge_signed_half_bottomlayersecondvaluedecode))) /\ ((dst_positive_bottomlayersecond) + ge_balance_negative_bottomlayersecondvalue = (dst_negative_bottomlayersecond) + ge_balance_positive_bottomlayersecondvalue))))))))) -> dst_first_bottomlayer = dst_second_bottomlayer

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