dirichlet_grid_entry_omitted

Exact expanded first-order arithmetic statement

forall F G H n a e. ((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omit_guardnondivisor. (n) = ((a)*(e)) * pvs_factor_omit_guardnondivisor))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_omit_result dfg_first_omit_result dfg_last_omit_result dfg_value_omit_result. (((n)=((a)*(e))*dfg_middle_omit_result) /\ (((exists dst_positive_code_omit_resultfirst dst_positive_scale_omit_resultfirst dst_negative_code_omit_resultfirst dst_negative_scale_omit_resultfirst dst_positive_omit_resultfirst dst_negative_omit_resultfirst. (((F) = (((((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) * S ((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) + ((dst_positive_scale_omit_resultfirst) + (dst_positive_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))) * S ((((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) * S ((dst_positive_code_omit_resultfirst) + (dst_positive_scale_omit_resultfirst)) + ((dst_positive_scale_omit_resultfirst) + (dst_positive_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))) + ((((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst))) + (((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) * S ((dst_negative_code_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)) + ((dst_negative_scale_omit_resultfirst) + (dst_negative_scale_omit_resultfirst)))))) /\ (((((exists ff_h_pvs_omit_resultfirstpositive. ff_h_pvs_omit_resultfirstpositive + S (dst_positive_omit_resultfirst) = S ((S (a)) * dst_positive_scale_omit_resultfirst)) /\ exists ff_q_pvs_omit_resultfirstpositive. dst_positive_code_omit_resultfirst = ff_q_pvs_omit_resultfirstpositive * S ((S (a)) * dst_positive_scale_omit_resultfirst) + (dst_positive_omit_resultfirst))) /\ (((((exists ff_h_pvs_omit_resultfirstnegative. ff_h_pvs_omit_resultfirstnegative + S (dst_negative_omit_resultfirst) = S ((S (a)) * dst_negative_scale_omit_resultfirst)) /\ exists ff_q_pvs_omit_resultfirstnegative. dst_negative_code_omit_resultfirst = ff_q_pvs_omit_resultfirstnegative * S ((S (a)) * dst_negative_scale_omit_resultfirst) + (dst_negative_omit_resultfirst))) /\ (exists ge_balance_positive_omit_resultfirstvalue ge_balance_negative_omit_resultfirstvalue. (((((dfg_first_omit_result) = 2 * (ge_balance_positive_omit_resultfirstvalue) /\ (ge_balance_negative_omit_resultfirstvalue) = 0) \/ exists ge_signed_half_omit_resultfirstvaluedecode. (((dfg_first_omit_result) = 2 * ge_signed_half_omit_resultfirstvaluedecode + 1 /\ (ge_balance_positive_omit_resultfirstvalue) = 0) /\ (ge_balance_negative_omit_resultfirstvalue) = S ge_signed_half_omit_resultfirstvaluedecode))) /\ ((dst_positive_omit_resultfirst) + ge_balance_negative_omit_resultfirstvalue = (dst_negative_omit_resultfirst) + ge_balance_positive_omit_resultfirstvalue))))))))) /\ (((exists dst_positive_code_omit_resultlast dst_positive_scale_omit_resultlast dst_negative_code_omit_resultlast dst_negative_scale_omit_resultlast dst_positive_omit_resultlast dst_negative_omit_resultlast. (((H) = (((((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) * S ((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) + ((dst_positive_scale_omit_resultlast) + (dst_positive_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))) * S ((((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) * S ((dst_positive_code_omit_resultlast) + (dst_positive_scale_omit_resultlast)) + ((dst_positive_scale_omit_resultlast) + (dst_positive_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))) + ((((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast))) + (((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) * S ((dst_negative_code_omit_resultlast) + (dst_negative_scale_omit_resultlast)) + ((dst_negative_scale_omit_resultlast) + (dst_negative_scale_omit_resultlast)))))) /\ (((((exists ff_h_pvs_omit_resultlastpositive. ff_h_pvs_omit_resultlastpositive + S (dst_positive_omit_resultlast) = S ((S (e)) * dst_positive_scale_omit_resultlast)) /\ exists ff_q_pvs_omit_resultlastpositive. dst_positive_code_omit_resultlast = ff_q_pvs_omit_resultlastpositive * S ((S (e)) * dst_positive_scale_omit_resultlast) + (dst_positive_omit_resultlast))) /\ (((((exists ff_h_pvs_omit_resultlastnegative. ff_h_pvs_omit_resultlastnegative + S (dst_negative_omit_resultlast) = S ((S (e)) * dst_negative_scale_omit_resultlast)) /\ exists ff_q_pvs_omit_resultlastnegative. dst_negative_code_omit_resultlast = ff_q_pvs_omit_resultlastnegative * S ((S (e)) * dst_negative_scale_omit_resultlast) + (dst_negative_omit_resultlast))) /\ (exists ge_balance_positive_omit_resultlastvalue ge_balance_negative_omit_resultlastvalue. (((((dfg_last_omit_result) = 2 * (ge_balance_positive_omit_resultlastvalue) /\ (ge_balance_negative_omit_resultlastvalue) = 0) \/ exists ge_signed_half_omit_resultlastvaluedecode. (((dfg_last_omit_result) = 2 * ge_signed_half_omit_resultlastvaluedecode + 1 /\ (ge_balance_positive_omit_resultlastvalue) = 0) /\ (ge_balance_negative_omit_resultlastvalue) = S ge_signed_half_omit_resultlastvaluedecode))) /\ ((dst_positive_omit_resultlast) + ge_balance_negative_omit_resultlastvalue = (dst_negative_omit_resultlast) + ge_balance_positive_omit_resultlastvalue))))))))) /\ (((exists dst_positive_code_omit_resultmiddle dst_positive_scale_omit_resultmiddle dst_negative_code_omit_resultmiddle dst_negative_scale_omit_resultmiddle dst_positive_omit_resultmiddle dst_negative_omit_resultmiddle. (((G) = (((((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) * S ((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) + ((dst_positive_scale_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))) * S ((((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) * S ((dst_positive_code_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle)) + ((dst_positive_scale_omit_resultmiddle) + (dst_positive_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))) + ((((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle))) + (((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) * S ((dst_negative_code_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)) + ((dst_negative_scale_omit_resultmiddle) + (dst_negative_scale_omit_resultmiddle)))))) /\ (((((exists ff_h_pvs_omit_resultmiddlepositive. ff_h_pvs_omit_resultmiddlepositive + S (dst_positive_omit_resultmiddle) = S ((S (dfg_middle_omit_result)) * dst_positive_scale_omit_resultmiddle)) /\ exists ff_q_pvs_omit_resultmiddlepositive. dst_positive_code_omit_resultmiddle = ff_q_pvs_omit_resultmiddlepositive * S ((S (dfg_middle_omit_result)) * dst_positive_scale_omit_resultmiddle) + (dst_positive_omit_resultmiddle))) /\ (((((exists ff_h_pvs_omit_resultmiddlenegative. ff_h_pvs_omit_resultmiddlenegative + S (dst_negative_omit_resultmiddle) = S ((S (dfg_middle_omit_result)) * dst_negative_scale_omit_resultmiddle)) /\ exists ff_q_pvs_omit_resultmiddlenegative. dst_negative_code_omit_resultmiddle = ff_q_pvs_omit_resultmiddlenegative * S ((S (dfg_middle_omit_result)) * dst_negative_scale_omit_resultmiddle) + (dst_negative_omit_resultmiddle))) /\ (exists ge_balance_positive_omit_resultmiddlevalue ge_balance_negative_omit_resultmiddlevalue. (((((dfg_value_omit_result) = 2 * (ge_balance_positive_omit_resultmiddlevalue) /\ (ge_balance_negative_omit_resultmiddlevalue) = 0) \/ exists ge_signed_half_omit_resultmiddlevaluedecode. (((dfg_value_omit_result) = 2 * ge_signed_half_omit_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_omit_resultmiddlevalue) = 0) /\ (ge_balance_negative_omit_resultmiddlevalue) = S ge_signed_half_omit_resultmiddlevaluedecode))) /\ ((dst_positive_omit_resultmiddle) + ge_balance_negative_omit_resultmiddlevalue = (dst_negative_omit_resultmiddle) + ge_balance_positive_omit_resultmiddlevalue))))))))) /\ (exists dfg_inner_omit_resultproduct. ((exists sto_ap_omit_resultproductinner sto_an_omit_resultproductinner sto_bp_omit_resultproductinner sto_bn_omit_resultproductinner sto_cp_omit_resultproductinner sto_cn_omit_resultproductinner. (((((dfg_last_omit_result) = 2 * (sto_ap_omit_resultproductinner) /\ (sto_an_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinnerleft. (((dfg_last_omit_result) = 2 * ge_signed_half_omit_resultproductinnerleft + 1 /\ (sto_ap_omit_resultproductinner) = 0) /\ (sto_an_omit_resultproductinner) = S ge_signed_half_omit_resultproductinnerleft))) /\ ((((((dfg_value_omit_result) = 2 * (sto_bp_omit_resultproductinner) /\ (sto_bn_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinnerright. (((dfg_value_omit_result) = 2 * ge_signed_half_omit_resultproductinnerright + 1 /\ (sto_bp_omit_resultproductinner) = 0) /\ (sto_bn_omit_resultproductinner) = S ge_signed_half_omit_resultproductinnerright))) /\ ((((((dfg_inner_omit_resultproduct) = 2 * (sto_cp_omit_resultproductinner) /\ (sto_cn_omit_resultproductinner) = 0) \/ exists ge_signed_half_omit_resultproductinneroutput. (((dfg_inner_omit_resultproduct) = 2 * ge_signed_half_omit_resultproductinneroutput + 1 /\ (sto_cp_omit_resultproductinner) = 0) /\ (sto_cn_omit_resultproductinner) = S ge_signed_half_omit_resultproductinneroutput))) /\ ((sto_ap_omit_resultproductinner * sto_bp_omit_resultproductinner + sto_an_omit_resultproductinner * sto_bn_omit_resultproductinner) + sto_cn_omit_resultproductinner = (sto_ap_omit_resultproductinner * sto_bn_omit_resultproductinner + sto_an_omit_resultproductinner * sto_bp_omit_resultproductinner) + sto_cp_omit_resultproductinner))))))) /\ (exists sto_ap_omit_resultproductouter sto_an_omit_resultproductouter sto_bp_omit_resultproductouter sto_bn_omit_resultproductouter sto_cp_omit_resultproductouter sto_cn_omit_resultproductouter. (((((dfg_first_omit_result) = 2 * (sto_ap_omit_resultproductouter) /\ (sto_an_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouterleft. (((dfg_first_omit_result) = 2 * ge_signed_half_omit_resultproductouterleft + 1 /\ (sto_ap_omit_resultproductouter) = 0) /\ (sto_an_omit_resultproductouter) = S ge_signed_half_omit_resultproductouterleft))) /\ ((((((dfg_inner_omit_resultproduct) = 2 * (sto_bp_omit_resultproductouter) /\ (sto_bn_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouterright. (((dfg_inner_omit_resultproduct) = 2 * ge_signed_half_omit_resultproductouterright + 1 /\ (sto_bp_omit_resultproductouter) = 0) /\ (sto_bn_omit_resultproductouter) = S ge_signed_half_omit_resultproductouterright))) /\ ((((((0) = 2 * (sto_cp_omit_resultproductouter) /\ (sto_cn_omit_resultproductouter) = 0) \/ exists ge_signed_half_omit_resultproductouteroutput. (((0) = 2 * ge_signed_half_omit_resultproductouteroutput + 1 /\ (sto_cp_omit_resultproductouter) = 0) /\ (sto_cn_omit_resultproductouter) = S ge_signed_half_omit_resultproductouteroutput))) /\ ((sto_ap_omit_resultproductouter * sto_bp_omit_resultproductouter + sto_an_omit_resultproductouter * sto_bn_omit_resultproductouter) + sto_cn_omit_resultproductouter = (sto_ap_omit_resultproductouter * sto_bn_omit_resultproductouter + sto_an_omit_resultproductouter * sto_bp_omit_resultproductouter) + sto_cp_omit_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_omit_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_omit_resultomittednondivisor))) /\ ((0)=0))))