signed_cartesian_product_empty_columns

Exact expanded first-order arithmetic statement

forall F G T m. (exists dst_positive_code_empty_F dst_positive_scale_empty_F dst_negative_code_empty_F dst_negative_scale_empty_F. (((F) = (((((dst_positive_code_empty_F) + (dst_positive_scale_empty_F)) * S ((dst_positive_code_empty_F) + (dst_positive_scale_empty_F)) + ((dst_positive_scale_empty_F) + (dst_positive_scale_empty_F))) + (((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) * S ((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) + ((dst_negative_scale_empty_F) + (dst_negative_scale_empty_F)))) * S ((((dst_positive_code_empty_F) + (dst_positive_scale_empty_F)) * S ((dst_positive_code_empty_F) + (dst_positive_scale_empty_F)) + ((dst_positive_scale_empty_F) + (dst_positive_scale_empty_F))) + (((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) * S ((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) + ((dst_negative_scale_empty_F) + (dst_negative_scale_empty_F)))) + ((((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) * S ((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) + ((dst_negative_scale_empty_F) + (dst_negative_scale_empty_F))) + (((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) * S ((dst_negative_code_empty_F) + (dst_negative_scale_empty_F)) + ((dst_negative_scale_empty_F) + (dst_negative_scale_empty_F)))))) /\ (forall dst_index_empty_F. (exists pvs_le_gap_empty_Fdomain. pvs_le_gap_empty_Fdomain + (dst_index_empty_F) = (0)) -> exists dst_positive_empty_F dst_negative_empty_F dst_value_empty_F. ((((exists ff_h_pvs_empty_Fentrypositive. ff_h_pvs_empty_Fentrypositive + S (dst_positive_empty_F) = S ((S (dst_index_empty_F)) * dst_positive_scale_empty_F)) /\ exists ff_q_pvs_empty_Fentrypositive. dst_positive_code_empty_F = ff_q_pvs_empty_Fentrypositive * S ((S (dst_index_empty_F)) * dst_positive_scale_empty_F) + (dst_positive_empty_F))) /\ (((((exists ff_h_pvs_empty_Fentrynegative. ff_h_pvs_empty_Fentrynegative + S (dst_negative_empty_F) = S ((S (dst_index_empty_F)) * dst_negative_scale_empty_F)) /\ exists ff_q_pvs_empty_Fentrynegative. dst_negative_code_empty_F = ff_q_pvs_empty_Fentrynegative * S ((S (dst_index_empty_F)) * dst_negative_scale_empty_F) + (dst_negative_empty_F))) /\ (exists ge_balance_positive_empty_Fentryvalue ge_balance_negative_empty_Fentryvalue. (((((dst_value_empty_F) = 2 * (ge_balance_positive_empty_Fentryvalue) /\ (ge_balance_negative_empty_Fentryvalue) = 0) \/ exists ge_signed_half_empty_Fentryvaluedecode. (((dst_value_empty_F) = 2 * ge_signed_half_empty_Fentryvaluedecode + 1 /\ (ge_balance_positive_empty_Fentryvalue) = 0) /\ (ge_balance_negative_empty_Fentryvalue) = S ge_signed_half_empty_Fentryvaluedecode))) /\ ((dst_positive_empty_F) + ge_balance_negative_empty_Fentryvalue = (dst_negative_empty_F) + ge_balance_positive_empty_Fentryvalue))))))))) -> (exists dst_positive_code_empty_G dst_positive_scale_empty_G dst_negative_code_empty_G dst_negative_scale_empty_G. (((G) = (((((dst_positive_code_empty_G) + (dst_positive_scale_empty_G)) * S ((dst_positive_code_empty_G) + (dst_positive_scale_empty_G)) + ((dst_positive_scale_empty_G) + (dst_positive_scale_empty_G))) + (((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) * S ((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) + ((dst_negative_scale_empty_G) + (dst_negative_scale_empty_G)))) * S ((((dst_positive_code_empty_G) + (dst_positive_scale_empty_G)) * S ((dst_positive_code_empty_G) + (dst_positive_scale_empty_G)) + ((dst_positive_scale_empty_G) + (dst_positive_scale_empty_G))) + (((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) * S ((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) + ((dst_negative_scale_empty_G) + (dst_negative_scale_empty_G)))) + ((((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) * S ((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) + ((dst_negative_scale_empty_G) + (dst_negative_scale_empty_G))) + (((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) * S ((dst_negative_code_empty_G) + (dst_negative_scale_empty_G)) + ((dst_negative_scale_empty_G) + (dst_negative_scale_empty_G)))))) /\ (forall dst_index_empty_G. (exists pvs_le_gap_empty_Gdomain. pvs_le_gap_empty_Gdomain + (dst_index_empty_G) = (0)) -> exists dst_positive_empty_G dst_negative_empty_G dst_value_empty_G. ((((exists ff_h_pvs_empty_Gentrypositive. ff_h_pvs_empty_Gentrypositive + S (dst_positive_empty_G) = S ((S (dst_index_empty_G)) * dst_positive_scale_empty_G)) /\ exists ff_q_pvs_empty_Gentrypositive. dst_positive_code_empty_G = ff_q_pvs_empty_Gentrypositive * S ((S (dst_index_empty_G)) * dst_positive_scale_empty_G) + (dst_positive_empty_G))) /\ (((((exists ff_h_pvs_empty_Gentrynegative. ff_h_pvs_empty_Gentrynegative + S (dst_negative_empty_G) = S ((S (dst_index_empty_G)) * dst_negative_scale_empty_G)) /\ exists ff_q_pvs_empty_Gentrynegative. dst_negative_code_empty_G = ff_q_pvs_empty_Gentrynegative * S ((S (dst_index_empty_G)) * dst_negative_scale_empty_G) + (dst_negative_empty_G))) /\ (exists ge_balance_positive_empty_Gentryvalue ge_balance_negative_empty_Gentryvalue. (((((dst_value_empty_G) = 2 * (ge_balance_positive_empty_Gentryvalue) /\ (ge_balance_negative_empty_Gentryvalue) = 0) \/ exists ge_signed_half_empty_Gentryvaluedecode. (((dst_value_empty_G) = 2 * ge_signed_half_empty_Gentryvaluedecode + 1 /\ (ge_balance_positive_empty_Gentryvalue) = 0) /\ (ge_balance_negative_empty_Gentryvalue) = S ge_signed_half_empty_Gentryvaluedecode))) /\ ((dst_positive_empty_G) + ge_balance_negative_empty_Gentryvalue = (dst_negative_empty_G) + ge_balance_positive_empty_Gentryvalue))))))))) -> (exists dst_positive_code_empty_T dst_positive_scale_empty_T dst_negative_code_empty_T dst_negative_scale_empty_T. (((T) = (((((dst_positive_code_empty_T) + (dst_positive_scale_empty_T)) * S ((dst_positive_code_empty_T) + (dst_positive_scale_empty_T)) + ((dst_positive_scale_empty_T) + (dst_positive_scale_empty_T))) + (((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) * S ((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) + ((dst_negative_scale_empty_T) + (dst_negative_scale_empty_T)))) * S ((((dst_positive_code_empty_T) + (dst_positive_scale_empty_T)) * S ((dst_positive_code_empty_T) + (dst_positive_scale_empty_T)) + ((dst_positive_scale_empty_T) + (dst_positive_scale_empty_T))) + (((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) * S ((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) + ((dst_negative_scale_empty_T) + (dst_negative_scale_empty_T)))) + ((((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) * S ((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) + ((dst_negative_scale_empty_T) + (dst_negative_scale_empty_T))) + (((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) * S ((dst_negative_code_empty_T) + (dst_negative_scale_empty_T)) + ((dst_negative_scale_empty_T) + (dst_negative_scale_empty_T)))))) /\ (forall dst_index_empty_T. (exists pvs_le_gap_empty_Tdomain. pvs_le_gap_empty_Tdomain + (dst_index_empty_T) = (0)) -> exists dst_positive_empty_T dst_negative_empty_T dst_value_empty_T. ((((exists ff_h_pvs_empty_Tentrypositive. ff_h_pvs_empty_Tentrypositive + S (dst_positive_empty_T) = S ((S (dst_index_empty_T)) * dst_positive_scale_empty_T)) /\ exists ff_q_pvs_empty_Tentrypositive. dst_positive_code_empty_T = ff_q_pvs_empty_Tentrypositive * S ((S (dst_index_empty_T)) * dst_positive_scale_empty_T) + (dst_positive_empty_T))) /\ (((((exists ff_h_pvs_empty_Tentrynegative. ff_h_pvs_empty_Tentrynegative + S (dst_negative_empty_T) = S ((S (dst_index_empty_T)) * dst_negative_scale_empty_T)) /\ exists ff_q_pvs_empty_Tentrynegative. dst_negative_code_empty_T = ff_q_pvs_empty_Tentrynegative * S ((S (dst_index_empty_T)) * dst_negative_scale_empty_T) + (dst_negative_empty_T))) /\ (exists ge_balance_positive_empty_Tentryvalue ge_balance_negative_empty_Tentryvalue. (((((dst_value_empty_T) = 2 * (ge_balance_positive_empty_Tentryvalue) /\ (ge_balance_negative_empty_Tentryvalue) = 0) \/ exists ge_signed_half_empty_Tentryvaluedecode. (((dst_value_empty_T) = 2 * ge_signed_half_empty_Tentryvaluedecode + 1 /\ (ge_balance_positive_empty_Tentryvalue) = 0) /\ (ge_balance_negative_empty_Tentryvalue) = S ge_signed_half_empty_Tentryvaluedecode))) /\ ((dst_positive_empty_T) + ge_balance_negative_empty_Tentryvalue = (dst_negative_empty_T) + ge_balance_positive_empty_Tentryvalue))))))))) -> (((exists dst_positive_code_empty_resultF dst_positive_scale_empty_resultF dst_negative_code_empty_resultF dst_negative_scale_empty_resultF. (((F) = (((((dst_positive_code_empty_resultF) + (dst_positive_scale_empty_resultF)) * S ((dst_positive_code_empty_resultF) + (dst_positive_scale_empty_resultF)) + ((dst_positive_scale_empty_resultF) + (dst_positive_scale_empty_resultF))) + (((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) * S ((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) + ((dst_negative_scale_empty_resultF) + (dst_negative_scale_empty_resultF)))) * S ((((dst_positive_code_empty_resultF) + (dst_positive_scale_empty_resultF)) * S ((dst_positive_code_empty_resultF) + (dst_positive_scale_empty_resultF)) + ((dst_positive_scale_empty_resultF) + (dst_positive_scale_empty_resultF))) + (((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) * S ((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) + ((dst_negative_scale_empty_resultF) + (dst_negative_scale_empty_resultF)))) + ((((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) * S ((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) + ((dst_negative_scale_empty_resultF) + (dst_negative_scale_empty_resultF))) + (((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) * S ((dst_negative_code_empty_resultF) + (dst_negative_scale_empty_resultF)) + ((dst_negative_scale_empty_resultF) + (dst_negative_scale_empty_resultF)))))) /\ (forall dst_index_empty_resultF. (exists pvs_le_gap_empty_resultFdomain. pvs_le_gap_empty_resultFdomain + (dst_index_empty_resultF) = (0)) -> exists dst_positive_empty_resultF dst_negative_empty_resultF dst_value_empty_resultF. ((((exists ff_h_pvs_empty_resultFentrypositive. ff_h_pvs_empty_resultFentrypositive + S (dst_positive_empty_resultF) = S ((S (dst_index_empty_resultF)) * dst_positive_scale_empty_resultF)) /\ exists ff_q_pvs_empty_resultFentrypositive. dst_positive_code_empty_resultF = ff_q_pvs_empty_resultFentrypositive * S ((S (dst_index_empty_resultF)) * dst_positive_scale_empty_resultF) + (dst_positive_empty_resultF))) /\ (((((exists ff_h_pvs_empty_resultFentrynegative. ff_h_pvs_empty_resultFentrynegative + S (dst_negative_empty_resultF) = S ((S (dst_index_empty_resultF)) * dst_negative_scale_empty_resultF)) /\ exists ff_q_pvs_empty_resultFentrynegative. dst_negative_code_empty_resultF = ff_q_pvs_empty_resultFentrynegative * S ((S (dst_index_empty_resultF)) * dst_negative_scale_empty_resultF) + (dst_negative_empty_resultF))) /\ (exists ge_balance_positive_empty_resultFentryvalue ge_balance_negative_empty_resultFentryvalue. (((((dst_value_empty_resultF) = 2 * (ge_balance_positive_empty_resultFentryvalue) /\ (ge_balance_negative_empty_resultFentryvalue) = 0) \/ exists ge_signed_half_empty_resultFentryvaluedecode. (((dst_value_empty_resultF) = 2 * ge_signed_half_empty_resultFentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultFentryvalue) = 0) /\ (ge_balance_negative_empty_resultFentryvalue) = S ge_signed_half_empty_resultFentryvaluedecode))) /\ ((dst_positive_empty_resultF) + ge_balance_negative_empty_resultFentryvalue = (dst_negative_empty_resultF) + ge_balance_positive_empty_resultFentryvalue))))))))) /\ (((exists dst_positive_code_empty_resultG dst_positive_scale_empty_resultG dst_negative_code_empty_resultG dst_negative_scale_empty_resultG. (((G) = (((((dst_positive_code_empty_resultG) + (dst_positive_scale_empty_resultG)) * S ((dst_positive_code_empty_resultG) + (dst_positive_scale_empty_resultG)) + ((dst_positive_scale_empty_resultG) + (dst_positive_scale_empty_resultG))) + (((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) * S ((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) + ((dst_negative_scale_empty_resultG) + (dst_negative_scale_empty_resultG)))) * S ((((dst_positive_code_empty_resultG) + (dst_positive_scale_empty_resultG)) * S ((dst_positive_code_empty_resultG) + (dst_positive_scale_empty_resultG)) + ((dst_positive_scale_empty_resultG) + (dst_positive_scale_empty_resultG))) + (((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) * S ((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) + ((dst_negative_scale_empty_resultG) + (dst_negative_scale_empty_resultG)))) + ((((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) * S ((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) + ((dst_negative_scale_empty_resultG) + (dst_negative_scale_empty_resultG))) + (((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) * S ((dst_negative_code_empty_resultG) + (dst_negative_scale_empty_resultG)) + ((dst_negative_scale_empty_resultG) + (dst_negative_scale_empty_resultG)))))) /\ (forall dst_index_empty_resultG. (exists pvs_le_gap_empty_resultGdomain. pvs_le_gap_empty_resultGdomain + (dst_index_empty_resultG) = (0)) -> exists dst_positive_empty_resultG dst_negative_empty_resultG dst_value_empty_resultG. ((((exists ff_h_pvs_empty_resultGentrypositive. ff_h_pvs_empty_resultGentrypositive + S (dst_positive_empty_resultG) = S ((S (dst_index_empty_resultG)) * dst_positive_scale_empty_resultG)) /\ exists ff_q_pvs_empty_resultGentrypositive. dst_positive_code_empty_resultG = ff_q_pvs_empty_resultGentrypositive * S ((S (dst_index_empty_resultG)) * dst_positive_scale_empty_resultG) + (dst_positive_empty_resultG))) /\ (((((exists ff_h_pvs_empty_resultGentrynegative. ff_h_pvs_empty_resultGentrynegative + S (dst_negative_empty_resultG) = S ((S (dst_index_empty_resultG)) * dst_negative_scale_empty_resultG)) /\ exists ff_q_pvs_empty_resultGentrynegative. dst_negative_code_empty_resultG = ff_q_pvs_empty_resultGentrynegative * S ((S (dst_index_empty_resultG)) * dst_negative_scale_empty_resultG) + (dst_negative_empty_resultG))) /\ (exists ge_balance_positive_empty_resultGentryvalue ge_balance_negative_empty_resultGentryvalue. (((((dst_value_empty_resultG) = 2 * (ge_balance_positive_empty_resultGentryvalue) /\ (ge_balance_negative_empty_resultGentryvalue) = 0) \/ exists ge_signed_half_empty_resultGentryvaluedecode. (((dst_value_empty_resultG) = 2 * ge_signed_half_empty_resultGentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultGentryvalue) = 0) /\ (ge_balance_negative_empty_resultGentryvalue) = S ge_signed_half_empty_resultGentryvaluedecode))) /\ ((dst_positive_empty_resultG) + ge_balance_negative_empty_resultGentryvalue = (dst_negative_empty_resultG) + ge_balance_positive_empty_resultGentryvalue))))))))) /\ (((exists dst_positive_code_empty_resultT dst_positive_scale_empty_resultT dst_negative_code_empty_resultT dst_negative_scale_empty_resultT. (((T) = (((((dst_positive_code_empty_resultT) + (dst_positive_scale_empty_resultT)) * S ((dst_positive_code_empty_resultT) + (dst_positive_scale_empty_resultT)) + ((dst_positive_scale_empty_resultT) + (dst_positive_scale_empty_resultT))) + (((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) * S ((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) + ((dst_negative_scale_empty_resultT) + (dst_negative_scale_empty_resultT)))) * S ((((dst_positive_code_empty_resultT) + (dst_positive_scale_empty_resultT)) * S ((dst_positive_code_empty_resultT) + (dst_positive_scale_empty_resultT)) + ((dst_positive_scale_empty_resultT) + (dst_positive_scale_empty_resultT))) + (((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) * S ((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) + ((dst_negative_scale_empty_resultT) + (dst_negative_scale_empty_resultT)))) + ((((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) * S ((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) + ((dst_negative_scale_empty_resultT) + (dst_negative_scale_empty_resultT))) + (((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) * S ((dst_negative_code_empty_resultT) + (dst_negative_scale_empty_resultT)) + ((dst_negative_scale_empty_resultT) + (dst_negative_scale_empty_resultT)))))) /\ (forall dst_index_empty_resultT. (exists pvs_le_gap_empty_resultTdomain. pvs_le_gap_empty_resultTdomain + (dst_index_empty_resultT) = ((m)*(0))) -> exists dst_positive_empty_resultT dst_negative_empty_resultT dst_value_empty_resultT. ((((exists ff_h_pvs_empty_resultTentrypositive. ff_h_pvs_empty_resultTentrypositive + S (dst_positive_empty_resultT) = S ((S (dst_index_empty_resultT)) * dst_positive_scale_empty_resultT)) /\ exists ff_q_pvs_empty_resultTentrypositive. dst_positive_code_empty_resultT = ff_q_pvs_empty_resultTentrypositive * S ((S (dst_index_empty_resultT)) * dst_positive_scale_empty_resultT) + (dst_positive_empty_resultT))) /\ (((((exists ff_h_pvs_empty_resultTentrynegative. ff_h_pvs_empty_resultTentrynegative + S (dst_negative_empty_resultT) = S ((S (dst_index_empty_resultT)) * dst_negative_scale_empty_resultT)) /\ exists ff_q_pvs_empty_resultTentrynegative. dst_negative_code_empty_resultT = ff_q_pvs_empty_resultTentrynegative * S ((S (dst_index_empty_resultT)) * dst_negative_scale_empty_resultT) + (dst_negative_empty_resultT))) /\ (exists ge_balance_positive_empty_resultTentryvalue ge_balance_negative_empty_resultTentryvalue. (((((dst_value_empty_resultT) = 2 * (ge_balance_positive_empty_resultTentryvalue) /\ (ge_balance_negative_empty_resultTentryvalue) = 0) \/ exists ge_signed_half_empty_resultTentryvaluedecode. (((dst_value_empty_resultT) = 2 * ge_signed_half_empty_resultTentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultTentryvalue) = 0) /\ (ge_balance_negative_empty_resultTentryvalue) = S ge_signed_half_empty_resultTentryvaluedecode))) /\ ((dst_positive_empty_resultT) + ge_balance_negative_empty_resultTentryvalue = (dst_negative_empty_resultT) + ge_balance_positive_empty_resultTentryvalue))))))))) /\ (forall scp_row_empty_result scp_column_empty_result scp_first_empty_result scp_second_empty_result scp_value_empty_result. (exists pvs_gap_empty_resultrows. pvs_gap_empty_resultrows + S (scp_row_empty_result) = (m)) -> (exists pvs_gap_empty_resultcolumns. pvs_gap_empty_resultcolumns + S (scp_column_empty_result) = (0)) -> (exists dst_positive_code_empty_resultfirst dst_positive_scale_empty_resultfirst dst_negative_code_empty_resultfirst dst_negative_scale_empty_resultfirst dst_positive_empty_resultfirst dst_negative_empty_resultfirst. (((F) = (((((dst_positive_code_empty_resultfirst) + (dst_positive_scale_empty_resultfirst)) * S ((dst_positive_code_empty_resultfirst) + (dst_positive_scale_empty_resultfirst)) + ((dst_positive_scale_empty_resultfirst) + (dst_positive_scale_empty_resultfirst))) + (((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) * S ((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) + ((dst_negative_scale_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)))) * S ((((dst_positive_code_empty_resultfirst) + (dst_positive_scale_empty_resultfirst)) * S ((dst_positive_code_empty_resultfirst) + (dst_positive_scale_empty_resultfirst)) + ((dst_positive_scale_empty_resultfirst) + (dst_positive_scale_empty_resultfirst))) + (((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) * S ((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) + ((dst_negative_scale_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)))) + ((((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) * S ((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) + ((dst_negative_scale_empty_resultfirst) + (dst_negative_scale_empty_resultfirst))) + (((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) * S ((dst_negative_code_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)) + ((dst_negative_scale_empty_resultfirst) + (dst_negative_scale_empty_resultfirst)))))) /\ (((((exists ff_h_pvs_empty_resultfirstpositive. ff_h_pvs_empty_resultfirstpositive + S (dst_positive_empty_resultfirst) = S ((S (scp_row_empty_result)) * dst_positive_scale_empty_resultfirst)) /\ exists ff_q_pvs_empty_resultfirstpositive. dst_positive_code_empty_resultfirst = ff_q_pvs_empty_resultfirstpositive * S ((S (scp_row_empty_result)) * dst_positive_scale_empty_resultfirst) + (dst_positive_empty_resultfirst))) /\ (((((exists ff_h_pvs_empty_resultfirstnegative. ff_h_pvs_empty_resultfirstnegative + S (dst_negative_empty_resultfirst) = S ((S (scp_row_empty_result)) * dst_negative_scale_empty_resultfirst)) /\ exists ff_q_pvs_empty_resultfirstnegative. dst_negative_code_empty_resultfirst = ff_q_pvs_empty_resultfirstnegative * S ((S (scp_row_empty_result)) * dst_negative_scale_empty_resultfirst) + (dst_negative_empty_resultfirst))) /\ (exists ge_balance_positive_empty_resultfirstvalue ge_balance_negative_empty_resultfirstvalue. (((((scp_first_empty_result) = 2 * (ge_balance_positive_empty_resultfirstvalue) /\ (ge_balance_negative_empty_resultfirstvalue) = 0) \/ exists ge_signed_half_empty_resultfirstvaluedecode. (((scp_first_empty_result) = 2 * ge_signed_half_empty_resultfirstvaluedecode + 1 /\ (ge_balance_positive_empty_resultfirstvalue) = 0) /\ (ge_balance_negative_empty_resultfirstvalue) = S ge_signed_half_empty_resultfirstvaluedecode))) /\ ((dst_positive_empty_resultfirst) + ge_balance_negative_empty_resultfirstvalue = (dst_negative_empty_resultfirst) + ge_balance_positive_empty_resultfirstvalue))))))))) -> (exists dst_positive_code_empty_resultsecond dst_positive_scale_empty_resultsecond dst_negative_code_empty_resultsecond dst_negative_scale_empty_resultsecond dst_positive_empty_resultsecond dst_negative_empty_resultsecond. (((G) = (((((dst_positive_code_empty_resultsecond) + (dst_positive_scale_empty_resultsecond)) * S ((dst_positive_code_empty_resultsecond) + (dst_positive_scale_empty_resultsecond)) + ((dst_positive_scale_empty_resultsecond) + (dst_positive_scale_empty_resultsecond))) + (((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) * S ((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) + ((dst_negative_scale_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)))) * S ((((dst_positive_code_empty_resultsecond) + (dst_positive_scale_empty_resultsecond)) * S ((dst_positive_code_empty_resultsecond) + (dst_positive_scale_empty_resultsecond)) + ((dst_positive_scale_empty_resultsecond) + (dst_positive_scale_empty_resultsecond))) + (((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) * S ((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) + ((dst_negative_scale_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)))) + ((((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) * S ((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) + ((dst_negative_scale_empty_resultsecond) + (dst_negative_scale_empty_resultsecond))) + (((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) * S ((dst_negative_code_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)) + ((dst_negative_scale_empty_resultsecond) + (dst_negative_scale_empty_resultsecond)))))) /\ (((((exists ff_h_pvs_empty_resultsecondpositive. ff_h_pvs_empty_resultsecondpositive + S (dst_positive_empty_resultsecond) = S ((S (scp_column_empty_result)) * dst_positive_scale_empty_resultsecond)) /\ exists ff_q_pvs_empty_resultsecondpositive. dst_positive_code_empty_resultsecond = ff_q_pvs_empty_resultsecondpositive * S ((S (scp_column_empty_result)) * dst_positive_scale_empty_resultsecond) + (dst_positive_empty_resultsecond))) /\ (((((exists ff_h_pvs_empty_resultsecondnegative. ff_h_pvs_empty_resultsecondnegative + S (dst_negative_empty_resultsecond) = S ((S (scp_column_empty_result)) * dst_negative_scale_empty_resultsecond)) /\ exists ff_q_pvs_empty_resultsecondnegative. dst_negative_code_empty_resultsecond = ff_q_pvs_empty_resultsecondnegative * S ((S (scp_column_empty_result)) * dst_negative_scale_empty_resultsecond) + (dst_negative_empty_resultsecond))) /\ (exists ge_balance_positive_empty_resultsecondvalue ge_balance_negative_empty_resultsecondvalue. (((((scp_second_empty_result) = 2 * (ge_balance_positive_empty_resultsecondvalue) /\ (ge_balance_negative_empty_resultsecondvalue) = 0) \/ exists ge_signed_half_empty_resultsecondvaluedecode. (((scp_second_empty_result) = 2 * ge_signed_half_empty_resultsecondvaluedecode + 1 /\ (ge_balance_positive_empty_resultsecondvalue) = 0) /\ (ge_balance_negative_empty_resultsecondvalue) = S ge_signed_half_empty_resultsecondvaluedecode))) /\ ((dst_positive_empty_resultsecond) + ge_balance_negative_empty_resultsecondvalue = (dst_negative_empty_resultsecond) + ge_balance_positive_empty_resultsecondvalue))))))))) -> (exists dst_positive_code_empty_resultentry dst_positive_scale_empty_resultentry dst_negative_code_empty_resultentry dst_negative_scale_empty_resultentry dst_positive_empty_resultentry dst_negative_empty_resultentry. (((T) = (((((dst_positive_code_empty_resultentry) + (dst_positive_scale_empty_resultentry)) * S ((dst_positive_code_empty_resultentry) + (dst_positive_scale_empty_resultentry)) + ((dst_positive_scale_empty_resultentry) + (dst_positive_scale_empty_resultentry))) + (((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) * S ((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) + ((dst_negative_scale_empty_resultentry) + (dst_negative_scale_empty_resultentry)))) * S ((((dst_positive_code_empty_resultentry) + (dst_positive_scale_empty_resultentry)) * S ((dst_positive_code_empty_resultentry) + (dst_positive_scale_empty_resultentry)) + ((dst_positive_scale_empty_resultentry) + (dst_positive_scale_empty_resultentry))) + (((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) * S ((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) + ((dst_negative_scale_empty_resultentry) + (dst_negative_scale_empty_resultentry)))) + ((((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) * S ((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) + ((dst_negative_scale_empty_resultentry) + (dst_negative_scale_empty_resultentry))) + (((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) * S ((dst_negative_code_empty_resultentry) + (dst_negative_scale_empty_resultentry)) + ((dst_negative_scale_empty_resultentry) + (dst_negative_scale_empty_resultentry)))))) /\ (((((exists ff_h_pvs_empty_resultentrypositive. ff_h_pvs_empty_resultentrypositive + S (dst_positive_empty_resultentry) = S ((S (((0)*(scp_row_empty_result)+(scp_column_empty_result)))) * dst_positive_scale_empty_resultentry)) /\ exists ff_q_pvs_empty_resultentrypositive. dst_positive_code_empty_resultentry = ff_q_pvs_empty_resultentrypositive * S ((S (((0)*(scp_row_empty_result)+(scp_column_empty_result)))) * dst_positive_scale_empty_resultentry) + (dst_positive_empty_resultentry))) /\ (((((exists ff_h_pvs_empty_resultentrynegative. ff_h_pvs_empty_resultentrynegative + S (dst_negative_empty_resultentry) = S ((S (((0)*(scp_row_empty_result)+(scp_column_empty_result)))) * dst_negative_scale_empty_resultentry)) /\ exists ff_q_pvs_empty_resultentrynegative. dst_negative_code_empty_resultentry = ff_q_pvs_empty_resultentrynegative * S ((S (((0)*(scp_row_empty_result)+(scp_column_empty_result)))) * dst_negative_scale_empty_resultentry) + (dst_negative_empty_resultentry))) /\ (exists ge_balance_positive_empty_resultentryvalue ge_balance_negative_empty_resultentryvalue. (((((scp_value_empty_result) = 2 * (ge_balance_positive_empty_resultentryvalue) /\ (ge_balance_negative_empty_resultentryvalue) = 0) \/ exists ge_signed_half_empty_resultentryvaluedecode. (((scp_value_empty_result) = 2 * ge_signed_half_empty_resultentryvaluedecode + 1 /\ (ge_balance_positive_empty_resultentryvalue) = 0) /\ (ge_balance_negative_empty_resultentryvalue) = S ge_signed_half_empty_resultentryvaluedecode))) /\ ((dst_positive_empty_resultentry) + ge_balance_negative_empty_resultentryvalue = (dst_negative_empty_resultentry) + ge_balance_positive_empty_resultentryvalue))))))))) -> (exists sto_ap_empty_resultmultiply sto_an_empty_resultmultiply sto_bp_empty_resultmultiply sto_bn_empty_resultmultiply sto_cp_empty_resultmultiply sto_cn_empty_resultmultiply. (((((scp_first_empty_result) = 2 * (sto_ap_empty_resultmultiply) /\ (sto_an_empty_resultmultiply) = 0) \/ exists ge_signed_half_empty_resultmultiplyleft. (((scp_first_empty_result) = 2 * ge_signed_half_empty_resultmultiplyleft + 1 /\ (sto_ap_empty_resultmultiply) = 0) /\ (sto_an_empty_resultmultiply) = S ge_signed_half_empty_resultmultiplyleft))) /\ ((((((scp_second_empty_result) = 2 * (sto_bp_empty_resultmultiply) /\ (sto_bn_empty_resultmultiply) = 0) \/ exists ge_signed_half_empty_resultmultiplyright. (((scp_second_empty_result) = 2 * ge_signed_half_empty_resultmultiplyright + 1 /\ (sto_bp_empty_resultmultiply) = 0) /\ (sto_bn_empty_resultmultiply) = S ge_signed_half_empty_resultmultiplyright))) /\ ((((((scp_value_empty_result) = 2 * (sto_cp_empty_resultmultiply) /\ (sto_cn_empty_resultmultiply) = 0) \/ exists ge_signed_half_empty_resultmultiplyoutput. (((scp_value_empty_result) = 2 * ge_signed_half_empty_resultmultiplyoutput + 1 /\ (sto_cp_empty_resultmultiply) = 0) /\ (sto_cn_empty_resultmultiply) = S ge_signed_half_empty_resultmultiplyoutput))) /\ ((sto_ap_empty_resultmultiply * sto_bp_empty_resultmultiply + sto_an_empty_resultmultiply * sto_bn_empty_resultmultiply) + sto_cn_empty_resultmultiply = (sto_ap_empty_resultmultiply * sto_bn_empty_resultmultiply + sto_an_empty_resultmultiply * sto_bp_empty_resultmultiply) + sto_cp_empty_resultmultiply))))))))))))))