DivisorMaskEntry(F,n,d,z)

(((~(((d))=0)) /\ (exists dm_quotient_lowertier. ((((n))=((d))*dm_quotient_lowertier) /\ (exists dst_positive_code_lowertierinput dst_positive_scale_lowertierinput dst_negative_code_lowertierinput dst_negative_scale_lowertierinput dst_positive_lowertierinput dst_negative_lowertierinput. ((((F)) = (((((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) * S ((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) + ((dst_positive_scale_lowertierinput) + (dst_positive_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))) * S ((((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) * S ((dst_positive_code_lowertierinput) + (dst_positive_scale_lowertierinput)) + ((dst_positive_scale_lowertierinput) + (dst_positive_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))) + ((((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput))) + (((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) * S ((dst_negative_code_lowertierinput) + (dst_negative_scale_lowertierinput)) + ((dst_negative_scale_lowertierinput) + (dst_negative_scale_lowertierinput)))))) /\ (((((exists ff_h_pvs_lowertierinputpositive. ff_h_pvs_lowertierinputpositive + S (dst_positive_lowertierinput) = S ((S ((d))) * dst_positive_scale_lowertierinput)) /\ exists ff_q_pvs_lowertierinputpositive. dst_positive_code_lowertierinput = ff_q_pvs_lowertierinputpositive * S ((S ((d))) * dst_positive_scale_lowertierinput) + (dst_positive_lowertierinput))) /\ (((((exists ff_h_pvs_lowertierinputnegative. ff_h_pvs_lowertierinputnegative + S (dst_negative_lowertierinput) = S ((S ((d))) * dst_negative_scale_lowertierinput)) /\ exists ff_q_pvs_lowertierinputnegative. dst_negative_code_lowertierinput = ff_q_pvs_lowertierinputnegative * S ((S ((d))) * dst_negative_scale_lowertierinput) + (dst_negative_lowertierinput))) /\ (exists ge_balance_positive_lowertierinputvalue ge_balance_negative_lowertierinputvalue. ((((((z)) = 2 * (ge_balance_positive_lowertierinputvalue) /\ (ge_balance_negative_lowertierinputvalue) = 0) \/ exists ge_signed_half_lowertierinputvaluedecode. ((((z)) = 2 * ge_signed_half_lowertierinputvaluedecode + 1 /\ (ge_balance_positive_lowertierinputvalue) = 0) /\ (ge_balance_negative_lowertierinputvalue) = S ge_signed_half_lowertierinputvaluedecode))) /\ ((dst_positive_lowertierinput) + ge_balance_negative_lowertierinputvalue = (dst_negative_lowertierinput) + ge_balance_positive_lowertierinputvalue))))))))))))) \/ (((((d))=0 \/ ~(exists pvs_factor_lowertiernondivisor. ((n)) = ((d)) * pvs_factor_lowertiernondivisor)) /\ (((z))=0)))

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