signed_cartesian_product_extensional_unique

Exact expanded first-order arithmetic statement

forall F G T U m n. (((exists dst_positive_code_unique_firstF dst_positive_scale_unique_firstF dst_negative_code_unique_firstF dst_negative_scale_unique_firstF. (((F) = (((((dst_positive_code_unique_firstF) + (dst_positive_scale_unique_firstF)) * S ((dst_positive_code_unique_firstF) + (dst_positive_scale_unique_firstF)) + ((dst_positive_scale_unique_firstF) + (dst_positive_scale_unique_firstF))) + (((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) * S ((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) + ((dst_negative_scale_unique_firstF) + (dst_negative_scale_unique_firstF)))) * S ((((dst_positive_code_unique_firstF) + (dst_positive_scale_unique_firstF)) * S ((dst_positive_code_unique_firstF) + (dst_positive_scale_unique_firstF)) + ((dst_positive_scale_unique_firstF) + (dst_positive_scale_unique_firstF))) + (((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) * S ((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) + ((dst_negative_scale_unique_firstF) + (dst_negative_scale_unique_firstF)))) + ((((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) * S ((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) + ((dst_negative_scale_unique_firstF) + (dst_negative_scale_unique_firstF))) + (((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) * S ((dst_negative_code_unique_firstF) + (dst_negative_scale_unique_firstF)) + ((dst_negative_scale_unique_firstF) + (dst_negative_scale_unique_firstF)))))) /\ (forall dst_index_unique_firstF. (exists pvs_le_gap_unique_firstFdomain. pvs_le_gap_unique_firstFdomain + (dst_index_unique_firstF) = (0)) -> exists dst_positive_unique_firstF dst_negative_unique_firstF dst_value_unique_firstF. ((((exists ff_h_pvs_unique_firstFentrypositive. ff_h_pvs_unique_firstFentrypositive + S (dst_positive_unique_firstF) = S ((S (dst_index_unique_firstF)) * dst_positive_scale_unique_firstF)) /\ exists ff_q_pvs_unique_firstFentrypositive. dst_positive_code_unique_firstF = ff_q_pvs_unique_firstFentrypositive * S ((S (dst_index_unique_firstF)) * dst_positive_scale_unique_firstF) + (dst_positive_unique_firstF))) /\ (((((exists ff_h_pvs_unique_firstFentrynegative. ff_h_pvs_unique_firstFentrynegative + S (dst_negative_unique_firstF) = S ((S (dst_index_unique_firstF)) * dst_negative_scale_unique_firstF)) /\ exists ff_q_pvs_unique_firstFentrynegative. dst_negative_code_unique_firstF = ff_q_pvs_unique_firstFentrynegative * S ((S (dst_index_unique_firstF)) * dst_negative_scale_unique_firstF) + (dst_negative_unique_firstF))) /\ (exists ge_balance_positive_unique_firstFentryvalue ge_balance_negative_unique_firstFentryvalue. (((((dst_value_unique_firstF) = 2 * (ge_balance_positive_unique_firstFentryvalue) /\ (ge_balance_negative_unique_firstFentryvalue) = 0) \/ exists ge_signed_half_unique_firstFentryvaluedecode. (((dst_value_unique_firstF) = 2 * ge_signed_half_unique_firstFentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstFentryvalue) = 0) /\ (ge_balance_negative_unique_firstFentryvalue) = S ge_signed_half_unique_firstFentryvaluedecode))) /\ ((dst_positive_unique_firstF) + ge_balance_negative_unique_firstFentryvalue = (dst_negative_unique_firstF) + ge_balance_positive_unique_firstFentryvalue))))))))) /\ (((exists dst_positive_code_unique_firstG dst_positive_scale_unique_firstG dst_negative_code_unique_firstG dst_negative_scale_unique_firstG. (((G) = (((((dst_positive_code_unique_firstG) + (dst_positive_scale_unique_firstG)) * S ((dst_positive_code_unique_firstG) + (dst_positive_scale_unique_firstG)) + ((dst_positive_scale_unique_firstG) + (dst_positive_scale_unique_firstG))) + (((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) * S ((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) + ((dst_negative_scale_unique_firstG) + (dst_negative_scale_unique_firstG)))) * S ((((dst_positive_code_unique_firstG) + (dst_positive_scale_unique_firstG)) * S ((dst_positive_code_unique_firstG) + (dst_positive_scale_unique_firstG)) + ((dst_positive_scale_unique_firstG) + (dst_positive_scale_unique_firstG))) + (((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) * S ((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) + ((dst_negative_scale_unique_firstG) + (dst_negative_scale_unique_firstG)))) + ((((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) * S ((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) + ((dst_negative_scale_unique_firstG) + (dst_negative_scale_unique_firstG))) + (((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) * S ((dst_negative_code_unique_firstG) + (dst_negative_scale_unique_firstG)) + ((dst_negative_scale_unique_firstG) + (dst_negative_scale_unique_firstG)))))) /\ (forall dst_index_unique_firstG. (exists pvs_le_gap_unique_firstGdomain. pvs_le_gap_unique_firstGdomain + (dst_index_unique_firstG) = (0)) -> exists dst_positive_unique_firstG dst_negative_unique_firstG dst_value_unique_firstG. ((((exists ff_h_pvs_unique_firstGentrypositive. ff_h_pvs_unique_firstGentrypositive + S (dst_positive_unique_firstG) = S ((S (dst_index_unique_firstG)) * dst_positive_scale_unique_firstG)) /\ exists ff_q_pvs_unique_firstGentrypositive. dst_positive_code_unique_firstG = ff_q_pvs_unique_firstGentrypositive * S ((S (dst_index_unique_firstG)) * dst_positive_scale_unique_firstG) + (dst_positive_unique_firstG))) /\ (((((exists ff_h_pvs_unique_firstGentrynegative. ff_h_pvs_unique_firstGentrynegative + S (dst_negative_unique_firstG) = S ((S (dst_index_unique_firstG)) * dst_negative_scale_unique_firstG)) /\ exists ff_q_pvs_unique_firstGentrynegative. dst_negative_code_unique_firstG = ff_q_pvs_unique_firstGentrynegative * S ((S (dst_index_unique_firstG)) * dst_negative_scale_unique_firstG) + (dst_negative_unique_firstG))) /\ (exists ge_balance_positive_unique_firstGentryvalue ge_balance_negative_unique_firstGentryvalue. (((((dst_value_unique_firstG) = 2 * (ge_balance_positive_unique_firstGentryvalue) /\ (ge_balance_negative_unique_firstGentryvalue) = 0) \/ exists ge_signed_half_unique_firstGentryvaluedecode. (((dst_value_unique_firstG) = 2 * ge_signed_half_unique_firstGentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstGentryvalue) = 0) /\ (ge_balance_negative_unique_firstGentryvalue) = S ge_signed_half_unique_firstGentryvaluedecode))) /\ ((dst_positive_unique_firstG) + ge_balance_negative_unique_firstGentryvalue = (dst_negative_unique_firstG) + ge_balance_positive_unique_firstGentryvalue))))))))) /\ (((exists dst_positive_code_unique_firstT dst_positive_scale_unique_firstT dst_negative_code_unique_firstT dst_negative_scale_unique_firstT. (((T) = (((((dst_positive_code_unique_firstT) + (dst_positive_scale_unique_firstT)) * S ((dst_positive_code_unique_firstT) + (dst_positive_scale_unique_firstT)) + ((dst_positive_scale_unique_firstT) + (dst_positive_scale_unique_firstT))) + (((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) * S ((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) + ((dst_negative_scale_unique_firstT) + (dst_negative_scale_unique_firstT)))) * S ((((dst_positive_code_unique_firstT) + (dst_positive_scale_unique_firstT)) * S ((dst_positive_code_unique_firstT) + (dst_positive_scale_unique_firstT)) + ((dst_positive_scale_unique_firstT) + (dst_positive_scale_unique_firstT))) + (((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) * S ((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) + ((dst_negative_scale_unique_firstT) + (dst_negative_scale_unique_firstT)))) + ((((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) * S ((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) + ((dst_negative_scale_unique_firstT) + (dst_negative_scale_unique_firstT))) + (((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) * S ((dst_negative_code_unique_firstT) + (dst_negative_scale_unique_firstT)) + ((dst_negative_scale_unique_firstT) + (dst_negative_scale_unique_firstT)))))) /\ (forall dst_index_unique_firstT. (exists pvs_le_gap_unique_firstTdomain. pvs_le_gap_unique_firstTdomain + (dst_index_unique_firstT) = ((m)*(n))) -> exists dst_positive_unique_firstT dst_negative_unique_firstT dst_value_unique_firstT. ((((exists ff_h_pvs_unique_firstTentrypositive. ff_h_pvs_unique_firstTentrypositive + S (dst_positive_unique_firstT) = S ((S (dst_index_unique_firstT)) * dst_positive_scale_unique_firstT)) /\ exists ff_q_pvs_unique_firstTentrypositive. dst_positive_code_unique_firstT = ff_q_pvs_unique_firstTentrypositive * S ((S (dst_index_unique_firstT)) * dst_positive_scale_unique_firstT) + (dst_positive_unique_firstT))) /\ (((((exists ff_h_pvs_unique_firstTentrynegative. ff_h_pvs_unique_firstTentrynegative + S (dst_negative_unique_firstT) = S ((S (dst_index_unique_firstT)) * dst_negative_scale_unique_firstT)) /\ exists ff_q_pvs_unique_firstTentrynegative. dst_negative_code_unique_firstT = ff_q_pvs_unique_firstTentrynegative * S ((S (dst_index_unique_firstT)) * dst_negative_scale_unique_firstT) + (dst_negative_unique_firstT))) /\ (exists ge_balance_positive_unique_firstTentryvalue ge_balance_negative_unique_firstTentryvalue. (((((dst_value_unique_firstT) = 2 * (ge_balance_positive_unique_firstTentryvalue) /\ (ge_balance_negative_unique_firstTentryvalue) = 0) \/ exists ge_signed_half_unique_firstTentryvaluedecode. (((dst_value_unique_firstT) = 2 * ge_signed_half_unique_firstTentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstTentryvalue) = 0) /\ (ge_balance_negative_unique_firstTentryvalue) = S ge_signed_half_unique_firstTentryvaluedecode))) /\ ((dst_positive_unique_firstT) + ge_balance_negative_unique_firstTentryvalue = (dst_negative_unique_firstT) + ge_balance_positive_unique_firstTentryvalue))))))))) /\ (forall scp_row_unique_first scp_column_unique_first scp_first_unique_first scp_second_unique_first scp_value_unique_first. (exists pvs_gap_unique_firstrows. pvs_gap_unique_firstrows + S (scp_row_unique_first) = (m)) -> (exists pvs_gap_unique_firstcolumns. pvs_gap_unique_firstcolumns + S (scp_column_unique_first) = (n)) -> (exists dst_positive_code_unique_firstfirst dst_positive_scale_unique_firstfirst dst_negative_code_unique_firstfirst dst_negative_scale_unique_firstfirst dst_positive_unique_firstfirst dst_negative_unique_firstfirst. (((F) = (((((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) * S ((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) + ((dst_positive_scale_unique_firstfirst) + (dst_positive_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))) * S ((((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) * S ((dst_positive_code_unique_firstfirst) + (dst_positive_scale_unique_firstfirst)) + ((dst_positive_scale_unique_firstfirst) + (dst_positive_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))) + ((((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst))) + (((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) * S ((dst_negative_code_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)) + ((dst_negative_scale_unique_firstfirst) + (dst_negative_scale_unique_firstfirst)))))) /\ (((((exists ff_h_pvs_unique_firstfirstpositive. ff_h_pvs_unique_firstfirstpositive + S (dst_positive_unique_firstfirst) = S ((S (scp_row_unique_first)) * dst_positive_scale_unique_firstfirst)) /\ exists ff_q_pvs_unique_firstfirstpositive. dst_positive_code_unique_firstfirst = ff_q_pvs_unique_firstfirstpositive * S ((S (scp_row_unique_first)) * dst_positive_scale_unique_firstfirst) + (dst_positive_unique_firstfirst))) /\ (((((exists ff_h_pvs_unique_firstfirstnegative. ff_h_pvs_unique_firstfirstnegative + S (dst_negative_unique_firstfirst) = S ((S (scp_row_unique_first)) * dst_negative_scale_unique_firstfirst)) /\ exists ff_q_pvs_unique_firstfirstnegative. dst_negative_code_unique_firstfirst = ff_q_pvs_unique_firstfirstnegative * S ((S (scp_row_unique_first)) * dst_negative_scale_unique_firstfirst) + (dst_negative_unique_firstfirst))) /\ (exists ge_balance_positive_unique_firstfirstvalue ge_balance_negative_unique_firstfirstvalue. (((((scp_first_unique_first) = 2 * (ge_balance_positive_unique_firstfirstvalue) /\ (ge_balance_negative_unique_firstfirstvalue) = 0) \/ exists ge_signed_half_unique_firstfirstvaluedecode. (((scp_first_unique_first) = 2 * ge_signed_half_unique_firstfirstvaluedecode + 1 /\ (ge_balance_positive_unique_firstfirstvalue) = 0) /\ (ge_balance_negative_unique_firstfirstvalue) = S ge_signed_half_unique_firstfirstvaluedecode))) /\ ((dst_positive_unique_firstfirst) + ge_balance_negative_unique_firstfirstvalue = (dst_negative_unique_firstfirst) + ge_balance_positive_unique_firstfirstvalue))))))))) -> (exists dst_positive_code_unique_firstsecond dst_positive_scale_unique_firstsecond dst_negative_code_unique_firstsecond dst_negative_scale_unique_firstsecond dst_positive_unique_firstsecond dst_negative_unique_firstsecond. (((G) = (((((dst_positive_code_unique_firstsecond) + (dst_positive_scale_unique_firstsecond)) * S ((dst_positive_code_unique_firstsecond) + (dst_positive_scale_unique_firstsecond)) + ((dst_positive_scale_unique_firstsecond) + (dst_positive_scale_unique_firstsecond))) + (((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) * S ((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) + ((dst_negative_scale_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)))) * S ((((dst_positive_code_unique_firstsecond) + (dst_positive_scale_unique_firstsecond)) * S ((dst_positive_code_unique_firstsecond) + (dst_positive_scale_unique_firstsecond)) + ((dst_positive_scale_unique_firstsecond) + (dst_positive_scale_unique_firstsecond))) + (((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) * S ((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) + ((dst_negative_scale_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)))) + ((((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) * S ((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) + ((dst_negative_scale_unique_firstsecond) + (dst_negative_scale_unique_firstsecond))) + (((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) * S ((dst_negative_code_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)) + ((dst_negative_scale_unique_firstsecond) + (dst_negative_scale_unique_firstsecond)))))) /\ (((((exists ff_h_pvs_unique_firstsecondpositive. ff_h_pvs_unique_firstsecondpositive + S (dst_positive_unique_firstsecond) = S ((S (scp_column_unique_first)) * dst_positive_scale_unique_firstsecond)) /\ exists ff_q_pvs_unique_firstsecondpositive. dst_positive_code_unique_firstsecond = ff_q_pvs_unique_firstsecondpositive * S ((S (scp_column_unique_first)) * dst_positive_scale_unique_firstsecond) + (dst_positive_unique_firstsecond))) /\ (((((exists ff_h_pvs_unique_firstsecondnegative. ff_h_pvs_unique_firstsecondnegative + S (dst_negative_unique_firstsecond) = S ((S (scp_column_unique_first)) * dst_negative_scale_unique_firstsecond)) /\ exists ff_q_pvs_unique_firstsecondnegative. dst_negative_code_unique_firstsecond = ff_q_pvs_unique_firstsecondnegative * S ((S (scp_column_unique_first)) * dst_negative_scale_unique_firstsecond) + (dst_negative_unique_firstsecond))) /\ (exists ge_balance_positive_unique_firstsecondvalue ge_balance_negative_unique_firstsecondvalue. (((((scp_second_unique_first) = 2 * (ge_balance_positive_unique_firstsecondvalue) /\ (ge_balance_negative_unique_firstsecondvalue) = 0) \/ exists ge_signed_half_unique_firstsecondvaluedecode. (((scp_second_unique_first) = 2 * ge_signed_half_unique_firstsecondvaluedecode + 1 /\ (ge_balance_positive_unique_firstsecondvalue) = 0) /\ (ge_balance_negative_unique_firstsecondvalue) = S ge_signed_half_unique_firstsecondvaluedecode))) /\ ((dst_positive_unique_firstsecond) + ge_balance_negative_unique_firstsecondvalue = (dst_negative_unique_firstsecond) + ge_balance_positive_unique_firstsecondvalue))))))))) -> (exists dst_positive_code_unique_firstentry dst_positive_scale_unique_firstentry dst_negative_code_unique_firstentry dst_negative_scale_unique_firstentry dst_positive_unique_firstentry dst_negative_unique_firstentry. (((T) = (((((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) * S ((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) + ((dst_positive_scale_unique_firstentry) + (dst_positive_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))) * S ((((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) * S ((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) + ((dst_positive_scale_unique_firstentry) + (dst_positive_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))) + ((((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))))) /\ (((((exists ff_h_pvs_unique_firstentrypositive. ff_h_pvs_unique_firstentrypositive + S (dst_positive_unique_firstentry) = S ((S (((n)*(scp_row_unique_first)+(scp_column_unique_first)))) * dst_positive_scale_unique_firstentry)) /\ exists ff_q_pvs_unique_firstentrypositive. dst_positive_code_unique_firstentry = ff_q_pvs_unique_firstentrypositive * S ((S (((n)*(scp_row_unique_first)+(scp_column_unique_first)))) * dst_positive_scale_unique_firstentry) + (dst_positive_unique_firstentry))) /\ (((((exists ff_h_pvs_unique_firstentrynegative. ff_h_pvs_unique_firstentrynegative + S (dst_negative_unique_firstentry) = S ((S (((n)*(scp_row_unique_first)+(scp_column_unique_first)))) * dst_negative_scale_unique_firstentry)) /\ exists ff_q_pvs_unique_firstentrynegative. dst_negative_code_unique_firstentry = ff_q_pvs_unique_firstentrynegative * S ((S (((n)*(scp_row_unique_first)+(scp_column_unique_first)))) * dst_negative_scale_unique_firstentry) + (dst_negative_unique_firstentry))) /\ (exists ge_balance_positive_unique_firstentryvalue ge_balance_negative_unique_firstentryvalue. (((((scp_value_unique_first) = 2 * (ge_balance_positive_unique_firstentryvalue) /\ (ge_balance_negative_unique_firstentryvalue) = 0) \/ exists ge_signed_half_unique_firstentryvaluedecode. (((scp_value_unique_first) = 2 * ge_signed_half_unique_firstentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstentryvalue) = 0) /\ (ge_balance_negative_unique_firstentryvalue) = S ge_signed_half_unique_firstentryvaluedecode))) /\ ((dst_positive_unique_firstentry) + ge_balance_negative_unique_firstentryvalue = (dst_negative_unique_firstentry) + ge_balance_positive_unique_firstentryvalue))))))))) -> (exists sto_ap_unique_firstmultiply sto_an_unique_firstmultiply sto_bp_unique_firstmultiply sto_bn_unique_firstmultiply sto_cp_unique_firstmultiply sto_cn_unique_firstmultiply. (((((scp_first_unique_first) = 2 * (sto_ap_unique_firstmultiply) /\ (sto_an_unique_firstmultiply) = 0) \/ exists ge_signed_half_unique_firstmultiplyleft. (((scp_first_unique_first) = 2 * ge_signed_half_unique_firstmultiplyleft + 1 /\ (sto_ap_unique_firstmultiply) = 0) /\ (sto_an_unique_firstmultiply) = S ge_signed_half_unique_firstmultiplyleft))) /\ ((((((scp_second_unique_first) = 2 * (sto_bp_unique_firstmultiply) /\ (sto_bn_unique_firstmultiply) = 0) \/ exists ge_signed_half_unique_firstmultiplyright. (((scp_second_unique_first) = 2 * ge_signed_half_unique_firstmultiplyright + 1 /\ (sto_bp_unique_firstmultiply) = 0) /\ (sto_bn_unique_firstmultiply) = S ge_signed_half_unique_firstmultiplyright))) /\ ((((((scp_value_unique_first) = 2 * (sto_cp_unique_firstmultiply) /\ (sto_cn_unique_firstmultiply) = 0) \/ exists ge_signed_half_unique_firstmultiplyoutput. (((scp_value_unique_first) = 2 * ge_signed_half_unique_firstmultiplyoutput + 1 /\ (sto_cp_unique_firstmultiply) = 0) /\ (sto_cn_unique_firstmultiply) = S ge_signed_half_unique_firstmultiplyoutput))) /\ ((sto_ap_unique_firstmultiply * sto_bp_unique_firstmultiply + sto_an_unique_firstmultiply * sto_bn_unique_firstmultiply) + sto_cn_unique_firstmultiply = (sto_ap_unique_firstmultiply * sto_bn_unique_firstmultiply + sto_an_unique_firstmultiply * sto_bp_unique_firstmultiply) + sto_cp_unique_firstmultiply)))))))))))))) -> (((exists dst_positive_code_unique_secondF dst_positive_scale_unique_secondF dst_negative_code_unique_secondF dst_negative_scale_unique_secondF. (((F) = (((((dst_positive_code_unique_secondF) + (dst_positive_scale_unique_secondF)) * S ((dst_positive_code_unique_secondF) + (dst_positive_scale_unique_secondF)) + ((dst_positive_scale_unique_secondF) + (dst_positive_scale_unique_secondF))) + (((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) * S ((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) + ((dst_negative_scale_unique_secondF) + (dst_negative_scale_unique_secondF)))) * S ((((dst_positive_code_unique_secondF) + (dst_positive_scale_unique_secondF)) * S ((dst_positive_code_unique_secondF) + (dst_positive_scale_unique_secondF)) + ((dst_positive_scale_unique_secondF) + (dst_positive_scale_unique_secondF))) + (((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) * S ((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) + ((dst_negative_scale_unique_secondF) + (dst_negative_scale_unique_secondF)))) + ((((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) * S ((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) + ((dst_negative_scale_unique_secondF) + (dst_negative_scale_unique_secondF))) + (((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) * S ((dst_negative_code_unique_secondF) + (dst_negative_scale_unique_secondF)) + ((dst_negative_scale_unique_secondF) + (dst_negative_scale_unique_secondF)))))) /\ (forall dst_index_unique_secondF. (exists pvs_le_gap_unique_secondFdomain. pvs_le_gap_unique_secondFdomain + (dst_index_unique_secondF) = (0)) -> exists dst_positive_unique_secondF dst_negative_unique_secondF dst_value_unique_secondF. ((((exists ff_h_pvs_unique_secondFentrypositive. ff_h_pvs_unique_secondFentrypositive + S (dst_positive_unique_secondF) = S ((S (dst_index_unique_secondF)) * dst_positive_scale_unique_secondF)) /\ exists ff_q_pvs_unique_secondFentrypositive. dst_positive_code_unique_secondF = ff_q_pvs_unique_secondFentrypositive * S ((S (dst_index_unique_secondF)) * dst_positive_scale_unique_secondF) + (dst_positive_unique_secondF))) /\ (((((exists ff_h_pvs_unique_secondFentrynegative. ff_h_pvs_unique_secondFentrynegative + S (dst_negative_unique_secondF) = S ((S (dst_index_unique_secondF)) * dst_negative_scale_unique_secondF)) /\ exists ff_q_pvs_unique_secondFentrynegative. dst_negative_code_unique_secondF = ff_q_pvs_unique_secondFentrynegative * S ((S (dst_index_unique_secondF)) * dst_negative_scale_unique_secondF) + (dst_negative_unique_secondF))) /\ (exists ge_balance_positive_unique_secondFentryvalue ge_balance_negative_unique_secondFentryvalue. (((((dst_value_unique_secondF) = 2 * (ge_balance_positive_unique_secondFentryvalue) /\ (ge_balance_negative_unique_secondFentryvalue) = 0) \/ exists ge_signed_half_unique_secondFentryvaluedecode. (((dst_value_unique_secondF) = 2 * ge_signed_half_unique_secondFentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondFentryvalue) = 0) /\ (ge_balance_negative_unique_secondFentryvalue) = S ge_signed_half_unique_secondFentryvaluedecode))) /\ ((dst_positive_unique_secondF) + ge_balance_negative_unique_secondFentryvalue = (dst_negative_unique_secondF) + ge_balance_positive_unique_secondFentryvalue))))))))) /\ (((exists dst_positive_code_unique_secondG dst_positive_scale_unique_secondG dst_negative_code_unique_secondG dst_negative_scale_unique_secondG. (((G) = (((((dst_positive_code_unique_secondG) + (dst_positive_scale_unique_secondG)) * S ((dst_positive_code_unique_secondG) + (dst_positive_scale_unique_secondG)) + ((dst_positive_scale_unique_secondG) + (dst_positive_scale_unique_secondG))) + (((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) * S ((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) + ((dst_negative_scale_unique_secondG) + (dst_negative_scale_unique_secondG)))) * S ((((dst_positive_code_unique_secondG) + (dst_positive_scale_unique_secondG)) * S ((dst_positive_code_unique_secondG) + (dst_positive_scale_unique_secondG)) + ((dst_positive_scale_unique_secondG) + (dst_positive_scale_unique_secondG))) + (((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) * S ((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) + ((dst_negative_scale_unique_secondG) + (dst_negative_scale_unique_secondG)))) + ((((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) * S ((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) + ((dst_negative_scale_unique_secondG) + (dst_negative_scale_unique_secondG))) + (((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) * S ((dst_negative_code_unique_secondG) + (dst_negative_scale_unique_secondG)) + ((dst_negative_scale_unique_secondG) + (dst_negative_scale_unique_secondG)))))) /\ (forall dst_index_unique_secondG. (exists pvs_le_gap_unique_secondGdomain. pvs_le_gap_unique_secondGdomain + (dst_index_unique_secondG) = (0)) -> exists dst_positive_unique_secondG dst_negative_unique_secondG dst_value_unique_secondG. ((((exists ff_h_pvs_unique_secondGentrypositive. ff_h_pvs_unique_secondGentrypositive + S (dst_positive_unique_secondG) = S ((S (dst_index_unique_secondG)) * dst_positive_scale_unique_secondG)) /\ exists ff_q_pvs_unique_secondGentrypositive. dst_positive_code_unique_secondG = ff_q_pvs_unique_secondGentrypositive * S ((S (dst_index_unique_secondG)) * dst_positive_scale_unique_secondG) + (dst_positive_unique_secondG))) /\ (((((exists ff_h_pvs_unique_secondGentrynegative. ff_h_pvs_unique_secondGentrynegative + S (dst_negative_unique_secondG) = S ((S (dst_index_unique_secondG)) * dst_negative_scale_unique_secondG)) /\ exists ff_q_pvs_unique_secondGentrynegative. dst_negative_code_unique_secondG = ff_q_pvs_unique_secondGentrynegative * S ((S (dst_index_unique_secondG)) * dst_negative_scale_unique_secondG) + (dst_negative_unique_secondG))) /\ (exists ge_balance_positive_unique_secondGentryvalue ge_balance_negative_unique_secondGentryvalue. (((((dst_value_unique_secondG) = 2 * (ge_balance_positive_unique_secondGentryvalue) /\ (ge_balance_negative_unique_secondGentryvalue) = 0) \/ exists ge_signed_half_unique_secondGentryvaluedecode. (((dst_value_unique_secondG) = 2 * ge_signed_half_unique_secondGentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondGentryvalue) = 0) /\ (ge_balance_negative_unique_secondGentryvalue) = S ge_signed_half_unique_secondGentryvaluedecode))) /\ ((dst_positive_unique_secondG) + ge_balance_negative_unique_secondGentryvalue = (dst_negative_unique_secondG) + ge_balance_positive_unique_secondGentryvalue))))))))) /\ (((exists dst_positive_code_unique_secondT dst_positive_scale_unique_secondT dst_negative_code_unique_secondT dst_negative_scale_unique_secondT. (((U) = (((((dst_positive_code_unique_secondT) + (dst_positive_scale_unique_secondT)) * S ((dst_positive_code_unique_secondT) + (dst_positive_scale_unique_secondT)) + ((dst_positive_scale_unique_secondT) + (dst_positive_scale_unique_secondT))) + (((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) * S ((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) + ((dst_negative_scale_unique_secondT) + (dst_negative_scale_unique_secondT)))) * S ((((dst_positive_code_unique_secondT) + (dst_positive_scale_unique_secondT)) * S ((dst_positive_code_unique_secondT) + (dst_positive_scale_unique_secondT)) + ((dst_positive_scale_unique_secondT) + (dst_positive_scale_unique_secondT))) + (((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) * S ((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) + ((dst_negative_scale_unique_secondT) + (dst_negative_scale_unique_secondT)))) + ((((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) * S ((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) + ((dst_negative_scale_unique_secondT) + (dst_negative_scale_unique_secondT))) + (((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) * S ((dst_negative_code_unique_secondT) + (dst_negative_scale_unique_secondT)) + ((dst_negative_scale_unique_secondT) + (dst_negative_scale_unique_secondT)))))) /\ (forall dst_index_unique_secondT. (exists pvs_le_gap_unique_secondTdomain. pvs_le_gap_unique_secondTdomain + (dst_index_unique_secondT) = ((m)*(n))) -> exists dst_positive_unique_secondT dst_negative_unique_secondT dst_value_unique_secondT. ((((exists ff_h_pvs_unique_secondTentrypositive. ff_h_pvs_unique_secondTentrypositive + S (dst_positive_unique_secondT) = S ((S (dst_index_unique_secondT)) * dst_positive_scale_unique_secondT)) /\ exists ff_q_pvs_unique_secondTentrypositive. dst_positive_code_unique_secondT = ff_q_pvs_unique_secondTentrypositive * S ((S (dst_index_unique_secondT)) * dst_positive_scale_unique_secondT) + (dst_positive_unique_secondT))) /\ (((((exists ff_h_pvs_unique_secondTentrynegative. ff_h_pvs_unique_secondTentrynegative + S (dst_negative_unique_secondT) = S ((S (dst_index_unique_secondT)) * dst_negative_scale_unique_secondT)) /\ exists ff_q_pvs_unique_secondTentrynegative. dst_negative_code_unique_secondT = ff_q_pvs_unique_secondTentrynegative * S ((S (dst_index_unique_secondT)) * dst_negative_scale_unique_secondT) + (dst_negative_unique_secondT))) /\ (exists ge_balance_positive_unique_secondTentryvalue ge_balance_negative_unique_secondTentryvalue. (((((dst_value_unique_secondT) = 2 * (ge_balance_positive_unique_secondTentryvalue) /\ (ge_balance_negative_unique_secondTentryvalue) = 0) \/ exists ge_signed_half_unique_secondTentryvaluedecode. (((dst_value_unique_secondT) = 2 * ge_signed_half_unique_secondTentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondTentryvalue) = 0) /\ (ge_balance_negative_unique_secondTentryvalue) = S ge_signed_half_unique_secondTentryvaluedecode))) /\ ((dst_positive_unique_secondT) + ge_balance_negative_unique_secondTentryvalue = (dst_negative_unique_secondT) + ge_balance_positive_unique_secondTentryvalue))))))))) /\ (forall scp_row_unique_second scp_column_unique_second scp_first_unique_second scp_second_unique_second scp_value_unique_second. (exists pvs_gap_unique_secondrows. pvs_gap_unique_secondrows + S (scp_row_unique_second) = (m)) -> (exists pvs_gap_unique_secondcolumns. pvs_gap_unique_secondcolumns + S (scp_column_unique_second) = (n)) -> (exists dst_positive_code_unique_secondfirst dst_positive_scale_unique_secondfirst dst_negative_code_unique_secondfirst dst_negative_scale_unique_secondfirst dst_positive_unique_secondfirst dst_negative_unique_secondfirst. (((F) = (((((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) * S ((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) + ((dst_positive_scale_unique_secondfirst) + (dst_positive_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))) * S ((((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) * S ((dst_positive_code_unique_secondfirst) + (dst_positive_scale_unique_secondfirst)) + ((dst_positive_scale_unique_secondfirst) + (dst_positive_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))) + ((((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst))) + (((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) * S ((dst_negative_code_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)) + ((dst_negative_scale_unique_secondfirst) + (dst_negative_scale_unique_secondfirst)))))) /\ (((((exists ff_h_pvs_unique_secondfirstpositive. ff_h_pvs_unique_secondfirstpositive + S (dst_positive_unique_secondfirst) = S ((S (scp_row_unique_second)) * dst_positive_scale_unique_secondfirst)) /\ exists ff_q_pvs_unique_secondfirstpositive. dst_positive_code_unique_secondfirst = ff_q_pvs_unique_secondfirstpositive * S ((S (scp_row_unique_second)) * dst_positive_scale_unique_secondfirst) + (dst_positive_unique_secondfirst))) /\ (((((exists ff_h_pvs_unique_secondfirstnegative. ff_h_pvs_unique_secondfirstnegative + S (dst_negative_unique_secondfirst) = S ((S (scp_row_unique_second)) * dst_negative_scale_unique_secondfirst)) /\ exists ff_q_pvs_unique_secondfirstnegative. dst_negative_code_unique_secondfirst = ff_q_pvs_unique_secondfirstnegative * S ((S (scp_row_unique_second)) * dst_negative_scale_unique_secondfirst) + (dst_negative_unique_secondfirst))) /\ (exists ge_balance_positive_unique_secondfirstvalue ge_balance_negative_unique_secondfirstvalue. (((((scp_first_unique_second) = 2 * (ge_balance_positive_unique_secondfirstvalue) /\ (ge_balance_negative_unique_secondfirstvalue) = 0) \/ exists ge_signed_half_unique_secondfirstvaluedecode. (((scp_first_unique_second) = 2 * ge_signed_half_unique_secondfirstvaluedecode + 1 /\ (ge_balance_positive_unique_secondfirstvalue) = 0) /\ (ge_balance_negative_unique_secondfirstvalue) = S ge_signed_half_unique_secondfirstvaluedecode))) /\ ((dst_positive_unique_secondfirst) + ge_balance_negative_unique_secondfirstvalue = (dst_negative_unique_secondfirst) + ge_balance_positive_unique_secondfirstvalue))))))))) -> (exists dst_positive_code_unique_secondsecond dst_positive_scale_unique_secondsecond dst_negative_code_unique_secondsecond dst_negative_scale_unique_secondsecond dst_positive_unique_secondsecond dst_negative_unique_secondsecond. (((G) = (((((dst_positive_code_unique_secondsecond) + (dst_positive_scale_unique_secondsecond)) * S ((dst_positive_code_unique_secondsecond) + (dst_positive_scale_unique_secondsecond)) + ((dst_positive_scale_unique_secondsecond) + (dst_positive_scale_unique_secondsecond))) + (((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) * S ((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) + ((dst_negative_scale_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)))) * S ((((dst_positive_code_unique_secondsecond) + (dst_positive_scale_unique_secondsecond)) * S ((dst_positive_code_unique_secondsecond) + (dst_positive_scale_unique_secondsecond)) + ((dst_positive_scale_unique_secondsecond) + (dst_positive_scale_unique_secondsecond))) + (((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) * S ((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) + ((dst_negative_scale_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)))) + ((((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) * S ((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) + ((dst_negative_scale_unique_secondsecond) + (dst_negative_scale_unique_secondsecond))) + (((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) * S ((dst_negative_code_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)) + ((dst_negative_scale_unique_secondsecond) + (dst_negative_scale_unique_secondsecond)))))) /\ (((((exists ff_h_pvs_unique_secondsecondpositive. ff_h_pvs_unique_secondsecondpositive + S (dst_positive_unique_secondsecond) = S ((S (scp_column_unique_second)) * dst_positive_scale_unique_secondsecond)) /\ exists ff_q_pvs_unique_secondsecondpositive. dst_positive_code_unique_secondsecond = ff_q_pvs_unique_secondsecondpositive * S ((S (scp_column_unique_second)) * dst_positive_scale_unique_secondsecond) + (dst_positive_unique_secondsecond))) /\ (((((exists ff_h_pvs_unique_secondsecondnegative. ff_h_pvs_unique_secondsecondnegative + S (dst_negative_unique_secondsecond) = S ((S (scp_column_unique_second)) * dst_negative_scale_unique_secondsecond)) /\ exists ff_q_pvs_unique_secondsecondnegative. dst_negative_code_unique_secondsecond = ff_q_pvs_unique_secondsecondnegative * S ((S (scp_column_unique_second)) * dst_negative_scale_unique_secondsecond) + (dst_negative_unique_secondsecond))) /\ (exists ge_balance_positive_unique_secondsecondvalue ge_balance_negative_unique_secondsecondvalue. (((((scp_second_unique_second) = 2 * (ge_balance_positive_unique_secondsecondvalue) /\ (ge_balance_negative_unique_secondsecondvalue) = 0) \/ exists ge_signed_half_unique_secondsecondvaluedecode. (((scp_second_unique_second) = 2 * ge_signed_half_unique_secondsecondvaluedecode + 1 /\ (ge_balance_positive_unique_secondsecondvalue) = 0) /\ (ge_balance_negative_unique_secondsecondvalue) = S ge_signed_half_unique_secondsecondvaluedecode))) /\ ((dst_positive_unique_secondsecond) + ge_balance_negative_unique_secondsecondvalue = (dst_negative_unique_secondsecond) + ge_balance_positive_unique_secondsecondvalue))))))))) -> (exists dst_positive_code_unique_secondentry dst_positive_scale_unique_secondentry dst_negative_code_unique_secondentry dst_negative_scale_unique_secondentry dst_positive_unique_secondentry dst_negative_unique_secondentry. (((U) = (((((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) * S ((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) + ((dst_positive_scale_unique_secondentry) + (dst_positive_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))) * S ((((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) * S ((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) + ((dst_positive_scale_unique_secondentry) + (dst_positive_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))) + ((((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))))) /\ (((((exists ff_h_pvs_unique_secondentrypositive. ff_h_pvs_unique_secondentrypositive + S (dst_positive_unique_secondentry) = S ((S (((n)*(scp_row_unique_second)+(scp_column_unique_second)))) * dst_positive_scale_unique_secondentry)) /\ exists ff_q_pvs_unique_secondentrypositive. dst_positive_code_unique_secondentry = ff_q_pvs_unique_secondentrypositive * S ((S (((n)*(scp_row_unique_second)+(scp_column_unique_second)))) * dst_positive_scale_unique_secondentry) + (dst_positive_unique_secondentry))) /\ (((((exists ff_h_pvs_unique_secondentrynegative. ff_h_pvs_unique_secondentrynegative + S (dst_negative_unique_secondentry) = S ((S (((n)*(scp_row_unique_second)+(scp_column_unique_second)))) * dst_negative_scale_unique_secondentry)) /\ exists ff_q_pvs_unique_secondentrynegative. dst_negative_code_unique_secondentry = ff_q_pvs_unique_secondentrynegative * S ((S (((n)*(scp_row_unique_second)+(scp_column_unique_second)))) * dst_negative_scale_unique_secondentry) + (dst_negative_unique_secondentry))) /\ (exists ge_balance_positive_unique_secondentryvalue ge_balance_negative_unique_secondentryvalue. (((((scp_value_unique_second) = 2 * (ge_balance_positive_unique_secondentryvalue) /\ (ge_balance_negative_unique_secondentryvalue) = 0) \/ exists ge_signed_half_unique_secondentryvaluedecode. (((scp_value_unique_second) = 2 * ge_signed_half_unique_secondentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondentryvalue) = 0) /\ (ge_balance_negative_unique_secondentryvalue) = S ge_signed_half_unique_secondentryvaluedecode))) /\ ((dst_positive_unique_secondentry) + ge_balance_negative_unique_secondentryvalue = (dst_negative_unique_secondentry) + ge_balance_positive_unique_secondentryvalue))))))))) -> (exists sto_ap_unique_secondmultiply sto_an_unique_secondmultiply sto_bp_unique_secondmultiply sto_bn_unique_secondmultiply sto_cp_unique_secondmultiply sto_cn_unique_secondmultiply. (((((scp_first_unique_second) = 2 * (sto_ap_unique_secondmultiply) /\ (sto_an_unique_secondmultiply) = 0) \/ exists ge_signed_half_unique_secondmultiplyleft. (((scp_first_unique_second) = 2 * ge_signed_half_unique_secondmultiplyleft + 1 /\ (sto_ap_unique_secondmultiply) = 0) /\ (sto_an_unique_secondmultiply) = S ge_signed_half_unique_secondmultiplyleft))) /\ ((((((scp_second_unique_second) = 2 * (sto_bp_unique_secondmultiply) /\ (sto_bn_unique_secondmultiply) = 0) \/ exists ge_signed_half_unique_secondmultiplyright. (((scp_second_unique_second) = 2 * ge_signed_half_unique_secondmultiplyright + 1 /\ (sto_bp_unique_secondmultiply) = 0) /\ (sto_bn_unique_secondmultiply) = S ge_signed_half_unique_secondmultiplyright))) /\ ((((((scp_value_unique_second) = 2 * (sto_cp_unique_secondmultiply) /\ (sto_cn_unique_secondmultiply) = 0) \/ exists ge_signed_half_unique_secondmultiplyoutput. (((scp_value_unique_second) = 2 * ge_signed_half_unique_secondmultiplyoutput + 1 /\ (sto_cp_unique_secondmultiply) = 0) /\ (sto_cn_unique_secondmultiply) = S ge_signed_half_unique_secondmultiplyoutput))) /\ ((sto_ap_unique_secondmultiply * sto_bp_unique_secondmultiply + sto_an_unique_secondmultiply * sto_bn_unique_secondmultiply) + sto_cn_unique_secondmultiply = (sto_ap_unique_secondmultiply * sto_bn_unique_secondmultiply + sto_an_unique_secondmultiply * sto_bp_unique_secondmultiply) + sto_cp_unique_secondmultiply)))))))))))))) -> (forall dst_index_unique_result dst_first_unique_result dst_second_unique_result. (exists pvs_gap_unique_resultbound. pvs_gap_unique_resultbound + S (dst_index_unique_result) = (m*n)) -> (exists dst_positive_code_unique_resultfirst dst_positive_scale_unique_resultfirst dst_negative_code_unique_resultfirst dst_negative_scale_unique_resultfirst dst_positive_unique_resultfirst dst_negative_unique_resultfirst. (((T) = (((((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) * S ((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) + ((dst_positive_scale_unique_resultfirst) + (dst_positive_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))) * S ((((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) * S ((dst_positive_code_unique_resultfirst) + (dst_positive_scale_unique_resultfirst)) + ((dst_positive_scale_unique_resultfirst) + (dst_positive_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))) + ((((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst))) + (((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) * S ((dst_negative_code_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)) + ((dst_negative_scale_unique_resultfirst) + (dst_negative_scale_unique_resultfirst)))))) /\ (((((exists ff_h_pvs_unique_resultfirstpositive. ff_h_pvs_unique_resultfirstpositive + S (dst_positive_unique_resultfirst) = S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultfirst)) /\ exists ff_q_pvs_unique_resultfirstpositive. dst_positive_code_unique_resultfirst = ff_q_pvs_unique_resultfirstpositive * S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultfirst) + (dst_positive_unique_resultfirst))) /\ (((((exists ff_h_pvs_unique_resultfirstnegative. ff_h_pvs_unique_resultfirstnegative + S (dst_negative_unique_resultfirst) = S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultfirst)) /\ exists ff_q_pvs_unique_resultfirstnegative. dst_negative_code_unique_resultfirst = ff_q_pvs_unique_resultfirstnegative * S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultfirst) + (dst_negative_unique_resultfirst))) /\ (exists ge_balance_positive_unique_resultfirstvalue ge_balance_negative_unique_resultfirstvalue. (((((dst_first_unique_result) = 2 * (ge_balance_positive_unique_resultfirstvalue) /\ (ge_balance_negative_unique_resultfirstvalue) = 0) \/ exists ge_signed_half_unique_resultfirstvaluedecode. (((dst_first_unique_result) = 2 * ge_signed_half_unique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_unique_resultfirstvalue) = 0) /\ (ge_balance_negative_unique_resultfirstvalue) = S ge_signed_half_unique_resultfirstvaluedecode))) /\ ((dst_positive_unique_resultfirst) + ge_balance_negative_unique_resultfirstvalue = (dst_negative_unique_resultfirst) + ge_balance_positive_unique_resultfirstvalue))))))))) -> (exists dst_positive_code_unique_resultsecond dst_positive_scale_unique_resultsecond dst_negative_code_unique_resultsecond dst_negative_scale_unique_resultsecond dst_positive_unique_resultsecond dst_negative_unique_resultsecond. (((U) = (((((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) * S ((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) + ((dst_positive_scale_unique_resultsecond) + (dst_positive_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))) * S ((((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) * S ((dst_positive_code_unique_resultsecond) + (dst_positive_scale_unique_resultsecond)) + ((dst_positive_scale_unique_resultsecond) + (dst_positive_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))) + ((((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond))) + (((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) * S ((dst_negative_code_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)) + ((dst_negative_scale_unique_resultsecond) + (dst_negative_scale_unique_resultsecond)))))) /\ (((((exists ff_h_pvs_unique_resultsecondpositive. ff_h_pvs_unique_resultsecondpositive + S (dst_positive_unique_resultsecond) = S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultsecond)) /\ exists ff_q_pvs_unique_resultsecondpositive. dst_positive_code_unique_resultsecond = ff_q_pvs_unique_resultsecondpositive * S ((S (dst_index_unique_result)) * dst_positive_scale_unique_resultsecond) + (dst_positive_unique_resultsecond))) /\ (((((exists ff_h_pvs_unique_resultsecondnegative. ff_h_pvs_unique_resultsecondnegative + S (dst_negative_unique_resultsecond) = S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultsecond)) /\ exists ff_q_pvs_unique_resultsecondnegative. dst_negative_code_unique_resultsecond = ff_q_pvs_unique_resultsecondnegative * S ((S (dst_index_unique_result)) * dst_negative_scale_unique_resultsecond) + (dst_negative_unique_resultsecond))) /\ (exists ge_balance_positive_unique_resultsecondvalue ge_balance_negative_unique_resultsecondvalue. (((((dst_second_unique_result) = 2 * (ge_balance_positive_unique_resultsecondvalue) /\ (ge_balance_negative_unique_resultsecondvalue) = 0) \/ exists ge_signed_half_unique_resultsecondvaluedecode. (((dst_second_unique_result) = 2 * ge_signed_half_unique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_unique_resultsecondvalue) = 0) /\ (ge_balance_negative_unique_resultsecondvalue) = S ge_signed_half_unique_resultsecondvaluedecode))) /\ ((dst_positive_unique_resultsecond) + ge_balance_negative_unique_resultsecondvalue = (dst_negative_unique_resultsecond) + ge_balance_positive_unique_resultsecondvalue))))))))) -> dst_first_unique_result = dst_second_unique_result)