dirichlet_convolution_prefix_zero_constructor

Exact expanded first-order arithmetic statement

forall F G n M. (exists dst_positive_code_base_table dst_positive_scale_base_table dst_negative_code_base_table dst_negative_scale_base_table. (((M) = (((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) * S ((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) + ((((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))))) /\ (forall dst_index_base_table. (exists pvs_le_gap_base_tabledomain. pvs_le_gap_base_tabledomain + (dst_index_base_table) = (0)) -> exists dst_positive_base_table dst_negative_base_table dst_value_base_table. ((((exists ff_h_pvs_base_tableentrypositive. ff_h_pvs_base_tableentrypositive + S (dst_positive_base_table) = S ((S (dst_index_base_table)) * dst_positive_scale_base_table)) /\ exists ff_q_pvs_base_tableentrypositive. dst_positive_code_base_table = ff_q_pvs_base_tableentrypositive * S ((S (dst_index_base_table)) * dst_positive_scale_base_table) + (dst_positive_base_table))) /\ (((((exists ff_h_pvs_base_tableentrynegative. ff_h_pvs_base_tableentrynegative + S (dst_negative_base_table) = S ((S (dst_index_base_table)) * dst_negative_scale_base_table)) /\ exists ff_q_pvs_base_tableentrynegative. dst_negative_code_base_table = ff_q_pvs_base_tableentrynegative * S ((S (dst_index_base_table)) * dst_negative_scale_base_table) + (dst_negative_base_table))) /\ (exists ge_balance_positive_base_tableentryvalue ge_balance_negative_base_tableentryvalue. (((((dst_value_base_table) = 2 * (ge_balance_positive_base_tableentryvalue) /\ (ge_balance_negative_base_tableentryvalue) = 0) \/ exists ge_signed_half_base_tableentryvaluedecode. (((dst_value_base_table) = 2 * ge_signed_half_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_base_tableentryvalue) = 0) /\ (ge_balance_negative_base_tableentryvalue) = S ge_signed_half_base_tableentryvaluedecode))) /\ ((dst_positive_base_table) + ge_balance_negative_base_tableentryvalue = (dst_negative_base_table) + ge_balance_positive_base_tableentryvalue))))))))) -> (exists dst_positive_code_base_entry dst_positive_scale_base_entry dst_negative_code_base_entry dst_negative_scale_base_entry dst_positive_base_entry dst_negative_base_entry. (((M) = (((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) * S ((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) + ((((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))))) /\ (((((exists ff_h_pvs_base_entrypositive. ff_h_pvs_base_entrypositive + S (dst_positive_base_entry) = S ((S (0)) * dst_positive_scale_base_entry)) /\ exists ff_q_pvs_base_entrypositive. dst_positive_code_base_entry = ff_q_pvs_base_entrypositive * S ((S (0)) * dst_positive_scale_base_entry) + (dst_positive_base_entry))) /\ (((((exists ff_h_pvs_base_entrynegative. ff_h_pvs_base_entrynegative + S (dst_negative_base_entry) = S ((S (0)) * dst_negative_scale_base_entry)) /\ exists ff_q_pvs_base_entrynegative. dst_negative_code_base_entry = ff_q_pvs_base_entrynegative * S ((S (0)) * dst_negative_scale_base_entry) + (dst_negative_base_entry))) /\ (exists ge_balance_positive_base_entryvalue ge_balance_negative_base_entryvalue. (((((0) = 2 * (ge_balance_positive_base_entryvalue) /\ (ge_balance_negative_base_entryvalue) = 0) \/ exists ge_signed_half_base_entryvaluedecode. (((0) = 2 * ge_signed_half_base_entryvaluedecode + 1 /\ (ge_balance_positive_base_entryvalue) = 0) /\ (ge_balance_negative_base_entryvalue) = S ge_signed_half_base_entryvaluedecode))) /\ ((dst_positive_base_entry) + ge_balance_negative_base_entryvalue = (dst_negative_base_entry) + ge_balance_positive_base_entryvalue))))))))) -> (((exists dst_positive_code_base_resulttable dst_positive_scale_base_resulttable dst_negative_code_base_resulttable dst_negative_scale_base_resulttable. (((M) = (((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) * S ((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) + ((((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))))) /\ (forall dst_index_base_resulttable. (exists pvs_le_gap_base_resulttabledomain. pvs_le_gap_base_resulttabledomain + (dst_index_base_resulttable) = (0)) -> exists dst_positive_base_resulttable dst_negative_base_resulttable dst_value_base_resulttable. ((((exists ff_h_pvs_base_resulttableentrypositive. ff_h_pvs_base_resulttableentrypositive + S (dst_positive_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrypositive. dst_positive_code_base_resulttable = ff_q_pvs_base_resulttableentrypositive * S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable) + (dst_positive_base_resulttable))) /\ (((((exists ff_h_pvs_base_resulttableentrynegative. ff_h_pvs_base_resulttableentrynegative + S (dst_negative_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrynegative. dst_negative_code_base_resulttable = ff_q_pvs_base_resulttableentrynegative * S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable) + (dst_negative_base_resulttable))) /\ (exists ge_balance_positive_base_resulttableentryvalue ge_balance_negative_base_resulttableentryvalue. (((((dst_value_base_resulttable) = 2 * (ge_balance_positive_base_resulttableentryvalue) /\ (ge_balance_negative_base_resulttableentryvalue) = 0) \/ exists ge_signed_half_base_resulttableentryvaluedecode. (((dst_value_base_resulttable) = 2 * ge_signed_half_base_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_base_resulttableentryvalue) = 0) /\ (ge_balance_negative_base_resulttableentryvalue) = S ge_signed_half_base_resulttableentryvaluedecode))) /\ ((dst_positive_base_resulttable) + ge_balance_negative_base_resulttableentryvalue = (dst_negative_base_resulttable) + ge_balance_positive_base_resulttableentryvalue))))))))) /\ (forall dc_index_base_result dc_value_base_result. (exists pvs_le_gap_base_resultdomain. pvs_le_gap_base_resultdomain + (dc_index_base_result) = (0)) -> (exists dst_positive_code_base_resultlookup dst_positive_scale_base_resultlookup dst_negative_code_base_resultlookup dst_negative_scale_base_resultlookup dst_positive_base_resultlookup dst_negative_base_resultlookup. (((M) = (((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) * S ((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) + ((((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))))) /\ (((((exists ff_h_pvs_base_resultlookuppositive. ff_h_pvs_base_resultlookuppositive + S (dst_positive_base_resultlookup) = S ((S (dc_index_base_result)) * dst_positive_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookuppositive. dst_positive_code_base_resultlookup = ff_q_pvs_base_resultlookuppositive * S ((S (dc_index_base_result)) * dst_positive_scale_base_resultlookup) + (dst_positive_base_resultlookup))) /\ (((((exists ff_h_pvs_base_resultlookupnegative. ff_h_pvs_base_resultlookupnegative + S (dst_negative_base_resultlookup) = S ((S (dc_index_base_result)) * dst_negative_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookupnegative. dst_negative_code_base_resultlookup = ff_q_pvs_base_resultlookupnegative * S ((S (dc_index_base_result)) * dst_negative_scale_base_resultlookup) + (dst_negative_base_resultlookup))) /\ (exists ge_balance_positive_base_resultlookupvalue ge_balance_negative_base_resultlookupvalue. (((((dc_value_base_result) = 2 * (ge_balance_positive_base_resultlookupvalue) /\ (ge_balance_negative_base_resultlookupvalue) = 0) \/ exists ge_signed_half_base_resultlookupvaluedecode. (((dc_value_base_result) = 2 * ge_signed_half_base_resultlookupvaluedecode + 1 /\ (ge_balance_positive_base_resultlookupvalue) = 0) /\ (ge_balance_negative_base_resultlookupvalue) = S ge_signed_half_base_resultlookupvaluedecode))) /\ ((dst_positive_base_resultlookup) + ge_balance_negative_base_resultlookupvalue = (dst_negative_base_resultlookup) + ge_balance_positive_base_resultlookupvalue))))))))) -> ((((~((dc_index_base_result)=0)) /\ (exists dc_quotient_base_resultentry dc_left_base_resultentry dc_right_base_resultentry. (((n)=(dc_index_base_result)*dc_quotient_base_resultentry) /\ (((exists dst_positive_code_base_resultentryleft dst_positive_scale_base_resultentryleft dst_negative_code_base_resultentryleft dst_negative_scale_base_resultentryleft dst_positive_base_resultentryleft dst_negative_base_resultentryleft. (((F) = (((((dst_positive_code_base_resultentryleft) + (dst_positive_scale_base_resultentryleft)) * S ((dst_positive_code_base_resultentryleft) + (dst_positive_scale_base_resultentryleft)) + ((dst_positive_scale_base_resultentryleft) + (dst_positive_scale_base_resultentryleft))) + (((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) * S ((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) + ((dst_negative_scale_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)))) * S ((((dst_positive_code_base_resultentryleft) + (dst_positive_scale_base_resultentryleft)) * S ((dst_positive_code_base_resultentryleft) + (dst_positive_scale_base_resultentryleft)) + ((dst_positive_scale_base_resultentryleft) + (dst_positive_scale_base_resultentryleft))) + (((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) * S ((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) + ((dst_negative_scale_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)))) + ((((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) * S ((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) + ((dst_negative_scale_base_resultentryleft) + (dst_negative_scale_base_resultentryleft))) + (((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) * S ((dst_negative_code_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)) + ((dst_negative_scale_base_resultentryleft) + (dst_negative_scale_base_resultentryleft)))))) /\ (((((exists ff_h_pvs_base_resultentryleftpositive. ff_h_pvs_base_resultentryleftpositive + S (dst_positive_base_resultentryleft) = S ((S (dc_index_base_result)) * dst_positive_scale_base_resultentryleft)) /\ exists ff_q_pvs_base_resultentryleftpositive. dst_positive_code_base_resultentryleft = ff_q_pvs_base_resultentryleftpositive * S ((S (dc_index_base_result)) * dst_positive_scale_base_resultentryleft) + (dst_positive_base_resultentryleft))) /\ (((((exists ff_h_pvs_base_resultentryleftnegative. ff_h_pvs_base_resultentryleftnegative + S (dst_negative_base_resultentryleft) = S ((S (dc_index_base_result)) * dst_negative_scale_base_resultentryleft)) /\ exists ff_q_pvs_base_resultentryleftnegative. dst_negative_code_base_resultentryleft = ff_q_pvs_base_resultentryleftnegative * S ((S (dc_index_base_result)) * dst_negative_scale_base_resultentryleft) + (dst_negative_base_resultentryleft))) /\ (exists ge_balance_positive_base_resultentryleftvalue ge_balance_negative_base_resultentryleftvalue. (((((dc_left_base_resultentry) = 2 * (ge_balance_positive_base_resultentryleftvalue) /\ (ge_balance_negative_base_resultentryleftvalue) = 0) \/ exists ge_signed_half_base_resultentryleftvaluedecode. (((dc_left_base_resultentry) = 2 * ge_signed_half_base_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_base_resultentryleftvalue) = 0) /\ (ge_balance_negative_base_resultentryleftvalue) = S ge_signed_half_base_resultentryleftvaluedecode))) /\ ((dst_positive_base_resultentryleft) + ge_balance_negative_base_resultentryleftvalue = (dst_negative_base_resultentryleft) + ge_balance_positive_base_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_base_resultentryright dst_positive_scale_base_resultentryright dst_negative_code_base_resultentryright dst_negative_scale_base_resultentryright dst_positive_base_resultentryright dst_negative_base_resultentryright. (((G) = (((((dst_positive_code_base_resultentryright) + (dst_positive_scale_base_resultentryright)) * S ((dst_positive_code_base_resultentryright) + (dst_positive_scale_base_resultentryright)) + ((dst_positive_scale_base_resultentryright) + (dst_positive_scale_base_resultentryright))) + (((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) * S ((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) + ((dst_negative_scale_base_resultentryright) + (dst_negative_scale_base_resultentryright)))) * S ((((dst_positive_code_base_resultentryright) + (dst_positive_scale_base_resultentryright)) * S ((dst_positive_code_base_resultentryright) + (dst_positive_scale_base_resultentryright)) + ((dst_positive_scale_base_resultentryright) + (dst_positive_scale_base_resultentryright))) + (((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) * S ((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) + ((dst_negative_scale_base_resultentryright) + (dst_negative_scale_base_resultentryright)))) + ((((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) * S ((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) + ((dst_negative_scale_base_resultentryright) + (dst_negative_scale_base_resultentryright))) + (((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) * S ((dst_negative_code_base_resultentryright) + (dst_negative_scale_base_resultentryright)) + ((dst_negative_scale_base_resultentryright) + (dst_negative_scale_base_resultentryright)))))) /\ (((((exists ff_h_pvs_base_resultentryrightpositive. ff_h_pvs_base_resultentryrightpositive + S (dst_positive_base_resultentryright) = S ((S (dc_quotient_base_resultentry)) * dst_positive_scale_base_resultentryright)) /\ exists ff_q_pvs_base_resultentryrightpositive. dst_positive_code_base_resultentryright = ff_q_pvs_base_resultentryrightpositive * S ((S (dc_quotient_base_resultentry)) * dst_positive_scale_base_resultentryright) + (dst_positive_base_resultentryright))) /\ (((((exists ff_h_pvs_base_resultentryrightnegative. ff_h_pvs_base_resultentryrightnegative + S (dst_negative_base_resultentryright) = S ((S (dc_quotient_base_resultentry)) * dst_negative_scale_base_resultentryright)) /\ exists ff_q_pvs_base_resultentryrightnegative. dst_negative_code_base_resultentryright = ff_q_pvs_base_resultentryrightnegative * S ((S (dc_quotient_base_resultentry)) * dst_negative_scale_base_resultentryright) + (dst_negative_base_resultentryright))) /\ (exists ge_balance_positive_base_resultentryrightvalue ge_balance_negative_base_resultentryrightvalue. (((((dc_right_base_resultentry) = 2 * (ge_balance_positive_base_resultentryrightvalue) /\ (ge_balance_negative_base_resultentryrightvalue) = 0) \/ exists ge_signed_half_base_resultentryrightvaluedecode. (((dc_right_base_resultentry) = 2 * ge_signed_half_base_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_base_resultentryrightvalue) = 0) /\ (ge_balance_negative_base_resultentryrightvalue) = S ge_signed_half_base_resultentryrightvaluedecode))) /\ ((dst_positive_base_resultentryright) + ge_balance_negative_base_resultentryrightvalue = (dst_negative_base_resultentryright) + ge_balance_positive_base_resultentryrightvalue))))))))) /\ (exists sto_ap_base_resultentryproduct sto_an_base_resultentryproduct sto_bp_base_resultentryproduct sto_bn_base_resultentryproduct sto_cp_base_resultentryproduct sto_cn_base_resultentryproduct. (((((dc_left_base_resultentry) = 2 * (sto_ap_base_resultentryproduct) /\ (sto_an_base_resultentryproduct) = 0) \/ exists ge_signed_half_base_resultentryproductleft. (((dc_left_base_resultentry) = 2 * ge_signed_half_base_resultentryproductleft + 1 /\ (sto_ap_base_resultentryproduct) = 0) /\ (sto_an_base_resultentryproduct) = S ge_signed_half_base_resultentryproductleft))) /\ ((((((dc_right_base_resultentry) = 2 * (sto_bp_base_resultentryproduct) /\ (sto_bn_base_resultentryproduct) = 0) \/ exists ge_signed_half_base_resultentryproductright. (((dc_right_base_resultentry) = 2 * ge_signed_half_base_resultentryproductright + 1 /\ (sto_bp_base_resultentryproduct) = 0) /\ (sto_bn_base_resultentryproduct) = S ge_signed_half_base_resultentryproductright))) /\ ((((((dc_value_base_result) = 2 * (sto_cp_base_resultentryproduct) /\ (sto_cn_base_resultentryproduct) = 0) \/ exists ge_signed_half_base_resultentryproductoutput. (((dc_value_base_result) = 2 * ge_signed_half_base_resultentryproductoutput + 1 /\ (sto_cp_base_resultentryproduct) = 0) /\ (sto_cn_base_resultentryproduct) = S ge_signed_half_base_resultentryproductoutput))) /\ ((sto_ap_base_resultentryproduct * sto_bp_base_resultentryproduct + sto_an_base_resultentryproduct * sto_bn_base_resultentryproduct) + sto_cn_base_resultentryproduct = (sto_ap_base_resultentryproduct * sto_bn_base_resultentryproduct + sto_an_base_resultentryproduct * sto_bp_base_resultentryproduct) + sto_cp_base_resultentryproduct))))))))))))))) \/ ((((dc_index_base_result)=0 \/ ~(exists pvs_factor_base_resultentrynondivisor. (n) = (dc_index_base_result) * pvs_factor_base_resultentrynondivisor)) /\ ((dc_value_base_result)=0)))))))