ArithScale(a,F,G,l)

((exists dst_positive_code_lowertierinput_table dst_positive_scale_lowertierinput_table dst_negative_code_lowertierinput_table dst_negative_scale_lowertierinput_table. ((((F)) = (((((dst_positive_code_lowertierinput_table) + (dst_positive_scale_lowertierinput_table)) * S ((dst_positive_code_lowertierinput_table) + (dst_positive_scale_lowertierinput_table)) + ((dst_positive_scale_lowertierinput_table) + (dst_positive_scale_lowertierinput_table))) + (((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) * S ((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) + ((dst_negative_scale_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)))) * S ((((dst_positive_code_lowertierinput_table) + (dst_positive_scale_lowertierinput_table)) * S ((dst_positive_code_lowertierinput_table) + (dst_positive_scale_lowertierinput_table)) + ((dst_positive_scale_lowertierinput_table) + (dst_positive_scale_lowertierinput_table))) + (((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) * S ((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) + ((dst_negative_scale_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)))) + ((((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) * S ((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) + ((dst_negative_scale_lowertierinput_table) + (dst_negative_scale_lowertierinput_table))) + (((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) * S ((dst_negative_code_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)) + ((dst_negative_scale_lowertierinput_table) + (dst_negative_scale_lowertierinput_table)))))) /\ (forall dst_index_lowertierinput_table. (exists pvs_le_gap_lowertierinput_tabledomain. pvs_le_gap_lowertierinput_tabledomain + (dst_index_lowertierinput_table) = ((l))) -> exists dst_positive_lowertierinput_table dst_negative_lowertierinput_table dst_value_lowertierinput_table. ((((exists ff_h_pvs_lowertierinput_tableentrypositive. ff_h_pvs_lowertierinput_tableentrypositive + S (dst_positive_lowertierinput_table) = S ((S (dst_index_lowertierinput_table)) * dst_positive_scale_lowertierinput_table)) /\ exists ff_q_pvs_lowertierinput_tableentrypositive. dst_positive_code_lowertierinput_table = ff_q_pvs_lowertierinput_tableentrypositive * S ((S (dst_index_lowertierinput_table)) * dst_positive_scale_lowertierinput_table) + (dst_positive_lowertierinput_table))) /\ (((((exists ff_h_pvs_lowertierinput_tableentrynegative. ff_h_pvs_lowertierinput_tableentrynegative + S (dst_negative_lowertierinput_table) = S ((S (dst_index_lowertierinput_table)) * dst_negative_scale_lowertierinput_table)) /\ exists ff_q_pvs_lowertierinput_tableentrynegative. dst_negative_code_lowertierinput_table = ff_q_pvs_lowertierinput_tableentrynegative * S ((S (dst_index_lowertierinput_table)) * dst_negative_scale_lowertierinput_table) + (dst_negative_lowertierinput_table))) /\ (exists ge_balance_positive_lowertierinput_tableentryvalue ge_balance_negative_lowertierinput_tableentryvalue. (((((dst_value_lowertierinput_table) = 2 * (ge_balance_positive_lowertierinput_tableentryvalue) /\ (ge_balance_negative_lowertierinput_tableentryvalue) = 0) \/ exists ge_signed_half_lowertierinput_tableentryvaluedecode. (((dst_value_lowertierinput_table) = 2 * ge_signed_half_lowertierinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowertierinput_tableentryvalue) = 0) /\ (ge_balance_negative_lowertierinput_tableentryvalue) = S ge_signed_half_lowertierinput_tableentryvaluedecode))) /\ ((dst_positive_lowertierinput_table) + ge_balance_negative_lowertierinput_tableentryvalue = (dst_negative_lowertierinput_table) + ge_balance_positive_lowertierinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowertieroutput_table dst_positive_scale_lowertieroutput_table dst_negative_code_lowertieroutput_table dst_negative_scale_lowertieroutput_table. ((((G)) = (((((dst_positive_code_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table)) * S ((dst_positive_code_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table)) + ((dst_positive_scale_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table))) + (((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) * S ((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) + ((dst_negative_scale_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)))) * S ((((dst_positive_code_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table)) * S ((dst_positive_code_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table)) + ((dst_positive_scale_lowertieroutput_table) + (dst_positive_scale_lowertieroutput_table))) + (((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) * S ((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) + ((dst_negative_scale_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)))) + ((((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) * S ((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) + ((dst_negative_scale_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table))) + (((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) * S ((dst_negative_code_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)) + ((dst_negative_scale_lowertieroutput_table) + (dst_negative_scale_lowertieroutput_table)))))) /\ (forall dst_index_lowertieroutput_table. (exists pvs_le_gap_lowertieroutput_tabledomain. pvs_le_gap_lowertieroutput_tabledomain + (dst_index_lowertieroutput_table) = ((l))) -> exists dst_positive_lowertieroutput_table dst_negative_lowertieroutput_table dst_value_lowertieroutput_table. ((((exists ff_h_pvs_lowertieroutput_tableentrypositive. ff_h_pvs_lowertieroutput_tableentrypositive + S (dst_positive_lowertieroutput_table) = S ((S (dst_index_lowertieroutput_table)) * dst_positive_scale_lowertieroutput_table)) /\ exists ff_q_pvs_lowertieroutput_tableentrypositive. dst_positive_code_lowertieroutput_table = ff_q_pvs_lowertieroutput_tableentrypositive * S ((S (dst_index_lowertieroutput_table)) * dst_positive_scale_lowertieroutput_table) + (dst_positive_lowertieroutput_table))) /\ (((((exists ff_h_pvs_lowertieroutput_tableentrynegative. ff_h_pvs_lowertieroutput_tableentrynegative + S (dst_negative_lowertieroutput_table) = S ((S (dst_index_lowertieroutput_table)) * dst_negative_scale_lowertieroutput_table)) /\ exists ff_q_pvs_lowertieroutput_tableentrynegative. dst_negative_code_lowertieroutput_table = ff_q_pvs_lowertieroutput_tableentrynegative * S ((S (dst_index_lowertieroutput_table)) * dst_negative_scale_lowertieroutput_table) + (dst_negative_lowertieroutput_table))) /\ (exists ge_balance_positive_lowertieroutput_tableentryvalue ge_balance_negative_lowertieroutput_tableentryvalue. (((((dst_value_lowertieroutput_table) = 2 * (ge_balance_positive_lowertieroutput_tableentryvalue) /\ (ge_balance_negative_lowertieroutput_tableentryvalue) = 0) \/ exists ge_signed_half_lowertieroutput_tableentryvaluedecode. (((dst_value_lowertieroutput_table) = 2 * ge_signed_half_lowertieroutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowertieroutput_tableentryvalue) = 0) /\ (ge_balance_negative_lowertieroutput_tableentryvalue) = S ge_signed_half_lowertieroutput_tableentryvaluedecode))) /\ ((dst_positive_lowertieroutput_table) + ge_balance_negative_lowertieroutput_tableentryvalue = (dst_negative_lowertieroutput_table) + ge_balance_positive_lowertieroutput_tableentryvalue))))))))) /\ (forall sto_index_lowertierentries. (exists pvs_gap_lowertierentriesbound. pvs_gap_lowertierentriesbound + S (sto_index_lowertierentries) = ((l))) -> exists sto_input_lowertierentries sto_output_lowertierentries. ((exists dst_positive_code_lowertierentriesentryinput dst_positive_scale_lowertierentriesentryinput dst_negative_code_lowertierentriesentryinput dst_negative_scale_lowertierentriesentryinput dst_positive_lowertierentriesentryinput dst_negative_lowertierentriesentryinput. ((((F)) = (((((dst_positive_code_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput)) * S ((dst_positive_code_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput)) + ((dst_positive_scale_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput))) + (((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) * S ((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) + ((dst_negative_scale_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)))) * S ((((dst_positive_code_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput)) * S ((dst_positive_code_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput)) + ((dst_positive_scale_lowertierentriesentryinput) + (dst_positive_scale_lowertierentriesentryinput))) + (((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) * S ((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) + ((dst_negative_scale_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)))) + ((((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) * S ((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) + ((dst_negative_scale_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput))) + (((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) * S ((dst_negative_code_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)) + ((dst_negative_scale_lowertierentriesentryinput) + (dst_negative_scale_lowertierentriesentryinput)))))) /\ (((((exists ff_h_pvs_lowertierentriesentryinputpositive. ff_h_pvs_lowertierentriesentryinputpositive + S (dst_positive_lowertierentriesentryinput) = S ((S (sto_index_lowertierentries)) * dst_positive_scale_lowertierentriesentryinput)) /\ exists ff_q_pvs_lowertierentriesentryinputpositive. dst_positive_code_lowertierentriesentryinput = ff_q_pvs_lowertierentriesentryinputpositive * S ((S (sto_index_lowertierentries)) * dst_positive_scale_lowertierentriesentryinput) + (dst_positive_lowertierentriesentryinput))) /\ (((((exists ff_h_pvs_lowertierentriesentryinputnegative. ff_h_pvs_lowertierentriesentryinputnegative + S (dst_negative_lowertierentriesentryinput) = S ((S (sto_index_lowertierentries)) * dst_negative_scale_lowertierentriesentryinput)) /\ exists ff_q_pvs_lowertierentriesentryinputnegative. dst_negative_code_lowertierentriesentryinput = ff_q_pvs_lowertierentriesentryinputnegative * S ((S (sto_index_lowertierentries)) * dst_negative_scale_lowertierentriesentryinput) + (dst_negative_lowertierentriesentryinput))) /\ (exists ge_balance_positive_lowertierentriesentryinputvalue ge_balance_negative_lowertierentriesentryinputvalue. (((((sto_input_lowertierentries) = 2 * (ge_balance_positive_lowertierentriesentryinputvalue) /\ (ge_balance_negative_lowertierentriesentryinputvalue) = 0) \/ exists ge_signed_half_lowertierentriesentryinputvaluedecode. (((sto_input_lowertierentries) = 2 * ge_signed_half_lowertierentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_lowertierentriesentryinputvalue) = 0) /\ (ge_balance_negative_lowertierentriesentryinputvalue) = S ge_signed_half_lowertierentriesentryinputvaluedecode))) /\ ((dst_positive_lowertierentriesentryinput) + ge_balance_negative_lowertierentriesentryinputvalue = (dst_negative_lowertierentriesentryinput) + ge_balance_positive_lowertierentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_lowertierentriesentryoutput dst_positive_scale_lowertierentriesentryoutput dst_negative_code_lowertierentriesentryoutput dst_negative_scale_lowertierentriesentryoutput dst_positive_lowertierentriesentryoutput dst_negative_lowertierentriesentryoutput. ((((G)) = (((((dst_positive_code_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput)) * S ((dst_positive_code_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput)) + ((dst_positive_scale_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput))) + (((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) * S ((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) + ((dst_negative_scale_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)))) * S ((((dst_positive_code_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput)) * S ((dst_positive_code_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput)) + ((dst_positive_scale_lowertierentriesentryoutput) + (dst_positive_scale_lowertierentriesentryoutput))) + (((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) * S ((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) + ((dst_negative_scale_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)))) + ((((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) * S ((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) + ((dst_negative_scale_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput))) + (((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) * S ((dst_negative_code_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)) + ((dst_negative_scale_lowertierentriesentryoutput) + (dst_negative_scale_lowertierentriesentryoutput)))))) /\ (((((exists ff_h_pvs_lowertierentriesentryoutputpositive. ff_h_pvs_lowertierentriesentryoutputpositive + S (dst_positive_lowertierentriesentryoutput) = S ((S (sto_index_lowertierentries)) * dst_positive_scale_lowertierentriesentryoutput)) /\ exists ff_q_pvs_lowertierentriesentryoutputpositive. dst_positive_code_lowertierentriesentryoutput = ff_q_pvs_lowertierentriesentryoutputpositive * S ((S (sto_index_lowertierentries)) * dst_positive_scale_lowertierentriesentryoutput) + (dst_positive_lowertierentriesentryoutput))) /\ (((((exists ff_h_pvs_lowertierentriesentryoutputnegative. ff_h_pvs_lowertierentriesentryoutputnegative + S (dst_negative_lowertierentriesentryoutput) = S ((S (sto_index_lowertierentries)) * dst_negative_scale_lowertierentriesentryoutput)) /\ exists ff_q_pvs_lowertierentriesentryoutputnegative. dst_negative_code_lowertierentriesentryoutput = ff_q_pvs_lowertierentriesentryoutputnegative * S ((S (sto_index_lowertierentries)) * dst_negative_scale_lowertierentriesentryoutput) + (dst_negative_lowertierentriesentryoutput))) /\ (exists ge_balance_positive_lowertierentriesentryoutputvalue ge_balance_negative_lowertierentriesentryoutputvalue. (((((sto_output_lowertierentries) = 2 * (ge_balance_positive_lowertierentriesentryoutputvalue) /\ (ge_balance_negative_lowertierentriesentryoutputvalue) = 0) \/ exists ge_signed_half_lowertierentriesentryoutputvaluedecode. (((sto_output_lowertierentries) = 2 * ge_signed_half_lowertierentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_lowertierentriesentryoutputvalue) = 0) /\ (ge_balance_negative_lowertierentriesentryoutputvalue) = S ge_signed_half_lowertierentriesentryoutputvaluedecode))) /\ ((dst_positive_lowertierentriesentryoutput) + ge_balance_negative_lowertierentriesentryoutputvalue = (dst_negative_lowertierentriesentryoutput) + ge_balance_positive_lowertierentriesentryoutputvalue))))))))) /\ (exists sto_ap_lowertierentriesentryoperation sto_an_lowertierentriesentryoperation sto_bp_lowertierentriesentryoperation sto_bn_lowertierentriesentryoperation sto_cp_lowertierentriesentryoperation sto_cn_lowertierentriesentryoperation. ((((((a)) = 2 * (sto_ap_lowertierentriesentryoperation) /\ (sto_an_lowertierentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierentriesentryoperationleft. ((((a)) = 2 * ge_signed_half_lowertierentriesentryoperationleft + 1 /\ (sto_ap_lowertierentriesentryoperation) = 0) /\ (sto_an_lowertierentriesentryoperation) = S ge_signed_half_lowertierentriesentryoperationleft))) /\ ((((((sto_input_lowertierentries) = 2 * (sto_bp_lowertierentriesentryoperation) /\ (sto_bn_lowertierentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierentriesentryoperationright. (((sto_input_lowertierentries) = 2 * ge_signed_half_lowertierentriesentryoperationright + 1 /\ (sto_bp_lowertierentriesentryoperation) = 0) /\ (sto_bn_lowertierentriesentryoperation) = S ge_signed_half_lowertierentriesentryoperationright))) /\ ((((((sto_output_lowertierentries) = 2 * (sto_cp_lowertierentriesentryoperation) /\ (sto_cn_lowertierentriesentryoperation) = 0) \/ exists ge_signed_half_lowertierentriesentryoperationoutput. (((sto_output_lowertierentries) = 2 * ge_signed_half_lowertierentriesentryoperationoutput + 1 /\ (sto_cp_lowertierentriesentryoperation) = 0) /\ (sto_cn_lowertierentriesentryoperation) = S ge_signed_half_lowertierentriesentryoperationoutput))) /\ ((sto_ap_lowertierentriesentryoperation * sto_bp_lowertierentriesentryoperation + sto_an_lowertierentriesentryoperation * sto_bn_lowertierentriesentryoperation) + sto_cn_lowertierentriesentryoperation = (sto_ap_lowertierentriesentryoperation * sto_bn_lowertierentriesentryoperation + sto_an_lowertierentriesentryoperation * sto_bp_lowertierentriesentryoperation) + sto_cp_lowertierentriesentryoperation))))))))))))))

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