DivisorMask(F,n,l,M)

((exists dst_positive_code_lowertiertable dst_positive_scale_lowertiertable dst_negative_code_lowertiertable dst_negative_scale_lowertiertable. ((((M)) = (((((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) * S ((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) + ((dst_positive_scale_lowertiertable) + (dst_positive_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))) * S ((((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) * S ((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) + ((dst_positive_scale_lowertiertable) + (dst_positive_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))) + ((((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))))) /\ (forall dst_index_lowertiertable. (exists pvs_le_gap_lowertiertabledomain. pvs_le_gap_lowertiertabledomain + (dst_index_lowertiertable) = ((l))) -> exists dst_positive_lowertiertable dst_negative_lowertiertable dst_value_lowertiertable. ((((exists ff_h_pvs_lowertiertableentrypositive. ff_h_pvs_lowertiertableentrypositive + S (dst_positive_lowertiertable) = S ((S (dst_index_lowertiertable)) * dst_positive_scale_lowertiertable)) /\ exists ff_q_pvs_lowertiertableentrypositive. dst_positive_code_lowertiertable = ff_q_pvs_lowertiertableentrypositive * S ((S (dst_index_lowertiertable)) * dst_positive_scale_lowertiertable) + (dst_positive_lowertiertable))) /\ (((((exists ff_h_pvs_lowertiertableentrynegative. ff_h_pvs_lowertiertableentrynegative + S (dst_negative_lowertiertable) = S ((S (dst_index_lowertiertable)) * dst_negative_scale_lowertiertable)) /\ exists ff_q_pvs_lowertiertableentrynegative. dst_negative_code_lowertiertable = ff_q_pvs_lowertiertableentrynegative * S ((S (dst_index_lowertiertable)) * dst_negative_scale_lowertiertable) + (dst_negative_lowertiertable))) /\ (exists ge_balance_positive_lowertiertableentryvalue ge_balance_negative_lowertiertableentryvalue. (((((dst_value_lowertiertable) = 2 * (ge_balance_positive_lowertiertableentryvalue) /\ (ge_balance_negative_lowertiertableentryvalue) = 0) \/ exists ge_signed_half_lowertiertableentryvaluedecode. (((dst_value_lowertiertable) = 2 * ge_signed_half_lowertiertableentryvaluedecode + 1 /\ (ge_balance_positive_lowertiertableentryvalue) = 0) /\ (ge_balance_negative_lowertiertableentryvalue) = S ge_signed_half_lowertiertableentryvaluedecode))) /\ ((dst_positive_lowertiertable) + ge_balance_negative_lowertiertableentryvalue = (dst_negative_lowertiertable) + ge_balance_positive_lowertiertableentryvalue))))))))) /\ (forall dm_index_lowertier dm_value_lowertier. (exists pvs_le_gap_lowertierdomain. pvs_le_gap_lowertierdomain + (dm_index_lowertier) = ((l))) -> (exists dst_positive_code_lowertierlookup dst_positive_scale_lowertierlookup dst_negative_code_lowertierlookup dst_negative_scale_lowertierlookup dst_positive_lowertierlookup dst_negative_lowertierlookup. ((((M)) = (((((dst_positive_code_lowertierlookup) + (dst_positive_scale_lowertierlookup)) * S ((dst_positive_code_lowertierlookup) + (dst_positive_scale_lowertierlookup)) + ((dst_positive_scale_lowertierlookup) + (dst_positive_scale_lowertierlookup))) + (((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) * S ((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) + ((dst_negative_scale_lowertierlookup) + (dst_negative_scale_lowertierlookup)))) * S ((((dst_positive_code_lowertierlookup) + (dst_positive_scale_lowertierlookup)) * S ((dst_positive_code_lowertierlookup) + (dst_positive_scale_lowertierlookup)) + ((dst_positive_scale_lowertierlookup) + (dst_positive_scale_lowertierlookup))) + (((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) * S ((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) + ((dst_negative_scale_lowertierlookup) + (dst_negative_scale_lowertierlookup)))) + ((((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) * S ((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) + ((dst_negative_scale_lowertierlookup) + (dst_negative_scale_lowertierlookup))) + (((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) * S ((dst_negative_code_lowertierlookup) + (dst_negative_scale_lowertierlookup)) + ((dst_negative_scale_lowertierlookup) + (dst_negative_scale_lowertierlookup)))))) /\ (((((exists ff_h_pvs_lowertierlookuppositive. ff_h_pvs_lowertierlookuppositive + S (dst_positive_lowertierlookup) = S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierlookup)) /\ exists ff_q_pvs_lowertierlookuppositive. dst_positive_code_lowertierlookup = ff_q_pvs_lowertierlookuppositive * S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierlookup) + (dst_positive_lowertierlookup))) /\ (((((exists ff_h_pvs_lowertierlookupnegative. ff_h_pvs_lowertierlookupnegative + S (dst_negative_lowertierlookup) = S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierlookup)) /\ exists ff_q_pvs_lowertierlookupnegative. dst_negative_code_lowertierlookup = ff_q_pvs_lowertierlookupnegative * S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierlookup) + (dst_negative_lowertierlookup))) /\ (exists ge_balance_positive_lowertierlookupvalue ge_balance_negative_lowertierlookupvalue. (((((dm_value_lowertier) = 2 * (ge_balance_positive_lowertierlookupvalue) /\ (ge_balance_negative_lowertierlookupvalue) = 0) \/ exists ge_signed_half_lowertierlookupvaluedecode. (((dm_value_lowertier) = 2 * ge_signed_half_lowertierlookupvaluedecode + 1 /\ (ge_balance_positive_lowertierlookupvalue) = 0) /\ (ge_balance_negative_lowertierlookupvalue) = S ge_signed_half_lowertierlookupvaluedecode))) /\ ((dst_positive_lowertierlookup) + ge_balance_negative_lowertierlookupvalue = (dst_negative_lowertierlookup) + ge_balance_positive_lowertierlookupvalue))))))))) -> ((((~((dm_index_lowertier)=0)) /\ (exists dm_quotient_lowertierentry. ((((n))=(dm_index_lowertier)*dm_quotient_lowertierentry) /\ (exists dst_positive_code_lowertierentryinput dst_positive_scale_lowertierentryinput dst_negative_code_lowertierentryinput dst_negative_scale_lowertierentryinput dst_positive_lowertierentryinput dst_negative_lowertierentryinput. ((((F)) = (((((dst_positive_code_lowertierentryinput) + (dst_positive_scale_lowertierentryinput)) * S ((dst_positive_code_lowertierentryinput) + (dst_positive_scale_lowertierentryinput)) + ((dst_positive_scale_lowertierentryinput) + (dst_positive_scale_lowertierentryinput))) + (((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) * S ((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) + ((dst_negative_scale_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)))) * S ((((dst_positive_code_lowertierentryinput) + (dst_positive_scale_lowertierentryinput)) * S ((dst_positive_code_lowertierentryinput) + (dst_positive_scale_lowertierentryinput)) + ((dst_positive_scale_lowertierentryinput) + (dst_positive_scale_lowertierentryinput))) + (((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) * S ((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) + ((dst_negative_scale_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)))) + ((((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) * S ((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) + ((dst_negative_scale_lowertierentryinput) + (dst_negative_scale_lowertierentryinput))) + (((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) * S ((dst_negative_code_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)) + ((dst_negative_scale_lowertierentryinput) + (dst_negative_scale_lowertierentryinput)))))) /\ (((((exists ff_h_pvs_lowertierentryinputpositive. ff_h_pvs_lowertierentryinputpositive + S (dst_positive_lowertierentryinput) = S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierentryinput)) /\ exists ff_q_pvs_lowertierentryinputpositive. dst_positive_code_lowertierentryinput = ff_q_pvs_lowertierentryinputpositive * S ((S (dm_index_lowertier)) * dst_positive_scale_lowertierentryinput) + (dst_positive_lowertierentryinput))) /\ (((((exists ff_h_pvs_lowertierentryinputnegative. ff_h_pvs_lowertierentryinputnegative + S (dst_negative_lowertierentryinput) = S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierentryinput)) /\ exists ff_q_pvs_lowertierentryinputnegative. dst_negative_code_lowertierentryinput = ff_q_pvs_lowertierentryinputnegative * S ((S (dm_index_lowertier)) * dst_negative_scale_lowertierentryinput) + (dst_negative_lowertierentryinput))) /\ (exists ge_balance_positive_lowertierentryinputvalue ge_balance_negative_lowertierentryinputvalue. (((((dm_value_lowertier) = 2 * (ge_balance_positive_lowertierentryinputvalue) /\ (ge_balance_negative_lowertierentryinputvalue) = 0) \/ exists ge_signed_half_lowertierentryinputvaluedecode. (((dm_value_lowertier) = 2 * ge_signed_half_lowertierentryinputvaluedecode + 1 /\ (ge_balance_positive_lowertierentryinputvalue) = 0) /\ (ge_balance_negative_lowertierentryinputvalue) = S ge_signed_half_lowertierentryinputvaluedecode))) /\ ((dst_positive_lowertierentryinput) + ge_balance_negative_lowertierentryinputvalue = (dst_negative_lowertierentryinput) + ge_balance_positive_lowertierentryinputvalue))))))))))))) \/ ((((dm_index_lowertier)=0 \/ ~(exists pvs_factor_lowertierentrynondivisor. ((n)) = (dm_index_lowertier) * pvs_factor_lowertierentrynondivisor)) /\ ((dm_value_lowertier)=0))))))

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