dirichlet_grid_flat_entry_coordinates

Exact expanded first-order arithmetic statement

forall F G H n a e z. (exists pvs_gap_flat_read_bound. pvs_gap_flat_read_bound + S (e) = (S n)) -> (exists dfg_flat_row_flat_read_source dfg_flat_column_flat_read_source. ((((S (n))*(a)+(e))=((S (n))*(dfg_flat_row_flat_read_source)+(dfg_flat_column_flat_read_source))) /\ (((exists pvs_gap_flat_read_sourceremainder. pvs_gap_flat_read_sourceremainder + S (dfg_flat_column_flat_read_source) = (S (n))) /\ ((((~((dfg_flat_row_flat_read_source)=0)) /\ (((~((dfg_flat_column_flat_read_source)=0)) /\ (exists dfg_middle_flat_read_sourcecell dfg_first_flat_read_sourcecell dfg_last_flat_read_sourcecell dfg_value_flat_read_sourcecell. (((n)=((dfg_flat_row_flat_read_source)*(dfg_flat_column_flat_read_source))*dfg_middle_flat_read_sourcecell) /\ (((exists dst_positive_code_flat_read_sourcecellfirst dst_positive_scale_flat_read_sourcecellfirst dst_negative_code_flat_read_sourcecellfirst dst_negative_scale_flat_read_sourcecellfirst dst_positive_flat_read_sourcecellfirst dst_negative_flat_read_sourcecellfirst. (((F) = (((((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) * S ((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) + ((dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))) * S ((((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) * S ((dst_positive_code_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst)) + ((dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))) + ((((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst))) + (((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) * S ((dst_negative_code_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)) + ((dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_scale_flat_read_sourcecellfirst)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecellfirstpositive. ff_h_pvs_flat_read_sourcecellfirstpositive + S (dst_positive_flat_read_sourcecellfirst) = S ((S (dfg_flat_row_flat_read_source)) * dst_positive_scale_flat_read_sourcecellfirst)) /\ exists ff_q_pvs_flat_read_sourcecellfirstpositive. dst_positive_code_flat_read_sourcecellfirst = ff_q_pvs_flat_read_sourcecellfirstpositive * S ((S (dfg_flat_row_flat_read_source)) * dst_positive_scale_flat_read_sourcecellfirst) + (dst_positive_flat_read_sourcecellfirst))) /\ (((((exists ff_h_pvs_flat_read_sourcecellfirstnegative. ff_h_pvs_flat_read_sourcecellfirstnegative + S (dst_negative_flat_read_sourcecellfirst) = S ((S (dfg_flat_row_flat_read_source)) * dst_negative_scale_flat_read_sourcecellfirst)) /\ exists ff_q_pvs_flat_read_sourcecellfirstnegative. dst_negative_code_flat_read_sourcecellfirst = ff_q_pvs_flat_read_sourcecellfirstnegative * S ((S (dfg_flat_row_flat_read_source)) * dst_negative_scale_flat_read_sourcecellfirst) + (dst_negative_flat_read_sourcecellfirst))) /\ (exists ge_balance_positive_flat_read_sourcecellfirstvalue ge_balance_negative_flat_read_sourcecellfirstvalue. (((((dfg_first_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecellfirstvalue) /\ (ge_balance_negative_flat_read_sourcecellfirstvalue) = 0) \/ exists ge_signed_half_flat_read_sourcecellfirstvaluedecode. (((dfg_first_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellfirstvaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecellfirstvalue) = 0) /\ (ge_balance_negative_flat_read_sourcecellfirstvalue) = S ge_signed_half_flat_read_sourcecellfirstvaluedecode))) /\ ((dst_positive_flat_read_sourcecellfirst) + ge_balance_negative_flat_read_sourcecellfirstvalue = (dst_negative_flat_read_sourcecellfirst) + ge_balance_positive_flat_read_sourcecellfirstvalue))))))))) /\ (((exists dst_positive_code_flat_read_sourcecelllast dst_positive_scale_flat_read_sourcecelllast dst_negative_code_flat_read_sourcecelllast dst_negative_scale_flat_read_sourcecelllast dst_positive_flat_read_sourcecelllast dst_negative_flat_read_sourcecelllast. (((H) = (((((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) * S ((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) + ((dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))) * S ((((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) * S ((dst_positive_code_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast)) + ((dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))) + ((((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast))) + (((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) * S ((dst_negative_code_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)) + ((dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_scale_flat_read_sourcecelllast)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecelllastpositive. ff_h_pvs_flat_read_sourcecelllastpositive + S (dst_positive_flat_read_sourcecelllast) = S ((S (dfg_flat_column_flat_read_source)) * dst_positive_scale_flat_read_sourcecelllast)) /\ exists ff_q_pvs_flat_read_sourcecelllastpositive. dst_positive_code_flat_read_sourcecelllast = ff_q_pvs_flat_read_sourcecelllastpositive * S ((S (dfg_flat_column_flat_read_source)) * dst_positive_scale_flat_read_sourcecelllast) + (dst_positive_flat_read_sourcecelllast))) /\ (((((exists ff_h_pvs_flat_read_sourcecelllastnegative. ff_h_pvs_flat_read_sourcecelllastnegative + S (dst_negative_flat_read_sourcecelllast) = S ((S (dfg_flat_column_flat_read_source)) * dst_negative_scale_flat_read_sourcecelllast)) /\ exists ff_q_pvs_flat_read_sourcecelllastnegative. dst_negative_code_flat_read_sourcecelllast = ff_q_pvs_flat_read_sourcecelllastnegative * S ((S (dfg_flat_column_flat_read_source)) * dst_negative_scale_flat_read_sourcecelllast) + (dst_negative_flat_read_sourcecelllast))) /\ (exists ge_balance_positive_flat_read_sourcecelllastvalue ge_balance_negative_flat_read_sourcecelllastvalue. (((((dfg_last_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecelllastvalue) /\ (ge_balance_negative_flat_read_sourcecelllastvalue) = 0) \/ exists ge_signed_half_flat_read_sourcecelllastvaluedecode. (((dfg_last_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecelllastvaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecelllastvalue) = 0) /\ (ge_balance_negative_flat_read_sourcecelllastvalue) = S ge_signed_half_flat_read_sourcecelllastvaluedecode))) /\ ((dst_positive_flat_read_sourcecelllast) + ge_balance_negative_flat_read_sourcecelllastvalue = (dst_negative_flat_read_sourcecelllast) + ge_balance_positive_flat_read_sourcecelllastvalue))))))))) /\ (((exists dst_positive_code_flat_read_sourcecellmiddle dst_positive_scale_flat_read_sourcecellmiddle dst_negative_code_flat_read_sourcecellmiddle dst_negative_scale_flat_read_sourcecellmiddle dst_positive_flat_read_sourcecellmiddle dst_negative_flat_read_sourcecellmiddle. (((G) = (((((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) * S ((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) + ((dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))) * S ((((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) * S ((dst_positive_code_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle)) + ((dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))) + ((((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle))) + (((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) * S ((dst_negative_code_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)) + ((dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_scale_flat_read_sourcecellmiddle)))))) /\ (((((exists ff_h_pvs_flat_read_sourcecellmiddlepositive. ff_h_pvs_flat_read_sourcecellmiddlepositive + S (dst_positive_flat_read_sourcecellmiddle) = S ((S (dfg_middle_flat_read_sourcecell)) * dst_positive_scale_flat_read_sourcecellmiddle)) /\ exists ff_q_pvs_flat_read_sourcecellmiddlepositive. dst_positive_code_flat_read_sourcecellmiddle = ff_q_pvs_flat_read_sourcecellmiddlepositive * S ((S (dfg_middle_flat_read_sourcecell)) * dst_positive_scale_flat_read_sourcecellmiddle) + (dst_positive_flat_read_sourcecellmiddle))) /\ (((((exists ff_h_pvs_flat_read_sourcecellmiddlenegative. ff_h_pvs_flat_read_sourcecellmiddlenegative + S (dst_negative_flat_read_sourcecellmiddle) = S ((S (dfg_middle_flat_read_sourcecell)) * dst_negative_scale_flat_read_sourcecellmiddle)) /\ exists ff_q_pvs_flat_read_sourcecellmiddlenegative. dst_negative_code_flat_read_sourcecellmiddle = ff_q_pvs_flat_read_sourcecellmiddlenegative * S ((S (dfg_middle_flat_read_sourcecell)) * dst_negative_scale_flat_read_sourcecellmiddle) + (dst_negative_flat_read_sourcecellmiddle))) /\ (exists ge_balance_positive_flat_read_sourcecellmiddlevalue ge_balance_negative_flat_read_sourcecellmiddlevalue. (((((dfg_value_flat_read_sourcecell) = 2 * (ge_balance_positive_flat_read_sourcecellmiddlevalue) /\ (ge_balance_negative_flat_read_sourcecellmiddlevalue) = 0) \/ exists ge_signed_half_flat_read_sourcecellmiddlevaluedecode. (((dfg_value_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellmiddlevaluedecode + 1 /\ (ge_balance_positive_flat_read_sourcecellmiddlevalue) = 0) /\ (ge_balance_negative_flat_read_sourcecellmiddlevalue) = S ge_signed_half_flat_read_sourcecellmiddlevaluedecode))) /\ ((dst_positive_flat_read_sourcecellmiddle) + ge_balance_negative_flat_read_sourcecellmiddlevalue = (dst_negative_flat_read_sourcecellmiddle) + ge_balance_positive_flat_read_sourcecellmiddlevalue))))))))) /\ (exists dfg_inner_flat_read_sourcecellproduct. ((exists sto_ap_flat_read_sourcecellproductinner sto_an_flat_read_sourcecellproductinner sto_bp_flat_read_sourcecellproductinner sto_bn_flat_read_sourcecellproductinner sto_cp_flat_read_sourcecellproductinner sto_cn_flat_read_sourcecellproductinner. (((((dfg_last_flat_read_sourcecell) = 2 * (sto_ap_flat_read_sourcecellproductinner) /\ (sto_an_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinnerleft. (((dfg_last_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductinnerleft + 1 /\ (sto_ap_flat_read_sourcecellproductinner) = 0) /\ (sto_an_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinnerleft))) /\ ((((((dfg_value_flat_read_sourcecell) = 2 * (sto_bp_flat_read_sourcecellproductinner) /\ (sto_bn_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinnerright. (((dfg_value_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductinnerright + 1 /\ (sto_bp_flat_read_sourcecellproductinner) = 0) /\ (sto_bn_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinnerright))) /\ ((((((dfg_inner_flat_read_sourcecellproduct) = 2 * (sto_cp_flat_read_sourcecellproductinner) /\ (sto_cn_flat_read_sourcecellproductinner) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductinneroutput. (((dfg_inner_flat_read_sourcecellproduct) = 2 * ge_signed_half_flat_read_sourcecellproductinneroutput + 1 /\ (sto_cp_flat_read_sourcecellproductinner) = 0) /\ (sto_cn_flat_read_sourcecellproductinner) = S ge_signed_half_flat_read_sourcecellproductinneroutput))) /\ ((sto_ap_flat_read_sourcecellproductinner * sto_bp_flat_read_sourcecellproductinner + sto_an_flat_read_sourcecellproductinner * sto_bn_flat_read_sourcecellproductinner) + sto_cn_flat_read_sourcecellproductinner = (sto_ap_flat_read_sourcecellproductinner * sto_bn_flat_read_sourcecellproductinner + sto_an_flat_read_sourcecellproductinner * sto_bp_flat_read_sourcecellproductinner) + sto_cp_flat_read_sourcecellproductinner))))))) /\ (exists sto_ap_flat_read_sourcecellproductouter sto_an_flat_read_sourcecellproductouter sto_bp_flat_read_sourcecellproductouter sto_bn_flat_read_sourcecellproductouter sto_cp_flat_read_sourcecellproductouter sto_cn_flat_read_sourcecellproductouter. (((((dfg_first_flat_read_sourcecell) = 2 * (sto_ap_flat_read_sourcecellproductouter) /\ (sto_an_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouterleft. (((dfg_first_flat_read_sourcecell) = 2 * ge_signed_half_flat_read_sourcecellproductouterleft + 1 /\ (sto_ap_flat_read_sourcecellproductouter) = 0) /\ (sto_an_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouterleft))) /\ ((((((dfg_inner_flat_read_sourcecellproduct) = 2 * (sto_bp_flat_read_sourcecellproductouter) /\ (sto_bn_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouterright. (((dfg_inner_flat_read_sourcecellproduct) = 2 * ge_signed_half_flat_read_sourcecellproductouterright + 1 /\ (sto_bp_flat_read_sourcecellproductouter) = 0) /\ (sto_bn_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_read_sourcecellproductouter) /\ (sto_cn_flat_read_sourcecellproductouter) = 0) \/ exists ge_signed_half_flat_read_sourcecellproductouteroutput. (((z) = 2 * ge_signed_half_flat_read_sourcecellproductouteroutput + 1 /\ (sto_cp_flat_read_sourcecellproductouter) = 0) /\ (sto_cn_flat_read_sourcecellproductouter) = S ge_signed_half_flat_read_sourcecellproductouteroutput))) /\ ((sto_ap_flat_read_sourcecellproductouter * sto_bp_flat_read_sourcecellproductouter + sto_an_flat_read_sourcecellproductouter * sto_bn_flat_read_sourcecellproductouter) + sto_cn_flat_read_sourcecellproductouter = (sto_ap_flat_read_sourcecellproductouter * sto_bn_flat_read_sourcecellproductouter + sto_an_flat_read_sourcecellproductouter * sto_bp_flat_read_sourcecellproductouter) + sto_cp_flat_read_sourcecellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_flat_read_source)=0 \/ ((dfg_flat_column_flat_read_source)=0 \/ ~(exists pvs_factor_flat_read_sourcecellomittednondivisor. (n) = ((dfg_flat_row_flat_read_source)*(dfg_flat_column_flat_read_source)) * pvs_factor_flat_read_sourcecellomittednondivisor))) /\ ((z)=0)))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_flat_read_target dfg_first_flat_read_target dfg_last_flat_read_target dfg_value_flat_read_target. (((n)=((a)*(e))*dfg_middle_flat_read_target) /\ (((exists dst_positive_code_flat_read_targetfirst dst_positive_scale_flat_read_targetfirst dst_negative_code_flat_read_targetfirst dst_negative_scale_flat_read_targetfirst dst_positive_flat_read_targetfirst dst_negative_flat_read_targetfirst. (((F) = (((((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) * S ((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) + ((dst_positive_scale_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))) * S ((((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) * S ((dst_positive_code_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst)) + ((dst_positive_scale_flat_read_targetfirst) + (dst_positive_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))) + ((((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst))) + (((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) * S ((dst_negative_code_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)) + ((dst_negative_scale_flat_read_targetfirst) + (dst_negative_scale_flat_read_targetfirst)))))) /\ (((((exists ff_h_pvs_flat_read_targetfirstpositive. ff_h_pvs_flat_read_targetfirstpositive + S (dst_positive_flat_read_targetfirst) = S ((S (a)) * dst_positive_scale_flat_read_targetfirst)) /\ exists ff_q_pvs_flat_read_targetfirstpositive. dst_positive_code_flat_read_targetfirst = ff_q_pvs_flat_read_targetfirstpositive * S ((S (a)) * dst_positive_scale_flat_read_targetfirst) + (dst_positive_flat_read_targetfirst))) /\ (((((exists ff_h_pvs_flat_read_targetfirstnegative. ff_h_pvs_flat_read_targetfirstnegative + S (dst_negative_flat_read_targetfirst) = S ((S (a)) * dst_negative_scale_flat_read_targetfirst)) /\ exists ff_q_pvs_flat_read_targetfirstnegative. dst_negative_code_flat_read_targetfirst = ff_q_pvs_flat_read_targetfirstnegative * S ((S (a)) * dst_negative_scale_flat_read_targetfirst) + (dst_negative_flat_read_targetfirst))) /\ (exists ge_balance_positive_flat_read_targetfirstvalue ge_balance_negative_flat_read_targetfirstvalue. (((((dfg_first_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetfirstvalue) /\ (ge_balance_negative_flat_read_targetfirstvalue) = 0) \/ exists ge_signed_half_flat_read_targetfirstvaluedecode. (((dfg_first_flat_read_target) = 2 * ge_signed_half_flat_read_targetfirstvaluedecode + 1 /\ (ge_balance_positive_flat_read_targetfirstvalue) = 0) /\ (ge_balance_negative_flat_read_targetfirstvalue) = S ge_signed_half_flat_read_targetfirstvaluedecode))) /\ ((dst_positive_flat_read_targetfirst) + ge_balance_negative_flat_read_targetfirstvalue = (dst_negative_flat_read_targetfirst) + ge_balance_positive_flat_read_targetfirstvalue))))))))) /\ (((exists dst_positive_code_flat_read_targetlast dst_positive_scale_flat_read_targetlast dst_negative_code_flat_read_targetlast dst_negative_scale_flat_read_targetlast dst_positive_flat_read_targetlast dst_negative_flat_read_targetlast. (((H) = (((((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) * S ((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) + ((dst_positive_scale_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))) * S ((((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) * S ((dst_positive_code_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast)) + ((dst_positive_scale_flat_read_targetlast) + (dst_positive_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))) + ((((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast))) + (((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) * S ((dst_negative_code_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)) + ((dst_negative_scale_flat_read_targetlast) + (dst_negative_scale_flat_read_targetlast)))))) /\ (((((exists ff_h_pvs_flat_read_targetlastpositive. ff_h_pvs_flat_read_targetlastpositive + S (dst_positive_flat_read_targetlast) = S ((S (e)) * dst_positive_scale_flat_read_targetlast)) /\ exists ff_q_pvs_flat_read_targetlastpositive. dst_positive_code_flat_read_targetlast = ff_q_pvs_flat_read_targetlastpositive * S ((S (e)) * dst_positive_scale_flat_read_targetlast) + (dst_positive_flat_read_targetlast))) /\ (((((exists ff_h_pvs_flat_read_targetlastnegative. ff_h_pvs_flat_read_targetlastnegative + S (dst_negative_flat_read_targetlast) = S ((S (e)) * dst_negative_scale_flat_read_targetlast)) /\ exists ff_q_pvs_flat_read_targetlastnegative. dst_negative_code_flat_read_targetlast = ff_q_pvs_flat_read_targetlastnegative * S ((S (e)) * dst_negative_scale_flat_read_targetlast) + (dst_negative_flat_read_targetlast))) /\ (exists ge_balance_positive_flat_read_targetlastvalue ge_balance_negative_flat_read_targetlastvalue. (((((dfg_last_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetlastvalue) /\ (ge_balance_negative_flat_read_targetlastvalue) = 0) \/ exists ge_signed_half_flat_read_targetlastvaluedecode. (((dfg_last_flat_read_target) = 2 * ge_signed_half_flat_read_targetlastvaluedecode + 1 /\ (ge_balance_positive_flat_read_targetlastvalue) = 0) /\ (ge_balance_negative_flat_read_targetlastvalue) = S ge_signed_half_flat_read_targetlastvaluedecode))) /\ ((dst_positive_flat_read_targetlast) + ge_balance_negative_flat_read_targetlastvalue = (dst_negative_flat_read_targetlast) + ge_balance_positive_flat_read_targetlastvalue))))))))) /\ (((exists dst_positive_code_flat_read_targetmiddle dst_positive_scale_flat_read_targetmiddle dst_negative_code_flat_read_targetmiddle dst_negative_scale_flat_read_targetmiddle dst_positive_flat_read_targetmiddle dst_negative_flat_read_targetmiddle. (((G) = (((((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) * S ((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) + ((dst_positive_scale_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))) * S ((((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) * S ((dst_positive_code_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle)) + ((dst_positive_scale_flat_read_targetmiddle) + (dst_positive_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))) + ((((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle))) + (((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) * S ((dst_negative_code_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)) + ((dst_negative_scale_flat_read_targetmiddle) + (dst_negative_scale_flat_read_targetmiddle)))))) /\ (((((exists ff_h_pvs_flat_read_targetmiddlepositive. ff_h_pvs_flat_read_targetmiddlepositive + S (dst_positive_flat_read_targetmiddle) = S ((S (dfg_middle_flat_read_target)) * dst_positive_scale_flat_read_targetmiddle)) /\ exists ff_q_pvs_flat_read_targetmiddlepositive. dst_positive_code_flat_read_targetmiddle = ff_q_pvs_flat_read_targetmiddlepositive * S ((S (dfg_middle_flat_read_target)) * dst_positive_scale_flat_read_targetmiddle) + (dst_positive_flat_read_targetmiddle))) /\ (((((exists ff_h_pvs_flat_read_targetmiddlenegative. ff_h_pvs_flat_read_targetmiddlenegative + S (dst_negative_flat_read_targetmiddle) = S ((S (dfg_middle_flat_read_target)) * dst_negative_scale_flat_read_targetmiddle)) /\ exists ff_q_pvs_flat_read_targetmiddlenegative. dst_negative_code_flat_read_targetmiddle = ff_q_pvs_flat_read_targetmiddlenegative * S ((S (dfg_middle_flat_read_target)) * dst_negative_scale_flat_read_targetmiddle) + (dst_negative_flat_read_targetmiddle))) /\ (exists ge_balance_positive_flat_read_targetmiddlevalue ge_balance_negative_flat_read_targetmiddlevalue. (((((dfg_value_flat_read_target) = 2 * (ge_balance_positive_flat_read_targetmiddlevalue) /\ (ge_balance_negative_flat_read_targetmiddlevalue) = 0) \/ exists ge_signed_half_flat_read_targetmiddlevaluedecode. (((dfg_value_flat_read_target) = 2 * ge_signed_half_flat_read_targetmiddlevaluedecode + 1 /\ (ge_balance_positive_flat_read_targetmiddlevalue) = 0) /\ (ge_balance_negative_flat_read_targetmiddlevalue) = S ge_signed_half_flat_read_targetmiddlevaluedecode))) /\ ((dst_positive_flat_read_targetmiddle) + ge_balance_negative_flat_read_targetmiddlevalue = (dst_negative_flat_read_targetmiddle) + ge_balance_positive_flat_read_targetmiddlevalue))))))))) /\ (exists dfg_inner_flat_read_targetproduct. ((exists sto_ap_flat_read_targetproductinner sto_an_flat_read_targetproductinner sto_bp_flat_read_targetproductinner sto_bn_flat_read_targetproductinner sto_cp_flat_read_targetproductinner sto_cn_flat_read_targetproductinner. (((((dfg_last_flat_read_target) = 2 * (sto_ap_flat_read_targetproductinner) /\ (sto_an_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinnerleft. (((dfg_last_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductinnerleft + 1 /\ (sto_ap_flat_read_targetproductinner) = 0) /\ (sto_an_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinnerleft))) /\ ((((((dfg_value_flat_read_target) = 2 * (sto_bp_flat_read_targetproductinner) /\ (sto_bn_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinnerright. (((dfg_value_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductinnerright + 1 /\ (sto_bp_flat_read_targetproductinner) = 0) /\ (sto_bn_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinnerright))) /\ ((((((dfg_inner_flat_read_targetproduct) = 2 * (sto_cp_flat_read_targetproductinner) /\ (sto_cn_flat_read_targetproductinner) = 0) \/ exists ge_signed_half_flat_read_targetproductinneroutput. (((dfg_inner_flat_read_targetproduct) = 2 * ge_signed_half_flat_read_targetproductinneroutput + 1 /\ (sto_cp_flat_read_targetproductinner) = 0) /\ (sto_cn_flat_read_targetproductinner) = S ge_signed_half_flat_read_targetproductinneroutput))) /\ ((sto_ap_flat_read_targetproductinner * sto_bp_flat_read_targetproductinner + sto_an_flat_read_targetproductinner * sto_bn_flat_read_targetproductinner) + sto_cn_flat_read_targetproductinner = (sto_ap_flat_read_targetproductinner * sto_bn_flat_read_targetproductinner + sto_an_flat_read_targetproductinner * sto_bp_flat_read_targetproductinner) + sto_cp_flat_read_targetproductinner))))))) /\ (exists sto_ap_flat_read_targetproductouter sto_an_flat_read_targetproductouter sto_bp_flat_read_targetproductouter sto_bn_flat_read_targetproductouter sto_cp_flat_read_targetproductouter sto_cn_flat_read_targetproductouter. (((((dfg_first_flat_read_target) = 2 * (sto_ap_flat_read_targetproductouter) /\ (sto_an_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouterleft. (((dfg_first_flat_read_target) = 2 * ge_signed_half_flat_read_targetproductouterleft + 1 /\ (sto_ap_flat_read_targetproductouter) = 0) /\ (sto_an_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouterleft))) /\ ((((((dfg_inner_flat_read_targetproduct) = 2 * (sto_bp_flat_read_targetproductouter) /\ (sto_bn_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouterright. (((dfg_inner_flat_read_targetproduct) = 2 * ge_signed_half_flat_read_targetproductouterright + 1 /\ (sto_bp_flat_read_targetproductouter) = 0) /\ (sto_bn_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouterright))) /\ ((((((z) = 2 * (sto_cp_flat_read_targetproductouter) /\ (sto_cn_flat_read_targetproductouter) = 0) \/ exists ge_signed_half_flat_read_targetproductouteroutput. (((z) = 2 * ge_signed_half_flat_read_targetproductouteroutput + 1 /\ (sto_cp_flat_read_targetproductouter) = 0) /\ (sto_cn_flat_read_targetproductouter) = S ge_signed_half_flat_read_targetproductouteroutput))) /\ ((sto_ap_flat_read_targetproductouter * sto_bp_flat_read_targetproductouter + sto_an_flat_read_targetproductouter * sto_bn_flat_read_targetproductouter) + sto_cn_flat_read_targetproductouter = (sto_ap_flat_read_targetproductouter * sto_bn_flat_read_targetproductouter + sto_an_flat_read_targetproductouter * sto_bp_flat_read_targetproductouter) + sto_cp_flat_read_targetproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_flat_read_targetomittednondivisor. (n) = ((a)*(e)) * pvs_factor_flat_read_targetomittednondivisor))) /\ ((z)=0))))