dirichlet_grid_nondivisor_row_value_zero

Exact expanded first-order arithmetic statement

forall F G H n a e z. (a=0 \/ ~(exists pvs_factor_zero_row_guard. (n) = (a) * pvs_factor_zero_row_guard)) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_zero_row_cell dfg_first_zero_row_cell dfg_last_zero_row_cell dfg_value_zero_row_cell. (((n)=((a)*(e))*dfg_middle_zero_row_cell) /\ (((exists dst_positive_code_zero_row_cellfirst dst_positive_scale_zero_row_cellfirst dst_negative_code_zero_row_cellfirst dst_negative_scale_zero_row_cellfirst dst_positive_zero_row_cellfirst dst_negative_zero_row_cellfirst. (((F) = (((((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) * S ((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) + ((dst_positive_scale_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))) * S ((((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) * S ((dst_positive_code_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst)) + ((dst_positive_scale_zero_row_cellfirst) + (dst_positive_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))) + ((((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst))) + (((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) * S ((dst_negative_code_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)) + ((dst_negative_scale_zero_row_cellfirst) + (dst_negative_scale_zero_row_cellfirst)))))) /\ (((((exists ff_h_pvs_zero_row_cellfirstpositive. ff_h_pvs_zero_row_cellfirstpositive + S (dst_positive_zero_row_cellfirst) = S ((S (a)) * dst_positive_scale_zero_row_cellfirst)) /\ exists ff_q_pvs_zero_row_cellfirstpositive. dst_positive_code_zero_row_cellfirst = ff_q_pvs_zero_row_cellfirstpositive * S ((S (a)) * dst_positive_scale_zero_row_cellfirst) + (dst_positive_zero_row_cellfirst))) /\ (((((exists ff_h_pvs_zero_row_cellfirstnegative. ff_h_pvs_zero_row_cellfirstnegative + S (dst_negative_zero_row_cellfirst) = S ((S (a)) * dst_negative_scale_zero_row_cellfirst)) /\ exists ff_q_pvs_zero_row_cellfirstnegative. dst_negative_code_zero_row_cellfirst = ff_q_pvs_zero_row_cellfirstnegative * S ((S (a)) * dst_negative_scale_zero_row_cellfirst) + (dst_negative_zero_row_cellfirst))) /\ (exists ge_balance_positive_zero_row_cellfirstvalue ge_balance_negative_zero_row_cellfirstvalue. (((((dfg_first_zero_row_cell) = 2 * (ge_balance_positive_zero_row_cellfirstvalue) /\ (ge_balance_negative_zero_row_cellfirstvalue) = 0) \/ exists ge_signed_half_zero_row_cellfirstvaluedecode. (((dfg_first_zero_row_cell) = 2 * ge_signed_half_zero_row_cellfirstvaluedecode + 1 /\ (ge_balance_positive_zero_row_cellfirstvalue) = 0) /\ (ge_balance_negative_zero_row_cellfirstvalue) = S ge_signed_half_zero_row_cellfirstvaluedecode))) /\ ((dst_positive_zero_row_cellfirst) + ge_balance_negative_zero_row_cellfirstvalue = (dst_negative_zero_row_cellfirst) + ge_balance_positive_zero_row_cellfirstvalue))))))))) /\ (((exists dst_positive_code_zero_row_celllast dst_positive_scale_zero_row_celllast dst_negative_code_zero_row_celllast dst_negative_scale_zero_row_celllast dst_positive_zero_row_celllast dst_negative_zero_row_celllast. (((H) = (((((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) * S ((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) + ((dst_positive_scale_zero_row_celllast) + (dst_positive_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))) * S ((((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) * S ((dst_positive_code_zero_row_celllast) + (dst_positive_scale_zero_row_celllast)) + ((dst_positive_scale_zero_row_celllast) + (dst_positive_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))) + ((((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast))) + (((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) * S ((dst_negative_code_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)) + ((dst_negative_scale_zero_row_celllast) + (dst_negative_scale_zero_row_celllast)))))) /\ (((((exists ff_h_pvs_zero_row_celllastpositive. ff_h_pvs_zero_row_celllastpositive + S (dst_positive_zero_row_celllast) = S ((S (e)) * dst_positive_scale_zero_row_celllast)) /\ exists ff_q_pvs_zero_row_celllastpositive. dst_positive_code_zero_row_celllast = ff_q_pvs_zero_row_celllastpositive * S ((S (e)) * dst_positive_scale_zero_row_celllast) + (dst_positive_zero_row_celllast))) /\ (((((exists ff_h_pvs_zero_row_celllastnegative. ff_h_pvs_zero_row_celllastnegative + S (dst_negative_zero_row_celllast) = S ((S (e)) * dst_negative_scale_zero_row_celllast)) /\ exists ff_q_pvs_zero_row_celllastnegative. dst_negative_code_zero_row_celllast = ff_q_pvs_zero_row_celllastnegative * S ((S (e)) * dst_negative_scale_zero_row_celllast) + (dst_negative_zero_row_celllast))) /\ (exists ge_balance_positive_zero_row_celllastvalue ge_balance_negative_zero_row_celllastvalue. (((((dfg_last_zero_row_cell) = 2 * (ge_balance_positive_zero_row_celllastvalue) /\ (ge_balance_negative_zero_row_celllastvalue) = 0) \/ exists ge_signed_half_zero_row_celllastvaluedecode. (((dfg_last_zero_row_cell) = 2 * ge_signed_half_zero_row_celllastvaluedecode + 1 /\ (ge_balance_positive_zero_row_celllastvalue) = 0) /\ (ge_balance_negative_zero_row_celllastvalue) = S ge_signed_half_zero_row_celllastvaluedecode))) /\ ((dst_positive_zero_row_celllast) + ge_balance_negative_zero_row_celllastvalue = (dst_negative_zero_row_celllast) + ge_balance_positive_zero_row_celllastvalue))))))))) /\ (((exists dst_positive_code_zero_row_cellmiddle dst_positive_scale_zero_row_cellmiddle dst_negative_code_zero_row_cellmiddle dst_negative_scale_zero_row_cellmiddle dst_positive_zero_row_cellmiddle dst_negative_zero_row_cellmiddle. (((G) = (((((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) * S ((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) + ((dst_positive_scale_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))) * S ((((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) * S ((dst_positive_code_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle)) + ((dst_positive_scale_zero_row_cellmiddle) + (dst_positive_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))) + ((((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle))) + (((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) * S ((dst_negative_code_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)) + ((dst_negative_scale_zero_row_cellmiddle) + (dst_negative_scale_zero_row_cellmiddle)))))) /\ (((((exists ff_h_pvs_zero_row_cellmiddlepositive. ff_h_pvs_zero_row_cellmiddlepositive + S (dst_positive_zero_row_cellmiddle) = S ((S (dfg_middle_zero_row_cell)) * dst_positive_scale_zero_row_cellmiddle)) /\ exists ff_q_pvs_zero_row_cellmiddlepositive. dst_positive_code_zero_row_cellmiddle = ff_q_pvs_zero_row_cellmiddlepositive * S ((S (dfg_middle_zero_row_cell)) * dst_positive_scale_zero_row_cellmiddle) + (dst_positive_zero_row_cellmiddle))) /\ (((((exists ff_h_pvs_zero_row_cellmiddlenegative. ff_h_pvs_zero_row_cellmiddlenegative + S (dst_negative_zero_row_cellmiddle) = S ((S (dfg_middle_zero_row_cell)) * dst_negative_scale_zero_row_cellmiddle)) /\ exists ff_q_pvs_zero_row_cellmiddlenegative. dst_negative_code_zero_row_cellmiddle = ff_q_pvs_zero_row_cellmiddlenegative * S ((S (dfg_middle_zero_row_cell)) * dst_negative_scale_zero_row_cellmiddle) + (dst_negative_zero_row_cellmiddle))) /\ (exists ge_balance_positive_zero_row_cellmiddlevalue ge_balance_negative_zero_row_cellmiddlevalue. (((((dfg_value_zero_row_cell) = 2 * (ge_balance_positive_zero_row_cellmiddlevalue) /\ (ge_balance_negative_zero_row_cellmiddlevalue) = 0) \/ exists ge_signed_half_zero_row_cellmiddlevaluedecode. (((dfg_value_zero_row_cell) = 2 * ge_signed_half_zero_row_cellmiddlevaluedecode + 1 /\ (ge_balance_positive_zero_row_cellmiddlevalue) = 0) /\ (ge_balance_negative_zero_row_cellmiddlevalue) = S ge_signed_half_zero_row_cellmiddlevaluedecode))) /\ ((dst_positive_zero_row_cellmiddle) + ge_balance_negative_zero_row_cellmiddlevalue = (dst_negative_zero_row_cellmiddle) + ge_balance_positive_zero_row_cellmiddlevalue))))))))) /\ (exists dfg_inner_zero_row_cellproduct. ((exists sto_ap_zero_row_cellproductinner sto_an_zero_row_cellproductinner sto_bp_zero_row_cellproductinner sto_bn_zero_row_cellproductinner sto_cp_zero_row_cellproductinner sto_cn_zero_row_cellproductinner. (((((dfg_last_zero_row_cell) = 2 * (sto_ap_zero_row_cellproductinner) /\ (sto_an_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinnerleft. (((dfg_last_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductinnerleft + 1 /\ (sto_ap_zero_row_cellproductinner) = 0) /\ (sto_an_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinnerleft))) /\ ((((((dfg_value_zero_row_cell) = 2 * (sto_bp_zero_row_cellproductinner) /\ (sto_bn_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinnerright. (((dfg_value_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductinnerright + 1 /\ (sto_bp_zero_row_cellproductinner) = 0) /\ (sto_bn_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinnerright))) /\ ((((((dfg_inner_zero_row_cellproduct) = 2 * (sto_cp_zero_row_cellproductinner) /\ (sto_cn_zero_row_cellproductinner) = 0) \/ exists ge_signed_half_zero_row_cellproductinneroutput. (((dfg_inner_zero_row_cellproduct) = 2 * ge_signed_half_zero_row_cellproductinneroutput + 1 /\ (sto_cp_zero_row_cellproductinner) = 0) /\ (sto_cn_zero_row_cellproductinner) = S ge_signed_half_zero_row_cellproductinneroutput))) /\ ((sto_ap_zero_row_cellproductinner * sto_bp_zero_row_cellproductinner + sto_an_zero_row_cellproductinner * sto_bn_zero_row_cellproductinner) + sto_cn_zero_row_cellproductinner = (sto_ap_zero_row_cellproductinner * sto_bn_zero_row_cellproductinner + sto_an_zero_row_cellproductinner * sto_bp_zero_row_cellproductinner) + sto_cp_zero_row_cellproductinner))))))) /\ (exists sto_ap_zero_row_cellproductouter sto_an_zero_row_cellproductouter sto_bp_zero_row_cellproductouter sto_bn_zero_row_cellproductouter sto_cp_zero_row_cellproductouter sto_cn_zero_row_cellproductouter. (((((dfg_first_zero_row_cell) = 2 * (sto_ap_zero_row_cellproductouter) /\ (sto_an_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouterleft. (((dfg_first_zero_row_cell) = 2 * ge_signed_half_zero_row_cellproductouterleft + 1 /\ (sto_ap_zero_row_cellproductouter) = 0) /\ (sto_an_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouterleft))) /\ ((((((dfg_inner_zero_row_cellproduct) = 2 * (sto_bp_zero_row_cellproductouter) /\ (sto_bn_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouterright. (((dfg_inner_zero_row_cellproduct) = 2 * ge_signed_half_zero_row_cellproductouterright + 1 /\ (sto_bp_zero_row_cellproductouter) = 0) /\ (sto_bn_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouterright))) /\ ((((((z) = 2 * (sto_cp_zero_row_cellproductouter) /\ (sto_cn_zero_row_cellproductouter) = 0) \/ exists ge_signed_half_zero_row_cellproductouteroutput. (((z) = 2 * ge_signed_half_zero_row_cellproductouteroutput + 1 /\ (sto_cp_zero_row_cellproductouter) = 0) /\ (sto_cn_zero_row_cellproductouter) = S ge_signed_half_zero_row_cellproductouteroutput))) /\ ((sto_ap_zero_row_cellproductouter * sto_bp_zero_row_cellproductouter + sto_an_zero_row_cellproductouter * sto_bn_zero_row_cellproductouter) + sto_cn_zero_row_cellproductouter = (sto_ap_zero_row_cellproductouter * sto_bn_zero_row_cellproductouter + sto_an_zero_row_cellproductouter * sto_bp_zero_row_cellproductouter) + sto_cp_zero_row_cellproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_zero_row_cellomittednondivisor. (n) = ((a)*(e)) * pvs_factor_zero_row_cellomittednondivisor))) /\ ((z)=0)))) -> z=0