Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ H. ∀ K. ∀ n. ∀ z. ArithTable(N,H) → ArithTable(N,K) → Le(n,N) → ArithPositiveEqual(F,H,n) → ArithPositiveEqual(G,K,n) → DirichletSum(F,G,n,z) → DirichletSum(H,K,n,z)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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)))))))))))))Complete tactic proof in conservative notation
All 41 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
41 script commands · 9 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–13
03Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases hz
04Establish huL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution sum exists.
- L15
have hu : ∃ u. DirichletSum(H,K,n,u)Definitions: DirichletSum(H,K,n,u)Original native command in the exact edition - L16
specialize dirichlet_convolution_sum_exists (N) - L17
specialize dirichlet_convolution_sum_exists (H) - L18
specialize dirichlet_convolution_sum_exists (K) - L19
specialize dirichlet_convolution_sum_exists (n) - L20
apply dirichlet_convolution_sum_exists - L21
exact hH - L22
exact hK - L23
exact hz_left - L24
exact hbound
05Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
cases hu
06Establish heqL26–35
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution positive source extensional.
- L26
have heq : z=x - L27
specialize dirichlet_convolution_positive_source_extensional (F) - L28
specialize dirichlet_convolution_positive_source_extensional (G) - L29
specialize dirichlet_convolution_positive_source_extensional (H) - L30
specialize dirichlet_convolution_positive_source_extensional (K) - L31
specialize dirichlet_convolution_positive_source_extensional (n) - L32
specialize dirichlet_convolution_positive_source_extensional (z) - L33
specialize dirichlet_convolution_positive_source_extensional (x) - L34
apply dirichlet_convolution_positive_source_extensional - L35
exact hF
07Use earlier factsL36–38
08Calculate and transport equalitiesL39–40
09Use earlier factsL41–41
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hu_witness
Original defined command ledger · 41 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro K - 0006
intro n - 0007
intro z - 0008
intro hH - 0009
intro hK - 0010
intro hbound - 0011
intro hF - 0012
intro hG - 0013
intro hz - 0014
cases hz - 0015
have hu : ∃ u. DirichletSum(H,K,n,u) - 0016
specialize dirichlet_convolution_sum_exists (N) - 0017
specialize dirichlet_convolution_sum_exists (H) - 0018
specialize dirichlet_convolution_sum_exists (K) - 0019
specialize dirichlet_convolution_sum_exists (n) - 0020
apply dirichlet_convolution_sum_exists - 0021
exact hH - 0022
exact hK - 0023
exact hz_left - 0024
exact hbound - 0025
cases hu - 0026
have heq : z=x - 0027
specialize dirichlet_convolution_positive_source_extensional (F) - 0028
specialize dirichlet_convolution_positive_source_extensional (G) - 0029
specialize dirichlet_convolution_positive_source_extensional (H) - 0030
specialize dirichlet_convolution_positive_source_extensional (K) - 0031
specialize dirichlet_convolution_positive_source_extensional (n) - 0032
specialize dirichlet_convolution_positive_source_extensional (z) - 0033
specialize dirichlet_convolution_positive_source_extensional (x) - 0034
apply dirichlet_convolution_positive_source_extensional - 0035
exact hF - 0036
exact hG - 0037
exact hz - 0038
exact hu_witness - 0039
rewrite heq - 0040
rewrite heq - 0041
exact hu_witness