signed_cartesian_product_sums_exists

Exact expanded first-order arithmetic statement

forall F G m n. (exists dst_positive_code_values_source_F dst_positive_scale_values_source_F dst_negative_code_values_source_F dst_negative_scale_values_source_F. (((F) = (((((dst_positive_code_values_source_F) + (dst_positive_scale_values_source_F)) * S ((dst_positive_code_values_source_F) + (dst_positive_scale_values_source_F)) + ((dst_positive_scale_values_source_F) + (dst_positive_scale_values_source_F))) + (((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) * S ((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) + ((dst_negative_scale_values_source_F) + (dst_negative_scale_values_source_F)))) * S ((((dst_positive_code_values_source_F) + (dst_positive_scale_values_source_F)) * S ((dst_positive_code_values_source_F) + (dst_positive_scale_values_source_F)) + ((dst_positive_scale_values_source_F) + (dst_positive_scale_values_source_F))) + (((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) * S ((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) + ((dst_negative_scale_values_source_F) + (dst_negative_scale_values_source_F)))) + ((((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) * S ((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) + ((dst_negative_scale_values_source_F) + (dst_negative_scale_values_source_F))) + (((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) * S ((dst_negative_code_values_source_F) + (dst_negative_scale_values_source_F)) + ((dst_negative_scale_values_source_F) + (dst_negative_scale_values_source_F)))))) /\ (forall dst_index_values_source_F. (exists pvs_le_gap_values_source_Fdomain. pvs_le_gap_values_source_Fdomain + (dst_index_values_source_F) = (0)) -> exists dst_positive_values_source_F dst_negative_values_source_F dst_value_values_source_F. ((((exists ff_h_pvs_values_source_Fentrypositive. ff_h_pvs_values_source_Fentrypositive + S (dst_positive_values_source_F) = S ((S (dst_index_values_source_F)) * dst_positive_scale_values_source_F)) /\ exists ff_q_pvs_values_source_Fentrypositive. dst_positive_code_values_source_F = ff_q_pvs_values_source_Fentrypositive * S ((S (dst_index_values_source_F)) * dst_positive_scale_values_source_F) + (dst_positive_values_source_F))) /\ (((((exists ff_h_pvs_values_source_Fentrynegative. ff_h_pvs_values_source_Fentrynegative + S (dst_negative_values_source_F) = S ((S (dst_index_values_source_F)) * dst_negative_scale_values_source_F)) /\ exists ff_q_pvs_values_source_Fentrynegative. dst_negative_code_values_source_F = ff_q_pvs_values_source_Fentrynegative * S ((S (dst_index_values_source_F)) * dst_negative_scale_values_source_F) + (dst_negative_values_source_F))) /\ (exists ge_balance_positive_values_source_Fentryvalue ge_balance_negative_values_source_Fentryvalue. (((((dst_value_values_source_F) = 2 * (ge_balance_positive_values_source_Fentryvalue) /\ (ge_balance_negative_values_source_Fentryvalue) = 0) \/ exists ge_signed_half_values_source_Fentryvaluedecode. (((dst_value_values_source_F) = 2 * ge_signed_half_values_source_Fentryvaluedecode + 1 /\ (ge_balance_positive_values_source_Fentryvalue) = 0) /\ (ge_balance_negative_values_source_Fentryvalue) = S ge_signed_half_values_source_Fentryvaluedecode))) /\ ((dst_positive_values_source_F) + ge_balance_negative_values_source_Fentryvalue = (dst_negative_values_source_F) + ge_balance_positive_values_source_Fentryvalue))))))))) -> (exists dst_positive_code_values_source_G dst_positive_scale_values_source_G dst_negative_code_values_source_G dst_negative_scale_values_source_G. (((G) = (((((dst_positive_code_values_source_G) + (dst_positive_scale_values_source_G)) * S ((dst_positive_code_values_source_G) + (dst_positive_scale_values_source_G)) + ((dst_positive_scale_values_source_G) + (dst_positive_scale_values_source_G))) + (((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) * S ((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) + ((dst_negative_scale_values_source_G) + (dst_negative_scale_values_source_G)))) * S ((((dst_positive_code_values_source_G) + (dst_positive_scale_values_source_G)) * S ((dst_positive_code_values_source_G) + (dst_positive_scale_values_source_G)) + ((dst_positive_scale_values_source_G) + (dst_positive_scale_values_source_G))) + (((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) * S ((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) + ((dst_negative_scale_values_source_G) + (dst_negative_scale_values_source_G)))) + ((((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) * S ((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) + ((dst_negative_scale_values_source_G) + (dst_negative_scale_values_source_G))) + (((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) * S ((dst_negative_code_values_source_G) + (dst_negative_scale_values_source_G)) + ((dst_negative_scale_values_source_G) + (dst_negative_scale_values_source_G)))))) /\ (forall dst_index_values_source_G. (exists pvs_le_gap_values_source_Gdomain. pvs_le_gap_values_source_Gdomain + (dst_index_values_source_G) = (0)) -> exists dst_positive_values_source_G dst_negative_values_source_G dst_value_values_source_G. ((((exists ff_h_pvs_values_source_Gentrypositive. ff_h_pvs_values_source_Gentrypositive + S (dst_positive_values_source_G) = S ((S (dst_index_values_source_G)) * dst_positive_scale_values_source_G)) /\ exists ff_q_pvs_values_source_Gentrypositive. dst_positive_code_values_source_G = ff_q_pvs_values_source_Gentrypositive * S ((S (dst_index_values_source_G)) * dst_positive_scale_values_source_G) + (dst_positive_values_source_G))) /\ (((((exists ff_h_pvs_values_source_Gentrynegative. ff_h_pvs_values_source_Gentrynegative + S (dst_negative_values_source_G) = S ((S (dst_index_values_source_G)) * dst_negative_scale_values_source_G)) /\ exists ff_q_pvs_values_source_Gentrynegative. dst_negative_code_values_source_G = ff_q_pvs_values_source_Gentrynegative * S ((S (dst_index_values_source_G)) * dst_negative_scale_values_source_G) + (dst_negative_values_source_G))) /\ (exists ge_balance_positive_values_source_Gentryvalue ge_balance_negative_values_source_Gentryvalue. (((((dst_value_values_source_G) = 2 * (ge_balance_positive_values_source_Gentryvalue) /\ (ge_balance_negative_values_source_Gentryvalue) = 0) \/ exists ge_signed_half_values_source_Gentryvaluedecode. (((dst_value_values_source_G) = 2 * ge_signed_half_values_source_Gentryvaluedecode + 1 /\ (ge_balance_positive_values_source_Gentryvalue) = 0) /\ (ge_balance_negative_values_source_Gentryvalue) = S ge_signed_half_values_source_Gentryvaluedecode))) /\ ((dst_positive_values_source_G) + ge_balance_negative_values_source_Gentryvalue = (dst_negative_values_source_G) + ge_balance_positive_values_source_Gentryvalue))))))))) -> exists T a b c. ((((exists dst_positive_code_values_productF dst_positive_scale_values_productF dst_negative_code_values_productF dst_negative_scale_values_productF. (((F) = (((((dst_positive_code_values_productF) + (dst_positive_scale_values_productF)) * S ((dst_positive_code_values_productF) + (dst_positive_scale_values_productF)) + ((dst_positive_scale_values_productF) + (dst_positive_scale_values_productF))) + (((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) * S ((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) + ((dst_negative_scale_values_productF) + (dst_negative_scale_values_productF)))) * S ((((dst_positive_code_values_productF) + (dst_positive_scale_values_productF)) * S ((dst_positive_code_values_productF) + (dst_positive_scale_values_productF)) + ((dst_positive_scale_values_productF) + (dst_positive_scale_values_productF))) + (((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) * S ((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) + ((dst_negative_scale_values_productF) + (dst_negative_scale_values_productF)))) + ((((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) * S ((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) + ((dst_negative_scale_values_productF) + (dst_negative_scale_values_productF))) + (((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) * S ((dst_negative_code_values_productF) + (dst_negative_scale_values_productF)) + ((dst_negative_scale_values_productF) + (dst_negative_scale_values_productF)))))) /\ (forall dst_index_values_productF. (exists pvs_le_gap_values_productFdomain. pvs_le_gap_values_productFdomain + (dst_index_values_productF) = (0)) -> exists dst_positive_values_productF dst_negative_values_productF dst_value_values_productF. ((((exists ff_h_pvs_values_productFentrypositive. ff_h_pvs_values_productFentrypositive + S (dst_positive_values_productF) = S ((S (dst_index_values_productF)) * dst_positive_scale_values_productF)) /\ exists ff_q_pvs_values_productFentrypositive. dst_positive_code_values_productF = ff_q_pvs_values_productFentrypositive * S ((S (dst_index_values_productF)) * dst_positive_scale_values_productF) + (dst_positive_values_productF))) /\ (((((exists ff_h_pvs_values_productFentrynegative. ff_h_pvs_values_productFentrynegative + S (dst_negative_values_productF) = S ((S (dst_index_values_productF)) * dst_negative_scale_values_productF)) /\ exists ff_q_pvs_values_productFentrynegative. dst_negative_code_values_productF = ff_q_pvs_values_productFentrynegative * S ((S (dst_index_values_productF)) * dst_negative_scale_values_productF) + (dst_negative_values_productF))) /\ (exists ge_balance_positive_values_productFentryvalue ge_balance_negative_values_productFentryvalue. (((((dst_value_values_productF) = 2 * (ge_balance_positive_values_productFentryvalue) /\ (ge_balance_negative_values_productFentryvalue) = 0) \/ exists ge_signed_half_values_productFentryvaluedecode. (((dst_value_values_productF) = 2 * ge_signed_half_values_productFentryvaluedecode + 1 /\ (ge_balance_positive_values_productFentryvalue) = 0) /\ (ge_balance_negative_values_productFentryvalue) = S ge_signed_half_values_productFentryvaluedecode))) /\ ((dst_positive_values_productF) + ge_balance_negative_values_productFentryvalue = (dst_negative_values_productF) + ge_balance_positive_values_productFentryvalue))))))))) /\ (((exists dst_positive_code_values_productG dst_positive_scale_values_productG dst_negative_code_values_productG dst_negative_scale_values_productG. (((G) = (((((dst_positive_code_values_productG) + (dst_positive_scale_values_productG)) * S ((dst_positive_code_values_productG) + (dst_positive_scale_values_productG)) + ((dst_positive_scale_values_productG) + (dst_positive_scale_values_productG))) + (((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) * S ((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) + ((dst_negative_scale_values_productG) + (dst_negative_scale_values_productG)))) * S ((((dst_positive_code_values_productG) + (dst_positive_scale_values_productG)) * S ((dst_positive_code_values_productG) + (dst_positive_scale_values_productG)) + ((dst_positive_scale_values_productG) + (dst_positive_scale_values_productG))) + (((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) * S ((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) + ((dst_negative_scale_values_productG) + (dst_negative_scale_values_productG)))) + ((((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) * S ((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) + ((dst_negative_scale_values_productG) + (dst_negative_scale_values_productG))) + (((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) * S ((dst_negative_code_values_productG) + (dst_negative_scale_values_productG)) + ((dst_negative_scale_values_productG) + (dst_negative_scale_values_productG)))))) /\ (forall dst_index_values_productG. (exists pvs_le_gap_values_productGdomain. pvs_le_gap_values_productGdomain + (dst_index_values_productG) = (0)) -> exists dst_positive_values_productG dst_negative_values_productG dst_value_values_productG. ((((exists ff_h_pvs_values_productGentrypositive. ff_h_pvs_values_productGentrypositive + S (dst_positive_values_productG) = S ((S (dst_index_values_productG)) * dst_positive_scale_values_productG)) /\ exists ff_q_pvs_values_productGentrypositive. dst_positive_code_values_productG = ff_q_pvs_values_productGentrypositive * S ((S (dst_index_values_productG)) * dst_positive_scale_values_productG) + (dst_positive_values_productG))) /\ (((((exists ff_h_pvs_values_productGentrynegative. ff_h_pvs_values_productGentrynegative + S (dst_negative_values_productG) = S ((S (dst_index_values_productG)) * dst_negative_scale_values_productG)) /\ exists ff_q_pvs_values_productGentrynegative. dst_negative_code_values_productG = ff_q_pvs_values_productGentrynegative * S ((S (dst_index_values_productG)) * dst_negative_scale_values_productG) + (dst_negative_values_productG))) /\ (exists ge_balance_positive_values_productGentryvalue ge_balance_negative_values_productGentryvalue. (((((dst_value_values_productG) = 2 * (ge_balance_positive_values_productGentryvalue) /\ (ge_balance_negative_values_productGentryvalue) = 0) \/ exists ge_signed_half_values_productGentryvaluedecode. (((dst_value_values_productG) = 2 * ge_signed_half_values_productGentryvaluedecode + 1 /\ (ge_balance_positive_values_productGentryvalue) = 0) /\ (ge_balance_negative_values_productGentryvalue) = S ge_signed_half_values_productGentryvaluedecode))) /\ ((dst_positive_values_productG) + ge_balance_negative_values_productGentryvalue = (dst_negative_values_productG) + ge_balance_positive_values_productGentryvalue))))))))) /\ (((exists dst_positive_code_values_productT dst_positive_scale_values_productT dst_negative_code_values_productT dst_negative_scale_values_productT. (((T) = (((((dst_positive_code_values_productT) + (dst_positive_scale_values_productT)) * S ((dst_positive_code_values_productT) + (dst_positive_scale_values_productT)) + ((dst_positive_scale_values_productT) + (dst_positive_scale_values_productT))) + (((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) * S ((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) + ((dst_negative_scale_values_productT) + (dst_negative_scale_values_productT)))) * S ((((dst_positive_code_values_productT) + (dst_positive_scale_values_productT)) * S ((dst_positive_code_values_productT) + (dst_positive_scale_values_productT)) + ((dst_positive_scale_values_productT) + (dst_positive_scale_values_productT))) + (((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) * S ((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) + ((dst_negative_scale_values_productT) + (dst_negative_scale_values_productT)))) + ((((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) * S ((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) + ((dst_negative_scale_values_productT) + (dst_negative_scale_values_productT))) + (((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) * S ((dst_negative_code_values_productT) + (dst_negative_scale_values_productT)) + ((dst_negative_scale_values_productT) + (dst_negative_scale_values_productT)))))) /\ (forall dst_index_values_productT. (exists pvs_le_gap_values_productTdomain. pvs_le_gap_values_productTdomain + (dst_index_values_productT) = ((m)*(n))) -> exists dst_positive_values_productT dst_negative_values_productT dst_value_values_productT. ((((exists ff_h_pvs_values_productTentrypositive. ff_h_pvs_values_productTentrypositive + S (dst_positive_values_productT) = S ((S (dst_index_values_productT)) * dst_positive_scale_values_productT)) /\ exists ff_q_pvs_values_productTentrypositive. dst_positive_code_values_productT = ff_q_pvs_values_productTentrypositive * S ((S (dst_index_values_productT)) * dst_positive_scale_values_productT) + (dst_positive_values_productT))) /\ (((((exists ff_h_pvs_values_productTentrynegative. ff_h_pvs_values_productTentrynegative + S (dst_negative_values_productT) = S ((S (dst_index_values_productT)) * dst_negative_scale_values_productT)) /\ exists ff_q_pvs_values_productTentrynegative. dst_negative_code_values_productT = ff_q_pvs_values_productTentrynegative * S ((S (dst_index_values_productT)) * dst_negative_scale_values_productT) + (dst_negative_values_productT))) /\ (exists ge_balance_positive_values_productTentryvalue ge_balance_negative_values_productTentryvalue. (((((dst_value_values_productT) = 2 * (ge_balance_positive_values_productTentryvalue) /\ (ge_balance_negative_values_productTentryvalue) = 0) \/ exists ge_signed_half_values_productTentryvaluedecode. (((dst_value_values_productT) = 2 * ge_signed_half_values_productTentryvaluedecode + 1 /\ (ge_balance_positive_values_productTentryvalue) = 0) /\ (ge_balance_negative_values_productTentryvalue) = S ge_signed_half_values_productTentryvaluedecode))) /\ ((dst_positive_values_productT) + ge_balance_negative_values_productTentryvalue = (dst_negative_values_productT) + ge_balance_positive_values_productTentryvalue))))))))) /\ (forall scp_row_values_product scp_column_values_product scp_first_values_product scp_second_values_product scp_value_values_product. (exists pvs_gap_values_productrows. pvs_gap_values_productrows + S (scp_row_values_product) = (m)) -> (exists pvs_gap_values_productcolumns. pvs_gap_values_productcolumns + S (scp_column_values_product) = (n)) -> (exists dst_positive_code_values_productfirst dst_positive_scale_values_productfirst dst_negative_code_values_productfirst dst_negative_scale_values_productfirst dst_positive_values_productfirst dst_negative_values_productfirst. (((F) = (((((dst_positive_code_values_productfirst) + (dst_positive_scale_values_productfirst)) * S ((dst_positive_code_values_productfirst) + (dst_positive_scale_values_productfirst)) + ((dst_positive_scale_values_productfirst) + (dst_positive_scale_values_productfirst))) + (((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) * S ((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) + ((dst_negative_scale_values_productfirst) + (dst_negative_scale_values_productfirst)))) * S ((((dst_positive_code_values_productfirst) + (dst_positive_scale_values_productfirst)) * S ((dst_positive_code_values_productfirst) + (dst_positive_scale_values_productfirst)) + ((dst_positive_scale_values_productfirst) + (dst_positive_scale_values_productfirst))) + (((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) * S ((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) + ((dst_negative_scale_values_productfirst) + (dst_negative_scale_values_productfirst)))) + ((((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) * S ((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) + ((dst_negative_scale_values_productfirst) + (dst_negative_scale_values_productfirst))) + (((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) * S ((dst_negative_code_values_productfirst) + (dst_negative_scale_values_productfirst)) + ((dst_negative_scale_values_productfirst) + (dst_negative_scale_values_productfirst)))))) /\ (((((exists ff_h_pvs_values_productfirstpositive. ff_h_pvs_values_productfirstpositive + S (dst_positive_values_productfirst) = S ((S (scp_row_values_product)) * dst_positive_scale_values_productfirst)) /\ exists ff_q_pvs_values_productfirstpositive. dst_positive_code_values_productfirst = ff_q_pvs_values_productfirstpositive * S ((S (scp_row_values_product)) * dst_positive_scale_values_productfirst) + (dst_positive_values_productfirst))) /\ (((((exists ff_h_pvs_values_productfirstnegative. ff_h_pvs_values_productfirstnegative + S (dst_negative_values_productfirst) = S ((S (scp_row_values_product)) * dst_negative_scale_values_productfirst)) /\ exists ff_q_pvs_values_productfirstnegative. dst_negative_code_values_productfirst = ff_q_pvs_values_productfirstnegative * S ((S (scp_row_values_product)) * dst_negative_scale_values_productfirst) + (dst_negative_values_productfirst))) /\ (exists ge_balance_positive_values_productfirstvalue ge_balance_negative_values_productfirstvalue. (((((scp_first_values_product) = 2 * (ge_balance_positive_values_productfirstvalue) /\ (ge_balance_negative_values_productfirstvalue) = 0) \/ exists ge_signed_half_values_productfirstvaluedecode. (((scp_first_values_product) = 2 * ge_signed_half_values_productfirstvaluedecode + 1 /\ (ge_balance_positive_values_productfirstvalue) = 0) /\ (ge_balance_negative_values_productfirstvalue) = S ge_signed_half_values_productfirstvaluedecode))) /\ ((dst_positive_values_productfirst) + ge_balance_negative_values_productfirstvalue = (dst_negative_values_productfirst) + ge_balance_positive_values_productfirstvalue))))))))) -> (exists dst_positive_code_values_productsecond dst_positive_scale_values_productsecond dst_negative_code_values_productsecond dst_negative_scale_values_productsecond dst_positive_values_productsecond dst_negative_values_productsecond. (((G) = (((((dst_positive_code_values_productsecond) + (dst_positive_scale_values_productsecond)) * S ((dst_positive_code_values_productsecond) + (dst_positive_scale_values_productsecond)) + ((dst_positive_scale_values_productsecond) + (dst_positive_scale_values_productsecond))) + (((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) * S ((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) + ((dst_negative_scale_values_productsecond) + (dst_negative_scale_values_productsecond)))) * S ((((dst_positive_code_values_productsecond) + (dst_positive_scale_values_productsecond)) * S ((dst_positive_code_values_productsecond) + (dst_positive_scale_values_productsecond)) + ((dst_positive_scale_values_productsecond) + (dst_positive_scale_values_productsecond))) + (((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) * S ((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) + ((dst_negative_scale_values_productsecond) + (dst_negative_scale_values_productsecond)))) + ((((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) * S ((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) + ((dst_negative_scale_values_productsecond) + (dst_negative_scale_values_productsecond))) + (((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) * S ((dst_negative_code_values_productsecond) + (dst_negative_scale_values_productsecond)) + ((dst_negative_scale_values_productsecond) + (dst_negative_scale_values_productsecond)))))) /\ (((((exists ff_h_pvs_values_productsecondpositive. ff_h_pvs_values_productsecondpositive + S (dst_positive_values_productsecond) = S ((S (scp_column_values_product)) * dst_positive_scale_values_productsecond)) /\ exists ff_q_pvs_values_productsecondpositive. dst_positive_code_values_productsecond = ff_q_pvs_values_productsecondpositive * S ((S (scp_column_values_product)) * dst_positive_scale_values_productsecond) + (dst_positive_values_productsecond))) /\ (((((exists ff_h_pvs_values_productsecondnegative. ff_h_pvs_values_productsecondnegative + S (dst_negative_values_productsecond) = S ((S (scp_column_values_product)) * dst_negative_scale_values_productsecond)) /\ exists ff_q_pvs_values_productsecondnegative. dst_negative_code_values_productsecond = ff_q_pvs_values_productsecondnegative * S ((S (scp_column_values_product)) * dst_negative_scale_values_productsecond) + (dst_negative_values_productsecond))) /\ (exists ge_balance_positive_values_productsecondvalue ge_balance_negative_values_productsecondvalue. (((((scp_second_values_product) = 2 * (ge_balance_positive_values_productsecondvalue) /\ (ge_balance_negative_values_productsecondvalue) = 0) \/ exists ge_signed_half_values_productsecondvaluedecode. (((scp_second_values_product) = 2 * ge_signed_half_values_productsecondvaluedecode + 1 /\ (ge_balance_positive_values_productsecondvalue) = 0) /\ (ge_balance_negative_values_productsecondvalue) = S ge_signed_half_values_productsecondvaluedecode))) /\ ((dst_positive_values_productsecond) + ge_balance_negative_values_productsecondvalue = (dst_negative_values_productsecond) + ge_balance_positive_values_productsecondvalue))))))))) -> (exists dst_positive_code_values_productentry dst_positive_scale_values_productentry dst_negative_code_values_productentry dst_negative_scale_values_productentry dst_positive_values_productentry dst_negative_values_productentry. (((T) = (((((dst_positive_code_values_productentry) + (dst_positive_scale_values_productentry)) * S ((dst_positive_code_values_productentry) + (dst_positive_scale_values_productentry)) + ((dst_positive_scale_values_productentry) + (dst_positive_scale_values_productentry))) + (((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) * S ((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) + ((dst_negative_scale_values_productentry) + (dst_negative_scale_values_productentry)))) * S ((((dst_positive_code_values_productentry) + (dst_positive_scale_values_productentry)) * S ((dst_positive_code_values_productentry) + (dst_positive_scale_values_productentry)) + ((dst_positive_scale_values_productentry) + (dst_positive_scale_values_productentry))) + (((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) * S ((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) + ((dst_negative_scale_values_productentry) + (dst_negative_scale_values_productentry)))) + ((((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) * S ((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) + ((dst_negative_scale_values_productentry) + (dst_negative_scale_values_productentry))) + (((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) * S ((dst_negative_code_values_productentry) + (dst_negative_scale_values_productentry)) + ((dst_negative_scale_values_productentry) + (dst_negative_scale_values_productentry)))))) /\ (((((exists ff_h_pvs_values_productentrypositive. ff_h_pvs_values_productentrypositive + S (dst_positive_values_productentry) = S ((S (((n)*(scp_row_values_product)+(scp_column_values_product)))) * dst_positive_scale_values_productentry)) /\ exists ff_q_pvs_values_productentrypositive. dst_positive_code_values_productentry = ff_q_pvs_values_productentrypositive * S ((S (((n)*(scp_row_values_product)+(scp_column_values_product)))) * dst_positive_scale_values_productentry) + (dst_positive_values_productentry))) /\ (((((exists ff_h_pvs_values_productentrynegative. ff_h_pvs_values_productentrynegative + S (dst_negative_values_productentry) = S ((S (((n)*(scp_row_values_product)+(scp_column_values_product)))) * dst_negative_scale_values_productentry)) /\ exists ff_q_pvs_values_productentrynegative. dst_negative_code_values_productentry = ff_q_pvs_values_productentrynegative * S ((S (((n)*(scp_row_values_product)+(scp_column_values_product)))) * dst_negative_scale_values_productentry) + (dst_negative_values_productentry))) /\ (exists ge_balance_positive_values_productentryvalue ge_balance_negative_values_productentryvalue. (((((scp_value_values_product) = 2 * (ge_balance_positive_values_productentryvalue) /\ (ge_balance_negative_values_productentryvalue) = 0) \/ exists ge_signed_half_values_productentryvaluedecode. (((scp_value_values_product) = 2 * ge_signed_half_values_productentryvaluedecode + 1 /\ (ge_balance_positive_values_productentryvalue) = 0) /\ (ge_balance_negative_values_productentryvalue) = S ge_signed_half_values_productentryvaluedecode))) /\ ((dst_positive_values_productentry) + ge_balance_negative_values_productentryvalue = (dst_negative_values_productentry) + ge_balance_positive_values_productentryvalue))))))))) -> (exists sto_ap_values_productmultiply sto_an_values_productmultiply sto_bp_values_productmultiply sto_bn_values_productmultiply sto_cp_values_productmultiply sto_cn_values_productmultiply. (((((scp_first_values_product) = 2 * (sto_ap_values_productmultiply) /\ (sto_an_values_productmultiply) = 0) \/ exists ge_signed_half_values_productmultiplyleft. (((scp_first_values_product) = 2 * ge_signed_half_values_productmultiplyleft + 1 /\ (sto_ap_values_productmultiply) = 0) /\ (sto_an_values_productmultiply) = S ge_signed_half_values_productmultiplyleft))) /\ ((((((scp_second_values_product) = 2 * (sto_bp_values_productmultiply) /\ (sto_bn_values_productmultiply) = 0) \/ exists ge_signed_half_values_productmultiplyright. (((scp_second_values_product) = 2 * ge_signed_half_values_productmultiplyright + 1 /\ (sto_bp_values_productmultiply) = 0) /\ (sto_bn_values_productmultiply) = S ge_signed_half_values_productmultiplyright))) /\ ((((((scp_value_values_product) = 2 * (sto_cp_values_productmultiply) /\ (sto_cn_values_productmultiply) = 0) \/ exists ge_signed_half_values_productmultiplyoutput. (((scp_value_values_product) = 2 * ge_signed_half_values_productmultiplyoutput + 1 /\ (sto_cp_values_productmultiply) = 0) /\ (sto_cn_values_productmultiply) = S ge_signed_half_values_productmultiplyoutput))) /\ ((sto_ap_values_productmultiply * sto_bp_values_productmultiply + sto_an_values_productmultiply * sto_bn_values_productmultiply) + sto_cn_values_productmultiply = (sto_ap_values_productmultiply * sto_bn_values_productmultiply + sto_an_values_productmultiply * sto_bp_values_productmultiply) + sto_cp_values_productmultiply)))))))))))))) /\ (((exists dst_positive_code_values_first dst_positive_scale_values_first dst_negative_code_values_first dst_negative_scale_values_first dst_positive_sum_values_first dst_negative_sum_values_first. (((F) = (((((dst_positive_code_values_first) + (dst_positive_scale_values_first)) * S ((dst_positive_code_values_first) + (dst_positive_scale_values_first)) + ((dst_positive_scale_values_first) + (dst_positive_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))) * S ((((dst_positive_code_values_first) + (dst_positive_scale_values_first)) * S ((dst_positive_code_values_first) + (dst_positive_scale_values_first)) + ((dst_positive_scale_values_first) + (dst_positive_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))) + ((((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first))) + (((dst_negative_code_values_first) + (dst_negative_scale_values_first)) * S ((dst_negative_code_values_first) + (dst_negative_scale_values_first)) + ((dst_negative_scale_values_first) + (dst_negative_scale_values_first)))))) /\ (((exists fs_u_dst_values_firstpositive fs_v_dst_values_firstpositive. ((((exists fs_h_dst_values_firstpositive_body_start. fs_h_dst_values_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_values_firstpositive)) /\ exists fs_q_dst_values_firstpositive_body_start. fs_u_dst_values_firstpositive = fs_q_dst_values_firstpositive_body_start * S ((S (0)) * fs_v_dst_values_firstpositive) + (0))) /\ ((((exists fs_h_dst_values_firstpositive_body_terminal. fs_h_dst_values_firstpositive_body_terminal + S (dst_positive_sum_values_first) = S ((S (m)) * fs_v_dst_values_firstpositive)) /\ exists fs_q_dst_values_firstpositive_body_terminal. fs_u_dst_values_firstpositive = fs_q_dst_values_firstpositive_body_terminal * S ((S (m)) * fs_v_dst_values_firstpositive) + (dst_positive_sum_values_first))) /\ forall fs_i_dst_values_firstpositive_body_steps. (exists fs_lt_dst_values_firstpositive_body_steps_bound. fs_lt_dst_values_firstpositive_body_steps_bound + S fs_i_dst_values_firstpositive_body_steps = m) -> exists fs_a_dst_values_firstpositive_body_steps fs_r_dst_values_firstpositive_body_steps fs_s_dst_values_firstpositive_body_steps. ((((exists fs_h_dst_values_firstpositive_body_steps_summand. fs_h_dst_values_firstpositive_body_steps_summand + S (fs_a_dst_values_firstpositive_body_steps) = S ((S (fs_i_dst_values_firstpositive_body_steps)) * dst_positive_scale_values_first)) /\ exists fs_q_dst_values_firstpositive_body_steps_summand. dst_positive_code_values_first = fs_q_dst_values_firstpositive_body_steps_summand * S ((S (fs_i_dst_values_firstpositive_body_steps)) * dst_positive_scale_values_first) + (fs_a_dst_values_firstpositive_body_steps))) /\ ((((exists fs_h_dst_values_firstpositive_body_steps_partial. fs_h_dst_values_firstpositive_body_steps_partial + S (fs_r_dst_values_firstpositive_body_steps) = S ((S (fs_i_dst_values_firstpositive_body_steps)) * fs_v_dst_values_firstpositive)) /\ exists fs_q_dst_values_firstpositive_body_steps_partial. fs_u_dst_values_firstpositive = fs_q_dst_values_firstpositive_body_steps_partial * S ((S (fs_i_dst_values_firstpositive_body_steps)) * fs_v_dst_values_firstpositive) + (fs_r_dst_values_firstpositive_body_steps))) /\ ((((exists fs_h_dst_values_firstpositive_body_steps_successor. fs_h_dst_values_firstpositive_body_steps_successor + S (fs_s_dst_values_firstpositive_body_steps) = S ((S (S fs_i_dst_values_firstpositive_body_steps)) * fs_v_dst_values_firstpositive)) /\ exists fs_q_dst_values_firstpositive_body_steps_successor. fs_u_dst_values_firstpositive = fs_q_dst_values_firstpositive_body_steps_successor * S ((S (S fs_i_dst_values_firstpositive_body_steps)) * fs_v_dst_values_firstpositive) + (fs_s_dst_values_firstpositive_body_steps))) /\ fs_s_dst_values_firstpositive_body_steps = fs_r_dst_values_firstpositive_body_steps + fs_a_dst_values_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_values_firstnegative fs_v_dst_values_firstnegative. ((((exists fs_h_dst_values_firstnegative_body_start. fs_h_dst_values_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_values_firstnegative)) /\ exists fs_q_dst_values_firstnegative_body_start. fs_u_dst_values_firstnegative = fs_q_dst_values_firstnegative_body_start * S ((S (0)) * fs_v_dst_values_firstnegative) + (0))) /\ ((((exists fs_h_dst_values_firstnegative_body_terminal. fs_h_dst_values_firstnegative_body_terminal + S (dst_negative_sum_values_first) = S ((S (m)) * fs_v_dst_values_firstnegative)) /\ exists fs_q_dst_values_firstnegative_body_terminal. fs_u_dst_values_firstnegative = fs_q_dst_values_firstnegative_body_terminal * S ((S (m)) * fs_v_dst_values_firstnegative) + (dst_negative_sum_values_first))) /\ forall fs_i_dst_values_firstnegative_body_steps. (exists fs_lt_dst_values_firstnegative_body_steps_bound. fs_lt_dst_values_firstnegative_body_steps_bound + S fs_i_dst_values_firstnegative_body_steps = m) -> exists fs_a_dst_values_firstnegative_body_steps fs_r_dst_values_firstnegative_body_steps fs_s_dst_values_firstnegative_body_steps. ((((exists fs_h_dst_values_firstnegative_body_steps_summand. fs_h_dst_values_firstnegative_body_steps_summand + S (fs_a_dst_values_firstnegative_body_steps) = S ((S (fs_i_dst_values_firstnegative_body_steps)) * dst_negative_scale_values_first)) /\ exists fs_q_dst_values_firstnegative_body_steps_summand. dst_negative_code_values_first = fs_q_dst_values_firstnegative_body_steps_summand * S ((S (fs_i_dst_values_firstnegative_body_steps)) * dst_negative_scale_values_first) + (fs_a_dst_values_firstnegative_body_steps))) /\ ((((exists fs_h_dst_values_firstnegative_body_steps_partial. fs_h_dst_values_firstnegative_body_steps_partial + S (fs_r_dst_values_firstnegative_body_steps) = S ((S (fs_i_dst_values_firstnegative_body_steps)) * fs_v_dst_values_firstnegative)) /\ exists fs_q_dst_values_firstnegative_body_steps_partial. fs_u_dst_values_firstnegative = fs_q_dst_values_firstnegative_body_steps_partial * S ((S (fs_i_dst_values_firstnegative_body_steps)) * fs_v_dst_values_firstnegative) + (fs_r_dst_values_firstnegative_body_steps))) /\ ((((exists fs_h_dst_values_firstnegative_body_steps_successor. fs_h_dst_values_firstnegative_body_steps_successor + S (fs_s_dst_values_firstnegative_body_steps) = S ((S (S fs_i_dst_values_firstnegative_body_steps)) * fs_v_dst_values_firstnegative)) /\ exists fs_q_dst_values_firstnegative_body_steps_successor. fs_u_dst_values_firstnegative = fs_q_dst_values_firstnegative_body_steps_successor * S ((S (S fs_i_dst_values_firstnegative_body_steps)) * fs_v_dst_values_firstnegative) + (fs_s_dst_values_firstnegative_body_steps))) /\ fs_s_dst_values_firstnegative_body_steps = fs_r_dst_values_firstnegative_body_steps + fs_a_dst_values_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_values_firstresult ge_balance_negative_values_firstresult. (((((a) = 2 * (ge_balance_positive_values_firstresult) /\ (ge_balance_negative_values_firstresult) = 0) \/ exists ge_signed_half_values_firstresultdecode. (((a) = 2 * ge_signed_half_values_firstresultdecode + 1 /\ (ge_balance_positive_values_firstresult) = 0) /\ (ge_balance_negative_values_firstresult) = S ge_signed_half_values_firstresultdecode))) /\ ((dst_positive_sum_values_first) + ge_balance_negative_values_firstresult = (dst_negative_sum_values_first) + ge_balance_positive_values_firstresult))))))))) /\ (((exists dst_positive_code_values_second dst_positive_scale_values_second dst_negative_code_values_second dst_negative_scale_values_second dst_positive_sum_values_second dst_negative_sum_values_second. (((G) = (((((dst_positive_code_values_second) + (dst_positive_scale_values_second)) * S ((dst_positive_code_values_second) + (dst_positive_scale_values_second)) + ((dst_positive_scale_values_second) + (dst_positive_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))) * S ((((dst_positive_code_values_second) + (dst_positive_scale_values_second)) * S ((dst_positive_code_values_second) + (dst_positive_scale_values_second)) + ((dst_positive_scale_values_second) + (dst_positive_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))) + ((((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second))) + (((dst_negative_code_values_second) + (dst_negative_scale_values_second)) * S ((dst_negative_code_values_second) + (dst_negative_scale_values_second)) + ((dst_negative_scale_values_second) + (dst_negative_scale_values_second)))))) /\ (((exists fs_u_dst_values_secondpositive fs_v_dst_values_secondpositive. ((((exists fs_h_dst_values_secondpositive_body_start. fs_h_dst_values_secondpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_values_secondpositive)) /\ exists fs_q_dst_values_secondpositive_body_start. fs_u_dst_values_secondpositive = fs_q_dst_values_secondpositive_body_start * S ((S (0)) * fs_v_dst_values_secondpositive) + (0))) /\ ((((exists fs_h_dst_values_secondpositive_body_terminal. fs_h_dst_values_secondpositive_body_terminal + S (dst_positive_sum_values_second) = S ((S (n)) * fs_v_dst_values_secondpositive)) /\ exists fs_q_dst_values_secondpositive_body_terminal. fs_u_dst_values_secondpositive = fs_q_dst_values_secondpositive_body_terminal * S ((S (n)) * fs_v_dst_values_secondpositive) + (dst_positive_sum_values_second))) /\ forall fs_i_dst_values_secondpositive_body_steps. (exists fs_lt_dst_values_secondpositive_body_steps_bound. fs_lt_dst_values_secondpositive_body_steps_bound + S fs_i_dst_values_secondpositive_body_steps = n) -> exists fs_a_dst_values_secondpositive_body_steps fs_r_dst_values_secondpositive_body_steps fs_s_dst_values_secondpositive_body_steps. ((((exists fs_h_dst_values_secondpositive_body_steps_summand. fs_h_dst_values_secondpositive_body_steps_summand + S (fs_a_dst_values_secondpositive_body_steps) = S ((S (fs_i_dst_values_secondpositive_body_steps)) * dst_positive_scale_values_second)) /\ exists fs_q_dst_values_secondpositive_body_steps_summand. dst_positive_code_values_second = fs_q_dst_values_secondpositive_body_steps_summand * S ((S (fs_i_dst_values_secondpositive_body_steps)) * dst_positive_scale_values_second) + (fs_a_dst_values_secondpositive_body_steps))) /\ ((((exists fs_h_dst_values_secondpositive_body_steps_partial. fs_h_dst_values_secondpositive_body_steps_partial + S (fs_r_dst_values_secondpositive_body_steps) = S ((S (fs_i_dst_values_secondpositive_body_steps)) * fs_v_dst_values_secondpositive)) /\ exists fs_q_dst_values_secondpositive_body_steps_partial. fs_u_dst_values_secondpositive = fs_q_dst_values_secondpositive_body_steps_partial * S ((S (fs_i_dst_values_secondpositive_body_steps)) * fs_v_dst_values_secondpositive) + (fs_r_dst_values_secondpositive_body_steps))) /\ ((((exists fs_h_dst_values_secondpositive_body_steps_successor. fs_h_dst_values_secondpositive_body_steps_successor + S (fs_s_dst_values_secondpositive_body_steps) = S ((S (S fs_i_dst_values_secondpositive_body_steps)) * fs_v_dst_values_secondpositive)) /\ exists fs_q_dst_values_secondpositive_body_steps_successor. fs_u_dst_values_secondpositive = fs_q_dst_values_secondpositive_body_steps_successor * S ((S (S fs_i_dst_values_secondpositive_body_steps)) * fs_v_dst_values_secondpositive) + (fs_s_dst_values_secondpositive_body_steps))) /\ fs_s_dst_values_secondpositive_body_steps = fs_r_dst_values_secondpositive_body_steps + fs_a_dst_values_secondpositive_body_steps)))))) /\ (((exists fs_u_dst_values_secondnegative fs_v_dst_values_secondnegative. ((((exists fs_h_dst_values_secondnegative_body_start. fs_h_dst_values_secondnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_values_secondnegative)) /\ exists fs_q_dst_values_secondnegative_body_start. fs_u_dst_values_secondnegative = fs_q_dst_values_secondnegative_body_start * S ((S (0)) * fs_v_dst_values_secondnegative) + (0))) /\ ((((exists fs_h_dst_values_secondnegative_body_terminal. fs_h_dst_values_secondnegative_body_terminal + S (dst_negative_sum_values_second) = S ((S (n)) * fs_v_dst_values_secondnegative)) /\ exists fs_q_dst_values_secondnegative_body_terminal. fs_u_dst_values_secondnegative = fs_q_dst_values_secondnegative_body_terminal * S ((S (n)) * fs_v_dst_values_secondnegative) + (dst_negative_sum_values_second))) /\ forall fs_i_dst_values_secondnegative_body_steps. (exists fs_lt_dst_values_secondnegative_body_steps_bound. fs_lt_dst_values_secondnegative_body_steps_bound + S fs_i_dst_values_secondnegative_body_steps = n) -> exists fs_a_dst_values_secondnegative_body_steps fs_r_dst_values_secondnegative_body_steps fs_s_dst_values_secondnegative_body_steps. ((((exists fs_h_dst_values_secondnegative_body_steps_summand. fs_h_dst_values_secondnegative_body_steps_summand + S (fs_a_dst_values_secondnegative_body_steps) = S ((S (fs_i_dst_values_secondnegative_body_steps)) * dst_negative_scale_values_second)) /\ exists fs_q_dst_values_secondnegative_body_steps_summand. dst_negative_code_values_second = fs_q_dst_values_secondnegative_body_steps_summand * S ((S (fs_i_dst_values_secondnegative_body_steps)) * dst_negative_scale_values_second) + (fs_a_dst_values_secondnegative_body_steps))) /\ ((((exists fs_h_dst_values_secondnegative_body_steps_partial. fs_h_dst_values_secondnegative_body_steps_partial + S (fs_r_dst_values_secondnegative_body_steps) = S ((S (fs_i_dst_values_secondnegative_body_steps)) * fs_v_dst_values_secondnegative)) /\ exists fs_q_dst_values_secondnegative_body_steps_partial. fs_u_dst_values_secondnegative = fs_q_dst_values_secondnegative_body_steps_partial * S ((S (fs_i_dst_values_secondnegative_body_steps)) * fs_v_dst_values_secondnegative) + (fs_r_dst_values_secondnegative_body_steps))) /\ ((((exists fs_h_dst_values_secondnegative_body_steps_successor. fs_h_dst_values_secondnegative_body_steps_successor + S (fs_s_dst_values_secondnegative_body_steps) = S ((S (S fs_i_dst_values_secondnegative_body_steps)) * fs_v_dst_values_secondnegative)) /\ exists fs_q_dst_values_secondnegative_body_steps_successor. fs_u_dst_values_secondnegative = fs_q_dst_values_secondnegative_body_steps_successor * S ((S (S fs_i_dst_values_secondnegative_body_steps)) * fs_v_dst_values_secondnegative) + (fs_s_dst_values_secondnegative_body_steps))) /\ fs_s_dst_values_secondnegative_body_steps = fs_r_dst_values_secondnegative_body_steps + fs_a_dst_values_secondnegative_body_steps)))))) /\ (exists ge_balance_positive_values_secondresult ge_balance_negative_values_secondresult. (((((b) = 2 * (ge_balance_positive_values_secondresult) /\ (ge_balance_negative_values_secondresult) = 0) \/ exists ge_signed_half_values_secondresultdecode. (((b) = 2 * ge_signed_half_values_secondresultdecode + 1 /\ (ge_balance_positive_values_secondresult) = 0) /\ (ge_balance_negative_values_secondresult) = S ge_signed_half_values_secondresultdecode))) /\ ((dst_positive_sum_values_second) + ge_balance_negative_values_secondresult = (dst_negative_sum_values_second) + ge_balance_positive_values_secondresult))))))))) /\ (((exists dst_positive_code_values_total dst_positive_scale_values_total dst_negative_code_values_total dst_negative_scale_values_total dst_positive_sum_values_total dst_negative_sum_values_total. (((T) = (((((dst_positive_code_values_total) + (dst_positive_scale_values_total)) * S ((dst_positive_code_values_total) + (dst_positive_scale_values_total)) + ((dst_positive_scale_values_total) + (dst_positive_scale_values_total))) + (((dst_negative_code_values_total) + (dst_negative_scale_values_total)) * S ((dst_negative_code_values_total) + (dst_negative_scale_values_total)) + ((dst_negative_scale_values_total) + (dst_negative_scale_values_total)))) * S ((((dst_positive_code_values_total) + (dst_positive_scale_values_total)) * S ((dst_positive_code_values_total) + (dst_positive_scale_values_total)) + ((dst_positive_scale_values_total) + (dst_positive_scale_values_total))) + (((dst_negative_code_values_total) + (dst_negative_scale_values_total)) * S ((dst_negative_code_values_total) + (dst_negative_scale_values_total)) + ((dst_negative_scale_values_total) + (dst_negative_scale_values_total)))) + ((((dst_negative_code_values_total) + (dst_negative_scale_values_total)) * S ((dst_negative_code_values_total) + (dst_negative_scale_values_total)) + ((dst_negative_scale_values_total) + (dst_negative_scale_values_total))) + (((dst_negative_code_values_total) + (dst_negative_scale_values_total)) * S ((dst_negative_code_values_total) + (dst_negative_scale_values_total)) + ((dst_negative_scale_values_total) + (dst_negative_scale_values_total)))))) /\ (((exists fs_u_dst_values_totalpositive fs_v_dst_values_totalpositive. ((((exists fs_h_dst_values_totalpositive_body_start. fs_h_dst_values_totalpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_values_totalpositive)) /\ exists fs_q_dst_values_totalpositive_body_start. fs_u_dst_values_totalpositive = fs_q_dst_values_totalpositive_body_start * S ((S (0)) * fs_v_dst_values_totalpositive) + (0))) /\ ((((exists fs_h_dst_values_totalpositive_body_terminal. fs_h_dst_values_totalpositive_body_terminal + S (dst_positive_sum_values_total) = S ((S (m*n)) * fs_v_dst_values_totalpositive)) /\ exists fs_q_dst_values_totalpositive_body_terminal. fs_u_dst_values_totalpositive = fs_q_dst_values_totalpositive_body_terminal * S ((S (m*n)) * fs_v_dst_values_totalpositive) + (dst_positive_sum_values_total))) /\ forall fs_i_dst_values_totalpositive_body_steps. (exists fs_lt_dst_values_totalpositive_body_steps_bound. fs_lt_dst_values_totalpositive_body_steps_bound + S fs_i_dst_values_totalpositive_body_steps = m*n) -> exists fs_a_dst_values_totalpositive_body_steps fs_r_dst_values_totalpositive_body_steps fs_s_dst_values_totalpositive_body_steps. ((((exists fs_h_dst_values_totalpositive_body_steps_summand. fs_h_dst_values_totalpositive_body_steps_summand + S (fs_a_dst_values_totalpositive_body_steps) = S ((S (fs_i_dst_values_totalpositive_body_steps)) * dst_positive_scale_values_total)) /\ exists fs_q_dst_values_totalpositive_body_steps_summand. dst_positive_code_values_total = fs_q_dst_values_totalpositive_body_steps_summand * S ((S (fs_i_dst_values_totalpositive_body_steps)) * dst_positive_scale_values_total) + (fs_a_dst_values_totalpositive_body_steps))) /\ ((((exists fs_h_dst_values_totalpositive_body_steps_partial. fs_h_dst_values_totalpositive_body_steps_partial + S (fs_r_dst_values_totalpositive_body_steps) = S ((S (fs_i_dst_values_totalpositive_body_steps)) * fs_v_dst_values_totalpositive)) /\ exists fs_q_dst_values_totalpositive_body_steps_partial. fs_u_dst_values_totalpositive = fs_q_dst_values_totalpositive_body_steps_partial * S ((S (fs_i_dst_values_totalpositive_body_steps)) * fs_v_dst_values_totalpositive) + (fs_r_dst_values_totalpositive_body_steps))) /\ ((((exists fs_h_dst_values_totalpositive_body_steps_successor. fs_h_dst_values_totalpositive_body_steps_successor + S (fs_s_dst_values_totalpositive_body_steps) = S ((S (S fs_i_dst_values_totalpositive_body_steps)) * fs_v_dst_values_totalpositive)) /\ exists fs_q_dst_values_totalpositive_body_steps_successor. fs_u_dst_values_totalpositive = fs_q_dst_values_totalpositive_body_steps_successor * S ((S (S fs_i_dst_values_totalpositive_body_steps)) * fs_v_dst_values_totalpositive) + (fs_s_dst_values_totalpositive_body_steps))) /\ fs_s_dst_values_totalpositive_body_steps = fs_r_dst_values_totalpositive_body_steps + fs_a_dst_values_totalpositive_body_steps)))))) /\ (((exists fs_u_dst_values_totalnegative fs_v_dst_values_totalnegative. ((((exists fs_h_dst_values_totalnegative_body_start. fs_h_dst_values_totalnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_values_totalnegative)) /\ exists fs_q_dst_values_totalnegative_body_start. fs_u_dst_values_totalnegative = fs_q_dst_values_totalnegative_body_start * S ((S (0)) * fs_v_dst_values_totalnegative) + (0))) /\ ((((exists fs_h_dst_values_totalnegative_body_terminal. fs_h_dst_values_totalnegative_body_terminal + S (dst_negative_sum_values_total) = S ((S (m*n)) * fs_v_dst_values_totalnegative)) /\ exists fs_q_dst_values_totalnegative_body_terminal. fs_u_dst_values_totalnegative = fs_q_dst_values_totalnegative_body_terminal * S ((S (m*n)) * fs_v_dst_values_totalnegative) + (dst_negative_sum_values_total))) /\ forall fs_i_dst_values_totalnegative_body_steps. (exists fs_lt_dst_values_totalnegative_body_steps_bound. fs_lt_dst_values_totalnegative_body_steps_bound + S fs_i_dst_values_totalnegative_body_steps = m*n) -> exists fs_a_dst_values_totalnegative_body_steps fs_r_dst_values_totalnegative_body_steps fs_s_dst_values_totalnegative_body_steps. ((((exists fs_h_dst_values_totalnegative_body_steps_summand. fs_h_dst_values_totalnegative_body_steps_summand + S (fs_a_dst_values_totalnegative_body_steps) = S ((S (fs_i_dst_values_totalnegative_body_steps)) * dst_negative_scale_values_total)) /\ exists fs_q_dst_values_totalnegative_body_steps_summand. dst_negative_code_values_total = fs_q_dst_values_totalnegative_body_steps_summand * S ((S (fs_i_dst_values_totalnegative_body_steps)) * dst_negative_scale_values_total) + (fs_a_dst_values_totalnegative_body_steps))) /\ ((((exists fs_h_dst_values_totalnegative_body_steps_partial. fs_h_dst_values_totalnegative_body_steps_partial + S (fs_r_dst_values_totalnegative_body_steps) = S ((S (fs_i_dst_values_totalnegative_body_steps)) * fs_v_dst_values_totalnegative)) /\ exists fs_q_dst_values_totalnegative_body_steps_partial. fs_u_dst_values_totalnegative = fs_q_dst_values_totalnegative_body_steps_partial * S ((S (fs_i_dst_values_totalnegative_body_steps)) * fs_v_dst_values_totalnegative) + (fs_r_dst_values_totalnegative_body_steps))) /\ ((((exists fs_h_dst_values_totalnegative_body_steps_successor. fs_h_dst_values_totalnegative_body_steps_successor + S (fs_s_dst_values_totalnegative_body_steps) = S ((S (S fs_i_dst_values_totalnegative_body_steps)) * fs_v_dst_values_totalnegative)) /\ exists fs_q_dst_values_totalnegative_body_steps_successor. fs_u_dst_values_totalnegative = fs_q_dst_values_totalnegative_body_steps_successor * S ((S (S fs_i_dst_values_totalnegative_body_steps)) * fs_v_dst_values_totalnegative) + (fs_s_dst_values_totalnegative_body_steps))) /\ fs_s_dst_values_totalnegative_body_steps = fs_r_dst_values_totalnegative_body_steps + fs_a_dst_values_totalnegative_body_steps)))))) /\ (exists ge_balance_positive_values_totalresult ge_balance_negative_values_totalresult. (((((c) = 2 * (ge_balance_positive_values_totalresult) /\ (ge_balance_negative_values_totalresult) = 0) \/ exists ge_signed_half_values_totalresultdecode. (((c) = 2 * ge_signed_half_values_totalresultdecode + 1 /\ (ge_balance_positive_values_totalresult) = 0) /\ (ge_balance_negative_values_totalresult) = S ge_signed_half_values_totalresultdecode))) /\ ((dst_positive_sum_values_total) + ge_balance_negative_values_totalresult = (dst_negative_sum_values_total) + ge_balance_positive_values_totalresult))))))))) /\ (exists sto_ap_values_result sto_an_values_result sto_bp_values_result sto_bn_values_result sto_cp_values_result sto_cn_values_result. (((((a) = 2 * (sto_ap_values_result) /\ (sto_an_values_result) = 0) \/ exists ge_signed_half_values_resultleft. (((a) = 2 * ge_signed_half_values_resultleft + 1 /\ (sto_ap_values_result) = 0) /\ (sto_an_values_result) = S ge_signed_half_values_resultleft))) /\ ((((((b) = 2 * (sto_bp_values_result) /\ (sto_bn_values_result) = 0) \/ exists ge_signed_half_values_resultright. (((b) = 2 * ge_signed_half_values_resultright + 1 /\ (sto_bp_values_result) = 0) /\ (sto_bn_values_result) = S ge_signed_half_values_resultright))) /\ ((((((c) = 2 * (sto_cp_values_result) /\ (sto_cn_values_result) = 0) \/ exists ge_signed_half_values_resultoutput. (((c) = 2 * ge_signed_half_values_resultoutput + 1 /\ (sto_cp_values_result) = 0) /\ (sto_cn_values_result) = S ge_signed_half_values_resultoutput))) /\ ((sto_ap_values_result * sto_bp_values_result + sto_an_values_result * sto_bn_values_result) + sto_cn_values_result = (sto_ap_values_result * sto_bn_values_result + sto_an_values_result * sto_bp_values_result) + sto_cp_values_result))))))))))))))