dirichlet_convolution_sum_swap

Exact expanded first-order arithmetic statement

forall N F G n z. (exists dst_positive_code_swap_left dst_positive_scale_swap_left dst_negative_code_swap_left dst_negative_scale_swap_left. (((F) = (((((dst_positive_code_swap_left) + (dst_positive_scale_swap_left)) * S ((dst_positive_code_swap_left) + (dst_positive_scale_swap_left)) + ((dst_positive_scale_swap_left) + (dst_positive_scale_swap_left))) + (((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) * S ((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) + ((dst_negative_scale_swap_left) + (dst_negative_scale_swap_left)))) * S ((((dst_positive_code_swap_left) + (dst_positive_scale_swap_left)) * S ((dst_positive_code_swap_left) + (dst_positive_scale_swap_left)) + ((dst_positive_scale_swap_left) + (dst_positive_scale_swap_left))) + (((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) * S ((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) + ((dst_negative_scale_swap_left) + (dst_negative_scale_swap_left)))) + ((((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) * S ((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) + ((dst_negative_scale_swap_left) + (dst_negative_scale_swap_left))) + (((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) * S ((dst_negative_code_swap_left) + (dst_negative_scale_swap_left)) + ((dst_negative_scale_swap_left) + (dst_negative_scale_swap_left)))))) /\ (forall dst_index_swap_left. (exists pvs_le_gap_swap_leftdomain. pvs_le_gap_swap_leftdomain + (dst_index_swap_left) = (N)) -> exists dst_positive_swap_left dst_negative_swap_left dst_value_swap_left. ((((exists ff_h_pvs_swap_leftentrypositive. ff_h_pvs_swap_leftentrypositive + S (dst_positive_swap_left) = S ((S (dst_index_swap_left)) * dst_positive_scale_swap_left)) /\ exists ff_q_pvs_swap_leftentrypositive. dst_positive_code_swap_left = ff_q_pvs_swap_leftentrypositive * S ((S (dst_index_swap_left)) * dst_positive_scale_swap_left) + (dst_positive_swap_left))) /\ (((((exists ff_h_pvs_swap_leftentrynegative. ff_h_pvs_swap_leftentrynegative + S (dst_negative_swap_left) = S ((S (dst_index_swap_left)) * dst_negative_scale_swap_left)) /\ exists ff_q_pvs_swap_leftentrynegative. dst_negative_code_swap_left = ff_q_pvs_swap_leftentrynegative * S ((S (dst_index_swap_left)) * dst_negative_scale_swap_left) + (dst_negative_swap_left))) /\ (exists ge_balance_positive_swap_leftentryvalue ge_balance_negative_swap_leftentryvalue. (((((dst_value_swap_left) = 2 * (ge_balance_positive_swap_leftentryvalue) /\ (ge_balance_negative_swap_leftentryvalue) = 0) \/ exists ge_signed_half_swap_leftentryvaluedecode. (((dst_value_swap_left) = 2 * ge_signed_half_swap_leftentryvaluedecode + 1 /\ (ge_balance_positive_swap_leftentryvalue) = 0) /\ (ge_balance_negative_swap_leftentryvalue) = S ge_signed_half_swap_leftentryvaluedecode))) /\ ((dst_positive_swap_left) + ge_balance_negative_swap_leftentryvalue = (dst_negative_swap_left) + ge_balance_positive_swap_leftentryvalue))))))))) -> (exists dst_positive_code_swap_right dst_positive_scale_swap_right dst_negative_code_swap_right dst_negative_scale_swap_right. (((G) = (((((dst_positive_code_swap_right) + (dst_positive_scale_swap_right)) * S ((dst_positive_code_swap_right) + (dst_positive_scale_swap_right)) + ((dst_positive_scale_swap_right) + (dst_positive_scale_swap_right))) + (((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) * S ((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) + ((dst_negative_scale_swap_right) + (dst_negative_scale_swap_right)))) * S ((((dst_positive_code_swap_right) + (dst_positive_scale_swap_right)) * S ((dst_positive_code_swap_right) + (dst_positive_scale_swap_right)) + ((dst_positive_scale_swap_right) + (dst_positive_scale_swap_right))) + (((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) * S ((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) + ((dst_negative_scale_swap_right) + (dst_negative_scale_swap_right)))) + ((((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) * S ((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) + ((dst_negative_scale_swap_right) + (dst_negative_scale_swap_right))) + (((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) * S ((dst_negative_code_swap_right) + (dst_negative_scale_swap_right)) + ((dst_negative_scale_swap_right) + (dst_negative_scale_swap_right)))))) /\ (forall dst_index_swap_right. (exists pvs_le_gap_swap_rightdomain. pvs_le_gap_swap_rightdomain + (dst_index_swap_right) = (N)) -> exists dst_positive_swap_right dst_negative_swap_right dst_value_swap_right. ((((exists ff_h_pvs_swap_rightentrypositive. ff_h_pvs_swap_rightentrypositive + S (dst_positive_swap_right) = S ((S (dst_index_swap_right)) * dst_positive_scale_swap_right)) /\ exists ff_q_pvs_swap_rightentrypositive. dst_positive_code_swap_right = ff_q_pvs_swap_rightentrypositive * S ((S (dst_index_swap_right)) * dst_positive_scale_swap_right) + (dst_positive_swap_right))) /\ (((((exists ff_h_pvs_swap_rightentrynegative. ff_h_pvs_swap_rightentrynegative + S (dst_negative_swap_right) = S ((S (dst_index_swap_right)) * dst_negative_scale_swap_right)) /\ exists ff_q_pvs_swap_rightentrynegative. dst_negative_code_swap_right = ff_q_pvs_swap_rightentrynegative * S ((S (dst_index_swap_right)) * dst_negative_scale_swap_right) + (dst_negative_swap_right))) /\ (exists ge_balance_positive_swap_rightentryvalue ge_balance_negative_swap_rightentryvalue. (((((dst_value_swap_right) = 2 * (ge_balance_positive_swap_rightentryvalue) /\ (ge_balance_negative_swap_rightentryvalue) = 0) \/ exists ge_signed_half_swap_rightentryvaluedecode. (((dst_value_swap_right) = 2 * ge_signed_half_swap_rightentryvaluedecode + 1 /\ (ge_balance_positive_swap_rightentryvalue) = 0) /\ (ge_balance_negative_swap_rightentryvalue) = S ge_signed_half_swap_rightentryvaluedecode))) /\ ((dst_positive_swap_right) + ge_balance_negative_swap_rightentryvalue = (dst_negative_swap_right) + ge_balance_positive_swap_rightentryvalue))))))))) -> (exists pvs_le_gap_swap_bound. pvs_le_gap_swap_bound + (n) = (N)) -> (((~((n)=0)) /\ (exists dc_mask_swap_given. ((((exists dst_positive_code_swap_givenmasktable dst_positive_scale_swap_givenmasktable dst_negative_code_swap_givenmasktable dst_negative_scale_swap_givenmasktable. (((dc_mask_swap_given) = (((((dst_positive_code_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable)) * S ((dst_positive_code_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable)) + ((dst_positive_scale_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable))) + (((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) * S ((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) + ((dst_negative_scale_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)))) * S ((((dst_positive_code_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable)) * S ((dst_positive_code_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable)) + ((dst_positive_scale_swap_givenmasktable) + (dst_positive_scale_swap_givenmasktable))) + (((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) * S ((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) + ((dst_negative_scale_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)))) + ((((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) * S ((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) + ((dst_negative_scale_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable))) + (((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) * S ((dst_negative_code_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)) + ((dst_negative_scale_swap_givenmasktable) + (dst_negative_scale_swap_givenmasktable)))))) /\ (forall dst_index_swap_givenmasktable. (exists pvs_le_gap_swap_givenmasktabledomain. pvs_le_gap_swap_givenmasktabledomain + (dst_index_swap_givenmasktable) = (n)) -> exists dst_positive_swap_givenmasktable dst_negative_swap_givenmasktable dst_value_swap_givenmasktable. ((((exists ff_h_pvs_swap_givenmasktableentrypositive. ff_h_pvs_swap_givenmasktableentrypositive + S (dst_positive_swap_givenmasktable) = S ((S (dst_index_swap_givenmasktable)) * dst_positive_scale_swap_givenmasktable)) /\ exists ff_q_pvs_swap_givenmasktableentrypositive. dst_positive_code_swap_givenmasktable = ff_q_pvs_swap_givenmasktableentrypositive * S ((S (dst_index_swap_givenmasktable)) * dst_positive_scale_swap_givenmasktable) + (dst_positive_swap_givenmasktable))) /\ (((((exists ff_h_pvs_swap_givenmasktableentrynegative. ff_h_pvs_swap_givenmasktableentrynegative + S (dst_negative_swap_givenmasktable) = S ((S (dst_index_swap_givenmasktable)) * dst_negative_scale_swap_givenmasktable)) /\ exists ff_q_pvs_swap_givenmasktableentrynegative. dst_negative_code_swap_givenmasktable = ff_q_pvs_swap_givenmasktableentrynegative * S ((S (dst_index_swap_givenmasktable)) * dst_negative_scale_swap_givenmasktable) + (dst_negative_swap_givenmasktable))) /\ (exists ge_balance_positive_swap_givenmasktableentryvalue ge_balance_negative_swap_givenmasktableentryvalue. (((((dst_value_swap_givenmasktable) = 2 * (ge_balance_positive_swap_givenmasktableentryvalue) /\ (ge_balance_negative_swap_givenmasktableentryvalue) = 0) \/ exists ge_signed_half_swap_givenmasktableentryvaluedecode. (((dst_value_swap_givenmasktable) = 2 * ge_signed_half_swap_givenmasktableentryvaluedecode + 1 /\ (ge_balance_positive_swap_givenmasktableentryvalue) = 0) /\ (ge_balance_negative_swap_givenmasktableentryvalue) = S ge_signed_half_swap_givenmasktableentryvaluedecode))) /\ ((dst_positive_swap_givenmasktable) + ge_balance_negative_swap_givenmasktableentryvalue = (dst_negative_swap_givenmasktable) + ge_balance_positive_swap_givenmasktableentryvalue))))))))) /\ (forall dc_index_swap_givenmask dc_value_swap_givenmask. (exists pvs_le_gap_swap_givenmaskdomain. pvs_le_gap_swap_givenmaskdomain + (dc_index_swap_givenmask) = (n)) -> (exists dst_positive_code_swap_givenmasklookup dst_positive_scale_swap_givenmasklookup dst_negative_code_swap_givenmasklookup dst_negative_scale_swap_givenmasklookup dst_positive_swap_givenmasklookup dst_negative_swap_givenmasklookup. (((dc_mask_swap_given) = (((((dst_positive_code_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup)) * S ((dst_positive_code_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup)) + ((dst_positive_scale_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup))) + (((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) * S ((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) + ((dst_negative_scale_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)))) * S ((((dst_positive_code_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup)) * S ((dst_positive_code_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup)) + ((dst_positive_scale_swap_givenmasklookup) + (dst_positive_scale_swap_givenmasklookup))) + (((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) * S ((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) + ((dst_negative_scale_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)))) + ((((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) * S ((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) + ((dst_negative_scale_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup))) + (((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) * S ((dst_negative_code_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)) + ((dst_negative_scale_swap_givenmasklookup) + (dst_negative_scale_swap_givenmasklookup)))))) /\ (((((exists ff_h_pvs_swap_givenmasklookuppositive. ff_h_pvs_swap_givenmasklookuppositive + S (dst_positive_swap_givenmasklookup) = S ((S (dc_index_swap_givenmask)) * dst_positive_scale_swap_givenmasklookup)) /\ exists ff_q_pvs_swap_givenmasklookuppositive. dst_positive_code_swap_givenmasklookup = ff_q_pvs_swap_givenmasklookuppositive * S ((S (dc_index_swap_givenmask)) * dst_positive_scale_swap_givenmasklookup) + (dst_positive_swap_givenmasklookup))) /\ (((((exists ff_h_pvs_swap_givenmasklookupnegative. ff_h_pvs_swap_givenmasklookupnegative + S (dst_negative_swap_givenmasklookup) = S ((S (dc_index_swap_givenmask)) * dst_negative_scale_swap_givenmasklookup)) /\ exists ff_q_pvs_swap_givenmasklookupnegative. dst_negative_code_swap_givenmasklookup = ff_q_pvs_swap_givenmasklookupnegative * S ((S (dc_index_swap_givenmask)) * dst_negative_scale_swap_givenmasklookup) + (dst_negative_swap_givenmasklookup))) /\ (exists ge_balance_positive_swap_givenmasklookupvalue ge_balance_negative_swap_givenmasklookupvalue. (((((dc_value_swap_givenmask) = 2 * (ge_balance_positive_swap_givenmasklookupvalue) /\ (ge_balance_negative_swap_givenmasklookupvalue) = 0) \/ exists ge_signed_half_swap_givenmasklookupvaluedecode. (((dc_value_swap_givenmask) = 2 * ge_signed_half_swap_givenmasklookupvaluedecode + 1 /\ (ge_balance_positive_swap_givenmasklookupvalue) = 0) /\ (ge_balance_negative_swap_givenmasklookupvalue) = S ge_signed_half_swap_givenmasklookupvaluedecode))) /\ ((dst_positive_swap_givenmasklookup) + ge_balance_negative_swap_givenmasklookupvalue = (dst_negative_swap_givenmasklookup) + ge_balance_positive_swap_givenmasklookupvalue))))))))) -> ((((~((dc_index_swap_givenmask)=0)) /\ (exists dc_quotient_swap_givenmaskentry dc_left_swap_givenmaskentry dc_right_swap_givenmaskentry. (((n)=(dc_index_swap_givenmask)*dc_quotient_swap_givenmaskentry) /\ (((exists dst_positive_code_swap_givenmaskentryleft dst_positive_scale_swap_givenmaskentryleft dst_negative_code_swap_givenmaskentryleft dst_negative_scale_swap_givenmaskentryleft dst_positive_swap_givenmaskentryleft dst_negative_swap_givenmaskentryleft. (((F) = (((((dst_positive_code_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft)) * S ((dst_positive_code_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft)) + ((dst_positive_scale_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft))) + (((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) * S ((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) + ((dst_negative_scale_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)))) * S ((((dst_positive_code_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft)) * S ((dst_positive_code_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft)) + ((dst_positive_scale_swap_givenmaskentryleft) + (dst_positive_scale_swap_givenmaskentryleft))) + (((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) * S ((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) + ((dst_negative_scale_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)))) + ((((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) * S ((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) + ((dst_negative_scale_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft))) + (((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) * S ((dst_negative_code_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)) + ((dst_negative_scale_swap_givenmaskentryleft) + (dst_negative_scale_swap_givenmaskentryleft)))))) /\ (((((exists ff_h_pvs_swap_givenmaskentryleftpositive. ff_h_pvs_swap_givenmaskentryleftpositive + S (dst_positive_swap_givenmaskentryleft) = S ((S (dc_index_swap_givenmask)) * dst_positive_scale_swap_givenmaskentryleft)) /\ exists ff_q_pvs_swap_givenmaskentryleftpositive. dst_positive_code_swap_givenmaskentryleft = ff_q_pvs_swap_givenmaskentryleftpositive * S ((S (dc_index_swap_givenmask)) * dst_positive_scale_swap_givenmaskentryleft) + (dst_positive_swap_givenmaskentryleft))) /\ (((((exists ff_h_pvs_swap_givenmaskentryleftnegative. ff_h_pvs_swap_givenmaskentryleftnegative + S (dst_negative_swap_givenmaskentryleft) = S ((S (dc_index_swap_givenmask)) * dst_negative_scale_swap_givenmaskentryleft)) /\ exists ff_q_pvs_swap_givenmaskentryleftnegative. dst_negative_code_swap_givenmaskentryleft = ff_q_pvs_swap_givenmaskentryleftnegative * S ((S (dc_index_swap_givenmask)) * dst_negative_scale_swap_givenmaskentryleft) + (dst_negative_swap_givenmaskentryleft))) /\ (exists ge_balance_positive_swap_givenmaskentryleftvalue ge_balance_negative_swap_givenmaskentryleftvalue. (((((dc_left_swap_givenmaskentry) = 2 * (ge_balance_positive_swap_givenmaskentryleftvalue) /\ (ge_balance_negative_swap_givenmaskentryleftvalue) = 0) \/ exists ge_signed_half_swap_givenmaskentryleftvaluedecode. (((dc_left_swap_givenmaskentry) = 2 * ge_signed_half_swap_givenmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_swap_givenmaskentryleftvalue) = 0) /\ (ge_balance_negative_swap_givenmaskentryleftvalue) = S ge_signed_half_swap_givenmaskentryleftvaluedecode))) /\ ((dst_positive_swap_givenmaskentryleft) + ge_balance_negative_swap_givenmaskentryleftvalue = (dst_negative_swap_givenmaskentryleft) + ge_balance_positive_swap_givenmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_swap_givenmaskentryright dst_positive_scale_swap_givenmaskentryright dst_negative_code_swap_givenmaskentryright dst_negative_scale_swap_givenmaskentryright dst_positive_swap_givenmaskentryright dst_negative_swap_givenmaskentryright. (((G) = (((((dst_positive_code_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright)) * S ((dst_positive_code_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright)) + ((dst_positive_scale_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright))) + (((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) * S ((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) + ((dst_negative_scale_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)))) * S ((((dst_positive_code_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright)) * S ((dst_positive_code_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright)) + ((dst_positive_scale_swap_givenmaskentryright) + (dst_positive_scale_swap_givenmaskentryright))) + (((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) * S ((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) + ((dst_negative_scale_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)))) + ((((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) * S ((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) + ((dst_negative_scale_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright))) + (((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) * S ((dst_negative_code_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)) + ((dst_negative_scale_swap_givenmaskentryright) + (dst_negative_scale_swap_givenmaskentryright)))))) /\ (((((exists ff_h_pvs_swap_givenmaskentryrightpositive. ff_h_pvs_swap_givenmaskentryrightpositive + S (dst_positive_swap_givenmaskentryright) = S ((S (dc_quotient_swap_givenmaskentry)) * dst_positive_scale_swap_givenmaskentryright)) /\ exists ff_q_pvs_swap_givenmaskentryrightpositive. dst_positive_code_swap_givenmaskentryright = ff_q_pvs_swap_givenmaskentryrightpositive * S ((S (dc_quotient_swap_givenmaskentry)) * dst_positive_scale_swap_givenmaskentryright) + (dst_positive_swap_givenmaskentryright))) /\ (((((exists ff_h_pvs_swap_givenmaskentryrightnegative. ff_h_pvs_swap_givenmaskentryrightnegative + S (dst_negative_swap_givenmaskentryright) = S ((S (dc_quotient_swap_givenmaskentry)) * dst_negative_scale_swap_givenmaskentryright)) /\ exists ff_q_pvs_swap_givenmaskentryrightnegative. dst_negative_code_swap_givenmaskentryright = ff_q_pvs_swap_givenmaskentryrightnegative * S ((S (dc_quotient_swap_givenmaskentry)) * dst_negative_scale_swap_givenmaskentryright) + (dst_negative_swap_givenmaskentryright))) /\ (exists ge_balance_positive_swap_givenmaskentryrightvalue ge_balance_negative_swap_givenmaskentryrightvalue. (((((dc_right_swap_givenmaskentry) = 2 * (ge_balance_positive_swap_givenmaskentryrightvalue) /\ (ge_balance_negative_swap_givenmaskentryrightvalue) = 0) \/ exists ge_signed_half_swap_givenmaskentryrightvaluedecode. (((dc_right_swap_givenmaskentry) = 2 * ge_signed_half_swap_givenmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_swap_givenmaskentryrightvalue) = 0) /\ (ge_balance_negative_swap_givenmaskentryrightvalue) = S ge_signed_half_swap_givenmaskentryrightvaluedecode))) /\ ((dst_positive_swap_givenmaskentryright) + ge_balance_negative_swap_givenmaskentryrightvalue = (dst_negative_swap_givenmaskentryright) + ge_balance_positive_swap_givenmaskentryrightvalue))))))))) /\ (exists sto_ap_swap_givenmaskentryproduct sto_an_swap_givenmaskentryproduct sto_bp_swap_givenmaskentryproduct sto_bn_swap_givenmaskentryproduct sto_cp_swap_givenmaskentryproduct sto_cn_swap_givenmaskentryproduct. (((((dc_left_swap_givenmaskentry) = 2 * (sto_ap_swap_givenmaskentryproduct) /\ (sto_an_swap_givenmaskentryproduct) = 0) \/ exists ge_signed_half_swap_givenmaskentryproductleft. (((dc_left_swap_givenmaskentry) = 2 * ge_signed_half_swap_givenmaskentryproductleft + 1 /\ (sto_ap_swap_givenmaskentryproduct) = 0) /\ (sto_an_swap_givenmaskentryproduct) = S ge_signed_half_swap_givenmaskentryproductleft))) /\ ((((((dc_right_swap_givenmaskentry) = 2 * (sto_bp_swap_givenmaskentryproduct) /\ (sto_bn_swap_givenmaskentryproduct) = 0) \/ exists ge_signed_half_swap_givenmaskentryproductright. (((dc_right_swap_givenmaskentry) = 2 * ge_signed_half_swap_givenmaskentryproductright + 1 /\ (sto_bp_swap_givenmaskentryproduct) = 0) /\ (sto_bn_swap_givenmaskentryproduct) = S ge_signed_half_swap_givenmaskentryproductright))) /\ ((((((dc_value_swap_givenmask) = 2 * (sto_cp_swap_givenmaskentryproduct) /\ (sto_cn_swap_givenmaskentryproduct) = 0) \/ exists ge_signed_half_swap_givenmaskentryproductoutput. (((dc_value_swap_givenmask) = 2 * ge_signed_half_swap_givenmaskentryproductoutput + 1 /\ (sto_cp_swap_givenmaskentryproduct) = 0) /\ (sto_cn_swap_givenmaskentryproduct) = S ge_signed_half_swap_givenmaskentryproductoutput))) /\ ((sto_ap_swap_givenmaskentryproduct * sto_bp_swap_givenmaskentryproduct + sto_an_swap_givenmaskentryproduct * sto_bn_swap_givenmaskentryproduct) + sto_cn_swap_givenmaskentryproduct = (sto_ap_swap_givenmaskentryproduct * sto_bn_swap_givenmaskentryproduct + sto_an_swap_givenmaskentryproduct * sto_bp_swap_givenmaskentryproduct) + sto_cp_swap_givenmaskentryproduct))))))))))))))) \/ ((((dc_index_swap_givenmask)=0 \/ ~(exists pvs_factor_swap_givenmaskentrynondivisor. (n) = (dc_index_swap_givenmask) * pvs_factor_swap_givenmaskentrynondivisor)) /\ ((dc_value_swap_givenmask)=0))))))) /\ (exists dst_positive_code_swap_givenfold dst_positive_scale_swap_givenfold dst_negative_code_swap_givenfold dst_negative_scale_swap_givenfold dst_positive_sum_swap_givenfold dst_negative_sum_swap_givenfold. (((dc_mask_swap_given) = (((((dst_positive_code_swap_givenfold) + (dst_positive_scale_swap_givenfold)) * S ((dst_positive_code_swap_givenfold) + (dst_positive_scale_swap_givenfold)) + ((dst_positive_scale_swap_givenfold) + (dst_positive_scale_swap_givenfold))) + (((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) * S ((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) + ((dst_negative_scale_swap_givenfold) + (dst_negative_scale_swap_givenfold)))) * S ((((dst_positive_code_swap_givenfold) + (dst_positive_scale_swap_givenfold)) * S ((dst_positive_code_swap_givenfold) + (dst_positive_scale_swap_givenfold)) + ((dst_positive_scale_swap_givenfold) + (dst_positive_scale_swap_givenfold))) + (((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) * S ((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) + ((dst_negative_scale_swap_givenfold) + (dst_negative_scale_swap_givenfold)))) + ((((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) * S ((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) + ((dst_negative_scale_swap_givenfold) + (dst_negative_scale_swap_givenfold))) + (((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) * S ((dst_negative_code_swap_givenfold) + (dst_negative_scale_swap_givenfold)) + ((dst_negative_scale_swap_givenfold) + (dst_negative_scale_swap_givenfold)))))) /\ (((exists fs_u_dst_swap_givenfoldpositive fs_v_dst_swap_givenfoldpositive. ((((exists fs_h_dst_swap_givenfoldpositive_body_start. fs_h_dst_swap_givenfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_swap_givenfoldpositive)) /\ exists fs_q_dst_swap_givenfoldpositive_body_start. fs_u_dst_swap_givenfoldpositive = fs_q_dst_swap_givenfoldpositive_body_start * S ((S (0)) * fs_v_dst_swap_givenfoldpositive) + (0))) /\ ((((exists fs_h_dst_swap_givenfoldpositive_body_terminal. fs_h_dst_swap_givenfoldpositive_body_terminal + S (dst_positive_sum_swap_givenfold) = S ((S (S (n))) * fs_v_dst_swap_givenfoldpositive)) /\ exists fs_q_dst_swap_givenfoldpositive_body_terminal. fs_u_dst_swap_givenfoldpositive = fs_q_dst_swap_givenfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_swap_givenfoldpositive) + (dst_positive_sum_swap_givenfold))) /\ forall fs_i_dst_swap_givenfoldpositive_body_steps. (exists fs_lt_dst_swap_givenfoldpositive_body_steps_bound. fs_lt_dst_swap_givenfoldpositive_body_steps_bound + S fs_i_dst_swap_givenfoldpositive_body_steps = S (n)) -> exists fs_a_dst_swap_givenfoldpositive_body_steps fs_r_dst_swap_givenfoldpositive_body_steps fs_s_dst_swap_givenfoldpositive_body_steps. ((((exists fs_h_dst_swap_givenfoldpositive_body_steps_summand. fs_h_dst_swap_givenfoldpositive_body_steps_summand + S (fs_a_dst_swap_givenfoldpositive_body_steps) = S ((S (fs_i_dst_swap_givenfoldpositive_body_steps)) * dst_positive_scale_swap_givenfold)) /\ exists fs_q_dst_swap_givenfoldpositive_body_steps_summand. dst_positive_code_swap_givenfold = fs_q_dst_swap_givenfoldpositive_body_steps_summand * S ((S (fs_i_dst_swap_givenfoldpositive_body_steps)) * dst_positive_scale_swap_givenfold) + (fs_a_dst_swap_givenfoldpositive_body_steps))) /\ ((((exists fs_h_dst_swap_givenfoldpositive_body_steps_partial. fs_h_dst_swap_givenfoldpositive_body_steps_partial + S (fs_r_dst_swap_givenfoldpositive_body_steps) = S ((S (fs_i_dst_swap_givenfoldpositive_body_steps)) * fs_v_dst_swap_givenfoldpositive)) /\ exists fs_q_dst_swap_givenfoldpositive_body_steps_partial. fs_u_dst_swap_givenfoldpositive = fs_q_dst_swap_givenfoldpositive_body_steps_partial * S ((S (fs_i_dst_swap_givenfoldpositive_body_steps)) * fs_v_dst_swap_givenfoldpositive) + (fs_r_dst_swap_givenfoldpositive_body_steps))) /\ ((((exists fs_h_dst_swap_givenfoldpositive_body_steps_successor. fs_h_dst_swap_givenfoldpositive_body_steps_successor + S (fs_s_dst_swap_givenfoldpositive_body_steps) = S ((S (S fs_i_dst_swap_givenfoldpositive_body_steps)) * fs_v_dst_swap_givenfoldpositive)) /\ exists fs_q_dst_swap_givenfoldpositive_body_steps_successor. fs_u_dst_swap_givenfoldpositive = fs_q_dst_swap_givenfoldpositive_body_steps_successor * S ((S (S fs_i_dst_swap_givenfoldpositive_body_steps)) * fs_v_dst_swap_givenfoldpositive) + (fs_s_dst_swap_givenfoldpositive_body_steps))) /\ fs_s_dst_swap_givenfoldpositive_body_steps = fs_r_dst_swap_givenfoldpositive_body_steps + fs_a_dst_swap_givenfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_swap_givenfoldnegative fs_v_dst_swap_givenfoldnegative. ((((exists fs_h_dst_swap_givenfoldnegative_body_start. fs_h_dst_swap_givenfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_swap_givenfoldnegative)) /\ exists fs_q_dst_swap_givenfoldnegative_body_start. fs_u_dst_swap_givenfoldnegative = fs_q_dst_swap_givenfoldnegative_body_start * S ((S (0)) * fs_v_dst_swap_givenfoldnegative) + (0))) /\ ((((exists fs_h_dst_swap_givenfoldnegative_body_terminal. fs_h_dst_swap_givenfoldnegative_body_terminal + S (dst_negative_sum_swap_givenfold) = S ((S (S (n))) * fs_v_dst_swap_givenfoldnegative)) /\ exists fs_q_dst_swap_givenfoldnegative_body_terminal. fs_u_dst_swap_givenfoldnegative = fs_q_dst_swap_givenfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_swap_givenfoldnegative) + (dst_negative_sum_swap_givenfold))) /\ forall fs_i_dst_swap_givenfoldnegative_body_steps. (exists fs_lt_dst_swap_givenfoldnegative_body_steps_bound. fs_lt_dst_swap_givenfoldnegative_body_steps_bound + S fs_i_dst_swap_givenfoldnegative_body_steps = S (n)) -> exists fs_a_dst_swap_givenfoldnegative_body_steps fs_r_dst_swap_givenfoldnegative_body_steps fs_s_dst_swap_givenfoldnegative_body_steps. ((((exists fs_h_dst_swap_givenfoldnegative_body_steps_summand. fs_h_dst_swap_givenfoldnegative_body_steps_summand + S (fs_a_dst_swap_givenfoldnegative_body_steps) = S ((S (fs_i_dst_swap_givenfoldnegative_body_steps)) * dst_negative_scale_swap_givenfold)) /\ exists fs_q_dst_swap_givenfoldnegative_body_steps_summand. dst_negative_code_swap_givenfold = fs_q_dst_swap_givenfoldnegative_body_steps_summand * S ((S (fs_i_dst_swap_givenfoldnegative_body_steps)) * dst_negative_scale_swap_givenfold) + (fs_a_dst_swap_givenfoldnegative_body_steps))) /\ ((((exists fs_h_dst_swap_givenfoldnegative_body_steps_partial. fs_h_dst_swap_givenfoldnegative_body_steps_partial + S (fs_r_dst_swap_givenfoldnegative_body_steps) = S ((S (fs_i_dst_swap_givenfoldnegative_body_steps)) * fs_v_dst_swap_givenfoldnegative)) /\ exists fs_q_dst_swap_givenfoldnegative_body_steps_partial. fs_u_dst_swap_givenfoldnegative = fs_q_dst_swap_givenfoldnegative_body_steps_partial * S ((S (fs_i_dst_swap_givenfoldnegative_body_steps)) * fs_v_dst_swap_givenfoldnegative) + (fs_r_dst_swap_givenfoldnegative_body_steps))) /\ ((((exists fs_h_dst_swap_givenfoldnegative_body_steps_successor. fs_h_dst_swap_givenfoldnegative_body_steps_successor + S (fs_s_dst_swap_givenfoldnegative_body_steps) = S ((S (S fs_i_dst_swap_givenfoldnegative_body_steps)) * fs_v_dst_swap_givenfoldnegative)) /\ exists fs_q_dst_swap_givenfoldnegative_body_steps_successor. fs_u_dst_swap_givenfoldnegative = fs_q_dst_swap_givenfoldnegative_body_steps_successor * S ((S (S fs_i_dst_swap_givenfoldnegative_body_steps)) * fs_v_dst_swap_givenfoldnegative) + (fs_s_dst_swap_givenfoldnegative_body_steps))) /\ fs_s_dst_swap_givenfoldnegative_body_steps = fs_r_dst_swap_givenfoldnegative_body_steps + fs_a_dst_swap_givenfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_swap_givenfoldresult ge_balance_negative_swap_givenfoldresult. (((((z) = 2 * (ge_balance_positive_swap_givenfoldresult) /\ (ge_balance_negative_swap_givenfoldresult) = 0) \/ exists ge_signed_half_swap_givenfoldresultdecode. (((z) = 2 * ge_signed_half_swap_givenfoldresultdecode + 1 /\ (ge_balance_positive_swap_givenfoldresult) = 0) /\ (ge_balance_negative_swap_givenfoldresult) = S ge_signed_half_swap_givenfoldresultdecode))) /\ ((dst_positive_sum_swap_givenfold) + ge_balance_negative_swap_givenfoldresult = (dst_negative_sum_swap_givenfold) + ge_balance_positive_swap_givenfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_swap_result. ((((exists dst_positive_code_swap_resultmasktable dst_positive_scale_swap_resultmasktable dst_negative_code_swap_resultmasktable dst_negative_scale_swap_resultmasktable. (((dc_mask_swap_result) = (((((dst_positive_code_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable)) * S ((dst_positive_code_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable)) + ((dst_positive_scale_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable))) + (((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) * S ((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) + ((dst_negative_scale_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)))) * S ((((dst_positive_code_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable)) * S ((dst_positive_code_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable)) + ((dst_positive_scale_swap_resultmasktable) + (dst_positive_scale_swap_resultmasktable))) + (((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) * S ((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) + ((dst_negative_scale_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)))) + ((((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) * S ((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) + ((dst_negative_scale_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable))) + (((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) * S ((dst_negative_code_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)) + ((dst_negative_scale_swap_resultmasktable) + (dst_negative_scale_swap_resultmasktable)))))) /\ (forall dst_index_swap_resultmasktable. (exists pvs_le_gap_swap_resultmasktabledomain. pvs_le_gap_swap_resultmasktabledomain + (dst_index_swap_resultmasktable) = (n)) -> exists dst_positive_swap_resultmasktable dst_negative_swap_resultmasktable dst_value_swap_resultmasktable. ((((exists ff_h_pvs_swap_resultmasktableentrypositive. ff_h_pvs_swap_resultmasktableentrypositive + S (dst_positive_swap_resultmasktable) = S ((S (dst_index_swap_resultmasktable)) * dst_positive_scale_swap_resultmasktable)) /\ exists ff_q_pvs_swap_resultmasktableentrypositive. dst_positive_code_swap_resultmasktable = ff_q_pvs_swap_resultmasktableentrypositive * S ((S (dst_index_swap_resultmasktable)) * dst_positive_scale_swap_resultmasktable) + (dst_positive_swap_resultmasktable))) /\ (((((exists ff_h_pvs_swap_resultmasktableentrynegative. ff_h_pvs_swap_resultmasktableentrynegative + S (dst_negative_swap_resultmasktable) = S ((S (dst_index_swap_resultmasktable)) * dst_negative_scale_swap_resultmasktable)) /\ exists ff_q_pvs_swap_resultmasktableentrynegative. dst_negative_code_swap_resultmasktable = ff_q_pvs_swap_resultmasktableentrynegative * S ((S (dst_index_swap_resultmasktable)) * dst_negative_scale_swap_resultmasktable) + (dst_negative_swap_resultmasktable))) /\ (exists ge_balance_positive_swap_resultmasktableentryvalue ge_balance_negative_swap_resultmasktableentryvalue. (((((dst_value_swap_resultmasktable) = 2 * (ge_balance_positive_swap_resultmasktableentryvalue) /\ (ge_balance_negative_swap_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_swap_resultmasktableentryvaluedecode. (((dst_value_swap_resultmasktable) = 2 * ge_signed_half_swap_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_swap_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_swap_resultmasktableentryvalue) = S ge_signed_half_swap_resultmasktableentryvaluedecode))) /\ ((dst_positive_swap_resultmasktable) + ge_balance_negative_swap_resultmasktableentryvalue = (dst_negative_swap_resultmasktable) + ge_balance_positive_swap_resultmasktableentryvalue))))))))) /\ (forall dc_index_swap_resultmask dc_value_swap_resultmask. (exists pvs_le_gap_swap_resultmaskdomain. pvs_le_gap_swap_resultmaskdomain + (dc_index_swap_resultmask) = (n)) -> (exists dst_positive_code_swap_resultmasklookup dst_positive_scale_swap_resultmasklookup dst_negative_code_swap_resultmasklookup dst_negative_scale_swap_resultmasklookup dst_positive_swap_resultmasklookup dst_negative_swap_resultmasklookup. (((dc_mask_swap_result) = (((((dst_positive_code_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup)) * S ((dst_positive_code_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup)) + ((dst_positive_scale_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup))) + (((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) * S ((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) + ((dst_negative_scale_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)))) * S ((((dst_positive_code_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup)) * S ((dst_positive_code_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup)) + ((dst_positive_scale_swap_resultmasklookup) + (dst_positive_scale_swap_resultmasklookup))) + (((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) * S ((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) + ((dst_negative_scale_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)))) + ((((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) * S ((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) + ((dst_negative_scale_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup))) + (((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) * S ((dst_negative_code_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)) + ((dst_negative_scale_swap_resultmasklookup) + (dst_negative_scale_swap_resultmasklookup)))))) /\ (((((exists ff_h_pvs_swap_resultmasklookuppositive. ff_h_pvs_swap_resultmasklookuppositive + S (dst_positive_swap_resultmasklookup) = S ((S (dc_index_swap_resultmask)) * dst_positive_scale_swap_resultmasklookup)) /\ exists ff_q_pvs_swap_resultmasklookuppositive. dst_positive_code_swap_resultmasklookup = ff_q_pvs_swap_resultmasklookuppositive * S ((S (dc_index_swap_resultmask)) * dst_positive_scale_swap_resultmasklookup) + (dst_positive_swap_resultmasklookup))) /\ (((((exists ff_h_pvs_swap_resultmasklookupnegative. ff_h_pvs_swap_resultmasklookupnegative + S (dst_negative_swap_resultmasklookup) = S ((S (dc_index_swap_resultmask)) * dst_negative_scale_swap_resultmasklookup)) /\ exists ff_q_pvs_swap_resultmasklookupnegative. dst_negative_code_swap_resultmasklookup = ff_q_pvs_swap_resultmasklookupnegative * S ((S (dc_index_swap_resultmask)) * dst_negative_scale_swap_resultmasklookup) + (dst_negative_swap_resultmasklookup))) /\ (exists ge_balance_positive_swap_resultmasklookupvalue ge_balance_negative_swap_resultmasklookupvalue. (((((dc_value_swap_resultmask) = 2 * (ge_balance_positive_swap_resultmasklookupvalue) /\ (ge_balance_negative_swap_resultmasklookupvalue) = 0) \/ exists ge_signed_half_swap_resultmasklookupvaluedecode. (((dc_value_swap_resultmask) = 2 * ge_signed_half_swap_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_swap_resultmasklookupvalue) = 0) /\ (ge_balance_negative_swap_resultmasklookupvalue) = S ge_signed_half_swap_resultmasklookupvaluedecode))) /\ ((dst_positive_swap_resultmasklookup) + ge_balance_negative_swap_resultmasklookupvalue = (dst_negative_swap_resultmasklookup) + ge_balance_positive_swap_resultmasklookupvalue))))))))) -> ((((~((dc_index_swap_resultmask)=0)) /\ (exists dc_quotient_swap_resultmaskentry dc_left_swap_resultmaskentry dc_right_swap_resultmaskentry. (((n)=(dc_index_swap_resultmask)*dc_quotient_swap_resultmaskentry) /\ (((exists dst_positive_code_swap_resultmaskentryleft dst_positive_scale_swap_resultmaskentryleft dst_negative_code_swap_resultmaskentryleft dst_negative_scale_swap_resultmaskentryleft dst_positive_swap_resultmaskentryleft dst_negative_swap_resultmaskentryleft. (((G) = (((((dst_positive_code_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft)) * S ((dst_positive_code_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft)) + ((dst_positive_scale_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft))) + (((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) * S ((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) + ((dst_negative_scale_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)))) * S ((((dst_positive_code_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft)) * S ((dst_positive_code_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft)) + ((dst_positive_scale_swap_resultmaskentryleft) + (dst_positive_scale_swap_resultmaskentryleft))) + (((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) * S ((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) + ((dst_negative_scale_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)))) + ((((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) * S ((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) + ((dst_negative_scale_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft))) + (((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) * S ((dst_negative_code_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)) + ((dst_negative_scale_swap_resultmaskentryleft) + (dst_negative_scale_swap_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_swap_resultmaskentryleftpositive. ff_h_pvs_swap_resultmaskentryleftpositive + S (dst_positive_swap_resultmaskentryleft) = S ((S (dc_index_swap_resultmask)) * dst_positive_scale_swap_resultmaskentryleft)) /\ exists ff_q_pvs_swap_resultmaskentryleftpositive. dst_positive_code_swap_resultmaskentryleft = ff_q_pvs_swap_resultmaskentryleftpositive * S ((S (dc_index_swap_resultmask)) * dst_positive_scale_swap_resultmaskentryleft) + (dst_positive_swap_resultmaskentryleft))) /\ (((((exists ff_h_pvs_swap_resultmaskentryleftnegative. ff_h_pvs_swap_resultmaskentryleftnegative + S (dst_negative_swap_resultmaskentryleft) = S ((S (dc_index_swap_resultmask)) * dst_negative_scale_swap_resultmaskentryleft)) /\ exists ff_q_pvs_swap_resultmaskentryleftnegative. dst_negative_code_swap_resultmaskentryleft = ff_q_pvs_swap_resultmaskentryleftnegative * S ((S (dc_index_swap_resultmask)) * dst_negative_scale_swap_resultmaskentryleft) + (dst_negative_swap_resultmaskentryleft))) /\ (exists ge_balance_positive_swap_resultmaskentryleftvalue ge_balance_negative_swap_resultmaskentryleftvalue. (((((dc_left_swap_resultmaskentry) = 2 * (ge_balance_positive_swap_resultmaskentryleftvalue) /\ (ge_balance_negative_swap_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_swap_resultmaskentryleftvaluedecode. (((dc_left_swap_resultmaskentry) = 2 * ge_signed_half_swap_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_swap_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_swap_resultmaskentryleftvalue) = S ge_signed_half_swap_resultmaskentryleftvaluedecode))) /\ ((dst_positive_swap_resultmaskentryleft) + ge_balance_negative_swap_resultmaskentryleftvalue = (dst_negative_swap_resultmaskentryleft) + ge_balance_positive_swap_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_swap_resultmaskentryright dst_positive_scale_swap_resultmaskentryright dst_negative_code_swap_resultmaskentryright dst_negative_scale_swap_resultmaskentryright dst_positive_swap_resultmaskentryright dst_negative_swap_resultmaskentryright. (((F) = (((((dst_positive_code_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright)) * S ((dst_positive_code_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright)) + ((dst_positive_scale_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright))) + (((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) * S ((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) + ((dst_negative_scale_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)))) * S ((((dst_positive_code_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright)) * S ((dst_positive_code_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright)) + ((dst_positive_scale_swap_resultmaskentryright) + (dst_positive_scale_swap_resultmaskentryright))) + (((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) * S ((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) + ((dst_negative_scale_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)))) + ((((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) * S ((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) + ((dst_negative_scale_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright))) + (((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) * S ((dst_negative_code_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)) + ((dst_negative_scale_swap_resultmaskentryright) + (dst_negative_scale_swap_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_swap_resultmaskentryrightpositive. ff_h_pvs_swap_resultmaskentryrightpositive + S (dst_positive_swap_resultmaskentryright) = S ((S (dc_quotient_swap_resultmaskentry)) * dst_positive_scale_swap_resultmaskentryright)) /\ exists ff_q_pvs_swap_resultmaskentryrightpositive. dst_positive_code_swap_resultmaskentryright = ff_q_pvs_swap_resultmaskentryrightpositive * S ((S (dc_quotient_swap_resultmaskentry)) * dst_positive_scale_swap_resultmaskentryright) + (dst_positive_swap_resultmaskentryright))) /\ (((((exists ff_h_pvs_swap_resultmaskentryrightnegative. ff_h_pvs_swap_resultmaskentryrightnegative + S (dst_negative_swap_resultmaskentryright) = S ((S (dc_quotient_swap_resultmaskentry)) * dst_negative_scale_swap_resultmaskentryright)) /\ exists ff_q_pvs_swap_resultmaskentryrightnegative. dst_negative_code_swap_resultmaskentryright = ff_q_pvs_swap_resultmaskentryrightnegative * S ((S (dc_quotient_swap_resultmaskentry)) * dst_negative_scale_swap_resultmaskentryright) + (dst_negative_swap_resultmaskentryright))) /\ (exists ge_balance_positive_swap_resultmaskentryrightvalue ge_balance_negative_swap_resultmaskentryrightvalue. (((((dc_right_swap_resultmaskentry) = 2 * (ge_balance_positive_swap_resultmaskentryrightvalue) /\ (ge_balance_negative_swap_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_swap_resultmaskentryrightvaluedecode. (((dc_right_swap_resultmaskentry) = 2 * ge_signed_half_swap_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_swap_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_swap_resultmaskentryrightvalue) = S ge_signed_half_swap_resultmaskentryrightvaluedecode))) /\ ((dst_positive_swap_resultmaskentryright) + ge_balance_negative_swap_resultmaskentryrightvalue = (dst_negative_swap_resultmaskentryright) + ge_balance_positive_swap_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_swap_resultmaskentryproduct sto_an_swap_resultmaskentryproduct sto_bp_swap_resultmaskentryproduct sto_bn_swap_resultmaskentryproduct sto_cp_swap_resultmaskentryproduct sto_cn_swap_resultmaskentryproduct. (((((dc_left_swap_resultmaskentry) = 2 * (sto_ap_swap_resultmaskentryproduct) /\ (sto_an_swap_resultmaskentryproduct) = 0) \/ exists ge_signed_half_swap_resultmaskentryproductleft. (((dc_left_swap_resultmaskentry) = 2 * ge_signed_half_swap_resultmaskentryproductleft + 1 /\ (sto_ap_swap_resultmaskentryproduct) = 0) /\ (sto_an_swap_resultmaskentryproduct) = S ge_signed_half_swap_resultmaskentryproductleft))) /\ ((((((dc_right_swap_resultmaskentry) = 2 * (sto_bp_swap_resultmaskentryproduct) /\ (sto_bn_swap_resultmaskentryproduct) = 0) \/ exists ge_signed_half_swap_resultmaskentryproductright. (((dc_right_swap_resultmaskentry) = 2 * ge_signed_half_swap_resultmaskentryproductright + 1 /\ (sto_bp_swap_resultmaskentryproduct) = 0) /\ (sto_bn_swap_resultmaskentryproduct) = S ge_signed_half_swap_resultmaskentryproductright))) /\ ((((((dc_value_swap_resultmask) = 2 * (sto_cp_swap_resultmaskentryproduct) /\ (sto_cn_swap_resultmaskentryproduct) = 0) \/ exists ge_signed_half_swap_resultmaskentryproductoutput. (((dc_value_swap_resultmask) = 2 * ge_signed_half_swap_resultmaskentryproductoutput + 1 /\ (sto_cp_swap_resultmaskentryproduct) = 0) /\ (sto_cn_swap_resultmaskentryproduct) = S ge_signed_half_swap_resultmaskentryproductoutput))) /\ ((sto_ap_swap_resultmaskentryproduct * sto_bp_swap_resultmaskentryproduct + sto_an_swap_resultmaskentryproduct * sto_bn_swap_resultmaskentryproduct) + sto_cn_swap_resultmaskentryproduct = (sto_ap_swap_resultmaskentryproduct * sto_bn_swap_resultmaskentryproduct + sto_an_swap_resultmaskentryproduct * sto_bp_swap_resultmaskentryproduct) + sto_cp_swap_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_swap_resultmask)=0 \/ ~(exists pvs_factor_swap_resultmaskentrynondivisor. (n) = (dc_index_swap_resultmask) * pvs_factor_swap_resultmaskentrynondivisor)) /\ ((dc_value_swap_resultmask)=0))))))) /\ (exists dst_positive_code_swap_resultfold dst_positive_scale_swap_resultfold dst_negative_code_swap_resultfold dst_negative_scale_swap_resultfold dst_positive_sum_swap_resultfold dst_negative_sum_swap_resultfold. (((dc_mask_swap_result) = (((((dst_positive_code_swap_resultfold) + (dst_positive_scale_swap_resultfold)) * S ((dst_positive_code_swap_resultfold) + (dst_positive_scale_swap_resultfold)) + ((dst_positive_scale_swap_resultfold) + (dst_positive_scale_swap_resultfold))) + (((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) * S ((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) + ((dst_negative_scale_swap_resultfold) + (dst_negative_scale_swap_resultfold)))) * S ((((dst_positive_code_swap_resultfold) + (dst_positive_scale_swap_resultfold)) * S ((dst_positive_code_swap_resultfold) + (dst_positive_scale_swap_resultfold)) + ((dst_positive_scale_swap_resultfold) + (dst_positive_scale_swap_resultfold))) + (((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) * S ((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) + ((dst_negative_scale_swap_resultfold) + (dst_negative_scale_swap_resultfold)))) + ((((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) * S ((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) + ((dst_negative_scale_swap_resultfold) + (dst_negative_scale_swap_resultfold))) + (((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) * S ((dst_negative_code_swap_resultfold) + (dst_negative_scale_swap_resultfold)) + ((dst_negative_scale_swap_resultfold) + (dst_negative_scale_swap_resultfold)))))) /\ (((exists fs_u_dst_swap_resultfoldpositive fs_v_dst_swap_resultfoldpositive. ((((exists fs_h_dst_swap_resultfoldpositive_body_start. fs_h_dst_swap_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_swap_resultfoldpositive)) /\ exists fs_q_dst_swap_resultfoldpositive_body_start. fs_u_dst_swap_resultfoldpositive = fs_q_dst_swap_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_swap_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_swap_resultfoldpositive_body_terminal. fs_h_dst_swap_resultfoldpositive_body_terminal + S (dst_positive_sum_swap_resultfold) = S ((S (S (n))) * fs_v_dst_swap_resultfoldpositive)) /\ exists fs_q_dst_swap_resultfoldpositive_body_terminal. fs_u_dst_swap_resultfoldpositive = fs_q_dst_swap_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_swap_resultfoldpositive) + (dst_positive_sum_swap_resultfold))) /\ forall fs_i_dst_swap_resultfoldpositive_body_steps. (exists fs_lt_dst_swap_resultfoldpositive_body_steps_bound. fs_lt_dst_swap_resultfoldpositive_body_steps_bound + S fs_i_dst_swap_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_swap_resultfoldpositive_body_steps fs_r_dst_swap_resultfoldpositive_body_steps fs_s_dst_swap_resultfoldpositive_body_steps. ((((exists fs_h_dst_swap_resultfoldpositive_body_steps_summand. fs_h_dst_swap_resultfoldpositive_body_steps_summand + S (fs_a_dst_swap_resultfoldpositive_body_steps) = S ((S (fs_i_dst_swap_resultfoldpositive_body_steps)) * dst_positive_scale_swap_resultfold)) /\ exists fs_q_dst_swap_resultfoldpositive_body_steps_summand. dst_positive_code_swap_resultfold = fs_q_dst_swap_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_swap_resultfoldpositive_body_steps)) * dst_positive_scale_swap_resultfold) + (fs_a_dst_swap_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_swap_resultfoldpositive_body_steps_partial. fs_h_dst_swap_resultfoldpositive_body_steps_partial + S (fs_r_dst_swap_resultfoldpositive_body_steps) = S ((S (fs_i_dst_swap_resultfoldpositive_body_steps)) * fs_v_dst_swap_resultfoldpositive)) /\ exists fs_q_dst_swap_resultfoldpositive_body_steps_partial. fs_u_dst_swap_resultfoldpositive = fs_q_dst_swap_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_swap_resultfoldpositive_body_steps)) * fs_v_dst_swap_resultfoldpositive) + (fs_r_dst_swap_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_swap_resultfoldpositive_body_steps_successor. fs_h_dst_swap_resultfoldpositive_body_steps_successor + S (fs_s_dst_swap_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_swap_resultfoldpositive_body_steps)) * fs_v_dst_swap_resultfoldpositive)) /\ exists fs_q_dst_swap_resultfoldpositive_body_steps_successor. fs_u_dst_swap_resultfoldpositive = fs_q_dst_swap_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_swap_resultfoldpositive_body_steps)) * fs_v_dst_swap_resultfoldpositive) + (fs_s_dst_swap_resultfoldpositive_body_steps))) /\ fs_s_dst_swap_resultfoldpositive_body_steps = fs_r_dst_swap_resultfoldpositive_body_steps + fs_a_dst_swap_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_swap_resultfoldnegative fs_v_dst_swap_resultfoldnegative. ((((exists fs_h_dst_swap_resultfoldnegative_body_start. fs_h_dst_swap_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_swap_resultfoldnegative)) /\ exists fs_q_dst_swap_resultfoldnegative_body_start. fs_u_dst_swap_resultfoldnegative = fs_q_dst_swap_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_swap_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_swap_resultfoldnegative_body_terminal. fs_h_dst_swap_resultfoldnegative_body_terminal + S (dst_negative_sum_swap_resultfold) = S ((S (S (n))) * fs_v_dst_swap_resultfoldnegative)) /\ exists fs_q_dst_swap_resultfoldnegative_body_terminal. fs_u_dst_swap_resultfoldnegative = fs_q_dst_swap_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_swap_resultfoldnegative) + (dst_negative_sum_swap_resultfold))) /\ forall fs_i_dst_swap_resultfoldnegative_body_steps. (exists fs_lt_dst_swap_resultfoldnegative_body_steps_bound. fs_lt_dst_swap_resultfoldnegative_body_steps_bound + S fs_i_dst_swap_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_swap_resultfoldnegative_body_steps fs_r_dst_swap_resultfoldnegative_body_steps fs_s_dst_swap_resultfoldnegative_body_steps. ((((exists fs_h_dst_swap_resultfoldnegative_body_steps_summand. fs_h_dst_swap_resultfoldnegative_body_steps_summand + S (fs_a_dst_swap_resultfoldnegative_body_steps) = S ((S (fs_i_dst_swap_resultfoldnegative_body_steps)) * dst_negative_scale_swap_resultfold)) /\ exists fs_q_dst_swap_resultfoldnegative_body_steps_summand. dst_negative_code_swap_resultfold = fs_q_dst_swap_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_swap_resultfoldnegative_body_steps)) * dst_negative_scale_swap_resultfold) + (fs_a_dst_swap_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_swap_resultfoldnegative_body_steps_partial. fs_h_dst_swap_resultfoldnegative_body_steps_partial + S (fs_r_dst_swap_resultfoldnegative_body_steps) = S ((S (fs_i_dst_swap_resultfoldnegative_body_steps)) * fs_v_dst_swap_resultfoldnegative)) /\ exists fs_q_dst_swap_resultfoldnegative_body_steps_partial. fs_u_dst_swap_resultfoldnegative = fs_q_dst_swap_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_swap_resultfoldnegative_body_steps)) * fs_v_dst_swap_resultfoldnegative) + (fs_r_dst_swap_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_swap_resultfoldnegative_body_steps_successor. fs_h_dst_swap_resultfoldnegative_body_steps_successor + S (fs_s_dst_swap_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_swap_resultfoldnegative_body_steps)) * fs_v_dst_swap_resultfoldnegative)) /\ exists fs_q_dst_swap_resultfoldnegative_body_steps_successor. fs_u_dst_swap_resultfoldnegative = fs_q_dst_swap_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_swap_resultfoldnegative_body_steps)) * fs_v_dst_swap_resultfoldnegative) + (fs_s_dst_swap_resultfoldnegative_body_steps))) /\ fs_s_dst_swap_resultfoldnegative_body_steps = fs_r_dst_swap_resultfoldnegative_body_steps + fs_a_dst_swap_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_swap_resultfoldresult ge_balance_negative_swap_resultfoldresult. (((((z) = 2 * (ge_balance_positive_swap_resultfoldresult) /\ (ge_balance_negative_swap_resultfoldresult) = 0) \/ exists ge_signed_half_swap_resultfoldresultdecode. (((z) = 2 * ge_signed_half_swap_resultfoldresultdecode + 1 /\ (ge_balance_positive_swap_resultfoldresult) = 0) /\ (ge_balance_negative_swap_resultfoldresult) = S ge_signed_half_swap_resultfoldresultdecode))) /\ ((dst_positive_sum_swap_resultfold) + ge_balance_negative_swap_resultfoldresult = (dst_negative_sum_swap_resultfold) + ge_balance_positive_swap_resultfoldresult)))))))))))))