MultiplicativePrefix(N,F)

((~(((N))=0)) /\ (((exists dst_positive_code_g009_definitiontable dst_positive_scale_g009_definitiontable dst_negative_code_g009_definitiontable dst_negative_scale_g009_definitiontable. ((((F)) = (((((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) * S ((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) + ((dst_positive_scale_g009_definitiontable) + (dst_positive_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))) * S ((((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) * S ((dst_positive_code_g009_definitiontable) + (dst_positive_scale_g009_definitiontable)) + ((dst_positive_scale_g009_definitiontable) + (dst_positive_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))) + ((((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable))) + (((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) * S ((dst_negative_code_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)) + ((dst_negative_scale_g009_definitiontable) + (dst_negative_scale_g009_definitiontable)))))) /\ (forall dst_index_g009_definitiontable. (exists pvs_le_gap_g009_definitiontabledomain. pvs_le_gap_g009_definitiontabledomain + (dst_index_g009_definitiontable) = ((N))) -> exists dst_positive_g009_definitiontable dst_negative_g009_definitiontable dst_value_g009_definitiontable. ((((exists ff_h_pvs_g009_definitiontableentrypositive. ff_h_pvs_g009_definitiontableentrypositive + S (dst_positive_g009_definitiontable) = S ((S (dst_index_g009_definitiontable)) * dst_positive_scale_g009_definitiontable)) /\ exists ff_q_pvs_g009_definitiontableentrypositive. dst_positive_code_g009_definitiontable = ff_q_pvs_g009_definitiontableentrypositive * S ((S (dst_index_g009_definitiontable)) * dst_positive_scale_g009_definitiontable) + (dst_positive_g009_definitiontable))) /\ (((((exists ff_h_pvs_g009_definitiontableentrynegative. ff_h_pvs_g009_definitiontableentrynegative + S (dst_negative_g009_definitiontable) = S ((S (dst_index_g009_definitiontable)) * dst_negative_scale_g009_definitiontable)) /\ exists ff_q_pvs_g009_definitiontableentrynegative. dst_negative_code_g009_definitiontable = ff_q_pvs_g009_definitiontableentrynegative * S ((S (dst_index_g009_definitiontable)) * dst_negative_scale_g009_definitiontable) + (dst_negative_g009_definitiontable))) /\ (exists ge_balance_positive_g009_definitiontableentryvalue ge_balance_negative_g009_definitiontableentryvalue. (((((dst_value_g009_definitiontable) = 2 * (ge_balance_positive_g009_definitiontableentryvalue) /\ (ge_balance_negative_g009_definitiontableentryvalue) = 0) \/ exists ge_signed_half_g009_definitiontableentryvaluedecode. (((dst_value_g009_definitiontable) = 2 * ge_signed_half_g009_definitiontableentryvaluedecode + 1 /\ (ge_balance_positive_g009_definitiontableentryvalue) = 0) /\ (ge_balance_negative_g009_definitiontableentryvalue) = S ge_signed_half_g009_definitiontableentryvaluedecode))) /\ ((dst_positive_g009_definitiontable) + ge_balance_negative_g009_definitiontableentryvalue = (dst_negative_g009_definitiontable) + ge_balance_positive_g009_definitiontableentryvalue))))))))) /\ (((exists dst_positive_code_g009_definitionone dst_positive_scale_g009_definitionone dst_negative_code_g009_definitionone dst_negative_scale_g009_definitionone dst_positive_g009_definitionone dst_negative_g009_definitionone. ((((F)) = (((((dst_positive_code_g009_definitionone) + (dst_positive_scale_g009_definitionone)) * S ((dst_positive_code_g009_definitionone) + (dst_positive_scale_g009_definitionone)) + ((dst_positive_scale_g009_definitionone) + (dst_positive_scale_g009_definitionone))) + (((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) * S ((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) + ((dst_negative_scale_g009_definitionone) + (dst_negative_scale_g009_definitionone)))) * S ((((dst_positive_code_g009_definitionone) + (dst_positive_scale_g009_definitionone)) * S ((dst_positive_code_g009_definitionone) + (dst_positive_scale_g009_definitionone)) + ((dst_positive_scale_g009_definitionone) + (dst_positive_scale_g009_definitionone))) + (((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) * S ((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) + ((dst_negative_scale_g009_definitionone) + (dst_negative_scale_g009_definitionone)))) + ((((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) * S ((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) + ((dst_negative_scale_g009_definitionone) + (dst_negative_scale_g009_definitionone))) + (((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) * S ((dst_negative_code_g009_definitionone) + (dst_negative_scale_g009_definitionone)) + ((dst_negative_scale_g009_definitionone) + (dst_negative_scale_g009_definitionone)))))) /\ (((((exists ff_h_pvs_g009_definitiononepositive. ff_h_pvs_g009_definitiononepositive + S (dst_positive_g009_definitionone) = S ((S (1)) * dst_positive_scale_g009_definitionone)) /\ exists ff_q_pvs_g009_definitiononepositive. dst_positive_code_g009_definitionone = ff_q_pvs_g009_definitiononepositive * S ((S (1)) * dst_positive_scale_g009_definitionone) + (dst_positive_g009_definitionone))) /\ (((((exists ff_h_pvs_g009_definitiononenegative. ff_h_pvs_g009_definitiononenegative + S (dst_negative_g009_definitionone) = S ((S (1)) * dst_negative_scale_g009_definitionone)) /\ exists ff_q_pvs_g009_definitiononenegative. dst_negative_code_g009_definitionone = ff_q_pvs_g009_definitiononenegative * S ((S (1)) * dst_negative_scale_g009_definitionone) + (dst_negative_g009_definitionone))) /\ (exists ge_balance_positive_g009_definitiononevalue ge_balance_negative_g009_definitiononevalue. (((((2) = 2 * (ge_balance_positive_g009_definitiononevalue) /\ (ge_balance_negative_g009_definitiononevalue) = 0) \/ exists ge_signed_half_g009_definitiononevaluedecode. (((2) = 2 * ge_signed_half_g009_definitiononevaluedecode + 1 /\ (ge_balance_positive_g009_definitiononevalue) = 0) /\ (ge_balance_negative_g009_definitiononevalue) = S ge_signed_half_g009_definitiononevaluedecode))) /\ ((dst_positive_g009_definitionone) + ge_balance_negative_g009_definitiononevalue = (dst_negative_g009_definitionone) + ge_balance_positive_g009_definitiononevalue))))))))) /\ (forall mp_a_g009_definition mp_b_g009_definition mp_x_g009_definition mp_y_g009_definition mp_z_g009_definition. ~(mp_a_g009_definition=0) -> ~(mp_b_g009_definition=0) -> (exists pvs_le_gap_g009_definitionbound. pvs_le_gap_g009_definitionbound + (mp_a_g009_definition*mp_b_g009_definition) = ((N))) -> (forall frp_divisor_g009_definitioncoprime. (exists frp_left_factor_g009_definitioncoprime. mp_a_g009_definition = frp_divisor_g009_definitioncoprime * frp_left_factor_g009_definitioncoprime) -> (exists frp_right_factor_g009_definitioncoprime. mp_b_g009_definition = frp_divisor_g009_definitioncoprime * frp_right_factor_g009_definitioncoprime) -> frp_divisor_g009_definitioncoprime = 1) -> (exists dst_positive_code_g009_definitionfirst dst_positive_scale_g009_definitionfirst dst_negative_code_g009_definitionfirst dst_negative_scale_g009_definitionfirst dst_positive_g009_definitionfirst dst_negative_g009_definitionfirst. ((((F)) = (((((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) * S ((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) + ((dst_positive_scale_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))) * S ((((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) * S ((dst_positive_code_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst)) + ((dst_positive_scale_g009_definitionfirst) + (dst_positive_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))) + ((((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst))) + (((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) * S ((dst_negative_code_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)) + ((dst_negative_scale_g009_definitionfirst) + (dst_negative_scale_g009_definitionfirst)))))) /\ (((((exists ff_h_pvs_g009_definitionfirstpositive. ff_h_pvs_g009_definitionfirstpositive + S (dst_positive_g009_definitionfirst) = S ((S (mp_a_g009_definition)) * dst_positive_scale_g009_definitionfirst)) /\ exists ff_q_pvs_g009_definitionfirstpositive. dst_positive_code_g009_definitionfirst = ff_q_pvs_g009_definitionfirstpositive * S ((S (mp_a_g009_definition)) * dst_positive_scale_g009_definitionfirst) + (dst_positive_g009_definitionfirst))) /\ (((((exists ff_h_pvs_g009_definitionfirstnegative. ff_h_pvs_g009_definitionfirstnegative + S (dst_negative_g009_definitionfirst) = S ((S (mp_a_g009_definition)) * dst_negative_scale_g009_definitionfirst)) /\ exists ff_q_pvs_g009_definitionfirstnegative. dst_negative_code_g009_definitionfirst = ff_q_pvs_g009_definitionfirstnegative * S ((S (mp_a_g009_definition)) * dst_negative_scale_g009_definitionfirst) + (dst_negative_g009_definitionfirst))) /\ (exists ge_balance_positive_g009_definitionfirstvalue ge_balance_negative_g009_definitionfirstvalue. (((((mp_x_g009_definition) = 2 * (ge_balance_positive_g009_definitionfirstvalue) /\ (ge_balance_negative_g009_definitionfirstvalue) = 0) \/ exists ge_signed_half_g009_definitionfirstvaluedecode. (((mp_x_g009_definition) = 2 * ge_signed_half_g009_definitionfirstvaluedecode + 1 /\ (ge_balance_positive_g009_definitionfirstvalue) = 0) /\ (ge_balance_negative_g009_definitionfirstvalue) = S ge_signed_half_g009_definitionfirstvaluedecode))) /\ ((dst_positive_g009_definitionfirst) + ge_balance_negative_g009_definitionfirstvalue = (dst_negative_g009_definitionfirst) + ge_balance_positive_g009_definitionfirstvalue))))))))) -> (exists dst_positive_code_g009_definitionsecond dst_positive_scale_g009_definitionsecond dst_negative_code_g009_definitionsecond dst_negative_scale_g009_definitionsecond dst_positive_g009_definitionsecond dst_negative_g009_definitionsecond. ((((F)) = (((((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) * S ((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) + ((dst_positive_scale_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))) * S ((((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) * S ((dst_positive_code_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond)) + ((dst_positive_scale_g009_definitionsecond) + (dst_positive_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))) + ((((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond))) + (((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) * S ((dst_negative_code_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)) + ((dst_negative_scale_g009_definitionsecond) + (dst_negative_scale_g009_definitionsecond)))))) /\ (((((exists ff_h_pvs_g009_definitionsecondpositive. ff_h_pvs_g009_definitionsecondpositive + S (dst_positive_g009_definitionsecond) = S ((S (mp_b_g009_definition)) * dst_positive_scale_g009_definitionsecond)) /\ exists ff_q_pvs_g009_definitionsecondpositive. dst_positive_code_g009_definitionsecond = ff_q_pvs_g009_definitionsecondpositive * S ((S (mp_b_g009_definition)) * dst_positive_scale_g009_definitionsecond) + (dst_positive_g009_definitionsecond))) /\ (((((exists ff_h_pvs_g009_definitionsecondnegative. ff_h_pvs_g009_definitionsecondnegative + S (dst_negative_g009_definitionsecond) = S ((S (mp_b_g009_definition)) * dst_negative_scale_g009_definitionsecond)) /\ exists ff_q_pvs_g009_definitionsecondnegative. dst_negative_code_g009_definitionsecond = ff_q_pvs_g009_definitionsecondnegative * S ((S (mp_b_g009_definition)) * dst_negative_scale_g009_definitionsecond) + (dst_negative_g009_definitionsecond))) /\ (exists ge_balance_positive_g009_definitionsecondvalue ge_balance_negative_g009_definitionsecondvalue. (((((mp_y_g009_definition) = 2 * (ge_balance_positive_g009_definitionsecondvalue) /\ (ge_balance_negative_g009_definitionsecondvalue) = 0) \/ exists ge_signed_half_g009_definitionsecondvaluedecode. (((mp_y_g009_definition) = 2 * ge_signed_half_g009_definitionsecondvaluedecode + 1 /\ (ge_balance_positive_g009_definitionsecondvalue) = 0) /\ (ge_balance_negative_g009_definitionsecondvalue) = S ge_signed_half_g009_definitionsecondvaluedecode))) /\ ((dst_positive_g009_definitionsecond) + ge_balance_negative_g009_definitionsecondvalue = (dst_negative_g009_definitionsecond) + ge_balance_positive_g009_definitionsecondvalue))))))))) -> (exists dst_positive_code_g009_definitionproduct dst_positive_scale_g009_definitionproduct dst_negative_code_g009_definitionproduct dst_negative_scale_g009_definitionproduct dst_positive_g009_definitionproduct dst_negative_g009_definitionproduct. ((((F)) = (((((dst_positive_code_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct)) * S ((dst_positive_code_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct)) + ((dst_positive_scale_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct))) + (((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) * S ((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) + ((dst_negative_scale_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)))) * S ((((dst_positive_code_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct)) * S ((dst_positive_code_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct)) + ((dst_positive_scale_g009_definitionproduct) + (dst_positive_scale_g009_definitionproduct))) + (((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) * S ((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) + ((dst_negative_scale_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)))) + ((((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) * S ((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) + ((dst_negative_scale_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct))) + (((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) * S ((dst_negative_code_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)) + ((dst_negative_scale_g009_definitionproduct) + (dst_negative_scale_g009_definitionproduct)))))) /\ (((((exists ff_h_pvs_g009_definitionproductpositive. ff_h_pvs_g009_definitionproductpositive + S (dst_positive_g009_definitionproduct) = S ((S (mp_a_g009_definition*mp_b_g009_definition)) * dst_positive_scale_g009_definitionproduct)) /\ exists ff_q_pvs_g009_definitionproductpositive. dst_positive_code_g009_definitionproduct = ff_q_pvs_g009_definitionproductpositive * S ((S (mp_a_g009_definition*mp_b_g009_definition)) * dst_positive_scale_g009_definitionproduct) + (dst_positive_g009_definitionproduct))) /\ (((((exists ff_h_pvs_g009_definitionproductnegative. ff_h_pvs_g009_definitionproductnegative + S (dst_negative_g009_definitionproduct) = S ((S (mp_a_g009_definition*mp_b_g009_definition)) * dst_negative_scale_g009_definitionproduct)) /\ exists ff_q_pvs_g009_definitionproductnegative. dst_negative_code_g009_definitionproduct = ff_q_pvs_g009_definitionproductnegative * S ((S (mp_a_g009_definition*mp_b_g009_definition)) * dst_negative_scale_g009_definitionproduct) + (dst_negative_g009_definitionproduct))) /\ (exists ge_balance_positive_g009_definitionproductvalue ge_balance_negative_g009_definitionproductvalue. (((((mp_z_g009_definition) = 2 * (ge_balance_positive_g009_definitionproductvalue) /\ (ge_balance_negative_g009_definitionproductvalue) = 0) \/ exists ge_signed_half_g009_definitionproductvaluedecode. (((mp_z_g009_definition) = 2 * ge_signed_half_g009_definitionproductvaluedecode + 1 /\ (ge_balance_positive_g009_definitionproductvalue) = 0) /\ (ge_balance_negative_g009_definitionproductvalue) = S ge_signed_half_g009_definitionproductvaluedecode))) /\ ((dst_positive_g009_definitionproduct) + ge_balance_negative_g009_definitionproductvalue = (dst_negative_g009_definitionproduct) + ge_balance_positive_g009_definitionproductvalue))))))))) -> (exists sto_ap_g009_definitionlaw sto_an_g009_definitionlaw sto_bp_g009_definitionlaw sto_bn_g009_definitionlaw sto_cp_g009_definitionlaw sto_cn_g009_definitionlaw. (((((mp_x_g009_definition) = 2 * (sto_ap_g009_definitionlaw) /\ (sto_an_g009_definitionlaw) = 0) \/ exists ge_signed_half_g009_definitionlawleft. (((mp_x_g009_definition) = 2 * ge_signed_half_g009_definitionlawleft + 1 /\ (sto_ap_g009_definitionlaw) = 0) /\ (sto_an_g009_definitionlaw) = S ge_signed_half_g009_definitionlawleft))) /\ ((((((mp_y_g009_definition) = 2 * (sto_bp_g009_definitionlaw) /\ (sto_bn_g009_definitionlaw) = 0) \/ exists ge_signed_half_g009_definitionlawright. (((mp_y_g009_definition) = 2 * ge_signed_half_g009_definitionlawright + 1 /\ (sto_bp_g009_definitionlaw) = 0) /\ (sto_bn_g009_definitionlaw) = S ge_signed_half_g009_definitionlawright))) /\ ((((((mp_z_g009_definition) = 2 * (sto_cp_g009_definitionlaw) /\ (sto_cn_g009_definitionlaw) = 0) \/ exists ge_signed_half_g009_definitionlawoutput. (((mp_z_g009_definition) = 2 * ge_signed_half_g009_definitionlawoutput + 1 /\ (sto_cp_g009_definitionlaw) = 0) /\ (sto_cn_g009_definitionlaw) = S ge_signed_half_g009_definitionlawoutput))) /\ ((sto_ap_g009_definitionlaw * sto_bp_g009_definitionlaw + sto_an_g009_definitionlaw * sto_bn_g009_definitionlaw) + sto_cn_g009_definitionlaw = (sto_ap_g009_definitionlaw * sto_bn_g009_definitionlaw + sto_an_g009_definitionlaw * sto_bp_g009_definitionlaw) + sto_cp_g009_definitionlaw)))))))))))))

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