dirichlet_convolution_prefix_extensional

Exact expanded first-order arithmetic statement

forall F G n l M K. (((exists dst_positive_code_unique_firsttable dst_positive_scale_unique_firsttable dst_negative_code_unique_firsttable dst_negative_scale_unique_firsttable. (((M) = (((((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) * S ((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) + ((dst_positive_scale_unique_firsttable) + (dst_positive_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))) * S ((((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) * S ((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) + ((dst_positive_scale_unique_firsttable) + (dst_positive_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))) + ((((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))))) /\ (forall dst_index_unique_firsttable. (exists pvs_le_gap_unique_firsttabledomain. pvs_le_gap_unique_firsttabledomain + (dst_index_unique_firsttable) = (l)) -> exists dst_positive_unique_firsttable dst_negative_unique_firsttable dst_value_unique_firsttable. ((((exists ff_h_pvs_unique_firsttableentrypositive. ff_h_pvs_unique_firsttableentrypositive + S (dst_positive_unique_firsttable) = S ((S (dst_index_unique_firsttable)) * dst_positive_scale_unique_firsttable)) /\ exists ff_q_pvs_unique_firsttableentrypositive. dst_positive_code_unique_firsttable = ff_q_pvs_unique_firsttableentrypositive * S ((S (dst_index_unique_firsttable)) * dst_positive_scale_unique_firsttable) + (dst_positive_unique_firsttable))) /\ (((((exists ff_h_pvs_unique_firsttableentrynegative. ff_h_pvs_unique_firsttableentrynegative + S (dst_negative_unique_firsttable) = S ((S (dst_index_unique_firsttable)) * dst_negative_scale_unique_firsttable)) /\ exists ff_q_pvs_unique_firsttableentrynegative. dst_negative_code_unique_firsttable = ff_q_pvs_unique_firsttableentrynegative * S ((S (dst_index_unique_firsttable)) * dst_negative_scale_unique_firsttable) + (dst_negative_unique_firsttable))) /\ (exists ge_balance_positive_unique_firsttableentryvalue ge_balance_negative_unique_firsttableentryvalue. (((((dst_value_unique_firsttable) = 2 * (ge_balance_positive_unique_firsttableentryvalue) /\ (ge_balance_negative_unique_firsttableentryvalue) = 0) \/ exists ge_signed_half_unique_firsttableentryvaluedecode. (((dst_value_unique_firsttable) = 2 * ge_signed_half_unique_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_unique_firsttableentryvalue) = 0) /\ (ge_balance_negative_unique_firsttableentryvalue) = S ge_signed_half_unique_firsttableentryvaluedecode))) /\ ((dst_positive_unique_firsttable) + ge_balance_negative_unique_firsttableentryvalue = (dst_negative_unique_firsttable) + ge_balance_positive_unique_firsttableentryvalue))))))))) /\ (forall dc_index_unique_first dc_value_unique_first. (exists pvs_le_gap_unique_firstdomain. pvs_le_gap_unique_firstdomain + (dc_index_unique_first) = (l)) -> (exists dst_positive_code_unique_firstlookup dst_positive_scale_unique_firstlookup dst_negative_code_unique_firstlookup dst_negative_scale_unique_firstlookup dst_positive_unique_firstlookup dst_negative_unique_firstlookup. (((M) = (((((dst_positive_code_unique_firstlookup) + (dst_positive_scale_unique_firstlookup)) * S ((dst_positive_code_unique_firstlookup) + (dst_positive_scale_unique_firstlookup)) + ((dst_positive_scale_unique_firstlookup) + (dst_positive_scale_unique_firstlookup))) + (((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) * S ((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) + ((dst_negative_scale_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)))) * S ((((dst_positive_code_unique_firstlookup) + (dst_positive_scale_unique_firstlookup)) * S ((dst_positive_code_unique_firstlookup) + (dst_positive_scale_unique_firstlookup)) + ((dst_positive_scale_unique_firstlookup) + (dst_positive_scale_unique_firstlookup))) + (((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) * S ((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) + ((dst_negative_scale_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)))) + ((((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) * S ((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) + ((dst_negative_scale_unique_firstlookup) + (dst_negative_scale_unique_firstlookup))) + (((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) * S ((dst_negative_code_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)) + ((dst_negative_scale_unique_firstlookup) + (dst_negative_scale_unique_firstlookup)))))) /\ (((((exists ff_h_pvs_unique_firstlookuppositive. ff_h_pvs_unique_firstlookuppositive + S (dst_positive_unique_firstlookup) = S ((S (dc_index_unique_first)) * dst_positive_scale_unique_firstlookup)) /\ exists ff_q_pvs_unique_firstlookuppositive. dst_positive_code_unique_firstlookup = ff_q_pvs_unique_firstlookuppositive * S ((S (dc_index_unique_first)) * dst_positive_scale_unique_firstlookup) + (dst_positive_unique_firstlookup))) /\ (((((exists ff_h_pvs_unique_firstlookupnegative. ff_h_pvs_unique_firstlookupnegative + S (dst_negative_unique_firstlookup) = S ((S (dc_index_unique_first)) * dst_negative_scale_unique_firstlookup)) /\ exists ff_q_pvs_unique_firstlookupnegative. dst_negative_code_unique_firstlookup = ff_q_pvs_unique_firstlookupnegative * S ((S (dc_index_unique_first)) * dst_negative_scale_unique_firstlookup) + (dst_negative_unique_firstlookup))) /\ (exists ge_balance_positive_unique_firstlookupvalue ge_balance_negative_unique_firstlookupvalue. (((((dc_value_unique_first) = 2 * (ge_balance_positive_unique_firstlookupvalue) /\ (ge_balance_negative_unique_firstlookupvalue) = 0) \/ exists ge_signed_half_unique_firstlookupvaluedecode. (((dc_value_unique_first) = 2 * ge_signed_half_unique_firstlookupvaluedecode + 1 /\ (ge_balance_positive_unique_firstlookupvalue) = 0) /\ (ge_balance_negative_unique_firstlookupvalue) = S ge_signed_half_unique_firstlookupvaluedecode))) /\ ((dst_positive_unique_firstlookup) + ge_balance_negative_unique_firstlookupvalue = (dst_negative_unique_firstlookup) + ge_balance_positive_unique_firstlookupvalue))))))))) -> ((((~((dc_index_unique_first)=0)) /\ (exists dc_quotient_unique_firstentry dc_left_unique_firstentry dc_right_unique_firstentry. (((n)=(dc_index_unique_first)*dc_quotient_unique_firstentry) /\ (((exists dst_positive_code_unique_firstentryleft dst_positive_scale_unique_firstentryleft dst_negative_code_unique_firstentryleft dst_negative_scale_unique_firstentryleft dst_positive_unique_firstentryleft dst_negative_unique_firstentryleft. (((F) = (((((dst_positive_code_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft)) * S ((dst_positive_code_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft)) + ((dst_positive_scale_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft))) + (((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) * S ((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) + ((dst_negative_scale_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)))) * S ((((dst_positive_code_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft)) * S ((dst_positive_code_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft)) + ((dst_positive_scale_unique_firstentryleft) + (dst_positive_scale_unique_firstentryleft))) + (((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) * S ((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) + ((dst_negative_scale_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)))) + ((((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) * S ((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) + ((dst_negative_scale_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft))) + (((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) * S ((dst_negative_code_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)) + ((dst_negative_scale_unique_firstentryleft) + (dst_negative_scale_unique_firstentryleft)))))) /\ (((((exists ff_h_pvs_unique_firstentryleftpositive. ff_h_pvs_unique_firstentryleftpositive + S (dst_positive_unique_firstentryleft) = S ((S (dc_index_unique_first)) * dst_positive_scale_unique_firstentryleft)) /\ exists ff_q_pvs_unique_firstentryleftpositive. dst_positive_code_unique_firstentryleft = ff_q_pvs_unique_firstentryleftpositive * S ((S (dc_index_unique_first)) * dst_positive_scale_unique_firstentryleft) + (dst_positive_unique_firstentryleft))) /\ (((((exists ff_h_pvs_unique_firstentryleftnegative. ff_h_pvs_unique_firstentryleftnegative + S (dst_negative_unique_firstentryleft) = S ((S (dc_index_unique_first)) * dst_negative_scale_unique_firstentryleft)) /\ exists ff_q_pvs_unique_firstentryleftnegative. dst_negative_code_unique_firstentryleft = ff_q_pvs_unique_firstentryleftnegative * S ((S (dc_index_unique_first)) * dst_negative_scale_unique_firstentryleft) + (dst_negative_unique_firstentryleft))) /\ (exists ge_balance_positive_unique_firstentryleftvalue ge_balance_negative_unique_firstentryleftvalue. (((((dc_left_unique_firstentry) = 2 * (ge_balance_positive_unique_firstentryleftvalue) /\ (ge_balance_negative_unique_firstentryleftvalue) = 0) \/ exists ge_signed_half_unique_firstentryleftvaluedecode. (((dc_left_unique_firstentry) = 2 * ge_signed_half_unique_firstentryleftvaluedecode + 1 /\ (ge_balance_positive_unique_firstentryleftvalue) = 0) /\ (ge_balance_negative_unique_firstentryleftvalue) = S ge_signed_half_unique_firstentryleftvaluedecode))) /\ ((dst_positive_unique_firstentryleft) + ge_balance_negative_unique_firstentryleftvalue = (dst_negative_unique_firstentryleft) + ge_balance_positive_unique_firstentryleftvalue))))))))) /\ (((exists dst_positive_code_unique_firstentryright dst_positive_scale_unique_firstentryright dst_negative_code_unique_firstentryright dst_negative_scale_unique_firstentryright dst_positive_unique_firstentryright dst_negative_unique_firstentryright. (((G) = (((((dst_positive_code_unique_firstentryright) + (dst_positive_scale_unique_firstentryright)) * S ((dst_positive_code_unique_firstentryright) + (dst_positive_scale_unique_firstentryright)) + ((dst_positive_scale_unique_firstentryright) + (dst_positive_scale_unique_firstentryright))) + (((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) * S ((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) + ((dst_negative_scale_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)))) * S ((((dst_positive_code_unique_firstentryright) + (dst_positive_scale_unique_firstentryright)) * S ((dst_positive_code_unique_firstentryright) + (dst_positive_scale_unique_firstentryright)) + ((dst_positive_scale_unique_firstentryright) + (dst_positive_scale_unique_firstentryright))) + (((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) * S ((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) + ((dst_negative_scale_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)))) + ((((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) * S ((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) + ((dst_negative_scale_unique_firstentryright) + (dst_negative_scale_unique_firstentryright))) + (((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) * S ((dst_negative_code_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)) + ((dst_negative_scale_unique_firstentryright) + (dst_negative_scale_unique_firstentryright)))))) /\ (((((exists ff_h_pvs_unique_firstentryrightpositive. ff_h_pvs_unique_firstentryrightpositive + S (dst_positive_unique_firstentryright) = S ((S (dc_quotient_unique_firstentry)) * dst_positive_scale_unique_firstentryright)) /\ exists ff_q_pvs_unique_firstentryrightpositive. dst_positive_code_unique_firstentryright = ff_q_pvs_unique_firstentryrightpositive * S ((S (dc_quotient_unique_firstentry)) * dst_positive_scale_unique_firstentryright) + (dst_positive_unique_firstentryright))) /\ (((((exists ff_h_pvs_unique_firstentryrightnegative. ff_h_pvs_unique_firstentryrightnegative + S (dst_negative_unique_firstentryright) = S ((S (dc_quotient_unique_firstentry)) * dst_negative_scale_unique_firstentryright)) /\ exists ff_q_pvs_unique_firstentryrightnegative. dst_negative_code_unique_firstentryright = ff_q_pvs_unique_firstentryrightnegative * S ((S (dc_quotient_unique_firstentry)) * dst_negative_scale_unique_firstentryright) + (dst_negative_unique_firstentryright))) /\ (exists ge_balance_positive_unique_firstentryrightvalue ge_balance_negative_unique_firstentryrightvalue. (((((dc_right_unique_firstentry) = 2 * (ge_balance_positive_unique_firstentryrightvalue) /\ (ge_balance_negative_unique_firstentryrightvalue) = 0) \/ exists ge_signed_half_unique_firstentryrightvaluedecode. (((dc_right_unique_firstentry) = 2 * ge_signed_half_unique_firstentryrightvaluedecode + 1 /\ (ge_balance_positive_unique_firstentryrightvalue) = 0) /\ (ge_balance_negative_unique_firstentryrightvalue) = S ge_signed_half_unique_firstentryrightvaluedecode))) /\ ((dst_positive_unique_firstentryright) + ge_balance_negative_unique_firstentryrightvalue = (dst_negative_unique_firstentryright) + ge_balance_positive_unique_firstentryrightvalue))))))))) /\ (exists sto_ap_unique_firstentryproduct sto_an_unique_firstentryproduct sto_bp_unique_firstentryproduct sto_bn_unique_firstentryproduct sto_cp_unique_firstentryproduct sto_cn_unique_firstentryproduct. (((((dc_left_unique_firstentry) = 2 * (sto_ap_unique_firstentryproduct) /\ (sto_an_unique_firstentryproduct) = 0) \/ exists ge_signed_half_unique_firstentryproductleft. (((dc_left_unique_firstentry) = 2 * ge_signed_half_unique_firstentryproductleft + 1 /\ (sto_ap_unique_firstentryproduct) = 0) /\ (sto_an_unique_firstentryproduct) = S ge_signed_half_unique_firstentryproductleft))) /\ ((((((dc_right_unique_firstentry) = 2 * (sto_bp_unique_firstentryproduct) /\ (sto_bn_unique_firstentryproduct) = 0) \/ exists ge_signed_half_unique_firstentryproductright. (((dc_right_unique_firstentry) = 2 * ge_signed_half_unique_firstentryproductright + 1 /\ (sto_bp_unique_firstentryproduct) = 0) /\ (sto_bn_unique_firstentryproduct) = S ge_signed_half_unique_firstentryproductright))) /\ ((((((dc_value_unique_first) = 2 * (sto_cp_unique_firstentryproduct) /\ (sto_cn_unique_firstentryproduct) = 0) \/ exists ge_signed_half_unique_firstentryproductoutput. (((dc_value_unique_first) = 2 * ge_signed_half_unique_firstentryproductoutput + 1 /\ (sto_cp_unique_firstentryproduct) = 0) /\ (sto_cn_unique_firstentryproduct) = S ge_signed_half_unique_firstentryproductoutput))) /\ ((sto_ap_unique_firstentryproduct * sto_bp_unique_firstentryproduct + sto_an_unique_firstentryproduct * sto_bn_unique_firstentryproduct) + sto_cn_unique_firstentryproduct = (sto_ap_unique_firstentryproduct * sto_bn_unique_firstentryproduct + sto_an_unique_firstentryproduct * sto_bp_unique_firstentryproduct) + sto_cp_unique_firstentryproduct))))))))))))))) \/ ((((dc_index_unique_first)=0 \/ ~(exists pvs_factor_unique_firstentrynondivisor. (n) = (dc_index_unique_first) * pvs_factor_unique_firstentrynondivisor)) /\ ((dc_value_unique_first)=0))))))) -> (((exists dst_positive_code_unique_secondtable dst_positive_scale_unique_secondtable dst_negative_code_unique_secondtable dst_negative_scale_unique_secondtable. (((K) = (((((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) * S ((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) + ((dst_positive_scale_unique_secondtable) + (dst_positive_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))) * S ((((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) * S ((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) + ((dst_positive_scale_unique_secondtable) + (dst_positive_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))) + ((((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))))) /\ (forall dst_index_unique_secondtable. (exists pvs_le_gap_unique_secondtabledomain. pvs_le_gap_unique_secondtabledomain + (dst_index_unique_secondtable) = (l)) -> exists dst_positive_unique_secondtable dst_negative_unique_secondtable dst_value_unique_secondtable. ((((exists ff_h_pvs_unique_secondtableentrypositive. ff_h_pvs_unique_secondtableentrypositive + S (dst_positive_unique_secondtable) = S ((S (dst_index_unique_secondtable)) * dst_positive_scale_unique_secondtable)) /\ exists ff_q_pvs_unique_secondtableentrypositive. dst_positive_code_unique_secondtable = ff_q_pvs_unique_secondtableentrypositive * S ((S (dst_index_unique_secondtable)) * dst_positive_scale_unique_secondtable) + (dst_positive_unique_secondtable))) /\ (((((exists ff_h_pvs_unique_secondtableentrynegative. ff_h_pvs_unique_secondtableentrynegative + S (dst_negative_unique_secondtable) = S ((S (dst_index_unique_secondtable)) * dst_negative_scale_unique_secondtable)) /\ exists ff_q_pvs_unique_secondtableentrynegative. dst_negative_code_unique_secondtable = ff_q_pvs_unique_secondtableentrynegative * S ((S (dst_index_unique_secondtable)) * dst_negative_scale_unique_secondtable) + (dst_negative_unique_secondtable))) /\ (exists ge_balance_positive_unique_secondtableentryvalue ge_balance_negative_unique_secondtableentryvalue. (((((dst_value_unique_secondtable) = 2 * (ge_balance_positive_unique_secondtableentryvalue) /\ (ge_balance_negative_unique_secondtableentryvalue) = 0) \/ exists ge_signed_half_unique_secondtableentryvaluedecode. (((dst_value_unique_secondtable) = 2 * ge_signed_half_unique_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondtableentryvalue) = 0) /\ (ge_balance_negative_unique_secondtableentryvalue) = S ge_signed_half_unique_secondtableentryvaluedecode))) /\ ((dst_positive_unique_secondtable) + ge_balance_negative_unique_secondtableentryvalue = (dst_negative_unique_secondtable) + ge_balance_positive_unique_secondtableentryvalue))))))))) /\ (forall dc_index_unique_second dc_value_unique_second. (exists pvs_le_gap_unique_seconddomain. pvs_le_gap_unique_seconddomain + (dc_index_unique_second) = (l)) -> (exists dst_positive_code_unique_secondlookup dst_positive_scale_unique_secondlookup dst_negative_code_unique_secondlookup dst_negative_scale_unique_secondlookup dst_positive_unique_secondlookup dst_negative_unique_secondlookup. (((K) = (((((dst_positive_code_unique_secondlookup) + (dst_positive_scale_unique_secondlookup)) * S ((dst_positive_code_unique_secondlookup) + (dst_positive_scale_unique_secondlookup)) + ((dst_positive_scale_unique_secondlookup) + (dst_positive_scale_unique_secondlookup))) + (((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) * S ((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) + ((dst_negative_scale_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)))) * S ((((dst_positive_code_unique_secondlookup) + (dst_positive_scale_unique_secondlookup)) * S ((dst_positive_code_unique_secondlookup) + (dst_positive_scale_unique_secondlookup)) + ((dst_positive_scale_unique_secondlookup) + (dst_positive_scale_unique_secondlookup))) + (((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) * S ((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) + ((dst_negative_scale_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)))) + ((((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) * S ((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) + ((dst_negative_scale_unique_secondlookup) + (dst_negative_scale_unique_secondlookup))) + (((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) * S ((dst_negative_code_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)) + ((dst_negative_scale_unique_secondlookup) + (dst_negative_scale_unique_secondlookup)))))) /\ (((((exists ff_h_pvs_unique_secondlookuppositive. ff_h_pvs_unique_secondlookuppositive + S (dst_positive_unique_secondlookup) = S ((S (dc_index_unique_second)) * dst_positive_scale_unique_secondlookup)) /\ exists ff_q_pvs_unique_secondlookuppositive. dst_positive_code_unique_secondlookup = ff_q_pvs_unique_secondlookuppositive * S ((S (dc_index_unique_second)) * dst_positive_scale_unique_secondlookup) + (dst_positive_unique_secondlookup))) /\ (((((exists ff_h_pvs_unique_secondlookupnegative. ff_h_pvs_unique_secondlookupnegative + S (dst_negative_unique_secondlookup) = S ((S (dc_index_unique_second)) * dst_negative_scale_unique_secondlookup)) /\ exists ff_q_pvs_unique_secondlookupnegative. dst_negative_code_unique_secondlookup = ff_q_pvs_unique_secondlookupnegative * S ((S (dc_index_unique_second)) * dst_negative_scale_unique_secondlookup) + (dst_negative_unique_secondlookup))) /\ (exists ge_balance_positive_unique_secondlookupvalue ge_balance_negative_unique_secondlookupvalue. (((((dc_value_unique_second) = 2 * (ge_balance_positive_unique_secondlookupvalue) /\ (ge_balance_negative_unique_secondlookupvalue) = 0) \/ exists ge_signed_half_unique_secondlookupvaluedecode. (((dc_value_unique_second) = 2 * ge_signed_half_unique_secondlookupvaluedecode + 1 /\ (ge_balance_positive_unique_secondlookupvalue) = 0) /\ (ge_balance_negative_unique_secondlookupvalue) = S ge_signed_half_unique_secondlookupvaluedecode))) /\ ((dst_positive_unique_secondlookup) + ge_balance_negative_unique_secondlookupvalue = (dst_negative_unique_secondlookup) + ge_balance_positive_unique_secondlookupvalue))))))))) -> ((((~((dc_index_unique_second)=0)) /\ (exists dc_quotient_unique_secondentry dc_left_unique_secondentry dc_right_unique_secondentry. (((n)=(dc_index_unique_second)*dc_quotient_unique_secondentry) /\ (((exists dst_positive_code_unique_secondentryleft dst_positive_scale_unique_secondentryleft dst_negative_code_unique_secondentryleft dst_negative_scale_unique_secondentryleft dst_positive_unique_secondentryleft dst_negative_unique_secondentryleft. (((F) = (((((dst_positive_code_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft)) * S ((dst_positive_code_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft)) + ((dst_positive_scale_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft))) + (((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) * S ((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) + ((dst_negative_scale_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)))) * S ((((dst_positive_code_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft)) * S ((dst_positive_code_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft)) + ((dst_positive_scale_unique_secondentryleft) + (dst_positive_scale_unique_secondentryleft))) + (((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) * S ((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) + ((dst_negative_scale_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)))) + ((((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) * S ((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) + ((dst_negative_scale_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft))) + (((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) * S ((dst_negative_code_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)) + ((dst_negative_scale_unique_secondentryleft) + (dst_negative_scale_unique_secondentryleft)))))) /\ (((((exists ff_h_pvs_unique_secondentryleftpositive. ff_h_pvs_unique_secondentryleftpositive + S (dst_positive_unique_secondentryleft) = S ((S (dc_index_unique_second)) * dst_positive_scale_unique_secondentryleft)) /\ exists ff_q_pvs_unique_secondentryleftpositive. dst_positive_code_unique_secondentryleft = ff_q_pvs_unique_secondentryleftpositive * S ((S (dc_index_unique_second)) * dst_positive_scale_unique_secondentryleft) + (dst_positive_unique_secondentryleft))) /\ (((((exists ff_h_pvs_unique_secondentryleftnegative. ff_h_pvs_unique_secondentryleftnegative + S (dst_negative_unique_secondentryleft) = S ((S (dc_index_unique_second)) * dst_negative_scale_unique_secondentryleft)) /\ exists ff_q_pvs_unique_secondentryleftnegative. dst_negative_code_unique_secondentryleft = ff_q_pvs_unique_secondentryleftnegative * S ((S (dc_index_unique_second)) * dst_negative_scale_unique_secondentryleft) + (dst_negative_unique_secondentryleft))) /\ (exists ge_balance_positive_unique_secondentryleftvalue ge_balance_negative_unique_secondentryleftvalue. (((((dc_left_unique_secondentry) = 2 * (ge_balance_positive_unique_secondentryleftvalue) /\ (ge_balance_negative_unique_secondentryleftvalue) = 0) \/ exists ge_signed_half_unique_secondentryleftvaluedecode. (((dc_left_unique_secondentry) = 2 * ge_signed_half_unique_secondentryleftvaluedecode + 1 /\ (ge_balance_positive_unique_secondentryleftvalue) = 0) /\ (ge_balance_negative_unique_secondentryleftvalue) = S ge_signed_half_unique_secondentryleftvaluedecode))) /\ ((dst_positive_unique_secondentryleft) + ge_balance_negative_unique_secondentryleftvalue = (dst_negative_unique_secondentryleft) + ge_balance_positive_unique_secondentryleftvalue))))))))) /\ (((exists dst_positive_code_unique_secondentryright dst_positive_scale_unique_secondentryright dst_negative_code_unique_secondentryright dst_negative_scale_unique_secondentryright dst_positive_unique_secondentryright dst_negative_unique_secondentryright. (((G) = (((((dst_positive_code_unique_secondentryright) + (dst_positive_scale_unique_secondentryright)) * S ((dst_positive_code_unique_secondentryright) + (dst_positive_scale_unique_secondentryright)) + ((dst_positive_scale_unique_secondentryright) + (dst_positive_scale_unique_secondentryright))) + (((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) * S ((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) + ((dst_negative_scale_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)))) * S ((((dst_positive_code_unique_secondentryright) + (dst_positive_scale_unique_secondentryright)) * S ((dst_positive_code_unique_secondentryright) + (dst_positive_scale_unique_secondentryright)) + ((dst_positive_scale_unique_secondentryright) + (dst_positive_scale_unique_secondentryright))) + (((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) * S ((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) + ((dst_negative_scale_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)))) + ((((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) * S ((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) + ((dst_negative_scale_unique_secondentryright) + (dst_negative_scale_unique_secondentryright))) + (((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) * S ((dst_negative_code_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)) + ((dst_negative_scale_unique_secondentryright) + (dst_negative_scale_unique_secondentryright)))))) /\ (((((exists ff_h_pvs_unique_secondentryrightpositive. ff_h_pvs_unique_secondentryrightpositive + S (dst_positive_unique_secondentryright) = S ((S (dc_quotient_unique_secondentry)) * dst_positive_scale_unique_secondentryright)) /\ exists ff_q_pvs_unique_secondentryrightpositive. dst_positive_code_unique_secondentryright = ff_q_pvs_unique_secondentryrightpositive * S ((S (dc_quotient_unique_secondentry)) * dst_positive_scale_unique_secondentryright) + (dst_positive_unique_secondentryright))) /\ (((((exists ff_h_pvs_unique_secondentryrightnegative. ff_h_pvs_unique_secondentryrightnegative + S (dst_negative_unique_secondentryright) = S ((S (dc_quotient_unique_secondentry)) * dst_negative_scale_unique_secondentryright)) /\ exists ff_q_pvs_unique_secondentryrightnegative. dst_negative_code_unique_secondentryright = ff_q_pvs_unique_secondentryrightnegative * S ((S (dc_quotient_unique_secondentry)) * dst_negative_scale_unique_secondentryright) + (dst_negative_unique_secondentryright))) /\ (exists ge_balance_positive_unique_secondentryrightvalue ge_balance_negative_unique_secondentryrightvalue. (((((dc_right_unique_secondentry) = 2 * (ge_balance_positive_unique_secondentryrightvalue) /\ (ge_balance_negative_unique_secondentryrightvalue) = 0) \/ exists ge_signed_half_unique_secondentryrightvaluedecode. (((dc_right_unique_secondentry) = 2 * ge_signed_half_unique_secondentryrightvaluedecode + 1 /\ (ge_balance_positive_unique_secondentryrightvalue) = 0) /\ (ge_balance_negative_unique_secondentryrightvalue) = S ge_signed_half_unique_secondentryrightvaluedecode))) /\ ((dst_positive_unique_secondentryright) + ge_balance_negative_unique_secondentryrightvalue = (dst_negative_unique_secondentryright) + ge_balance_positive_unique_secondentryrightvalue))))))))) /\ (exists sto_ap_unique_secondentryproduct sto_an_unique_secondentryproduct sto_bp_unique_secondentryproduct sto_bn_unique_secondentryproduct sto_cp_unique_secondentryproduct sto_cn_unique_secondentryproduct. (((((dc_left_unique_secondentry) = 2 * (sto_ap_unique_secondentryproduct) /\ (sto_an_unique_secondentryproduct) = 0) \/ exists ge_signed_half_unique_secondentryproductleft. (((dc_left_unique_secondentry) = 2 * ge_signed_half_unique_secondentryproductleft + 1 /\ (sto_ap_unique_secondentryproduct) = 0) /\ (sto_an_unique_secondentryproduct) = S ge_signed_half_unique_secondentryproductleft))) /\ ((((((dc_right_unique_secondentry) = 2 * (sto_bp_unique_secondentryproduct) /\ (sto_bn_unique_secondentryproduct) = 0) \/ exists ge_signed_half_unique_secondentryproductright. (((dc_right_unique_secondentry) = 2 * ge_signed_half_unique_secondentryproductright + 1 /\ (sto_bp_unique_secondentryproduct) = 0) /\ (sto_bn_unique_secondentryproduct) = S ge_signed_half_unique_secondentryproductright))) /\ ((((((dc_value_unique_second) = 2 * (sto_cp_unique_secondentryproduct) /\ (sto_cn_unique_secondentryproduct) = 0) \/ exists ge_signed_half_unique_secondentryproductoutput. (((dc_value_unique_second) = 2 * ge_signed_half_unique_secondentryproductoutput + 1 /\ (sto_cp_unique_secondentryproduct) = 0) /\ (sto_cn_unique_secondentryproduct) = S ge_signed_half_unique_secondentryproductoutput))) /\ ((sto_ap_unique_secondentryproduct * sto_bp_unique_secondentryproduct + sto_an_unique_secondentryproduct * sto_bn_unique_secondentryproduct) + sto_cn_unique_secondentryproduct = (sto_ap_unique_secondentryproduct * sto_bn_unique_secondentryproduct + sto_an_unique_secondentryproduct * sto_bp_unique_secondentryproduct) + sto_cp_unique_secondentryproduct))))))))))))))) \/ ((((dc_index_unique_second)=0 \/ ~(exists pvs_factor_unique_secondentrynondivisor. (n) = (dc_index_unique_second) * pvs_factor_unique_secondentrynondivisor)) /\ ((dc_value_unique_second)=0))))))) -> (forall dst_index_unique_values dst_first_unique_values dst_second_unique_values. (exists pvs_gap_unique_valuesbound. pvs_gap_unique_valuesbound + S (dst_index_unique_values) = (S l)) -> (exists dst_positive_code_unique_valuesfirst dst_positive_scale_unique_valuesfirst dst_negative_code_unique_valuesfirst dst_negative_scale_unique_valuesfirst dst_positive_unique_valuesfirst dst_negative_unique_valuesfirst. (((M) = (((((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) * S ((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) + ((dst_positive_scale_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))) * S ((((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) * S ((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) + ((dst_positive_scale_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))) + ((((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))))) /\ (((((exists ff_h_pvs_unique_valuesfirstpositive. ff_h_pvs_unique_valuesfirstpositive + S (dst_positive_unique_valuesfirst) = S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuesfirst)) /\ exists ff_q_pvs_unique_valuesfirstpositive. dst_positive_code_unique_valuesfirst = ff_q_pvs_unique_valuesfirstpositive * S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuesfirst) + (dst_positive_unique_valuesfirst))) /\ (((((exists ff_h_pvs_unique_valuesfirstnegative. ff_h_pvs_unique_valuesfirstnegative + S (dst_negative_unique_valuesfirst) = S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuesfirst)) /\ exists ff_q_pvs_unique_valuesfirstnegative. dst_negative_code_unique_valuesfirst = ff_q_pvs_unique_valuesfirstnegative * S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuesfirst) + (dst_negative_unique_valuesfirst))) /\ (exists ge_balance_positive_unique_valuesfirstvalue ge_balance_negative_unique_valuesfirstvalue. (((((dst_first_unique_values) = 2 * (ge_balance_positive_unique_valuesfirstvalue) /\ (ge_balance_negative_unique_valuesfirstvalue) = 0) \/ exists ge_signed_half_unique_valuesfirstvaluedecode. (((dst_first_unique_values) = 2 * ge_signed_half_unique_valuesfirstvaluedecode + 1 /\ (ge_balance_positive_unique_valuesfirstvalue) = 0) /\ (ge_balance_negative_unique_valuesfirstvalue) = S ge_signed_half_unique_valuesfirstvaluedecode))) /\ ((dst_positive_unique_valuesfirst) + ge_balance_negative_unique_valuesfirstvalue = (dst_negative_unique_valuesfirst) + ge_balance_positive_unique_valuesfirstvalue))))))))) -> (exists dst_positive_code_unique_valuessecond dst_positive_scale_unique_valuessecond dst_negative_code_unique_valuessecond dst_negative_scale_unique_valuessecond dst_positive_unique_valuessecond dst_negative_unique_valuessecond. (((K) = (((((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) * S ((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) + ((dst_positive_scale_unique_valuessecond) + (dst_positive_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))) * S ((((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) * S ((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) + ((dst_positive_scale_unique_valuessecond) + (dst_positive_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))) + ((((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))))) /\ (((((exists ff_h_pvs_unique_valuessecondpositive. ff_h_pvs_unique_valuessecondpositive + S (dst_positive_unique_valuessecond) = S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuessecond)) /\ exists ff_q_pvs_unique_valuessecondpositive. dst_positive_code_unique_valuessecond = ff_q_pvs_unique_valuessecondpositive * S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuessecond) + (dst_positive_unique_valuessecond))) /\ (((((exists ff_h_pvs_unique_valuessecondnegative. ff_h_pvs_unique_valuessecondnegative + S (dst_negative_unique_valuessecond) = S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuessecond)) /\ exists ff_q_pvs_unique_valuessecondnegative. dst_negative_code_unique_valuessecond = ff_q_pvs_unique_valuessecondnegative * S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuessecond) + (dst_negative_unique_valuessecond))) /\ (exists ge_balance_positive_unique_valuessecondvalue ge_balance_negative_unique_valuessecondvalue. (((((dst_second_unique_values) = 2 * (ge_balance_positive_unique_valuessecondvalue) /\ (ge_balance_negative_unique_valuessecondvalue) = 0) \/ exists ge_signed_half_unique_valuessecondvaluedecode. (((dst_second_unique_values) = 2 * ge_signed_half_unique_valuessecondvaluedecode + 1 /\ (ge_balance_positive_unique_valuessecondvalue) = 0) /\ (ge_balance_negative_unique_valuessecondvalue) = S ge_signed_half_unique_valuessecondvaluedecode))) /\ ((dst_positive_unique_valuessecond) + ge_balance_negative_unique_valuessecondvalue = (dst_negative_unique_valuessecond) + ge_balance_positive_unique_valuessecondvalue))))))))) -> dst_first_unique_values = dst_second_unique_values)