signed_cartesian_product_reencode

Exact expanded first-order arithmetic statement

forall F G T U m n. (((exists dst_positive_code_reencode_sourceF dst_positive_scale_reencode_sourceF dst_negative_code_reencode_sourceF dst_negative_scale_reencode_sourceF. (((F) = (((((dst_positive_code_reencode_sourceF) + (dst_positive_scale_reencode_sourceF)) * S ((dst_positive_code_reencode_sourceF) + (dst_positive_scale_reencode_sourceF)) + ((dst_positive_scale_reencode_sourceF) + (dst_positive_scale_reencode_sourceF))) + (((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) * S ((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) + ((dst_negative_scale_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)))) * S ((((dst_positive_code_reencode_sourceF) + (dst_positive_scale_reencode_sourceF)) * S ((dst_positive_code_reencode_sourceF) + (dst_positive_scale_reencode_sourceF)) + ((dst_positive_scale_reencode_sourceF) + (dst_positive_scale_reencode_sourceF))) + (((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) * S ((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) + ((dst_negative_scale_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)))) + ((((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) * S ((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) + ((dst_negative_scale_reencode_sourceF) + (dst_negative_scale_reencode_sourceF))) + (((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) * S ((dst_negative_code_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)) + ((dst_negative_scale_reencode_sourceF) + (dst_negative_scale_reencode_sourceF)))))) /\ (forall dst_index_reencode_sourceF. (exists pvs_le_gap_reencode_sourceFdomain. pvs_le_gap_reencode_sourceFdomain + (dst_index_reencode_sourceF) = (0)) -> exists dst_positive_reencode_sourceF dst_negative_reencode_sourceF dst_value_reencode_sourceF. ((((exists ff_h_pvs_reencode_sourceFentrypositive. ff_h_pvs_reencode_sourceFentrypositive + S (dst_positive_reencode_sourceF) = S ((S (dst_index_reencode_sourceF)) * dst_positive_scale_reencode_sourceF)) /\ exists ff_q_pvs_reencode_sourceFentrypositive. dst_positive_code_reencode_sourceF = ff_q_pvs_reencode_sourceFentrypositive * S ((S (dst_index_reencode_sourceF)) * dst_positive_scale_reencode_sourceF) + (dst_positive_reencode_sourceF))) /\ (((((exists ff_h_pvs_reencode_sourceFentrynegative. ff_h_pvs_reencode_sourceFentrynegative + S (dst_negative_reencode_sourceF) = S ((S (dst_index_reencode_sourceF)) * dst_negative_scale_reencode_sourceF)) /\ exists ff_q_pvs_reencode_sourceFentrynegative. dst_negative_code_reencode_sourceF = ff_q_pvs_reencode_sourceFentrynegative * S ((S (dst_index_reencode_sourceF)) * dst_negative_scale_reencode_sourceF) + (dst_negative_reencode_sourceF))) /\ (exists ge_balance_positive_reencode_sourceFentryvalue ge_balance_negative_reencode_sourceFentryvalue. (((((dst_value_reencode_sourceF) = 2 * (ge_balance_positive_reencode_sourceFentryvalue) /\ (ge_balance_negative_reencode_sourceFentryvalue) = 0) \/ exists ge_signed_half_reencode_sourceFentryvaluedecode. (((dst_value_reencode_sourceF) = 2 * ge_signed_half_reencode_sourceFentryvaluedecode + 1 /\ (ge_balance_positive_reencode_sourceFentryvalue) = 0) /\ (ge_balance_negative_reencode_sourceFentryvalue) = S ge_signed_half_reencode_sourceFentryvaluedecode))) /\ ((dst_positive_reencode_sourceF) + ge_balance_negative_reencode_sourceFentryvalue = (dst_negative_reencode_sourceF) + ge_balance_positive_reencode_sourceFentryvalue))))))))) /\ (((exists dst_positive_code_reencode_sourceG dst_positive_scale_reencode_sourceG dst_negative_code_reencode_sourceG dst_negative_scale_reencode_sourceG. (((G) = (((((dst_positive_code_reencode_sourceG) + (dst_positive_scale_reencode_sourceG)) * S ((dst_positive_code_reencode_sourceG) + (dst_positive_scale_reencode_sourceG)) + ((dst_positive_scale_reencode_sourceG) + (dst_positive_scale_reencode_sourceG))) + (((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) * S ((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) + ((dst_negative_scale_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)))) * S ((((dst_positive_code_reencode_sourceG) + (dst_positive_scale_reencode_sourceG)) * S ((dst_positive_code_reencode_sourceG) + (dst_positive_scale_reencode_sourceG)) + ((dst_positive_scale_reencode_sourceG) + (dst_positive_scale_reencode_sourceG))) + (((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) * S ((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) + ((dst_negative_scale_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)))) + ((((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) * S ((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) + ((dst_negative_scale_reencode_sourceG) + (dst_negative_scale_reencode_sourceG))) + (((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) * S ((dst_negative_code_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)) + ((dst_negative_scale_reencode_sourceG) + (dst_negative_scale_reencode_sourceG)))))) /\ (forall dst_index_reencode_sourceG. (exists pvs_le_gap_reencode_sourceGdomain. pvs_le_gap_reencode_sourceGdomain + (dst_index_reencode_sourceG) = (0)) -> exists dst_positive_reencode_sourceG dst_negative_reencode_sourceG dst_value_reencode_sourceG. ((((exists ff_h_pvs_reencode_sourceGentrypositive. ff_h_pvs_reencode_sourceGentrypositive + S (dst_positive_reencode_sourceG) = S ((S (dst_index_reencode_sourceG)) * dst_positive_scale_reencode_sourceG)) /\ exists ff_q_pvs_reencode_sourceGentrypositive. dst_positive_code_reencode_sourceG = ff_q_pvs_reencode_sourceGentrypositive * S ((S (dst_index_reencode_sourceG)) * dst_positive_scale_reencode_sourceG) + (dst_positive_reencode_sourceG))) /\ (((((exists ff_h_pvs_reencode_sourceGentrynegative. ff_h_pvs_reencode_sourceGentrynegative + S (dst_negative_reencode_sourceG) = S ((S (dst_index_reencode_sourceG)) * dst_negative_scale_reencode_sourceG)) /\ exists ff_q_pvs_reencode_sourceGentrynegative. dst_negative_code_reencode_sourceG = ff_q_pvs_reencode_sourceGentrynegative * S ((S (dst_index_reencode_sourceG)) * dst_negative_scale_reencode_sourceG) + (dst_negative_reencode_sourceG))) /\ (exists ge_balance_positive_reencode_sourceGentryvalue ge_balance_negative_reencode_sourceGentryvalue. (((((dst_value_reencode_sourceG) = 2 * (ge_balance_positive_reencode_sourceGentryvalue) /\ (ge_balance_negative_reencode_sourceGentryvalue) = 0) \/ exists ge_signed_half_reencode_sourceGentryvaluedecode. (((dst_value_reencode_sourceG) = 2 * ge_signed_half_reencode_sourceGentryvaluedecode + 1 /\ (ge_balance_positive_reencode_sourceGentryvalue) = 0) /\ (ge_balance_negative_reencode_sourceGentryvalue) = S ge_signed_half_reencode_sourceGentryvaluedecode))) /\ ((dst_positive_reencode_sourceG) + ge_balance_negative_reencode_sourceGentryvalue = (dst_negative_reencode_sourceG) + ge_balance_positive_reencode_sourceGentryvalue))))))))) /\ (((exists dst_positive_code_reencode_sourceT dst_positive_scale_reencode_sourceT dst_negative_code_reencode_sourceT dst_negative_scale_reencode_sourceT. (((T) = (((((dst_positive_code_reencode_sourceT) + (dst_positive_scale_reencode_sourceT)) * S ((dst_positive_code_reencode_sourceT) + (dst_positive_scale_reencode_sourceT)) + ((dst_positive_scale_reencode_sourceT) + (dst_positive_scale_reencode_sourceT))) + (((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) * S ((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) + ((dst_negative_scale_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)))) * S ((((dst_positive_code_reencode_sourceT) + (dst_positive_scale_reencode_sourceT)) * S ((dst_positive_code_reencode_sourceT) + (dst_positive_scale_reencode_sourceT)) + ((dst_positive_scale_reencode_sourceT) + (dst_positive_scale_reencode_sourceT))) + (((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) * S ((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) + ((dst_negative_scale_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)))) + ((((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) * S ((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) + ((dst_negative_scale_reencode_sourceT) + (dst_negative_scale_reencode_sourceT))) + (((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) * S ((dst_negative_code_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)) + ((dst_negative_scale_reencode_sourceT) + (dst_negative_scale_reencode_sourceT)))))) /\ (forall dst_index_reencode_sourceT. (exists pvs_le_gap_reencode_sourceTdomain. pvs_le_gap_reencode_sourceTdomain + (dst_index_reencode_sourceT) = ((m)*(n))) -> exists dst_positive_reencode_sourceT dst_negative_reencode_sourceT dst_value_reencode_sourceT. ((((exists ff_h_pvs_reencode_sourceTentrypositive. ff_h_pvs_reencode_sourceTentrypositive + S (dst_positive_reencode_sourceT) = S ((S (dst_index_reencode_sourceT)) * dst_positive_scale_reencode_sourceT)) /\ exists ff_q_pvs_reencode_sourceTentrypositive. dst_positive_code_reencode_sourceT = ff_q_pvs_reencode_sourceTentrypositive * S ((S (dst_index_reencode_sourceT)) * dst_positive_scale_reencode_sourceT) + (dst_positive_reencode_sourceT))) /\ (((((exists ff_h_pvs_reencode_sourceTentrynegative. ff_h_pvs_reencode_sourceTentrynegative + S (dst_negative_reencode_sourceT) = S ((S (dst_index_reencode_sourceT)) * dst_negative_scale_reencode_sourceT)) /\ exists ff_q_pvs_reencode_sourceTentrynegative. dst_negative_code_reencode_sourceT = ff_q_pvs_reencode_sourceTentrynegative * S ((S (dst_index_reencode_sourceT)) * dst_negative_scale_reencode_sourceT) + (dst_negative_reencode_sourceT))) /\ (exists ge_balance_positive_reencode_sourceTentryvalue ge_balance_negative_reencode_sourceTentryvalue. (((((dst_value_reencode_sourceT) = 2 * (ge_balance_positive_reencode_sourceTentryvalue) /\ (ge_balance_negative_reencode_sourceTentryvalue) = 0) \/ exists ge_signed_half_reencode_sourceTentryvaluedecode. (((dst_value_reencode_sourceT) = 2 * ge_signed_half_reencode_sourceTentryvaluedecode + 1 /\ (ge_balance_positive_reencode_sourceTentryvalue) = 0) /\ (ge_balance_negative_reencode_sourceTentryvalue) = S ge_signed_half_reencode_sourceTentryvaluedecode))) /\ ((dst_positive_reencode_sourceT) + ge_balance_negative_reencode_sourceTentryvalue = (dst_negative_reencode_sourceT) + ge_balance_positive_reencode_sourceTentryvalue))))))))) /\ (forall scp_row_reencode_source scp_column_reencode_source scp_first_reencode_source scp_second_reencode_source scp_value_reencode_source. (exists pvs_gap_reencode_sourcerows. pvs_gap_reencode_sourcerows + S (scp_row_reencode_source) = (m)) -> (exists pvs_gap_reencode_sourcecolumns. pvs_gap_reencode_sourcecolumns + S (scp_column_reencode_source) = (n)) -> (exists dst_positive_code_reencode_sourcefirst dst_positive_scale_reencode_sourcefirst dst_negative_code_reencode_sourcefirst dst_negative_scale_reencode_sourcefirst dst_positive_reencode_sourcefirst dst_negative_reencode_sourcefirst. (((F) = (((((dst_positive_code_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst)) * S ((dst_positive_code_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst)) + ((dst_positive_scale_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst))) + (((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) * S ((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) + ((dst_negative_scale_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)))) * S ((((dst_positive_code_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst)) * S ((dst_positive_code_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst)) + ((dst_positive_scale_reencode_sourcefirst) + (dst_positive_scale_reencode_sourcefirst))) + (((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) * S ((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) + ((dst_negative_scale_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)))) + ((((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) * S ((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) + ((dst_negative_scale_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst))) + (((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) * S ((dst_negative_code_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)) + ((dst_negative_scale_reencode_sourcefirst) + (dst_negative_scale_reencode_sourcefirst)))))) /\ (((((exists ff_h_pvs_reencode_sourcefirstpositive. ff_h_pvs_reencode_sourcefirstpositive + S (dst_positive_reencode_sourcefirst) = S ((S (scp_row_reencode_source)) * dst_positive_scale_reencode_sourcefirst)) /\ exists ff_q_pvs_reencode_sourcefirstpositive. dst_positive_code_reencode_sourcefirst = ff_q_pvs_reencode_sourcefirstpositive * S ((S (scp_row_reencode_source)) * dst_positive_scale_reencode_sourcefirst) + (dst_positive_reencode_sourcefirst))) /\ (((((exists ff_h_pvs_reencode_sourcefirstnegative. ff_h_pvs_reencode_sourcefirstnegative + S (dst_negative_reencode_sourcefirst) = S ((S (scp_row_reencode_source)) * dst_negative_scale_reencode_sourcefirst)) /\ exists ff_q_pvs_reencode_sourcefirstnegative. dst_negative_code_reencode_sourcefirst = ff_q_pvs_reencode_sourcefirstnegative * S ((S (scp_row_reencode_source)) * dst_negative_scale_reencode_sourcefirst) + (dst_negative_reencode_sourcefirst))) /\ (exists ge_balance_positive_reencode_sourcefirstvalue ge_balance_negative_reencode_sourcefirstvalue. (((((scp_first_reencode_source) = 2 * (ge_balance_positive_reencode_sourcefirstvalue) /\ (ge_balance_negative_reencode_sourcefirstvalue) = 0) \/ exists ge_signed_half_reencode_sourcefirstvaluedecode. (((scp_first_reencode_source) = 2 * ge_signed_half_reencode_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_reencode_sourcefirstvalue) = 0) /\ (ge_balance_negative_reencode_sourcefirstvalue) = S ge_signed_half_reencode_sourcefirstvaluedecode))) /\ ((dst_positive_reencode_sourcefirst) + ge_balance_negative_reencode_sourcefirstvalue = (dst_negative_reencode_sourcefirst) + ge_balance_positive_reencode_sourcefirstvalue))))))))) -> (exists dst_positive_code_reencode_sourcesecond dst_positive_scale_reencode_sourcesecond dst_negative_code_reencode_sourcesecond dst_negative_scale_reencode_sourcesecond dst_positive_reencode_sourcesecond dst_negative_reencode_sourcesecond. (((G) = (((((dst_positive_code_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond)) * S ((dst_positive_code_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond)) + ((dst_positive_scale_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond))) + (((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) * S ((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) + ((dst_negative_scale_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)))) * S ((((dst_positive_code_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond)) * S ((dst_positive_code_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond)) + ((dst_positive_scale_reencode_sourcesecond) + (dst_positive_scale_reencode_sourcesecond))) + (((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) * S ((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) + ((dst_negative_scale_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)))) + ((((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) * S ((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) + ((dst_negative_scale_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond))) + (((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) * S ((dst_negative_code_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)) + ((dst_negative_scale_reencode_sourcesecond) + (dst_negative_scale_reencode_sourcesecond)))))) /\ (((((exists ff_h_pvs_reencode_sourcesecondpositive. ff_h_pvs_reencode_sourcesecondpositive + S (dst_positive_reencode_sourcesecond) = S ((S (scp_column_reencode_source)) * dst_positive_scale_reencode_sourcesecond)) /\ exists ff_q_pvs_reencode_sourcesecondpositive. dst_positive_code_reencode_sourcesecond = ff_q_pvs_reencode_sourcesecondpositive * S ((S (scp_column_reencode_source)) * dst_positive_scale_reencode_sourcesecond) + (dst_positive_reencode_sourcesecond))) /\ (((((exists ff_h_pvs_reencode_sourcesecondnegative. ff_h_pvs_reencode_sourcesecondnegative + S (dst_negative_reencode_sourcesecond) = S ((S (scp_column_reencode_source)) * dst_negative_scale_reencode_sourcesecond)) /\ exists ff_q_pvs_reencode_sourcesecondnegative. dst_negative_code_reencode_sourcesecond = ff_q_pvs_reencode_sourcesecondnegative * S ((S (scp_column_reencode_source)) * dst_negative_scale_reencode_sourcesecond) + (dst_negative_reencode_sourcesecond))) /\ (exists ge_balance_positive_reencode_sourcesecondvalue ge_balance_negative_reencode_sourcesecondvalue. (((((scp_second_reencode_source) = 2 * (ge_balance_positive_reencode_sourcesecondvalue) /\ (ge_balance_negative_reencode_sourcesecondvalue) = 0) \/ exists ge_signed_half_reencode_sourcesecondvaluedecode. (((scp_second_reencode_source) = 2 * ge_signed_half_reencode_sourcesecondvaluedecode + 1 /\ (ge_balance_positive_reencode_sourcesecondvalue) = 0) /\ (ge_balance_negative_reencode_sourcesecondvalue) = S ge_signed_half_reencode_sourcesecondvaluedecode))) /\ ((dst_positive_reencode_sourcesecond) + ge_balance_negative_reencode_sourcesecondvalue = (dst_negative_reencode_sourcesecond) + ge_balance_positive_reencode_sourcesecondvalue))))))))) -> (exists dst_positive_code_reencode_sourceentry dst_positive_scale_reencode_sourceentry dst_negative_code_reencode_sourceentry dst_negative_scale_reencode_sourceentry dst_positive_reencode_sourceentry dst_negative_reencode_sourceentry. (((T) = (((((dst_positive_code_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry)) * S ((dst_positive_code_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry)) + ((dst_positive_scale_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry))) + (((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) * S ((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) + ((dst_negative_scale_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)))) * S ((((dst_positive_code_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry)) * S ((dst_positive_code_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry)) + ((dst_positive_scale_reencode_sourceentry) + (dst_positive_scale_reencode_sourceentry))) + (((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) * S ((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) + ((dst_negative_scale_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)))) + ((((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) * S ((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) + ((dst_negative_scale_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry))) + (((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) * S ((dst_negative_code_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)) + ((dst_negative_scale_reencode_sourceentry) + (dst_negative_scale_reencode_sourceentry)))))) /\ (((((exists ff_h_pvs_reencode_sourceentrypositive. ff_h_pvs_reencode_sourceentrypositive + S (dst_positive_reencode_sourceentry) = S ((S (((n)*(scp_row_reencode_source)+(scp_column_reencode_source)))) * dst_positive_scale_reencode_sourceentry)) /\ exists ff_q_pvs_reencode_sourceentrypositive. dst_positive_code_reencode_sourceentry = ff_q_pvs_reencode_sourceentrypositive * S ((S (((n)*(scp_row_reencode_source)+(scp_column_reencode_source)))) * dst_positive_scale_reencode_sourceentry) + (dst_positive_reencode_sourceentry))) /\ (((((exists ff_h_pvs_reencode_sourceentrynegative. ff_h_pvs_reencode_sourceentrynegative + S (dst_negative_reencode_sourceentry) = S ((S (((n)*(scp_row_reencode_source)+(scp_column_reencode_source)))) * dst_negative_scale_reencode_sourceentry)) /\ exists ff_q_pvs_reencode_sourceentrynegative. dst_negative_code_reencode_sourceentry = ff_q_pvs_reencode_sourceentrynegative * S ((S (((n)*(scp_row_reencode_source)+(scp_column_reencode_source)))) * dst_negative_scale_reencode_sourceentry) + (dst_negative_reencode_sourceentry))) /\ (exists ge_balance_positive_reencode_sourceentryvalue ge_balance_negative_reencode_sourceentryvalue. (((((scp_value_reencode_source) = 2 * (ge_balance_positive_reencode_sourceentryvalue) /\ (ge_balance_negative_reencode_sourceentryvalue) = 0) \/ exists ge_signed_half_reencode_sourceentryvaluedecode. (((scp_value_reencode_source) = 2 * ge_signed_half_reencode_sourceentryvaluedecode + 1 /\ (ge_balance_positive_reencode_sourceentryvalue) = 0) /\ (ge_balance_negative_reencode_sourceentryvalue) = S ge_signed_half_reencode_sourceentryvaluedecode))) /\ ((dst_positive_reencode_sourceentry) + ge_balance_negative_reencode_sourceentryvalue = (dst_negative_reencode_sourceentry) + ge_balance_positive_reencode_sourceentryvalue))))))))) -> (exists sto_ap_reencode_sourcemultiply sto_an_reencode_sourcemultiply sto_bp_reencode_sourcemultiply sto_bn_reencode_sourcemultiply sto_cp_reencode_sourcemultiply sto_cn_reencode_sourcemultiply. (((((scp_first_reencode_source) = 2 * (sto_ap_reencode_sourcemultiply) /\ (sto_an_reencode_sourcemultiply) = 0) \/ exists ge_signed_half_reencode_sourcemultiplyleft. (((scp_first_reencode_source) = 2 * ge_signed_half_reencode_sourcemultiplyleft + 1 /\ (sto_ap_reencode_sourcemultiply) = 0) /\ (sto_an_reencode_sourcemultiply) = S ge_signed_half_reencode_sourcemultiplyleft))) /\ ((((((scp_second_reencode_source) = 2 * (sto_bp_reencode_sourcemultiply) /\ (sto_bn_reencode_sourcemultiply) = 0) \/ exists ge_signed_half_reencode_sourcemultiplyright. (((scp_second_reencode_source) = 2 * ge_signed_half_reencode_sourcemultiplyright + 1 /\ (sto_bp_reencode_sourcemultiply) = 0) /\ (sto_bn_reencode_sourcemultiply) = S ge_signed_half_reencode_sourcemultiplyright))) /\ ((((((scp_value_reencode_source) = 2 * (sto_cp_reencode_sourcemultiply) /\ (sto_cn_reencode_sourcemultiply) = 0) \/ exists ge_signed_half_reencode_sourcemultiplyoutput. (((scp_value_reencode_source) = 2 * ge_signed_half_reencode_sourcemultiplyoutput + 1 /\ (sto_cp_reencode_sourcemultiply) = 0) /\ (sto_cn_reencode_sourcemultiply) = S ge_signed_half_reencode_sourcemultiplyoutput))) /\ ((sto_ap_reencode_sourcemultiply * sto_bp_reencode_sourcemultiply + sto_an_reencode_sourcemultiply * sto_bn_reencode_sourcemultiply) + sto_cn_reencode_sourcemultiply = (sto_ap_reencode_sourcemultiply * sto_bn_reencode_sourcemultiply + sto_an_reencode_sourcemultiply * sto_bp_reencode_sourcemultiply) + sto_cp_reencode_sourcemultiply)))))))))))))) -> (exists dst_positive_code_reencode_valid dst_positive_scale_reencode_valid dst_negative_code_reencode_valid dst_negative_scale_reencode_valid. (((U) = (((((dst_positive_code_reencode_valid) + (dst_positive_scale_reencode_valid)) * S ((dst_positive_code_reencode_valid) + (dst_positive_scale_reencode_valid)) + ((dst_positive_scale_reencode_valid) + (dst_positive_scale_reencode_valid))) + (((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) * S ((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) + ((dst_negative_scale_reencode_valid) + (dst_negative_scale_reencode_valid)))) * S ((((dst_positive_code_reencode_valid) + (dst_positive_scale_reencode_valid)) * S ((dst_positive_code_reencode_valid) + (dst_positive_scale_reencode_valid)) + ((dst_positive_scale_reencode_valid) + (dst_positive_scale_reencode_valid))) + (((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) * S ((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) + ((dst_negative_scale_reencode_valid) + (dst_negative_scale_reencode_valid)))) + ((((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) * S ((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) + ((dst_negative_scale_reencode_valid) + (dst_negative_scale_reencode_valid))) + (((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) * S ((dst_negative_code_reencode_valid) + (dst_negative_scale_reencode_valid)) + ((dst_negative_scale_reencode_valid) + (dst_negative_scale_reencode_valid)))))) /\ (forall dst_index_reencode_valid. (exists pvs_le_gap_reencode_validdomain. pvs_le_gap_reencode_validdomain + (dst_index_reencode_valid) = (0)) -> exists dst_positive_reencode_valid dst_negative_reencode_valid dst_value_reencode_valid. ((((exists ff_h_pvs_reencode_validentrypositive. ff_h_pvs_reencode_validentrypositive + S (dst_positive_reencode_valid) = S ((S (dst_index_reencode_valid)) * dst_positive_scale_reencode_valid)) /\ exists ff_q_pvs_reencode_validentrypositive. dst_positive_code_reencode_valid = ff_q_pvs_reencode_validentrypositive * S ((S (dst_index_reencode_valid)) * dst_positive_scale_reencode_valid) + (dst_positive_reencode_valid))) /\ (((((exists ff_h_pvs_reencode_validentrynegative. ff_h_pvs_reencode_validentrynegative + S (dst_negative_reencode_valid) = S ((S (dst_index_reencode_valid)) * dst_negative_scale_reencode_valid)) /\ exists ff_q_pvs_reencode_validentrynegative. dst_negative_code_reencode_valid = ff_q_pvs_reencode_validentrynegative * S ((S (dst_index_reencode_valid)) * dst_negative_scale_reencode_valid) + (dst_negative_reencode_valid))) /\ (exists ge_balance_positive_reencode_validentryvalue ge_balance_negative_reencode_validentryvalue. (((((dst_value_reencode_valid) = 2 * (ge_balance_positive_reencode_validentryvalue) /\ (ge_balance_negative_reencode_validentryvalue) = 0) \/ exists ge_signed_half_reencode_validentryvaluedecode. (((dst_value_reencode_valid) = 2 * ge_signed_half_reencode_validentryvaluedecode + 1 /\ (ge_balance_positive_reencode_validentryvalue) = 0) /\ (ge_balance_negative_reencode_validentryvalue) = S ge_signed_half_reencode_validentryvaluedecode))) /\ ((dst_positive_reencode_valid) + ge_balance_negative_reencode_validentryvalue = (dst_negative_reencode_valid) + ge_balance_positive_reencode_validentryvalue))))))))) -> (forall dst_index_reencode_preserved dst_first_reencode_preserved dst_second_reencode_preserved. (exists pvs_gap_reencode_preservedbound. pvs_gap_reencode_preservedbound + S (dst_index_reencode_preserved) = (m*n)) -> (exists dst_positive_code_reencode_preservedfirst dst_positive_scale_reencode_preservedfirst dst_negative_code_reencode_preservedfirst dst_negative_scale_reencode_preservedfirst dst_positive_reencode_preservedfirst dst_negative_reencode_preservedfirst. (((T) = (((((dst_positive_code_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst)) * S ((dst_positive_code_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst)) + ((dst_positive_scale_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst))) + (((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) * S ((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) + ((dst_negative_scale_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)))) * S ((((dst_positive_code_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst)) * S ((dst_positive_code_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst)) + ((dst_positive_scale_reencode_preservedfirst) + (dst_positive_scale_reencode_preservedfirst))) + (((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) * S ((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) + ((dst_negative_scale_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)))) + ((((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) * S ((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) + ((dst_negative_scale_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst))) + (((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) * S ((dst_negative_code_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)) + ((dst_negative_scale_reencode_preservedfirst) + (dst_negative_scale_reencode_preservedfirst)))))) /\ (((((exists ff_h_pvs_reencode_preservedfirstpositive. ff_h_pvs_reencode_preservedfirstpositive + S (dst_positive_reencode_preservedfirst) = S ((S (dst_index_reencode_preserved)) * dst_positive_scale_reencode_preservedfirst)) /\ exists ff_q_pvs_reencode_preservedfirstpositive. dst_positive_code_reencode_preservedfirst = ff_q_pvs_reencode_preservedfirstpositive * S ((S (dst_index_reencode_preserved)) * dst_positive_scale_reencode_preservedfirst) + (dst_positive_reencode_preservedfirst))) /\ (((((exists ff_h_pvs_reencode_preservedfirstnegative. ff_h_pvs_reencode_preservedfirstnegative + S (dst_negative_reencode_preservedfirst) = S ((S (dst_index_reencode_preserved)) * dst_negative_scale_reencode_preservedfirst)) /\ exists ff_q_pvs_reencode_preservedfirstnegative. dst_negative_code_reencode_preservedfirst = ff_q_pvs_reencode_preservedfirstnegative * S ((S (dst_index_reencode_preserved)) * dst_negative_scale_reencode_preservedfirst) + (dst_negative_reencode_preservedfirst))) /\ (exists ge_balance_positive_reencode_preservedfirstvalue ge_balance_negative_reencode_preservedfirstvalue. (((((dst_first_reencode_preserved) = 2 * (ge_balance_positive_reencode_preservedfirstvalue) /\ (ge_balance_negative_reencode_preservedfirstvalue) = 0) \/ exists ge_signed_half_reencode_preservedfirstvaluedecode. (((dst_first_reencode_preserved) = 2 * ge_signed_half_reencode_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_reencode_preservedfirstvalue) = 0) /\ (ge_balance_negative_reencode_preservedfirstvalue) = S ge_signed_half_reencode_preservedfirstvaluedecode))) /\ ((dst_positive_reencode_preservedfirst) + ge_balance_negative_reencode_preservedfirstvalue = (dst_negative_reencode_preservedfirst) + ge_balance_positive_reencode_preservedfirstvalue))))))))) -> (exists dst_positive_code_reencode_preservedsecond dst_positive_scale_reencode_preservedsecond dst_negative_code_reencode_preservedsecond dst_negative_scale_reencode_preservedsecond dst_positive_reencode_preservedsecond dst_negative_reencode_preservedsecond. (((U) = (((((dst_positive_code_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond)) * S ((dst_positive_code_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond)) + ((dst_positive_scale_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond))) + (((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) * S ((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) + ((dst_negative_scale_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)))) * S ((((dst_positive_code_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond)) * S ((dst_positive_code_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond)) + ((dst_positive_scale_reencode_preservedsecond) + (dst_positive_scale_reencode_preservedsecond))) + (((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) * S ((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) + ((dst_negative_scale_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)))) + ((((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) * S ((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) + ((dst_negative_scale_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond))) + (((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) * S ((dst_negative_code_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)) + ((dst_negative_scale_reencode_preservedsecond) + (dst_negative_scale_reencode_preservedsecond)))))) /\ (((((exists ff_h_pvs_reencode_preservedsecondpositive. ff_h_pvs_reencode_preservedsecondpositive + S (dst_positive_reencode_preservedsecond) = S ((S (dst_index_reencode_preserved)) * dst_positive_scale_reencode_preservedsecond)) /\ exists ff_q_pvs_reencode_preservedsecondpositive. dst_positive_code_reencode_preservedsecond = ff_q_pvs_reencode_preservedsecondpositive * S ((S (dst_index_reencode_preserved)) * dst_positive_scale_reencode_preservedsecond) + (dst_positive_reencode_preservedsecond))) /\ (((((exists ff_h_pvs_reencode_preservedsecondnegative. ff_h_pvs_reencode_preservedsecondnegative + S (dst_negative_reencode_preservedsecond) = S ((S (dst_index_reencode_preserved)) * dst_negative_scale_reencode_preservedsecond)) /\ exists ff_q_pvs_reencode_preservedsecondnegative. dst_negative_code_reencode_preservedsecond = ff_q_pvs_reencode_preservedsecondnegative * S ((S (dst_index_reencode_preserved)) * dst_negative_scale_reencode_preservedsecond) + (dst_negative_reencode_preservedsecond))) /\ (exists ge_balance_positive_reencode_preservedsecondvalue ge_balance_negative_reencode_preservedsecondvalue. (((((dst_second_reencode_preserved) = 2 * (ge_balance_positive_reencode_preservedsecondvalue) /\ (ge_balance_negative_reencode_preservedsecondvalue) = 0) \/ exists ge_signed_half_reencode_preservedsecondvaluedecode. (((dst_second_reencode_preserved) = 2 * ge_signed_half_reencode_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_reencode_preservedsecondvalue) = 0) /\ (ge_balance_negative_reencode_preservedsecondvalue) = S ge_signed_half_reencode_preservedsecondvaluedecode))) /\ ((dst_positive_reencode_preservedsecond) + ge_balance_negative_reencode_preservedsecondvalue = (dst_negative_reencode_preservedsecond) + ge_balance_positive_reencode_preservedsecondvalue))))))))) -> dst_first_reencode_preserved = dst_second_reencode_preserved) -> (((exists dst_positive_code_reencode_resultF dst_positive_scale_reencode_resultF dst_negative_code_reencode_resultF dst_negative_scale_reencode_resultF. (((F) = (((((dst_positive_code_reencode_resultF) + (dst_positive_scale_reencode_resultF)) * S ((dst_positive_code_reencode_resultF) + (dst_positive_scale_reencode_resultF)) + ((dst_positive_scale_reencode_resultF) + (dst_positive_scale_reencode_resultF))) + (((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) * S ((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) + ((dst_negative_scale_reencode_resultF) + (dst_negative_scale_reencode_resultF)))) * S ((((dst_positive_code_reencode_resultF) + (dst_positive_scale_reencode_resultF)) * S ((dst_positive_code_reencode_resultF) + (dst_positive_scale_reencode_resultF)) + ((dst_positive_scale_reencode_resultF) + (dst_positive_scale_reencode_resultF))) + (((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) * S ((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) + ((dst_negative_scale_reencode_resultF) + (dst_negative_scale_reencode_resultF)))) + ((((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) * S ((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) + ((dst_negative_scale_reencode_resultF) + (dst_negative_scale_reencode_resultF))) + (((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) * S ((dst_negative_code_reencode_resultF) + (dst_negative_scale_reencode_resultF)) + ((dst_negative_scale_reencode_resultF) + (dst_negative_scale_reencode_resultF)))))) /\ (forall dst_index_reencode_resultF. (exists pvs_le_gap_reencode_resultFdomain. pvs_le_gap_reencode_resultFdomain + (dst_index_reencode_resultF) = (0)) -> exists dst_positive_reencode_resultF dst_negative_reencode_resultF dst_value_reencode_resultF. ((((exists ff_h_pvs_reencode_resultFentrypositive. ff_h_pvs_reencode_resultFentrypositive + S (dst_positive_reencode_resultF) = S ((S (dst_index_reencode_resultF)) * dst_positive_scale_reencode_resultF)) /\ exists ff_q_pvs_reencode_resultFentrypositive. dst_positive_code_reencode_resultF = ff_q_pvs_reencode_resultFentrypositive * S ((S (dst_index_reencode_resultF)) * dst_positive_scale_reencode_resultF) + (dst_positive_reencode_resultF))) /\ (((((exists ff_h_pvs_reencode_resultFentrynegative. ff_h_pvs_reencode_resultFentrynegative + S (dst_negative_reencode_resultF) = S ((S (dst_index_reencode_resultF)) * dst_negative_scale_reencode_resultF)) /\ exists ff_q_pvs_reencode_resultFentrynegative. dst_negative_code_reencode_resultF = ff_q_pvs_reencode_resultFentrynegative * S ((S (dst_index_reencode_resultF)) * dst_negative_scale_reencode_resultF) + (dst_negative_reencode_resultF))) /\ (exists ge_balance_positive_reencode_resultFentryvalue ge_balance_negative_reencode_resultFentryvalue. (((((dst_value_reencode_resultF) = 2 * (ge_balance_positive_reencode_resultFentryvalue) /\ (ge_balance_negative_reencode_resultFentryvalue) = 0) \/ exists ge_signed_half_reencode_resultFentryvaluedecode. (((dst_value_reencode_resultF) = 2 * ge_signed_half_reencode_resultFentryvaluedecode + 1 /\ (ge_balance_positive_reencode_resultFentryvalue) = 0) /\ (ge_balance_negative_reencode_resultFentryvalue) = S ge_signed_half_reencode_resultFentryvaluedecode))) /\ ((dst_positive_reencode_resultF) + ge_balance_negative_reencode_resultFentryvalue = (dst_negative_reencode_resultF) + ge_balance_positive_reencode_resultFentryvalue))))))))) /\ (((exists dst_positive_code_reencode_resultG dst_positive_scale_reencode_resultG dst_negative_code_reencode_resultG dst_negative_scale_reencode_resultG. (((G) = (((((dst_positive_code_reencode_resultG) + (dst_positive_scale_reencode_resultG)) * S ((dst_positive_code_reencode_resultG) + (dst_positive_scale_reencode_resultG)) + ((dst_positive_scale_reencode_resultG) + (dst_positive_scale_reencode_resultG))) + (((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) * S ((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) + ((dst_negative_scale_reencode_resultG) + (dst_negative_scale_reencode_resultG)))) * S ((((dst_positive_code_reencode_resultG) + (dst_positive_scale_reencode_resultG)) * S ((dst_positive_code_reencode_resultG) + (dst_positive_scale_reencode_resultG)) + ((dst_positive_scale_reencode_resultG) + (dst_positive_scale_reencode_resultG))) + (((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) * S ((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) + ((dst_negative_scale_reencode_resultG) + (dst_negative_scale_reencode_resultG)))) + ((((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) * S ((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) + ((dst_negative_scale_reencode_resultG) + (dst_negative_scale_reencode_resultG))) + (((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) * S ((dst_negative_code_reencode_resultG) + (dst_negative_scale_reencode_resultG)) + ((dst_negative_scale_reencode_resultG) + (dst_negative_scale_reencode_resultG)))))) /\ (forall dst_index_reencode_resultG. (exists pvs_le_gap_reencode_resultGdomain. pvs_le_gap_reencode_resultGdomain + (dst_index_reencode_resultG) = (0)) -> exists dst_positive_reencode_resultG dst_negative_reencode_resultG dst_value_reencode_resultG. ((((exists ff_h_pvs_reencode_resultGentrypositive. ff_h_pvs_reencode_resultGentrypositive + S (dst_positive_reencode_resultG) = S ((S (dst_index_reencode_resultG)) * dst_positive_scale_reencode_resultG)) /\ exists ff_q_pvs_reencode_resultGentrypositive. dst_positive_code_reencode_resultG = ff_q_pvs_reencode_resultGentrypositive * S ((S (dst_index_reencode_resultG)) * dst_positive_scale_reencode_resultG) + (dst_positive_reencode_resultG))) /\ (((((exists ff_h_pvs_reencode_resultGentrynegative. ff_h_pvs_reencode_resultGentrynegative + S (dst_negative_reencode_resultG) = S ((S (dst_index_reencode_resultG)) * dst_negative_scale_reencode_resultG)) /\ exists ff_q_pvs_reencode_resultGentrynegative. dst_negative_code_reencode_resultG = ff_q_pvs_reencode_resultGentrynegative * S ((S (dst_index_reencode_resultG)) * dst_negative_scale_reencode_resultG) + (dst_negative_reencode_resultG))) /\ (exists ge_balance_positive_reencode_resultGentryvalue ge_balance_negative_reencode_resultGentryvalue. (((((dst_value_reencode_resultG) = 2 * (ge_balance_positive_reencode_resultGentryvalue) /\ (ge_balance_negative_reencode_resultGentryvalue) = 0) \/ exists ge_signed_half_reencode_resultGentryvaluedecode. (((dst_value_reencode_resultG) = 2 * ge_signed_half_reencode_resultGentryvaluedecode + 1 /\ (ge_balance_positive_reencode_resultGentryvalue) = 0) /\ (ge_balance_negative_reencode_resultGentryvalue) = S ge_signed_half_reencode_resultGentryvaluedecode))) /\ ((dst_positive_reencode_resultG) + ge_balance_negative_reencode_resultGentryvalue = (dst_negative_reencode_resultG) + ge_balance_positive_reencode_resultGentryvalue))))))))) /\ (((exists dst_positive_code_reencode_resultT dst_positive_scale_reencode_resultT dst_negative_code_reencode_resultT dst_negative_scale_reencode_resultT. (((U) = (((((dst_positive_code_reencode_resultT) + (dst_positive_scale_reencode_resultT)) * S ((dst_positive_code_reencode_resultT) + (dst_positive_scale_reencode_resultT)) + ((dst_positive_scale_reencode_resultT) + (dst_positive_scale_reencode_resultT))) + (((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) * S ((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) + ((dst_negative_scale_reencode_resultT) + (dst_negative_scale_reencode_resultT)))) * S ((((dst_positive_code_reencode_resultT) + (dst_positive_scale_reencode_resultT)) * S ((dst_positive_code_reencode_resultT) + (dst_positive_scale_reencode_resultT)) + ((dst_positive_scale_reencode_resultT) + (dst_positive_scale_reencode_resultT))) + (((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) * S ((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) + ((dst_negative_scale_reencode_resultT) + (dst_negative_scale_reencode_resultT)))) + ((((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) * S ((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) + ((dst_negative_scale_reencode_resultT) + (dst_negative_scale_reencode_resultT))) + (((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) * S ((dst_negative_code_reencode_resultT) + (dst_negative_scale_reencode_resultT)) + ((dst_negative_scale_reencode_resultT) + (dst_negative_scale_reencode_resultT)))))) /\ (forall dst_index_reencode_resultT. (exists pvs_le_gap_reencode_resultTdomain. pvs_le_gap_reencode_resultTdomain + (dst_index_reencode_resultT) = ((m)*(n))) -> exists dst_positive_reencode_resultT dst_negative_reencode_resultT dst_value_reencode_resultT. ((((exists ff_h_pvs_reencode_resultTentrypositive. ff_h_pvs_reencode_resultTentrypositive + S (dst_positive_reencode_resultT) = S ((S (dst_index_reencode_resultT)) * dst_positive_scale_reencode_resultT)) /\ exists ff_q_pvs_reencode_resultTentrypositive. dst_positive_code_reencode_resultT = ff_q_pvs_reencode_resultTentrypositive * S ((S (dst_index_reencode_resultT)) * dst_positive_scale_reencode_resultT) + (dst_positive_reencode_resultT))) /\ (((((exists ff_h_pvs_reencode_resultTentrynegative. ff_h_pvs_reencode_resultTentrynegative + S (dst_negative_reencode_resultT) = S ((S (dst_index_reencode_resultT)) * dst_negative_scale_reencode_resultT)) /\ exists ff_q_pvs_reencode_resultTentrynegative. dst_negative_code_reencode_resultT = ff_q_pvs_reencode_resultTentrynegative * S ((S (dst_index_reencode_resultT)) * dst_negative_scale_reencode_resultT) + (dst_negative_reencode_resultT))) /\ (exists ge_balance_positive_reencode_resultTentryvalue ge_balance_negative_reencode_resultTentryvalue. (((((dst_value_reencode_resultT) = 2 * (ge_balance_positive_reencode_resultTentryvalue) /\ (ge_balance_negative_reencode_resultTentryvalue) = 0) \/ exists ge_signed_half_reencode_resultTentryvaluedecode. (((dst_value_reencode_resultT) = 2 * ge_signed_half_reencode_resultTentryvaluedecode + 1 /\ (ge_balance_positive_reencode_resultTentryvalue) = 0) /\ (ge_balance_negative_reencode_resultTentryvalue) = S ge_signed_half_reencode_resultTentryvaluedecode))) /\ ((dst_positive_reencode_resultT) + ge_balance_negative_reencode_resultTentryvalue = (dst_negative_reencode_resultT) + ge_balance_positive_reencode_resultTentryvalue))))))))) /\ (forall scp_row_reencode_result scp_column_reencode_result scp_first_reencode_result scp_second_reencode_result scp_value_reencode_result. (exists pvs_gap_reencode_resultrows. pvs_gap_reencode_resultrows + S (scp_row_reencode_result) = (m)) -> (exists pvs_gap_reencode_resultcolumns. pvs_gap_reencode_resultcolumns + S (scp_column_reencode_result) = (n)) -> (exists dst_positive_code_reencode_resultfirst dst_positive_scale_reencode_resultfirst dst_negative_code_reencode_resultfirst dst_negative_scale_reencode_resultfirst dst_positive_reencode_resultfirst dst_negative_reencode_resultfirst. (((F) = (((((dst_positive_code_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst)) * S ((dst_positive_code_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst)) + ((dst_positive_scale_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst))) + (((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) * S ((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) + ((dst_negative_scale_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)))) * S ((((dst_positive_code_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst)) * S ((dst_positive_code_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst)) + ((dst_positive_scale_reencode_resultfirst) + (dst_positive_scale_reencode_resultfirst))) + (((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) * S ((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) + ((dst_negative_scale_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)))) + ((((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) * S ((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) + ((dst_negative_scale_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst))) + (((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) * S ((dst_negative_code_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)) + ((dst_negative_scale_reencode_resultfirst) + (dst_negative_scale_reencode_resultfirst)))))) /\ (((((exists ff_h_pvs_reencode_resultfirstpositive. ff_h_pvs_reencode_resultfirstpositive + S (dst_positive_reencode_resultfirst) = S ((S (scp_row_reencode_result)) * dst_positive_scale_reencode_resultfirst)) /\ exists ff_q_pvs_reencode_resultfirstpositive. dst_positive_code_reencode_resultfirst = ff_q_pvs_reencode_resultfirstpositive * S ((S (scp_row_reencode_result)) * dst_positive_scale_reencode_resultfirst) + (dst_positive_reencode_resultfirst))) /\ (((((exists ff_h_pvs_reencode_resultfirstnegative. ff_h_pvs_reencode_resultfirstnegative + S (dst_negative_reencode_resultfirst) = S ((S (scp_row_reencode_result)) * dst_negative_scale_reencode_resultfirst)) /\ exists ff_q_pvs_reencode_resultfirstnegative. dst_negative_code_reencode_resultfirst = ff_q_pvs_reencode_resultfirstnegative * S ((S (scp_row_reencode_result)) * dst_negative_scale_reencode_resultfirst) + (dst_negative_reencode_resultfirst))) /\ (exists ge_balance_positive_reencode_resultfirstvalue ge_balance_negative_reencode_resultfirstvalue. (((((scp_first_reencode_result) = 2 * (ge_balance_positive_reencode_resultfirstvalue) /\ (ge_balance_negative_reencode_resultfirstvalue) = 0) \/ exists ge_signed_half_reencode_resultfirstvaluedecode. (((scp_first_reencode_result) = 2 * ge_signed_half_reencode_resultfirstvaluedecode + 1 /\ (ge_balance_positive_reencode_resultfirstvalue) = 0) /\ (ge_balance_negative_reencode_resultfirstvalue) = S ge_signed_half_reencode_resultfirstvaluedecode))) /\ ((dst_positive_reencode_resultfirst) + ge_balance_negative_reencode_resultfirstvalue = (dst_negative_reencode_resultfirst) + ge_balance_positive_reencode_resultfirstvalue))))))))) -> (exists dst_positive_code_reencode_resultsecond dst_positive_scale_reencode_resultsecond dst_negative_code_reencode_resultsecond dst_negative_scale_reencode_resultsecond dst_positive_reencode_resultsecond dst_negative_reencode_resultsecond. (((G) = (((((dst_positive_code_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond)) * S ((dst_positive_code_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond)) + ((dst_positive_scale_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond))) + (((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) * S ((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) + ((dst_negative_scale_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)))) * S ((((dst_positive_code_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond)) * S ((dst_positive_code_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond)) + ((dst_positive_scale_reencode_resultsecond) + (dst_positive_scale_reencode_resultsecond))) + (((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) * S ((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) + ((dst_negative_scale_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)))) + ((((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) * S ((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) + ((dst_negative_scale_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond))) + (((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) * S ((dst_negative_code_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)) + ((dst_negative_scale_reencode_resultsecond) + (dst_negative_scale_reencode_resultsecond)))))) /\ (((((exists ff_h_pvs_reencode_resultsecondpositive. ff_h_pvs_reencode_resultsecondpositive + S (dst_positive_reencode_resultsecond) = S ((S (scp_column_reencode_result)) * dst_positive_scale_reencode_resultsecond)) /\ exists ff_q_pvs_reencode_resultsecondpositive. dst_positive_code_reencode_resultsecond = ff_q_pvs_reencode_resultsecondpositive * S ((S (scp_column_reencode_result)) * dst_positive_scale_reencode_resultsecond) + (dst_positive_reencode_resultsecond))) /\ (((((exists ff_h_pvs_reencode_resultsecondnegative. ff_h_pvs_reencode_resultsecondnegative + S (dst_negative_reencode_resultsecond) = S ((S (scp_column_reencode_result)) * dst_negative_scale_reencode_resultsecond)) /\ exists ff_q_pvs_reencode_resultsecondnegative. dst_negative_code_reencode_resultsecond = ff_q_pvs_reencode_resultsecondnegative * S ((S (scp_column_reencode_result)) * dst_negative_scale_reencode_resultsecond) + (dst_negative_reencode_resultsecond))) /\ (exists ge_balance_positive_reencode_resultsecondvalue ge_balance_negative_reencode_resultsecondvalue. (((((scp_second_reencode_result) = 2 * (ge_balance_positive_reencode_resultsecondvalue) /\ (ge_balance_negative_reencode_resultsecondvalue) = 0) \/ exists ge_signed_half_reencode_resultsecondvaluedecode. (((scp_second_reencode_result) = 2 * ge_signed_half_reencode_resultsecondvaluedecode + 1 /\ (ge_balance_positive_reencode_resultsecondvalue) = 0) /\ (ge_balance_negative_reencode_resultsecondvalue) = S ge_signed_half_reencode_resultsecondvaluedecode))) /\ ((dst_positive_reencode_resultsecond) + ge_balance_negative_reencode_resultsecondvalue = (dst_negative_reencode_resultsecond) + ge_balance_positive_reencode_resultsecondvalue))))))))) -> (exists dst_positive_code_reencode_resultentry dst_positive_scale_reencode_resultentry dst_negative_code_reencode_resultentry dst_negative_scale_reencode_resultentry dst_positive_reencode_resultentry dst_negative_reencode_resultentry. (((U) = (((((dst_positive_code_reencode_resultentry) + (dst_positive_scale_reencode_resultentry)) * S ((dst_positive_code_reencode_resultentry) + (dst_positive_scale_reencode_resultentry)) + ((dst_positive_scale_reencode_resultentry) + (dst_positive_scale_reencode_resultentry))) + (((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) * S ((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) + ((dst_negative_scale_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)))) * S ((((dst_positive_code_reencode_resultentry) + (dst_positive_scale_reencode_resultentry)) * S ((dst_positive_code_reencode_resultentry) + (dst_positive_scale_reencode_resultentry)) + ((dst_positive_scale_reencode_resultentry) + (dst_positive_scale_reencode_resultentry))) + (((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) * S ((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) + ((dst_negative_scale_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)))) + ((((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) * S ((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) + ((dst_negative_scale_reencode_resultentry) + (dst_negative_scale_reencode_resultentry))) + (((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) * S ((dst_negative_code_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)) + ((dst_negative_scale_reencode_resultentry) + (dst_negative_scale_reencode_resultentry)))))) /\ (((((exists ff_h_pvs_reencode_resultentrypositive. ff_h_pvs_reencode_resultentrypositive + S (dst_positive_reencode_resultentry) = S ((S (((n)*(scp_row_reencode_result)+(scp_column_reencode_result)))) * dst_positive_scale_reencode_resultentry)) /\ exists ff_q_pvs_reencode_resultentrypositive. dst_positive_code_reencode_resultentry = ff_q_pvs_reencode_resultentrypositive * S ((S (((n)*(scp_row_reencode_result)+(scp_column_reencode_result)))) * dst_positive_scale_reencode_resultentry) + (dst_positive_reencode_resultentry))) /\ (((((exists ff_h_pvs_reencode_resultentrynegative. ff_h_pvs_reencode_resultentrynegative + S (dst_negative_reencode_resultentry) = S ((S (((n)*(scp_row_reencode_result)+(scp_column_reencode_result)))) * dst_negative_scale_reencode_resultentry)) /\ exists ff_q_pvs_reencode_resultentrynegative. dst_negative_code_reencode_resultentry = ff_q_pvs_reencode_resultentrynegative * S ((S (((n)*(scp_row_reencode_result)+(scp_column_reencode_result)))) * dst_negative_scale_reencode_resultentry) + (dst_negative_reencode_resultentry))) /\ (exists ge_balance_positive_reencode_resultentryvalue ge_balance_negative_reencode_resultentryvalue. (((((scp_value_reencode_result) = 2 * (ge_balance_positive_reencode_resultentryvalue) /\ (ge_balance_negative_reencode_resultentryvalue) = 0) \/ exists ge_signed_half_reencode_resultentryvaluedecode. (((scp_value_reencode_result) = 2 * ge_signed_half_reencode_resultentryvaluedecode + 1 /\ (ge_balance_positive_reencode_resultentryvalue) = 0) /\ (ge_balance_negative_reencode_resultentryvalue) = S ge_signed_half_reencode_resultentryvaluedecode))) /\ ((dst_positive_reencode_resultentry) + ge_balance_negative_reencode_resultentryvalue = (dst_negative_reencode_resultentry) + ge_balance_positive_reencode_resultentryvalue))))))))) -> (exists sto_ap_reencode_resultmultiply sto_an_reencode_resultmultiply sto_bp_reencode_resultmultiply sto_bn_reencode_resultmultiply sto_cp_reencode_resultmultiply sto_cn_reencode_resultmultiply. (((((scp_first_reencode_result) = 2 * (sto_ap_reencode_resultmultiply) /\ (sto_an_reencode_resultmultiply) = 0) \/ exists ge_signed_half_reencode_resultmultiplyleft. (((scp_first_reencode_result) = 2 * ge_signed_half_reencode_resultmultiplyleft + 1 /\ (sto_ap_reencode_resultmultiply) = 0) /\ (sto_an_reencode_resultmultiply) = S ge_signed_half_reencode_resultmultiplyleft))) /\ ((((((scp_second_reencode_result) = 2 * (sto_bp_reencode_resultmultiply) /\ (sto_bn_reencode_resultmultiply) = 0) \/ exists ge_signed_half_reencode_resultmultiplyright. (((scp_second_reencode_result) = 2 * ge_signed_half_reencode_resultmultiplyright + 1 /\ (sto_bp_reencode_resultmultiply) = 0) /\ (sto_bn_reencode_resultmultiply) = S ge_signed_half_reencode_resultmultiplyright))) /\ ((((((scp_value_reencode_result) = 2 * (sto_cp_reencode_resultmultiply) /\ (sto_cn_reencode_resultmultiply) = 0) \/ exists ge_signed_half_reencode_resultmultiplyoutput. (((scp_value_reencode_result) = 2 * ge_signed_half_reencode_resultmultiplyoutput + 1 /\ (sto_cp_reencode_resultmultiply) = 0) /\ (sto_cn_reencode_resultmultiply) = S ge_signed_half_reencode_resultmultiplyoutput))) /\ ((sto_ap_reencode_resultmultiply * sto_bp_reencode_resultmultiply + sto_an_reencode_resultmultiply * sto_bn_reencode_resultmultiply) + sto_cn_reencode_resultmultiply = (sto_ap_reencode_resultmultiply * sto_bn_reencode_resultmultiply + sto_an_reencode_resultmultiply * sto_bp_reencode_resultmultiply) + sto_cp_reencode_resultmultiply))))))))))))))