signed_cartesian_flat_prefix_zero

Exact expanded first-order arithmetic statement

forall F G n T z. (exists dst_positive_code_prefix_zero_table dst_positive_scale_prefix_zero_table dst_negative_code_prefix_zero_table dst_negative_scale_prefix_zero_table. (((T) = (((((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) * S ((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) + ((dst_positive_scale_prefix_zero_table) + (dst_positive_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))) * S ((((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) * S ((dst_positive_code_prefix_zero_table) + (dst_positive_scale_prefix_zero_table)) + ((dst_positive_scale_prefix_zero_table) + (dst_positive_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))) + ((((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table))) + (((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) * S ((dst_negative_code_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)) + ((dst_negative_scale_prefix_zero_table) + (dst_negative_scale_prefix_zero_table)))))) /\ (forall dst_index_prefix_zero_table. (exists pvs_le_gap_prefix_zero_tabledomain. pvs_le_gap_prefix_zero_tabledomain + (dst_index_prefix_zero_table) = (0)) -> exists dst_positive_prefix_zero_table dst_negative_prefix_zero_table dst_value_prefix_zero_table. ((((exists ff_h_pvs_prefix_zero_tableentrypositive. ff_h_pvs_prefix_zero_tableentrypositive + S (dst_positive_prefix_zero_table) = S ((S (dst_index_prefix_zero_table)) * dst_positive_scale_prefix_zero_table)) /\ exists ff_q_pvs_prefix_zero_tableentrypositive. dst_positive_code_prefix_zero_table = ff_q_pvs_prefix_zero_tableentrypositive * S ((S (dst_index_prefix_zero_table)) * dst_positive_scale_prefix_zero_table) + (dst_positive_prefix_zero_table))) /\ (((((exists ff_h_pvs_prefix_zero_tableentrynegative. ff_h_pvs_prefix_zero_tableentrynegative + S (dst_negative_prefix_zero_table) = S ((S (dst_index_prefix_zero_table)) * dst_negative_scale_prefix_zero_table)) /\ exists ff_q_pvs_prefix_zero_tableentrynegative. dst_negative_code_prefix_zero_table = ff_q_pvs_prefix_zero_tableentrynegative * S ((S (dst_index_prefix_zero_table)) * dst_negative_scale_prefix_zero_table) + (dst_negative_prefix_zero_table))) /\ (exists ge_balance_positive_prefix_zero_tableentryvalue ge_balance_negative_prefix_zero_tableentryvalue. (((((dst_value_prefix_zero_table) = 2 * (ge_balance_positive_prefix_zero_tableentryvalue) /\ (ge_balance_negative_prefix_zero_tableentryvalue) = 0) \/ exists ge_signed_half_prefix_zero_tableentryvaluedecode. (((dst_value_prefix_zero_table) = 2 * ge_signed_half_prefix_zero_tableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_tableentryvalue) = 0) /\ (ge_balance_negative_prefix_zero_tableentryvalue) = S ge_signed_half_prefix_zero_tableentryvaluedecode))) /\ ((dst_positive_prefix_zero_table) + ge_balance_negative_prefix_zero_tableentryvalue = (dst_negative_prefix_zero_table) + ge_balance_positive_prefix_zero_tableentryvalue))))))))) -> (exists dst_positive_code_prefix_zero_entry dst_positive_scale_prefix_zero_entry dst_negative_code_prefix_zero_entry dst_negative_scale_prefix_zero_entry dst_positive_prefix_zero_entry dst_negative_prefix_zero_entry. (((T) = (((((dst_positive_code_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry)) * S ((dst_positive_code_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry)) + ((dst_positive_scale_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry))) + (((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) * S ((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) + ((dst_negative_scale_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)))) * S ((((dst_positive_code_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry)) * S ((dst_positive_code_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry)) + ((dst_positive_scale_prefix_zero_entry) + (dst_positive_scale_prefix_zero_entry))) + (((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) * S ((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) + ((dst_negative_scale_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)))) + ((((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) * S ((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) + ((dst_negative_scale_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry))) + (((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) * S ((dst_negative_code_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)) + ((dst_negative_scale_prefix_zero_entry) + (dst_negative_scale_prefix_zero_entry)))))) /\ (((((exists ff_h_pvs_prefix_zero_entrypositive. ff_h_pvs_prefix_zero_entrypositive + S (dst_positive_prefix_zero_entry) = S ((S (0)) * dst_positive_scale_prefix_zero_entry)) /\ exists ff_q_pvs_prefix_zero_entrypositive. dst_positive_code_prefix_zero_entry = ff_q_pvs_prefix_zero_entrypositive * S ((S (0)) * dst_positive_scale_prefix_zero_entry) + (dst_positive_prefix_zero_entry))) /\ (((((exists ff_h_pvs_prefix_zero_entrynegative. ff_h_pvs_prefix_zero_entrynegative + S (dst_negative_prefix_zero_entry) = S ((S (0)) * dst_negative_scale_prefix_zero_entry)) /\ exists ff_q_pvs_prefix_zero_entrynegative. dst_negative_code_prefix_zero_entry = ff_q_pvs_prefix_zero_entrynegative * S ((S (0)) * dst_negative_scale_prefix_zero_entry) + (dst_negative_prefix_zero_entry))) /\ (exists ge_balance_positive_prefix_zero_entryvalue ge_balance_negative_prefix_zero_entryvalue. (((((z) = 2 * (ge_balance_positive_prefix_zero_entryvalue) /\ (ge_balance_negative_prefix_zero_entryvalue) = 0) \/ exists ge_signed_half_prefix_zero_entryvaluedecode. (((z) = 2 * ge_signed_half_prefix_zero_entryvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_entryvalue) = 0) /\ (ge_balance_negative_prefix_zero_entryvalue) = S ge_signed_half_prefix_zero_entryvaluedecode))) /\ ((dst_positive_prefix_zero_entry) + ge_balance_negative_prefix_zero_entryvalue = (dst_negative_prefix_zero_entry) + ge_balance_positive_prefix_zero_entryvalue))))))))) -> (exists scp_flat_row_prefix_zero_value scp_flat_column_prefix_zero_value scp_flat_first_prefix_zero_value scp_flat_second_prefix_zero_value. (((0)=((n)*(scp_flat_row_prefix_zero_value)+(scp_flat_column_prefix_zero_value))) /\ (((exists pvs_gap_prefix_zero_valueremainder. pvs_gap_prefix_zero_valueremainder + S (scp_flat_column_prefix_zero_value) = (n)) /\ (((exists dst_positive_code_prefix_zero_valueF dst_positive_scale_prefix_zero_valueF dst_negative_code_prefix_zero_valueF dst_negative_scale_prefix_zero_valueF dst_positive_prefix_zero_valueF dst_negative_prefix_zero_valueF. (((F) = (((((dst_positive_code_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF)) * S ((dst_positive_code_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF)) + ((dst_positive_scale_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF))) + (((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) * S ((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) + ((dst_negative_scale_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)))) * S ((((dst_positive_code_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF)) * S ((dst_positive_code_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF)) + ((dst_positive_scale_prefix_zero_valueF) + (dst_positive_scale_prefix_zero_valueF))) + (((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) * S ((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) + ((dst_negative_scale_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)))) + ((((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) * S ((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) + ((dst_negative_scale_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF))) + (((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) * S ((dst_negative_code_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)) + ((dst_negative_scale_prefix_zero_valueF) + (dst_negative_scale_prefix_zero_valueF)))))) /\ (((((exists ff_h_pvs_prefix_zero_valueFpositive. ff_h_pvs_prefix_zero_valueFpositive + S (dst_positive_prefix_zero_valueF) = S ((S (scp_flat_row_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueF)) /\ exists ff_q_pvs_prefix_zero_valueFpositive. dst_positive_code_prefix_zero_valueF = ff_q_pvs_prefix_zero_valueFpositive * S ((S (scp_flat_row_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueF) + (dst_positive_prefix_zero_valueF))) /\ (((((exists ff_h_pvs_prefix_zero_valueFnegative. ff_h_pvs_prefix_zero_valueFnegative + S (dst_negative_prefix_zero_valueF) = S ((S (scp_flat_row_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueF)) /\ exists ff_q_pvs_prefix_zero_valueFnegative. dst_negative_code_prefix_zero_valueF = ff_q_pvs_prefix_zero_valueFnegative * S ((S (scp_flat_row_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueF) + (dst_negative_prefix_zero_valueF))) /\ (exists ge_balance_positive_prefix_zero_valueFvalue ge_balance_negative_prefix_zero_valueFvalue. (((((scp_flat_first_prefix_zero_value) = 2 * (ge_balance_positive_prefix_zero_valueFvalue) /\ (ge_balance_negative_prefix_zero_valueFvalue) = 0) \/ exists ge_signed_half_prefix_zero_valueFvaluedecode. (((scp_flat_first_prefix_zero_value) = 2 * ge_signed_half_prefix_zero_valueFvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_valueFvalue) = 0) /\ (ge_balance_negative_prefix_zero_valueFvalue) = S ge_signed_half_prefix_zero_valueFvaluedecode))) /\ ((dst_positive_prefix_zero_valueF) + ge_balance_negative_prefix_zero_valueFvalue = (dst_negative_prefix_zero_valueF) + ge_balance_positive_prefix_zero_valueFvalue))))))))) /\ (((exists dst_positive_code_prefix_zero_valueG dst_positive_scale_prefix_zero_valueG dst_negative_code_prefix_zero_valueG dst_negative_scale_prefix_zero_valueG dst_positive_prefix_zero_valueG dst_negative_prefix_zero_valueG. (((G) = (((((dst_positive_code_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG)) * S ((dst_positive_code_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG)) + ((dst_positive_scale_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG))) + (((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) * S ((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) + ((dst_negative_scale_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)))) * S ((((dst_positive_code_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG)) * S ((dst_positive_code_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG)) + ((dst_positive_scale_prefix_zero_valueG) + (dst_positive_scale_prefix_zero_valueG))) + (((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) * S ((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) + ((dst_negative_scale_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)))) + ((((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) * S ((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) + ((dst_negative_scale_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG))) + (((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) * S ((dst_negative_code_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)) + ((dst_negative_scale_prefix_zero_valueG) + (dst_negative_scale_prefix_zero_valueG)))))) /\ (((((exists ff_h_pvs_prefix_zero_valueGpositive. ff_h_pvs_prefix_zero_valueGpositive + S (dst_positive_prefix_zero_valueG) = S ((S (scp_flat_column_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueG)) /\ exists ff_q_pvs_prefix_zero_valueGpositive. dst_positive_code_prefix_zero_valueG = ff_q_pvs_prefix_zero_valueGpositive * S ((S (scp_flat_column_prefix_zero_value)) * dst_positive_scale_prefix_zero_valueG) + (dst_positive_prefix_zero_valueG))) /\ (((((exists ff_h_pvs_prefix_zero_valueGnegative. ff_h_pvs_prefix_zero_valueGnegative + S (dst_negative_prefix_zero_valueG) = S ((S (scp_flat_column_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueG)) /\ exists ff_q_pvs_prefix_zero_valueGnegative. dst_negative_code_prefix_zero_valueG = ff_q_pvs_prefix_zero_valueGnegative * S ((S (scp_flat_column_prefix_zero_value)) * dst_negative_scale_prefix_zero_valueG) + (dst_negative_prefix_zero_valueG))) /\ (exists ge_balance_positive_prefix_zero_valueGvalue ge_balance_negative_prefix_zero_valueGvalue. (((((scp_flat_second_prefix_zero_value) = 2 * (ge_balance_positive_prefix_zero_valueGvalue) /\ (ge_balance_negative_prefix_zero_valueGvalue) = 0) \/ exists ge_signed_half_prefix_zero_valueGvaluedecode. (((scp_flat_second_prefix_zero_value) = 2 * ge_signed_half_prefix_zero_valueGvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_valueGvalue) = 0) /\ (ge_balance_negative_prefix_zero_valueGvalue) = S ge_signed_half_prefix_zero_valueGvaluedecode))) /\ ((dst_positive_prefix_zero_valueG) + ge_balance_negative_prefix_zero_valueGvalue = (dst_negative_prefix_zero_valueG) + ge_balance_positive_prefix_zero_valueGvalue))))))))) /\ (exists sto_ap_prefix_zero_valuevalue sto_an_prefix_zero_valuevalue sto_bp_prefix_zero_valuevalue sto_bn_prefix_zero_valuevalue sto_cp_prefix_zero_valuevalue sto_cn_prefix_zero_valuevalue. (((((scp_flat_first_prefix_zero_value) = 2 * (sto_ap_prefix_zero_valuevalue) /\ (sto_an_prefix_zero_valuevalue) = 0) \/ exists ge_signed_half_prefix_zero_valuevalueleft. (((scp_flat_first_prefix_zero_value) = 2 * ge_signed_half_prefix_zero_valuevalueleft + 1 /\ (sto_ap_prefix_zero_valuevalue) = 0) /\ (sto_an_prefix_zero_valuevalue) = S ge_signed_half_prefix_zero_valuevalueleft))) /\ ((((((scp_flat_second_prefix_zero_value) = 2 * (sto_bp_prefix_zero_valuevalue) /\ (sto_bn_prefix_zero_valuevalue) = 0) \/ exists ge_signed_half_prefix_zero_valuevalueright. (((scp_flat_second_prefix_zero_value) = 2 * ge_signed_half_prefix_zero_valuevalueright + 1 /\ (sto_bp_prefix_zero_valuevalue) = 0) /\ (sto_bn_prefix_zero_valuevalue) = S ge_signed_half_prefix_zero_valuevalueright))) /\ ((((((z) = 2 * (sto_cp_prefix_zero_valuevalue) /\ (sto_cn_prefix_zero_valuevalue) = 0) \/ exists ge_signed_half_prefix_zero_valuevalueoutput. (((z) = 2 * ge_signed_half_prefix_zero_valuevalueoutput + 1 /\ (sto_cp_prefix_zero_valuevalue) = 0) /\ (sto_cn_prefix_zero_valuevalue) = S ge_signed_half_prefix_zero_valuevalueoutput))) /\ ((sto_ap_prefix_zero_valuevalue * sto_bp_prefix_zero_valuevalue + sto_an_prefix_zero_valuevalue * sto_bn_prefix_zero_valuevalue) + sto_cn_prefix_zero_valuevalue = (sto_ap_prefix_zero_valuevalue * sto_bn_prefix_zero_valuevalue + sto_an_prefix_zero_valuevalue * sto_bp_prefix_zero_valuevalue) + sto_cp_prefix_zero_valuevalue))))))))))))))) -> (((exists dst_positive_code_prefix_zero_resulttable dst_positive_scale_prefix_zero_resulttable dst_negative_code_prefix_zero_resulttable dst_negative_scale_prefix_zero_resulttable. (((T) = (((((dst_positive_code_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable)) * S ((dst_positive_code_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable)) + ((dst_positive_scale_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable))) + (((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) * S ((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) + ((dst_negative_scale_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)))) * S ((((dst_positive_code_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable)) * S ((dst_positive_code_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable)) + ((dst_positive_scale_prefix_zero_resulttable) + (dst_positive_scale_prefix_zero_resulttable))) + (((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) * S ((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) + ((dst_negative_scale_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)))) + ((((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) * S ((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) + ((dst_negative_scale_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable))) + (((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) * S ((dst_negative_code_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)) + ((dst_negative_scale_prefix_zero_resulttable) + (dst_negative_scale_prefix_zero_resulttable)))))) /\ (forall dst_index_prefix_zero_resulttable. (exists pvs_le_gap_prefix_zero_resulttabledomain. pvs_le_gap_prefix_zero_resulttabledomain + (dst_index_prefix_zero_resulttable) = (0)) -> exists dst_positive_prefix_zero_resulttable dst_negative_prefix_zero_resulttable dst_value_prefix_zero_resulttable. ((((exists ff_h_pvs_prefix_zero_resulttableentrypositive. ff_h_pvs_prefix_zero_resulttableentrypositive + S (dst_positive_prefix_zero_resulttable) = S ((S (dst_index_prefix_zero_resulttable)) * dst_positive_scale_prefix_zero_resulttable)) /\ exists ff_q_pvs_prefix_zero_resulttableentrypositive. dst_positive_code_prefix_zero_resulttable = ff_q_pvs_prefix_zero_resulttableentrypositive * S ((S (dst_index_prefix_zero_resulttable)) * dst_positive_scale_prefix_zero_resulttable) + (dst_positive_prefix_zero_resulttable))) /\ (((((exists ff_h_pvs_prefix_zero_resulttableentrynegative. ff_h_pvs_prefix_zero_resulttableentrynegative + S (dst_negative_prefix_zero_resulttable) = S ((S (dst_index_prefix_zero_resulttable)) * dst_negative_scale_prefix_zero_resulttable)) /\ exists ff_q_pvs_prefix_zero_resulttableentrynegative. dst_negative_code_prefix_zero_resulttable = ff_q_pvs_prefix_zero_resulttableentrynegative * S ((S (dst_index_prefix_zero_resulttable)) * dst_negative_scale_prefix_zero_resulttable) + (dst_negative_prefix_zero_resulttable))) /\ (exists ge_balance_positive_prefix_zero_resulttableentryvalue ge_balance_negative_prefix_zero_resulttableentryvalue. (((((dst_value_prefix_zero_resulttable) = 2 * (ge_balance_positive_prefix_zero_resulttableentryvalue) /\ (ge_balance_negative_prefix_zero_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_zero_resulttableentryvaluedecode. (((dst_value_prefix_zero_resulttable) = 2 * ge_signed_half_prefix_zero_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_zero_resulttableentryvalue) = S ge_signed_half_prefix_zero_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_zero_resulttable) + ge_balance_negative_prefix_zero_resulttableentryvalue = (dst_negative_prefix_zero_resulttable) + ge_balance_positive_prefix_zero_resulttableentryvalue))))))))) /\ (forall scp_flat_index_prefix_zero_result scp_flat_value_prefix_zero_result. (exists pvs_le_gap_prefix_zero_resultbound. pvs_le_gap_prefix_zero_resultbound + (scp_flat_index_prefix_zero_result) = (0)) -> (exists dst_positive_code_prefix_zero_resultentry dst_positive_scale_prefix_zero_resultentry dst_negative_code_prefix_zero_resultentry dst_negative_scale_prefix_zero_resultentry dst_positive_prefix_zero_resultentry dst_negative_prefix_zero_resultentry. (((T) = (((((dst_positive_code_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry)) * S ((dst_positive_code_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry)) + ((dst_positive_scale_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry))) + (((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) * S ((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) + ((dst_negative_scale_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)))) * S ((((dst_positive_code_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry)) * S ((dst_positive_code_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry)) + ((dst_positive_scale_prefix_zero_resultentry) + (dst_positive_scale_prefix_zero_resultentry))) + (((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) * S ((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) + ((dst_negative_scale_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)))) + ((((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) * S ((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) + ((dst_negative_scale_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry))) + (((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) * S ((dst_negative_code_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)) + ((dst_negative_scale_prefix_zero_resultentry) + (dst_negative_scale_prefix_zero_resultentry)))))) /\ (((((exists ff_h_pvs_prefix_zero_resultentrypositive. ff_h_pvs_prefix_zero_resultentrypositive + S (dst_positive_prefix_zero_resultentry) = S ((S (scp_flat_index_prefix_zero_result)) * dst_positive_scale_prefix_zero_resultentry)) /\ exists ff_q_pvs_prefix_zero_resultentrypositive. dst_positive_code_prefix_zero_resultentry = ff_q_pvs_prefix_zero_resultentrypositive * S ((S (scp_flat_index_prefix_zero_result)) * dst_positive_scale_prefix_zero_resultentry) + (dst_positive_prefix_zero_resultentry))) /\ (((((exists ff_h_pvs_prefix_zero_resultentrynegative. ff_h_pvs_prefix_zero_resultentrynegative + S (dst_negative_prefix_zero_resultentry) = S ((S (scp_flat_index_prefix_zero_result)) * dst_negative_scale_prefix_zero_resultentry)) /\ exists ff_q_pvs_prefix_zero_resultentrynegative. dst_negative_code_prefix_zero_resultentry = ff_q_pvs_prefix_zero_resultentrynegative * S ((S (scp_flat_index_prefix_zero_result)) * dst_negative_scale_prefix_zero_resultentry) + (dst_negative_prefix_zero_resultentry))) /\ (exists ge_balance_positive_prefix_zero_resultentryvalue ge_balance_negative_prefix_zero_resultentryvalue. (((((scp_flat_value_prefix_zero_result) = 2 * (ge_balance_positive_prefix_zero_resultentryvalue) /\ (ge_balance_negative_prefix_zero_resultentryvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultentryvaluedecode. (((scp_flat_value_prefix_zero_result) = 2 * ge_signed_half_prefix_zero_resultentryvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_resultentryvalue) = 0) /\ (ge_balance_negative_prefix_zero_resultentryvalue) = S ge_signed_half_prefix_zero_resultentryvaluedecode))) /\ ((dst_positive_prefix_zero_resultentry) + ge_balance_negative_prefix_zero_resultentryvalue = (dst_negative_prefix_zero_resultentry) + ge_balance_positive_prefix_zero_resultentryvalue))))))))) -> (exists scp_flat_row_prefix_zero_resultproduct scp_flat_column_prefix_zero_resultproduct scp_flat_first_prefix_zero_resultproduct scp_flat_second_prefix_zero_resultproduct. (((scp_flat_index_prefix_zero_result)=((n)*(scp_flat_row_prefix_zero_resultproduct)+(scp_flat_column_prefix_zero_resultproduct))) /\ (((exists pvs_gap_prefix_zero_resultproductremainder. pvs_gap_prefix_zero_resultproductremainder + S (scp_flat_column_prefix_zero_resultproduct) = (n)) /\ (((exists dst_positive_code_prefix_zero_resultproductF dst_positive_scale_prefix_zero_resultproductF dst_negative_code_prefix_zero_resultproductF dst_negative_scale_prefix_zero_resultproductF dst_positive_prefix_zero_resultproductF dst_negative_prefix_zero_resultproductF. (((F) = (((((dst_positive_code_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF)) * S ((dst_positive_code_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF)) + ((dst_positive_scale_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF))) + (((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) * S ((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) + ((dst_negative_scale_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)))) * S ((((dst_positive_code_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF)) * S ((dst_positive_code_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF)) + ((dst_positive_scale_prefix_zero_resultproductF) + (dst_positive_scale_prefix_zero_resultproductF))) + (((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) * S ((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) + ((dst_negative_scale_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)))) + ((((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) * S ((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) + ((dst_negative_scale_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF))) + (((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) * S ((dst_negative_code_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)) + ((dst_negative_scale_prefix_zero_resultproductF) + (dst_negative_scale_prefix_zero_resultproductF)))))) /\ (((((exists ff_h_pvs_prefix_zero_resultproductFpositive. ff_h_pvs_prefix_zero_resultproductFpositive + S (dst_positive_prefix_zero_resultproductF) = S ((S (scp_flat_row_prefix_zero_resultproduct)) * dst_positive_scale_prefix_zero_resultproductF)) /\ exists ff_q_pvs_prefix_zero_resultproductFpositive. dst_positive_code_prefix_zero_resultproductF = ff_q_pvs_prefix_zero_resultproductFpositive * S ((S (scp_flat_row_prefix_zero_resultproduct)) * dst_positive_scale_prefix_zero_resultproductF) + (dst_positive_prefix_zero_resultproductF))) /\ (((((exists ff_h_pvs_prefix_zero_resultproductFnegative. ff_h_pvs_prefix_zero_resultproductFnegative + S (dst_negative_prefix_zero_resultproductF) = S ((S (scp_flat_row_prefix_zero_resultproduct)) * dst_negative_scale_prefix_zero_resultproductF)) /\ exists ff_q_pvs_prefix_zero_resultproductFnegative. dst_negative_code_prefix_zero_resultproductF = ff_q_pvs_prefix_zero_resultproductFnegative * S ((S (scp_flat_row_prefix_zero_resultproduct)) * dst_negative_scale_prefix_zero_resultproductF) + (dst_negative_prefix_zero_resultproductF))) /\ (exists ge_balance_positive_prefix_zero_resultproductFvalue ge_balance_negative_prefix_zero_resultproductFvalue. (((((scp_flat_first_prefix_zero_resultproduct) = 2 * (ge_balance_positive_prefix_zero_resultproductFvalue) /\ (ge_balance_negative_prefix_zero_resultproductFvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultproductFvaluedecode. (((scp_flat_first_prefix_zero_resultproduct) = 2 * ge_signed_half_prefix_zero_resultproductFvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_resultproductFvalue) = 0) /\ (ge_balance_negative_prefix_zero_resultproductFvalue) = S ge_signed_half_prefix_zero_resultproductFvaluedecode))) /\ ((dst_positive_prefix_zero_resultproductF) + ge_balance_negative_prefix_zero_resultproductFvalue = (dst_negative_prefix_zero_resultproductF) + ge_balance_positive_prefix_zero_resultproductFvalue))))))))) /\ (((exists dst_positive_code_prefix_zero_resultproductG dst_positive_scale_prefix_zero_resultproductG dst_negative_code_prefix_zero_resultproductG dst_negative_scale_prefix_zero_resultproductG dst_positive_prefix_zero_resultproductG dst_negative_prefix_zero_resultproductG. (((G) = (((((dst_positive_code_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG)) * S ((dst_positive_code_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG)) + ((dst_positive_scale_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG))) + (((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) * S ((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) + ((dst_negative_scale_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)))) * S ((((dst_positive_code_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG)) * S ((dst_positive_code_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG)) + ((dst_positive_scale_prefix_zero_resultproductG) + (dst_positive_scale_prefix_zero_resultproductG))) + (((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) * S ((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) + ((dst_negative_scale_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)))) + ((((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) * S ((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) + ((dst_negative_scale_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG))) + (((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) * S ((dst_negative_code_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)) + ((dst_negative_scale_prefix_zero_resultproductG) + (dst_negative_scale_prefix_zero_resultproductG)))))) /\ (((((exists ff_h_pvs_prefix_zero_resultproductGpositive. ff_h_pvs_prefix_zero_resultproductGpositive + S (dst_positive_prefix_zero_resultproductG) = S ((S (scp_flat_column_prefix_zero_resultproduct)) * dst_positive_scale_prefix_zero_resultproductG)) /\ exists ff_q_pvs_prefix_zero_resultproductGpositive. dst_positive_code_prefix_zero_resultproductG = ff_q_pvs_prefix_zero_resultproductGpositive * S ((S (scp_flat_column_prefix_zero_resultproduct)) * dst_positive_scale_prefix_zero_resultproductG) + (dst_positive_prefix_zero_resultproductG))) /\ (((((exists ff_h_pvs_prefix_zero_resultproductGnegative. ff_h_pvs_prefix_zero_resultproductGnegative + S (dst_negative_prefix_zero_resultproductG) = S ((S (scp_flat_column_prefix_zero_resultproduct)) * dst_negative_scale_prefix_zero_resultproductG)) /\ exists ff_q_pvs_prefix_zero_resultproductGnegative. dst_negative_code_prefix_zero_resultproductG = ff_q_pvs_prefix_zero_resultproductGnegative * S ((S (scp_flat_column_prefix_zero_resultproduct)) * dst_negative_scale_prefix_zero_resultproductG) + (dst_negative_prefix_zero_resultproductG))) /\ (exists ge_balance_positive_prefix_zero_resultproductGvalue ge_balance_negative_prefix_zero_resultproductGvalue. (((((scp_flat_second_prefix_zero_resultproduct) = 2 * (ge_balance_positive_prefix_zero_resultproductGvalue) /\ (ge_balance_negative_prefix_zero_resultproductGvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultproductGvaluedecode. (((scp_flat_second_prefix_zero_resultproduct) = 2 * ge_signed_half_prefix_zero_resultproductGvaluedecode + 1 /\ (ge_balance_positive_prefix_zero_resultproductGvalue) = 0) /\ (ge_balance_negative_prefix_zero_resultproductGvalue) = S ge_signed_half_prefix_zero_resultproductGvaluedecode))) /\ ((dst_positive_prefix_zero_resultproductG) + ge_balance_negative_prefix_zero_resultproductGvalue = (dst_negative_prefix_zero_resultproductG) + ge_balance_positive_prefix_zero_resultproductGvalue))))))))) /\ (exists sto_ap_prefix_zero_resultproductvalue sto_an_prefix_zero_resultproductvalue sto_bp_prefix_zero_resultproductvalue sto_bn_prefix_zero_resultproductvalue sto_cp_prefix_zero_resultproductvalue sto_cn_prefix_zero_resultproductvalue. (((((scp_flat_first_prefix_zero_resultproduct) = 2 * (sto_ap_prefix_zero_resultproductvalue) /\ (sto_an_prefix_zero_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultproductvalueleft. (((scp_flat_first_prefix_zero_resultproduct) = 2 * ge_signed_half_prefix_zero_resultproductvalueleft + 1 /\ (sto_ap_prefix_zero_resultproductvalue) = 0) /\ (sto_an_prefix_zero_resultproductvalue) = S ge_signed_half_prefix_zero_resultproductvalueleft))) /\ ((((((scp_flat_second_prefix_zero_resultproduct) = 2 * (sto_bp_prefix_zero_resultproductvalue) /\ (sto_bn_prefix_zero_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultproductvalueright. (((scp_flat_second_prefix_zero_resultproduct) = 2 * ge_signed_half_prefix_zero_resultproductvalueright + 1 /\ (sto_bp_prefix_zero_resultproductvalue) = 0) /\ (sto_bn_prefix_zero_resultproductvalue) = S ge_signed_half_prefix_zero_resultproductvalueright))) /\ ((((((scp_flat_value_prefix_zero_result) = 2 * (sto_cp_prefix_zero_resultproductvalue) /\ (sto_cn_prefix_zero_resultproductvalue) = 0) \/ exists ge_signed_half_prefix_zero_resultproductvalueoutput. (((scp_flat_value_prefix_zero_result) = 2 * ge_signed_half_prefix_zero_resultproductvalueoutput + 1 /\ (sto_cp_prefix_zero_resultproductvalue) = 0) /\ (sto_cn_prefix_zero_resultproductvalue) = S ge_signed_half_prefix_zero_resultproductvalueoutput))) /\ ((sto_ap_prefix_zero_resultproductvalue * sto_bp_prefix_zero_resultproductvalue + sto_an_prefix_zero_resultproductvalue * sto_bn_prefix_zero_resultproductvalue) + sto_cn_prefix_zero_resultproductvalue = (sto_ap_prefix_zero_resultproductvalue * sto_bn_prefix_zero_resultproductvalue + sto_an_prefix_zero_resultproductvalue * sto_bp_prefix_zero_resultproductvalue) + sto_cp_prefix_zero_resultproductvalue))))))))))))))))))