ArithReindex(F,G,r,s,l)

forall dsr_index_bottomlayer dsr_image_bottomlayer dsr_value_bottomlayer. (exists pvs_gap_bottomlayerbound. pvs_gap_bottomlayerbound + S (dsr_index_bottomlayer) = ((l))) -> (((exists ff_h_pvs_bottomlayermap. ff_h_pvs_bottomlayermap + S (dsr_image_bottomlayer) = S ((S (dsr_index_bottomlayer)) * (s))) /\ exists ff_q_pvs_bottomlayermap. (r) = ff_q_pvs_bottomlayermap * S ((S (dsr_index_bottomlayer)) * (s)) + (dsr_image_bottomlayer))) -> (exists dst_positive_code_bottomlayersource dst_positive_scale_bottomlayersource dst_negative_code_bottomlayersource dst_negative_scale_bottomlayersource dst_positive_bottomlayersource dst_negative_bottomlayersource. ((((F)) = (((((dst_positive_code_bottomlayersource) + (dst_positive_scale_bottomlayersource)) * S ((dst_positive_code_bottomlayersource) + (dst_positive_scale_bottomlayersource)) + ((dst_positive_scale_bottomlayersource) + (dst_positive_scale_bottomlayersource))) + (((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) * S ((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) + ((dst_negative_scale_bottomlayersource) + (dst_negative_scale_bottomlayersource)))) * S ((((dst_positive_code_bottomlayersource) + (dst_positive_scale_bottomlayersource)) * S ((dst_positive_code_bottomlayersource) + (dst_positive_scale_bottomlayersource)) + ((dst_positive_scale_bottomlayersource) + (dst_positive_scale_bottomlayersource))) + (((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) * S ((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) + ((dst_negative_scale_bottomlayersource) + (dst_negative_scale_bottomlayersource)))) + ((((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) * S ((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) + ((dst_negative_scale_bottomlayersource) + (dst_negative_scale_bottomlayersource))) + (((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) * S ((dst_negative_code_bottomlayersource) + (dst_negative_scale_bottomlayersource)) + ((dst_negative_scale_bottomlayersource) + (dst_negative_scale_bottomlayersource)))))) /\ (((((exists ff_h_pvs_bottomlayersourcepositive. ff_h_pvs_bottomlayersourcepositive + S (dst_positive_bottomlayersource) = S ((S (dsr_image_bottomlayer)) * dst_positive_scale_bottomlayersource)) /\ exists ff_q_pvs_bottomlayersourcepositive. dst_positive_code_bottomlayersource = ff_q_pvs_bottomlayersourcepositive * S ((S (dsr_image_bottomlayer)) * dst_positive_scale_bottomlayersource) + (dst_positive_bottomlayersource))) /\ (((((exists ff_h_pvs_bottomlayersourcenegative. ff_h_pvs_bottomlayersourcenegative + S (dst_negative_bottomlayersource) = S ((S (dsr_image_bottomlayer)) * dst_negative_scale_bottomlayersource)) /\ exists ff_q_pvs_bottomlayersourcenegative. dst_negative_code_bottomlayersource = ff_q_pvs_bottomlayersourcenegative * S ((S (dsr_image_bottomlayer)) * dst_negative_scale_bottomlayersource) + (dst_negative_bottomlayersource))) /\ (exists ge_balance_positive_bottomlayersourcevalue ge_balance_negative_bottomlayersourcevalue. (((((dsr_value_bottomlayer) = 2 * (ge_balance_positive_bottomlayersourcevalue) /\ (ge_balance_negative_bottomlayersourcevalue) = 0) \/ exists ge_signed_half_bottomlayersourcevaluedecode. (((dsr_value_bottomlayer) = 2 * ge_signed_half_bottomlayersourcevaluedecode + 1 /\ (ge_balance_positive_bottomlayersourcevalue) = 0) /\ (ge_balance_negative_bottomlayersourcevalue) = S ge_signed_half_bottomlayersourcevaluedecode))) /\ ((dst_positive_bottomlayersource) + ge_balance_negative_bottomlayersourcevalue = (dst_negative_bottomlayersource) + ge_balance_positive_bottomlayersourcevalue))))))))) -> (exists dst_positive_code_bottomlayertarget dst_positive_scale_bottomlayertarget dst_negative_code_bottomlayertarget dst_negative_scale_bottomlayertarget dst_positive_bottomlayertarget dst_negative_bottomlayertarget. ((((G)) = (((((dst_positive_code_bottomlayertarget) + (dst_positive_scale_bottomlayertarget)) * S ((dst_positive_code_bottomlayertarget) + (dst_positive_scale_bottomlayertarget)) + ((dst_positive_scale_bottomlayertarget) + (dst_positive_scale_bottomlayertarget))) + (((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) * S ((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) + ((dst_negative_scale_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)))) * S ((((dst_positive_code_bottomlayertarget) + (dst_positive_scale_bottomlayertarget)) * S ((dst_positive_code_bottomlayertarget) + (dst_positive_scale_bottomlayertarget)) + ((dst_positive_scale_bottomlayertarget) + (dst_positive_scale_bottomlayertarget))) + (((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) * S ((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) + ((dst_negative_scale_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)))) + ((((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) * S ((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) + ((dst_negative_scale_bottomlayertarget) + (dst_negative_scale_bottomlayertarget))) + (((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) * S ((dst_negative_code_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)) + ((dst_negative_scale_bottomlayertarget) + (dst_negative_scale_bottomlayertarget)))))) /\ (((((exists ff_h_pvs_bottomlayertargetpositive. ff_h_pvs_bottomlayertargetpositive + S (dst_positive_bottomlayertarget) = S ((S (dsr_index_bottomlayer)) * dst_positive_scale_bottomlayertarget)) /\ exists ff_q_pvs_bottomlayertargetpositive. dst_positive_code_bottomlayertarget = ff_q_pvs_bottomlayertargetpositive * S ((S (dsr_index_bottomlayer)) * dst_positive_scale_bottomlayertarget) + (dst_positive_bottomlayertarget))) /\ (((((exists ff_h_pvs_bottomlayertargetnegative. ff_h_pvs_bottomlayertargetnegative + S (dst_negative_bottomlayertarget) = S ((S (dsr_index_bottomlayer)) * dst_negative_scale_bottomlayertarget)) /\ exists ff_q_pvs_bottomlayertargetnegative. dst_negative_code_bottomlayertarget = ff_q_pvs_bottomlayertargetnegative * S ((S (dsr_index_bottomlayer)) * dst_negative_scale_bottomlayertarget) + (dst_negative_bottomlayertarget))) /\ (exists ge_balance_positive_bottomlayertargetvalue ge_balance_negative_bottomlayertargetvalue. (((((dsr_value_bottomlayer) = 2 * (ge_balance_positive_bottomlayertargetvalue) /\ (ge_balance_negative_bottomlayertargetvalue) = 0) \/ exists ge_signed_half_bottomlayertargetvaluedecode. (((dsr_value_bottomlayer) = 2 * ge_signed_half_bottomlayertargetvaluedecode + 1 /\ (ge_balance_positive_bottomlayertargetvalue) = 0) /\ (ge_balance_negative_bottomlayertargetvalue) = S ge_signed_half_bottomlayertargetvaluedecode))) /\ ((dst_positive_bottomlayertarget) + ge_balance_negative_bottomlayertargetvalue = (dst_negative_bottomlayertarget) + ge_balance_positive_bottomlayertargetvalue)))))))))

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