signed_prefix_sum_row_major_iff

Exact expanded first-order arithmetic statement

forall F m n z. (exists dst_positive_code_flat_source dst_positive_scale_flat_source dst_negative_code_flat_source dst_negative_scale_flat_source. (((F) = (((((dst_positive_code_flat_source) + (dst_positive_scale_flat_source)) * S ((dst_positive_code_flat_source) + (dst_positive_scale_flat_source)) + ((dst_positive_scale_flat_source) + (dst_positive_scale_flat_source))) + (((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) * S ((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) + ((dst_negative_scale_flat_source) + (dst_negative_scale_flat_source)))) * S ((((dst_positive_code_flat_source) + (dst_positive_scale_flat_source)) * S ((dst_positive_code_flat_source) + (dst_positive_scale_flat_source)) + ((dst_positive_scale_flat_source) + (dst_positive_scale_flat_source))) + (((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) * S ((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) + ((dst_negative_scale_flat_source) + (dst_negative_scale_flat_source)))) + ((((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) * S ((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) + ((dst_negative_scale_flat_source) + (dst_negative_scale_flat_source))) + (((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) * S ((dst_negative_code_flat_source) + (dst_negative_scale_flat_source)) + ((dst_negative_scale_flat_source) + (dst_negative_scale_flat_source)))))) /\ (forall dst_index_flat_source. (exists pvs_le_gap_flat_sourcedomain. pvs_le_gap_flat_sourcedomain + (dst_index_flat_source) = (0)) -> exists dst_positive_flat_source dst_negative_flat_source dst_value_flat_source. ((((exists ff_h_pvs_flat_sourceentrypositive. ff_h_pvs_flat_sourceentrypositive + S (dst_positive_flat_source) = S ((S (dst_index_flat_source)) * dst_positive_scale_flat_source)) /\ exists ff_q_pvs_flat_sourceentrypositive. dst_positive_code_flat_source = ff_q_pvs_flat_sourceentrypositive * S ((S (dst_index_flat_source)) * dst_positive_scale_flat_source) + (dst_positive_flat_source))) /\ (((((exists ff_h_pvs_flat_sourceentrynegative. ff_h_pvs_flat_sourceentrynegative + S (dst_negative_flat_source) = S ((S (dst_index_flat_source)) * dst_negative_scale_flat_source)) /\ exists ff_q_pvs_flat_sourceentrynegative. dst_negative_code_flat_source = ff_q_pvs_flat_sourceentrynegative * S ((S (dst_index_flat_source)) * dst_negative_scale_flat_source) + (dst_negative_flat_source))) /\ (exists ge_balance_positive_flat_sourceentryvalue ge_balance_negative_flat_sourceentryvalue. (((((dst_value_flat_source) = 2 * (ge_balance_positive_flat_sourceentryvalue) /\ (ge_balance_negative_flat_sourceentryvalue) = 0) \/ exists ge_signed_half_flat_sourceentryvaluedecode. (((dst_value_flat_source) = 2 * ge_signed_half_flat_sourceentryvaluedecode + 1 /\ (ge_balance_positive_flat_sourceentryvalue) = 0) /\ (ge_balance_negative_flat_sourceentryvalue) = S ge_signed_half_flat_sourceentryvaluedecode))) /\ ((dst_positive_flat_source) + ge_balance_negative_flat_sourceentryvalue = (dst_negative_flat_source) + ge_balance_positive_flat_sourceentryvalue))))))))) -> (((exists dst_positive_code_flat_prefix dst_positive_scale_flat_prefix dst_negative_code_flat_prefix dst_negative_scale_flat_prefix dst_positive_sum_flat_prefix dst_negative_sum_flat_prefix. (((F) = (((((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) * S ((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) + ((dst_positive_scale_flat_prefix) + (dst_positive_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))) * S ((((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) * S ((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) + ((dst_positive_scale_flat_prefix) + (dst_positive_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))) + ((((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))))) /\ (((exists fs_u_dst_flat_prefixpositive fs_v_dst_flat_prefixpositive. ((((exists fs_h_dst_flat_prefixpositive_body_start. fs_h_dst_flat_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_start. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_start * S ((S (0)) * fs_v_dst_flat_prefixpositive) + (0))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_terminal. fs_h_dst_flat_prefixpositive_body_terminal + S (dst_positive_sum_flat_prefix) = S ((S (m*n)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_terminal. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_terminal * S ((S (m*n)) * fs_v_dst_flat_prefixpositive) + (dst_positive_sum_flat_prefix))) /\ forall fs_i_dst_flat_prefixpositive_body_steps. (exists fs_lt_dst_flat_prefixpositive_body_steps_bound. fs_lt_dst_flat_prefixpositive_body_steps_bound + S fs_i_dst_flat_prefixpositive_body_steps = m*n) -> exists fs_a_dst_flat_prefixpositive_body_steps fs_r_dst_flat_prefixpositive_body_steps fs_s_dst_flat_prefixpositive_body_steps. ((((exists fs_h_dst_flat_prefixpositive_body_steps_summand. fs_h_dst_flat_prefixpositive_body_steps_summand + S (fs_a_dst_flat_prefixpositive_body_steps) = S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * dst_positive_scale_flat_prefix)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_summand. dst_positive_code_flat_prefix = fs_q_dst_flat_prefixpositive_body_steps_summand * S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * dst_positive_scale_flat_prefix) + (fs_a_dst_flat_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_steps_partial. fs_h_dst_flat_prefixpositive_body_steps_partial + S (fs_r_dst_flat_prefixpositive_body_steps) = S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_partial. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_steps_partial * S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive) + (fs_r_dst_flat_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_steps_successor. fs_h_dst_flat_prefixpositive_body_steps_successor + S (fs_s_dst_flat_prefixpositive_body_steps) = S ((S (S fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_successor. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive) + (fs_s_dst_flat_prefixpositive_body_steps))) /\ fs_s_dst_flat_prefixpositive_body_steps = fs_r_dst_flat_prefixpositive_body_steps + fs_a_dst_flat_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_prefixnegative fs_v_dst_flat_prefixnegative. ((((exists fs_h_dst_flat_prefixnegative_body_start. fs_h_dst_flat_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_start. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_start * S ((S (0)) * fs_v_dst_flat_prefixnegative) + (0))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_terminal. fs_h_dst_flat_prefixnegative_body_terminal + S (dst_negative_sum_flat_prefix) = S ((S (m*n)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_terminal. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_terminal * S ((S (m*n)) * fs_v_dst_flat_prefixnegative) + (dst_negative_sum_flat_prefix))) /\ forall fs_i_dst_flat_prefixnegative_body_steps. (exists fs_lt_dst_flat_prefixnegative_body_steps_bound. fs_lt_dst_flat_prefixnegative_body_steps_bound + S fs_i_dst_flat_prefixnegative_body_steps = m*n) -> exists fs_a_dst_flat_prefixnegative_body_steps fs_r_dst_flat_prefixnegative_body_steps fs_s_dst_flat_prefixnegative_body_steps. ((((exists fs_h_dst_flat_prefixnegative_body_steps_summand. fs_h_dst_flat_prefixnegative_body_steps_summand + S (fs_a_dst_flat_prefixnegative_body_steps) = S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * dst_negative_scale_flat_prefix)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_summand. dst_negative_code_flat_prefix = fs_q_dst_flat_prefixnegative_body_steps_summand * S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * dst_negative_scale_flat_prefix) + (fs_a_dst_flat_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_steps_partial. fs_h_dst_flat_prefixnegative_body_steps_partial + S (fs_r_dst_flat_prefixnegative_body_steps) = S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_partial. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_steps_partial * S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative) + (fs_r_dst_flat_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_steps_successor. fs_h_dst_flat_prefixnegative_body_steps_successor + S (fs_s_dst_flat_prefixnegative_body_steps) = S ((S (S fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_successor. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative) + (fs_s_dst_flat_prefixnegative_body_steps))) /\ fs_s_dst_flat_prefixnegative_body_steps = fs_r_dst_flat_prefixnegative_body_steps + fs_a_dst_flat_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_prefixresult ge_balance_negative_flat_prefixresult. (((((z) = 2 * (ge_balance_positive_flat_prefixresult) /\ (ge_balance_negative_flat_prefixresult) = 0) \/ exists ge_signed_half_flat_prefixresultdecode. (((z) = 2 * ge_signed_half_flat_prefixresultdecode + 1 /\ (ge_balance_positive_flat_prefixresult) = 0) /\ (ge_balance_negative_flat_prefixresult) = S ge_signed_half_flat_prefixresultdecode))) /\ ((dst_positive_sum_flat_prefix) + ge_balance_negative_flat_prefixresult = (dst_negative_sum_flat_prefix) + ge_balance_positive_flat_prefixresult))))))))) -> (exists srt_rows_flat_rectangle. ((((exists dst_positive_code_flat_rectanglerowssource_table dst_positive_scale_flat_rectanglerowssource_table dst_negative_code_flat_rectanglerowssource_table dst_negative_scale_flat_rectanglerowssource_table. (((F) = (((((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) * S ((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) + ((dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))) * S ((((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) * S ((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) + ((dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))) + ((((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))))) /\ (forall dst_index_flat_rectanglerowssource_table. (exists pvs_le_gap_flat_rectanglerowssource_tabledomain. pvs_le_gap_flat_rectanglerowssource_tabledomain + (dst_index_flat_rectanglerowssource_table) = (0)) -> exists dst_positive_flat_rectanglerowssource_table dst_negative_flat_rectanglerowssource_table dst_value_flat_rectanglerowssource_table. ((((exists ff_h_pvs_flat_rectanglerowssource_tableentrypositive. ff_h_pvs_flat_rectanglerowssource_tableentrypositive + S (dst_positive_flat_rectanglerowssource_table) = S ((S (dst_index_flat_rectanglerowssource_table)) * dst_positive_scale_flat_rectanglerowssource_table)) /\ exists ff_q_pvs_flat_rectanglerowssource_tableentrypositive. dst_positive_code_flat_rectanglerowssource_table = ff_q_pvs_flat_rectanglerowssource_tableentrypositive * S ((S (dst_index_flat_rectanglerowssource_table)) * dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_flat_rectanglerowssource_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowssource_tableentrynegative. ff_h_pvs_flat_rectanglerowssource_tableentrynegative + S (dst_negative_flat_rectanglerowssource_table) = S ((S (dst_index_flat_rectanglerowssource_table)) * dst_negative_scale_flat_rectanglerowssource_table)) /\ exists ff_q_pvs_flat_rectanglerowssource_tableentrynegative. dst_negative_code_flat_rectanglerowssource_table = ff_q_pvs_flat_rectanglerowssource_tableentrynegative * S ((S (dst_index_flat_rectanglerowssource_table)) * dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_flat_rectanglerowssource_table))) /\ (exists ge_balance_positive_flat_rectanglerowssource_tableentryvalue ge_balance_negative_flat_rectanglerowssource_tableentryvalue. (((((dst_value_flat_rectanglerowssource_table) = 2 * (ge_balance_positive_flat_rectanglerowssource_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowssource_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode. (((dst_value_flat_rectanglerowssource_table) = 2 * ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowssource_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowssource_tableentryvalue) = S ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowssource_table) + ge_balance_negative_flat_rectanglerowssource_tableentryvalue = (dst_negative_flat_rectanglerowssource_table) + ge_balance_positive_flat_rectanglerowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flat_rectanglerowsrow_table dst_positive_scale_flat_rectanglerowsrow_table dst_negative_code_flat_rectanglerowsrow_table dst_negative_scale_flat_rectanglerowsrow_table. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) * S ((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) + ((dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))) * S ((((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) * S ((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) + ((dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))) + ((((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))))) /\ (forall dst_index_flat_rectanglerowsrow_table. (exists pvs_le_gap_flat_rectanglerowsrow_tabledomain. pvs_le_gap_flat_rectanglerowsrow_tabledomain + (dst_index_flat_rectanglerowsrow_table) = (m)) -> exists dst_positive_flat_rectanglerowsrow_table dst_negative_flat_rectanglerowsrow_table dst_value_flat_rectanglerowsrow_table. ((((exists ff_h_pvs_flat_rectanglerowsrow_tableentrypositive. ff_h_pvs_flat_rectanglerowsrow_tableentrypositive + S (dst_positive_flat_rectanglerowsrow_table) = S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_positive_scale_flat_rectanglerowsrow_table)) /\ exists ff_q_pvs_flat_rectanglerowsrow_tableentrypositive. dst_positive_code_flat_rectanglerowsrow_table = ff_q_pvs_flat_rectanglerowsrow_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_flat_rectanglerowsrow_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrow_tableentrynegative. ff_h_pvs_flat_rectanglerowsrow_tableentrynegative + S (dst_negative_flat_rectanglerowsrow_table) = S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_negative_scale_flat_rectanglerowsrow_table)) /\ exists ff_q_pvs_flat_rectanglerowsrow_tableentrynegative. dst_negative_code_flat_rectanglerowsrow_table = ff_q_pvs_flat_rectanglerowsrow_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_flat_rectanglerowsrow_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrow_tableentryvalue ge_balance_negative_flat_rectanglerowsrow_tableentryvalue. (((((dst_value_flat_rectanglerowsrow_table) = 2 * (ge_balance_positive_flat_rectanglerowsrow_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrow_table) = 2 * ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrow_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrow_table) + ge_balance_negative_flat_rectanglerowsrow_tableentryvalue = (dst_negative_flat_rectanglerowsrow_table) + ge_balance_positive_flat_rectanglerowsrow_tableentryvalue))))))))) /\ (forall srt_index_flat_rectanglerows. (exists pvs_gap_flat_rectanglerowsbound. pvs_gap_flat_rectanglerowsbound + S (srt_index_flat_rectanglerows) = (m)) -> exists srt_value_flat_rectanglerows. (((exists dst_positive_code_flat_rectanglerowsrowentry dst_positive_scale_flat_rectanglerowsrowentry dst_negative_code_flat_rectanglerowsrowentry dst_negative_scale_flat_rectanglerowsrowentry dst_positive_flat_rectanglerowsrowentry dst_negative_flat_rectanglerowsrowentry. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) * S ((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) + ((dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))) * S ((((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) * S ((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) + ((dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))) + ((((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowentrypositive. ff_h_pvs_flat_rectanglerowsrowentrypositive + S (dst_positive_flat_rectanglerowsrowentry) = S ((S (srt_index_flat_rectanglerows)) * dst_positive_scale_flat_rectanglerowsrowentry)) /\ exists ff_q_pvs_flat_rectanglerowsrowentrypositive. dst_positive_code_flat_rectanglerowsrowentry = ff_q_pvs_flat_rectanglerowsrowentrypositive * S ((S (srt_index_flat_rectanglerows)) * dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_flat_rectanglerowsrowentry))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowentrynegative. ff_h_pvs_flat_rectanglerowsrowentrynegative + S (dst_negative_flat_rectanglerowsrowentry) = S ((S (srt_index_flat_rectanglerows)) * dst_negative_scale_flat_rectanglerowsrowentry)) /\ exists ff_q_pvs_flat_rectanglerowsrowentrynegative. dst_negative_code_flat_rectanglerowsrowentry = ff_q_pvs_flat_rectanglerowsrowentrynegative * S ((S (srt_index_flat_rectanglerows)) * dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_flat_rectanglerowsrowentry))) /\ (exists ge_balance_positive_flat_rectanglerowsrowentryvalue ge_balance_negative_flat_rectanglerowsrowentryvalue. (((((srt_value_flat_rectanglerows) = 2 * (ge_balance_positive_flat_rectanglerowsrowentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowentryvaluedecode. (((srt_value_flat_rectanglerows) = 2 * ge_signed_half_flat_rectanglerowsrowentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowentryvalue) = S ge_signed_half_flat_rectanglerowsrowentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowentry) + ge_balance_negative_flat_rectanglerowsrowentryvalue = (dst_negative_flat_rectanglerowsrowentry) + ge_balance_positive_flat_rectanglerowsrowentryvalue))))))))) /\ (exists srs_slice_flat_rectanglerowsrowrow_sum. ((((exists dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_flat_rectanglerowsrowrow_sumslicesource_table. (exists pvs_le_gap_flat_rectanglerowsrowrow_sumslicesource_tabledomain. pvs_le_gap_flat_rectanglerowsrowrow_sumslicesource_tabledomain + (dst_index_flat_rectanglerowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_flat_rectanglerowsrowrow_sumslicesource_table dst_value_flat_rectanglerowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_flat_rectanglerowsrowrow_sumslicesource_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table = ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_flat_rectanglerowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table = ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_flat_rectanglerowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrowrow_sumslicesource_table) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumslicesource_table) + ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue = (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table) + ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_flat_rectanglerowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_flat_rectanglerowsrowrow_sumsliceoutput_tabledomain + (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_flat_rectanglerowsrowrow_sumslice. (exists pvs_gap_flat_rectanglerowsrowrow_sumslicebound. pvs_gap_flat_rectanglerowsrowrow_sumslicebound + S (srs_index_flat_rectanglerowsrowrow_sumslice) = (n)) -> exists srs_value_flat_rectanglerowsrowrow_sumslice. (((exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue. (((((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue. (((((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_flat_rectanglerowsrowrow_sumsum dst_positive_scale_flat_rectanglerowsrowrow_sumsum dst_negative_code_flat_rectanglerowsrowrow_sumsum dst_negative_scale_flat_rectanglerowsrowrow_sumsum dst_positive_sum_flat_rectanglerowsrowrow_sumsum dst_negative_sum_flat_rectanglerowsrowrow_sumsum. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_flat_rectanglerowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (dst_positive_sum_flat_rectanglerowsrowrow_sumsum))) /\ forall fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_flat_rectanglerowsrowrow_sumsum = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps = fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps + fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_flat_rectanglerowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (dst_negative_sum_flat_rectanglerowsrowrow_sumsum))) /\ forall fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_flat_rectanglerowsrowrow_sumsum = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps = fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps + fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult. (((((srt_value_flat_rectanglerows) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode. (((srt_value_flat_rectanglerows) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult) = S ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_flat_rectanglerowsrowrow_sumsum) + ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult = (dst_negative_sum_flat_rectanglerowsrowrow_sumsum) + ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_flat_rectangletotal dst_positive_scale_flat_rectangletotal dst_negative_code_flat_rectangletotal dst_negative_scale_flat_rectangletotal dst_positive_sum_flat_rectangletotal dst_negative_sum_flat_rectangletotal. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) * S ((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) + ((dst_positive_scale_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))) * S ((((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) * S ((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) + ((dst_positive_scale_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))) + ((((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))))) /\ (((exists fs_u_dst_flat_rectangletotalpositive fs_v_dst_flat_rectangletotalpositive. ((((exists fs_h_dst_flat_rectangletotalpositive_body_start. fs_h_dst_flat_rectangletotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_start. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_start * S ((S (0)) * fs_v_dst_flat_rectangletotalpositive) + (0))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_terminal. fs_h_dst_flat_rectangletotalpositive_body_terminal + S (dst_positive_sum_flat_rectangletotal) = S ((S (m)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_terminal. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_terminal * S ((S (m)) * fs_v_dst_flat_rectangletotalpositive) + (dst_positive_sum_flat_rectangletotal))) /\ forall fs_i_dst_flat_rectangletotalpositive_body_steps. (exists fs_lt_dst_flat_rectangletotalpositive_body_steps_bound. fs_lt_dst_flat_rectangletotalpositive_body_steps_bound + S fs_i_dst_flat_rectangletotalpositive_body_steps = m) -> exists fs_a_dst_flat_rectangletotalpositive_body_steps fs_r_dst_flat_rectangletotalpositive_body_steps fs_s_dst_flat_rectangletotalpositive_body_steps. ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_summand. fs_h_dst_flat_rectangletotalpositive_body_steps_summand + S (fs_a_dst_flat_rectangletotalpositive_body_steps) = S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * dst_positive_scale_flat_rectangletotal)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_summand. dst_positive_code_flat_rectangletotal = fs_q_dst_flat_rectangletotalpositive_body_steps_summand * S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * dst_positive_scale_flat_rectangletotal) + (fs_a_dst_flat_rectangletotalpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_partial. fs_h_dst_flat_rectangletotalpositive_body_steps_partial + S (fs_r_dst_flat_rectangletotalpositive_body_steps) = S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_partial. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_steps_partial * S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive) + (fs_r_dst_flat_rectangletotalpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_successor. fs_h_dst_flat_rectangletotalpositive_body_steps_successor + S (fs_s_dst_flat_rectangletotalpositive_body_steps) = S ((S (S fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_successor. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_steps_successor * S ((S (S fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive) + (fs_s_dst_flat_rectangletotalpositive_body_steps))) /\ fs_s_dst_flat_rectangletotalpositive_body_steps = fs_r_dst_flat_rectangletotalpositive_body_steps + fs_a_dst_flat_rectangletotalpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_rectangletotalnegative fs_v_dst_flat_rectangletotalnegative. ((((exists fs_h_dst_flat_rectangletotalnegative_body_start. fs_h_dst_flat_rectangletotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_start. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_start * S ((S (0)) * fs_v_dst_flat_rectangletotalnegative) + (0))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_terminal. fs_h_dst_flat_rectangletotalnegative_body_terminal + S (dst_negative_sum_flat_rectangletotal) = S ((S (m)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_terminal. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_terminal * S ((S (m)) * fs_v_dst_flat_rectangletotalnegative) + (dst_negative_sum_flat_rectangletotal))) /\ forall fs_i_dst_flat_rectangletotalnegative_body_steps. (exists fs_lt_dst_flat_rectangletotalnegative_body_steps_bound. fs_lt_dst_flat_rectangletotalnegative_body_steps_bound + S fs_i_dst_flat_rectangletotalnegative_body_steps = m) -> exists fs_a_dst_flat_rectangletotalnegative_body_steps fs_r_dst_flat_rectangletotalnegative_body_steps fs_s_dst_flat_rectangletotalnegative_body_steps. ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_summand. fs_h_dst_flat_rectangletotalnegative_body_steps_summand + S (fs_a_dst_flat_rectangletotalnegative_body_steps) = S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * dst_negative_scale_flat_rectangletotal)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_summand. dst_negative_code_flat_rectangletotal = fs_q_dst_flat_rectangletotalnegative_body_steps_summand * S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * dst_negative_scale_flat_rectangletotal) + (fs_a_dst_flat_rectangletotalnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_partial. fs_h_dst_flat_rectangletotalnegative_body_steps_partial + S (fs_r_dst_flat_rectangletotalnegative_body_steps) = S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_partial. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_steps_partial * S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative) + (fs_r_dst_flat_rectangletotalnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_successor. fs_h_dst_flat_rectangletotalnegative_body_steps_successor + S (fs_s_dst_flat_rectangletotalnegative_body_steps) = S ((S (S fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_successor. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_steps_successor * S ((S (S fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative) + (fs_s_dst_flat_rectangletotalnegative_body_steps))) /\ fs_s_dst_flat_rectangletotalnegative_body_steps = fs_r_dst_flat_rectangletotalnegative_body_steps + fs_a_dst_flat_rectangletotalnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_rectangletotalresult ge_balance_negative_flat_rectangletotalresult. (((((z) = 2 * (ge_balance_positive_flat_rectangletotalresult) /\ (ge_balance_negative_flat_rectangletotalresult) = 0) \/ exists ge_signed_half_flat_rectangletotalresultdecode. (((z) = 2 * ge_signed_half_flat_rectangletotalresultdecode + 1 /\ (ge_balance_positive_flat_rectangletotalresult) = 0) /\ (ge_balance_negative_flat_rectangletotalresult) = S ge_signed_half_flat_rectangletotalresultdecode))) /\ ((dst_positive_sum_flat_rectangletotal) + ge_balance_negative_flat_rectangletotalresult = (dst_negative_sum_flat_rectangletotal) + ge_balance_positive_flat_rectangletotalresult)))))))))))) /\ ((exists srt_rows_flat_rectangle. ((((exists dst_positive_code_flat_rectanglerowssource_table dst_positive_scale_flat_rectanglerowssource_table dst_negative_code_flat_rectanglerowssource_table dst_negative_scale_flat_rectanglerowssource_table. (((F) = (((((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) * S ((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) + ((dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))) * S ((((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) * S ((dst_positive_code_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table)) + ((dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))) + ((((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table))) + (((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) * S ((dst_negative_code_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)) + ((dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_scale_flat_rectanglerowssource_table)))))) /\ (forall dst_index_flat_rectanglerowssource_table. (exists pvs_le_gap_flat_rectanglerowssource_tabledomain. pvs_le_gap_flat_rectanglerowssource_tabledomain + (dst_index_flat_rectanglerowssource_table) = (0)) -> exists dst_positive_flat_rectanglerowssource_table dst_negative_flat_rectanglerowssource_table dst_value_flat_rectanglerowssource_table. ((((exists ff_h_pvs_flat_rectanglerowssource_tableentrypositive. ff_h_pvs_flat_rectanglerowssource_tableentrypositive + S (dst_positive_flat_rectanglerowssource_table) = S ((S (dst_index_flat_rectanglerowssource_table)) * dst_positive_scale_flat_rectanglerowssource_table)) /\ exists ff_q_pvs_flat_rectanglerowssource_tableentrypositive. dst_positive_code_flat_rectanglerowssource_table = ff_q_pvs_flat_rectanglerowssource_tableentrypositive * S ((S (dst_index_flat_rectanglerowssource_table)) * dst_positive_scale_flat_rectanglerowssource_table) + (dst_positive_flat_rectanglerowssource_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowssource_tableentrynegative. ff_h_pvs_flat_rectanglerowssource_tableentrynegative + S (dst_negative_flat_rectanglerowssource_table) = S ((S (dst_index_flat_rectanglerowssource_table)) * dst_negative_scale_flat_rectanglerowssource_table)) /\ exists ff_q_pvs_flat_rectanglerowssource_tableentrynegative. dst_negative_code_flat_rectanglerowssource_table = ff_q_pvs_flat_rectanglerowssource_tableentrynegative * S ((S (dst_index_flat_rectanglerowssource_table)) * dst_negative_scale_flat_rectanglerowssource_table) + (dst_negative_flat_rectanglerowssource_table))) /\ (exists ge_balance_positive_flat_rectanglerowssource_tableentryvalue ge_balance_negative_flat_rectanglerowssource_tableentryvalue. (((((dst_value_flat_rectanglerowssource_table) = 2 * (ge_balance_positive_flat_rectanglerowssource_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowssource_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode. (((dst_value_flat_rectanglerowssource_table) = 2 * ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowssource_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowssource_tableentryvalue) = S ge_signed_half_flat_rectanglerowssource_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowssource_table) + ge_balance_negative_flat_rectanglerowssource_tableentryvalue = (dst_negative_flat_rectanglerowssource_table) + ge_balance_positive_flat_rectanglerowssource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flat_rectanglerowsrow_table dst_positive_scale_flat_rectanglerowsrow_table dst_negative_code_flat_rectanglerowsrow_table dst_negative_scale_flat_rectanglerowsrow_table. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) * S ((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) + ((dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))) * S ((((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) * S ((dst_positive_code_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table)) + ((dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))) + ((((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table))) + (((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) * S ((dst_negative_code_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)) + ((dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_scale_flat_rectanglerowsrow_table)))))) /\ (forall dst_index_flat_rectanglerowsrow_table. (exists pvs_le_gap_flat_rectanglerowsrow_tabledomain. pvs_le_gap_flat_rectanglerowsrow_tabledomain + (dst_index_flat_rectanglerowsrow_table) = (m)) -> exists dst_positive_flat_rectanglerowsrow_table dst_negative_flat_rectanglerowsrow_table dst_value_flat_rectanglerowsrow_table. ((((exists ff_h_pvs_flat_rectanglerowsrow_tableentrypositive. ff_h_pvs_flat_rectanglerowsrow_tableentrypositive + S (dst_positive_flat_rectanglerowsrow_table) = S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_positive_scale_flat_rectanglerowsrow_table)) /\ exists ff_q_pvs_flat_rectanglerowsrow_tableentrypositive. dst_positive_code_flat_rectanglerowsrow_table = ff_q_pvs_flat_rectanglerowsrow_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_positive_scale_flat_rectanglerowsrow_table) + (dst_positive_flat_rectanglerowsrow_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrow_tableentrynegative. ff_h_pvs_flat_rectanglerowsrow_tableentrynegative + S (dst_negative_flat_rectanglerowsrow_table) = S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_negative_scale_flat_rectanglerowsrow_table)) /\ exists ff_q_pvs_flat_rectanglerowsrow_tableentrynegative. dst_negative_code_flat_rectanglerowsrow_table = ff_q_pvs_flat_rectanglerowsrow_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrow_table)) * dst_negative_scale_flat_rectanglerowsrow_table) + (dst_negative_flat_rectanglerowsrow_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrow_tableentryvalue ge_balance_negative_flat_rectanglerowsrow_tableentryvalue. (((((dst_value_flat_rectanglerowsrow_table) = 2 * (ge_balance_positive_flat_rectanglerowsrow_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrow_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrow_table) = 2 * ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrow_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrow_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrow_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrow_table) + ge_balance_negative_flat_rectanglerowsrow_tableentryvalue = (dst_negative_flat_rectanglerowsrow_table) + ge_balance_positive_flat_rectanglerowsrow_tableentryvalue))))))))) /\ (forall srt_index_flat_rectanglerows. (exists pvs_gap_flat_rectanglerowsbound. pvs_gap_flat_rectanglerowsbound + S (srt_index_flat_rectanglerows) = (m)) -> exists srt_value_flat_rectanglerows. (((exists dst_positive_code_flat_rectanglerowsrowentry dst_positive_scale_flat_rectanglerowsrowentry dst_negative_code_flat_rectanglerowsrowentry dst_negative_scale_flat_rectanglerowsrowentry dst_positive_flat_rectanglerowsrowentry dst_negative_flat_rectanglerowsrowentry. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) * S ((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) + ((dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))) * S ((((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) * S ((dst_positive_code_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry)) + ((dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))) + ((((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry))) + (((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) * S ((dst_negative_code_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)) + ((dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_scale_flat_rectanglerowsrowentry)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowentrypositive. ff_h_pvs_flat_rectanglerowsrowentrypositive + S (dst_positive_flat_rectanglerowsrowentry) = S ((S (srt_index_flat_rectanglerows)) * dst_positive_scale_flat_rectanglerowsrowentry)) /\ exists ff_q_pvs_flat_rectanglerowsrowentrypositive. dst_positive_code_flat_rectanglerowsrowentry = ff_q_pvs_flat_rectanglerowsrowentrypositive * S ((S (srt_index_flat_rectanglerows)) * dst_positive_scale_flat_rectanglerowsrowentry) + (dst_positive_flat_rectanglerowsrowentry))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowentrynegative. ff_h_pvs_flat_rectanglerowsrowentrynegative + S (dst_negative_flat_rectanglerowsrowentry) = S ((S (srt_index_flat_rectanglerows)) * dst_negative_scale_flat_rectanglerowsrowentry)) /\ exists ff_q_pvs_flat_rectanglerowsrowentrynegative. dst_negative_code_flat_rectanglerowsrowentry = ff_q_pvs_flat_rectanglerowsrowentrynegative * S ((S (srt_index_flat_rectanglerows)) * dst_negative_scale_flat_rectanglerowsrowentry) + (dst_negative_flat_rectanglerowsrowentry))) /\ (exists ge_balance_positive_flat_rectanglerowsrowentryvalue ge_balance_negative_flat_rectanglerowsrowentryvalue. (((((srt_value_flat_rectanglerows) = 2 * (ge_balance_positive_flat_rectanglerowsrowentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowentryvaluedecode. (((srt_value_flat_rectanglerows) = 2 * ge_signed_half_flat_rectanglerowsrowentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowentryvalue) = S ge_signed_half_flat_rectanglerowsrowentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowentry) + ge_balance_negative_flat_rectanglerowsrowentryvalue = (dst_negative_flat_rectanglerowsrowentry) + ge_balance_positive_flat_rectanglerowsrowentryvalue))))))))) /\ (exists srs_slice_flat_rectanglerowsrowrow_sum. ((((exists dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table. (((F) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)))))) /\ (forall dst_index_flat_rectanglerowsrowrow_sumslicesource_table. (exists pvs_le_gap_flat_rectanglerowsrowrow_sumslicesource_tabledomain. pvs_le_gap_flat_rectanglerowsrowrow_sumslicesource_tabledomain + (dst_index_flat_rectanglerowsrowrow_sumslicesource_table) = (0)) -> exists dst_positive_flat_rectanglerowsrowrow_sumslicesource_table dst_negative_flat_rectanglerowsrowrow_sumslicesource_table dst_value_flat_rectanglerowsrowrow_sumslicesource_table. ((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive. ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive + S (dst_positive_flat_rectanglerowsrowrow_sumslicesource_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive. dst_positive_code_flat_rectanglerowsrowrow_sumslicesource_table = ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_positive_flat_rectanglerowsrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative. ff_h_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative + S (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative. dst_negative_code_flat_rectanglerowsrowrow_sumslicesource_table = ff_q_pvs_flat_rectanglerowsrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrowrow_sumslicesource_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumslicesource_table) + (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue. (((((dst_value_flat_rectanglerowsrowrow_sumslicesource_table) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrowrow_sumslicesource_table) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumslicesource_table) + ge_balance_negative_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue = (dst_negative_flat_rectanglerowsrowrow_sumslicesource_table) + ge_balance_positive_flat_rectanglerowsrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table. (exists pvs_le_gap_flat_rectanglerowsrowrow_sumsliceoutput_tabledomain. pvs_le_gap_flat_rectanglerowsrowrow_sumsliceoutput_tabledomain + (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table) = (n)) -> exists dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceoutput_table = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table) = S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceoutput_table = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_flat_rectanglerowsrowrow_sumsliceoutput_table)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceoutput_table) + (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_flat_rectanglerowsrowrow_sumsliceoutput_table) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceoutput_table) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceoutput_table) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_flat_rectanglerowsrowrow_sumslice. (exists pvs_gap_flat_rectanglerowsrowrow_sumslicebound. pvs_gap_flat_rectanglerowsrowrow_sumslicebound + S (srs_index_flat_rectanglerowsrowrow_sumslice) = (n)) -> exists srs_value_flat_rectanglerowsrowrow_sumslice. (((exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource. (((F) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceentrysource = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcepositive * S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource) = S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceentrysource = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentrysourcenegative * S ((S (((((0) + ((n) * (srt_index_flat_rectanglerows)))) + ((1) * (srs_index_flat_rectanglerowsrowrow_sumslice))))) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentrysource) + (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue. (((((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode. (((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceentrysource) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentrysourcevalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceentrysource) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive + S (dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive. dst_positive_code_flat_rectanglerowsrowrow_sumsliceentryoutput = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputpositive * S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative. ff_h_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative + S (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput) = S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative. dst_negative_code_flat_rectanglerowsrowrow_sumsliceentryoutput = ff_q_pvs_flat_rectanglerowsrowrow_sumsliceentryoutputnegative * S ((S (srs_index_flat_rectanglerowsrowrow_sumslice)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsliceentryoutput) + (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue. (((((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode. (((srs_value_flat_rectanglerowsrowrow_sumslice) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue) = S ge_signed_half_flat_rectanglerowsrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_flat_rectanglerowsrowrow_sumsliceentryoutput) + ge_balance_negative_flat_rectanglerowsrowrow_sumsliceentryoutputvalue = (dst_negative_flat_rectanglerowsrowrow_sumsliceentryoutput) + ge_balance_positive_flat_rectanglerowsrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_flat_rectanglerowsrowrow_sumsum dst_positive_scale_flat_rectanglerowsrowrow_sumsum dst_negative_code_flat_rectanglerowsrowrow_sumsum dst_negative_scale_flat_rectanglerowsrowrow_sumsum dst_positive_sum_flat_rectanglerowsrowrow_sumsum dst_negative_sum_flat_rectanglerowsrowrow_sumsum. (((srs_slice_flat_rectanglerowsrowrow_sum) = (((((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))) * S ((((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_positive_code_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (dst_positive_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))) + ((((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum))) + (((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) * S ((dst_negative_code_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) + ((dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (dst_negative_scale_flat_rectanglerowsrowrow_sumsum)))))) /\ (((exists fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_flat_rectanglerowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_terminal * S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (dst_positive_sum_flat_rectanglerowsrowrow_sumsum))) /\ forall fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps = n) -> exists fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsum)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand. dst_positive_code_flat_rectanglerowsrowrow_sumsum = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * dst_positive_scale_flat_rectanglerowsrowrow_sumsum) + (fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor. fs_h_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor. fs_u_dst_flat_rectanglerowsrowrow_sumsumpositive = fs_q_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumpositive) + (fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps = fs_r_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps + fs_a_dst_flat_rectanglerowsrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_flat_rectanglerowsrowrow_sumsum) = S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_terminal * S ((S (n)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (dst_negative_sum_flat_rectanglerowsrowrow_sumsum))) /\ forall fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps = n) -> exists fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsum)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand. dst_negative_code_flat_rectanglerowsrowrow_sumsum = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * dst_negative_scale_flat_rectanglerowsrowrow_sumsum) + (fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor. fs_h_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative)) /\ exists fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor. fs_u_dst_flat_rectanglerowsrowrow_sumsumnegative = fs_q_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)) * fs_v_dst_flat_rectanglerowsrowrow_sumsumnegative) + (fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps = fs_r_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps + fs_a_dst_flat_rectanglerowsrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult. (((((srt_value_flat_rectanglerows) = 2 * (ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult) = 0) \/ exists ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode. (((srt_value_flat_rectanglerows) = 2 * ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult) = 0) /\ (ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult) = S ge_signed_half_flat_rectanglerowsrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_flat_rectanglerowsrowrow_sumsum) + ge_balance_negative_flat_rectanglerowsrowrow_sumsumresult = (dst_negative_sum_flat_rectanglerowsrowrow_sumsum) + ge_balance_positive_flat_rectanglerowsrowrow_sumsumresult)))))))))))))))))) /\ (exists dst_positive_code_flat_rectangletotal dst_positive_scale_flat_rectangletotal dst_negative_code_flat_rectangletotal dst_negative_scale_flat_rectangletotal dst_positive_sum_flat_rectangletotal dst_negative_sum_flat_rectangletotal. (((srt_rows_flat_rectangle) = (((((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) * S ((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) + ((dst_positive_scale_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))) * S ((((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) * S ((dst_positive_code_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal)) + ((dst_positive_scale_flat_rectangletotal) + (dst_positive_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))) + ((((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal))) + (((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) * S ((dst_negative_code_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)) + ((dst_negative_scale_flat_rectangletotal) + (dst_negative_scale_flat_rectangletotal)))))) /\ (((exists fs_u_dst_flat_rectangletotalpositive fs_v_dst_flat_rectangletotalpositive. ((((exists fs_h_dst_flat_rectangletotalpositive_body_start. fs_h_dst_flat_rectangletotalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_start. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_start * S ((S (0)) * fs_v_dst_flat_rectangletotalpositive) + (0))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_terminal. fs_h_dst_flat_rectangletotalpositive_body_terminal + S (dst_positive_sum_flat_rectangletotal) = S ((S (m)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_terminal. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_terminal * S ((S (m)) * fs_v_dst_flat_rectangletotalpositive) + (dst_positive_sum_flat_rectangletotal))) /\ forall fs_i_dst_flat_rectangletotalpositive_body_steps. (exists fs_lt_dst_flat_rectangletotalpositive_body_steps_bound. fs_lt_dst_flat_rectangletotalpositive_body_steps_bound + S fs_i_dst_flat_rectangletotalpositive_body_steps = m) -> exists fs_a_dst_flat_rectangletotalpositive_body_steps fs_r_dst_flat_rectangletotalpositive_body_steps fs_s_dst_flat_rectangletotalpositive_body_steps. ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_summand. fs_h_dst_flat_rectangletotalpositive_body_steps_summand + S (fs_a_dst_flat_rectangletotalpositive_body_steps) = S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * dst_positive_scale_flat_rectangletotal)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_summand. dst_positive_code_flat_rectangletotal = fs_q_dst_flat_rectangletotalpositive_body_steps_summand * S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * dst_positive_scale_flat_rectangletotal) + (fs_a_dst_flat_rectangletotalpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_partial. fs_h_dst_flat_rectangletotalpositive_body_steps_partial + S (fs_r_dst_flat_rectangletotalpositive_body_steps) = S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_partial. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_steps_partial * S ((S (fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive) + (fs_r_dst_flat_rectangletotalpositive_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalpositive_body_steps_successor. fs_h_dst_flat_rectangletotalpositive_body_steps_successor + S (fs_s_dst_flat_rectangletotalpositive_body_steps) = S ((S (S fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive)) /\ exists fs_q_dst_flat_rectangletotalpositive_body_steps_successor. fs_u_dst_flat_rectangletotalpositive = fs_q_dst_flat_rectangletotalpositive_body_steps_successor * S ((S (S fs_i_dst_flat_rectangletotalpositive_body_steps)) * fs_v_dst_flat_rectangletotalpositive) + (fs_s_dst_flat_rectangletotalpositive_body_steps))) /\ fs_s_dst_flat_rectangletotalpositive_body_steps = fs_r_dst_flat_rectangletotalpositive_body_steps + fs_a_dst_flat_rectangletotalpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_rectangletotalnegative fs_v_dst_flat_rectangletotalnegative. ((((exists fs_h_dst_flat_rectangletotalnegative_body_start. fs_h_dst_flat_rectangletotalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_start. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_start * S ((S (0)) * fs_v_dst_flat_rectangletotalnegative) + (0))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_terminal. fs_h_dst_flat_rectangletotalnegative_body_terminal + S (dst_negative_sum_flat_rectangletotal) = S ((S (m)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_terminal. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_terminal * S ((S (m)) * fs_v_dst_flat_rectangletotalnegative) + (dst_negative_sum_flat_rectangletotal))) /\ forall fs_i_dst_flat_rectangletotalnegative_body_steps. (exists fs_lt_dst_flat_rectangletotalnegative_body_steps_bound. fs_lt_dst_flat_rectangletotalnegative_body_steps_bound + S fs_i_dst_flat_rectangletotalnegative_body_steps = m) -> exists fs_a_dst_flat_rectangletotalnegative_body_steps fs_r_dst_flat_rectangletotalnegative_body_steps fs_s_dst_flat_rectangletotalnegative_body_steps. ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_summand. fs_h_dst_flat_rectangletotalnegative_body_steps_summand + S (fs_a_dst_flat_rectangletotalnegative_body_steps) = S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * dst_negative_scale_flat_rectangletotal)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_summand. dst_negative_code_flat_rectangletotal = fs_q_dst_flat_rectangletotalnegative_body_steps_summand * S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * dst_negative_scale_flat_rectangletotal) + (fs_a_dst_flat_rectangletotalnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_partial. fs_h_dst_flat_rectangletotalnegative_body_steps_partial + S (fs_r_dst_flat_rectangletotalnegative_body_steps) = S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_partial. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_steps_partial * S ((S (fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative) + (fs_r_dst_flat_rectangletotalnegative_body_steps))) /\ ((((exists fs_h_dst_flat_rectangletotalnegative_body_steps_successor. fs_h_dst_flat_rectangletotalnegative_body_steps_successor + S (fs_s_dst_flat_rectangletotalnegative_body_steps) = S ((S (S fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative)) /\ exists fs_q_dst_flat_rectangletotalnegative_body_steps_successor. fs_u_dst_flat_rectangletotalnegative = fs_q_dst_flat_rectangletotalnegative_body_steps_successor * S ((S (S fs_i_dst_flat_rectangletotalnegative_body_steps)) * fs_v_dst_flat_rectangletotalnegative) + (fs_s_dst_flat_rectangletotalnegative_body_steps))) /\ fs_s_dst_flat_rectangletotalnegative_body_steps = fs_r_dst_flat_rectangletotalnegative_body_steps + fs_a_dst_flat_rectangletotalnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_rectangletotalresult ge_balance_negative_flat_rectangletotalresult. (((((z) = 2 * (ge_balance_positive_flat_rectangletotalresult) /\ (ge_balance_negative_flat_rectangletotalresult) = 0) \/ exists ge_signed_half_flat_rectangletotalresultdecode. (((z) = 2 * ge_signed_half_flat_rectangletotalresultdecode + 1 /\ (ge_balance_positive_flat_rectangletotalresult) = 0) /\ (ge_balance_negative_flat_rectangletotalresult) = S ge_signed_half_flat_rectangletotalresultdecode))) /\ ((dst_positive_sum_flat_rectangletotal) + ge_balance_negative_flat_rectangletotalresult = (dst_negative_sum_flat_rectangletotal) + ge_balance_positive_flat_rectangletotalresult))))))))))) -> (exists dst_positive_code_flat_prefix dst_positive_scale_flat_prefix dst_negative_code_flat_prefix dst_negative_scale_flat_prefix dst_positive_sum_flat_prefix dst_negative_sum_flat_prefix. (((F) = (((((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) * S ((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) + ((dst_positive_scale_flat_prefix) + (dst_positive_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))) * S ((((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) * S ((dst_positive_code_flat_prefix) + (dst_positive_scale_flat_prefix)) + ((dst_positive_scale_flat_prefix) + (dst_positive_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))) + ((((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix))) + (((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) * S ((dst_negative_code_flat_prefix) + (dst_negative_scale_flat_prefix)) + ((dst_negative_scale_flat_prefix) + (dst_negative_scale_flat_prefix)))))) /\ (((exists fs_u_dst_flat_prefixpositive fs_v_dst_flat_prefixpositive. ((((exists fs_h_dst_flat_prefixpositive_body_start. fs_h_dst_flat_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_start. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_start * S ((S (0)) * fs_v_dst_flat_prefixpositive) + (0))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_terminal. fs_h_dst_flat_prefixpositive_body_terminal + S (dst_positive_sum_flat_prefix) = S ((S (m*n)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_terminal. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_terminal * S ((S (m*n)) * fs_v_dst_flat_prefixpositive) + (dst_positive_sum_flat_prefix))) /\ forall fs_i_dst_flat_prefixpositive_body_steps. (exists fs_lt_dst_flat_prefixpositive_body_steps_bound. fs_lt_dst_flat_prefixpositive_body_steps_bound + S fs_i_dst_flat_prefixpositive_body_steps = m*n) -> exists fs_a_dst_flat_prefixpositive_body_steps fs_r_dst_flat_prefixpositive_body_steps fs_s_dst_flat_prefixpositive_body_steps. ((((exists fs_h_dst_flat_prefixpositive_body_steps_summand. fs_h_dst_flat_prefixpositive_body_steps_summand + S (fs_a_dst_flat_prefixpositive_body_steps) = S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * dst_positive_scale_flat_prefix)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_summand. dst_positive_code_flat_prefix = fs_q_dst_flat_prefixpositive_body_steps_summand * S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * dst_positive_scale_flat_prefix) + (fs_a_dst_flat_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_steps_partial. fs_h_dst_flat_prefixpositive_body_steps_partial + S (fs_r_dst_flat_prefixpositive_body_steps) = S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_partial. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_steps_partial * S ((S (fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive) + (fs_r_dst_flat_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_flat_prefixpositive_body_steps_successor. fs_h_dst_flat_prefixpositive_body_steps_successor + S (fs_s_dst_flat_prefixpositive_body_steps) = S ((S (S fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive)) /\ exists fs_q_dst_flat_prefixpositive_body_steps_successor. fs_u_dst_flat_prefixpositive = fs_q_dst_flat_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_flat_prefixpositive_body_steps)) * fs_v_dst_flat_prefixpositive) + (fs_s_dst_flat_prefixpositive_body_steps))) /\ fs_s_dst_flat_prefixpositive_body_steps = fs_r_dst_flat_prefixpositive_body_steps + fs_a_dst_flat_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_flat_prefixnegative fs_v_dst_flat_prefixnegative. ((((exists fs_h_dst_flat_prefixnegative_body_start. fs_h_dst_flat_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_start. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_start * S ((S (0)) * fs_v_dst_flat_prefixnegative) + (0))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_terminal. fs_h_dst_flat_prefixnegative_body_terminal + S (dst_negative_sum_flat_prefix) = S ((S (m*n)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_terminal. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_terminal * S ((S (m*n)) * fs_v_dst_flat_prefixnegative) + (dst_negative_sum_flat_prefix))) /\ forall fs_i_dst_flat_prefixnegative_body_steps. (exists fs_lt_dst_flat_prefixnegative_body_steps_bound. fs_lt_dst_flat_prefixnegative_body_steps_bound + S fs_i_dst_flat_prefixnegative_body_steps = m*n) -> exists fs_a_dst_flat_prefixnegative_body_steps fs_r_dst_flat_prefixnegative_body_steps fs_s_dst_flat_prefixnegative_body_steps. ((((exists fs_h_dst_flat_prefixnegative_body_steps_summand. fs_h_dst_flat_prefixnegative_body_steps_summand + S (fs_a_dst_flat_prefixnegative_body_steps) = S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * dst_negative_scale_flat_prefix)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_summand. dst_negative_code_flat_prefix = fs_q_dst_flat_prefixnegative_body_steps_summand * S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * dst_negative_scale_flat_prefix) + (fs_a_dst_flat_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_steps_partial. fs_h_dst_flat_prefixnegative_body_steps_partial + S (fs_r_dst_flat_prefixnegative_body_steps) = S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_partial. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_steps_partial * S ((S (fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative) + (fs_r_dst_flat_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_flat_prefixnegative_body_steps_successor. fs_h_dst_flat_prefixnegative_body_steps_successor + S (fs_s_dst_flat_prefixnegative_body_steps) = S ((S (S fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative)) /\ exists fs_q_dst_flat_prefixnegative_body_steps_successor. fs_u_dst_flat_prefixnegative = fs_q_dst_flat_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_flat_prefixnegative_body_steps)) * fs_v_dst_flat_prefixnegative) + (fs_s_dst_flat_prefixnegative_body_steps))) /\ fs_s_dst_flat_prefixnegative_body_steps = fs_r_dst_flat_prefixnegative_body_steps + fs_a_dst_flat_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_flat_prefixresult ge_balance_negative_flat_prefixresult. (((((z) = 2 * (ge_balance_positive_flat_prefixresult) /\ (ge_balance_negative_flat_prefixresult) = 0) \/ exists ge_signed_half_flat_prefixresultdecode. (((z) = 2 * ge_signed_half_flat_prefixresultdecode + 1 /\ (ge_balance_positive_flat_prefixresult) = 0) /\ (ge_balance_negative_flat_prefixresult) = S ge_signed_half_flat_prefixresultdecode))) /\ ((dst_positive_sum_flat_prefix) + ge_balance_negative_flat_prefixresult = (dst_negative_sum_flat_prefix) + ge_balance_positive_flat_prefixresult)))))))))))