ArithExtend(F,G,l,z)

((exists dst_positive_code_lowertiertable dst_positive_scale_lowertiertable dst_negative_code_lowertiertable dst_negative_scale_lowertiertable. ((((G)) = (((((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 dst_index_lowertierprefix dst_first_lowertierprefix dst_second_lowertierprefix. (exists pvs_gap_lowertierprefixbound. pvs_gap_lowertierprefixbound + S (dst_index_lowertierprefix) = ((l))) -> (exists dst_positive_code_lowertierprefixfirst dst_positive_scale_lowertierprefixfirst dst_negative_code_lowertierprefixfirst dst_negative_scale_lowertierprefixfirst dst_positive_lowertierprefixfirst dst_negative_lowertierprefixfirst. ((((F)) = (((((dst_positive_code_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst)) * S ((dst_positive_code_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst)) + ((dst_positive_scale_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst))) + (((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) * S ((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) + ((dst_negative_scale_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)))) * S ((((dst_positive_code_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst)) * S ((dst_positive_code_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst)) + ((dst_positive_scale_lowertierprefixfirst) + (dst_positive_scale_lowertierprefixfirst))) + (((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) * S ((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) + ((dst_negative_scale_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)))) + ((((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) * S ((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) + ((dst_negative_scale_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst))) + (((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) * S ((dst_negative_code_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)) + ((dst_negative_scale_lowertierprefixfirst) + (dst_negative_scale_lowertierprefixfirst)))))) /\ (((((exists ff_h_pvs_lowertierprefixfirstpositive. ff_h_pvs_lowertierprefixfirstpositive + S (dst_positive_lowertierprefixfirst) = S ((S (dst_index_lowertierprefix)) * dst_positive_scale_lowertierprefixfirst)) /\ exists ff_q_pvs_lowertierprefixfirstpositive. dst_positive_code_lowertierprefixfirst = ff_q_pvs_lowertierprefixfirstpositive * S ((S (dst_index_lowertierprefix)) * dst_positive_scale_lowertierprefixfirst) + (dst_positive_lowertierprefixfirst))) /\ (((((exists ff_h_pvs_lowertierprefixfirstnegative. ff_h_pvs_lowertierprefixfirstnegative + S (dst_negative_lowertierprefixfirst) = S ((S (dst_index_lowertierprefix)) * dst_negative_scale_lowertierprefixfirst)) /\ exists ff_q_pvs_lowertierprefixfirstnegative. dst_negative_code_lowertierprefixfirst = ff_q_pvs_lowertierprefixfirstnegative * S ((S (dst_index_lowertierprefix)) * dst_negative_scale_lowertierprefixfirst) + (dst_negative_lowertierprefixfirst))) /\ (exists ge_balance_positive_lowertierprefixfirstvalue ge_balance_negative_lowertierprefixfirstvalue. (((((dst_first_lowertierprefix) = 2 * (ge_balance_positive_lowertierprefixfirstvalue) /\ (ge_balance_negative_lowertierprefixfirstvalue) = 0) \/ exists ge_signed_half_lowertierprefixfirstvaluedecode. (((dst_first_lowertierprefix) = 2 * ge_signed_half_lowertierprefixfirstvaluedecode + 1 /\ (ge_balance_positive_lowertierprefixfirstvalue) = 0) /\ (ge_balance_negative_lowertierprefixfirstvalue) = S ge_signed_half_lowertierprefixfirstvaluedecode))) /\ ((dst_positive_lowertierprefixfirst) + ge_balance_negative_lowertierprefixfirstvalue = (dst_negative_lowertierprefixfirst) + ge_balance_positive_lowertierprefixfirstvalue))))))))) -> (exists dst_positive_code_lowertierprefixsecond dst_positive_scale_lowertierprefixsecond dst_negative_code_lowertierprefixsecond dst_negative_scale_lowertierprefixsecond dst_positive_lowertierprefixsecond dst_negative_lowertierprefixsecond. ((((G)) = (((((dst_positive_code_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond)) * S ((dst_positive_code_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond)) + ((dst_positive_scale_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond))) + (((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) * S ((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) + ((dst_negative_scale_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)))) * S ((((dst_positive_code_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond)) * S ((dst_positive_code_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond)) + ((dst_positive_scale_lowertierprefixsecond) + (dst_positive_scale_lowertierprefixsecond))) + (((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) * S ((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) + ((dst_negative_scale_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)))) + ((((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) * S ((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) + ((dst_negative_scale_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond))) + (((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) * S ((dst_negative_code_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)) + ((dst_negative_scale_lowertierprefixsecond) + (dst_negative_scale_lowertierprefixsecond)))))) /\ (((((exists ff_h_pvs_lowertierprefixsecondpositive. ff_h_pvs_lowertierprefixsecondpositive + S (dst_positive_lowertierprefixsecond) = S ((S (dst_index_lowertierprefix)) * dst_positive_scale_lowertierprefixsecond)) /\ exists ff_q_pvs_lowertierprefixsecondpositive. dst_positive_code_lowertierprefixsecond = ff_q_pvs_lowertierprefixsecondpositive * S ((S (dst_index_lowertierprefix)) * dst_positive_scale_lowertierprefixsecond) + (dst_positive_lowertierprefixsecond))) /\ (((((exists ff_h_pvs_lowertierprefixsecondnegative. ff_h_pvs_lowertierprefixsecondnegative + S (dst_negative_lowertierprefixsecond) = S ((S (dst_index_lowertierprefix)) * dst_negative_scale_lowertierprefixsecond)) /\ exists ff_q_pvs_lowertierprefixsecondnegative. dst_negative_code_lowertierprefixsecond = ff_q_pvs_lowertierprefixsecondnegative * S ((S (dst_index_lowertierprefix)) * dst_negative_scale_lowertierprefixsecond) + (dst_negative_lowertierprefixsecond))) /\ (exists ge_balance_positive_lowertierprefixsecondvalue ge_balance_negative_lowertierprefixsecondvalue. (((((dst_second_lowertierprefix) = 2 * (ge_balance_positive_lowertierprefixsecondvalue) /\ (ge_balance_negative_lowertierprefixsecondvalue) = 0) \/ exists ge_signed_half_lowertierprefixsecondvaluedecode. (((dst_second_lowertierprefix) = 2 * ge_signed_half_lowertierprefixsecondvaluedecode + 1 /\ (ge_balance_positive_lowertierprefixsecondvalue) = 0) /\ (ge_balance_negative_lowertierprefixsecondvalue) = S ge_signed_half_lowertierprefixsecondvaluedecode))) /\ ((dst_positive_lowertierprefixsecond) + ge_balance_negative_lowertierprefixsecondvalue = (dst_negative_lowertierprefixsecond) + ge_balance_positive_lowertierprefixsecondvalue))))))))) -> dst_first_lowertierprefix = dst_second_lowertierprefix) /\ (exists dst_positive_code_lowertierlast dst_positive_scale_lowertierlast dst_negative_code_lowertierlast dst_negative_scale_lowertierlast dst_positive_lowertierlast dst_negative_lowertierlast. ((((G)) = (((((dst_positive_code_lowertierlast) + (dst_positive_scale_lowertierlast)) * S ((dst_positive_code_lowertierlast) + (dst_positive_scale_lowertierlast)) + ((dst_positive_scale_lowertierlast) + (dst_positive_scale_lowertierlast))) + (((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) * S ((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) + ((dst_negative_scale_lowertierlast) + (dst_negative_scale_lowertierlast)))) * S ((((dst_positive_code_lowertierlast) + (dst_positive_scale_lowertierlast)) * S ((dst_positive_code_lowertierlast) + (dst_positive_scale_lowertierlast)) + ((dst_positive_scale_lowertierlast) + (dst_positive_scale_lowertierlast))) + (((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) * S ((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) + ((dst_negative_scale_lowertierlast) + (dst_negative_scale_lowertierlast)))) + ((((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) * S ((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) + ((dst_negative_scale_lowertierlast) + (dst_negative_scale_lowertierlast))) + (((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) * S ((dst_negative_code_lowertierlast) + (dst_negative_scale_lowertierlast)) + ((dst_negative_scale_lowertierlast) + (dst_negative_scale_lowertierlast)))))) /\ (((((exists ff_h_pvs_lowertierlastpositive. ff_h_pvs_lowertierlastpositive + S (dst_positive_lowertierlast) = S ((S ((l))) * dst_positive_scale_lowertierlast)) /\ exists ff_q_pvs_lowertierlastpositive. dst_positive_code_lowertierlast = ff_q_pvs_lowertierlastpositive * S ((S ((l))) * dst_positive_scale_lowertierlast) + (dst_positive_lowertierlast))) /\ (((((exists ff_h_pvs_lowertierlastnegative. ff_h_pvs_lowertierlastnegative + S (dst_negative_lowertierlast) = S ((S ((l))) * dst_negative_scale_lowertierlast)) /\ exists ff_q_pvs_lowertierlastnegative. dst_negative_code_lowertierlast = ff_q_pvs_lowertierlastnegative * S ((S ((l))) * dst_negative_scale_lowertierlast) + (dst_negative_lowertierlast))) /\ (exists ge_balance_positive_lowertierlastvalue ge_balance_negative_lowertierlastvalue. ((((((z)) = 2 * (ge_balance_positive_lowertierlastvalue) /\ (ge_balance_negative_lowertierlastvalue) = 0) \/ exists ge_signed_half_lowertierlastvaluedecode. ((((z)) = 2 * ge_signed_half_lowertierlastvaluedecode + 1 /\ (ge_balance_positive_lowertierlastvalue) = 0) /\ (ge_balance_negative_lowertierlastvalue) = S ge_signed_half_lowertierlastvaluedecode))) /\ ((dst_positive_lowertierlast) + ge_balance_negative_lowertierlastvalue = (dst_negative_lowertierlast) + ge_balance_positive_lowertierlastvalue))))))))))))

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