signed_cartesian_product_prefix_sum

Exact expanded first-order arithmetic statement

forall F G T m n a b c. (((exists dst_positive_code_product_prefix_tableF dst_positive_scale_product_prefix_tableF dst_negative_code_product_prefix_tableF dst_negative_scale_product_prefix_tableF. (((F) = (((((dst_positive_code_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF)) * S ((dst_positive_code_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF)) + ((dst_positive_scale_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF))) + (((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) * S ((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) + ((dst_negative_scale_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)))) * S ((((dst_positive_code_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF)) * S ((dst_positive_code_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF)) + ((dst_positive_scale_product_prefix_tableF) + (dst_positive_scale_product_prefix_tableF))) + (((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) * S ((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) + ((dst_negative_scale_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)))) + ((((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) * S ((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) + ((dst_negative_scale_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF))) + (((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) * S ((dst_negative_code_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)) + ((dst_negative_scale_product_prefix_tableF) + (dst_negative_scale_product_prefix_tableF)))))) /\ (forall dst_index_product_prefix_tableF. (exists pvs_le_gap_product_prefix_tableFdomain. pvs_le_gap_product_prefix_tableFdomain + (dst_index_product_prefix_tableF) = (0)) -> exists dst_positive_product_prefix_tableF dst_negative_product_prefix_tableF dst_value_product_prefix_tableF. ((((exists ff_h_pvs_product_prefix_tableFentrypositive. ff_h_pvs_product_prefix_tableFentrypositive + S (dst_positive_product_prefix_tableF) = S ((S (dst_index_product_prefix_tableF)) * dst_positive_scale_product_prefix_tableF)) /\ exists ff_q_pvs_product_prefix_tableFentrypositive. dst_positive_code_product_prefix_tableF = ff_q_pvs_product_prefix_tableFentrypositive * S ((S (dst_index_product_prefix_tableF)) * dst_positive_scale_product_prefix_tableF) + (dst_positive_product_prefix_tableF))) /\ (((((exists ff_h_pvs_product_prefix_tableFentrynegative. ff_h_pvs_product_prefix_tableFentrynegative + S (dst_negative_product_prefix_tableF) = S ((S (dst_index_product_prefix_tableF)) * dst_negative_scale_product_prefix_tableF)) /\ exists ff_q_pvs_product_prefix_tableFentrynegative. dst_negative_code_product_prefix_tableF = ff_q_pvs_product_prefix_tableFentrynegative * S ((S (dst_index_product_prefix_tableF)) * dst_negative_scale_product_prefix_tableF) + (dst_negative_product_prefix_tableF))) /\ (exists ge_balance_positive_product_prefix_tableFentryvalue ge_balance_negative_product_prefix_tableFentryvalue. (((((dst_value_product_prefix_tableF) = 2 * (ge_balance_positive_product_prefix_tableFentryvalue) /\ (ge_balance_negative_product_prefix_tableFentryvalue) = 0) \/ exists ge_signed_half_product_prefix_tableFentryvaluedecode. (((dst_value_product_prefix_tableF) = 2 * ge_signed_half_product_prefix_tableFentryvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tableFentryvalue) = 0) /\ (ge_balance_negative_product_prefix_tableFentryvalue) = S ge_signed_half_product_prefix_tableFentryvaluedecode))) /\ ((dst_positive_product_prefix_tableF) + ge_balance_negative_product_prefix_tableFentryvalue = (dst_negative_product_prefix_tableF) + ge_balance_positive_product_prefix_tableFentryvalue))))))))) /\ (((exists dst_positive_code_product_prefix_tableG dst_positive_scale_product_prefix_tableG dst_negative_code_product_prefix_tableG dst_negative_scale_product_prefix_tableG. (((G) = (((((dst_positive_code_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG)) * S ((dst_positive_code_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG)) + ((dst_positive_scale_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG))) + (((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) * S ((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) + ((dst_negative_scale_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)))) * S ((((dst_positive_code_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG)) * S ((dst_positive_code_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG)) + ((dst_positive_scale_product_prefix_tableG) + (dst_positive_scale_product_prefix_tableG))) + (((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) * S ((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) + ((dst_negative_scale_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)))) + ((((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) * S ((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) + ((dst_negative_scale_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG))) + (((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) * S ((dst_negative_code_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)) + ((dst_negative_scale_product_prefix_tableG) + (dst_negative_scale_product_prefix_tableG)))))) /\ (forall dst_index_product_prefix_tableG. (exists pvs_le_gap_product_prefix_tableGdomain. pvs_le_gap_product_prefix_tableGdomain + (dst_index_product_prefix_tableG) = (0)) -> exists dst_positive_product_prefix_tableG dst_negative_product_prefix_tableG dst_value_product_prefix_tableG. ((((exists ff_h_pvs_product_prefix_tableGentrypositive. ff_h_pvs_product_prefix_tableGentrypositive + S (dst_positive_product_prefix_tableG) = S ((S (dst_index_product_prefix_tableG)) * dst_positive_scale_product_prefix_tableG)) /\ exists ff_q_pvs_product_prefix_tableGentrypositive. dst_positive_code_product_prefix_tableG = ff_q_pvs_product_prefix_tableGentrypositive * S ((S (dst_index_product_prefix_tableG)) * dst_positive_scale_product_prefix_tableG) + (dst_positive_product_prefix_tableG))) /\ (((((exists ff_h_pvs_product_prefix_tableGentrynegative. ff_h_pvs_product_prefix_tableGentrynegative + S (dst_negative_product_prefix_tableG) = S ((S (dst_index_product_prefix_tableG)) * dst_negative_scale_product_prefix_tableG)) /\ exists ff_q_pvs_product_prefix_tableGentrynegative. dst_negative_code_product_prefix_tableG = ff_q_pvs_product_prefix_tableGentrynegative * S ((S (dst_index_product_prefix_tableG)) * dst_negative_scale_product_prefix_tableG) + (dst_negative_product_prefix_tableG))) /\ (exists ge_balance_positive_product_prefix_tableGentryvalue ge_balance_negative_product_prefix_tableGentryvalue. (((((dst_value_product_prefix_tableG) = 2 * (ge_balance_positive_product_prefix_tableGentryvalue) /\ (ge_balance_negative_product_prefix_tableGentryvalue) = 0) \/ exists ge_signed_half_product_prefix_tableGentryvaluedecode. (((dst_value_product_prefix_tableG) = 2 * ge_signed_half_product_prefix_tableGentryvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tableGentryvalue) = 0) /\ (ge_balance_negative_product_prefix_tableGentryvalue) = S ge_signed_half_product_prefix_tableGentryvaluedecode))) /\ ((dst_positive_product_prefix_tableG) + ge_balance_negative_product_prefix_tableGentryvalue = (dst_negative_product_prefix_tableG) + ge_balance_positive_product_prefix_tableGentryvalue))))))))) /\ (((exists dst_positive_code_product_prefix_tableT dst_positive_scale_product_prefix_tableT dst_negative_code_product_prefix_tableT dst_negative_scale_product_prefix_tableT. (((T) = (((((dst_positive_code_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT)) * S ((dst_positive_code_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT)) + ((dst_positive_scale_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT))) + (((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) * S ((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) + ((dst_negative_scale_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)))) * S ((((dst_positive_code_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT)) * S ((dst_positive_code_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT)) + ((dst_positive_scale_product_prefix_tableT) + (dst_positive_scale_product_prefix_tableT))) + (((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) * S ((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) + ((dst_negative_scale_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)))) + ((((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) * S ((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) + ((dst_negative_scale_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT))) + (((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) * S ((dst_negative_code_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)) + ((dst_negative_scale_product_prefix_tableT) + (dst_negative_scale_product_prefix_tableT)))))) /\ (forall dst_index_product_prefix_tableT. (exists pvs_le_gap_product_prefix_tableTdomain. pvs_le_gap_product_prefix_tableTdomain + (dst_index_product_prefix_tableT) = ((m)*(n))) -> exists dst_positive_product_prefix_tableT dst_negative_product_prefix_tableT dst_value_product_prefix_tableT. ((((exists ff_h_pvs_product_prefix_tableTentrypositive. ff_h_pvs_product_prefix_tableTentrypositive + S (dst_positive_product_prefix_tableT) = S ((S (dst_index_product_prefix_tableT)) * dst_positive_scale_product_prefix_tableT)) /\ exists ff_q_pvs_product_prefix_tableTentrypositive. dst_positive_code_product_prefix_tableT = ff_q_pvs_product_prefix_tableTentrypositive * S ((S (dst_index_product_prefix_tableT)) * dst_positive_scale_product_prefix_tableT) + (dst_positive_product_prefix_tableT))) /\ (((((exists ff_h_pvs_product_prefix_tableTentrynegative. ff_h_pvs_product_prefix_tableTentrynegative + S (dst_negative_product_prefix_tableT) = S ((S (dst_index_product_prefix_tableT)) * dst_negative_scale_product_prefix_tableT)) /\ exists ff_q_pvs_product_prefix_tableTentrynegative. dst_negative_code_product_prefix_tableT = ff_q_pvs_product_prefix_tableTentrynegative * S ((S (dst_index_product_prefix_tableT)) * dst_negative_scale_product_prefix_tableT) + (dst_negative_product_prefix_tableT))) /\ (exists ge_balance_positive_product_prefix_tableTentryvalue ge_balance_negative_product_prefix_tableTentryvalue. (((((dst_value_product_prefix_tableT) = 2 * (ge_balance_positive_product_prefix_tableTentryvalue) /\ (ge_balance_negative_product_prefix_tableTentryvalue) = 0) \/ exists ge_signed_half_product_prefix_tableTentryvaluedecode. (((dst_value_product_prefix_tableT) = 2 * ge_signed_half_product_prefix_tableTentryvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tableTentryvalue) = 0) /\ (ge_balance_negative_product_prefix_tableTentryvalue) = S ge_signed_half_product_prefix_tableTentryvaluedecode))) /\ ((dst_positive_product_prefix_tableT) + ge_balance_negative_product_prefix_tableTentryvalue = (dst_negative_product_prefix_tableT) + ge_balance_positive_product_prefix_tableTentryvalue))))))))) /\ (forall scp_row_product_prefix_table scp_column_product_prefix_table scp_first_product_prefix_table scp_second_product_prefix_table scp_value_product_prefix_table. (exists pvs_gap_product_prefix_tablerows. pvs_gap_product_prefix_tablerows + S (scp_row_product_prefix_table) = (m)) -> (exists pvs_gap_product_prefix_tablecolumns. pvs_gap_product_prefix_tablecolumns + S (scp_column_product_prefix_table) = (n)) -> (exists dst_positive_code_product_prefix_tablefirst dst_positive_scale_product_prefix_tablefirst dst_negative_code_product_prefix_tablefirst dst_negative_scale_product_prefix_tablefirst dst_positive_product_prefix_tablefirst dst_negative_product_prefix_tablefirst. (((F) = (((((dst_positive_code_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst)) * S ((dst_positive_code_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst)) + ((dst_positive_scale_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst))) + (((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) * S ((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) + ((dst_negative_scale_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)))) * S ((((dst_positive_code_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst)) * S ((dst_positive_code_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst)) + ((dst_positive_scale_product_prefix_tablefirst) + (dst_positive_scale_product_prefix_tablefirst))) + (((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) * S ((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) + ((dst_negative_scale_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)))) + ((((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) * S ((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) + ((dst_negative_scale_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst))) + (((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) * S ((dst_negative_code_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)) + ((dst_negative_scale_product_prefix_tablefirst) + (dst_negative_scale_product_prefix_tablefirst)))))) /\ (((((exists ff_h_pvs_product_prefix_tablefirstpositive. ff_h_pvs_product_prefix_tablefirstpositive + S (dst_positive_product_prefix_tablefirst) = S ((S (scp_row_product_prefix_table)) * dst_positive_scale_product_prefix_tablefirst)) /\ exists ff_q_pvs_product_prefix_tablefirstpositive. dst_positive_code_product_prefix_tablefirst = ff_q_pvs_product_prefix_tablefirstpositive * S ((S (scp_row_product_prefix_table)) * dst_positive_scale_product_prefix_tablefirst) + (dst_positive_product_prefix_tablefirst))) /\ (((((exists ff_h_pvs_product_prefix_tablefirstnegative. ff_h_pvs_product_prefix_tablefirstnegative + S (dst_negative_product_prefix_tablefirst) = S ((S (scp_row_product_prefix_table)) * dst_negative_scale_product_prefix_tablefirst)) /\ exists ff_q_pvs_product_prefix_tablefirstnegative. dst_negative_code_product_prefix_tablefirst = ff_q_pvs_product_prefix_tablefirstnegative * S ((S (scp_row_product_prefix_table)) * dst_negative_scale_product_prefix_tablefirst) + (dst_negative_product_prefix_tablefirst))) /\ (exists ge_balance_positive_product_prefix_tablefirstvalue ge_balance_negative_product_prefix_tablefirstvalue. (((((scp_first_product_prefix_table) = 2 * (ge_balance_positive_product_prefix_tablefirstvalue) /\ (ge_balance_negative_product_prefix_tablefirstvalue) = 0) \/ exists ge_signed_half_product_prefix_tablefirstvaluedecode. (((scp_first_product_prefix_table) = 2 * ge_signed_half_product_prefix_tablefirstvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tablefirstvalue) = 0) /\ (ge_balance_negative_product_prefix_tablefirstvalue) = S ge_signed_half_product_prefix_tablefirstvaluedecode))) /\ ((dst_positive_product_prefix_tablefirst) + ge_balance_negative_product_prefix_tablefirstvalue = (dst_negative_product_prefix_tablefirst) + ge_balance_positive_product_prefix_tablefirstvalue))))))))) -> (exists dst_positive_code_product_prefix_tablesecond dst_positive_scale_product_prefix_tablesecond dst_negative_code_product_prefix_tablesecond dst_negative_scale_product_prefix_tablesecond dst_positive_product_prefix_tablesecond dst_negative_product_prefix_tablesecond. (((G) = (((((dst_positive_code_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond)) * S ((dst_positive_code_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond)) + ((dst_positive_scale_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond))) + (((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) * S ((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) + ((dst_negative_scale_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)))) * S ((((dst_positive_code_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond)) * S ((dst_positive_code_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond)) + ((dst_positive_scale_product_prefix_tablesecond) + (dst_positive_scale_product_prefix_tablesecond))) + (((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) * S ((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) + ((dst_negative_scale_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)))) + ((((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) * S ((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) + ((dst_negative_scale_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond))) + (((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) * S ((dst_negative_code_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)) + ((dst_negative_scale_product_prefix_tablesecond) + (dst_negative_scale_product_prefix_tablesecond)))))) /\ (((((exists ff_h_pvs_product_prefix_tablesecondpositive. ff_h_pvs_product_prefix_tablesecondpositive + S (dst_positive_product_prefix_tablesecond) = S ((S (scp_column_product_prefix_table)) * dst_positive_scale_product_prefix_tablesecond)) /\ exists ff_q_pvs_product_prefix_tablesecondpositive. dst_positive_code_product_prefix_tablesecond = ff_q_pvs_product_prefix_tablesecondpositive * S ((S (scp_column_product_prefix_table)) * dst_positive_scale_product_prefix_tablesecond) + (dst_positive_product_prefix_tablesecond))) /\ (((((exists ff_h_pvs_product_prefix_tablesecondnegative. ff_h_pvs_product_prefix_tablesecondnegative + S (dst_negative_product_prefix_tablesecond) = S ((S (scp_column_product_prefix_table)) * dst_negative_scale_product_prefix_tablesecond)) /\ exists ff_q_pvs_product_prefix_tablesecondnegative. dst_negative_code_product_prefix_tablesecond = ff_q_pvs_product_prefix_tablesecondnegative * S ((S (scp_column_product_prefix_table)) * dst_negative_scale_product_prefix_tablesecond) + (dst_negative_product_prefix_tablesecond))) /\ (exists ge_balance_positive_product_prefix_tablesecondvalue ge_balance_negative_product_prefix_tablesecondvalue. (((((scp_second_product_prefix_table) = 2 * (ge_balance_positive_product_prefix_tablesecondvalue) /\ (ge_balance_negative_product_prefix_tablesecondvalue) = 0) \/ exists ge_signed_half_product_prefix_tablesecondvaluedecode. (((scp_second_product_prefix_table) = 2 * ge_signed_half_product_prefix_tablesecondvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tablesecondvalue) = 0) /\ (ge_balance_negative_product_prefix_tablesecondvalue) = S ge_signed_half_product_prefix_tablesecondvaluedecode))) /\ ((dst_positive_product_prefix_tablesecond) + ge_balance_negative_product_prefix_tablesecondvalue = (dst_negative_product_prefix_tablesecond) + ge_balance_positive_product_prefix_tablesecondvalue))))))))) -> (exists dst_positive_code_product_prefix_tableentry dst_positive_scale_product_prefix_tableentry dst_negative_code_product_prefix_tableentry dst_negative_scale_product_prefix_tableentry dst_positive_product_prefix_tableentry dst_negative_product_prefix_tableentry. (((T) = (((((dst_positive_code_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry)) * S ((dst_positive_code_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry)) + ((dst_positive_scale_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry))) + (((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) * S ((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) + ((dst_negative_scale_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)))) * S ((((dst_positive_code_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry)) * S ((dst_positive_code_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry)) + ((dst_positive_scale_product_prefix_tableentry) + (dst_positive_scale_product_prefix_tableentry))) + (((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) * S ((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) + ((dst_negative_scale_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)))) + ((((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) * S ((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) + ((dst_negative_scale_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry))) + (((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) * S ((dst_negative_code_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)) + ((dst_negative_scale_product_prefix_tableentry) + (dst_negative_scale_product_prefix_tableentry)))))) /\ (((((exists ff_h_pvs_product_prefix_tableentrypositive. ff_h_pvs_product_prefix_tableentrypositive + S (dst_positive_product_prefix_tableentry) = S ((S (((n)*(scp_row_product_prefix_table)+(scp_column_product_prefix_table)))) * dst_positive_scale_product_prefix_tableentry)) /\ exists ff_q_pvs_product_prefix_tableentrypositive. dst_positive_code_product_prefix_tableentry = ff_q_pvs_product_prefix_tableentrypositive * S ((S (((n)*(scp_row_product_prefix_table)+(scp_column_product_prefix_table)))) * dst_positive_scale_product_prefix_tableentry) + (dst_positive_product_prefix_tableentry))) /\ (((((exists ff_h_pvs_product_prefix_tableentrynegative. ff_h_pvs_product_prefix_tableentrynegative + S (dst_negative_product_prefix_tableentry) = S ((S (((n)*(scp_row_product_prefix_table)+(scp_column_product_prefix_table)))) * dst_negative_scale_product_prefix_tableentry)) /\ exists ff_q_pvs_product_prefix_tableentrynegative. dst_negative_code_product_prefix_tableentry = ff_q_pvs_product_prefix_tableentrynegative * S ((S (((n)*(scp_row_product_prefix_table)+(scp_column_product_prefix_table)))) * dst_negative_scale_product_prefix_tableentry) + (dst_negative_product_prefix_tableentry))) /\ (exists ge_balance_positive_product_prefix_tableentryvalue ge_balance_negative_product_prefix_tableentryvalue. (((((scp_value_product_prefix_table) = 2 * (ge_balance_positive_product_prefix_tableentryvalue) /\ (ge_balance_negative_product_prefix_tableentryvalue) = 0) \/ exists ge_signed_half_product_prefix_tableentryvaluedecode. (((scp_value_product_prefix_table) = 2 * ge_signed_half_product_prefix_tableentryvaluedecode + 1 /\ (ge_balance_positive_product_prefix_tableentryvalue) = 0) /\ (ge_balance_negative_product_prefix_tableentryvalue) = S ge_signed_half_product_prefix_tableentryvaluedecode))) /\ ((dst_positive_product_prefix_tableentry) + ge_balance_negative_product_prefix_tableentryvalue = (dst_negative_product_prefix_tableentry) + ge_balance_positive_product_prefix_tableentryvalue))))))))) -> (exists sto_ap_product_prefix_tablemultiply sto_an_product_prefix_tablemultiply sto_bp_product_prefix_tablemultiply sto_bn_product_prefix_tablemultiply sto_cp_product_prefix_tablemultiply sto_cn_product_prefix_tablemultiply. (((((scp_first_product_prefix_table) = 2 * (sto_ap_product_prefix_tablemultiply) /\ (sto_an_product_prefix_tablemultiply) = 0) \/ exists ge_signed_half_product_prefix_tablemultiplyleft. (((scp_first_product_prefix_table) = 2 * ge_signed_half_product_prefix_tablemultiplyleft + 1 /\ (sto_ap_product_prefix_tablemultiply) = 0) /\ (sto_an_product_prefix_tablemultiply) = S ge_signed_half_product_prefix_tablemultiplyleft))) /\ ((((((scp_second_product_prefix_table) = 2 * (sto_bp_product_prefix_tablemultiply) /\ (sto_bn_product_prefix_tablemultiply) = 0) \/ exists ge_signed_half_product_prefix_tablemultiplyright. (((scp_second_product_prefix_table) = 2 * ge_signed_half_product_prefix_tablemultiplyright + 1 /\ (sto_bp_product_prefix_tablemultiply) = 0) /\ (sto_bn_product_prefix_tablemultiply) = S ge_signed_half_product_prefix_tablemultiplyright))) /\ ((((((scp_value_product_prefix_table) = 2 * (sto_cp_product_prefix_tablemultiply) /\ (sto_cn_product_prefix_tablemultiply) = 0) \/ exists ge_signed_half_product_prefix_tablemultiplyoutput. (((scp_value_product_prefix_table) = 2 * ge_signed_half_product_prefix_tablemultiplyoutput + 1 /\ (sto_cp_product_prefix_tablemultiply) = 0) /\ (sto_cn_product_prefix_tablemultiply) = S ge_signed_half_product_prefix_tablemultiplyoutput))) /\ ((sto_ap_product_prefix_tablemultiply * sto_bp_product_prefix_tablemultiply + sto_an_product_prefix_tablemultiply * sto_bn_product_prefix_tablemultiply) + sto_cn_product_prefix_tablemultiply = (sto_ap_product_prefix_tablemultiply * sto_bn_product_prefix_tablemultiply + sto_an_product_prefix_tablemultiply * sto_bp_product_prefix_tablemultiply) + sto_cp_product_prefix_tablemultiply)))))))))))))) -> (exists dst_positive_code_product_prefix_first dst_positive_scale_product_prefix_first dst_negative_code_product_prefix_first dst_negative_scale_product_prefix_first dst_positive_sum_product_prefix_first dst_negative_sum_product_prefix_first. (((F) = (((((dst_positive_code_product_prefix_first) + (dst_positive_scale_product_prefix_first)) * S ((dst_positive_code_product_prefix_first) + (dst_positive_scale_product_prefix_first)) + ((dst_positive_scale_product_prefix_first) + (dst_positive_scale_product_prefix_first))) + (((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) * S ((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) + ((dst_negative_scale_product_prefix_first) + (dst_negative_scale_product_prefix_first)))) * S ((((dst_positive_code_product_prefix_first) + (dst_positive_scale_product_prefix_first)) * S ((dst_positive_code_product_prefix_first) + (dst_positive_scale_product_prefix_first)) + ((dst_positive_scale_product_prefix_first) + (dst_positive_scale_product_prefix_first))) + (((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) * S ((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) + ((dst_negative_scale_product_prefix_first) + (dst_negative_scale_product_prefix_first)))) + ((((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) * S ((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) + ((dst_negative_scale_product_prefix_first) + (dst_negative_scale_product_prefix_first))) + (((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) * S ((dst_negative_code_product_prefix_first) + (dst_negative_scale_product_prefix_first)) + ((dst_negative_scale_product_prefix_first) + (dst_negative_scale_product_prefix_first)))))) /\ (((exists fs_u_dst_product_prefix_firstpositive fs_v_dst_product_prefix_firstpositive. ((((exists fs_h_dst_product_prefix_firstpositive_body_start. fs_h_dst_product_prefix_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_firstpositive)) /\ exists fs_q_dst_product_prefix_firstpositive_body_start. fs_u_dst_product_prefix_firstpositive = fs_q_dst_product_prefix_firstpositive_body_start * S ((S (0)) * fs_v_dst_product_prefix_firstpositive) + (0))) /\ ((((exists fs_h_dst_product_prefix_firstpositive_body_terminal. fs_h_dst_product_prefix_firstpositive_body_terminal + S (dst_positive_sum_product_prefix_first) = S ((S (m)) * fs_v_dst_product_prefix_firstpositive)) /\ exists fs_q_dst_product_prefix_firstpositive_body_terminal. fs_u_dst_product_prefix_firstpositive = fs_q_dst_product_prefix_firstpositive_body_terminal * S ((S (m)) * fs_v_dst_product_prefix_firstpositive) + (dst_positive_sum_product_prefix_first))) /\ forall fs_i_dst_product_prefix_firstpositive_body_steps. (exists fs_lt_dst_product_prefix_firstpositive_body_steps_bound. fs_lt_dst_product_prefix_firstpositive_body_steps_bound + S fs_i_dst_product_prefix_firstpositive_body_steps = m) -> exists fs_a_dst_product_prefix_firstpositive_body_steps fs_r_dst_product_prefix_firstpositive_body_steps fs_s_dst_product_prefix_firstpositive_body_steps. ((((exists fs_h_dst_product_prefix_firstpositive_body_steps_summand. fs_h_dst_product_prefix_firstpositive_body_steps_summand + S (fs_a_dst_product_prefix_firstpositive_body_steps) = S ((S (fs_i_dst_product_prefix_firstpositive_body_steps)) * dst_positive_scale_product_prefix_first)) /\ exists fs_q_dst_product_prefix_firstpositive_body_steps_summand. dst_positive_code_product_prefix_first = fs_q_dst_product_prefix_firstpositive_body_steps_summand * S ((S (fs_i_dst_product_prefix_firstpositive_body_steps)) * dst_positive_scale_product_prefix_first) + (fs_a_dst_product_prefix_firstpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_firstpositive_body_steps_partial. fs_h_dst_product_prefix_firstpositive_body_steps_partial + S (fs_r_dst_product_prefix_firstpositive_body_steps) = S ((S (fs_i_dst_product_prefix_firstpositive_body_steps)) * fs_v_dst_product_prefix_firstpositive)) /\ exists fs_q_dst_product_prefix_firstpositive_body_steps_partial. fs_u_dst_product_prefix_firstpositive = fs_q_dst_product_prefix_firstpositive_body_steps_partial * S ((S (fs_i_dst_product_prefix_firstpositive_body_steps)) * fs_v_dst_product_prefix_firstpositive) + (fs_r_dst_product_prefix_firstpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_firstpositive_body_steps_successor. fs_h_dst_product_prefix_firstpositive_body_steps_successor + S (fs_s_dst_product_prefix_firstpositive_body_steps) = S ((S (S fs_i_dst_product_prefix_firstpositive_body_steps)) * fs_v_dst_product_prefix_firstpositive)) /\ exists fs_q_dst_product_prefix_firstpositive_body_steps_successor. fs_u_dst_product_prefix_firstpositive = fs_q_dst_product_prefix_firstpositive_body_steps_successor * S ((S (S fs_i_dst_product_prefix_firstpositive_body_steps)) * fs_v_dst_product_prefix_firstpositive) + (fs_s_dst_product_prefix_firstpositive_body_steps))) /\ fs_s_dst_product_prefix_firstpositive_body_steps = fs_r_dst_product_prefix_firstpositive_body_steps + fs_a_dst_product_prefix_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_product_prefix_firstnegative fs_v_dst_product_prefix_firstnegative. ((((exists fs_h_dst_product_prefix_firstnegative_body_start. fs_h_dst_product_prefix_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_firstnegative)) /\ exists fs_q_dst_product_prefix_firstnegative_body_start. fs_u_dst_product_prefix_firstnegative = fs_q_dst_product_prefix_firstnegative_body_start * S ((S (0)) * fs_v_dst_product_prefix_firstnegative) + (0))) /\ ((((exists fs_h_dst_product_prefix_firstnegative_body_terminal. fs_h_dst_product_prefix_firstnegative_body_terminal + S (dst_negative_sum_product_prefix_first) = S ((S (m)) * fs_v_dst_product_prefix_firstnegative)) /\ exists fs_q_dst_product_prefix_firstnegative_body_terminal. fs_u_dst_product_prefix_firstnegative = fs_q_dst_product_prefix_firstnegative_body_terminal * S ((S (m)) * fs_v_dst_product_prefix_firstnegative) + (dst_negative_sum_product_prefix_first))) /\ forall fs_i_dst_product_prefix_firstnegative_body_steps. (exists fs_lt_dst_product_prefix_firstnegative_body_steps_bound. fs_lt_dst_product_prefix_firstnegative_body_steps_bound + S fs_i_dst_product_prefix_firstnegative_body_steps = m) -> exists fs_a_dst_product_prefix_firstnegative_body_steps fs_r_dst_product_prefix_firstnegative_body_steps fs_s_dst_product_prefix_firstnegative_body_steps. ((((exists fs_h_dst_product_prefix_firstnegative_body_steps_summand. fs_h_dst_product_prefix_firstnegative_body_steps_summand + S (fs_a_dst_product_prefix_firstnegative_body_steps) = S ((S (fs_i_dst_product_prefix_firstnegative_body_steps)) * dst_negative_scale_product_prefix_first)) /\ exists fs_q_dst_product_prefix_firstnegative_body_steps_summand. dst_negative_code_product_prefix_first = fs_q_dst_product_prefix_firstnegative_body_steps_summand * S ((S (fs_i_dst_product_prefix_firstnegative_body_steps)) * dst_negative_scale_product_prefix_first) + (fs_a_dst_product_prefix_firstnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_firstnegative_body_steps_partial. fs_h_dst_product_prefix_firstnegative_body_steps_partial + S (fs_r_dst_product_prefix_firstnegative_body_steps) = S ((S (fs_i_dst_product_prefix_firstnegative_body_steps)) * fs_v_dst_product_prefix_firstnegative)) /\ exists fs_q_dst_product_prefix_firstnegative_body_steps_partial. fs_u_dst_product_prefix_firstnegative = fs_q_dst_product_prefix_firstnegative_body_steps_partial * S ((S (fs_i_dst_product_prefix_firstnegative_body_steps)) * fs_v_dst_product_prefix_firstnegative) + (fs_r_dst_product_prefix_firstnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_firstnegative_body_steps_successor. fs_h_dst_product_prefix_firstnegative_body_steps_successor + S (fs_s_dst_product_prefix_firstnegative_body_steps) = S ((S (S fs_i_dst_product_prefix_firstnegative_body_steps)) * fs_v_dst_product_prefix_firstnegative)) /\ exists fs_q_dst_product_prefix_firstnegative_body_steps_successor. fs_u_dst_product_prefix_firstnegative = fs_q_dst_product_prefix_firstnegative_body_steps_successor * S ((S (S fs_i_dst_product_prefix_firstnegative_body_steps)) * fs_v_dst_product_prefix_firstnegative) + (fs_s_dst_product_prefix_firstnegative_body_steps))) /\ fs_s_dst_product_prefix_firstnegative_body_steps = fs_r_dst_product_prefix_firstnegative_body_steps + fs_a_dst_product_prefix_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_product_prefix_firstresult ge_balance_negative_product_prefix_firstresult. (((((a) = 2 * (ge_balance_positive_product_prefix_firstresult) /\ (ge_balance_negative_product_prefix_firstresult) = 0) \/ exists ge_signed_half_product_prefix_firstresultdecode. (((a) = 2 * ge_signed_half_product_prefix_firstresultdecode + 1 /\ (ge_balance_positive_product_prefix_firstresult) = 0) /\ (ge_balance_negative_product_prefix_firstresult) = S ge_signed_half_product_prefix_firstresultdecode))) /\ ((dst_positive_sum_product_prefix_first) + ge_balance_negative_product_prefix_firstresult = (dst_negative_sum_product_prefix_first) + ge_balance_positive_product_prefix_firstresult))))))))) -> (exists dst_positive_code_product_prefix_second dst_positive_scale_product_prefix_second dst_negative_code_product_prefix_second dst_negative_scale_product_prefix_second dst_positive_sum_product_prefix_second dst_negative_sum_product_prefix_second. (((G) = (((((dst_positive_code_product_prefix_second) + (dst_positive_scale_product_prefix_second)) * S ((dst_positive_code_product_prefix_second) + (dst_positive_scale_product_prefix_second)) + ((dst_positive_scale_product_prefix_second) + (dst_positive_scale_product_prefix_second))) + (((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) * S ((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) + ((dst_negative_scale_product_prefix_second) + (dst_negative_scale_product_prefix_second)))) * S ((((dst_positive_code_product_prefix_second) + (dst_positive_scale_product_prefix_second)) * S ((dst_positive_code_product_prefix_second) + (dst_positive_scale_product_prefix_second)) + ((dst_positive_scale_product_prefix_second) + (dst_positive_scale_product_prefix_second))) + (((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) * S ((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) + ((dst_negative_scale_product_prefix_second) + (dst_negative_scale_product_prefix_second)))) + ((((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) * S ((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) + ((dst_negative_scale_product_prefix_second) + (dst_negative_scale_product_prefix_second))) + (((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) * S ((dst_negative_code_product_prefix_second) + (dst_negative_scale_product_prefix_second)) + ((dst_negative_scale_product_prefix_second) + (dst_negative_scale_product_prefix_second)))))) /\ (((exists fs_u_dst_product_prefix_secondpositive fs_v_dst_product_prefix_secondpositive. ((((exists fs_h_dst_product_prefix_secondpositive_body_start. fs_h_dst_product_prefix_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_secondpositive)) /\ exists fs_q_dst_product_prefix_secondpositive_body_start. fs_u_dst_product_prefix_secondpositive = fs_q_dst_product_prefix_secondpositive_body_start * S ((S (0)) * fs_v_dst_product_prefix_secondpositive) + (0))) /\ ((((exists fs_h_dst_product_prefix_secondpositive_body_terminal. fs_h_dst_product_prefix_secondpositive_body_terminal + S (dst_positive_sum_product_prefix_second) = S ((S (n)) * fs_v_dst_product_prefix_secondpositive)) /\ exists fs_q_dst_product_prefix_secondpositive_body_terminal. fs_u_dst_product_prefix_secondpositive = fs_q_dst_product_prefix_secondpositive_body_terminal * S ((S (n)) * fs_v_dst_product_prefix_secondpositive) + (dst_positive_sum_product_prefix_second))) /\ forall fs_i_dst_product_prefix_secondpositive_body_steps. (exists fs_lt_dst_product_prefix_secondpositive_body_steps_bound. fs_lt_dst_product_prefix_secondpositive_body_steps_bound + S fs_i_dst_product_prefix_secondpositive_body_steps = n) -> exists fs_a_dst_product_prefix_secondpositive_body_steps fs_r_dst_product_prefix_secondpositive_body_steps fs_s_dst_product_prefix_secondpositive_body_steps. ((((exists fs_h_dst_product_prefix_secondpositive_body_steps_summand. fs_h_dst_product_prefix_secondpositive_body_steps_summand + S (fs_a_dst_product_prefix_secondpositive_body_steps) = S ((S (fs_i_dst_product_prefix_secondpositive_body_steps)) * dst_positive_scale_product_prefix_second)) /\ exists fs_q_dst_product_prefix_secondpositive_body_steps_summand. dst_positive_code_product_prefix_second = fs_q_dst_product_prefix_secondpositive_body_steps_summand * S ((S (fs_i_dst_product_prefix_secondpositive_body_steps)) * dst_positive_scale_product_prefix_second) + (fs_a_dst_product_prefix_secondpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_secondpositive_body_steps_partial. fs_h_dst_product_prefix_secondpositive_body_steps_partial + S (fs_r_dst_product_prefix_secondpositive_body_steps) = S ((S (fs_i_dst_product_prefix_secondpositive_body_steps)) * fs_v_dst_product_prefix_secondpositive)) /\ exists fs_q_dst_product_prefix_secondpositive_body_steps_partial. fs_u_dst_product_prefix_secondpositive = fs_q_dst_product_prefix_secondpositive_body_steps_partial * S ((S (fs_i_dst_product_prefix_secondpositive_body_steps)) * fs_v_dst_product_prefix_secondpositive) + (fs_r_dst_product_prefix_secondpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_secondpositive_body_steps_successor. fs_h_dst_product_prefix_secondpositive_body_steps_successor + S (fs_s_dst_product_prefix_secondpositive_body_steps) = S ((S (S fs_i_dst_product_prefix_secondpositive_body_steps)) * fs_v_dst_product_prefix_secondpositive)) /\ exists fs_q_dst_product_prefix_secondpositive_body_steps_successor. fs_u_dst_product_prefix_secondpositive = fs_q_dst_product_prefix_secondpositive_body_steps_successor * S ((S (S fs_i_dst_product_prefix_secondpositive_body_steps)) * fs_v_dst_product_prefix_secondpositive) + (fs_s_dst_product_prefix_secondpositive_body_steps))) /\ fs_s_dst_product_prefix_secondpositive_body_steps = fs_r_dst_product_prefix_secondpositive_body_steps + fs_a_dst_product_prefix_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_product_prefix_secondnegative fs_v_dst_product_prefix_secondnegative. ((((exists fs_h_dst_product_prefix_secondnegative_body_start. fs_h_dst_product_prefix_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_secondnegative)) /\ exists fs_q_dst_product_prefix_secondnegative_body_start. fs_u_dst_product_prefix_secondnegative = fs_q_dst_product_prefix_secondnegative_body_start * S ((S (0)) * fs_v_dst_product_prefix_secondnegative) + (0))) /\ ((((exists fs_h_dst_product_prefix_secondnegative_body_terminal. fs_h_dst_product_prefix_secondnegative_body_terminal + S (dst_negative_sum_product_prefix_second) = S ((S (n)) * fs_v_dst_product_prefix_secondnegative)) /\ exists fs_q_dst_product_prefix_secondnegative_body_terminal. fs_u_dst_product_prefix_secondnegative = fs_q_dst_product_prefix_secondnegative_body_terminal * S ((S (n)) * fs_v_dst_product_prefix_secondnegative) + (dst_negative_sum_product_prefix_second))) /\ forall fs_i_dst_product_prefix_secondnegative_body_steps. (exists fs_lt_dst_product_prefix_secondnegative_body_steps_bound. fs_lt_dst_product_prefix_secondnegative_body_steps_bound + S fs_i_dst_product_prefix_secondnegative_body_steps = n) -> exists fs_a_dst_product_prefix_secondnegative_body_steps fs_r_dst_product_prefix_secondnegative_body_steps fs_s_dst_product_prefix_secondnegative_body_steps. ((((exists fs_h_dst_product_prefix_secondnegative_body_steps_summand. fs_h_dst_product_prefix_secondnegative_body_steps_summand + S (fs_a_dst_product_prefix_secondnegative_body_steps) = S ((S (fs_i_dst_product_prefix_secondnegative_body_steps)) * dst_negative_scale_product_prefix_second)) /\ exists fs_q_dst_product_prefix_secondnegative_body_steps_summand. dst_negative_code_product_prefix_second = fs_q_dst_product_prefix_secondnegative_body_steps_summand * S ((S (fs_i_dst_product_prefix_secondnegative_body_steps)) * dst_negative_scale_product_prefix_second) + (fs_a_dst_product_prefix_secondnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_secondnegative_body_steps_partial. fs_h_dst_product_prefix_secondnegative_body_steps_partial + S (fs_r_dst_product_prefix_secondnegative_body_steps) = S ((S (fs_i_dst_product_prefix_secondnegative_body_steps)) * fs_v_dst_product_prefix_secondnegative)) /\ exists fs_q_dst_product_prefix_secondnegative_body_steps_partial. fs_u_dst_product_prefix_secondnegative = fs_q_dst_product_prefix_secondnegative_body_steps_partial * S ((S (fs_i_dst_product_prefix_secondnegative_body_steps)) * fs_v_dst_product_prefix_secondnegative) + (fs_r_dst_product_prefix_secondnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_secondnegative_body_steps_successor. fs_h_dst_product_prefix_secondnegative_body_steps_successor + S (fs_s_dst_product_prefix_secondnegative_body_steps) = S ((S (S fs_i_dst_product_prefix_secondnegative_body_steps)) * fs_v_dst_product_prefix_secondnegative)) /\ exists fs_q_dst_product_prefix_secondnegative_body_steps_successor. fs_u_dst_product_prefix_secondnegative = fs_q_dst_product_prefix_secondnegative_body_steps_successor * S ((S (S fs_i_dst_product_prefix_secondnegative_body_steps)) * fs_v_dst_product_prefix_secondnegative) + (fs_s_dst_product_prefix_secondnegative_body_steps))) /\ fs_s_dst_product_prefix_secondnegative_body_steps = fs_r_dst_product_prefix_secondnegative_body_steps + fs_a_dst_product_prefix_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_product_prefix_secondresult ge_balance_negative_product_prefix_secondresult. (((((b) = 2 * (ge_balance_positive_product_prefix_secondresult) /\ (ge_balance_negative_product_prefix_secondresult) = 0) \/ exists ge_signed_half_product_prefix_secondresultdecode. (((b) = 2 * ge_signed_half_product_prefix_secondresultdecode + 1 /\ (ge_balance_positive_product_prefix_secondresult) = 0) /\ (ge_balance_negative_product_prefix_secondresult) = S ge_signed_half_product_prefix_secondresultdecode))) /\ ((dst_positive_sum_product_prefix_second) + ge_balance_negative_product_prefix_secondresult = (dst_negative_sum_product_prefix_second) + ge_balance_positive_product_prefix_secondresult))))))))) -> (exists dst_positive_code_product_prefix_total dst_positive_scale_product_prefix_total dst_negative_code_product_prefix_total dst_negative_scale_product_prefix_total dst_positive_sum_product_prefix_total dst_negative_sum_product_prefix_total. (((T) = (((((dst_positive_code_product_prefix_total) + (dst_positive_scale_product_prefix_total)) * S ((dst_positive_code_product_prefix_total) + (dst_positive_scale_product_prefix_total)) + ((dst_positive_scale_product_prefix_total) + (dst_positive_scale_product_prefix_total))) + (((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) * S ((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) + ((dst_negative_scale_product_prefix_total) + (dst_negative_scale_product_prefix_total)))) * S ((((dst_positive_code_product_prefix_total) + (dst_positive_scale_product_prefix_total)) * S ((dst_positive_code_product_prefix_total) + (dst_positive_scale_product_prefix_total)) + ((dst_positive_scale_product_prefix_total) + (dst_positive_scale_product_prefix_total))) + (((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) * S ((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) + ((dst_negative_scale_product_prefix_total) + (dst_negative_scale_product_prefix_total)))) + ((((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) * S ((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) + ((dst_negative_scale_product_prefix_total) + (dst_negative_scale_product_prefix_total))) + (((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) * S ((dst_negative_code_product_prefix_total) + (dst_negative_scale_product_prefix_total)) + ((dst_negative_scale_product_prefix_total) + (dst_negative_scale_product_prefix_total)))))) /\ (((exists fs_u_dst_product_prefix_totalpositive fs_v_dst_product_prefix_totalpositive. ((((exists fs_h_dst_product_prefix_totalpositive_body_start. fs_h_dst_product_prefix_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_totalpositive)) /\ exists fs_q_dst_product_prefix_totalpositive_body_start. fs_u_dst_product_prefix_totalpositive = fs_q_dst_product_prefix_totalpositive_body_start * S ((S (0)) * fs_v_dst_product_prefix_totalpositive) + (0))) /\ ((((exists fs_h_dst_product_prefix_totalpositive_body_terminal. fs_h_dst_product_prefix_totalpositive_body_terminal + S (dst_positive_sum_product_prefix_total) = S ((S (m*n)) * fs_v_dst_product_prefix_totalpositive)) /\ exists fs_q_dst_product_prefix_totalpositive_body_terminal. fs_u_dst_product_prefix_totalpositive = fs_q_dst_product_prefix_totalpositive_body_terminal * S ((S (m*n)) * fs_v_dst_product_prefix_totalpositive) + (dst_positive_sum_product_prefix_total))) /\ forall fs_i_dst_product_prefix_totalpositive_body_steps. (exists fs_lt_dst_product_prefix_totalpositive_body_steps_bound. fs_lt_dst_product_prefix_totalpositive_body_steps_bound + S fs_i_dst_product_prefix_totalpositive_body_steps = m*n) -> exists fs_a_dst_product_prefix_totalpositive_body_steps fs_r_dst_product_prefix_totalpositive_body_steps fs_s_dst_product_prefix_totalpositive_body_steps. ((((exists fs_h_dst_product_prefix_totalpositive_body_steps_summand. fs_h_dst_product_prefix_totalpositive_body_steps_summand + S (fs_a_dst_product_prefix_totalpositive_body_steps) = S ((S (fs_i_dst_product_prefix_totalpositive_body_steps)) * dst_positive_scale_product_prefix_total)) /\ exists fs_q_dst_product_prefix_totalpositive_body_steps_summand. dst_positive_code_product_prefix_total = fs_q_dst_product_prefix_totalpositive_body_steps_summand * S ((S (fs_i_dst_product_prefix_totalpositive_body_steps)) * dst_positive_scale_product_prefix_total) + (fs_a_dst_product_prefix_totalpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_totalpositive_body_steps_partial. fs_h_dst_product_prefix_totalpositive_body_steps_partial + S (fs_r_dst_product_prefix_totalpositive_body_steps) = S ((S (fs_i_dst_product_prefix_totalpositive_body_steps)) * fs_v_dst_product_prefix_totalpositive)) /\ exists fs_q_dst_product_prefix_totalpositive_body_steps_partial. fs_u_dst_product_prefix_totalpositive = fs_q_dst_product_prefix_totalpositive_body_steps_partial * S ((S (fs_i_dst_product_prefix_totalpositive_body_steps)) * fs_v_dst_product_prefix_totalpositive) + (fs_r_dst_product_prefix_totalpositive_body_steps))) /\ ((((exists fs_h_dst_product_prefix_totalpositive_body_steps_successor. fs_h_dst_product_prefix_totalpositive_body_steps_successor + S (fs_s_dst_product_prefix_totalpositive_body_steps) = S ((S (S fs_i_dst_product_prefix_totalpositive_body_steps)) * fs_v_dst_product_prefix_totalpositive)) /\ exists fs_q_dst_product_prefix_totalpositive_body_steps_successor. fs_u_dst_product_prefix_totalpositive = fs_q_dst_product_prefix_totalpositive_body_steps_successor * S ((S (S fs_i_dst_product_prefix_totalpositive_body_steps)) * fs_v_dst_product_prefix_totalpositive) + (fs_s_dst_product_prefix_totalpositive_body_steps))) /\ fs_s_dst_product_prefix_totalpositive_body_steps = fs_r_dst_product_prefix_totalpositive_body_steps + fs_a_dst_product_prefix_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_product_prefix_totalnegative fs_v_dst_product_prefix_totalnegative. ((((exists fs_h_dst_product_prefix_totalnegative_body_start. fs_h_dst_product_prefix_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_product_prefix_totalnegative)) /\ exists fs_q_dst_product_prefix_totalnegative_body_start. fs_u_dst_product_prefix_totalnegative = fs_q_dst_product_prefix_totalnegative_body_start * S ((S (0)) * fs_v_dst_product_prefix_totalnegative) + (0))) /\ ((((exists fs_h_dst_product_prefix_totalnegative_body_terminal. fs_h_dst_product_prefix_totalnegative_body_terminal + S (dst_negative_sum_product_prefix_total) = S ((S (m*n)) * fs_v_dst_product_prefix_totalnegative)) /\ exists fs_q_dst_product_prefix_totalnegative_body_terminal. fs_u_dst_product_prefix_totalnegative = fs_q_dst_product_prefix_totalnegative_body_terminal * S ((S (m*n)) * fs_v_dst_product_prefix_totalnegative) + (dst_negative_sum_product_prefix_total))) /\ forall fs_i_dst_product_prefix_totalnegative_body_steps. (exists fs_lt_dst_product_prefix_totalnegative_body_steps_bound. fs_lt_dst_product_prefix_totalnegative_body_steps_bound + S fs_i_dst_product_prefix_totalnegative_body_steps = m*n) -> exists fs_a_dst_product_prefix_totalnegative_body_steps fs_r_dst_product_prefix_totalnegative_body_steps fs_s_dst_product_prefix_totalnegative_body_steps. ((((exists fs_h_dst_product_prefix_totalnegative_body_steps_summand. fs_h_dst_product_prefix_totalnegative_body_steps_summand + S (fs_a_dst_product_prefix_totalnegative_body_steps) = S ((S (fs_i_dst_product_prefix_totalnegative_body_steps)) * dst_negative_scale_product_prefix_total)) /\ exists fs_q_dst_product_prefix_totalnegative_body_steps_summand. dst_negative_code_product_prefix_total = fs_q_dst_product_prefix_totalnegative_body_steps_summand * S ((S (fs_i_dst_product_prefix_totalnegative_body_steps)) * dst_negative_scale_product_prefix_total) + (fs_a_dst_product_prefix_totalnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_totalnegative_body_steps_partial. fs_h_dst_product_prefix_totalnegative_body_steps_partial + S (fs_r_dst_product_prefix_totalnegative_body_steps) = S ((S (fs_i_dst_product_prefix_totalnegative_body_steps)) * fs_v_dst_product_prefix_totalnegative)) /\ exists fs_q_dst_product_prefix_totalnegative_body_steps_partial. fs_u_dst_product_prefix_totalnegative = fs_q_dst_product_prefix_totalnegative_body_steps_partial * S ((S (fs_i_dst_product_prefix_totalnegative_body_steps)) * fs_v_dst_product_prefix_totalnegative) + (fs_r_dst_product_prefix_totalnegative_body_steps))) /\ ((((exists fs_h_dst_product_prefix_totalnegative_body_steps_successor. fs_h_dst_product_prefix_totalnegative_body_steps_successor + S (fs_s_dst_product_prefix_totalnegative_body_steps) = S ((S (S fs_i_dst_product_prefix_totalnegative_body_steps)) * fs_v_dst_product_prefix_totalnegative)) /\ exists fs_q_dst_product_prefix_totalnegative_body_steps_successor. fs_u_dst_product_prefix_totalnegative = fs_q_dst_product_prefix_totalnegative_body_steps_successor * S ((S (S fs_i_dst_product_prefix_totalnegative_body_steps)) * fs_v_dst_product_prefix_totalnegative) + (fs_s_dst_product_prefix_totalnegative_body_steps))) /\ fs_s_dst_product_prefix_totalnegative_body_steps = fs_r_dst_product_prefix_totalnegative_body_steps + fs_a_dst_product_prefix_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_product_prefix_totalresult ge_balance_negative_product_prefix_totalresult. (((((c) = 2 * (ge_balance_positive_product_prefix_totalresult) /\ (ge_balance_negative_product_prefix_totalresult) = 0) \/ exists ge_signed_half_product_prefix_totalresultdecode. (((c) = 2 * ge_signed_half_product_prefix_totalresultdecode + 1 /\ (ge_balance_positive_product_prefix_totalresult) = 0) /\ (ge_balance_negative_product_prefix_totalresult) = S ge_signed_half_product_prefix_totalresultdecode))) /\ ((dst_positive_sum_product_prefix_total) + ge_balance_negative_product_prefix_totalresult = (dst_negative_sum_product_prefix_total) + ge_balance_positive_product_prefix_totalresult))))))))) -> (exists sto_ap_product_prefix_result sto_an_product_prefix_result sto_bp_product_prefix_result sto_bn_product_prefix_result sto_cp_product_prefix_result sto_cn_product_prefix_result. (((((a) = 2 * (sto_ap_product_prefix_result) /\ (sto_an_product_prefix_result) = 0) \/ exists ge_signed_half_product_prefix_resultleft. (((a) = 2 * ge_signed_half_product_prefix_resultleft + 1 /\ (sto_ap_product_prefix_result) = 0) /\ (sto_an_product_prefix_result) = S ge_signed_half_product_prefix_resultleft))) /\ ((((((b) = 2 * (sto_bp_product_prefix_result) /\ (sto_bn_product_prefix_result) = 0) \/ exists ge_signed_half_product_prefix_resultright. (((b) = 2 * ge_signed_half_product_prefix_resultright + 1 /\ (sto_bp_product_prefix_result) = 0) /\ (sto_bn_product_prefix_result) = S ge_signed_half_product_prefix_resultright))) /\ ((((((c) = 2 * (sto_cp_product_prefix_result) /\ (sto_cn_product_prefix_result) = 0) \/ exists ge_signed_half_product_prefix_resultoutput. (((c) = 2 * ge_signed_half_product_prefix_resultoutput + 1 /\ (sto_cp_product_prefix_result) = 0) /\ (sto_cn_product_prefix_result) = S ge_signed_half_product_prefix_resultoutput))) /\ ((sto_ap_product_prefix_result * sto_bp_product_prefix_result + sto_an_product_prefix_result * sto_bn_product_prefix_result) + sto_cn_product_prefix_result = (sto_ap_product_prefix_result * sto_bn_product_prefix_result + sto_an_product_prefix_result * sto_bp_product_prefix_result) + sto_cp_product_prefix_result)))))))