dirichlet_grid_flat_prefix_zero

Exact expanded first-order arithmetic statement

forall F G H n T z. (exists dst_positive_code_base_table dst_positive_scale_base_table dst_negative_code_base_table dst_negative_scale_base_table. (((T) = (((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) * S ((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) + ((((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))))) /\ (forall dst_index_base_table. (exists pvs_le_gap_base_tabledomain. pvs_le_gap_base_tabledomain + (dst_index_base_table) = (0)) -> exists dst_positive_base_table dst_negative_base_table dst_value_base_table. ((((exists ff_h_pvs_base_tableentrypositive. ff_h_pvs_base_tableentrypositive + S (dst_positive_base_table) = S ((S (dst_index_base_table)) * dst_positive_scale_base_table)) /\ exists ff_q_pvs_base_tableentrypositive. dst_positive_code_base_table = ff_q_pvs_base_tableentrypositive * S ((S (dst_index_base_table)) * dst_positive_scale_base_table) + (dst_positive_base_table))) /\ (((((exists ff_h_pvs_base_tableentrynegative. ff_h_pvs_base_tableentrynegative + S (dst_negative_base_table) = S ((S (dst_index_base_table)) * dst_negative_scale_base_table)) /\ exists ff_q_pvs_base_tableentrynegative. dst_negative_code_base_table = ff_q_pvs_base_tableentrynegative * S ((S (dst_index_base_table)) * dst_negative_scale_base_table) + (dst_negative_base_table))) /\ (exists ge_balance_positive_base_tableentryvalue ge_balance_negative_base_tableentryvalue. (((((dst_value_base_table) = 2 * (ge_balance_positive_base_tableentryvalue) /\ (ge_balance_negative_base_tableentryvalue) = 0) \/ exists ge_signed_half_base_tableentryvaluedecode. (((dst_value_base_table) = 2 * ge_signed_half_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_base_tableentryvalue) = 0) /\ (ge_balance_negative_base_tableentryvalue) = S ge_signed_half_base_tableentryvaluedecode))) /\ ((dst_positive_base_table) + ge_balance_negative_base_tableentryvalue = (dst_negative_base_table) + ge_balance_positive_base_tableentryvalue))))))))) -> (exists dst_positive_code_base_entry dst_positive_scale_base_entry dst_negative_code_base_entry dst_negative_scale_base_entry dst_positive_base_entry dst_negative_base_entry. (((T) = (((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) * S ((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) + ((((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))))) /\ (((((exists ff_h_pvs_base_entrypositive. ff_h_pvs_base_entrypositive + S (dst_positive_base_entry) = S ((S (0)) * dst_positive_scale_base_entry)) /\ exists ff_q_pvs_base_entrypositive. dst_positive_code_base_entry = ff_q_pvs_base_entrypositive * S ((S (0)) * dst_positive_scale_base_entry) + (dst_positive_base_entry))) /\ (((((exists ff_h_pvs_base_entrynegative. ff_h_pvs_base_entrynegative + S (dst_negative_base_entry) = S ((S (0)) * dst_negative_scale_base_entry)) /\ exists ff_q_pvs_base_entrynegative. dst_negative_code_base_entry = ff_q_pvs_base_entrynegative * S ((S (0)) * dst_negative_scale_base_entry) + (dst_negative_base_entry))) /\ (exists ge_balance_positive_base_entryvalue ge_balance_negative_base_entryvalue. (((((z) = 2 * (ge_balance_positive_base_entryvalue) /\ (ge_balance_negative_base_entryvalue) = 0) \/ exists ge_signed_half_base_entryvaluedecode. (((z) = 2 * ge_signed_half_base_entryvaluedecode + 1 /\ (ge_balance_positive_base_entryvalue) = 0) /\ (ge_balance_negative_base_entryvalue) = S ge_signed_half_base_entryvaluedecode))) /\ ((dst_positive_base_entry) + ge_balance_negative_base_entryvalue = (dst_negative_base_entry) + ge_balance_positive_base_entryvalue))))))))) -> (exists dfg_flat_row_base_value dfg_flat_column_base_value. (((0)=((S (n))*(dfg_flat_row_base_value)+(dfg_flat_column_base_value))) /\ (((exists pvs_gap_base_valueremainder. pvs_gap_base_valueremainder + S (dfg_flat_column_base_value) = (S (n))) /\ ((((~((dfg_flat_row_base_value)=0)) /\ (((~((dfg_flat_column_base_value)=0)) /\ (exists dfg_middle_base_valuecell dfg_first_base_valuecell dfg_last_base_valuecell dfg_value_base_valuecell. (((n)=((dfg_flat_row_base_value)*(dfg_flat_column_base_value))*dfg_middle_base_valuecell) /\ (((exists dst_positive_code_base_valuecellfirst dst_positive_scale_base_valuecellfirst dst_negative_code_base_valuecellfirst dst_negative_scale_base_valuecellfirst dst_positive_base_valuecellfirst dst_negative_base_valuecellfirst. (((F) = (((((dst_positive_code_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst)) * S ((dst_positive_code_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst)) + ((dst_positive_scale_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst))) + (((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) * S ((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) + ((dst_negative_scale_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)))) * S ((((dst_positive_code_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst)) * S ((dst_positive_code_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst)) + ((dst_positive_scale_base_valuecellfirst) + (dst_positive_scale_base_valuecellfirst))) + (((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) * S ((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) + ((dst_negative_scale_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)))) + ((((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) * S ((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) + ((dst_negative_scale_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst))) + (((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) * S ((dst_negative_code_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)) + ((dst_negative_scale_base_valuecellfirst) + (dst_negative_scale_base_valuecellfirst)))))) /\ (((((exists ff_h_pvs_base_valuecellfirstpositive. ff_h_pvs_base_valuecellfirstpositive + S (dst_positive_base_valuecellfirst) = S ((S (dfg_flat_row_base_value)) * dst_positive_scale_base_valuecellfirst)) /\ exists ff_q_pvs_base_valuecellfirstpositive. dst_positive_code_base_valuecellfirst = ff_q_pvs_base_valuecellfirstpositive * S ((S (dfg_flat_row_base_value)) * dst_positive_scale_base_valuecellfirst) + (dst_positive_base_valuecellfirst))) /\ (((((exists ff_h_pvs_base_valuecellfirstnegative. ff_h_pvs_base_valuecellfirstnegative + S (dst_negative_base_valuecellfirst) = S ((S (dfg_flat_row_base_value)) * dst_negative_scale_base_valuecellfirst)) /\ exists ff_q_pvs_base_valuecellfirstnegative. dst_negative_code_base_valuecellfirst = ff_q_pvs_base_valuecellfirstnegative * S ((S (dfg_flat_row_base_value)) * dst_negative_scale_base_valuecellfirst) + (dst_negative_base_valuecellfirst))) /\ (exists ge_balance_positive_base_valuecellfirstvalue ge_balance_negative_base_valuecellfirstvalue. (((((dfg_first_base_valuecell) = 2 * (ge_balance_positive_base_valuecellfirstvalue) /\ (ge_balance_negative_base_valuecellfirstvalue) = 0) \/ exists ge_signed_half_base_valuecellfirstvaluedecode. (((dfg_first_base_valuecell) = 2 * ge_signed_half_base_valuecellfirstvaluedecode + 1 /\ (ge_balance_positive_base_valuecellfirstvalue) = 0) /\ (ge_balance_negative_base_valuecellfirstvalue) = S ge_signed_half_base_valuecellfirstvaluedecode))) /\ ((dst_positive_base_valuecellfirst) + ge_balance_negative_base_valuecellfirstvalue = (dst_negative_base_valuecellfirst) + ge_balance_positive_base_valuecellfirstvalue))))))))) /\ (((exists dst_positive_code_base_valuecelllast dst_positive_scale_base_valuecelllast dst_negative_code_base_valuecelllast dst_negative_scale_base_valuecelllast dst_positive_base_valuecelllast dst_negative_base_valuecelllast. (((H) = (((((dst_positive_code_base_valuecelllast) + (dst_positive_scale_base_valuecelllast)) * S ((dst_positive_code_base_valuecelllast) + (dst_positive_scale_base_valuecelllast)) + ((dst_positive_scale_base_valuecelllast) + (dst_positive_scale_base_valuecelllast))) + (((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) * S ((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) + ((dst_negative_scale_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)))) * S ((((dst_positive_code_base_valuecelllast) + (dst_positive_scale_base_valuecelllast)) * S ((dst_positive_code_base_valuecelllast) + (dst_positive_scale_base_valuecelllast)) + ((dst_positive_scale_base_valuecelllast) + (dst_positive_scale_base_valuecelllast))) + (((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) * S ((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) + ((dst_negative_scale_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)))) + ((((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) * S ((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) + ((dst_negative_scale_base_valuecelllast) + (dst_negative_scale_base_valuecelllast))) + (((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) * S ((dst_negative_code_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)) + ((dst_negative_scale_base_valuecelllast) + (dst_negative_scale_base_valuecelllast)))))) /\ (((((exists ff_h_pvs_base_valuecelllastpositive. ff_h_pvs_base_valuecelllastpositive + S (dst_positive_base_valuecelllast) = S ((S (dfg_flat_column_base_value)) * dst_positive_scale_base_valuecelllast)) /\ exists ff_q_pvs_base_valuecelllastpositive. dst_positive_code_base_valuecelllast = ff_q_pvs_base_valuecelllastpositive * S ((S (dfg_flat_column_base_value)) * dst_positive_scale_base_valuecelllast) + (dst_positive_base_valuecelllast))) /\ (((((exists ff_h_pvs_base_valuecelllastnegative. ff_h_pvs_base_valuecelllastnegative + S (dst_negative_base_valuecelllast) = S ((S (dfg_flat_column_base_value)) * dst_negative_scale_base_valuecelllast)) /\ exists ff_q_pvs_base_valuecelllastnegative. dst_negative_code_base_valuecelllast = ff_q_pvs_base_valuecelllastnegative * S ((S (dfg_flat_column_base_value)) * dst_negative_scale_base_valuecelllast) + (dst_negative_base_valuecelllast))) /\ (exists ge_balance_positive_base_valuecelllastvalue ge_balance_negative_base_valuecelllastvalue. (((((dfg_last_base_valuecell) = 2 * (ge_balance_positive_base_valuecelllastvalue) /\ (ge_balance_negative_base_valuecelllastvalue) = 0) \/ exists ge_signed_half_base_valuecelllastvaluedecode. (((dfg_last_base_valuecell) = 2 * ge_signed_half_base_valuecelllastvaluedecode + 1 /\ (ge_balance_positive_base_valuecelllastvalue) = 0) /\ (ge_balance_negative_base_valuecelllastvalue) = S ge_signed_half_base_valuecelllastvaluedecode))) /\ ((dst_positive_base_valuecelllast) + ge_balance_negative_base_valuecelllastvalue = (dst_negative_base_valuecelllast) + ge_balance_positive_base_valuecelllastvalue))))))))) /\ (((exists dst_positive_code_base_valuecellmiddle dst_positive_scale_base_valuecellmiddle dst_negative_code_base_valuecellmiddle dst_negative_scale_base_valuecellmiddle dst_positive_base_valuecellmiddle dst_negative_base_valuecellmiddle. (((G) = (((((dst_positive_code_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle)) * S ((dst_positive_code_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle)) + ((dst_positive_scale_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle))) + (((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) * S ((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) + ((dst_negative_scale_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)))) * S ((((dst_positive_code_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle)) * S ((dst_positive_code_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle)) + ((dst_positive_scale_base_valuecellmiddle) + (dst_positive_scale_base_valuecellmiddle))) + (((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) * S ((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) + ((dst_negative_scale_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)))) + ((((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) * S ((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) + ((dst_negative_scale_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle))) + (((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) * S ((dst_negative_code_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)) + ((dst_negative_scale_base_valuecellmiddle) + (dst_negative_scale_base_valuecellmiddle)))))) /\ (((((exists ff_h_pvs_base_valuecellmiddlepositive. ff_h_pvs_base_valuecellmiddlepositive + S (dst_positive_base_valuecellmiddle) = S ((S (dfg_middle_base_valuecell)) * dst_positive_scale_base_valuecellmiddle)) /\ exists ff_q_pvs_base_valuecellmiddlepositive. dst_positive_code_base_valuecellmiddle = ff_q_pvs_base_valuecellmiddlepositive * S ((S (dfg_middle_base_valuecell)) * dst_positive_scale_base_valuecellmiddle) + (dst_positive_base_valuecellmiddle))) /\ (((((exists ff_h_pvs_base_valuecellmiddlenegative. ff_h_pvs_base_valuecellmiddlenegative + S (dst_negative_base_valuecellmiddle) = S ((S (dfg_middle_base_valuecell)) * dst_negative_scale_base_valuecellmiddle)) /\ exists ff_q_pvs_base_valuecellmiddlenegative. dst_negative_code_base_valuecellmiddle = ff_q_pvs_base_valuecellmiddlenegative * S ((S (dfg_middle_base_valuecell)) * dst_negative_scale_base_valuecellmiddle) + (dst_negative_base_valuecellmiddle))) /\ (exists ge_balance_positive_base_valuecellmiddlevalue ge_balance_negative_base_valuecellmiddlevalue. (((((dfg_value_base_valuecell) = 2 * (ge_balance_positive_base_valuecellmiddlevalue) /\ (ge_balance_negative_base_valuecellmiddlevalue) = 0) \/ exists ge_signed_half_base_valuecellmiddlevaluedecode. (((dfg_value_base_valuecell) = 2 * ge_signed_half_base_valuecellmiddlevaluedecode + 1 /\ (ge_balance_positive_base_valuecellmiddlevalue) = 0) /\ (ge_balance_negative_base_valuecellmiddlevalue) = S ge_signed_half_base_valuecellmiddlevaluedecode))) /\ ((dst_positive_base_valuecellmiddle) + ge_balance_negative_base_valuecellmiddlevalue = (dst_negative_base_valuecellmiddle) + ge_balance_positive_base_valuecellmiddlevalue))))))))) /\ (exists dfg_inner_base_valuecellproduct. ((exists sto_ap_base_valuecellproductinner sto_an_base_valuecellproductinner sto_bp_base_valuecellproductinner sto_bn_base_valuecellproductinner sto_cp_base_valuecellproductinner sto_cn_base_valuecellproductinner. (((((dfg_last_base_valuecell) = 2 * (sto_ap_base_valuecellproductinner) /\ (sto_an_base_valuecellproductinner) = 0) \/ exists ge_signed_half_base_valuecellproductinnerleft. (((dfg_last_base_valuecell) = 2 * ge_signed_half_base_valuecellproductinnerleft + 1 /\ (sto_ap_base_valuecellproductinner) = 0) /\ (sto_an_base_valuecellproductinner) = S ge_signed_half_base_valuecellproductinnerleft))) /\ ((((((dfg_value_base_valuecell) = 2 * (sto_bp_base_valuecellproductinner) /\ (sto_bn_base_valuecellproductinner) = 0) \/ exists ge_signed_half_base_valuecellproductinnerright. (((dfg_value_base_valuecell) = 2 * ge_signed_half_base_valuecellproductinnerright + 1 /\ (sto_bp_base_valuecellproductinner) = 0) /\ (sto_bn_base_valuecellproductinner) = S ge_signed_half_base_valuecellproductinnerright))) /\ ((((((dfg_inner_base_valuecellproduct) = 2 * (sto_cp_base_valuecellproductinner) /\ (sto_cn_base_valuecellproductinner) = 0) \/ exists ge_signed_half_base_valuecellproductinneroutput. (((dfg_inner_base_valuecellproduct) = 2 * ge_signed_half_base_valuecellproductinneroutput + 1 /\ (sto_cp_base_valuecellproductinner) = 0) /\ (sto_cn_base_valuecellproductinner) = S ge_signed_half_base_valuecellproductinneroutput))) /\ ((sto_ap_base_valuecellproductinner * sto_bp_base_valuecellproductinner + sto_an_base_valuecellproductinner * sto_bn_base_valuecellproductinner) + sto_cn_base_valuecellproductinner = (sto_ap_base_valuecellproductinner * sto_bn_base_valuecellproductinner + sto_an_base_valuecellproductinner * sto_bp_base_valuecellproductinner) + sto_cp_base_valuecellproductinner))))))) /\ (exists sto_ap_base_valuecellproductouter sto_an_base_valuecellproductouter sto_bp_base_valuecellproductouter sto_bn_base_valuecellproductouter sto_cp_base_valuecellproductouter sto_cn_base_valuecellproductouter. (((((dfg_first_base_valuecell) = 2 * (sto_ap_base_valuecellproductouter) /\ (sto_an_base_valuecellproductouter) = 0) \/ exists ge_signed_half_base_valuecellproductouterleft. (((dfg_first_base_valuecell) = 2 * ge_signed_half_base_valuecellproductouterleft + 1 /\ (sto_ap_base_valuecellproductouter) = 0) /\ (sto_an_base_valuecellproductouter) = S ge_signed_half_base_valuecellproductouterleft))) /\ ((((((dfg_inner_base_valuecellproduct) = 2 * (sto_bp_base_valuecellproductouter) /\ (sto_bn_base_valuecellproductouter) = 0) \/ exists ge_signed_half_base_valuecellproductouterright. (((dfg_inner_base_valuecellproduct) = 2 * ge_signed_half_base_valuecellproductouterright + 1 /\ (sto_bp_base_valuecellproductouter) = 0) /\ (sto_bn_base_valuecellproductouter) = S ge_signed_half_base_valuecellproductouterright))) /\ ((((((z) = 2 * (sto_cp_base_valuecellproductouter) /\ (sto_cn_base_valuecellproductouter) = 0) \/ exists ge_signed_half_base_valuecellproductouteroutput. (((z) = 2 * ge_signed_half_base_valuecellproductouteroutput + 1 /\ (sto_cp_base_valuecellproductouter) = 0) /\ (sto_cn_base_valuecellproductouter) = S ge_signed_half_base_valuecellproductouteroutput))) /\ ((sto_ap_base_valuecellproductouter * sto_bp_base_valuecellproductouter + sto_an_base_valuecellproductouter * sto_bn_base_valuecellproductouter) + sto_cn_base_valuecellproductouter = (sto_ap_base_valuecellproductouter * sto_bn_base_valuecellproductouter + sto_an_base_valuecellproductouter * sto_bp_base_valuecellproductouter) + sto_cp_base_valuecellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_base_value)=0 \/ ((dfg_flat_column_base_value)=0 \/ ~(exists pvs_factor_base_valuecellomittednondivisor. (n) = ((dfg_flat_row_base_value)*(dfg_flat_column_base_value)) * pvs_factor_base_valuecellomittednondivisor))) /\ ((z)=0)))))))) -> (((exists dst_positive_code_base_prefixtable dst_positive_scale_base_prefixtable dst_negative_code_base_prefixtable dst_negative_scale_base_prefixtable. (((T) = (((((dst_positive_code_base_prefixtable) + (dst_positive_scale_base_prefixtable)) * S ((dst_positive_code_base_prefixtable) + (dst_positive_scale_base_prefixtable)) + ((dst_positive_scale_base_prefixtable) + (dst_positive_scale_base_prefixtable))) + (((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) * S ((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) + ((dst_negative_scale_base_prefixtable) + (dst_negative_scale_base_prefixtable)))) * S ((((dst_positive_code_base_prefixtable) + (dst_positive_scale_base_prefixtable)) * S ((dst_positive_code_base_prefixtable) + (dst_positive_scale_base_prefixtable)) + ((dst_positive_scale_base_prefixtable) + (dst_positive_scale_base_prefixtable))) + (((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) * S ((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) + ((dst_negative_scale_base_prefixtable) + (dst_negative_scale_base_prefixtable)))) + ((((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) * S ((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) + ((dst_negative_scale_base_prefixtable) + (dst_negative_scale_base_prefixtable))) + (((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) * S ((dst_negative_code_base_prefixtable) + (dst_negative_scale_base_prefixtable)) + ((dst_negative_scale_base_prefixtable) + (dst_negative_scale_base_prefixtable)))))) /\ (forall dst_index_base_prefixtable. (exists pvs_le_gap_base_prefixtabledomain. pvs_le_gap_base_prefixtabledomain + (dst_index_base_prefixtable) = (0)) -> exists dst_positive_base_prefixtable dst_negative_base_prefixtable dst_value_base_prefixtable. ((((exists ff_h_pvs_base_prefixtableentrypositive. ff_h_pvs_base_prefixtableentrypositive + S (dst_positive_base_prefixtable) = S ((S (dst_index_base_prefixtable)) * dst_positive_scale_base_prefixtable)) /\ exists ff_q_pvs_base_prefixtableentrypositive. dst_positive_code_base_prefixtable = ff_q_pvs_base_prefixtableentrypositive * S ((S (dst_index_base_prefixtable)) * dst_positive_scale_base_prefixtable) + (dst_positive_base_prefixtable))) /\ (((((exists ff_h_pvs_base_prefixtableentrynegative. ff_h_pvs_base_prefixtableentrynegative + S (dst_negative_base_prefixtable) = S ((S (dst_index_base_prefixtable)) * dst_negative_scale_base_prefixtable)) /\ exists ff_q_pvs_base_prefixtableentrynegative. dst_negative_code_base_prefixtable = ff_q_pvs_base_prefixtableentrynegative * S ((S (dst_index_base_prefixtable)) * dst_negative_scale_base_prefixtable) + (dst_negative_base_prefixtable))) /\ (exists ge_balance_positive_base_prefixtableentryvalue ge_balance_negative_base_prefixtableentryvalue. (((((dst_value_base_prefixtable) = 2 * (ge_balance_positive_base_prefixtableentryvalue) /\ (ge_balance_negative_base_prefixtableentryvalue) = 0) \/ exists ge_signed_half_base_prefixtableentryvaluedecode. (((dst_value_base_prefixtable) = 2 * ge_signed_half_base_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_base_prefixtableentryvalue) = 0) /\ (ge_balance_negative_base_prefixtableentryvalue) = S ge_signed_half_base_prefixtableentryvaluedecode))) /\ ((dst_positive_base_prefixtable) + ge_balance_negative_base_prefixtableentryvalue = (dst_negative_base_prefixtable) + ge_balance_positive_base_prefixtableentryvalue))))))))) /\ (forall dfg_flat_index_base_prefix dfg_flat_value_base_prefix. (exists pvs_le_gap_base_prefixbound. pvs_le_gap_base_prefixbound + (dfg_flat_index_base_prefix) = (0)) -> (exists dst_positive_code_base_prefixlookup dst_positive_scale_base_prefixlookup dst_negative_code_base_prefixlookup dst_negative_scale_base_prefixlookup dst_positive_base_prefixlookup dst_negative_base_prefixlookup. (((T) = (((((dst_positive_code_base_prefixlookup) + (dst_positive_scale_base_prefixlookup)) * S ((dst_positive_code_base_prefixlookup) + (dst_positive_scale_base_prefixlookup)) + ((dst_positive_scale_base_prefixlookup) + (dst_positive_scale_base_prefixlookup))) + (((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) * S ((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) + ((dst_negative_scale_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)))) * S ((((dst_positive_code_base_prefixlookup) + (dst_positive_scale_base_prefixlookup)) * S ((dst_positive_code_base_prefixlookup) + (dst_positive_scale_base_prefixlookup)) + ((dst_positive_scale_base_prefixlookup) + (dst_positive_scale_base_prefixlookup))) + (((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) * S ((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) + ((dst_negative_scale_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)))) + ((((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) * S ((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) + ((dst_negative_scale_base_prefixlookup) + (dst_negative_scale_base_prefixlookup))) + (((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) * S ((dst_negative_code_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)) + ((dst_negative_scale_base_prefixlookup) + (dst_negative_scale_base_prefixlookup)))))) /\ (((((exists ff_h_pvs_base_prefixlookuppositive. ff_h_pvs_base_prefixlookuppositive + S (dst_positive_base_prefixlookup) = S ((S (dfg_flat_index_base_prefix)) * dst_positive_scale_base_prefixlookup)) /\ exists ff_q_pvs_base_prefixlookuppositive. dst_positive_code_base_prefixlookup = ff_q_pvs_base_prefixlookuppositive * S ((S (dfg_flat_index_base_prefix)) * dst_positive_scale_base_prefixlookup) + (dst_positive_base_prefixlookup))) /\ (((((exists ff_h_pvs_base_prefixlookupnegative. ff_h_pvs_base_prefixlookupnegative + S (dst_negative_base_prefixlookup) = S ((S (dfg_flat_index_base_prefix)) * dst_negative_scale_base_prefixlookup)) /\ exists ff_q_pvs_base_prefixlookupnegative. dst_negative_code_base_prefixlookup = ff_q_pvs_base_prefixlookupnegative * S ((S (dfg_flat_index_base_prefix)) * dst_negative_scale_base_prefixlookup) + (dst_negative_base_prefixlookup))) /\ (exists ge_balance_positive_base_prefixlookupvalue ge_balance_negative_base_prefixlookupvalue. (((((dfg_flat_value_base_prefix) = 2 * (ge_balance_positive_base_prefixlookupvalue) /\ (ge_balance_negative_base_prefixlookupvalue) = 0) \/ exists ge_signed_half_base_prefixlookupvaluedecode. (((dfg_flat_value_base_prefix) = 2 * ge_signed_half_base_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_base_prefixlookupvalue) = 0) /\ (ge_balance_negative_base_prefixlookupvalue) = S ge_signed_half_base_prefixlookupvaluedecode))) /\ ((dst_positive_base_prefixlookup) + ge_balance_negative_base_prefixlookupvalue = (dst_negative_base_prefixlookup) + ge_balance_positive_base_prefixlookupvalue))))))))) -> (exists dfg_flat_row_base_prefixentry dfg_flat_column_base_prefixentry. (((dfg_flat_index_base_prefix)=((S (n))*(dfg_flat_row_base_prefixentry)+(dfg_flat_column_base_prefixentry))) /\ (((exists pvs_gap_base_prefixentryremainder. pvs_gap_base_prefixentryremainder + S (dfg_flat_column_base_prefixentry) = (S (n))) /\ ((((~((dfg_flat_row_base_prefixentry)=0)) /\ (((~((dfg_flat_column_base_prefixentry)=0)) /\ (exists dfg_middle_base_prefixentrycell dfg_first_base_prefixentrycell dfg_last_base_prefixentrycell dfg_value_base_prefixentrycell. (((n)=((dfg_flat_row_base_prefixentry)*(dfg_flat_column_base_prefixentry))*dfg_middle_base_prefixentrycell) /\ (((exists dst_positive_code_base_prefixentrycellfirst dst_positive_scale_base_prefixentrycellfirst dst_negative_code_base_prefixentrycellfirst dst_negative_scale_base_prefixentrycellfirst dst_positive_base_prefixentrycellfirst dst_negative_base_prefixentrycellfirst. (((F) = (((((dst_positive_code_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst)) * S ((dst_positive_code_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst)) + ((dst_positive_scale_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst))) + (((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) * S ((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) + ((dst_negative_scale_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)))) * S ((((dst_positive_code_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst)) * S ((dst_positive_code_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst)) + ((dst_positive_scale_base_prefixentrycellfirst) + (dst_positive_scale_base_prefixentrycellfirst))) + (((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) * S ((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) + ((dst_negative_scale_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)))) + ((((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) * S ((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) + ((dst_negative_scale_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst))) + (((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) * S ((dst_negative_code_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)) + ((dst_negative_scale_base_prefixentrycellfirst) + (dst_negative_scale_base_prefixentrycellfirst)))))) /\ (((((exists ff_h_pvs_base_prefixentrycellfirstpositive. ff_h_pvs_base_prefixentrycellfirstpositive + S (dst_positive_base_prefixentrycellfirst) = S ((S (dfg_flat_row_base_prefixentry)) * dst_positive_scale_base_prefixentrycellfirst)) /\ exists ff_q_pvs_base_prefixentrycellfirstpositive. dst_positive_code_base_prefixentrycellfirst = ff_q_pvs_base_prefixentrycellfirstpositive * S ((S (dfg_flat_row_base_prefixentry)) * dst_positive_scale_base_prefixentrycellfirst) + (dst_positive_base_prefixentrycellfirst))) /\ (((((exists ff_h_pvs_base_prefixentrycellfirstnegative. ff_h_pvs_base_prefixentrycellfirstnegative + S (dst_negative_base_prefixentrycellfirst) = S ((S (dfg_flat_row_base_prefixentry)) * dst_negative_scale_base_prefixentrycellfirst)) /\ exists ff_q_pvs_base_prefixentrycellfirstnegative. dst_negative_code_base_prefixentrycellfirst = ff_q_pvs_base_prefixentrycellfirstnegative * S ((S (dfg_flat_row_base_prefixentry)) * dst_negative_scale_base_prefixentrycellfirst) + (dst_negative_base_prefixentrycellfirst))) /\ (exists ge_balance_positive_base_prefixentrycellfirstvalue ge_balance_negative_base_prefixentrycellfirstvalue. (((((dfg_first_base_prefixentrycell) = 2 * (ge_balance_positive_base_prefixentrycellfirstvalue) /\ (ge_balance_negative_base_prefixentrycellfirstvalue) = 0) \/ exists ge_signed_half_base_prefixentrycellfirstvaluedecode. (((dfg_first_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycellfirstvaluedecode + 1 /\ (ge_balance_positive_base_prefixentrycellfirstvalue) = 0) /\ (ge_balance_negative_base_prefixentrycellfirstvalue) = S ge_signed_half_base_prefixentrycellfirstvaluedecode))) /\ ((dst_positive_base_prefixentrycellfirst) + ge_balance_negative_base_prefixentrycellfirstvalue = (dst_negative_base_prefixentrycellfirst) + ge_balance_positive_base_prefixentrycellfirstvalue))))))))) /\ (((exists dst_positive_code_base_prefixentrycelllast dst_positive_scale_base_prefixentrycelllast dst_negative_code_base_prefixentrycelllast dst_negative_scale_base_prefixentrycelllast dst_positive_base_prefixentrycelllast dst_negative_base_prefixentrycelllast. (((H) = (((((dst_positive_code_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast)) * S ((dst_positive_code_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast)) + ((dst_positive_scale_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast))) + (((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) * S ((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) + ((dst_negative_scale_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)))) * S ((((dst_positive_code_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast)) * S ((dst_positive_code_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast)) + ((dst_positive_scale_base_prefixentrycelllast) + (dst_positive_scale_base_prefixentrycelllast))) + (((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) * S ((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) + ((dst_negative_scale_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)))) + ((((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) * S ((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) + ((dst_negative_scale_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast))) + (((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) * S ((dst_negative_code_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)) + ((dst_negative_scale_base_prefixentrycelllast) + (dst_negative_scale_base_prefixentrycelllast)))))) /\ (((((exists ff_h_pvs_base_prefixentrycelllastpositive. ff_h_pvs_base_prefixentrycelllastpositive + S (dst_positive_base_prefixentrycelllast) = S ((S (dfg_flat_column_base_prefixentry)) * dst_positive_scale_base_prefixentrycelllast)) /\ exists ff_q_pvs_base_prefixentrycelllastpositive. dst_positive_code_base_prefixentrycelllast = ff_q_pvs_base_prefixentrycelllastpositive * S ((S (dfg_flat_column_base_prefixentry)) * dst_positive_scale_base_prefixentrycelllast) + (dst_positive_base_prefixentrycelllast))) /\ (((((exists ff_h_pvs_base_prefixentrycelllastnegative. ff_h_pvs_base_prefixentrycelllastnegative + S (dst_negative_base_prefixentrycelllast) = S ((S (dfg_flat_column_base_prefixentry)) * dst_negative_scale_base_prefixentrycelllast)) /\ exists ff_q_pvs_base_prefixentrycelllastnegative. dst_negative_code_base_prefixentrycelllast = ff_q_pvs_base_prefixentrycelllastnegative * S ((S (dfg_flat_column_base_prefixentry)) * dst_negative_scale_base_prefixentrycelllast) + (dst_negative_base_prefixentrycelllast))) /\ (exists ge_balance_positive_base_prefixentrycelllastvalue ge_balance_negative_base_prefixentrycelllastvalue. (((((dfg_last_base_prefixentrycell) = 2 * (ge_balance_positive_base_prefixentrycelllastvalue) /\ (ge_balance_negative_base_prefixentrycelllastvalue) = 0) \/ exists ge_signed_half_base_prefixentrycelllastvaluedecode. (((dfg_last_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycelllastvaluedecode + 1 /\ (ge_balance_positive_base_prefixentrycelllastvalue) = 0) /\ (ge_balance_negative_base_prefixentrycelllastvalue) = S ge_signed_half_base_prefixentrycelllastvaluedecode))) /\ ((dst_positive_base_prefixentrycelllast) + ge_balance_negative_base_prefixentrycelllastvalue = (dst_negative_base_prefixentrycelllast) + ge_balance_positive_base_prefixentrycelllastvalue))))))))) /\ (((exists dst_positive_code_base_prefixentrycellmiddle dst_positive_scale_base_prefixentrycellmiddle dst_negative_code_base_prefixentrycellmiddle dst_negative_scale_base_prefixentrycellmiddle dst_positive_base_prefixentrycellmiddle dst_negative_base_prefixentrycellmiddle. (((G) = (((((dst_positive_code_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle)) * S ((dst_positive_code_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle)) + ((dst_positive_scale_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle))) + (((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) * S ((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) + ((dst_negative_scale_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)))) * S ((((dst_positive_code_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle)) * S ((dst_positive_code_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle)) + ((dst_positive_scale_base_prefixentrycellmiddle) + (dst_positive_scale_base_prefixentrycellmiddle))) + (((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) * S ((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) + ((dst_negative_scale_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)))) + ((((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) * S ((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) + ((dst_negative_scale_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle))) + (((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) * S ((dst_negative_code_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)) + ((dst_negative_scale_base_prefixentrycellmiddle) + (dst_negative_scale_base_prefixentrycellmiddle)))))) /\ (((((exists ff_h_pvs_base_prefixentrycellmiddlepositive. ff_h_pvs_base_prefixentrycellmiddlepositive + S (dst_positive_base_prefixentrycellmiddle) = S ((S (dfg_middle_base_prefixentrycell)) * dst_positive_scale_base_prefixentrycellmiddle)) /\ exists ff_q_pvs_base_prefixentrycellmiddlepositive. dst_positive_code_base_prefixentrycellmiddle = ff_q_pvs_base_prefixentrycellmiddlepositive * S ((S (dfg_middle_base_prefixentrycell)) * dst_positive_scale_base_prefixentrycellmiddle) + (dst_positive_base_prefixentrycellmiddle))) /\ (((((exists ff_h_pvs_base_prefixentrycellmiddlenegative. ff_h_pvs_base_prefixentrycellmiddlenegative + S (dst_negative_base_prefixentrycellmiddle) = S ((S (dfg_middle_base_prefixentrycell)) * dst_negative_scale_base_prefixentrycellmiddle)) /\ exists ff_q_pvs_base_prefixentrycellmiddlenegative. dst_negative_code_base_prefixentrycellmiddle = ff_q_pvs_base_prefixentrycellmiddlenegative * S ((S (dfg_middle_base_prefixentrycell)) * dst_negative_scale_base_prefixentrycellmiddle) + (dst_negative_base_prefixentrycellmiddle))) /\ (exists ge_balance_positive_base_prefixentrycellmiddlevalue ge_balance_negative_base_prefixentrycellmiddlevalue. (((((dfg_value_base_prefixentrycell) = 2 * (ge_balance_positive_base_prefixentrycellmiddlevalue) /\ (ge_balance_negative_base_prefixentrycellmiddlevalue) = 0) \/ exists ge_signed_half_base_prefixentrycellmiddlevaluedecode. (((dfg_value_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycellmiddlevaluedecode + 1 /\ (ge_balance_positive_base_prefixentrycellmiddlevalue) = 0) /\ (ge_balance_negative_base_prefixentrycellmiddlevalue) = S ge_signed_half_base_prefixentrycellmiddlevaluedecode))) /\ ((dst_positive_base_prefixentrycellmiddle) + ge_balance_negative_base_prefixentrycellmiddlevalue = (dst_negative_base_prefixentrycellmiddle) + ge_balance_positive_base_prefixentrycellmiddlevalue))))))))) /\ (exists dfg_inner_base_prefixentrycellproduct. ((exists sto_ap_base_prefixentrycellproductinner sto_an_base_prefixentrycellproductinner sto_bp_base_prefixentrycellproductinner sto_bn_base_prefixentrycellproductinner sto_cp_base_prefixentrycellproductinner sto_cn_base_prefixentrycellproductinner. (((((dfg_last_base_prefixentrycell) = 2 * (sto_ap_base_prefixentrycellproductinner) /\ (sto_an_base_prefixentrycellproductinner) = 0) \/ exists ge_signed_half_base_prefixentrycellproductinnerleft. (((dfg_last_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycellproductinnerleft + 1 /\ (sto_ap_base_prefixentrycellproductinner) = 0) /\ (sto_an_base_prefixentrycellproductinner) = S ge_signed_half_base_prefixentrycellproductinnerleft))) /\ ((((((dfg_value_base_prefixentrycell) = 2 * (sto_bp_base_prefixentrycellproductinner) /\ (sto_bn_base_prefixentrycellproductinner) = 0) \/ exists ge_signed_half_base_prefixentrycellproductinnerright. (((dfg_value_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycellproductinnerright + 1 /\ (sto_bp_base_prefixentrycellproductinner) = 0) /\ (sto_bn_base_prefixentrycellproductinner) = S ge_signed_half_base_prefixentrycellproductinnerright))) /\ ((((((dfg_inner_base_prefixentrycellproduct) = 2 * (sto_cp_base_prefixentrycellproductinner) /\ (sto_cn_base_prefixentrycellproductinner) = 0) \/ exists ge_signed_half_base_prefixentrycellproductinneroutput. (((dfg_inner_base_prefixentrycellproduct) = 2 * ge_signed_half_base_prefixentrycellproductinneroutput + 1 /\ (sto_cp_base_prefixentrycellproductinner) = 0) /\ (sto_cn_base_prefixentrycellproductinner) = S ge_signed_half_base_prefixentrycellproductinneroutput))) /\ ((sto_ap_base_prefixentrycellproductinner * sto_bp_base_prefixentrycellproductinner + sto_an_base_prefixentrycellproductinner * sto_bn_base_prefixentrycellproductinner) + sto_cn_base_prefixentrycellproductinner = (sto_ap_base_prefixentrycellproductinner * sto_bn_base_prefixentrycellproductinner + sto_an_base_prefixentrycellproductinner * sto_bp_base_prefixentrycellproductinner) + sto_cp_base_prefixentrycellproductinner))))))) /\ (exists sto_ap_base_prefixentrycellproductouter sto_an_base_prefixentrycellproductouter sto_bp_base_prefixentrycellproductouter sto_bn_base_prefixentrycellproductouter sto_cp_base_prefixentrycellproductouter sto_cn_base_prefixentrycellproductouter. (((((dfg_first_base_prefixentrycell) = 2 * (sto_ap_base_prefixentrycellproductouter) /\ (sto_an_base_prefixentrycellproductouter) = 0) \/ exists ge_signed_half_base_prefixentrycellproductouterleft. (((dfg_first_base_prefixentrycell) = 2 * ge_signed_half_base_prefixentrycellproductouterleft + 1 /\ (sto_ap_base_prefixentrycellproductouter) = 0) /\ (sto_an_base_prefixentrycellproductouter) = S ge_signed_half_base_prefixentrycellproductouterleft))) /\ ((((((dfg_inner_base_prefixentrycellproduct) = 2 * (sto_bp_base_prefixentrycellproductouter) /\ (sto_bn_base_prefixentrycellproductouter) = 0) \/ exists ge_signed_half_base_prefixentrycellproductouterright. (((dfg_inner_base_prefixentrycellproduct) = 2 * ge_signed_half_base_prefixentrycellproductouterright + 1 /\ (sto_bp_base_prefixentrycellproductouter) = 0) /\ (sto_bn_base_prefixentrycellproductouter) = S ge_signed_half_base_prefixentrycellproductouterright))) /\ ((((((dfg_flat_value_base_prefix) = 2 * (sto_cp_base_prefixentrycellproductouter) /\ (sto_cn_base_prefixentrycellproductouter) = 0) \/ exists ge_signed_half_base_prefixentrycellproductouteroutput. (((dfg_flat_value_base_prefix) = 2 * ge_signed_half_base_prefixentrycellproductouteroutput + 1 /\ (sto_cp_base_prefixentrycellproductouter) = 0) /\ (sto_cn_base_prefixentrycellproductouter) = S ge_signed_half_base_prefixentrycellproductouteroutput))) /\ ((sto_ap_base_prefixentrycellproductouter * sto_bp_base_prefixentrycellproductouter + sto_an_base_prefixentrycellproductouter * sto_bn_base_prefixentrycellproductouter) + sto_cn_base_prefixentrycellproductouter = (sto_ap_base_prefixentrycellproductouter * sto_bn_base_prefixentrycellproductouter + sto_an_base_prefixentrycellproductouter * sto_bp_base_prefixentrycellproductouter) + sto_cp_base_prefixentrycellproductouter))))))))))))))))))))) \/ ((((dfg_flat_row_base_prefixentry)=0 \/ ((dfg_flat_column_base_prefixentry)=0 \/ ~(exists pvs_factor_base_prefixentrycellomittednondivisor. (n) = ((dfg_flat_row_base_prefixentry)*(dfg_flat_column_base_prefixentry)) * pvs_factor_base_prefixentrycellomittednondivisor))) /\ ((dfg_flat_value_base_prefix)=0)))))))))))