dirichlet_convolution_sum_exists_unique

Exact expanded first-order arithmetic statement

forall N F G n. (exists dst_positive_code_sum_unique_left dst_positive_scale_sum_unique_left dst_negative_code_sum_unique_left dst_negative_scale_sum_unique_left. (((F) = (((((dst_positive_code_sum_unique_left) + (dst_positive_scale_sum_unique_left)) * S ((dst_positive_code_sum_unique_left) + (dst_positive_scale_sum_unique_left)) + ((dst_positive_scale_sum_unique_left) + (dst_positive_scale_sum_unique_left))) + (((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) * S ((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) + ((dst_negative_scale_sum_unique_left) + (dst_negative_scale_sum_unique_left)))) * S ((((dst_positive_code_sum_unique_left) + (dst_positive_scale_sum_unique_left)) * S ((dst_positive_code_sum_unique_left) + (dst_positive_scale_sum_unique_left)) + ((dst_positive_scale_sum_unique_left) + (dst_positive_scale_sum_unique_left))) + (((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) * S ((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) + ((dst_negative_scale_sum_unique_left) + (dst_negative_scale_sum_unique_left)))) + ((((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) * S ((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) + ((dst_negative_scale_sum_unique_left) + (dst_negative_scale_sum_unique_left))) + (((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) * S ((dst_negative_code_sum_unique_left) + (dst_negative_scale_sum_unique_left)) + ((dst_negative_scale_sum_unique_left) + (dst_negative_scale_sum_unique_left)))))) /\ (forall dst_index_sum_unique_left. (exists pvs_le_gap_sum_unique_leftdomain. pvs_le_gap_sum_unique_leftdomain + (dst_index_sum_unique_left) = (N)) -> exists dst_positive_sum_unique_left dst_negative_sum_unique_left dst_value_sum_unique_left. ((((exists ff_h_pvs_sum_unique_leftentrypositive. ff_h_pvs_sum_unique_leftentrypositive + S (dst_positive_sum_unique_left) = S ((S (dst_index_sum_unique_left)) * dst_positive_scale_sum_unique_left)) /\ exists ff_q_pvs_sum_unique_leftentrypositive. dst_positive_code_sum_unique_left = ff_q_pvs_sum_unique_leftentrypositive * S ((S (dst_index_sum_unique_left)) * dst_positive_scale_sum_unique_left) + (dst_positive_sum_unique_left))) /\ (((((exists ff_h_pvs_sum_unique_leftentrynegative. ff_h_pvs_sum_unique_leftentrynegative + S (dst_negative_sum_unique_left) = S ((S (dst_index_sum_unique_left)) * dst_negative_scale_sum_unique_left)) /\ exists ff_q_pvs_sum_unique_leftentrynegative. dst_negative_code_sum_unique_left = ff_q_pvs_sum_unique_leftentrynegative * S ((S (dst_index_sum_unique_left)) * dst_negative_scale_sum_unique_left) + (dst_negative_sum_unique_left))) /\ (exists ge_balance_positive_sum_unique_leftentryvalue ge_balance_negative_sum_unique_leftentryvalue. (((((dst_value_sum_unique_left) = 2 * (ge_balance_positive_sum_unique_leftentryvalue) /\ (ge_balance_negative_sum_unique_leftentryvalue) = 0) \/ exists ge_signed_half_sum_unique_leftentryvaluedecode. (((dst_value_sum_unique_left) = 2 * ge_signed_half_sum_unique_leftentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_leftentryvalue) = 0) /\ (ge_balance_negative_sum_unique_leftentryvalue) = S ge_signed_half_sum_unique_leftentryvaluedecode))) /\ ((dst_positive_sum_unique_left) + ge_balance_negative_sum_unique_leftentryvalue = (dst_negative_sum_unique_left) + ge_balance_positive_sum_unique_leftentryvalue))))))))) -> (exists dst_positive_code_sum_unique_right dst_positive_scale_sum_unique_right dst_negative_code_sum_unique_right dst_negative_scale_sum_unique_right. (((G) = (((((dst_positive_code_sum_unique_right) + (dst_positive_scale_sum_unique_right)) * S ((dst_positive_code_sum_unique_right) + (dst_positive_scale_sum_unique_right)) + ((dst_positive_scale_sum_unique_right) + (dst_positive_scale_sum_unique_right))) + (((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) * S ((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) + ((dst_negative_scale_sum_unique_right) + (dst_negative_scale_sum_unique_right)))) * S ((((dst_positive_code_sum_unique_right) + (dst_positive_scale_sum_unique_right)) * S ((dst_positive_code_sum_unique_right) + (dst_positive_scale_sum_unique_right)) + ((dst_positive_scale_sum_unique_right) + (dst_positive_scale_sum_unique_right))) + (((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) * S ((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) + ((dst_negative_scale_sum_unique_right) + (dst_negative_scale_sum_unique_right)))) + ((((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) * S ((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) + ((dst_negative_scale_sum_unique_right) + (dst_negative_scale_sum_unique_right))) + (((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) * S ((dst_negative_code_sum_unique_right) + (dst_negative_scale_sum_unique_right)) + ((dst_negative_scale_sum_unique_right) + (dst_negative_scale_sum_unique_right)))))) /\ (forall dst_index_sum_unique_right. (exists pvs_le_gap_sum_unique_rightdomain. pvs_le_gap_sum_unique_rightdomain + (dst_index_sum_unique_right) = (N)) -> exists dst_positive_sum_unique_right dst_negative_sum_unique_right dst_value_sum_unique_right. ((((exists ff_h_pvs_sum_unique_rightentrypositive. ff_h_pvs_sum_unique_rightentrypositive + S (dst_positive_sum_unique_right) = S ((S (dst_index_sum_unique_right)) * dst_positive_scale_sum_unique_right)) /\ exists ff_q_pvs_sum_unique_rightentrypositive. dst_positive_code_sum_unique_right = ff_q_pvs_sum_unique_rightentrypositive * S ((S (dst_index_sum_unique_right)) * dst_positive_scale_sum_unique_right) + (dst_positive_sum_unique_right))) /\ (((((exists ff_h_pvs_sum_unique_rightentrynegative. ff_h_pvs_sum_unique_rightentrynegative + S (dst_negative_sum_unique_right) = S ((S (dst_index_sum_unique_right)) * dst_negative_scale_sum_unique_right)) /\ exists ff_q_pvs_sum_unique_rightentrynegative. dst_negative_code_sum_unique_right = ff_q_pvs_sum_unique_rightentrynegative * S ((S (dst_index_sum_unique_right)) * dst_negative_scale_sum_unique_right) + (dst_negative_sum_unique_right))) /\ (exists ge_balance_positive_sum_unique_rightentryvalue ge_balance_negative_sum_unique_rightentryvalue. (((((dst_value_sum_unique_right) = 2 * (ge_balance_positive_sum_unique_rightentryvalue) /\ (ge_balance_negative_sum_unique_rightentryvalue) = 0) \/ exists ge_signed_half_sum_unique_rightentryvaluedecode. (((dst_value_sum_unique_right) = 2 * ge_signed_half_sum_unique_rightentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_rightentryvalue) = 0) /\ (ge_balance_negative_sum_unique_rightentryvalue) = S ge_signed_half_sum_unique_rightentryvaluedecode))) /\ ((dst_positive_sum_unique_right) + ge_balance_negative_sum_unique_rightentryvalue = (dst_negative_sum_unique_right) + ge_balance_positive_sum_unique_rightentryvalue))))))))) -> ~(n=0) -> (exists pvs_le_gap_sum_unique_bound. pvs_le_gap_sum_unique_bound + (n) = (N)) -> exists z. (((~((n)=0)) /\ (exists dc_mask_sum_unique_value. ((((exists dst_positive_code_sum_unique_valuemasktable dst_positive_scale_sum_unique_valuemasktable dst_negative_code_sum_unique_valuemasktable dst_negative_scale_sum_unique_valuemasktable. (((dc_mask_sum_unique_value) = (((((dst_positive_code_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable)) * S ((dst_positive_code_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable)) + ((dst_positive_scale_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable))) + (((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) * S ((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) + ((dst_negative_scale_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)))) * S ((((dst_positive_code_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable)) * S ((dst_positive_code_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable)) + ((dst_positive_scale_sum_unique_valuemasktable) + (dst_positive_scale_sum_unique_valuemasktable))) + (((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) * S ((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) + ((dst_negative_scale_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)))) + ((((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) * S ((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) + ((dst_negative_scale_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable))) + (((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) * S ((dst_negative_code_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)) + ((dst_negative_scale_sum_unique_valuemasktable) + (dst_negative_scale_sum_unique_valuemasktable)))))) /\ (forall dst_index_sum_unique_valuemasktable. (exists pvs_le_gap_sum_unique_valuemasktabledomain. pvs_le_gap_sum_unique_valuemasktabledomain + (dst_index_sum_unique_valuemasktable) = (n)) -> exists dst_positive_sum_unique_valuemasktable dst_negative_sum_unique_valuemasktable dst_value_sum_unique_valuemasktable. ((((exists ff_h_pvs_sum_unique_valuemasktableentrypositive. ff_h_pvs_sum_unique_valuemasktableentrypositive + S (dst_positive_sum_unique_valuemasktable) = S ((S (dst_index_sum_unique_valuemasktable)) * dst_positive_scale_sum_unique_valuemasktable)) /\ exists ff_q_pvs_sum_unique_valuemasktableentrypositive. dst_positive_code_sum_unique_valuemasktable = ff_q_pvs_sum_unique_valuemasktableentrypositive * S ((S (dst_index_sum_unique_valuemasktable)) * dst_positive_scale_sum_unique_valuemasktable) + (dst_positive_sum_unique_valuemasktable))) /\ (((((exists ff_h_pvs_sum_unique_valuemasktableentrynegative. ff_h_pvs_sum_unique_valuemasktableentrynegative + S (dst_negative_sum_unique_valuemasktable) = S ((S (dst_index_sum_unique_valuemasktable)) * dst_negative_scale_sum_unique_valuemasktable)) /\ exists ff_q_pvs_sum_unique_valuemasktableentrynegative. dst_negative_code_sum_unique_valuemasktable = ff_q_pvs_sum_unique_valuemasktableentrynegative * S ((S (dst_index_sum_unique_valuemasktable)) * dst_negative_scale_sum_unique_valuemasktable) + (dst_negative_sum_unique_valuemasktable))) /\ (exists ge_balance_positive_sum_unique_valuemasktableentryvalue ge_balance_negative_sum_unique_valuemasktableentryvalue. (((((dst_value_sum_unique_valuemasktable) = 2 * (ge_balance_positive_sum_unique_valuemasktableentryvalue) /\ (ge_balance_negative_sum_unique_valuemasktableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_valuemasktableentryvaluedecode. (((dst_value_sum_unique_valuemasktable) = 2 * ge_signed_half_sum_unique_valuemasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_valuemasktableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_valuemasktableentryvalue) = S ge_signed_half_sum_unique_valuemasktableentryvaluedecode))) /\ ((dst_positive_sum_unique_valuemasktable) + ge_balance_negative_sum_unique_valuemasktableentryvalue = (dst_negative_sum_unique_valuemasktable) + ge_balance_positive_sum_unique_valuemasktableentryvalue))))))))) /\ (forall dc_index_sum_unique_valuemask dc_value_sum_unique_valuemask. (exists pvs_le_gap_sum_unique_valuemaskdomain. pvs_le_gap_sum_unique_valuemaskdomain + (dc_index_sum_unique_valuemask) = (n)) -> (exists dst_positive_code_sum_unique_valuemasklookup dst_positive_scale_sum_unique_valuemasklookup dst_negative_code_sum_unique_valuemasklookup dst_negative_scale_sum_unique_valuemasklookup dst_positive_sum_unique_valuemasklookup dst_negative_sum_unique_valuemasklookup. (((dc_mask_sum_unique_value) = (((((dst_positive_code_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup)) * S ((dst_positive_code_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup)) + ((dst_positive_scale_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup))) + (((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) * S ((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) + ((dst_negative_scale_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)))) * S ((((dst_positive_code_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup)) * S ((dst_positive_code_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup)) + ((dst_positive_scale_sum_unique_valuemasklookup) + (dst_positive_scale_sum_unique_valuemasklookup))) + (((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) * S ((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) + ((dst_negative_scale_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)))) + ((((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) * S ((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) + ((dst_negative_scale_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup))) + (((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) * S ((dst_negative_code_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)) + ((dst_negative_scale_sum_unique_valuemasklookup) + (dst_negative_scale_sum_unique_valuemasklookup)))))) /\ (((((exists ff_h_pvs_sum_unique_valuemasklookuppositive. ff_h_pvs_sum_unique_valuemasklookuppositive + S (dst_positive_sum_unique_valuemasklookup) = S ((S (dc_index_sum_unique_valuemask)) * dst_positive_scale_sum_unique_valuemasklookup)) /\ exists ff_q_pvs_sum_unique_valuemasklookuppositive. dst_positive_code_sum_unique_valuemasklookup = ff_q_pvs_sum_unique_valuemasklookuppositive * S ((S (dc_index_sum_unique_valuemask)) * dst_positive_scale_sum_unique_valuemasklookup) + (dst_positive_sum_unique_valuemasklookup))) /\ (((((exists ff_h_pvs_sum_unique_valuemasklookupnegative. ff_h_pvs_sum_unique_valuemasklookupnegative + S (dst_negative_sum_unique_valuemasklookup) = S ((S (dc_index_sum_unique_valuemask)) * dst_negative_scale_sum_unique_valuemasklookup)) /\ exists ff_q_pvs_sum_unique_valuemasklookupnegative. dst_negative_code_sum_unique_valuemasklookup = ff_q_pvs_sum_unique_valuemasklookupnegative * S ((S (dc_index_sum_unique_valuemask)) * dst_negative_scale_sum_unique_valuemasklookup) + (dst_negative_sum_unique_valuemasklookup))) /\ (exists ge_balance_positive_sum_unique_valuemasklookupvalue ge_balance_negative_sum_unique_valuemasklookupvalue. (((((dc_value_sum_unique_valuemask) = 2 * (ge_balance_positive_sum_unique_valuemasklookupvalue) /\ (ge_balance_negative_sum_unique_valuemasklookupvalue) = 0) \/ exists ge_signed_half_sum_unique_valuemasklookupvaluedecode. (((dc_value_sum_unique_valuemask) = 2 * ge_signed_half_sum_unique_valuemasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_unique_valuemasklookupvalue) = 0) /\ (ge_balance_negative_sum_unique_valuemasklookupvalue) = S ge_signed_half_sum_unique_valuemasklookupvaluedecode))) /\ ((dst_positive_sum_unique_valuemasklookup) + ge_balance_negative_sum_unique_valuemasklookupvalue = (dst_negative_sum_unique_valuemasklookup) + ge_balance_positive_sum_unique_valuemasklookupvalue))))))))) -> ((((~((dc_index_sum_unique_valuemask)=0)) /\ (exists dc_quotient_sum_unique_valuemaskentry dc_left_sum_unique_valuemaskentry dc_right_sum_unique_valuemaskentry. (((n)=(dc_index_sum_unique_valuemask)*dc_quotient_sum_unique_valuemaskentry) /\ (((exists dst_positive_code_sum_unique_valuemaskentryleft dst_positive_scale_sum_unique_valuemaskentryleft dst_negative_code_sum_unique_valuemaskentryleft dst_negative_scale_sum_unique_valuemaskentryleft dst_positive_sum_unique_valuemaskentryleft dst_negative_sum_unique_valuemaskentryleft. (((F) = (((((dst_positive_code_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft)) * S ((dst_positive_code_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft)) + ((dst_positive_scale_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft))) + (((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) * S ((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) + ((dst_negative_scale_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)))) * S ((((dst_positive_code_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft)) * S ((dst_positive_code_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft)) + ((dst_positive_scale_sum_unique_valuemaskentryleft) + (dst_positive_scale_sum_unique_valuemaskentryleft))) + (((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) * S ((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) + ((dst_negative_scale_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)))) + ((((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) * S ((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) + ((dst_negative_scale_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft))) + (((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) * S ((dst_negative_code_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)) + ((dst_negative_scale_sum_unique_valuemaskentryleft) + (dst_negative_scale_sum_unique_valuemaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_unique_valuemaskentryleftpositive. ff_h_pvs_sum_unique_valuemaskentryleftpositive + S (dst_positive_sum_unique_valuemaskentryleft) = S ((S (dc_index_sum_unique_valuemask)) * dst_positive_scale_sum_unique_valuemaskentryleft)) /\ exists ff_q_pvs_sum_unique_valuemaskentryleftpositive. dst_positive_code_sum_unique_valuemaskentryleft = ff_q_pvs_sum_unique_valuemaskentryleftpositive * S ((S (dc_index_sum_unique_valuemask)) * dst_positive_scale_sum_unique_valuemaskentryleft) + (dst_positive_sum_unique_valuemaskentryleft))) /\ (((((exists ff_h_pvs_sum_unique_valuemaskentryleftnegative. ff_h_pvs_sum_unique_valuemaskentryleftnegative + S (dst_negative_sum_unique_valuemaskentryleft) = S ((S (dc_index_sum_unique_valuemask)) * dst_negative_scale_sum_unique_valuemaskentryleft)) /\ exists ff_q_pvs_sum_unique_valuemaskentryleftnegative. dst_negative_code_sum_unique_valuemaskentryleft = ff_q_pvs_sum_unique_valuemaskentryleftnegative * S ((S (dc_index_sum_unique_valuemask)) * dst_negative_scale_sum_unique_valuemaskentryleft) + (dst_negative_sum_unique_valuemaskentryleft))) /\ (exists ge_balance_positive_sum_unique_valuemaskentryleftvalue ge_balance_negative_sum_unique_valuemaskentryleftvalue. (((((dc_left_sum_unique_valuemaskentry) = 2 * (ge_balance_positive_sum_unique_valuemaskentryleftvalue) /\ (ge_balance_negative_sum_unique_valuemaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_unique_valuemaskentryleftvaluedecode. (((dc_left_sum_unique_valuemaskentry) = 2 * ge_signed_half_sum_unique_valuemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_unique_valuemaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_unique_valuemaskentryleftvalue) = S ge_signed_half_sum_unique_valuemaskentryleftvaluedecode))) /\ ((dst_positive_sum_unique_valuemaskentryleft) + ge_balance_negative_sum_unique_valuemaskentryleftvalue = (dst_negative_sum_unique_valuemaskentryleft) + ge_balance_positive_sum_unique_valuemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_unique_valuemaskentryright dst_positive_scale_sum_unique_valuemaskentryright dst_negative_code_sum_unique_valuemaskentryright dst_negative_scale_sum_unique_valuemaskentryright dst_positive_sum_unique_valuemaskentryright dst_negative_sum_unique_valuemaskentryright. (((G) = (((((dst_positive_code_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright)) * S ((dst_positive_code_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright)) + ((dst_positive_scale_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright))) + (((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) * S ((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) + ((dst_negative_scale_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)))) * S ((((dst_positive_code_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright)) * S ((dst_positive_code_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright)) + ((dst_positive_scale_sum_unique_valuemaskentryright) + (dst_positive_scale_sum_unique_valuemaskentryright))) + (((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) * S ((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) + ((dst_negative_scale_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)))) + ((((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) * S ((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) + ((dst_negative_scale_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright))) + (((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) * S ((dst_negative_code_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)) + ((dst_negative_scale_sum_unique_valuemaskentryright) + (dst_negative_scale_sum_unique_valuemaskentryright)))))) /\ (((((exists ff_h_pvs_sum_unique_valuemaskentryrightpositive. ff_h_pvs_sum_unique_valuemaskentryrightpositive + S (dst_positive_sum_unique_valuemaskentryright) = S ((S (dc_quotient_sum_unique_valuemaskentry)) * dst_positive_scale_sum_unique_valuemaskentryright)) /\ exists ff_q_pvs_sum_unique_valuemaskentryrightpositive. dst_positive_code_sum_unique_valuemaskentryright = ff_q_pvs_sum_unique_valuemaskentryrightpositive * S ((S (dc_quotient_sum_unique_valuemaskentry)) * dst_positive_scale_sum_unique_valuemaskentryright) + (dst_positive_sum_unique_valuemaskentryright))) /\ (((((exists ff_h_pvs_sum_unique_valuemaskentryrightnegative. ff_h_pvs_sum_unique_valuemaskentryrightnegative + S (dst_negative_sum_unique_valuemaskentryright) = S ((S (dc_quotient_sum_unique_valuemaskentry)) * dst_negative_scale_sum_unique_valuemaskentryright)) /\ exists ff_q_pvs_sum_unique_valuemaskentryrightnegative. dst_negative_code_sum_unique_valuemaskentryright = ff_q_pvs_sum_unique_valuemaskentryrightnegative * S ((S (dc_quotient_sum_unique_valuemaskentry)) * dst_negative_scale_sum_unique_valuemaskentryright) + (dst_negative_sum_unique_valuemaskentryright))) /\ (exists ge_balance_positive_sum_unique_valuemaskentryrightvalue ge_balance_negative_sum_unique_valuemaskentryrightvalue. (((((dc_right_sum_unique_valuemaskentry) = 2 * (ge_balance_positive_sum_unique_valuemaskentryrightvalue) /\ (ge_balance_negative_sum_unique_valuemaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_unique_valuemaskentryrightvaluedecode. (((dc_right_sum_unique_valuemaskentry) = 2 * ge_signed_half_sum_unique_valuemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_unique_valuemaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_unique_valuemaskentryrightvalue) = S ge_signed_half_sum_unique_valuemaskentryrightvaluedecode))) /\ ((dst_positive_sum_unique_valuemaskentryright) + ge_balance_negative_sum_unique_valuemaskentryrightvalue = (dst_negative_sum_unique_valuemaskentryright) + ge_balance_positive_sum_unique_valuemaskentryrightvalue))))))))) /\ (exists sto_ap_sum_unique_valuemaskentryproduct sto_an_sum_unique_valuemaskentryproduct sto_bp_sum_unique_valuemaskentryproduct sto_bn_sum_unique_valuemaskentryproduct sto_cp_sum_unique_valuemaskentryproduct sto_cn_sum_unique_valuemaskentryproduct. (((((dc_left_sum_unique_valuemaskentry) = 2 * (sto_ap_sum_unique_valuemaskentryproduct) /\ (sto_an_sum_unique_valuemaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_valuemaskentryproductleft. (((dc_left_sum_unique_valuemaskentry) = 2 * ge_signed_half_sum_unique_valuemaskentryproductleft + 1 /\ (sto_ap_sum_unique_valuemaskentryproduct) = 0) /\ (sto_an_sum_unique_valuemaskentryproduct) = S ge_signed_half_sum_unique_valuemaskentryproductleft))) /\ ((((((dc_right_sum_unique_valuemaskentry) = 2 * (sto_bp_sum_unique_valuemaskentryproduct) /\ (sto_bn_sum_unique_valuemaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_valuemaskentryproductright. (((dc_right_sum_unique_valuemaskentry) = 2 * ge_signed_half_sum_unique_valuemaskentryproductright + 1 /\ (sto_bp_sum_unique_valuemaskentryproduct) = 0) /\ (sto_bn_sum_unique_valuemaskentryproduct) = S ge_signed_half_sum_unique_valuemaskentryproductright))) /\ ((((((dc_value_sum_unique_valuemask) = 2 * (sto_cp_sum_unique_valuemaskentryproduct) /\ (sto_cn_sum_unique_valuemaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_valuemaskentryproductoutput. (((dc_value_sum_unique_valuemask) = 2 * ge_signed_half_sum_unique_valuemaskentryproductoutput + 1 /\ (sto_cp_sum_unique_valuemaskentryproduct) = 0) /\ (sto_cn_sum_unique_valuemaskentryproduct) = S ge_signed_half_sum_unique_valuemaskentryproductoutput))) /\ ((sto_ap_sum_unique_valuemaskentryproduct * sto_bp_sum_unique_valuemaskentryproduct + sto_an_sum_unique_valuemaskentryproduct * sto_bn_sum_unique_valuemaskentryproduct) + sto_cn_sum_unique_valuemaskentryproduct = (sto_ap_sum_unique_valuemaskentryproduct * sto_bn_sum_unique_valuemaskentryproduct + sto_an_sum_unique_valuemaskentryproduct * sto_bp_sum_unique_valuemaskentryproduct) + sto_cp_sum_unique_valuemaskentryproduct))))))))))))))) \/ ((((dc_index_sum_unique_valuemask)=0 \/ ~(exists pvs_factor_sum_unique_valuemaskentrynondivisor. (n) = (dc_index_sum_unique_valuemask) * pvs_factor_sum_unique_valuemaskentrynondivisor)) /\ ((dc_value_sum_unique_valuemask)=0))))))) /\ (exists dst_positive_code_sum_unique_valuefold dst_positive_scale_sum_unique_valuefold dst_negative_code_sum_unique_valuefold dst_negative_scale_sum_unique_valuefold dst_positive_sum_sum_unique_valuefold dst_negative_sum_sum_unique_valuefold. (((dc_mask_sum_unique_value) = (((((dst_positive_code_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold)) * S ((dst_positive_code_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold)) + ((dst_positive_scale_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold))) + (((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) * S ((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) + ((dst_negative_scale_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)))) * S ((((dst_positive_code_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold)) * S ((dst_positive_code_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold)) + ((dst_positive_scale_sum_unique_valuefold) + (dst_positive_scale_sum_unique_valuefold))) + (((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) * S ((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) + ((dst_negative_scale_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)))) + ((((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) * S ((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) + ((dst_negative_scale_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold))) + (((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) * S ((dst_negative_code_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)) + ((dst_negative_scale_sum_unique_valuefold) + (dst_negative_scale_sum_unique_valuefold)))))) /\ (((exists fs_u_dst_sum_unique_valuefoldpositive fs_v_dst_sum_unique_valuefoldpositive. ((((exists fs_h_dst_sum_unique_valuefoldpositive_body_start. fs_h_dst_sum_unique_valuefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_valuefoldpositive)) /\ exists fs_q_dst_sum_unique_valuefoldpositive_body_start. fs_u_dst_sum_unique_valuefoldpositive = fs_q_dst_sum_unique_valuefoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_valuefoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_valuefoldpositive_body_terminal. fs_h_dst_sum_unique_valuefoldpositive_body_terminal + S (dst_positive_sum_sum_unique_valuefold) = S ((S (S (n))) * fs_v_dst_sum_unique_valuefoldpositive)) /\ exists fs_q_dst_sum_unique_valuefoldpositive_body_terminal. fs_u_dst_sum_unique_valuefoldpositive = fs_q_dst_sum_unique_valuefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_valuefoldpositive) + (dst_positive_sum_sum_unique_valuefold))) /\ forall fs_i_dst_sum_unique_valuefoldpositive_body_steps. (exists fs_lt_dst_sum_unique_valuefoldpositive_body_steps_bound. fs_lt_dst_sum_unique_valuefoldpositive_body_steps_bound + S fs_i_dst_sum_unique_valuefoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_unique_valuefoldpositive_body_steps fs_r_dst_sum_unique_valuefoldpositive_body_steps fs_s_dst_sum_unique_valuefoldpositive_body_steps. ((((exists fs_h_dst_sum_unique_valuefoldpositive_body_steps_summand. fs_h_dst_sum_unique_valuefoldpositive_body_steps_summand + S (fs_a_dst_sum_unique_valuefoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * dst_positive_scale_sum_unique_valuefold)) /\ exists fs_q_dst_sum_unique_valuefoldpositive_body_steps_summand. dst_positive_code_sum_unique_valuefold = fs_q_dst_sum_unique_valuefoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * dst_positive_scale_sum_unique_valuefold) + (fs_a_dst_sum_unique_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_valuefoldpositive_body_steps_partial. fs_h_dst_sum_unique_valuefoldpositive_body_steps_partial + S (fs_r_dst_sum_unique_valuefoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * fs_v_dst_sum_unique_valuefoldpositive)) /\ exists fs_q_dst_sum_unique_valuefoldpositive_body_steps_partial. fs_u_dst_sum_unique_valuefoldpositive = fs_q_dst_sum_unique_valuefoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * fs_v_dst_sum_unique_valuefoldpositive) + (fs_r_dst_sum_unique_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_valuefoldpositive_body_steps_successor. fs_h_dst_sum_unique_valuefoldpositive_body_steps_successor + S (fs_s_dst_sum_unique_valuefoldpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * fs_v_dst_sum_unique_valuefoldpositive)) /\ exists fs_q_dst_sum_unique_valuefoldpositive_body_steps_successor. fs_u_dst_sum_unique_valuefoldpositive = fs_q_dst_sum_unique_valuefoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_valuefoldpositive_body_steps)) * fs_v_dst_sum_unique_valuefoldpositive) + (fs_s_dst_sum_unique_valuefoldpositive_body_steps))) /\ fs_s_dst_sum_unique_valuefoldpositive_body_steps = fs_r_dst_sum_unique_valuefoldpositive_body_steps + fs_a_dst_sum_unique_valuefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_valuefoldnegative fs_v_dst_sum_unique_valuefoldnegative. ((((exists fs_h_dst_sum_unique_valuefoldnegative_body_start. fs_h_dst_sum_unique_valuefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_valuefoldnegative)) /\ exists fs_q_dst_sum_unique_valuefoldnegative_body_start. fs_u_dst_sum_unique_valuefoldnegative = fs_q_dst_sum_unique_valuefoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_valuefoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_valuefoldnegative_body_terminal. fs_h_dst_sum_unique_valuefoldnegative_body_terminal + S (dst_negative_sum_sum_unique_valuefold) = S ((S (S (n))) * fs_v_dst_sum_unique_valuefoldnegative)) /\ exists fs_q_dst_sum_unique_valuefoldnegative_body_terminal. fs_u_dst_sum_unique_valuefoldnegative = fs_q_dst_sum_unique_valuefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_valuefoldnegative) + (dst_negative_sum_sum_unique_valuefold))) /\ forall fs_i_dst_sum_unique_valuefoldnegative_body_steps. (exists fs_lt_dst_sum_unique_valuefoldnegative_body_steps_bound. fs_lt_dst_sum_unique_valuefoldnegative_body_steps_bound + S fs_i_dst_sum_unique_valuefoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_unique_valuefoldnegative_body_steps fs_r_dst_sum_unique_valuefoldnegative_body_steps fs_s_dst_sum_unique_valuefoldnegative_body_steps. ((((exists fs_h_dst_sum_unique_valuefoldnegative_body_steps_summand. fs_h_dst_sum_unique_valuefoldnegative_body_steps_summand + S (fs_a_dst_sum_unique_valuefoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * dst_negative_scale_sum_unique_valuefold)) /\ exists fs_q_dst_sum_unique_valuefoldnegative_body_steps_summand. dst_negative_code_sum_unique_valuefold = fs_q_dst_sum_unique_valuefoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * dst_negative_scale_sum_unique_valuefold) + (fs_a_dst_sum_unique_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_valuefoldnegative_body_steps_partial. fs_h_dst_sum_unique_valuefoldnegative_body_steps_partial + S (fs_r_dst_sum_unique_valuefoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * fs_v_dst_sum_unique_valuefoldnegative)) /\ exists fs_q_dst_sum_unique_valuefoldnegative_body_steps_partial. fs_u_dst_sum_unique_valuefoldnegative = fs_q_dst_sum_unique_valuefoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * fs_v_dst_sum_unique_valuefoldnegative) + (fs_r_dst_sum_unique_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_valuefoldnegative_body_steps_successor. fs_h_dst_sum_unique_valuefoldnegative_body_steps_successor + S (fs_s_dst_sum_unique_valuefoldnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * fs_v_dst_sum_unique_valuefoldnegative)) /\ exists fs_q_dst_sum_unique_valuefoldnegative_body_steps_successor. fs_u_dst_sum_unique_valuefoldnegative = fs_q_dst_sum_unique_valuefoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_valuefoldnegative_body_steps)) * fs_v_dst_sum_unique_valuefoldnegative) + (fs_s_dst_sum_unique_valuefoldnegative_body_steps))) /\ fs_s_dst_sum_unique_valuefoldnegative_body_steps = fs_r_dst_sum_unique_valuefoldnegative_body_steps + fs_a_dst_sum_unique_valuefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_valuefoldresult ge_balance_negative_sum_unique_valuefoldresult. (((((z) = 2 * (ge_balance_positive_sum_unique_valuefoldresult) /\ (ge_balance_negative_sum_unique_valuefoldresult) = 0) \/ exists ge_signed_half_sum_unique_valuefoldresultdecode. (((z) = 2 * ge_signed_half_sum_unique_valuefoldresultdecode + 1 /\ (ge_balance_positive_sum_unique_valuefoldresult) = 0) /\ (ge_balance_negative_sum_unique_valuefoldresult) = S ge_signed_half_sum_unique_valuefoldresultdecode))) /\ ((dst_positive_sum_sum_unique_valuefold) + ge_balance_negative_sum_unique_valuefoldresult = (dst_negative_sum_sum_unique_valuefold) + ge_balance_positive_sum_unique_valuefoldresult))))))))))))) /\ forall w. (((~((n)=0)) /\ (exists dc_mask_sum_unique_other. ((((exists dst_positive_code_sum_unique_othermasktable dst_positive_scale_sum_unique_othermasktable dst_negative_code_sum_unique_othermasktable dst_negative_scale_sum_unique_othermasktable. (((dc_mask_sum_unique_other) = (((((dst_positive_code_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable)) * S ((dst_positive_code_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable)) + ((dst_positive_scale_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable))) + (((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) * S ((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) + ((dst_negative_scale_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)))) * S ((((dst_positive_code_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable)) * S ((dst_positive_code_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable)) + ((dst_positive_scale_sum_unique_othermasktable) + (dst_positive_scale_sum_unique_othermasktable))) + (((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) * S ((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) + ((dst_negative_scale_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)))) + ((((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) * S ((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) + ((dst_negative_scale_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable))) + (((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) * S ((dst_negative_code_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)) + ((dst_negative_scale_sum_unique_othermasktable) + (dst_negative_scale_sum_unique_othermasktable)))))) /\ (forall dst_index_sum_unique_othermasktable. (exists pvs_le_gap_sum_unique_othermasktabledomain. pvs_le_gap_sum_unique_othermasktabledomain + (dst_index_sum_unique_othermasktable) = (n)) -> exists dst_positive_sum_unique_othermasktable dst_negative_sum_unique_othermasktable dst_value_sum_unique_othermasktable. ((((exists ff_h_pvs_sum_unique_othermasktableentrypositive. ff_h_pvs_sum_unique_othermasktableentrypositive + S (dst_positive_sum_unique_othermasktable) = S ((S (dst_index_sum_unique_othermasktable)) * dst_positive_scale_sum_unique_othermasktable)) /\ exists ff_q_pvs_sum_unique_othermasktableentrypositive. dst_positive_code_sum_unique_othermasktable = ff_q_pvs_sum_unique_othermasktableentrypositive * S ((S (dst_index_sum_unique_othermasktable)) * dst_positive_scale_sum_unique_othermasktable) + (dst_positive_sum_unique_othermasktable))) /\ (((((exists ff_h_pvs_sum_unique_othermasktableentrynegative. ff_h_pvs_sum_unique_othermasktableentrynegative + S (dst_negative_sum_unique_othermasktable) = S ((S (dst_index_sum_unique_othermasktable)) * dst_negative_scale_sum_unique_othermasktable)) /\ exists ff_q_pvs_sum_unique_othermasktableentrynegative. dst_negative_code_sum_unique_othermasktable = ff_q_pvs_sum_unique_othermasktableentrynegative * S ((S (dst_index_sum_unique_othermasktable)) * dst_negative_scale_sum_unique_othermasktable) + (dst_negative_sum_unique_othermasktable))) /\ (exists ge_balance_positive_sum_unique_othermasktableentryvalue ge_balance_negative_sum_unique_othermasktableentryvalue. (((((dst_value_sum_unique_othermasktable) = 2 * (ge_balance_positive_sum_unique_othermasktableentryvalue) /\ (ge_balance_negative_sum_unique_othermasktableentryvalue) = 0) \/ exists ge_signed_half_sum_unique_othermasktableentryvaluedecode. (((dst_value_sum_unique_othermasktable) = 2 * ge_signed_half_sum_unique_othermasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othermasktableentryvalue) = 0) /\ (ge_balance_negative_sum_unique_othermasktableentryvalue) = S ge_signed_half_sum_unique_othermasktableentryvaluedecode))) /\ ((dst_positive_sum_unique_othermasktable) + ge_balance_negative_sum_unique_othermasktableentryvalue = (dst_negative_sum_unique_othermasktable) + ge_balance_positive_sum_unique_othermasktableentryvalue))))))))) /\ (forall dc_index_sum_unique_othermask dc_value_sum_unique_othermask. (exists pvs_le_gap_sum_unique_othermaskdomain. pvs_le_gap_sum_unique_othermaskdomain + (dc_index_sum_unique_othermask) = (n)) -> (exists dst_positive_code_sum_unique_othermasklookup dst_positive_scale_sum_unique_othermasklookup dst_negative_code_sum_unique_othermasklookup dst_negative_scale_sum_unique_othermasklookup dst_positive_sum_unique_othermasklookup dst_negative_sum_unique_othermasklookup. (((dc_mask_sum_unique_other) = (((((dst_positive_code_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup)) * S ((dst_positive_code_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup)) + ((dst_positive_scale_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup))) + (((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) * S ((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) + ((dst_negative_scale_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)))) * S ((((dst_positive_code_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup)) * S ((dst_positive_code_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup)) + ((dst_positive_scale_sum_unique_othermasklookup) + (dst_positive_scale_sum_unique_othermasklookup))) + (((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) * S ((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) + ((dst_negative_scale_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)))) + ((((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) * S ((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) + ((dst_negative_scale_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup))) + (((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) * S ((dst_negative_code_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)) + ((dst_negative_scale_sum_unique_othermasklookup) + (dst_negative_scale_sum_unique_othermasklookup)))))) /\ (((((exists ff_h_pvs_sum_unique_othermasklookuppositive. ff_h_pvs_sum_unique_othermasklookuppositive + S (dst_positive_sum_unique_othermasklookup) = S ((S (dc_index_sum_unique_othermask)) * dst_positive_scale_sum_unique_othermasklookup)) /\ exists ff_q_pvs_sum_unique_othermasklookuppositive. dst_positive_code_sum_unique_othermasklookup = ff_q_pvs_sum_unique_othermasklookuppositive * S ((S (dc_index_sum_unique_othermask)) * dst_positive_scale_sum_unique_othermasklookup) + (dst_positive_sum_unique_othermasklookup))) /\ (((((exists ff_h_pvs_sum_unique_othermasklookupnegative. ff_h_pvs_sum_unique_othermasklookupnegative + S (dst_negative_sum_unique_othermasklookup) = S ((S (dc_index_sum_unique_othermask)) * dst_negative_scale_sum_unique_othermasklookup)) /\ exists ff_q_pvs_sum_unique_othermasklookupnegative. dst_negative_code_sum_unique_othermasklookup = ff_q_pvs_sum_unique_othermasklookupnegative * S ((S (dc_index_sum_unique_othermask)) * dst_negative_scale_sum_unique_othermasklookup) + (dst_negative_sum_unique_othermasklookup))) /\ (exists ge_balance_positive_sum_unique_othermasklookupvalue ge_balance_negative_sum_unique_othermasklookupvalue. (((((dc_value_sum_unique_othermask) = 2 * (ge_balance_positive_sum_unique_othermasklookupvalue) /\ (ge_balance_negative_sum_unique_othermasklookupvalue) = 0) \/ exists ge_signed_half_sum_unique_othermasklookupvaluedecode. (((dc_value_sum_unique_othermask) = 2 * ge_signed_half_sum_unique_othermasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othermasklookupvalue) = 0) /\ (ge_balance_negative_sum_unique_othermasklookupvalue) = S ge_signed_half_sum_unique_othermasklookupvaluedecode))) /\ ((dst_positive_sum_unique_othermasklookup) + ge_balance_negative_sum_unique_othermasklookupvalue = (dst_negative_sum_unique_othermasklookup) + ge_balance_positive_sum_unique_othermasklookupvalue))))))))) -> ((((~((dc_index_sum_unique_othermask)=0)) /\ (exists dc_quotient_sum_unique_othermaskentry dc_left_sum_unique_othermaskentry dc_right_sum_unique_othermaskentry. (((n)=(dc_index_sum_unique_othermask)*dc_quotient_sum_unique_othermaskentry) /\ (((exists dst_positive_code_sum_unique_othermaskentryleft dst_positive_scale_sum_unique_othermaskentryleft dst_negative_code_sum_unique_othermaskentryleft dst_negative_scale_sum_unique_othermaskentryleft dst_positive_sum_unique_othermaskentryleft dst_negative_sum_unique_othermaskentryleft. (((F) = (((((dst_positive_code_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft)) * S ((dst_positive_code_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft)) + ((dst_positive_scale_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft))) + (((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) * S ((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) + ((dst_negative_scale_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)))) * S ((((dst_positive_code_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft)) * S ((dst_positive_code_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft)) + ((dst_positive_scale_sum_unique_othermaskentryleft) + (dst_positive_scale_sum_unique_othermaskentryleft))) + (((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) * S ((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) + ((dst_negative_scale_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)))) + ((((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) * S ((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) + ((dst_negative_scale_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft))) + (((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) * S ((dst_negative_code_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)) + ((dst_negative_scale_sum_unique_othermaskentryleft) + (dst_negative_scale_sum_unique_othermaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_unique_othermaskentryleftpositive. ff_h_pvs_sum_unique_othermaskentryleftpositive + S (dst_positive_sum_unique_othermaskentryleft) = S ((S (dc_index_sum_unique_othermask)) * dst_positive_scale_sum_unique_othermaskentryleft)) /\ exists ff_q_pvs_sum_unique_othermaskentryleftpositive. dst_positive_code_sum_unique_othermaskentryleft = ff_q_pvs_sum_unique_othermaskentryleftpositive * S ((S (dc_index_sum_unique_othermask)) * dst_positive_scale_sum_unique_othermaskentryleft) + (dst_positive_sum_unique_othermaskentryleft))) /\ (((((exists ff_h_pvs_sum_unique_othermaskentryleftnegative. ff_h_pvs_sum_unique_othermaskentryleftnegative + S (dst_negative_sum_unique_othermaskentryleft) = S ((S (dc_index_sum_unique_othermask)) * dst_negative_scale_sum_unique_othermaskentryleft)) /\ exists ff_q_pvs_sum_unique_othermaskentryleftnegative. dst_negative_code_sum_unique_othermaskentryleft = ff_q_pvs_sum_unique_othermaskentryleftnegative * S ((S (dc_index_sum_unique_othermask)) * dst_negative_scale_sum_unique_othermaskentryleft) + (dst_negative_sum_unique_othermaskentryleft))) /\ (exists ge_balance_positive_sum_unique_othermaskentryleftvalue ge_balance_negative_sum_unique_othermaskentryleftvalue. (((((dc_left_sum_unique_othermaskentry) = 2 * (ge_balance_positive_sum_unique_othermaskentryleftvalue) /\ (ge_balance_negative_sum_unique_othermaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_unique_othermaskentryleftvaluedecode. (((dc_left_sum_unique_othermaskentry) = 2 * ge_signed_half_sum_unique_othermaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othermaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_unique_othermaskentryleftvalue) = S ge_signed_half_sum_unique_othermaskentryleftvaluedecode))) /\ ((dst_positive_sum_unique_othermaskentryleft) + ge_balance_negative_sum_unique_othermaskentryleftvalue = (dst_negative_sum_unique_othermaskentryleft) + ge_balance_positive_sum_unique_othermaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_unique_othermaskentryright dst_positive_scale_sum_unique_othermaskentryright dst_negative_code_sum_unique_othermaskentryright dst_negative_scale_sum_unique_othermaskentryright dst_positive_sum_unique_othermaskentryright dst_negative_sum_unique_othermaskentryright. (((G) = (((((dst_positive_code_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright)) * S ((dst_positive_code_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright)) + ((dst_positive_scale_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright))) + (((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) * S ((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) + ((dst_negative_scale_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)))) * S ((((dst_positive_code_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright)) * S ((dst_positive_code_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright)) + ((dst_positive_scale_sum_unique_othermaskentryright) + (dst_positive_scale_sum_unique_othermaskentryright))) + (((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) * S ((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) + ((dst_negative_scale_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)))) + ((((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) * S ((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) + ((dst_negative_scale_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright))) + (((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) * S ((dst_negative_code_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)) + ((dst_negative_scale_sum_unique_othermaskentryright) + (dst_negative_scale_sum_unique_othermaskentryright)))))) /\ (((((exists ff_h_pvs_sum_unique_othermaskentryrightpositive. ff_h_pvs_sum_unique_othermaskentryrightpositive + S (dst_positive_sum_unique_othermaskentryright) = S ((S (dc_quotient_sum_unique_othermaskentry)) * dst_positive_scale_sum_unique_othermaskentryright)) /\ exists ff_q_pvs_sum_unique_othermaskentryrightpositive. dst_positive_code_sum_unique_othermaskentryright = ff_q_pvs_sum_unique_othermaskentryrightpositive * S ((S (dc_quotient_sum_unique_othermaskentry)) * dst_positive_scale_sum_unique_othermaskentryright) + (dst_positive_sum_unique_othermaskentryright))) /\ (((((exists ff_h_pvs_sum_unique_othermaskentryrightnegative. ff_h_pvs_sum_unique_othermaskentryrightnegative + S (dst_negative_sum_unique_othermaskentryright) = S ((S (dc_quotient_sum_unique_othermaskentry)) * dst_negative_scale_sum_unique_othermaskentryright)) /\ exists ff_q_pvs_sum_unique_othermaskentryrightnegative. dst_negative_code_sum_unique_othermaskentryright = ff_q_pvs_sum_unique_othermaskentryrightnegative * S ((S (dc_quotient_sum_unique_othermaskentry)) * dst_negative_scale_sum_unique_othermaskentryright) + (dst_negative_sum_unique_othermaskentryright))) /\ (exists ge_balance_positive_sum_unique_othermaskentryrightvalue ge_balance_negative_sum_unique_othermaskentryrightvalue. (((((dc_right_sum_unique_othermaskentry) = 2 * (ge_balance_positive_sum_unique_othermaskentryrightvalue) /\ (ge_balance_negative_sum_unique_othermaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_unique_othermaskentryrightvaluedecode. (((dc_right_sum_unique_othermaskentry) = 2 * ge_signed_half_sum_unique_othermaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_unique_othermaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_unique_othermaskentryrightvalue) = S ge_signed_half_sum_unique_othermaskentryrightvaluedecode))) /\ ((dst_positive_sum_unique_othermaskentryright) + ge_balance_negative_sum_unique_othermaskentryrightvalue = (dst_negative_sum_unique_othermaskentryright) + ge_balance_positive_sum_unique_othermaskentryrightvalue))))))))) /\ (exists sto_ap_sum_unique_othermaskentryproduct sto_an_sum_unique_othermaskentryproduct sto_bp_sum_unique_othermaskentryproduct sto_bn_sum_unique_othermaskentryproduct sto_cp_sum_unique_othermaskentryproduct sto_cn_sum_unique_othermaskentryproduct. (((((dc_left_sum_unique_othermaskentry) = 2 * (sto_ap_sum_unique_othermaskentryproduct) /\ (sto_an_sum_unique_othermaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_othermaskentryproductleft. (((dc_left_sum_unique_othermaskentry) = 2 * ge_signed_half_sum_unique_othermaskentryproductleft + 1 /\ (sto_ap_sum_unique_othermaskentryproduct) = 0) /\ (sto_an_sum_unique_othermaskentryproduct) = S ge_signed_half_sum_unique_othermaskentryproductleft))) /\ ((((((dc_right_sum_unique_othermaskentry) = 2 * (sto_bp_sum_unique_othermaskentryproduct) /\ (sto_bn_sum_unique_othermaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_othermaskentryproductright. (((dc_right_sum_unique_othermaskentry) = 2 * ge_signed_half_sum_unique_othermaskentryproductright + 1 /\ (sto_bp_sum_unique_othermaskentryproduct) = 0) /\ (sto_bn_sum_unique_othermaskentryproduct) = S ge_signed_half_sum_unique_othermaskentryproductright))) /\ ((((((dc_value_sum_unique_othermask) = 2 * (sto_cp_sum_unique_othermaskentryproduct) /\ (sto_cn_sum_unique_othermaskentryproduct) = 0) \/ exists ge_signed_half_sum_unique_othermaskentryproductoutput. (((dc_value_sum_unique_othermask) = 2 * ge_signed_half_sum_unique_othermaskentryproductoutput + 1 /\ (sto_cp_sum_unique_othermaskentryproduct) = 0) /\ (sto_cn_sum_unique_othermaskentryproduct) = S ge_signed_half_sum_unique_othermaskentryproductoutput))) /\ ((sto_ap_sum_unique_othermaskentryproduct * sto_bp_sum_unique_othermaskentryproduct + sto_an_sum_unique_othermaskentryproduct * sto_bn_sum_unique_othermaskentryproduct) + sto_cn_sum_unique_othermaskentryproduct = (sto_ap_sum_unique_othermaskentryproduct * sto_bn_sum_unique_othermaskentryproduct + sto_an_sum_unique_othermaskentryproduct * sto_bp_sum_unique_othermaskentryproduct) + sto_cp_sum_unique_othermaskentryproduct))))))))))))))) \/ ((((dc_index_sum_unique_othermask)=0 \/ ~(exists pvs_factor_sum_unique_othermaskentrynondivisor. (n) = (dc_index_sum_unique_othermask) * pvs_factor_sum_unique_othermaskentrynondivisor)) /\ ((dc_value_sum_unique_othermask)=0))))))) /\ (exists dst_positive_code_sum_unique_otherfold dst_positive_scale_sum_unique_otherfold dst_negative_code_sum_unique_otherfold dst_negative_scale_sum_unique_otherfold dst_positive_sum_sum_unique_otherfold dst_negative_sum_sum_unique_otherfold. (((dc_mask_sum_unique_other) = (((((dst_positive_code_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold)) * S ((dst_positive_code_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold)) + ((dst_positive_scale_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold))) + (((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) * S ((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) + ((dst_negative_scale_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)))) * S ((((dst_positive_code_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold)) * S ((dst_positive_code_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold)) + ((dst_positive_scale_sum_unique_otherfold) + (dst_positive_scale_sum_unique_otherfold))) + (((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) * S ((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) + ((dst_negative_scale_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)))) + ((((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) * S ((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) + ((dst_negative_scale_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold))) + (((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) * S ((dst_negative_code_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)) + ((dst_negative_scale_sum_unique_otherfold) + (dst_negative_scale_sum_unique_otherfold)))))) /\ (((exists fs_u_dst_sum_unique_otherfoldpositive fs_v_dst_sum_unique_otherfoldpositive. ((((exists fs_h_dst_sum_unique_otherfoldpositive_body_start. fs_h_dst_sum_unique_otherfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_otherfoldpositive)) /\ exists fs_q_dst_sum_unique_otherfoldpositive_body_start. fs_u_dst_sum_unique_otherfoldpositive = fs_q_dst_sum_unique_otherfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_unique_otherfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_unique_otherfoldpositive_body_terminal. fs_h_dst_sum_unique_otherfoldpositive_body_terminal + S (dst_positive_sum_sum_unique_otherfold) = S ((S (S (n))) * fs_v_dst_sum_unique_otherfoldpositive)) /\ exists fs_q_dst_sum_unique_otherfoldpositive_body_terminal. fs_u_dst_sum_unique_otherfoldpositive = fs_q_dst_sum_unique_otherfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_otherfoldpositive) + (dst_positive_sum_sum_unique_otherfold))) /\ forall fs_i_dst_sum_unique_otherfoldpositive_body_steps. (exists fs_lt_dst_sum_unique_otherfoldpositive_body_steps_bound. fs_lt_dst_sum_unique_otherfoldpositive_body_steps_bound + S fs_i_dst_sum_unique_otherfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_unique_otherfoldpositive_body_steps fs_r_dst_sum_unique_otherfoldpositive_body_steps fs_s_dst_sum_unique_otherfoldpositive_body_steps. ((((exists fs_h_dst_sum_unique_otherfoldpositive_body_steps_summand. fs_h_dst_sum_unique_otherfoldpositive_body_steps_summand + S (fs_a_dst_sum_unique_otherfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * dst_positive_scale_sum_unique_otherfold)) /\ exists fs_q_dst_sum_unique_otherfoldpositive_body_steps_summand. dst_positive_code_sum_unique_otherfold = fs_q_dst_sum_unique_otherfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * dst_positive_scale_sum_unique_otherfold) + (fs_a_dst_sum_unique_otherfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_otherfoldpositive_body_steps_partial. fs_h_dst_sum_unique_otherfoldpositive_body_steps_partial + S (fs_r_dst_sum_unique_otherfoldpositive_body_steps) = S ((S (fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * fs_v_dst_sum_unique_otherfoldpositive)) /\ exists fs_q_dst_sum_unique_otherfoldpositive_body_steps_partial. fs_u_dst_sum_unique_otherfoldpositive = fs_q_dst_sum_unique_otherfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * fs_v_dst_sum_unique_otherfoldpositive) + (fs_r_dst_sum_unique_otherfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_unique_otherfoldpositive_body_steps_successor. fs_h_dst_sum_unique_otherfoldpositive_body_steps_successor + S (fs_s_dst_sum_unique_otherfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * fs_v_dst_sum_unique_otherfoldpositive)) /\ exists fs_q_dst_sum_unique_otherfoldpositive_body_steps_successor. fs_u_dst_sum_unique_otherfoldpositive = fs_q_dst_sum_unique_otherfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_unique_otherfoldpositive_body_steps)) * fs_v_dst_sum_unique_otherfoldpositive) + (fs_s_dst_sum_unique_otherfoldpositive_body_steps))) /\ fs_s_dst_sum_unique_otherfoldpositive_body_steps = fs_r_dst_sum_unique_otherfoldpositive_body_steps + fs_a_dst_sum_unique_otherfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_unique_otherfoldnegative fs_v_dst_sum_unique_otherfoldnegative. ((((exists fs_h_dst_sum_unique_otherfoldnegative_body_start. fs_h_dst_sum_unique_otherfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_unique_otherfoldnegative)) /\ exists fs_q_dst_sum_unique_otherfoldnegative_body_start. fs_u_dst_sum_unique_otherfoldnegative = fs_q_dst_sum_unique_otherfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_unique_otherfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_unique_otherfoldnegative_body_terminal. fs_h_dst_sum_unique_otherfoldnegative_body_terminal + S (dst_negative_sum_sum_unique_otherfold) = S ((S (S (n))) * fs_v_dst_sum_unique_otherfoldnegative)) /\ exists fs_q_dst_sum_unique_otherfoldnegative_body_terminal. fs_u_dst_sum_unique_otherfoldnegative = fs_q_dst_sum_unique_otherfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_unique_otherfoldnegative) + (dst_negative_sum_sum_unique_otherfold))) /\ forall fs_i_dst_sum_unique_otherfoldnegative_body_steps. (exists fs_lt_dst_sum_unique_otherfoldnegative_body_steps_bound. fs_lt_dst_sum_unique_otherfoldnegative_body_steps_bound + S fs_i_dst_sum_unique_otherfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_unique_otherfoldnegative_body_steps fs_r_dst_sum_unique_otherfoldnegative_body_steps fs_s_dst_sum_unique_otherfoldnegative_body_steps. ((((exists fs_h_dst_sum_unique_otherfoldnegative_body_steps_summand. fs_h_dst_sum_unique_otherfoldnegative_body_steps_summand + S (fs_a_dst_sum_unique_otherfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * dst_negative_scale_sum_unique_otherfold)) /\ exists fs_q_dst_sum_unique_otherfoldnegative_body_steps_summand. dst_negative_code_sum_unique_otherfold = fs_q_dst_sum_unique_otherfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * dst_negative_scale_sum_unique_otherfold) + (fs_a_dst_sum_unique_otherfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_otherfoldnegative_body_steps_partial. fs_h_dst_sum_unique_otherfoldnegative_body_steps_partial + S (fs_r_dst_sum_unique_otherfoldnegative_body_steps) = S ((S (fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * fs_v_dst_sum_unique_otherfoldnegative)) /\ exists fs_q_dst_sum_unique_otherfoldnegative_body_steps_partial. fs_u_dst_sum_unique_otherfoldnegative = fs_q_dst_sum_unique_otherfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * fs_v_dst_sum_unique_otherfoldnegative) + (fs_r_dst_sum_unique_otherfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_unique_otherfoldnegative_body_steps_successor. fs_h_dst_sum_unique_otherfoldnegative_body_steps_successor + S (fs_s_dst_sum_unique_otherfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * fs_v_dst_sum_unique_otherfoldnegative)) /\ exists fs_q_dst_sum_unique_otherfoldnegative_body_steps_successor. fs_u_dst_sum_unique_otherfoldnegative = fs_q_dst_sum_unique_otherfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_unique_otherfoldnegative_body_steps)) * fs_v_dst_sum_unique_otherfoldnegative) + (fs_s_dst_sum_unique_otherfoldnegative_body_steps))) /\ fs_s_dst_sum_unique_otherfoldnegative_body_steps = fs_r_dst_sum_unique_otherfoldnegative_body_steps + fs_a_dst_sum_unique_otherfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_unique_otherfoldresult ge_balance_negative_sum_unique_otherfoldresult. (((((w) = 2 * (ge_balance_positive_sum_unique_otherfoldresult) /\ (ge_balance_negative_sum_unique_otherfoldresult) = 0) \/ exists ge_signed_half_sum_unique_otherfoldresultdecode. (((w) = 2 * ge_signed_half_sum_unique_otherfoldresultdecode + 1 /\ (ge_balance_positive_sum_unique_otherfoldresult) = 0) /\ (ge_balance_negative_sum_unique_otherfoldresult) = S ge_signed_half_sum_unique_otherfoldresultdecode))) /\ ((dst_positive_sum_sum_unique_otherfold) + ge_balance_negative_sum_unique_otherfoldresult = (dst_negative_sum_sum_unique_otherfold) + ge_balance_positive_sum_unique_otherfoldresult))))))))))))) -> w=z