dirichlet_convolution_prefix_complement_reindex

Exact expanded first-order arithmetic statement

forall F G n P Q r s. ~(n=0) -> (((exists dst_positive_code_pullback_firsttable dst_positive_scale_pullback_firsttable dst_negative_code_pullback_firsttable dst_negative_scale_pullback_firsttable. (((P) = (((((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) * S ((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) + ((dst_positive_scale_pullback_firsttable) + (dst_positive_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))) * S ((((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) * S ((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) + ((dst_positive_scale_pullback_firsttable) + (dst_positive_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))) + ((((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))))) /\ (forall dst_index_pullback_firsttable. (exists pvs_le_gap_pullback_firsttabledomain. pvs_le_gap_pullback_firsttabledomain + (dst_index_pullback_firsttable) = (n)) -> exists dst_positive_pullback_firsttable dst_negative_pullback_firsttable dst_value_pullback_firsttable. ((((exists ff_h_pvs_pullback_firsttableentrypositive. ff_h_pvs_pullback_firsttableentrypositive + S (dst_positive_pullback_firsttable) = S ((S (dst_index_pullback_firsttable)) * dst_positive_scale_pullback_firsttable)) /\ exists ff_q_pvs_pullback_firsttableentrypositive. dst_positive_code_pullback_firsttable = ff_q_pvs_pullback_firsttableentrypositive * S ((S (dst_index_pullback_firsttable)) * dst_positive_scale_pullback_firsttable) + (dst_positive_pullback_firsttable))) /\ (((((exists ff_h_pvs_pullback_firsttableentrynegative. ff_h_pvs_pullback_firsttableentrynegative + S (dst_negative_pullback_firsttable) = S ((S (dst_index_pullback_firsttable)) * dst_negative_scale_pullback_firsttable)) /\ exists ff_q_pvs_pullback_firsttableentrynegative. dst_negative_code_pullback_firsttable = ff_q_pvs_pullback_firsttableentrynegative * S ((S (dst_index_pullback_firsttable)) * dst_negative_scale_pullback_firsttable) + (dst_negative_pullback_firsttable))) /\ (exists ge_balance_positive_pullback_firsttableentryvalue ge_balance_negative_pullback_firsttableentryvalue. (((((dst_value_pullback_firsttable) = 2 * (ge_balance_positive_pullback_firsttableentryvalue) /\ (ge_balance_negative_pullback_firsttableentryvalue) = 0) \/ exists ge_signed_half_pullback_firsttableentryvaluedecode. (((dst_value_pullback_firsttable) = 2 * ge_signed_half_pullback_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_pullback_firsttableentryvalue) = 0) /\ (ge_balance_negative_pullback_firsttableentryvalue) = S ge_signed_half_pullback_firsttableentryvaluedecode))) /\ ((dst_positive_pullback_firsttable) + ge_balance_negative_pullback_firsttableentryvalue = (dst_negative_pullback_firsttable) + ge_balance_positive_pullback_firsttableentryvalue))))))))) /\ (forall dc_index_pullback_first dc_value_pullback_first. (exists pvs_le_gap_pullback_firstdomain. pvs_le_gap_pullback_firstdomain + (dc_index_pullback_first) = (n)) -> (exists dst_positive_code_pullback_firstlookup dst_positive_scale_pullback_firstlookup dst_negative_code_pullback_firstlookup dst_negative_scale_pullback_firstlookup dst_positive_pullback_firstlookup dst_negative_pullback_firstlookup. (((P) = (((((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) * S ((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) + ((dst_positive_scale_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))) * S ((((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) * S ((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) + ((dst_positive_scale_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))) + ((((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))))) /\ (((((exists ff_h_pvs_pullback_firstlookuppositive. ff_h_pvs_pullback_firstlookuppositive + S (dst_positive_pullback_firstlookup) = S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstlookup)) /\ exists ff_q_pvs_pullback_firstlookuppositive. dst_positive_code_pullback_firstlookup = ff_q_pvs_pullback_firstlookuppositive * S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstlookup) + (dst_positive_pullback_firstlookup))) /\ (((((exists ff_h_pvs_pullback_firstlookupnegative. ff_h_pvs_pullback_firstlookupnegative + S (dst_negative_pullback_firstlookup) = S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstlookup)) /\ exists ff_q_pvs_pullback_firstlookupnegative. dst_negative_code_pullback_firstlookup = ff_q_pvs_pullback_firstlookupnegative * S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstlookup) + (dst_negative_pullback_firstlookup))) /\ (exists ge_balance_positive_pullback_firstlookupvalue ge_balance_negative_pullback_firstlookupvalue. (((((dc_value_pullback_first) = 2 * (ge_balance_positive_pullback_firstlookupvalue) /\ (ge_balance_negative_pullback_firstlookupvalue) = 0) \/ exists ge_signed_half_pullback_firstlookupvaluedecode. (((dc_value_pullback_first) = 2 * ge_signed_half_pullback_firstlookupvaluedecode + 1 /\ (ge_balance_positive_pullback_firstlookupvalue) = 0) /\ (ge_balance_negative_pullback_firstlookupvalue) = S ge_signed_half_pullback_firstlookupvaluedecode))) /\ ((dst_positive_pullback_firstlookup) + ge_balance_negative_pullback_firstlookupvalue = (dst_negative_pullback_firstlookup) + ge_balance_positive_pullback_firstlookupvalue))))))))) -> ((((~((dc_index_pullback_first)=0)) /\ (exists dc_quotient_pullback_firstentry dc_left_pullback_firstentry dc_right_pullback_firstentry. (((n)=(dc_index_pullback_first)*dc_quotient_pullback_firstentry) /\ (((exists dst_positive_code_pullback_firstentryleft dst_positive_scale_pullback_firstentryleft dst_negative_code_pullback_firstentryleft dst_negative_scale_pullback_firstentryleft dst_positive_pullback_firstentryleft dst_negative_pullback_firstentryleft. (((F) = (((((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) * S ((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) + ((dst_positive_scale_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))) * S ((((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) * S ((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) + ((dst_positive_scale_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))) + ((((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))))) /\ (((((exists ff_h_pvs_pullback_firstentryleftpositive. ff_h_pvs_pullback_firstentryleftpositive + S (dst_positive_pullback_firstentryleft) = S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstentryleft)) /\ exists ff_q_pvs_pullback_firstentryleftpositive. dst_positive_code_pullback_firstentryleft = ff_q_pvs_pullback_firstentryleftpositive * S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstentryleft) + (dst_positive_pullback_firstentryleft))) /\ (((((exists ff_h_pvs_pullback_firstentryleftnegative. ff_h_pvs_pullback_firstentryleftnegative + S (dst_negative_pullback_firstentryleft) = S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstentryleft)) /\ exists ff_q_pvs_pullback_firstentryleftnegative. dst_negative_code_pullback_firstentryleft = ff_q_pvs_pullback_firstentryleftnegative * S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstentryleft) + (dst_negative_pullback_firstentryleft))) /\ (exists ge_balance_positive_pullback_firstentryleftvalue ge_balance_negative_pullback_firstentryleftvalue. (((((dc_left_pullback_firstentry) = 2 * (ge_balance_positive_pullback_firstentryleftvalue) /\ (ge_balance_negative_pullback_firstentryleftvalue) = 0) \/ exists ge_signed_half_pullback_firstentryleftvaluedecode. (((dc_left_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryleftvaluedecode + 1 /\ (ge_balance_positive_pullback_firstentryleftvalue) = 0) /\ (ge_balance_negative_pullback_firstentryleftvalue) = S ge_signed_half_pullback_firstentryleftvaluedecode))) /\ ((dst_positive_pullback_firstentryleft) + ge_balance_negative_pullback_firstentryleftvalue = (dst_negative_pullback_firstentryleft) + ge_balance_positive_pullback_firstentryleftvalue))))))))) /\ (((exists dst_positive_code_pullback_firstentryright dst_positive_scale_pullback_firstentryright dst_negative_code_pullback_firstentryright dst_negative_scale_pullback_firstentryright dst_positive_pullback_firstentryright dst_negative_pullback_firstentryright. (((G) = (((((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) * S ((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) + ((dst_positive_scale_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))) * S ((((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) * S ((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) + ((dst_positive_scale_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))) + ((((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))))) /\ (((((exists ff_h_pvs_pullback_firstentryrightpositive. ff_h_pvs_pullback_firstentryrightpositive + S (dst_positive_pullback_firstentryright) = S ((S (dc_quotient_pullback_firstentry)) * dst_positive_scale_pullback_firstentryright)) /\ exists ff_q_pvs_pullback_firstentryrightpositive. dst_positive_code_pullback_firstentryright = ff_q_pvs_pullback_firstentryrightpositive * S ((S (dc_quotient_pullback_firstentry)) * dst_positive_scale_pullback_firstentryright) + (dst_positive_pullback_firstentryright))) /\ (((((exists ff_h_pvs_pullback_firstentryrightnegative. ff_h_pvs_pullback_firstentryrightnegative + S (dst_negative_pullback_firstentryright) = S ((S (dc_quotient_pullback_firstentry)) * dst_negative_scale_pullback_firstentryright)) /\ exists ff_q_pvs_pullback_firstentryrightnegative. dst_negative_code_pullback_firstentryright = ff_q_pvs_pullback_firstentryrightnegative * S ((S (dc_quotient_pullback_firstentry)) * dst_negative_scale_pullback_firstentryright) + (dst_negative_pullback_firstentryright))) /\ (exists ge_balance_positive_pullback_firstentryrightvalue ge_balance_negative_pullback_firstentryrightvalue. (((((dc_right_pullback_firstentry) = 2 * (ge_balance_positive_pullback_firstentryrightvalue) /\ (ge_balance_negative_pullback_firstentryrightvalue) = 0) \/ exists ge_signed_half_pullback_firstentryrightvaluedecode. (((dc_right_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryrightvaluedecode + 1 /\ (ge_balance_positive_pullback_firstentryrightvalue) = 0) /\ (ge_balance_negative_pullback_firstentryrightvalue) = S ge_signed_half_pullback_firstentryrightvaluedecode))) /\ ((dst_positive_pullback_firstentryright) + ge_balance_negative_pullback_firstentryrightvalue = (dst_negative_pullback_firstentryright) + ge_balance_positive_pullback_firstentryrightvalue))))))))) /\ (exists sto_ap_pullback_firstentryproduct sto_an_pullback_firstentryproduct sto_bp_pullback_firstentryproduct sto_bn_pullback_firstentryproduct sto_cp_pullback_firstentryproduct sto_cn_pullback_firstentryproduct. (((((dc_left_pullback_firstentry) = 2 * (sto_ap_pullback_firstentryproduct) /\ (sto_an_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductleft. (((dc_left_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryproductleft + 1 /\ (sto_ap_pullback_firstentryproduct) = 0) /\ (sto_an_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductleft))) /\ ((((((dc_right_pullback_firstentry) = 2 * (sto_bp_pullback_firstentryproduct) /\ (sto_bn_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductright. (((dc_right_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryproductright + 1 /\ (sto_bp_pullback_firstentryproduct) = 0) /\ (sto_bn_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductright))) /\ ((((((dc_value_pullback_first) = 2 * (sto_cp_pullback_firstentryproduct) /\ (sto_cn_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductoutput. (((dc_value_pullback_first) = 2 * ge_signed_half_pullback_firstentryproductoutput + 1 /\ (sto_cp_pullback_firstentryproduct) = 0) /\ (sto_cn_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductoutput))) /\ ((sto_ap_pullback_firstentryproduct * sto_bp_pullback_firstentryproduct + sto_an_pullback_firstentryproduct * sto_bn_pullback_firstentryproduct) + sto_cn_pullback_firstentryproduct = (sto_ap_pullback_firstentryproduct * sto_bn_pullback_firstentryproduct + sto_an_pullback_firstentryproduct * sto_bp_pullback_firstentryproduct) + sto_cp_pullback_firstentryproduct))))))))))))))) \/ ((((dc_index_pullback_first)=0 \/ ~(exists pvs_factor_pullback_firstentrynondivisor. (n) = (dc_index_pullback_first) * pvs_factor_pullback_firstentrynondivisor)) /\ ((dc_value_pullback_first)=0))))))) -> (((exists dst_positive_code_pullback_secondtable dst_positive_scale_pullback_secondtable dst_negative_code_pullback_secondtable dst_negative_scale_pullback_secondtable. (((Q) = (((((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) * S ((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) + ((dst_positive_scale_pullback_secondtable) + (dst_positive_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))) * S ((((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) * S ((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) + ((dst_positive_scale_pullback_secondtable) + (dst_positive_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))) + ((((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))))) /\ (forall dst_index_pullback_secondtable. (exists pvs_le_gap_pullback_secondtabledomain. pvs_le_gap_pullback_secondtabledomain + (dst_index_pullback_secondtable) = (n)) -> exists dst_positive_pullback_secondtable dst_negative_pullback_secondtable dst_value_pullback_secondtable. ((((exists ff_h_pvs_pullback_secondtableentrypositive. ff_h_pvs_pullback_secondtableentrypositive + S (dst_positive_pullback_secondtable) = S ((S (dst_index_pullback_secondtable)) * dst_positive_scale_pullback_secondtable)) /\ exists ff_q_pvs_pullback_secondtableentrypositive. dst_positive_code_pullback_secondtable = ff_q_pvs_pullback_secondtableentrypositive * S ((S (dst_index_pullback_secondtable)) * dst_positive_scale_pullback_secondtable) + (dst_positive_pullback_secondtable))) /\ (((((exists ff_h_pvs_pullback_secondtableentrynegative. ff_h_pvs_pullback_secondtableentrynegative + S (dst_negative_pullback_secondtable) = S ((S (dst_index_pullback_secondtable)) * dst_negative_scale_pullback_secondtable)) /\ exists ff_q_pvs_pullback_secondtableentrynegative. dst_negative_code_pullback_secondtable = ff_q_pvs_pullback_secondtableentrynegative * S ((S (dst_index_pullback_secondtable)) * dst_negative_scale_pullback_secondtable) + (dst_negative_pullback_secondtable))) /\ (exists ge_balance_positive_pullback_secondtableentryvalue ge_balance_negative_pullback_secondtableentryvalue. (((((dst_value_pullback_secondtable) = 2 * (ge_balance_positive_pullback_secondtableentryvalue) /\ (ge_balance_negative_pullback_secondtableentryvalue) = 0) \/ exists ge_signed_half_pullback_secondtableentryvaluedecode. (((dst_value_pullback_secondtable) = 2 * ge_signed_half_pullback_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_pullback_secondtableentryvalue) = 0) /\ (ge_balance_negative_pullback_secondtableentryvalue) = S ge_signed_half_pullback_secondtableentryvaluedecode))) /\ ((dst_positive_pullback_secondtable) + ge_balance_negative_pullback_secondtableentryvalue = (dst_negative_pullback_secondtable) + ge_balance_positive_pullback_secondtableentryvalue))))))))) /\ (forall dc_index_pullback_second dc_value_pullback_second. (exists pvs_le_gap_pullback_seconddomain. pvs_le_gap_pullback_seconddomain + (dc_index_pullback_second) = (n)) -> (exists dst_positive_code_pullback_secondlookup dst_positive_scale_pullback_secondlookup dst_negative_code_pullback_secondlookup dst_negative_scale_pullback_secondlookup dst_positive_pullback_secondlookup dst_negative_pullback_secondlookup. (((Q) = (((((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) * S ((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) + ((dst_positive_scale_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))) * S ((((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) * S ((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) + ((dst_positive_scale_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))) + ((((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))))) /\ (((((exists ff_h_pvs_pullback_secondlookuppositive. ff_h_pvs_pullback_secondlookuppositive + S (dst_positive_pullback_secondlookup) = S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondlookup)) /\ exists ff_q_pvs_pullback_secondlookuppositive. dst_positive_code_pullback_secondlookup = ff_q_pvs_pullback_secondlookuppositive * S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondlookup) + (dst_positive_pullback_secondlookup))) /\ (((((exists ff_h_pvs_pullback_secondlookupnegative. ff_h_pvs_pullback_secondlookupnegative + S (dst_negative_pullback_secondlookup) = S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondlookup)) /\ exists ff_q_pvs_pullback_secondlookupnegative. dst_negative_code_pullback_secondlookup = ff_q_pvs_pullback_secondlookupnegative * S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondlookup) + (dst_negative_pullback_secondlookup))) /\ (exists ge_balance_positive_pullback_secondlookupvalue ge_balance_negative_pullback_secondlookupvalue. (((((dc_value_pullback_second) = 2 * (ge_balance_positive_pullback_secondlookupvalue) /\ (ge_balance_negative_pullback_secondlookupvalue) = 0) \/ exists ge_signed_half_pullback_secondlookupvaluedecode. (((dc_value_pullback_second) = 2 * ge_signed_half_pullback_secondlookupvaluedecode + 1 /\ (ge_balance_positive_pullback_secondlookupvalue) = 0) /\ (ge_balance_negative_pullback_secondlookupvalue) = S ge_signed_half_pullback_secondlookupvaluedecode))) /\ ((dst_positive_pullback_secondlookup) + ge_balance_negative_pullback_secondlookupvalue = (dst_negative_pullback_secondlookup) + ge_balance_positive_pullback_secondlookupvalue))))))))) -> ((((~((dc_index_pullback_second)=0)) /\ (exists dc_quotient_pullback_secondentry dc_left_pullback_secondentry dc_right_pullback_secondentry. (((n)=(dc_index_pullback_second)*dc_quotient_pullback_secondentry) /\ (((exists dst_positive_code_pullback_secondentryleft dst_positive_scale_pullback_secondentryleft dst_negative_code_pullback_secondentryleft dst_negative_scale_pullback_secondentryleft dst_positive_pullback_secondentryleft dst_negative_pullback_secondentryleft. (((G) = (((((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) * S ((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) + ((dst_positive_scale_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))) * S ((((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) * S ((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) + ((dst_positive_scale_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))) + ((((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))))) /\ (((((exists ff_h_pvs_pullback_secondentryleftpositive. ff_h_pvs_pullback_secondentryleftpositive + S (dst_positive_pullback_secondentryleft) = S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondentryleft)) /\ exists ff_q_pvs_pullback_secondentryleftpositive. dst_positive_code_pullback_secondentryleft = ff_q_pvs_pullback_secondentryleftpositive * S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondentryleft) + (dst_positive_pullback_secondentryleft))) /\ (((((exists ff_h_pvs_pullback_secondentryleftnegative. ff_h_pvs_pullback_secondentryleftnegative + S (dst_negative_pullback_secondentryleft) = S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondentryleft)) /\ exists ff_q_pvs_pullback_secondentryleftnegative. dst_negative_code_pullback_secondentryleft = ff_q_pvs_pullback_secondentryleftnegative * S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondentryleft) + (dst_negative_pullback_secondentryleft))) /\ (exists ge_balance_positive_pullback_secondentryleftvalue ge_balance_negative_pullback_secondentryleftvalue. (((((dc_left_pullback_secondentry) = 2 * (ge_balance_positive_pullback_secondentryleftvalue) /\ (ge_balance_negative_pullback_secondentryleftvalue) = 0) \/ exists ge_signed_half_pullback_secondentryleftvaluedecode. (((dc_left_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryleftvaluedecode + 1 /\ (ge_balance_positive_pullback_secondentryleftvalue) = 0) /\ (ge_balance_negative_pullback_secondentryleftvalue) = S ge_signed_half_pullback_secondentryleftvaluedecode))) /\ ((dst_positive_pullback_secondentryleft) + ge_balance_negative_pullback_secondentryleftvalue = (dst_negative_pullback_secondentryleft) + ge_balance_positive_pullback_secondentryleftvalue))))))))) /\ (((exists dst_positive_code_pullback_secondentryright dst_positive_scale_pullback_secondentryright dst_negative_code_pullback_secondentryright dst_negative_scale_pullback_secondentryright dst_positive_pullback_secondentryright dst_negative_pullback_secondentryright. (((F) = (((((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) * S ((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) + ((dst_positive_scale_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))) * S ((((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) * S ((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) + ((dst_positive_scale_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))) + ((((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))))) /\ (((((exists ff_h_pvs_pullback_secondentryrightpositive. ff_h_pvs_pullback_secondentryrightpositive + S (dst_positive_pullback_secondentryright) = S ((S (dc_quotient_pullback_secondentry)) * dst_positive_scale_pullback_secondentryright)) /\ exists ff_q_pvs_pullback_secondentryrightpositive. dst_positive_code_pullback_secondentryright = ff_q_pvs_pullback_secondentryrightpositive * S ((S (dc_quotient_pullback_secondentry)) * dst_positive_scale_pullback_secondentryright) + (dst_positive_pullback_secondentryright))) /\ (((((exists ff_h_pvs_pullback_secondentryrightnegative. ff_h_pvs_pullback_secondentryrightnegative + S (dst_negative_pullback_secondentryright) = S ((S (dc_quotient_pullback_secondentry)) * dst_negative_scale_pullback_secondentryright)) /\ exists ff_q_pvs_pullback_secondentryrightnegative. dst_negative_code_pullback_secondentryright = ff_q_pvs_pullback_secondentryrightnegative * S ((S (dc_quotient_pullback_secondentry)) * dst_negative_scale_pullback_secondentryright) + (dst_negative_pullback_secondentryright))) /\ (exists ge_balance_positive_pullback_secondentryrightvalue ge_balance_negative_pullback_secondentryrightvalue. (((((dc_right_pullback_secondentry) = 2 * (ge_balance_positive_pullback_secondentryrightvalue) /\ (ge_balance_negative_pullback_secondentryrightvalue) = 0) \/ exists ge_signed_half_pullback_secondentryrightvaluedecode. (((dc_right_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryrightvaluedecode + 1 /\ (ge_balance_positive_pullback_secondentryrightvalue) = 0) /\ (ge_balance_negative_pullback_secondentryrightvalue) = S ge_signed_half_pullback_secondentryrightvaluedecode))) /\ ((dst_positive_pullback_secondentryright) + ge_balance_negative_pullback_secondentryrightvalue = (dst_negative_pullback_secondentryright) + ge_balance_positive_pullback_secondentryrightvalue))))))))) /\ (exists sto_ap_pullback_secondentryproduct sto_an_pullback_secondentryproduct sto_bp_pullback_secondentryproduct sto_bn_pullback_secondentryproduct sto_cp_pullback_secondentryproduct sto_cn_pullback_secondentryproduct. (((((dc_left_pullback_secondentry) = 2 * (sto_ap_pullback_secondentryproduct) /\ (sto_an_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductleft. (((dc_left_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryproductleft + 1 /\ (sto_ap_pullback_secondentryproduct) = 0) /\ (sto_an_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductleft))) /\ ((((((dc_right_pullback_secondentry) = 2 * (sto_bp_pullback_secondentryproduct) /\ (sto_bn_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductright. (((dc_right_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryproductright + 1 /\ (sto_bp_pullback_secondentryproduct) = 0) /\ (sto_bn_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductright))) /\ ((((((dc_value_pullback_second) = 2 * (sto_cp_pullback_secondentryproduct) /\ (sto_cn_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductoutput. (((dc_value_pullback_second) = 2 * ge_signed_half_pullback_secondentryproductoutput + 1 /\ (sto_cp_pullback_secondentryproduct) = 0) /\ (sto_cn_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductoutput))) /\ ((sto_ap_pullback_secondentryproduct * sto_bp_pullback_secondentryproduct + sto_an_pullback_secondentryproduct * sto_bn_pullback_secondentryproduct) + sto_cn_pullback_secondentryproduct = (sto_ap_pullback_secondentryproduct * sto_bn_pullback_secondentryproduct + sto_an_pullback_secondentryproduct * sto_bp_pullback_secondentryproduct) + sto_cp_pullback_secondentryproduct))))))))))))))) \/ ((((dc_index_pullback_second)=0 \/ ~(exists pvs_factor_pullback_secondentrynondivisor. (n) = (dc_index_pullback_second) * pvs_factor_pullback_secondentrynondivisor)) /\ ((dc_value_pullback_second)=0))))))) -> (forall dvi_index_pullback_map. (exists pvs_gap_pullback_mapdomain. pvs_gap_pullback_mapdomain + S (dvi_index_pullback_map) = (S n)) -> exists dvi_value_pullback_map. ((((exists ff_h_pvs_pullback_mapentry. ff_h_pvs_pullback_mapentry + S (dvi_value_pullback_map) = S ((S (dvi_index_pullback_map)) * s)) /\ exists ff_q_pvs_pullback_mapentry. r = ff_q_pvs_pullback_mapentry * S ((S (dvi_index_pullback_map)) * s) + (dvi_value_pullback_map))) /\ ((((~((dvi_index_pullback_map)=0)) /\ ((n)=(dvi_index_pullback_map)*(dvi_value_pullback_map)))) \/ ((((dvi_index_pullback_map)=0 \/ ~(exists pvs_factor_pullback_mapgraphnondivisor. (n) = (dvi_index_pullback_map) * pvs_factor_pullback_mapgraphnondivisor)) /\ ((dvi_value_pullback_map)=(dvi_index_pullback_map))))))) -> (forall dsr_index_pullback_result dsr_image_pullback_result dsr_value_pullback_result. (exists pvs_gap_pullback_resultbound. pvs_gap_pullback_resultbound + S (dsr_index_pullback_result) = (S n)) -> (((exists ff_h_pvs_pullback_resultmap. ff_h_pvs_pullback_resultmap + S (dsr_image_pullback_result) = S ((S (dsr_index_pullback_result)) * s)) /\ exists ff_q_pvs_pullback_resultmap. r = ff_q_pvs_pullback_resultmap * S ((S (dsr_index_pullback_result)) * s) + (dsr_image_pullback_result))) -> (exists dst_positive_code_pullback_resultsource dst_positive_scale_pullback_resultsource dst_negative_code_pullback_resultsource dst_negative_scale_pullback_resultsource dst_positive_pullback_resultsource dst_negative_pullback_resultsource. (((P) = (((((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) * S ((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) + ((dst_positive_scale_pullback_resultsource) + (dst_positive_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))) * S ((((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) * S ((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) + ((dst_positive_scale_pullback_resultsource) + (dst_positive_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))) + ((((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))))) /\ (((((exists ff_h_pvs_pullback_resultsourcepositive. ff_h_pvs_pullback_resultsourcepositive + S (dst_positive_pullback_resultsource) = S ((S (dsr_image_pullback_result)) * dst_positive_scale_pullback_resultsource)) /\ exists ff_q_pvs_pullback_resultsourcepositive. dst_positive_code_pullback_resultsource = ff_q_pvs_pullback_resultsourcepositive * S ((S (dsr_image_pullback_result)) * dst_positive_scale_pullback_resultsource) + (dst_positive_pullback_resultsource))) /\ (((((exists ff_h_pvs_pullback_resultsourcenegative. ff_h_pvs_pullback_resultsourcenegative + S (dst_negative_pullback_resultsource) = S ((S (dsr_image_pullback_result)) * dst_negative_scale_pullback_resultsource)) /\ exists ff_q_pvs_pullback_resultsourcenegative. dst_negative_code_pullback_resultsource = ff_q_pvs_pullback_resultsourcenegative * S ((S (dsr_image_pullback_result)) * dst_negative_scale_pullback_resultsource) + (dst_negative_pullback_resultsource))) /\ (exists ge_balance_positive_pullback_resultsourcevalue ge_balance_negative_pullback_resultsourcevalue. (((((dsr_value_pullback_result) = 2 * (ge_balance_positive_pullback_resultsourcevalue) /\ (ge_balance_negative_pullback_resultsourcevalue) = 0) \/ exists ge_signed_half_pullback_resultsourcevaluedecode. (((dsr_value_pullback_result) = 2 * ge_signed_half_pullback_resultsourcevaluedecode + 1 /\ (ge_balance_positive_pullback_resultsourcevalue) = 0) /\ (ge_balance_negative_pullback_resultsourcevalue) = S ge_signed_half_pullback_resultsourcevaluedecode))) /\ ((dst_positive_pullback_resultsource) + ge_balance_negative_pullback_resultsourcevalue = (dst_negative_pullback_resultsource) + ge_balance_positive_pullback_resultsourcevalue))))))))) -> (exists dst_positive_code_pullback_resulttarget dst_positive_scale_pullback_resulttarget dst_negative_code_pullback_resulttarget dst_negative_scale_pullback_resulttarget dst_positive_pullback_resulttarget dst_negative_pullback_resulttarget. (((Q) = (((((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) * S ((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) + ((dst_positive_scale_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))) * S ((((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) * S ((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) + ((dst_positive_scale_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))) + ((((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))))) /\ (((((exists ff_h_pvs_pullback_resulttargetpositive. ff_h_pvs_pullback_resulttargetpositive + S (dst_positive_pullback_resulttarget) = S ((S (dsr_index_pullback_result)) * dst_positive_scale_pullback_resulttarget)) /\ exists ff_q_pvs_pullback_resulttargetpositive. dst_positive_code_pullback_resulttarget = ff_q_pvs_pullback_resulttargetpositive * S ((S (dsr_index_pullback_result)) * dst_positive_scale_pullback_resulttarget) + (dst_positive_pullback_resulttarget))) /\ (((((exists ff_h_pvs_pullback_resulttargetnegative. ff_h_pvs_pullback_resulttargetnegative + S (dst_negative_pullback_resulttarget) = S ((S (dsr_index_pullback_result)) * dst_negative_scale_pullback_resulttarget)) /\ exists ff_q_pvs_pullback_resulttargetnegative. dst_negative_code_pullback_resulttarget = ff_q_pvs_pullback_resulttargetnegative * S ((S (dsr_index_pullback_result)) * dst_negative_scale_pullback_resulttarget) + (dst_negative_pullback_resulttarget))) /\ (exists ge_balance_positive_pullback_resulttargetvalue ge_balance_negative_pullback_resulttargetvalue. (((((dsr_value_pullback_result) = 2 * (ge_balance_positive_pullback_resulttargetvalue) /\ (ge_balance_negative_pullback_resulttargetvalue) = 0) \/ exists ge_signed_half_pullback_resulttargetvaluedecode. (((dsr_value_pullback_result) = 2 * ge_signed_half_pullback_resulttargetvaluedecode + 1 /\ (ge_balance_positive_pullback_resulttargetvalue) = 0) /\ (ge_balance_negative_pullback_resulttargetvalue) = S ge_signed_half_pullback_resulttargetvaluedecode))) /\ ((dst_positive_pullback_resulttarget) + ge_balance_negative_pullback_resulttargetvalue = (dst_negative_pullback_resulttarget) + ge_balance_positive_pullback_resulttargetvalue))))))))))