dirichlet_convolution_positive_source_transport

Exact expanded first-order arithmetic statement

forall N F G H K n z. (exists dst_positive_code_transport_left dst_positive_scale_transport_left dst_negative_code_transport_left dst_negative_scale_transport_left. (((H) = (((((dst_positive_code_transport_left) + (dst_positive_scale_transport_left)) * S ((dst_positive_code_transport_left) + (dst_positive_scale_transport_left)) + ((dst_positive_scale_transport_left) + (dst_positive_scale_transport_left))) + (((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) * S ((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) + ((dst_negative_scale_transport_left) + (dst_negative_scale_transport_left)))) * S ((((dst_positive_code_transport_left) + (dst_positive_scale_transport_left)) * S ((dst_positive_code_transport_left) + (dst_positive_scale_transport_left)) + ((dst_positive_scale_transport_left) + (dst_positive_scale_transport_left))) + (((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) * S ((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) + ((dst_negative_scale_transport_left) + (dst_negative_scale_transport_left)))) + ((((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) * S ((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) + ((dst_negative_scale_transport_left) + (dst_negative_scale_transport_left))) + (((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) * S ((dst_negative_code_transport_left) + (dst_negative_scale_transport_left)) + ((dst_negative_scale_transport_left) + (dst_negative_scale_transport_left)))))) /\ (forall dst_index_transport_left. (exists pvs_le_gap_transport_leftdomain. pvs_le_gap_transport_leftdomain + (dst_index_transport_left) = (N)) -> exists dst_positive_transport_left dst_negative_transport_left dst_value_transport_left. ((((exists ff_h_pvs_transport_leftentrypositive. ff_h_pvs_transport_leftentrypositive + S (dst_positive_transport_left) = S ((S (dst_index_transport_left)) * dst_positive_scale_transport_left)) /\ exists ff_q_pvs_transport_leftentrypositive. dst_positive_code_transport_left = ff_q_pvs_transport_leftentrypositive * S ((S (dst_index_transport_left)) * dst_positive_scale_transport_left) + (dst_positive_transport_left))) /\ (((((exists ff_h_pvs_transport_leftentrynegative. ff_h_pvs_transport_leftentrynegative + S (dst_negative_transport_left) = S ((S (dst_index_transport_left)) * dst_negative_scale_transport_left)) /\ exists ff_q_pvs_transport_leftentrynegative. dst_negative_code_transport_left = ff_q_pvs_transport_leftentrynegative * S ((S (dst_index_transport_left)) * dst_negative_scale_transport_left) + (dst_negative_transport_left))) /\ (exists ge_balance_positive_transport_leftentryvalue ge_balance_negative_transport_leftentryvalue. (((((dst_value_transport_left) = 2 * (ge_balance_positive_transport_leftentryvalue) /\ (ge_balance_negative_transport_leftentryvalue) = 0) \/ exists ge_signed_half_transport_leftentryvaluedecode. (((dst_value_transport_left) = 2 * ge_signed_half_transport_leftentryvaluedecode + 1 /\ (ge_balance_positive_transport_leftentryvalue) = 0) /\ (ge_balance_negative_transport_leftentryvalue) = S ge_signed_half_transport_leftentryvaluedecode))) /\ ((dst_positive_transport_left) + ge_balance_negative_transport_leftentryvalue = (dst_negative_transport_left) + ge_balance_positive_transport_leftentryvalue))))))))) -> (exists dst_positive_code_transport_right dst_positive_scale_transport_right dst_negative_code_transport_right dst_negative_scale_transport_right. (((K) = (((((dst_positive_code_transport_right) + (dst_positive_scale_transport_right)) * S ((dst_positive_code_transport_right) + (dst_positive_scale_transport_right)) + ((dst_positive_scale_transport_right) + (dst_positive_scale_transport_right))) + (((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) * S ((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) + ((dst_negative_scale_transport_right) + (dst_negative_scale_transport_right)))) * S ((((dst_positive_code_transport_right) + (dst_positive_scale_transport_right)) * S ((dst_positive_code_transport_right) + (dst_positive_scale_transport_right)) + ((dst_positive_scale_transport_right) + (dst_positive_scale_transport_right))) + (((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) * S ((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) + ((dst_negative_scale_transport_right) + (dst_negative_scale_transport_right)))) + ((((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) * S ((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) + ((dst_negative_scale_transport_right) + (dst_negative_scale_transport_right))) + (((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) * S ((dst_negative_code_transport_right) + (dst_negative_scale_transport_right)) + ((dst_negative_scale_transport_right) + (dst_negative_scale_transport_right)))))) /\ (forall dst_index_transport_right. (exists pvs_le_gap_transport_rightdomain. pvs_le_gap_transport_rightdomain + (dst_index_transport_right) = (N)) -> exists dst_positive_transport_right dst_negative_transport_right dst_value_transport_right. ((((exists ff_h_pvs_transport_rightentrypositive. ff_h_pvs_transport_rightentrypositive + S (dst_positive_transport_right) = S ((S (dst_index_transport_right)) * dst_positive_scale_transport_right)) /\ exists ff_q_pvs_transport_rightentrypositive. dst_positive_code_transport_right = ff_q_pvs_transport_rightentrypositive * S ((S (dst_index_transport_right)) * dst_positive_scale_transport_right) + (dst_positive_transport_right))) /\ (((((exists ff_h_pvs_transport_rightentrynegative. ff_h_pvs_transport_rightentrynegative + S (dst_negative_transport_right) = S ((S (dst_index_transport_right)) * dst_negative_scale_transport_right)) /\ exists ff_q_pvs_transport_rightentrynegative. dst_negative_code_transport_right = ff_q_pvs_transport_rightentrynegative * S ((S (dst_index_transport_right)) * dst_negative_scale_transport_right) + (dst_negative_transport_right))) /\ (exists ge_balance_positive_transport_rightentryvalue ge_balance_negative_transport_rightentryvalue. (((((dst_value_transport_right) = 2 * (ge_balance_positive_transport_rightentryvalue) /\ (ge_balance_negative_transport_rightentryvalue) = 0) \/ exists ge_signed_half_transport_rightentryvaluedecode. (((dst_value_transport_right) = 2 * ge_signed_half_transport_rightentryvaluedecode + 1 /\ (ge_balance_positive_transport_rightentryvalue) = 0) /\ (ge_balance_negative_transport_rightentryvalue) = S ge_signed_half_transport_rightentryvaluedecode))) /\ ((dst_positive_transport_right) + ge_balance_negative_transport_rightentryvalue = (dst_negative_transport_right) + ge_balance_positive_transport_rightentryvalue))))))))) -> (exists pvs_le_gap_transport_bound. pvs_le_gap_transport_bound + (n) = (N)) -> (forall dm_index_transport_equal_left dm_first_value_transport_equal_left dm_second_value_transport_equal_left. ~(dm_index_transport_equal_left=0) -> (exists pvs_le_gap_transport_equal_leftdomain. pvs_le_gap_transport_equal_leftdomain + (dm_index_transport_equal_left) = (n)) -> (exists dst_positive_code_transport_equal_leftfirst dst_positive_scale_transport_equal_leftfirst dst_negative_code_transport_equal_leftfirst dst_negative_scale_transport_equal_leftfirst dst_positive_transport_equal_leftfirst dst_negative_transport_equal_leftfirst. (((F) = (((((dst_positive_code_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst)) * S ((dst_positive_code_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst)) + ((dst_positive_scale_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst))) + (((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) * S ((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) + ((dst_negative_scale_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)))) * S ((((dst_positive_code_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst)) * S ((dst_positive_code_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst)) + ((dst_positive_scale_transport_equal_leftfirst) + (dst_positive_scale_transport_equal_leftfirst))) + (((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) * S ((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) + ((dst_negative_scale_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)))) + ((((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) * S ((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) + ((dst_negative_scale_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst))) + (((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) * S ((dst_negative_code_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)) + ((dst_negative_scale_transport_equal_leftfirst) + (dst_negative_scale_transport_equal_leftfirst)))))) /\ (((((exists ff_h_pvs_transport_equal_leftfirstpositive. ff_h_pvs_transport_equal_leftfirstpositive + S (dst_positive_transport_equal_leftfirst) = S ((S (dm_index_transport_equal_left)) * dst_positive_scale_transport_equal_leftfirst)) /\ exists ff_q_pvs_transport_equal_leftfirstpositive. dst_positive_code_transport_equal_leftfirst = ff_q_pvs_transport_equal_leftfirstpositive * S ((S (dm_index_transport_equal_left)) * dst_positive_scale_transport_equal_leftfirst) + (dst_positive_transport_equal_leftfirst))) /\ (((((exists ff_h_pvs_transport_equal_leftfirstnegative. ff_h_pvs_transport_equal_leftfirstnegative + S (dst_negative_transport_equal_leftfirst) = S ((S (dm_index_transport_equal_left)) * dst_negative_scale_transport_equal_leftfirst)) /\ exists ff_q_pvs_transport_equal_leftfirstnegative. dst_negative_code_transport_equal_leftfirst = ff_q_pvs_transport_equal_leftfirstnegative * S ((S (dm_index_transport_equal_left)) * dst_negative_scale_transport_equal_leftfirst) + (dst_negative_transport_equal_leftfirst))) /\ (exists ge_balance_positive_transport_equal_leftfirstvalue ge_balance_negative_transport_equal_leftfirstvalue. (((((dm_first_value_transport_equal_left) = 2 * (ge_balance_positive_transport_equal_leftfirstvalue) /\ (ge_balance_negative_transport_equal_leftfirstvalue) = 0) \/ exists ge_signed_half_transport_equal_leftfirstvaluedecode. (((dm_first_value_transport_equal_left) = 2 * ge_signed_half_transport_equal_leftfirstvaluedecode + 1 /\ (ge_balance_positive_transport_equal_leftfirstvalue) = 0) /\ (ge_balance_negative_transport_equal_leftfirstvalue) = S ge_signed_half_transport_equal_leftfirstvaluedecode))) /\ ((dst_positive_transport_equal_leftfirst) + ge_balance_negative_transport_equal_leftfirstvalue = (dst_negative_transport_equal_leftfirst) + ge_balance_positive_transport_equal_leftfirstvalue))))))))) -> (exists dst_positive_code_transport_equal_leftsecond dst_positive_scale_transport_equal_leftsecond dst_negative_code_transport_equal_leftsecond dst_negative_scale_transport_equal_leftsecond dst_positive_transport_equal_leftsecond dst_negative_transport_equal_leftsecond. (((H) = (((((dst_positive_code_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond)) * S ((dst_positive_code_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond)) + ((dst_positive_scale_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond))) + (((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) * S ((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) + ((dst_negative_scale_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)))) * S ((((dst_positive_code_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond)) * S ((dst_positive_code_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond)) + ((dst_positive_scale_transport_equal_leftsecond) + (dst_positive_scale_transport_equal_leftsecond))) + (((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) * S ((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) + ((dst_negative_scale_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)))) + ((((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) * S ((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) + ((dst_negative_scale_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond))) + (((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) * S ((dst_negative_code_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)) + ((dst_negative_scale_transport_equal_leftsecond) + (dst_negative_scale_transport_equal_leftsecond)))))) /\ (((((exists ff_h_pvs_transport_equal_leftsecondpositive. ff_h_pvs_transport_equal_leftsecondpositive + S (dst_positive_transport_equal_leftsecond) = S ((S (dm_index_transport_equal_left)) * dst_positive_scale_transport_equal_leftsecond)) /\ exists ff_q_pvs_transport_equal_leftsecondpositive. dst_positive_code_transport_equal_leftsecond = ff_q_pvs_transport_equal_leftsecondpositive * S ((S (dm_index_transport_equal_left)) * dst_positive_scale_transport_equal_leftsecond) + (dst_positive_transport_equal_leftsecond))) /\ (((((exists ff_h_pvs_transport_equal_leftsecondnegative. ff_h_pvs_transport_equal_leftsecondnegative + S (dst_negative_transport_equal_leftsecond) = S ((S (dm_index_transport_equal_left)) * dst_negative_scale_transport_equal_leftsecond)) /\ exists ff_q_pvs_transport_equal_leftsecondnegative. dst_negative_code_transport_equal_leftsecond = ff_q_pvs_transport_equal_leftsecondnegative * S ((S (dm_index_transport_equal_left)) * dst_negative_scale_transport_equal_leftsecond) + (dst_negative_transport_equal_leftsecond))) /\ (exists ge_balance_positive_transport_equal_leftsecondvalue ge_balance_negative_transport_equal_leftsecondvalue. (((((dm_second_value_transport_equal_left) = 2 * (ge_balance_positive_transport_equal_leftsecondvalue) /\ (ge_balance_negative_transport_equal_leftsecondvalue) = 0) \/ exists ge_signed_half_transport_equal_leftsecondvaluedecode. (((dm_second_value_transport_equal_left) = 2 * ge_signed_half_transport_equal_leftsecondvaluedecode + 1 /\ (ge_balance_positive_transport_equal_leftsecondvalue) = 0) /\ (ge_balance_negative_transport_equal_leftsecondvalue) = S ge_signed_half_transport_equal_leftsecondvaluedecode))) /\ ((dst_positive_transport_equal_leftsecond) + ge_balance_negative_transport_equal_leftsecondvalue = (dst_negative_transport_equal_leftsecond) + ge_balance_positive_transport_equal_leftsecondvalue))))))))) -> dm_first_value_transport_equal_left=dm_second_value_transport_equal_left) -> (forall dm_index_transport_equal_right dm_first_value_transport_equal_right dm_second_value_transport_equal_right. ~(dm_index_transport_equal_right=0) -> (exists pvs_le_gap_transport_equal_rightdomain. pvs_le_gap_transport_equal_rightdomain + (dm_index_transport_equal_right) = (n)) -> (exists dst_positive_code_transport_equal_rightfirst dst_positive_scale_transport_equal_rightfirst dst_negative_code_transport_equal_rightfirst dst_negative_scale_transport_equal_rightfirst dst_positive_transport_equal_rightfirst dst_negative_transport_equal_rightfirst. (((G) = (((((dst_positive_code_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst)) * S ((dst_positive_code_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst)) + ((dst_positive_scale_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst))) + (((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) * S ((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) + ((dst_negative_scale_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)))) * S ((((dst_positive_code_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst)) * S ((dst_positive_code_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst)) + ((dst_positive_scale_transport_equal_rightfirst) + (dst_positive_scale_transport_equal_rightfirst))) + (((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) * S ((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) + ((dst_negative_scale_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)))) + ((((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) * S ((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) + ((dst_negative_scale_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst))) + (((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) * S ((dst_negative_code_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)) + ((dst_negative_scale_transport_equal_rightfirst) + (dst_negative_scale_transport_equal_rightfirst)))))) /\ (((((exists ff_h_pvs_transport_equal_rightfirstpositive. ff_h_pvs_transport_equal_rightfirstpositive + S (dst_positive_transport_equal_rightfirst) = S ((S (dm_index_transport_equal_right)) * dst_positive_scale_transport_equal_rightfirst)) /\ exists ff_q_pvs_transport_equal_rightfirstpositive. dst_positive_code_transport_equal_rightfirst = ff_q_pvs_transport_equal_rightfirstpositive * S ((S (dm_index_transport_equal_right)) * dst_positive_scale_transport_equal_rightfirst) + (dst_positive_transport_equal_rightfirst))) /\ (((((exists ff_h_pvs_transport_equal_rightfirstnegative. ff_h_pvs_transport_equal_rightfirstnegative + S (dst_negative_transport_equal_rightfirst) = S ((S (dm_index_transport_equal_right)) * dst_negative_scale_transport_equal_rightfirst)) /\ exists ff_q_pvs_transport_equal_rightfirstnegative. dst_negative_code_transport_equal_rightfirst = ff_q_pvs_transport_equal_rightfirstnegative * S ((S (dm_index_transport_equal_right)) * dst_negative_scale_transport_equal_rightfirst) + (dst_negative_transport_equal_rightfirst))) /\ (exists ge_balance_positive_transport_equal_rightfirstvalue ge_balance_negative_transport_equal_rightfirstvalue. (((((dm_first_value_transport_equal_right) = 2 * (ge_balance_positive_transport_equal_rightfirstvalue) /\ (ge_balance_negative_transport_equal_rightfirstvalue) = 0) \/ exists ge_signed_half_transport_equal_rightfirstvaluedecode. (((dm_first_value_transport_equal_right) = 2 * ge_signed_half_transport_equal_rightfirstvaluedecode + 1 /\ (ge_balance_positive_transport_equal_rightfirstvalue) = 0) /\ (ge_balance_negative_transport_equal_rightfirstvalue) = S ge_signed_half_transport_equal_rightfirstvaluedecode))) /\ ((dst_positive_transport_equal_rightfirst) + ge_balance_negative_transport_equal_rightfirstvalue = (dst_negative_transport_equal_rightfirst) + ge_balance_positive_transport_equal_rightfirstvalue))))))))) -> (exists dst_positive_code_transport_equal_rightsecond dst_positive_scale_transport_equal_rightsecond dst_negative_code_transport_equal_rightsecond dst_negative_scale_transport_equal_rightsecond dst_positive_transport_equal_rightsecond dst_negative_transport_equal_rightsecond. (((K) = (((((dst_positive_code_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond)) * S ((dst_positive_code_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond)) + ((dst_positive_scale_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond))) + (((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) * S ((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) + ((dst_negative_scale_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)))) * S ((((dst_positive_code_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond)) * S ((dst_positive_code_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond)) + ((dst_positive_scale_transport_equal_rightsecond) + (dst_positive_scale_transport_equal_rightsecond))) + (((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) * S ((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) + ((dst_negative_scale_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)))) + ((((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) * S ((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) + ((dst_negative_scale_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond))) + (((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) * S ((dst_negative_code_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)) + ((dst_negative_scale_transport_equal_rightsecond) + (dst_negative_scale_transport_equal_rightsecond)))))) /\ (((((exists ff_h_pvs_transport_equal_rightsecondpositive. ff_h_pvs_transport_equal_rightsecondpositive + S (dst_positive_transport_equal_rightsecond) = S ((S (dm_index_transport_equal_right)) * dst_positive_scale_transport_equal_rightsecond)) /\ exists ff_q_pvs_transport_equal_rightsecondpositive. dst_positive_code_transport_equal_rightsecond = ff_q_pvs_transport_equal_rightsecondpositive * S ((S (dm_index_transport_equal_right)) * dst_positive_scale_transport_equal_rightsecond) + (dst_positive_transport_equal_rightsecond))) /\ (((((exists ff_h_pvs_transport_equal_rightsecondnegative. ff_h_pvs_transport_equal_rightsecondnegative + S (dst_negative_transport_equal_rightsecond) = S ((S (dm_index_transport_equal_right)) * dst_negative_scale_transport_equal_rightsecond)) /\ exists ff_q_pvs_transport_equal_rightsecondnegative. dst_negative_code_transport_equal_rightsecond = ff_q_pvs_transport_equal_rightsecondnegative * S ((S (dm_index_transport_equal_right)) * dst_negative_scale_transport_equal_rightsecond) + (dst_negative_transport_equal_rightsecond))) /\ (exists ge_balance_positive_transport_equal_rightsecondvalue ge_balance_negative_transport_equal_rightsecondvalue. (((((dm_second_value_transport_equal_right) = 2 * (ge_balance_positive_transport_equal_rightsecondvalue) /\ (ge_balance_negative_transport_equal_rightsecondvalue) = 0) \/ exists ge_signed_half_transport_equal_rightsecondvaluedecode. (((dm_second_value_transport_equal_right) = 2 * ge_signed_half_transport_equal_rightsecondvaluedecode + 1 /\ (ge_balance_positive_transport_equal_rightsecondvalue) = 0) /\ (ge_balance_negative_transport_equal_rightsecondvalue) = S ge_signed_half_transport_equal_rightsecondvaluedecode))) /\ ((dst_positive_transport_equal_rightsecond) + ge_balance_negative_transport_equal_rightsecondvalue = (dst_negative_transport_equal_rightsecond) + ge_balance_positive_transport_equal_rightsecondvalue))))))))) -> dm_first_value_transport_equal_right=dm_second_value_transport_equal_right) -> (((~((n)=0)) /\ (exists dc_mask_transport_source. ((((exists dst_positive_code_transport_sourcemasktable dst_positive_scale_transport_sourcemasktable dst_negative_code_transport_sourcemasktable dst_negative_scale_transport_sourcemasktable. (((dc_mask_transport_source) = (((((dst_positive_code_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable)) * S ((dst_positive_code_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable)) + ((dst_positive_scale_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable))) + (((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) * S ((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) + ((dst_negative_scale_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)))) * S ((((dst_positive_code_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable)) * S ((dst_positive_code_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable)) + ((dst_positive_scale_transport_sourcemasktable) + (dst_positive_scale_transport_sourcemasktable))) + (((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) * S ((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) + ((dst_negative_scale_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)))) + ((((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) * S ((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) + ((dst_negative_scale_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable))) + (((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) * S ((dst_negative_code_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)) + ((dst_negative_scale_transport_sourcemasktable) + (dst_negative_scale_transport_sourcemasktable)))))) /\ (forall dst_index_transport_sourcemasktable. (exists pvs_le_gap_transport_sourcemasktabledomain. pvs_le_gap_transport_sourcemasktabledomain + (dst_index_transport_sourcemasktable) = (n)) -> exists dst_positive_transport_sourcemasktable dst_negative_transport_sourcemasktable dst_value_transport_sourcemasktable. ((((exists ff_h_pvs_transport_sourcemasktableentrypositive. ff_h_pvs_transport_sourcemasktableentrypositive + S (dst_positive_transport_sourcemasktable) = S ((S (dst_index_transport_sourcemasktable)) * dst_positive_scale_transport_sourcemasktable)) /\ exists ff_q_pvs_transport_sourcemasktableentrypositive. dst_positive_code_transport_sourcemasktable = ff_q_pvs_transport_sourcemasktableentrypositive * S ((S (dst_index_transport_sourcemasktable)) * dst_positive_scale_transport_sourcemasktable) + (dst_positive_transport_sourcemasktable))) /\ (((((exists ff_h_pvs_transport_sourcemasktableentrynegative. ff_h_pvs_transport_sourcemasktableentrynegative + S (dst_negative_transport_sourcemasktable) = S ((S (dst_index_transport_sourcemasktable)) * dst_negative_scale_transport_sourcemasktable)) /\ exists ff_q_pvs_transport_sourcemasktableentrynegative. dst_negative_code_transport_sourcemasktable = ff_q_pvs_transport_sourcemasktableentrynegative * S ((S (dst_index_transport_sourcemasktable)) * dst_negative_scale_transport_sourcemasktable) + (dst_negative_transport_sourcemasktable))) /\ (exists ge_balance_positive_transport_sourcemasktableentryvalue ge_balance_negative_transport_sourcemasktableentryvalue. (((((dst_value_transport_sourcemasktable) = 2 * (ge_balance_positive_transport_sourcemasktableentryvalue) /\ (ge_balance_negative_transport_sourcemasktableentryvalue) = 0) \/ exists ge_signed_half_transport_sourcemasktableentryvaluedecode. (((dst_value_transport_sourcemasktable) = 2 * ge_signed_half_transport_sourcemasktableentryvaluedecode + 1 /\ (ge_balance_positive_transport_sourcemasktableentryvalue) = 0) /\ (ge_balance_negative_transport_sourcemasktableentryvalue) = S ge_signed_half_transport_sourcemasktableentryvaluedecode))) /\ ((dst_positive_transport_sourcemasktable) + ge_balance_negative_transport_sourcemasktableentryvalue = (dst_negative_transport_sourcemasktable) + ge_balance_positive_transport_sourcemasktableentryvalue))))))))) /\ (forall dc_index_transport_sourcemask dc_value_transport_sourcemask. (exists pvs_le_gap_transport_sourcemaskdomain. pvs_le_gap_transport_sourcemaskdomain + (dc_index_transport_sourcemask) = (n)) -> (exists dst_positive_code_transport_sourcemasklookup dst_positive_scale_transport_sourcemasklookup dst_negative_code_transport_sourcemasklookup dst_negative_scale_transport_sourcemasklookup dst_positive_transport_sourcemasklookup dst_negative_transport_sourcemasklookup. (((dc_mask_transport_source) = (((((dst_positive_code_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup)) * S ((dst_positive_code_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup)) + ((dst_positive_scale_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup))) + (((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) * S ((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) + ((dst_negative_scale_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)))) * S ((((dst_positive_code_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup)) * S ((dst_positive_code_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup)) + ((dst_positive_scale_transport_sourcemasklookup) + (dst_positive_scale_transport_sourcemasklookup))) + (((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) * S ((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) + ((dst_negative_scale_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)))) + ((((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) * S ((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) + ((dst_negative_scale_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup))) + (((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) * S ((dst_negative_code_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)) + ((dst_negative_scale_transport_sourcemasklookup) + (dst_negative_scale_transport_sourcemasklookup)))))) /\ (((((exists ff_h_pvs_transport_sourcemasklookuppositive. ff_h_pvs_transport_sourcemasklookuppositive + S (dst_positive_transport_sourcemasklookup) = S ((S (dc_index_transport_sourcemask)) * dst_positive_scale_transport_sourcemasklookup)) /\ exists ff_q_pvs_transport_sourcemasklookuppositive. dst_positive_code_transport_sourcemasklookup = ff_q_pvs_transport_sourcemasklookuppositive * S ((S (dc_index_transport_sourcemask)) * dst_positive_scale_transport_sourcemasklookup) + (dst_positive_transport_sourcemasklookup))) /\ (((((exists ff_h_pvs_transport_sourcemasklookupnegative. ff_h_pvs_transport_sourcemasklookupnegative + S (dst_negative_transport_sourcemasklookup) = S ((S (dc_index_transport_sourcemask)) * dst_negative_scale_transport_sourcemasklookup)) /\ exists ff_q_pvs_transport_sourcemasklookupnegative. dst_negative_code_transport_sourcemasklookup = ff_q_pvs_transport_sourcemasklookupnegative * S ((S (dc_index_transport_sourcemask)) * dst_negative_scale_transport_sourcemasklookup) + (dst_negative_transport_sourcemasklookup))) /\ (exists ge_balance_positive_transport_sourcemasklookupvalue ge_balance_negative_transport_sourcemasklookupvalue. (((((dc_value_transport_sourcemask) = 2 * (ge_balance_positive_transport_sourcemasklookupvalue) /\ (ge_balance_negative_transport_sourcemasklookupvalue) = 0) \/ exists ge_signed_half_transport_sourcemasklookupvaluedecode. (((dc_value_transport_sourcemask) = 2 * ge_signed_half_transport_sourcemasklookupvaluedecode + 1 /\ (ge_balance_positive_transport_sourcemasklookupvalue) = 0) /\ (ge_balance_negative_transport_sourcemasklookupvalue) = S ge_signed_half_transport_sourcemasklookupvaluedecode))) /\ ((dst_positive_transport_sourcemasklookup) + ge_balance_negative_transport_sourcemasklookupvalue = (dst_negative_transport_sourcemasklookup) + ge_balance_positive_transport_sourcemasklookupvalue))))))))) -> ((((~((dc_index_transport_sourcemask)=0)) /\ (exists dc_quotient_transport_sourcemaskentry dc_left_transport_sourcemaskentry dc_right_transport_sourcemaskentry. (((n)=(dc_index_transport_sourcemask)*dc_quotient_transport_sourcemaskentry) /\ (((exists dst_positive_code_transport_sourcemaskentryleft dst_positive_scale_transport_sourcemaskentryleft dst_negative_code_transport_sourcemaskentryleft dst_negative_scale_transport_sourcemaskentryleft dst_positive_transport_sourcemaskentryleft dst_negative_transport_sourcemaskentryleft. (((F) = (((((dst_positive_code_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft)) * S ((dst_positive_code_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft)) + ((dst_positive_scale_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft))) + (((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) * S ((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) + ((dst_negative_scale_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)))) * S ((((dst_positive_code_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft)) * S ((dst_positive_code_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft)) + ((dst_positive_scale_transport_sourcemaskentryleft) + (dst_positive_scale_transport_sourcemaskentryleft))) + (((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) * S ((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) + ((dst_negative_scale_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)))) + ((((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) * S ((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) + ((dst_negative_scale_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft))) + (((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) * S ((dst_negative_code_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)) + ((dst_negative_scale_transport_sourcemaskentryleft) + (dst_negative_scale_transport_sourcemaskentryleft)))))) /\ (((((exists ff_h_pvs_transport_sourcemaskentryleftpositive. ff_h_pvs_transport_sourcemaskentryleftpositive + S (dst_positive_transport_sourcemaskentryleft) = S ((S (dc_index_transport_sourcemask)) * dst_positive_scale_transport_sourcemaskentryleft)) /\ exists ff_q_pvs_transport_sourcemaskentryleftpositive. dst_positive_code_transport_sourcemaskentryleft = ff_q_pvs_transport_sourcemaskentryleftpositive * S ((S (dc_index_transport_sourcemask)) * dst_positive_scale_transport_sourcemaskentryleft) + (dst_positive_transport_sourcemaskentryleft))) /\ (((((exists ff_h_pvs_transport_sourcemaskentryleftnegative. ff_h_pvs_transport_sourcemaskentryleftnegative + S (dst_negative_transport_sourcemaskentryleft) = S ((S (dc_index_transport_sourcemask)) * dst_negative_scale_transport_sourcemaskentryleft)) /\ exists ff_q_pvs_transport_sourcemaskentryleftnegative. dst_negative_code_transport_sourcemaskentryleft = ff_q_pvs_transport_sourcemaskentryleftnegative * S ((S (dc_index_transport_sourcemask)) * dst_negative_scale_transport_sourcemaskentryleft) + (dst_negative_transport_sourcemaskentryleft))) /\ (exists ge_balance_positive_transport_sourcemaskentryleftvalue ge_balance_negative_transport_sourcemaskentryleftvalue. (((((dc_left_transport_sourcemaskentry) = 2 * (ge_balance_positive_transport_sourcemaskentryleftvalue) /\ (ge_balance_negative_transport_sourcemaskentryleftvalue) = 0) \/ exists ge_signed_half_transport_sourcemaskentryleftvaluedecode. (((dc_left_transport_sourcemaskentry) = 2 * ge_signed_half_transport_sourcemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_transport_sourcemaskentryleftvalue) = 0) /\ (ge_balance_negative_transport_sourcemaskentryleftvalue) = S ge_signed_half_transport_sourcemaskentryleftvaluedecode))) /\ ((dst_positive_transport_sourcemaskentryleft) + ge_balance_negative_transport_sourcemaskentryleftvalue = (dst_negative_transport_sourcemaskentryleft) + ge_balance_positive_transport_sourcemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_transport_sourcemaskentryright dst_positive_scale_transport_sourcemaskentryright dst_negative_code_transport_sourcemaskentryright dst_negative_scale_transport_sourcemaskentryright dst_positive_transport_sourcemaskentryright dst_negative_transport_sourcemaskentryright. (((G) = (((((dst_positive_code_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright)) * S ((dst_positive_code_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright)) + ((dst_positive_scale_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright))) + (((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) * S ((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) + ((dst_negative_scale_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)))) * S ((((dst_positive_code_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright)) * S ((dst_positive_code_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright)) + ((dst_positive_scale_transport_sourcemaskentryright) + (dst_positive_scale_transport_sourcemaskentryright))) + (((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) * S ((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) + ((dst_negative_scale_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)))) + ((((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) * S ((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) + ((dst_negative_scale_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright))) + (((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) * S ((dst_negative_code_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)) + ((dst_negative_scale_transport_sourcemaskentryright) + (dst_negative_scale_transport_sourcemaskentryright)))))) /\ (((((exists ff_h_pvs_transport_sourcemaskentryrightpositive. ff_h_pvs_transport_sourcemaskentryrightpositive + S (dst_positive_transport_sourcemaskentryright) = S ((S (dc_quotient_transport_sourcemaskentry)) * dst_positive_scale_transport_sourcemaskentryright)) /\ exists ff_q_pvs_transport_sourcemaskentryrightpositive. dst_positive_code_transport_sourcemaskentryright = ff_q_pvs_transport_sourcemaskentryrightpositive * S ((S (dc_quotient_transport_sourcemaskentry)) * dst_positive_scale_transport_sourcemaskentryright) + (dst_positive_transport_sourcemaskentryright))) /\ (((((exists ff_h_pvs_transport_sourcemaskentryrightnegative. ff_h_pvs_transport_sourcemaskentryrightnegative + S (dst_negative_transport_sourcemaskentryright) = S ((S (dc_quotient_transport_sourcemaskentry)) * dst_negative_scale_transport_sourcemaskentryright)) /\ exists ff_q_pvs_transport_sourcemaskentryrightnegative. dst_negative_code_transport_sourcemaskentryright = ff_q_pvs_transport_sourcemaskentryrightnegative * S ((S (dc_quotient_transport_sourcemaskentry)) * dst_negative_scale_transport_sourcemaskentryright) + (dst_negative_transport_sourcemaskentryright))) /\ (exists ge_balance_positive_transport_sourcemaskentryrightvalue ge_balance_negative_transport_sourcemaskentryrightvalue. (((((dc_right_transport_sourcemaskentry) = 2 * (ge_balance_positive_transport_sourcemaskentryrightvalue) /\ (ge_balance_negative_transport_sourcemaskentryrightvalue) = 0) \/ exists ge_signed_half_transport_sourcemaskentryrightvaluedecode. (((dc_right_transport_sourcemaskentry) = 2 * ge_signed_half_transport_sourcemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_transport_sourcemaskentryrightvalue) = 0) /\ (ge_balance_negative_transport_sourcemaskentryrightvalue) = S ge_signed_half_transport_sourcemaskentryrightvaluedecode))) /\ ((dst_positive_transport_sourcemaskentryright) + ge_balance_negative_transport_sourcemaskentryrightvalue = (dst_negative_transport_sourcemaskentryright) + ge_balance_positive_transport_sourcemaskentryrightvalue))))))))) /\ (exists sto_ap_transport_sourcemaskentryproduct sto_an_transport_sourcemaskentryproduct sto_bp_transport_sourcemaskentryproduct sto_bn_transport_sourcemaskentryproduct sto_cp_transport_sourcemaskentryproduct sto_cn_transport_sourcemaskentryproduct. (((((dc_left_transport_sourcemaskentry) = 2 * (sto_ap_transport_sourcemaskentryproduct) /\ (sto_an_transport_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_transport_sourcemaskentryproductleft. (((dc_left_transport_sourcemaskentry) = 2 * ge_signed_half_transport_sourcemaskentryproductleft + 1 /\ (sto_ap_transport_sourcemaskentryproduct) = 0) /\ (sto_an_transport_sourcemaskentryproduct) = S ge_signed_half_transport_sourcemaskentryproductleft))) /\ ((((((dc_right_transport_sourcemaskentry) = 2 * (sto_bp_transport_sourcemaskentryproduct) /\ (sto_bn_transport_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_transport_sourcemaskentryproductright. (((dc_right_transport_sourcemaskentry) = 2 * ge_signed_half_transport_sourcemaskentryproductright + 1 /\ (sto_bp_transport_sourcemaskentryproduct) = 0) /\ (sto_bn_transport_sourcemaskentryproduct) = S ge_signed_half_transport_sourcemaskentryproductright))) /\ ((((((dc_value_transport_sourcemask) = 2 * (sto_cp_transport_sourcemaskentryproduct) /\ (sto_cn_transport_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_transport_sourcemaskentryproductoutput. (((dc_value_transport_sourcemask) = 2 * ge_signed_half_transport_sourcemaskentryproductoutput + 1 /\ (sto_cp_transport_sourcemaskentryproduct) = 0) /\ (sto_cn_transport_sourcemaskentryproduct) = S ge_signed_half_transport_sourcemaskentryproductoutput))) /\ ((sto_ap_transport_sourcemaskentryproduct * sto_bp_transport_sourcemaskentryproduct + sto_an_transport_sourcemaskentryproduct * sto_bn_transport_sourcemaskentryproduct) + sto_cn_transport_sourcemaskentryproduct = (sto_ap_transport_sourcemaskentryproduct * sto_bn_transport_sourcemaskentryproduct + sto_an_transport_sourcemaskentryproduct * sto_bp_transport_sourcemaskentryproduct) + sto_cp_transport_sourcemaskentryproduct))))))))))))))) \/ ((((dc_index_transport_sourcemask)=0 \/ ~(exists pvs_factor_transport_sourcemaskentrynondivisor. (n) = (dc_index_transport_sourcemask) * pvs_factor_transport_sourcemaskentrynondivisor)) /\ ((dc_value_transport_sourcemask)=0))))))) /\ (exists dst_positive_code_transport_sourcefold dst_positive_scale_transport_sourcefold dst_negative_code_transport_sourcefold dst_negative_scale_transport_sourcefold dst_positive_sum_transport_sourcefold dst_negative_sum_transport_sourcefold. (((dc_mask_transport_source) = (((((dst_positive_code_transport_sourcefold) + (dst_positive_scale_transport_sourcefold)) * S ((dst_positive_code_transport_sourcefold) + (dst_positive_scale_transport_sourcefold)) + ((dst_positive_scale_transport_sourcefold) + (dst_positive_scale_transport_sourcefold))) + (((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) * S ((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) + ((dst_negative_scale_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)))) * S ((((dst_positive_code_transport_sourcefold) + (dst_positive_scale_transport_sourcefold)) * S ((dst_positive_code_transport_sourcefold) + (dst_positive_scale_transport_sourcefold)) + ((dst_positive_scale_transport_sourcefold) + (dst_positive_scale_transport_sourcefold))) + (((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) * S ((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) + ((dst_negative_scale_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)))) + ((((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) * S ((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) + ((dst_negative_scale_transport_sourcefold) + (dst_negative_scale_transport_sourcefold))) + (((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) * S ((dst_negative_code_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)) + ((dst_negative_scale_transport_sourcefold) + (dst_negative_scale_transport_sourcefold)))))) /\ (((exists fs_u_dst_transport_sourcefoldpositive fs_v_dst_transport_sourcefoldpositive. ((((exists fs_h_dst_transport_sourcefoldpositive_body_start. fs_h_dst_transport_sourcefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transport_sourcefoldpositive)) /\ exists fs_q_dst_transport_sourcefoldpositive_body_start. fs_u_dst_transport_sourcefoldpositive = fs_q_dst_transport_sourcefoldpositive_body_start * S ((S (0)) * fs_v_dst_transport_sourcefoldpositive) + (0))) /\ ((((exists fs_h_dst_transport_sourcefoldpositive_body_terminal. fs_h_dst_transport_sourcefoldpositive_body_terminal + S (dst_positive_sum_transport_sourcefold) = S ((S (S (n))) * fs_v_dst_transport_sourcefoldpositive)) /\ exists fs_q_dst_transport_sourcefoldpositive_body_terminal. fs_u_dst_transport_sourcefoldpositive = fs_q_dst_transport_sourcefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_transport_sourcefoldpositive) + (dst_positive_sum_transport_sourcefold))) /\ forall fs_i_dst_transport_sourcefoldpositive_body_steps. (exists fs_lt_dst_transport_sourcefoldpositive_body_steps_bound. fs_lt_dst_transport_sourcefoldpositive_body_steps_bound + S fs_i_dst_transport_sourcefoldpositive_body_steps = S (n)) -> exists fs_a_dst_transport_sourcefoldpositive_body_steps fs_r_dst_transport_sourcefoldpositive_body_steps fs_s_dst_transport_sourcefoldpositive_body_steps. ((((exists fs_h_dst_transport_sourcefoldpositive_body_steps_summand. fs_h_dst_transport_sourcefoldpositive_body_steps_summand + S (fs_a_dst_transport_sourcefoldpositive_body_steps) = S ((S (fs_i_dst_transport_sourcefoldpositive_body_steps)) * dst_positive_scale_transport_sourcefold)) /\ exists fs_q_dst_transport_sourcefoldpositive_body_steps_summand. dst_positive_code_transport_sourcefold = fs_q_dst_transport_sourcefoldpositive_body_steps_summand * S ((S (fs_i_dst_transport_sourcefoldpositive_body_steps)) * dst_positive_scale_transport_sourcefold) + (fs_a_dst_transport_sourcefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transport_sourcefoldpositive_body_steps_partial. fs_h_dst_transport_sourcefoldpositive_body_steps_partial + S (fs_r_dst_transport_sourcefoldpositive_body_steps) = S ((S (fs_i_dst_transport_sourcefoldpositive_body_steps)) * fs_v_dst_transport_sourcefoldpositive)) /\ exists fs_q_dst_transport_sourcefoldpositive_body_steps_partial. fs_u_dst_transport_sourcefoldpositive = fs_q_dst_transport_sourcefoldpositive_body_steps_partial * S ((S (fs_i_dst_transport_sourcefoldpositive_body_steps)) * fs_v_dst_transport_sourcefoldpositive) + (fs_r_dst_transport_sourcefoldpositive_body_steps))) /\ ((((exists fs_h_dst_transport_sourcefoldpositive_body_steps_successor. fs_h_dst_transport_sourcefoldpositive_body_steps_successor + S (fs_s_dst_transport_sourcefoldpositive_body_steps) = S ((S (S fs_i_dst_transport_sourcefoldpositive_body_steps)) * fs_v_dst_transport_sourcefoldpositive)) /\ exists fs_q_dst_transport_sourcefoldpositive_body_steps_successor. fs_u_dst_transport_sourcefoldpositive = fs_q_dst_transport_sourcefoldpositive_body_steps_successor * S ((S (S fs_i_dst_transport_sourcefoldpositive_body_steps)) * fs_v_dst_transport_sourcefoldpositive) + (fs_s_dst_transport_sourcefoldpositive_body_steps))) /\ fs_s_dst_transport_sourcefoldpositive_body_steps = fs_r_dst_transport_sourcefoldpositive_body_steps + fs_a_dst_transport_sourcefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transport_sourcefoldnegative fs_v_dst_transport_sourcefoldnegative. ((((exists fs_h_dst_transport_sourcefoldnegative_body_start. fs_h_dst_transport_sourcefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transport_sourcefoldnegative)) /\ exists fs_q_dst_transport_sourcefoldnegative_body_start. fs_u_dst_transport_sourcefoldnegative = fs_q_dst_transport_sourcefoldnegative_body_start * S ((S (0)) * fs_v_dst_transport_sourcefoldnegative) + (0))) /\ ((((exists fs_h_dst_transport_sourcefoldnegative_body_terminal. fs_h_dst_transport_sourcefoldnegative_body_terminal + S (dst_negative_sum_transport_sourcefold) = S ((S (S (n))) * fs_v_dst_transport_sourcefoldnegative)) /\ exists fs_q_dst_transport_sourcefoldnegative_body_terminal. fs_u_dst_transport_sourcefoldnegative = fs_q_dst_transport_sourcefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_transport_sourcefoldnegative) + (dst_negative_sum_transport_sourcefold))) /\ forall fs_i_dst_transport_sourcefoldnegative_body_steps. (exists fs_lt_dst_transport_sourcefoldnegative_body_steps_bound. fs_lt_dst_transport_sourcefoldnegative_body_steps_bound + S fs_i_dst_transport_sourcefoldnegative_body_steps = S (n)) -> exists fs_a_dst_transport_sourcefoldnegative_body_steps fs_r_dst_transport_sourcefoldnegative_body_steps fs_s_dst_transport_sourcefoldnegative_body_steps. ((((exists fs_h_dst_transport_sourcefoldnegative_body_steps_summand. fs_h_dst_transport_sourcefoldnegative_body_steps_summand + S (fs_a_dst_transport_sourcefoldnegative_body_steps) = S ((S (fs_i_dst_transport_sourcefoldnegative_body_steps)) * dst_negative_scale_transport_sourcefold)) /\ exists fs_q_dst_transport_sourcefoldnegative_body_steps_summand. dst_negative_code_transport_sourcefold = fs_q_dst_transport_sourcefoldnegative_body_steps_summand * S ((S (fs_i_dst_transport_sourcefoldnegative_body_steps)) * dst_negative_scale_transport_sourcefold) + (fs_a_dst_transport_sourcefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transport_sourcefoldnegative_body_steps_partial. fs_h_dst_transport_sourcefoldnegative_body_steps_partial + S (fs_r_dst_transport_sourcefoldnegative_body_steps) = S ((S (fs_i_dst_transport_sourcefoldnegative_body_steps)) * fs_v_dst_transport_sourcefoldnegative)) /\ exists fs_q_dst_transport_sourcefoldnegative_body_steps_partial. fs_u_dst_transport_sourcefoldnegative = fs_q_dst_transport_sourcefoldnegative_body_steps_partial * S ((S (fs_i_dst_transport_sourcefoldnegative_body_steps)) * fs_v_dst_transport_sourcefoldnegative) + (fs_r_dst_transport_sourcefoldnegative_body_steps))) /\ ((((exists fs_h_dst_transport_sourcefoldnegative_body_steps_successor. fs_h_dst_transport_sourcefoldnegative_body_steps_successor + S (fs_s_dst_transport_sourcefoldnegative_body_steps) = S ((S (S fs_i_dst_transport_sourcefoldnegative_body_steps)) * fs_v_dst_transport_sourcefoldnegative)) /\ exists fs_q_dst_transport_sourcefoldnegative_body_steps_successor. fs_u_dst_transport_sourcefoldnegative = fs_q_dst_transport_sourcefoldnegative_body_steps_successor * S ((S (S fs_i_dst_transport_sourcefoldnegative_body_steps)) * fs_v_dst_transport_sourcefoldnegative) + (fs_s_dst_transport_sourcefoldnegative_body_steps))) /\ fs_s_dst_transport_sourcefoldnegative_body_steps = fs_r_dst_transport_sourcefoldnegative_body_steps + fs_a_dst_transport_sourcefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transport_sourcefoldresult ge_balance_negative_transport_sourcefoldresult. (((((z) = 2 * (ge_balance_positive_transport_sourcefoldresult) /\ (ge_balance_negative_transport_sourcefoldresult) = 0) \/ exists ge_signed_half_transport_sourcefoldresultdecode. (((z) = 2 * ge_signed_half_transport_sourcefoldresultdecode + 1 /\ (ge_balance_positive_transport_sourcefoldresult) = 0) /\ (ge_balance_negative_transport_sourcefoldresult) = S ge_signed_half_transport_sourcefoldresultdecode))) /\ ((dst_positive_sum_transport_sourcefold) + ge_balance_negative_transport_sourcefoldresult = (dst_negative_sum_transport_sourcefold) + ge_balance_positive_transport_sourcefoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_transport_result. ((((exists dst_positive_code_transport_resultmasktable dst_positive_scale_transport_resultmasktable dst_negative_code_transport_resultmasktable dst_negative_scale_transport_resultmasktable. (((dc_mask_transport_result) = (((((dst_positive_code_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable)) * S ((dst_positive_code_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable)) + ((dst_positive_scale_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable))) + (((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) * S ((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) + ((dst_negative_scale_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)))) * S ((((dst_positive_code_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable)) * S ((dst_positive_code_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable)) + ((dst_positive_scale_transport_resultmasktable) + (dst_positive_scale_transport_resultmasktable))) + (((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) * S ((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) + ((dst_negative_scale_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)))) + ((((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) * S ((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) + ((dst_negative_scale_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable))) + (((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) * S ((dst_negative_code_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)) + ((dst_negative_scale_transport_resultmasktable) + (dst_negative_scale_transport_resultmasktable)))))) /\ (forall dst_index_transport_resultmasktable. (exists pvs_le_gap_transport_resultmasktabledomain. pvs_le_gap_transport_resultmasktabledomain + (dst_index_transport_resultmasktable) = (n)) -> exists dst_positive_transport_resultmasktable dst_negative_transport_resultmasktable dst_value_transport_resultmasktable. ((((exists ff_h_pvs_transport_resultmasktableentrypositive. ff_h_pvs_transport_resultmasktableentrypositive + S (dst_positive_transport_resultmasktable) = S ((S (dst_index_transport_resultmasktable)) * dst_positive_scale_transport_resultmasktable)) /\ exists ff_q_pvs_transport_resultmasktableentrypositive. dst_positive_code_transport_resultmasktable = ff_q_pvs_transport_resultmasktableentrypositive * S ((S (dst_index_transport_resultmasktable)) * dst_positive_scale_transport_resultmasktable) + (dst_positive_transport_resultmasktable))) /\ (((((exists ff_h_pvs_transport_resultmasktableentrynegative. ff_h_pvs_transport_resultmasktableentrynegative + S (dst_negative_transport_resultmasktable) = S ((S (dst_index_transport_resultmasktable)) * dst_negative_scale_transport_resultmasktable)) /\ exists ff_q_pvs_transport_resultmasktableentrynegative. dst_negative_code_transport_resultmasktable = ff_q_pvs_transport_resultmasktableentrynegative * S ((S (dst_index_transport_resultmasktable)) * dst_negative_scale_transport_resultmasktable) + (dst_negative_transport_resultmasktable))) /\ (exists ge_balance_positive_transport_resultmasktableentryvalue ge_balance_negative_transport_resultmasktableentryvalue. (((((dst_value_transport_resultmasktable) = 2 * (ge_balance_positive_transport_resultmasktableentryvalue) /\ (ge_balance_negative_transport_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_transport_resultmasktableentryvaluedecode. (((dst_value_transport_resultmasktable) = 2 * ge_signed_half_transport_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_transport_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_transport_resultmasktableentryvalue) = S ge_signed_half_transport_resultmasktableentryvaluedecode))) /\ ((dst_positive_transport_resultmasktable) + ge_balance_negative_transport_resultmasktableentryvalue = (dst_negative_transport_resultmasktable) + ge_balance_positive_transport_resultmasktableentryvalue))))))))) /\ (forall dc_index_transport_resultmask dc_value_transport_resultmask. (exists pvs_le_gap_transport_resultmaskdomain. pvs_le_gap_transport_resultmaskdomain + (dc_index_transport_resultmask) = (n)) -> (exists dst_positive_code_transport_resultmasklookup dst_positive_scale_transport_resultmasklookup dst_negative_code_transport_resultmasklookup dst_negative_scale_transport_resultmasklookup dst_positive_transport_resultmasklookup dst_negative_transport_resultmasklookup. (((dc_mask_transport_result) = (((((dst_positive_code_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup)) * S ((dst_positive_code_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup)) + ((dst_positive_scale_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup))) + (((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) * S ((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) + ((dst_negative_scale_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)))) * S ((((dst_positive_code_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup)) * S ((dst_positive_code_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup)) + ((dst_positive_scale_transport_resultmasklookup) + (dst_positive_scale_transport_resultmasklookup))) + (((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) * S ((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) + ((dst_negative_scale_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)))) + ((((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) * S ((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) + ((dst_negative_scale_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup))) + (((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) * S ((dst_negative_code_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)) + ((dst_negative_scale_transport_resultmasklookup) + (dst_negative_scale_transport_resultmasklookup)))))) /\ (((((exists ff_h_pvs_transport_resultmasklookuppositive. ff_h_pvs_transport_resultmasklookuppositive + S (dst_positive_transport_resultmasklookup) = S ((S (dc_index_transport_resultmask)) * dst_positive_scale_transport_resultmasklookup)) /\ exists ff_q_pvs_transport_resultmasklookuppositive. dst_positive_code_transport_resultmasklookup = ff_q_pvs_transport_resultmasklookuppositive * S ((S (dc_index_transport_resultmask)) * dst_positive_scale_transport_resultmasklookup) + (dst_positive_transport_resultmasklookup))) /\ (((((exists ff_h_pvs_transport_resultmasklookupnegative. ff_h_pvs_transport_resultmasklookupnegative + S (dst_negative_transport_resultmasklookup) = S ((S (dc_index_transport_resultmask)) * dst_negative_scale_transport_resultmasklookup)) /\ exists ff_q_pvs_transport_resultmasklookupnegative. dst_negative_code_transport_resultmasklookup = ff_q_pvs_transport_resultmasklookupnegative * S ((S (dc_index_transport_resultmask)) * dst_negative_scale_transport_resultmasklookup) + (dst_negative_transport_resultmasklookup))) /\ (exists ge_balance_positive_transport_resultmasklookupvalue ge_balance_negative_transport_resultmasklookupvalue. (((((dc_value_transport_resultmask) = 2 * (ge_balance_positive_transport_resultmasklookupvalue) /\ (ge_balance_negative_transport_resultmasklookupvalue) = 0) \/ exists ge_signed_half_transport_resultmasklookupvaluedecode. (((dc_value_transport_resultmask) = 2 * ge_signed_half_transport_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_transport_resultmasklookupvalue) = 0) /\ (ge_balance_negative_transport_resultmasklookupvalue) = S ge_signed_half_transport_resultmasklookupvaluedecode))) /\ ((dst_positive_transport_resultmasklookup) + ge_balance_negative_transport_resultmasklookupvalue = (dst_negative_transport_resultmasklookup) + ge_balance_positive_transport_resultmasklookupvalue))))))))) -> ((((~((dc_index_transport_resultmask)=0)) /\ (exists dc_quotient_transport_resultmaskentry dc_left_transport_resultmaskentry dc_right_transport_resultmaskentry. (((n)=(dc_index_transport_resultmask)*dc_quotient_transport_resultmaskentry) /\ (((exists dst_positive_code_transport_resultmaskentryleft dst_positive_scale_transport_resultmaskentryleft dst_negative_code_transport_resultmaskentryleft dst_negative_scale_transport_resultmaskentryleft dst_positive_transport_resultmaskentryleft dst_negative_transport_resultmaskentryleft. (((H) = (((((dst_positive_code_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft)) * S ((dst_positive_code_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft)) + ((dst_positive_scale_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft))) + (((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) * S ((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) + ((dst_negative_scale_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)))) * S ((((dst_positive_code_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft)) * S ((dst_positive_code_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft)) + ((dst_positive_scale_transport_resultmaskentryleft) + (dst_positive_scale_transport_resultmaskentryleft))) + (((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) * S ((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) + ((dst_negative_scale_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)))) + ((((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) * S ((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) + ((dst_negative_scale_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft))) + (((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) * S ((dst_negative_code_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)) + ((dst_negative_scale_transport_resultmaskentryleft) + (dst_negative_scale_transport_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_transport_resultmaskentryleftpositive. ff_h_pvs_transport_resultmaskentryleftpositive + S (dst_positive_transport_resultmaskentryleft) = S ((S (dc_index_transport_resultmask)) * dst_positive_scale_transport_resultmaskentryleft)) /\ exists ff_q_pvs_transport_resultmaskentryleftpositive. dst_positive_code_transport_resultmaskentryleft = ff_q_pvs_transport_resultmaskentryleftpositive * S ((S (dc_index_transport_resultmask)) * dst_positive_scale_transport_resultmaskentryleft) + (dst_positive_transport_resultmaskentryleft))) /\ (((((exists ff_h_pvs_transport_resultmaskentryleftnegative. ff_h_pvs_transport_resultmaskentryleftnegative + S (dst_negative_transport_resultmaskentryleft) = S ((S (dc_index_transport_resultmask)) * dst_negative_scale_transport_resultmaskentryleft)) /\ exists ff_q_pvs_transport_resultmaskentryleftnegative. dst_negative_code_transport_resultmaskentryleft = ff_q_pvs_transport_resultmaskentryleftnegative * S ((S (dc_index_transport_resultmask)) * dst_negative_scale_transport_resultmaskentryleft) + (dst_negative_transport_resultmaskentryleft))) /\ (exists ge_balance_positive_transport_resultmaskentryleftvalue ge_balance_negative_transport_resultmaskentryleftvalue. (((((dc_left_transport_resultmaskentry) = 2 * (ge_balance_positive_transport_resultmaskentryleftvalue) /\ (ge_balance_negative_transport_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_transport_resultmaskentryleftvaluedecode. (((dc_left_transport_resultmaskentry) = 2 * ge_signed_half_transport_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_transport_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_transport_resultmaskentryleftvalue) = S ge_signed_half_transport_resultmaskentryleftvaluedecode))) /\ ((dst_positive_transport_resultmaskentryleft) + ge_balance_negative_transport_resultmaskentryleftvalue = (dst_negative_transport_resultmaskentryleft) + ge_balance_positive_transport_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_transport_resultmaskentryright dst_positive_scale_transport_resultmaskentryright dst_negative_code_transport_resultmaskentryright dst_negative_scale_transport_resultmaskentryright dst_positive_transport_resultmaskentryright dst_negative_transport_resultmaskentryright. (((K) = (((((dst_positive_code_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright)) * S ((dst_positive_code_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright)) + ((dst_positive_scale_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright))) + (((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) * S ((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) + ((dst_negative_scale_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)))) * S ((((dst_positive_code_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright)) * S ((dst_positive_code_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright)) + ((dst_positive_scale_transport_resultmaskentryright) + (dst_positive_scale_transport_resultmaskentryright))) + (((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) * S ((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) + ((dst_negative_scale_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)))) + ((((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) * S ((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) + ((dst_negative_scale_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright))) + (((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) * S ((dst_negative_code_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)) + ((dst_negative_scale_transport_resultmaskentryright) + (dst_negative_scale_transport_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_transport_resultmaskentryrightpositive. ff_h_pvs_transport_resultmaskentryrightpositive + S (dst_positive_transport_resultmaskentryright) = S ((S (dc_quotient_transport_resultmaskentry)) * dst_positive_scale_transport_resultmaskentryright)) /\ exists ff_q_pvs_transport_resultmaskentryrightpositive. dst_positive_code_transport_resultmaskentryright = ff_q_pvs_transport_resultmaskentryrightpositive * S ((S (dc_quotient_transport_resultmaskentry)) * dst_positive_scale_transport_resultmaskentryright) + (dst_positive_transport_resultmaskentryright))) /\ (((((exists ff_h_pvs_transport_resultmaskentryrightnegative. ff_h_pvs_transport_resultmaskentryrightnegative + S (dst_negative_transport_resultmaskentryright) = S ((S (dc_quotient_transport_resultmaskentry)) * dst_negative_scale_transport_resultmaskentryright)) /\ exists ff_q_pvs_transport_resultmaskentryrightnegative. dst_negative_code_transport_resultmaskentryright = ff_q_pvs_transport_resultmaskentryrightnegative * S ((S (dc_quotient_transport_resultmaskentry)) * dst_negative_scale_transport_resultmaskentryright) + (dst_negative_transport_resultmaskentryright))) /\ (exists ge_balance_positive_transport_resultmaskentryrightvalue ge_balance_negative_transport_resultmaskentryrightvalue. (((((dc_right_transport_resultmaskentry) = 2 * (ge_balance_positive_transport_resultmaskentryrightvalue) /\ (ge_balance_negative_transport_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_transport_resultmaskentryrightvaluedecode. (((dc_right_transport_resultmaskentry) = 2 * ge_signed_half_transport_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_transport_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_transport_resultmaskentryrightvalue) = S ge_signed_half_transport_resultmaskentryrightvaluedecode))) /\ ((dst_positive_transport_resultmaskentryright) + ge_balance_negative_transport_resultmaskentryrightvalue = (dst_negative_transport_resultmaskentryright) + ge_balance_positive_transport_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_transport_resultmaskentryproduct sto_an_transport_resultmaskentryproduct sto_bp_transport_resultmaskentryproduct sto_bn_transport_resultmaskentryproduct sto_cp_transport_resultmaskentryproduct sto_cn_transport_resultmaskentryproduct. (((((dc_left_transport_resultmaskentry) = 2 * (sto_ap_transport_resultmaskentryproduct) /\ (sto_an_transport_resultmaskentryproduct) = 0) \/ exists ge_signed_half_transport_resultmaskentryproductleft. (((dc_left_transport_resultmaskentry) = 2 * ge_signed_half_transport_resultmaskentryproductleft + 1 /\ (sto_ap_transport_resultmaskentryproduct) = 0) /\ (sto_an_transport_resultmaskentryproduct) = S ge_signed_half_transport_resultmaskentryproductleft))) /\ ((((((dc_right_transport_resultmaskentry) = 2 * (sto_bp_transport_resultmaskentryproduct) /\ (sto_bn_transport_resultmaskentryproduct) = 0) \/ exists ge_signed_half_transport_resultmaskentryproductright. (((dc_right_transport_resultmaskentry) = 2 * ge_signed_half_transport_resultmaskentryproductright + 1 /\ (sto_bp_transport_resultmaskentryproduct) = 0) /\ (sto_bn_transport_resultmaskentryproduct) = S ge_signed_half_transport_resultmaskentryproductright))) /\ ((((((dc_value_transport_resultmask) = 2 * (sto_cp_transport_resultmaskentryproduct) /\ (sto_cn_transport_resultmaskentryproduct) = 0) \/ exists ge_signed_half_transport_resultmaskentryproductoutput. (((dc_value_transport_resultmask) = 2 * ge_signed_half_transport_resultmaskentryproductoutput + 1 /\ (sto_cp_transport_resultmaskentryproduct) = 0) /\ (sto_cn_transport_resultmaskentryproduct) = S ge_signed_half_transport_resultmaskentryproductoutput))) /\ ((sto_ap_transport_resultmaskentryproduct * sto_bp_transport_resultmaskentryproduct + sto_an_transport_resultmaskentryproduct * sto_bn_transport_resultmaskentryproduct) + sto_cn_transport_resultmaskentryproduct = (sto_ap_transport_resultmaskentryproduct * sto_bn_transport_resultmaskentryproduct + sto_an_transport_resultmaskentryproduct * sto_bp_transport_resultmaskentryproduct) + sto_cp_transport_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_transport_resultmask)=0 \/ ~(exists pvs_factor_transport_resultmaskentrynondivisor. (n) = (dc_index_transport_resultmask) * pvs_factor_transport_resultmaskentrynondivisor)) /\ ((dc_value_transport_resultmask)=0))))))) /\ (exists dst_positive_code_transport_resultfold dst_positive_scale_transport_resultfold dst_negative_code_transport_resultfold dst_negative_scale_transport_resultfold dst_positive_sum_transport_resultfold dst_negative_sum_transport_resultfold. (((dc_mask_transport_result) = (((((dst_positive_code_transport_resultfold) + (dst_positive_scale_transport_resultfold)) * S ((dst_positive_code_transport_resultfold) + (dst_positive_scale_transport_resultfold)) + ((dst_positive_scale_transport_resultfold) + (dst_positive_scale_transport_resultfold))) + (((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) * S ((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) + ((dst_negative_scale_transport_resultfold) + (dst_negative_scale_transport_resultfold)))) * S ((((dst_positive_code_transport_resultfold) + (dst_positive_scale_transport_resultfold)) * S ((dst_positive_code_transport_resultfold) + (dst_positive_scale_transport_resultfold)) + ((dst_positive_scale_transport_resultfold) + (dst_positive_scale_transport_resultfold))) + (((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) * S ((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) + ((dst_negative_scale_transport_resultfold) + (dst_negative_scale_transport_resultfold)))) + ((((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) * S ((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) + ((dst_negative_scale_transport_resultfold) + (dst_negative_scale_transport_resultfold))) + (((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) * S ((dst_negative_code_transport_resultfold) + (dst_negative_scale_transport_resultfold)) + ((dst_negative_scale_transport_resultfold) + (dst_negative_scale_transport_resultfold)))))) /\ (((exists fs_u_dst_transport_resultfoldpositive fs_v_dst_transport_resultfoldpositive. ((((exists fs_h_dst_transport_resultfoldpositive_body_start. fs_h_dst_transport_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_transport_resultfoldpositive)) /\ exists fs_q_dst_transport_resultfoldpositive_body_start. fs_u_dst_transport_resultfoldpositive = fs_q_dst_transport_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_transport_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_transport_resultfoldpositive_body_terminal. fs_h_dst_transport_resultfoldpositive_body_terminal + S (dst_positive_sum_transport_resultfold) = S ((S (S (n))) * fs_v_dst_transport_resultfoldpositive)) /\ exists fs_q_dst_transport_resultfoldpositive_body_terminal. fs_u_dst_transport_resultfoldpositive = fs_q_dst_transport_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_transport_resultfoldpositive) + (dst_positive_sum_transport_resultfold))) /\ forall fs_i_dst_transport_resultfoldpositive_body_steps. (exists fs_lt_dst_transport_resultfoldpositive_body_steps_bound. fs_lt_dst_transport_resultfoldpositive_body_steps_bound + S fs_i_dst_transport_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_transport_resultfoldpositive_body_steps fs_r_dst_transport_resultfoldpositive_body_steps fs_s_dst_transport_resultfoldpositive_body_steps. ((((exists fs_h_dst_transport_resultfoldpositive_body_steps_summand. fs_h_dst_transport_resultfoldpositive_body_steps_summand + S (fs_a_dst_transport_resultfoldpositive_body_steps) = S ((S (fs_i_dst_transport_resultfoldpositive_body_steps)) * dst_positive_scale_transport_resultfold)) /\ exists fs_q_dst_transport_resultfoldpositive_body_steps_summand. dst_positive_code_transport_resultfold = fs_q_dst_transport_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_transport_resultfoldpositive_body_steps)) * dst_positive_scale_transport_resultfold) + (fs_a_dst_transport_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transport_resultfoldpositive_body_steps_partial. fs_h_dst_transport_resultfoldpositive_body_steps_partial + S (fs_r_dst_transport_resultfoldpositive_body_steps) = S ((S (fs_i_dst_transport_resultfoldpositive_body_steps)) * fs_v_dst_transport_resultfoldpositive)) /\ exists fs_q_dst_transport_resultfoldpositive_body_steps_partial. fs_u_dst_transport_resultfoldpositive = fs_q_dst_transport_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_transport_resultfoldpositive_body_steps)) * fs_v_dst_transport_resultfoldpositive) + (fs_r_dst_transport_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_transport_resultfoldpositive_body_steps_successor. fs_h_dst_transport_resultfoldpositive_body_steps_successor + S (fs_s_dst_transport_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_transport_resultfoldpositive_body_steps)) * fs_v_dst_transport_resultfoldpositive)) /\ exists fs_q_dst_transport_resultfoldpositive_body_steps_successor. fs_u_dst_transport_resultfoldpositive = fs_q_dst_transport_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_transport_resultfoldpositive_body_steps)) * fs_v_dst_transport_resultfoldpositive) + (fs_s_dst_transport_resultfoldpositive_body_steps))) /\ fs_s_dst_transport_resultfoldpositive_body_steps = fs_r_dst_transport_resultfoldpositive_body_steps + fs_a_dst_transport_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_transport_resultfoldnegative fs_v_dst_transport_resultfoldnegative. ((((exists fs_h_dst_transport_resultfoldnegative_body_start. fs_h_dst_transport_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_transport_resultfoldnegative)) /\ exists fs_q_dst_transport_resultfoldnegative_body_start. fs_u_dst_transport_resultfoldnegative = fs_q_dst_transport_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_transport_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_transport_resultfoldnegative_body_terminal. fs_h_dst_transport_resultfoldnegative_body_terminal + S (dst_negative_sum_transport_resultfold) = S ((S (S (n))) * fs_v_dst_transport_resultfoldnegative)) /\ exists fs_q_dst_transport_resultfoldnegative_body_terminal. fs_u_dst_transport_resultfoldnegative = fs_q_dst_transport_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_transport_resultfoldnegative) + (dst_negative_sum_transport_resultfold))) /\ forall fs_i_dst_transport_resultfoldnegative_body_steps. (exists fs_lt_dst_transport_resultfoldnegative_body_steps_bound. fs_lt_dst_transport_resultfoldnegative_body_steps_bound + S fs_i_dst_transport_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_transport_resultfoldnegative_body_steps fs_r_dst_transport_resultfoldnegative_body_steps fs_s_dst_transport_resultfoldnegative_body_steps. ((((exists fs_h_dst_transport_resultfoldnegative_body_steps_summand. fs_h_dst_transport_resultfoldnegative_body_steps_summand + S (fs_a_dst_transport_resultfoldnegative_body_steps) = S ((S (fs_i_dst_transport_resultfoldnegative_body_steps)) * dst_negative_scale_transport_resultfold)) /\ exists fs_q_dst_transport_resultfoldnegative_body_steps_summand. dst_negative_code_transport_resultfold = fs_q_dst_transport_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_transport_resultfoldnegative_body_steps)) * dst_negative_scale_transport_resultfold) + (fs_a_dst_transport_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transport_resultfoldnegative_body_steps_partial. fs_h_dst_transport_resultfoldnegative_body_steps_partial + S (fs_r_dst_transport_resultfoldnegative_body_steps) = S ((S (fs_i_dst_transport_resultfoldnegative_body_steps)) * fs_v_dst_transport_resultfoldnegative)) /\ exists fs_q_dst_transport_resultfoldnegative_body_steps_partial. fs_u_dst_transport_resultfoldnegative = fs_q_dst_transport_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_transport_resultfoldnegative_body_steps)) * fs_v_dst_transport_resultfoldnegative) + (fs_r_dst_transport_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_transport_resultfoldnegative_body_steps_successor. fs_h_dst_transport_resultfoldnegative_body_steps_successor + S (fs_s_dst_transport_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_transport_resultfoldnegative_body_steps)) * fs_v_dst_transport_resultfoldnegative)) /\ exists fs_q_dst_transport_resultfoldnegative_body_steps_successor. fs_u_dst_transport_resultfoldnegative = fs_q_dst_transport_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_transport_resultfoldnegative_body_steps)) * fs_v_dst_transport_resultfoldnegative) + (fs_s_dst_transport_resultfoldnegative_body_steps))) /\ fs_s_dst_transport_resultfoldnegative_body_steps = fs_r_dst_transport_resultfoldnegative_body_steps + fs_a_dst_transport_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_transport_resultfoldresult ge_balance_negative_transport_resultfoldresult. (((((z) = 2 * (ge_balance_positive_transport_resultfoldresult) /\ (ge_balance_negative_transport_resultfoldresult) = 0) \/ exists ge_signed_half_transport_resultfoldresultdecode. (((z) = 2 * ge_signed_half_transport_resultfoldresultdecode + 1 /\ (ge_balance_positive_transport_resultfoldresult) = 0) /\ (ge_balance_negative_transport_resultfoldresult) = S ge_signed_half_transport_resultfoldresultdecode))) /\ ((dst_positive_sum_transport_resultfold) + ge_balance_negative_transport_resultfoldresult = (dst_negative_sum_transport_resultfold) + ge_balance_positive_transport_resultfoldresult)))))))))))))