signed_cartesian_product_from_flat_prefix

Exact expanded first-order arithmetic statement

forall F G T m n. (exists dst_positive_code_from_flat_F dst_positive_scale_from_flat_F dst_negative_code_from_flat_F dst_negative_scale_from_flat_F. (((F) = (((((dst_positive_code_from_flat_F) + (dst_positive_scale_from_flat_F)) * S ((dst_positive_code_from_flat_F) + (dst_positive_scale_from_flat_F)) + ((dst_positive_scale_from_flat_F) + (dst_positive_scale_from_flat_F))) + (((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) * S ((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) + ((dst_negative_scale_from_flat_F) + (dst_negative_scale_from_flat_F)))) * S ((((dst_positive_code_from_flat_F) + (dst_positive_scale_from_flat_F)) * S ((dst_positive_code_from_flat_F) + (dst_positive_scale_from_flat_F)) + ((dst_positive_scale_from_flat_F) + (dst_positive_scale_from_flat_F))) + (((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) * S ((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) + ((dst_negative_scale_from_flat_F) + (dst_negative_scale_from_flat_F)))) + ((((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) * S ((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) + ((dst_negative_scale_from_flat_F) + (dst_negative_scale_from_flat_F))) + (((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) * S ((dst_negative_code_from_flat_F) + (dst_negative_scale_from_flat_F)) + ((dst_negative_scale_from_flat_F) + (dst_negative_scale_from_flat_F)))))) /\ (forall dst_index_from_flat_F. (exists pvs_le_gap_from_flat_Fdomain. pvs_le_gap_from_flat_Fdomain + (dst_index_from_flat_F) = (0)) -> exists dst_positive_from_flat_F dst_negative_from_flat_F dst_value_from_flat_F. ((((exists ff_h_pvs_from_flat_Fentrypositive. ff_h_pvs_from_flat_Fentrypositive + S (dst_positive_from_flat_F) = S ((S (dst_index_from_flat_F)) * dst_positive_scale_from_flat_F)) /\ exists ff_q_pvs_from_flat_Fentrypositive. dst_positive_code_from_flat_F = ff_q_pvs_from_flat_Fentrypositive * S ((S (dst_index_from_flat_F)) * dst_positive_scale_from_flat_F) + (dst_positive_from_flat_F))) /\ (((((exists ff_h_pvs_from_flat_Fentrynegative. ff_h_pvs_from_flat_Fentrynegative + S (dst_negative_from_flat_F) = S ((S (dst_index_from_flat_F)) * dst_negative_scale_from_flat_F)) /\ exists ff_q_pvs_from_flat_Fentrynegative. dst_negative_code_from_flat_F = ff_q_pvs_from_flat_Fentrynegative * S ((S (dst_index_from_flat_F)) * dst_negative_scale_from_flat_F) + (dst_negative_from_flat_F))) /\ (exists ge_balance_positive_from_flat_Fentryvalue ge_balance_negative_from_flat_Fentryvalue. (((((dst_value_from_flat_F) = 2 * (ge_balance_positive_from_flat_Fentryvalue) /\ (ge_balance_negative_from_flat_Fentryvalue) = 0) \/ exists ge_signed_half_from_flat_Fentryvaluedecode. (((dst_value_from_flat_F) = 2 * ge_signed_half_from_flat_Fentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_Fentryvalue) = 0) /\ (ge_balance_negative_from_flat_Fentryvalue) = S ge_signed_half_from_flat_Fentryvaluedecode))) /\ ((dst_positive_from_flat_F) + ge_balance_negative_from_flat_Fentryvalue = (dst_negative_from_flat_F) + ge_balance_positive_from_flat_Fentryvalue))))))))) -> (exists dst_positive_code_from_flat_G dst_positive_scale_from_flat_G dst_negative_code_from_flat_G dst_negative_scale_from_flat_G. (((G) = (((((dst_positive_code_from_flat_G) + (dst_positive_scale_from_flat_G)) * S ((dst_positive_code_from_flat_G) + (dst_positive_scale_from_flat_G)) + ((dst_positive_scale_from_flat_G) + (dst_positive_scale_from_flat_G))) + (((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) * S ((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) + ((dst_negative_scale_from_flat_G) + (dst_negative_scale_from_flat_G)))) * S ((((dst_positive_code_from_flat_G) + (dst_positive_scale_from_flat_G)) * S ((dst_positive_code_from_flat_G) + (dst_positive_scale_from_flat_G)) + ((dst_positive_scale_from_flat_G) + (dst_positive_scale_from_flat_G))) + (((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) * S ((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) + ((dst_negative_scale_from_flat_G) + (dst_negative_scale_from_flat_G)))) + ((((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) * S ((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) + ((dst_negative_scale_from_flat_G) + (dst_negative_scale_from_flat_G))) + (((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) * S ((dst_negative_code_from_flat_G) + (dst_negative_scale_from_flat_G)) + ((dst_negative_scale_from_flat_G) + (dst_negative_scale_from_flat_G)))))) /\ (forall dst_index_from_flat_G. (exists pvs_le_gap_from_flat_Gdomain. pvs_le_gap_from_flat_Gdomain + (dst_index_from_flat_G) = (0)) -> exists dst_positive_from_flat_G dst_negative_from_flat_G dst_value_from_flat_G. ((((exists ff_h_pvs_from_flat_Gentrypositive. ff_h_pvs_from_flat_Gentrypositive + S (dst_positive_from_flat_G) = S ((S (dst_index_from_flat_G)) * dst_positive_scale_from_flat_G)) /\ exists ff_q_pvs_from_flat_Gentrypositive. dst_positive_code_from_flat_G = ff_q_pvs_from_flat_Gentrypositive * S ((S (dst_index_from_flat_G)) * dst_positive_scale_from_flat_G) + (dst_positive_from_flat_G))) /\ (((((exists ff_h_pvs_from_flat_Gentrynegative. ff_h_pvs_from_flat_Gentrynegative + S (dst_negative_from_flat_G) = S ((S (dst_index_from_flat_G)) * dst_negative_scale_from_flat_G)) /\ exists ff_q_pvs_from_flat_Gentrynegative. dst_negative_code_from_flat_G = ff_q_pvs_from_flat_Gentrynegative * S ((S (dst_index_from_flat_G)) * dst_negative_scale_from_flat_G) + (dst_negative_from_flat_G))) /\ (exists ge_balance_positive_from_flat_Gentryvalue ge_balance_negative_from_flat_Gentryvalue. (((((dst_value_from_flat_G) = 2 * (ge_balance_positive_from_flat_Gentryvalue) /\ (ge_balance_negative_from_flat_Gentryvalue) = 0) \/ exists ge_signed_half_from_flat_Gentryvaluedecode. (((dst_value_from_flat_G) = 2 * ge_signed_half_from_flat_Gentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_Gentryvalue) = 0) /\ (ge_balance_negative_from_flat_Gentryvalue) = S ge_signed_half_from_flat_Gentryvaluedecode))) /\ ((dst_positive_from_flat_G) + ge_balance_negative_from_flat_Gentryvalue = (dst_negative_from_flat_G) + ge_balance_positive_from_flat_Gentryvalue))))))))) -> (((exists dst_positive_code_from_flat_inputtable dst_positive_scale_from_flat_inputtable dst_negative_code_from_flat_inputtable dst_negative_scale_from_flat_inputtable. (((T) = (((((dst_positive_code_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable)) * S ((dst_positive_code_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable)) + ((dst_positive_scale_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable))) + (((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) * S ((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) + ((dst_negative_scale_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)))) * S ((((dst_positive_code_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable)) * S ((dst_positive_code_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable)) + ((dst_positive_scale_from_flat_inputtable) + (dst_positive_scale_from_flat_inputtable))) + (((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) * S ((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) + ((dst_negative_scale_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)))) + ((((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) * S ((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) + ((dst_negative_scale_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable))) + (((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) * S ((dst_negative_code_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)) + ((dst_negative_scale_from_flat_inputtable) + (dst_negative_scale_from_flat_inputtable)))))) /\ (forall dst_index_from_flat_inputtable. (exists pvs_le_gap_from_flat_inputtabledomain. pvs_le_gap_from_flat_inputtabledomain + (dst_index_from_flat_inputtable) = (m*n)) -> exists dst_positive_from_flat_inputtable dst_negative_from_flat_inputtable dst_value_from_flat_inputtable. ((((exists ff_h_pvs_from_flat_inputtableentrypositive. ff_h_pvs_from_flat_inputtableentrypositive + S (dst_positive_from_flat_inputtable) = S ((S (dst_index_from_flat_inputtable)) * dst_positive_scale_from_flat_inputtable)) /\ exists ff_q_pvs_from_flat_inputtableentrypositive. dst_positive_code_from_flat_inputtable = ff_q_pvs_from_flat_inputtableentrypositive * S ((S (dst_index_from_flat_inputtable)) * dst_positive_scale_from_flat_inputtable) + (dst_positive_from_flat_inputtable))) /\ (((((exists ff_h_pvs_from_flat_inputtableentrynegative. ff_h_pvs_from_flat_inputtableentrynegative + S (dst_negative_from_flat_inputtable) = S ((S (dst_index_from_flat_inputtable)) * dst_negative_scale_from_flat_inputtable)) /\ exists ff_q_pvs_from_flat_inputtableentrynegative. dst_negative_code_from_flat_inputtable = ff_q_pvs_from_flat_inputtableentrynegative * S ((S (dst_index_from_flat_inputtable)) * dst_negative_scale_from_flat_inputtable) + (dst_negative_from_flat_inputtable))) /\ (exists ge_balance_positive_from_flat_inputtableentryvalue ge_balance_negative_from_flat_inputtableentryvalue. (((((dst_value_from_flat_inputtable) = 2 * (ge_balance_positive_from_flat_inputtableentryvalue) /\ (ge_balance_negative_from_flat_inputtableentryvalue) = 0) \/ exists ge_signed_half_from_flat_inputtableentryvaluedecode. (((dst_value_from_flat_inputtable) = 2 * ge_signed_half_from_flat_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_inputtableentryvalue) = 0) /\ (ge_balance_negative_from_flat_inputtableentryvalue) = S ge_signed_half_from_flat_inputtableentryvaluedecode))) /\ ((dst_positive_from_flat_inputtable) + ge_balance_negative_from_flat_inputtableentryvalue = (dst_negative_from_flat_inputtable) + ge_balance_positive_from_flat_inputtableentryvalue))))))))) /\ (forall scp_flat_index_from_flat_input scp_flat_value_from_flat_input. (exists pvs_le_gap_from_flat_inputbound. pvs_le_gap_from_flat_inputbound + (scp_flat_index_from_flat_input) = (m*n)) -> (exists dst_positive_code_from_flat_inputentry dst_positive_scale_from_flat_inputentry dst_negative_code_from_flat_inputentry dst_negative_scale_from_flat_inputentry dst_positive_from_flat_inputentry dst_negative_from_flat_inputentry. (((T) = (((((dst_positive_code_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry)) * S ((dst_positive_code_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry)) + ((dst_positive_scale_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry))) + (((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) * S ((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) + ((dst_negative_scale_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)))) * S ((((dst_positive_code_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry)) * S ((dst_positive_code_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry)) + ((dst_positive_scale_from_flat_inputentry) + (dst_positive_scale_from_flat_inputentry))) + (((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) * S ((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) + ((dst_negative_scale_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)))) + ((((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) * S ((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) + ((dst_negative_scale_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry))) + (((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) * S ((dst_negative_code_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)) + ((dst_negative_scale_from_flat_inputentry) + (dst_negative_scale_from_flat_inputentry)))))) /\ (((((exists ff_h_pvs_from_flat_inputentrypositive. ff_h_pvs_from_flat_inputentrypositive + S (dst_positive_from_flat_inputentry) = S ((S (scp_flat_index_from_flat_input)) * dst_positive_scale_from_flat_inputentry)) /\ exists ff_q_pvs_from_flat_inputentrypositive. dst_positive_code_from_flat_inputentry = ff_q_pvs_from_flat_inputentrypositive * S ((S (scp_flat_index_from_flat_input)) * dst_positive_scale_from_flat_inputentry) + (dst_positive_from_flat_inputentry))) /\ (((((exists ff_h_pvs_from_flat_inputentrynegative. ff_h_pvs_from_flat_inputentrynegative + S (dst_negative_from_flat_inputentry) = S ((S (scp_flat_index_from_flat_input)) * dst_negative_scale_from_flat_inputentry)) /\ exists ff_q_pvs_from_flat_inputentrynegative. dst_negative_code_from_flat_inputentry = ff_q_pvs_from_flat_inputentrynegative * S ((S (scp_flat_index_from_flat_input)) * dst_negative_scale_from_flat_inputentry) + (dst_negative_from_flat_inputentry))) /\ (exists ge_balance_positive_from_flat_inputentryvalue ge_balance_negative_from_flat_inputentryvalue. (((((scp_flat_value_from_flat_input) = 2 * (ge_balance_positive_from_flat_inputentryvalue) /\ (ge_balance_negative_from_flat_inputentryvalue) = 0) \/ exists ge_signed_half_from_flat_inputentryvaluedecode. (((scp_flat_value_from_flat_input) = 2 * ge_signed_half_from_flat_inputentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_inputentryvalue) = 0) /\ (ge_balance_negative_from_flat_inputentryvalue) = S ge_signed_half_from_flat_inputentryvaluedecode))) /\ ((dst_positive_from_flat_inputentry) + ge_balance_negative_from_flat_inputentryvalue = (dst_negative_from_flat_inputentry) + ge_balance_positive_from_flat_inputentryvalue))))))))) -> (exists scp_flat_row_from_flat_inputproduct scp_flat_column_from_flat_inputproduct scp_flat_first_from_flat_inputproduct scp_flat_second_from_flat_inputproduct. (((scp_flat_index_from_flat_input)=((n)*(scp_flat_row_from_flat_inputproduct)+(scp_flat_column_from_flat_inputproduct))) /\ (((exists pvs_gap_from_flat_inputproductremainder. pvs_gap_from_flat_inputproductremainder + S (scp_flat_column_from_flat_inputproduct) = (n)) /\ (((exists dst_positive_code_from_flat_inputproductF dst_positive_scale_from_flat_inputproductF dst_negative_code_from_flat_inputproductF dst_negative_scale_from_flat_inputproductF dst_positive_from_flat_inputproductF dst_negative_from_flat_inputproductF. (((F) = (((((dst_positive_code_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF)) * S ((dst_positive_code_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF)) + ((dst_positive_scale_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF))) + (((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) * S ((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) + ((dst_negative_scale_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)))) * S ((((dst_positive_code_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF)) * S ((dst_positive_code_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF)) + ((dst_positive_scale_from_flat_inputproductF) + (dst_positive_scale_from_flat_inputproductF))) + (((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) * S ((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) + ((dst_negative_scale_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)))) + ((((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) * S ((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) + ((dst_negative_scale_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF))) + (((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) * S ((dst_negative_code_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)) + ((dst_negative_scale_from_flat_inputproductF) + (dst_negative_scale_from_flat_inputproductF)))))) /\ (((((exists ff_h_pvs_from_flat_inputproductFpositive. ff_h_pvs_from_flat_inputproductFpositive + S (dst_positive_from_flat_inputproductF) = S ((S (scp_flat_row_from_flat_inputproduct)) * dst_positive_scale_from_flat_inputproductF)) /\ exists ff_q_pvs_from_flat_inputproductFpositive. dst_positive_code_from_flat_inputproductF = ff_q_pvs_from_flat_inputproductFpositive * S ((S (scp_flat_row_from_flat_inputproduct)) * dst_positive_scale_from_flat_inputproductF) + (dst_positive_from_flat_inputproductF))) /\ (((((exists ff_h_pvs_from_flat_inputproductFnegative. ff_h_pvs_from_flat_inputproductFnegative + S (dst_negative_from_flat_inputproductF) = S ((S (scp_flat_row_from_flat_inputproduct)) * dst_negative_scale_from_flat_inputproductF)) /\ exists ff_q_pvs_from_flat_inputproductFnegative. dst_negative_code_from_flat_inputproductF = ff_q_pvs_from_flat_inputproductFnegative * S ((S (scp_flat_row_from_flat_inputproduct)) * dst_negative_scale_from_flat_inputproductF) + (dst_negative_from_flat_inputproductF))) /\ (exists ge_balance_positive_from_flat_inputproductFvalue ge_balance_negative_from_flat_inputproductFvalue. (((((scp_flat_first_from_flat_inputproduct) = 2 * (ge_balance_positive_from_flat_inputproductFvalue) /\ (ge_balance_negative_from_flat_inputproductFvalue) = 0) \/ exists ge_signed_half_from_flat_inputproductFvaluedecode. (((scp_flat_first_from_flat_inputproduct) = 2 * ge_signed_half_from_flat_inputproductFvaluedecode + 1 /\ (ge_balance_positive_from_flat_inputproductFvalue) = 0) /\ (ge_balance_negative_from_flat_inputproductFvalue) = S ge_signed_half_from_flat_inputproductFvaluedecode))) /\ ((dst_positive_from_flat_inputproductF) + ge_balance_negative_from_flat_inputproductFvalue = (dst_negative_from_flat_inputproductF) + ge_balance_positive_from_flat_inputproductFvalue))))))))) /\ (((exists dst_positive_code_from_flat_inputproductG dst_positive_scale_from_flat_inputproductG dst_negative_code_from_flat_inputproductG dst_negative_scale_from_flat_inputproductG dst_positive_from_flat_inputproductG dst_negative_from_flat_inputproductG. (((G) = (((((dst_positive_code_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG)) * S ((dst_positive_code_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG)) + ((dst_positive_scale_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG))) + (((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) * S ((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) + ((dst_negative_scale_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)))) * S ((((dst_positive_code_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG)) * S ((dst_positive_code_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG)) + ((dst_positive_scale_from_flat_inputproductG) + (dst_positive_scale_from_flat_inputproductG))) + (((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) * S ((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) + ((dst_negative_scale_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)))) + ((((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) * S ((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) + ((dst_negative_scale_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG))) + (((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) * S ((dst_negative_code_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)) + ((dst_negative_scale_from_flat_inputproductG) + (dst_negative_scale_from_flat_inputproductG)))))) /\ (((((exists ff_h_pvs_from_flat_inputproductGpositive. ff_h_pvs_from_flat_inputproductGpositive + S (dst_positive_from_flat_inputproductG) = S ((S (scp_flat_column_from_flat_inputproduct)) * dst_positive_scale_from_flat_inputproductG)) /\ exists ff_q_pvs_from_flat_inputproductGpositive. dst_positive_code_from_flat_inputproductG = ff_q_pvs_from_flat_inputproductGpositive * S ((S (scp_flat_column_from_flat_inputproduct)) * dst_positive_scale_from_flat_inputproductG) + (dst_positive_from_flat_inputproductG))) /\ (((((exists ff_h_pvs_from_flat_inputproductGnegative. ff_h_pvs_from_flat_inputproductGnegative + S (dst_negative_from_flat_inputproductG) = S ((S (scp_flat_column_from_flat_inputproduct)) * dst_negative_scale_from_flat_inputproductG)) /\ exists ff_q_pvs_from_flat_inputproductGnegative. dst_negative_code_from_flat_inputproductG = ff_q_pvs_from_flat_inputproductGnegative * S ((S (scp_flat_column_from_flat_inputproduct)) * dst_negative_scale_from_flat_inputproductG) + (dst_negative_from_flat_inputproductG))) /\ (exists ge_balance_positive_from_flat_inputproductGvalue ge_balance_negative_from_flat_inputproductGvalue. (((((scp_flat_second_from_flat_inputproduct) = 2 * (ge_balance_positive_from_flat_inputproductGvalue) /\ (ge_balance_negative_from_flat_inputproductGvalue) = 0) \/ exists ge_signed_half_from_flat_inputproductGvaluedecode. (((scp_flat_second_from_flat_inputproduct) = 2 * ge_signed_half_from_flat_inputproductGvaluedecode + 1 /\ (ge_balance_positive_from_flat_inputproductGvalue) = 0) /\ (ge_balance_negative_from_flat_inputproductGvalue) = S ge_signed_half_from_flat_inputproductGvaluedecode))) /\ ((dst_positive_from_flat_inputproductG) + ge_balance_negative_from_flat_inputproductGvalue = (dst_negative_from_flat_inputproductG) + ge_balance_positive_from_flat_inputproductGvalue))))))))) /\ (exists sto_ap_from_flat_inputproductvalue sto_an_from_flat_inputproductvalue sto_bp_from_flat_inputproductvalue sto_bn_from_flat_inputproductvalue sto_cp_from_flat_inputproductvalue sto_cn_from_flat_inputproductvalue. (((((scp_flat_first_from_flat_inputproduct) = 2 * (sto_ap_from_flat_inputproductvalue) /\ (sto_an_from_flat_inputproductvalue) = 0) \/ exists ge_signed_half_from_flat_inputproductvalueleft. (((scp_flat_first_from_flat_inputproduct) = 2 * ge_signed_half_from_flat_inputproductvalueleft + 1 /\ (sto_ap_from_flat_inputproductvalue) = 0) /\ (sto_an_from_flat_inputproductvalue) = S ge_signed_half_from_flat_inputproductvalueleft))) /\ ((((((scp_flat_second_from_flat_inputproduct) = 2 * (sto_bp_from_flat_inputproductvalue) /\ (sto_bn_from_flat_inputproductvalue) = 0) \/ exists ge_signed_half_from_flat_inputproductvalueright. (((scp_flat_second_from_flat_inputproduct) = 2 * ge_signed_half_from_flat_inputproductvalueright + 1 /\ (sto_bp_from_flat_inputproductvalue) = 0) /\ (sto_bn_from_flat_inputproductvalue) = S ge_signed_half_from_flat_inputproductvalueright))) /\ ((((((scp_flat_value_from_flat_input) = 2 * (sto_cp_from_flat_inputproductvalue) /\ (sto_cn_from_flat_inputproductvalue) = 0) \/ exists ge_signed_half_from_flat_inputproductvalueoutput. (((scp_flat_value_from_flat_input) = 2 * ge_signed_half_from_flat_inputproductvalueoutput + 1 /\ (sto_cp_from_flat_inputproductvalue) = 0) /\ (sto_cn_from_flat_inputproductvalue) = S ge_signed_half_from_flat_inputproductvalueoutput))) /\ ((sto_ap_from_flat_inputproductvalue * sto_bp_from_flat_inputproductvalue + sto_an_from_flat_inputproductvalue * sto_bn_from_flat_inputproductvalue) + sto_cn_from_flat_inputproductvalue = (sto_ap_from_flat_inputproductvalue * sto_bn_from_flat_inputproductvalue + sto_an_from_flat_inputproductvalue * sto_bp_from_flat_inputproductvalue) + sto_cp_from_flat_inputproductvalue)))))))))))))))))) -> (((exists dst_positive_code_from_flat_resultF dst_positive_scale_from_flat_resultF dst_negative_code_from_flat_resultF dst_negative_scale_from_flat_resultF. (((F) = (((((dst_positive_code_from_flat_resultF) + (dst_positive_scale_from_flat_resultF)) * S ((dst_positive_code_from_flat_resultF) + (dst_positive_scale_from_flat_resultF)) + ((dst_positive_scale_from_flat_resultF) + (dst_positive_scale_from_flat_resultF))) + (((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) * S ((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) + ((dst_negative_scale_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)))) * S ((((dst_positive_code_from_flat_resultF) + (dst_positive_scale_from_flat_resultF)) * S ((dst_positive_code_from_flat_resultF) + (dst_positive_scale_from_flat_resultF)) + ((dst_positive_scale_from_flat_resultF) + (dst_positive_scale_from_flat_resultF))) + (((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) * S ((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) + ((dst_negative_scale_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)))) + ((((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) * S ((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) + ((dst_negative_scale_from_flat_resultF) + (dst_negative_scale_from_flat_resultF))) + (((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) * S ((dst_negative_code_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)) + ((dst_negative_scale_from_flat_resultF) + (dst_negative_scale_from_flat_resultF)))))) /\ (forall dst_index_from_flat_resultF. (exists pvs_le_gap_from_flat_resultFdomain. pvs_le_gap_from_flat_resultFdomain + (dst_index_from_flat_resultF) = (0)) -> exists dst_positive_from_flat_resultF dst_negative_from_flat_resultF dst_value_from_flat_resultF. ((((exists ff_h_pvs_from_flat_resultFentrypositive. ff_h_pvs_from_flat_resultFentrypositive + S (dst_positive_from_flat_resultF) = S ((S (dst_index_from_flat_resultF)) * dst_positive_scale_from_flat_resultF)) /\ exists ff_q_pvs_from_flat_resultFentrypositive. dst_positive_code_from_flat_resultF = ff_q_pvs_from_flat_resultFentrypositive * S ((S (dst_index_from_flat_resultF)) * dst_positive_scale_from_flat_resultF) + (dst_positive_from_flat_resultF))) /\ (((((exists ff_h_pvs_from_flat_resultFentrynegative. ff_h_pvs_from_flat_resultFentrynegative + S (dst_negative_from_flat_resultF) = S ((S (dst_index_from_flat_resultF)) * dst_negative_scale_from_flat_resultF)) /\ exists ff_q_pvs_from_flat_resultFentrynegative. dst_negative_code_from_flat_resultF = ff_q_pvs_from_flat_resultFentrynegative * S ((S (dst_index_from_flat_resultF)) * dst_negative_scale_from_flat_resultF) + (dst_negative_from_flat_resultF))) /\ (exists ge_balance_positive_from_flat_resultFentryvalue ge_balance_negative_from_flat_resultFentryvalue. (((((dst_value_from_flat_resultF) = 2 * (ge_balance_positive_from_flat_resultFentryvalue) /\ (ge_balance_negative_from_flat_resultFentryvalue) = 0) \/ exists ge_signed_half_from_flat_resultFentryvaluedecode. (((dst_value_from_flat_resultF) = 2 * ge_signed_half_from_flat_resultFentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultFentryvalue) = 0) /\ (ge_balance_negative_from_flat_resultFentryvalue) = S ge_signed_half_from_flat_resultFentryvaluedecode))) /\ ((dst_positive_from_flat_resultF) + ge_balance_negative_from_flat_resultFentryvalue = (dst_negative_from_flat_resultF) + ge_balance_positive_from_flat_resultFentryvalue))))))))) /\ (((exists dst_positive_code_from_flat_resultG dst_positive_scale_from_flat_resultG dst_negative_code_from_flat_resultG dst_negative_scale_from_flat_resultG. (((G) = (((((dst_positive_code_from_flat_resultG) + (dst_positive_scale_from_flat_resultG)) * S ((dst_positive_code_from_flat_resultG) + (dst_positive_scale_from_flat_resultG)) + ((dst_positive_scale_from_flat_resultG) + (dst_positive_scale_from_flat_resultG))) + (((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) * S ((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) + ((dst_negative_scale_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)))) * S ((((dst_positive_code_from_flat_resultG) + (dst_positive_scale_from_flat_resultG)) * S ((dst_positive_code_from_flat_resultG) + (dst_positive_scale_from_flat_resultG)) + ((dst_positive_scale_from_flat_resultG) + (dst_positive_scale_from_flat_resultG))) + (((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) * S ((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) + ((dst_negative_scale_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)))) + ((((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) * S ((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) + ((dst_negative_scale_from_flat_resultG) + (dst_negative_scale_from_flat_resultG))) + (((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) * S ((dst_negative_code_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)) + ((dst_negative_scale_from_flat_resultG) + (dst_negative_scale_from_flat_resultG)))))) /\ (forall dst_index_from_flat_resultG. (exists pvs_le_gap_from_flat_resultGdomain. pvs_le_gap_from_flat_resultGdomain + (dst_index_from_flat_resultG) = (0)) -> exists dst_positive_from_flat_resultG dst_negative_from_flat_resultG dst_value_from_flat_resultG. ((((exists ff_h_pvs_from_flat_resultGentrypositive. ff_h_pvs_from_flat_resultGentrypositive + S (dst_positive_from_flat_resultG) = S ((S (dst_index_from_flat_resultG)) * dst_positive_scale_from_flat_resultG)) /\ exists ff_q_pvs_from_flat_resultGentrypositive. dst_positive_code_from_flat_resultG = ff_q_pvs_from_flat_resultGentrypositive * S ((S (dst_index_from_flat_resultG)) * dst_positive_scale_from_flat_resultG) + (dst_positive_from_flat_resultG))) /\ (((((exists ff_h_pvs_from_flat_resultGentrynegative. ff_h_pvs_from_flat_resultGentrynegative + S (dst_negative_from_flat_resultG) = S ((S (dst_index_from_flat_resultG)) * dst_negative_scale_from_flat_resultG)) /\ exists ff_q_pvs_from_flat_resultGentrynegative. dst_negative_code_from_flat_resultG = ff_q_pvs_from_flat_resultGentrynegative * S ((S (dst_index_from_flat_resultG)) * dst_negative_scale_from_flat_resultG) + (dst_negative_from_flat_resultG))) /\ (exists ge_balance_positive_from_flat_resultGentryvalue ge_balance_negative_from_flat_resultGentryvalue. (((((dst_value_from_flat_resultG) = 2 * (ge_balance_positive_from_flat_resultGentryvalue) /\ (ge_balance_negative_from_flat_resultGentryvalue) = 0) \/ exists ge_signed_half_from_flat_resultGentryvaluedecode. (((dst_value_from_flat_resultG) = 2 * ge_signed_half_from_flat_resultGentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultGentryvalue) = 0) /\ (ge_balance_negative_from_flat_resultGentryvalue) = S ge_signed_half_from_flat_resultGentryvaluedecode))) /\ ((dst_positive_from_flat_resultG) + ge_balance_negative_from_flat_resultGentryvalue = (dst_negative_from_flat_resultG) + ge_balance_positive_from_flat_resultGentryvalue))))))))) /\ (((exists dst_positive_code_from_flat_resultT dst_positive_scale_from_flat_resultT dst_negative_code_from_flat_resultT dst_negative_scale_from_flat_resultT. (((T) = (((((dst_positive_code_from_flat_resultT) + (dst_positive_scale_from_flat_resultT)) * S ((dst_positive_code_from_flat_resultT) + (dst_positive_scale_from_flat_resultT)) + ((dst_positive_scale_from_flat_resultT) + (dst_positive_scale_from_flat_resultT))) + (((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) * S ((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) + ((dst_negative_scale_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)))) * S ((((dst_positive_code_from_flat_resultT) + (dst_positive_scale_from_flat_resultT)) * S ((dst_positive_code_from_flat_resultT) + (dst_positive_scale_from_flat_resultT)) + ((dst_positive_scale_from_flat_resultT) + (dst_positive_scale_from_flat_resultT))) + (((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) * S ((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) + ((dst_negative_scale_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)))) + ((((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) * S ((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) + ((dst_negative_scale_from_flat_resultT) + (dst_negative_scale_from_flat_resultT))) + (((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) * S ((dst_negative_code_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)) + ((dst_negative_scale_from_flat_resultT) + (dst_negative_scale_from_flat_resultT)))))) /\ (forall dst_index_from_flat_resultT. (exists pvs_le_gap_from_flat_resultTdomain. pvs_le_gap_from_flat_resultTdomain + (dst_index_from_flat_resultT) = ((m)*(n))) -> exists dst_positive_from_flat_resultT dst_negative_from_flat_resultT dst_value_from_flat_resultT. ((((exists ff_h_pvs_from_flat_resultTentrypositive. ff_h_pvs_from_flat_resultTentrypositive + S (dst_positive_from_flat_resultT) = S ((S (dst_index_from_flat_resultT)) * dst_positive_scale_from_flat_resultT)) /\ exists ff_q_pvs_from_flat_resultTentrypositive. dst_positive_code_from_flat_resultT = ff_q_pvs_from_flat_resultTentrypositive * S ((S (dst_index_from_flat_resultT)) * dst_positive_scale_from_flat_resultT) + (dst_positive_from_flat_resultT))) /\ (((((exists ff_h_pvs_from_flat_resultTentrynegative. ff_h_pvs_from_flat_resultTentrynegative + S (dst_negative_from_flat_resultT) = S ((S (dst_index_from_flat_resultT)) * dst_negative_scale_from_flat_resultT)) /\ exists ff_q_pvs_from_flat_resultTentrynegative. dst_negative_code_from_flat_resultT = ff_q_pvs_from_flat_resultTentrynegative * S ((S (dst_index_from_flat_resultT)) * dst_negative_scale_from_flat_resultT) + (dst_negative_from_flat_resultT))) /\ (exists ge_balance_positive_from_flat_resultTentryvalue ge_balance_negative_from_flat_resultTentryvalue. (((((dst_value_from_flat_resultT) = 2 * (ge_balance_positive_from_flat_resultTentryvalue) /\ (ge_balance_negative_from_flat_resultTentryvalue) = 0) \/ exists ge_signed_half_from_flat_resultTentryvaluedecode. (((dst_value_from_flat_resultT) = 2 * ge_signed_half_from_flat_resultTentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultTentryvalue) = 0) /\ (ge_balance_negative_from_flat_resultTentryvalue) = S ge_signed_half_from_flat_resultTentryvaluedecode))) /\ ((dst_positive_from_flat_resultT) + ge_balance_negative_from_flat_resultTentryvalue = (dst_negative_from_flat_resultT) + ge_balance_positive_from_flat_resultTentryvalue))))))))) /\ (forall scp_row_from_flat_result scp_column_from_flat_result scp_first_from_flat_result scp_second_from_flat_result scp_value_from_flat_result. (exists pvs_gap_from_flat_resultrows. pvs_gap_from_flat_resultrows + S (scp_row_from_flat_result) = (m)) -> (exists pvs_gap_from_flat_resultcolumns. pvs_gap_from_flat_resultcolumns + S (scp_column_from_flat_result) = (n)) -> (exists dst_positive_code_from_flat_resultfirst dst_positive_scale_from_flat_resultfirst dst_negative_code_from_flat_resultfirst dst_negative_scale_from_flat_resultfirst dst_positive_from_flat_resultfirst dst_negative_from_flat_resultfirst. (((F) = (((((dst_positive_code_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst)) * S ((dst_positive_code_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst)) + ((dst_positive_scale_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst))) + (((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) * S ((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) + ((dst_negative_scale_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)))) * S ((((dst_positive_code_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst)) * S ((dst_positive_code_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst)) + ((dst_positive_scale_from_flat_resultfirst) + (dst_positive_scale_from_flat_resultfirst))) + (((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) * S ((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) + ((dst_negative_scale_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)))) + ((((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) * S ((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) + ((dst_negative_scale_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst))) + (((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) * S ((dst_negative_code_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)) + ((dst_negative_scale_from_flat_resultfirst) + (dst_negative_scale_from_flat_resultfirst)))))) /\ (((((exists ff_h_pvs_from_flat_resultfirstpositive. ff_h_pvs_from_flat_resultfirstpositive + S (dst_positive_from_flat_resultfirst) = S ((S (scp_row_from_flat_result)) * dst_positive_scale_from_flat_resultfirst)) /\ exists ff_q_pvs_from_flat_resultfirstpositive. dst_positive_code_from_flat_resultfirst = ff_q_pvs_from_flat_resultfirstpositive * S ((S (scp_row_from_flat_result)) * dst_positive_scale_from_flat_resultfirst) + (dst_positive_from_flat_resultfirst))) /\ (((((exists ff_h_pvs_from_flat_resultfirstnegative. ff_h_pvs_from_flat_resultfirstnegative + S (dst_negative_from_flat_resultfirst) = S ((S (scp_row_from_flat_result)) * dst_negative_scale_from_flat_resultfirst)) /\ exists ff_q_pvs_from_flat_resultfirstnegative. dst_negative_code_from_flat_resultfirst = ff_q_pvs_from_flat_resultfirstnegative * S ((S (scp_row_from_flat_result)) * dst_negative_scale_from_flat_resultfirst) + (dst_negative_from_flat_resultfirst))) /\ (exists ge_balance_positive_from_flat_resultfirstvalue ge_balance_negative_from_flat_resultfirstvalue. (((((scp_first_from_flat_result) = 2 * (ge_balance_positive_from_flat_resultfirstvalue) /\ (ge_balance_negative_from_flat_resultfirstvalue) = 0) \/ exists ge_signed_half_from_flat_resultfirstvaluedecode. (((scp_first_from_flat_result) = 2 * ge_signed_half_from_flat_resultfirstvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultfirstvalue) = 0) /\ (ge_balance_negative_from_flat_resultfirstvalue) = S ge_signed_half_from_flat_resultfirstvaluedecode))) /\ ((dst_positive_from_flat_resultfirst) + ge_balance_negative_from_flat_resultfirstvalue = (dst_negative_from_flat_resultfirst) + ge_balance_positive_from_flat_resultfirstvalue))))))))) -> (exists dst_positive_code_from_flat_resultsecond dst_positive_scale_from_flat_resultsecond dst_negative_code_from_flat_resultsecond dst_negative_scale_from_flat_resultsecond dst_positive_from_flat_resultsecond dst_negative_from_flat_resultsecond. (((G) = (((((dst_positive_code_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond)) * S ((dst_positive_code_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond)) + ((dst_positive_scale_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond))) + (((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) * S ((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) + ((dst_negative_scale_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)))) * S ((((dst_positive_code_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond)) * S ((dst_positive_code_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond)) + ((dst_positive_scale_from_flat_resultsecond) + (dst_positive_scale_from_flat_resultsecond))) + (((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) * S ((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) + ((dst_negative_scale_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)))) + ((((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) * S ((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) + ((dst_negative_scale_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond))) + (((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) * S ((dst_negative_code_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)) + ((dst_negative_scale_from_flat_resultsecond) + (dst_negative_scale_from_flat_resultsecond)))))) /\ (((((exists ff_h_pvs_from_flat_resultsecondpositive. ff_h_pvs_from_flat_resultsecondpositive + S (dst_positive_from_flat_resultsecond) = S ((S (scp_column_from_flat_result)) * dst_positive_scale_from_flat_resultsecond)) /\ exists ff_q_pvs_from_flat_resultsecondpositive. dst_positive_code_from_flat_resultsecond = ff_q_pvs_from_flat_resultsecondpositive * S ((S (scp_column_from_flat_result)) * dst_positive_scale_from_flat_resultsecond) + (dst_positive_from_flat_resultsecond))) /\ (((((exists ff_h_pvs_from_flat_resultsecondnegative. ff_h_pvs_from_flat_resultsecondnegative + S (dst_negative_from_flat_resultsecond) = S ((S (scp_column_from_flat_result)) * dst_negative_scale_from_flat_resultsecond)) /\ exists ff_q_pvs_from_flat_resultsecondnegative. dst_negative_code_from_flat_resultsecond = ff_q_pvs_from_flat_resultsecondnegative * S ((S (scp_column_from_flat_result)) * dst_negative_scale_from_flat_resultsecond) + (dst_negative_from_flat_resultsecond))) /\ (exists ge_balance_positive_from_flat_resultsecondvalue ge_balance_negative_from_flat_resultsecondvalue. (((((scp_second_from_flat_result) = 2 * (ge_balance_positive_from_flat_resultsecondvalue) /\ (ge_balance_negative_from_flat_resultsecondvalue) = 0) \/ exists ge_signed_half_from_flat_resultsecondvaluedecode. (((scp_second_from_flat_result) = 2 * ge_signed_half_from_flat_resultsecondvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultsecondvalue) = 0) /\ (ge_balance_negative_from_flat_resultsecondvalue) = S ge_signed_half_from_flat_resultsecondvaluedecode))) /\ ((dst_positive_from_flat_resultsecond) + ge_balance_negative_from_flat_resultsecondvalue = (dst_negative_from_flat_resultsecond) + ge_balance_positive_from_flat_resultsecondvalue))))))))) -> (exists dst_positive_code_from_flat_resultentry dst_positive_scale_from_flat_resultentry dst_negative_code_from_flat_resultentry dst_negative_scale_from_flat_resultentry dst_positive_from_flat_resultentry dst_negative_from_flat_resultentry. (((T) = (((((dst_positive_code_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry)) * S ((dst_positive_code_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry)) + ((dst_positive_scale_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry))) + (((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) * S ((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) + ((dst_negative_scale_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)))) * S ((((dst_positive_code_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry)) * S ((dst_positive_code_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry)) + ((dst_positive_scale_from_flat_resultentry) + (dst_positive_scale_from_flat_resultentry))) + (((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) * S ((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) + ((dst_negative_scale_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)))) + ((((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) * S ((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) + ((dst_negative_scale_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry))) + (((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) * S ((dst_negative_code_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)) + ((dst_negative_scale_from_flat_resultentry) + (dst_negative_scale_from_flat_resultentry)))))) /\ (((((exists ff_h_pvs_from_flat_resultentrypositive. ff_h_pvs_from_flat_resultentrypositive + S (dst_positive_from_flat_resultentry) = S ((S (((n)*(scp_row_from_flat_result)+(scp_column_from_flat_result)))) * dst_positive_scale_from_flat_resultentry)) /\ exists ff_q_pvs_from_flat_resultentrypositive. dst_positive_code_from_flat_resultentry = ff_q_pvs_from_flat_resultentrypositive * S ((S (((n)*(scp_row_from_flat_result)+(scp_column_from_flat_result)))) * dst_positive_scale_from_flat_resultentry) + (dst_positive_from_flat_resultentry))) /\ (((((exists ff_h_pvs_from_flat_resultentrynegative. ff_h_pvs_from_flat_resultentrynegative + S (dst_negative_from_flat_resultentry) = S ((S (((n)*(scp_row_from_flat_result)+(scp_column_from_flat_result)))) * dst_negative_scale_from_flat_resultentry)) /\ exists ff_q_pvs_from_flat_resultentrynegative. dst_negative_code_from_flat_resultentry = ff_q_pvs_from_flat_resultentrynegative * S ((S (((n)*(scp_row_from_flat_result)+(scp_column_from_flat_result)))) * dst_negative_scale_from_flat_resultentry) + (dst_negative_from_flat_resultentry))) /\ (exists ge_balance_positive_from_flat_resultentryvalue ge_balance_negative_from_flat_resultentryvalue. (((((scp_value_from_flat_result) = 2 * (ge_balance_positive_from_flat_resultentryvalue) /\ (ge_balance_negative_from_flat_resultentryvalue) = 0) \/ exists ge_signed_half_from_flat_resultentryvaluedecode. (((scp_value_from_flat_result) = 2 * ge_signed_half_from_flat_resultentryvaluedecode + 1 /\ (ge_balance_positive_from_flat_resultentryvalue) = 0) /\ (ge_balance_negative_from_flat_resultentryvalue) = S ge_signed_half_from_flat_resultentryvaluedecode))) /\ ((dst_positive_from_flat_resultentry) + ge_balance_negative_from_flat_resultentryvalue = (dst_negative_from_flat_resultentry) + ge_balance_positive_from_flat_resultentryvalue))))))))) -> (exists sto_ap_from_flat_resultmultiply sto_an_from_flat_resultmultiply sto_bp_from_flat_resultmultiply sto_bn_from_flat_resultmultiply sto_cp_from_flat_resultmultiply sto_cn_from_flat_resultmultiply. (((((scp_first_from_flat_result) = 2 * (sto_ap_from_flat_resultmultiply) /\ (sto_an_from_flat_resultmultiply) = 0) \/ exists ge_signed_half_from_flat_resultmultiplyleft. (((scp_first_from_flat_result) = 2 * ge_signed_half_from_flat_resultmultiplyleft + 1 /\ (sto_ap_from_flat_resultmultiply) = 0) /\ (sto_an_from_flat_resultmultiply) = S ge_signed_half_from_flat_resultmultiplyleft))) /\ ((((((scp_second_from_flat_result) = 2 * (sto_bp_from_flat_resultmultiply) /\ (sto_bn_from_flat_resultmultiply) = 0) \/ exists ge_signed_half_from_flat_resultmultiplyright. (((scp_second_from_flat_result) = 2 * ge_signed_half_from_flat_resultmultiplyright + 1 /\ (sto_bp_from_flat_resultmultiply) = 0) /\ (sto_bn_from_flat_resultmultiply) = S ge_signed_half_from_flat_resultmultiplyright))) /\ ((((((scp_value_from_flat_result) = 2 * (sto_cp_from_flat_resultmultiply) /\ (sto_cn_from_flat_resultmultiply) = 0) \/ exists ge_signed_half_from_flat_resultmultiplyoutput. (((scp_value_from_flat_result) = 2 * ge_signed_half_from_flat_resultmultiplyoutput + 1 /\ (sto_cp_from_flat_resultmultiply) = 0) /\ (sto_cn_from_flat_resultmultiply) = S ge_signed_half_from_flat_resultmultiplyoutput))) /\ ((sto_ap_from_flat_resultmultiply * sto_bp_from_flat_resultmultiply + sto_an_from_flat_resultmultiply * sto_bn_from_flat_resultmultiply) + sto_cn_from_flat_resultmultiply = (sto_ap_from_flat_resultmultiply * sto_bn_from_flat_resultmultiply + sto_an_from_flat_resultmultiply * sto_bp_from_flat_resultmultiply) + sto_cp_from_flat_resultmultiply))))))))))))))