dirichlet_grid_entry_from_factorization

Exact expanded first-order arithmetic statement

forall F G H n a e c u v w r z. ~(a=0) -> ~(e=0) -> n=(a*e)*c -> (exists dst_positive_code_factor_first dst_positive_scale_factor_first dst_negative_code_factor_first dst_negative_scale_factor_first dst_positive_factor_first dst_negative_factor_first. (((F) = (((((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) * S ((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) + ((dst_positive_scale_factor_first) + (dst_positive_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))) * S ((((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) * S ((dst_positive_code_factor_first) + (dst_positive_scale_factor_first)) + ((dst_positive_scale_factor_first) + (dst_positive_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))) + ((((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first))) + (((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) * S ((dst_negative_code_factor_first) + (dst_negative_scale_factor_first)) + ((dst_negative_scale_factor_first) + (dst_negative_scale_factor_first)))))) /\ (((((exists ff_h_pvs_factor_firstpositive. ff_h_pvs_factor_firstpositive + S (dst_positive_factor_first) = S ((S (a)) * dst_positive_scale_factor_first)) /\ exists ff_q_pvs_factor_firstpositive. dst_positive_code_factor_first = ff_q_pvs_factor_firstpositive * S ((S (a)) * dst_positive_scale_factor_first) + (dst_positive_factor_first))) /\ (((((exists ff_h_pvs_factor_firstnegative. ff_h_pvs_factor_firstnegative + S (dst_negative_factor_first) = S ((S (a)) * dst_negative_scale_factor_first)) /\ exists ff_q_pvs_factor_firstnegative. dst_negative_code_factor_first = ff_q_pvs_factor_firstnegative * S ((S (a)) * dst_negative_scale_factor_first) + (dst_negative_factor_first))) /\ (exists ge_balance_positive_factor_firstvalue ge_balance_negative_factor_firstvalue. (((((u) = 2 * (ge_balance_positive_factor_firstvalue) /\ (ge_balance_negative_factor_firstvalue) = 0) \/ exists ge_signed_half_factor_firstvaluedecode. (((u) = 2 * ge_signed_half_factor_firstvaluedecode + 1 /\ (ge_balance_positive_factor_firstvalue) = 0) /\ (ge_balance_negative_factor_firstvalue) = S ge_signed_half_factor_firstvaluedecode))) /\ ((dst_positive_factor_first) + ge_balance_negative_factor_firstvalue = (dst_negative_factor_first) + ge_balance_positive_factor_firstvalue))))))))) -> (exists dst_positive_code_factor_last dst_positive_scale_factor_last dst_negative_code_factor_last dst_negative_scale_factor_last dst_positive_factor_last dst_negative_factor_last. (((H) = (((((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) * S ((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) + ((dst_positive_scale_factor_last) + (dst_positive_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))) * S ((((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) * S ((dst_positive_code_factor_last) + (dst_positive_scale_factor_last)) + ((dst_positive_scale_factor_last) + (dst_positive_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))) + ((((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last))) + (((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) * S ((dst_negative_code_factor_last) + (dst_negative_scale_factor_last)) + ((dst_negative_scale_factor_last) + (dst_negative_scale_factor_last)))))) /\ (((((exists ff_h_pvs_factor_lastpositive. ff_h_pvs_factor_lastpositive + S (dst_positive_factor_last) = S ((S (e)) * dst_positive_scale_factor_last)) /\ exists ff_q_pvs_factor_lastpositive. dst_positive_code_factor_last = ff_q_pvs_factor_lastpositive * S ((S (e)) * dst_positive_scale_factor_last) + (dst_positive_factor_last))) /\ (((((exists ff_h_pvs_factor_lastnegative. ff_h_pvs_factor_lastnegative + S (dst_negative_factor_last) = S ((S (e)) * dst_negative_scale_factor_last)) /\ exists ff_q_pvs_factor_lastnegative. dst_negative_code_factor_last = ff_q_pvs_factor_lastnegative * S ((S (e)) * dst_negative_scale_factor_last) + (dst_negative_factor_last))) /\ (exists ge_balance_positive_factor_lastvalue ge_balance_negative_factor_lastvalue. (((((v) = 2 * (ge_balance_positive_factor_lastvalue) /\ (ge_balance_negative_factor_lastvalue) = 0) \/ exists ge_signed_half_factor_lastvaluedecode. (((v) = 2 * ge_signed_half_factor_lastvaluedecode + 1 /\ (ge_balance_positive_factor_lastvalue) = 0) /\ (ge_balance_negative_factor_lastvalue) = S ge_signed_half_factor_lastvaluedecode))) /\ ((dst_positive_factor_last) + ge_balance_negative_factor_lastvalue = (dst_negative_factor_last) + ge_balance_positive_factor_lastvalue))))))))) -> (exists dst_positive_code_factor_middle dst_positive_scale_factor_middle dst_negative_code_factor_middle dst_negative_scale_factor_middle dst_positive_factor_middle dst_negative_factor_middle. (((G) = (((((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) * S ((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) + ((dst_positive_scale_factor_middle) + (dst_positive_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))) * S ((((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) * S ((dst_positive_code_factor_middle) + (dst_positive_scale_factor_middle)) + ((dst_positive_scale_factor_middle) + (dst_positive_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))) + ((((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle))) + (((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) * S ((dst_negative_code_factor_middle) + (dst_negative_scale_factor_middle)) + ((dst_negative_scale_factor_middle) + (dst_negative_scale_factor_middle)))))) /\ (((((exists ff_h_pvs_factor_middlepositive. ff_h_pvs_factor_middlepositive + S (dst_positive_factor_middle) = S ((S (c)) * dst_positive_scale_factor_middle)) /\ exists ff_q_pvs_factor_middlepositive. dst_positive_code_factor_middle = ff_q_pvs_factor_middlepositive * S ((S (c)) * dst_positive_scale_factor_middle) + (dst_positive_factor_middle))) /\ (((((exists ff_h_pvs_factor_middlenegative. ff_h_pvs_factor_middlenegative + S (dst_negative_factor_middle) = S ((S (c)) * dst_negative_scale_factor_middle)) /\ exists ff_q_pvs_factor_middlenegative. dst_negative_code_factor_middle = ff_q_pvs_factor_middlenegative * S ((S (c)) * dst_negative_scale_factor_middle) + (dst_negative_factor_middle))) /\ (exists ge_balance_positive_factor_middlevalue ge_balance_negative_factor_middlevalue. (((((w) = 2 * (ge_balance_positive_factor_middlevalue) /\ (ge_balance_negative_factor_middlevalue) = 0) \/ exists ge_signed_half_factor_middlevaluedecode. (((w) = 2 * ge_signed_half_factor_middlevaluedecode + 1 /\ (ge_balance_positive_factor_middlevalue) = 0) /\ (ge_balance_negative_factor_middlevalue) = S ge_signed_half_factor_middlevaluedecode))) /\ ((dst_positive_factor_middle) + ge_balance_negative_factor_middlevalue = (dst_negative_factor_middle) + ge_balance_positive_factor_middlevalue))))))))) -> (exists sto_ap_factor_inner sto_an_factor_inner sto_bp_factor_inner sto_bn_factor_inner sto_cp_factor_inner sto_cn_factor_inner. (((((v) = 2 * (sto_ap_factor_inner) /\ (sto_an_factor_inner) = 0) \/ exists ge_signed_half_factor_innerleft. (((v) = 2 * ge_signed_half_factor_innerleft + 1 /\ (sto_ap_factor_inner) = 0) /\ (sto_an_factor_inner) = S ge_signed_half_factor_innerleft))) /\ ((((((w) = 2 * (sto_bp_factor_inner) /\ (sto_bn_factor_inner) = 0) \/ exists ge_signed_half_factor_innerright. (((w) = 2 * ge_signed_half_factor_innerright + 1 /\ (sto_bp_factor_inner) = 0) /\ (sto_bn_factor_inner) = S ge_signed_half_factor_innerright))) /\ ((((((r) = 2 * (sto_cp_factor_inner) /\ (sto_cn_factor_inner) = 0) \/ exists ge_signed_half_factor_inneroutput. (((r) = 2 * ge_signed_half_factor_inneroutput + 1 /\ (sto_cp_factor_inner) = 0) /\ (sto_cn_factor_inner) = S ge_signed_half_factor_inneroutput))) /\ ((sto_ap_factor_inner * sto_bp_factor_inner + sto_an_factor_inner * sto_bn_factor_inner) + sto_cn_factor_inner = (sto_ap_factor_inner * sto_bn_factor_inner + sto_an_factor_inner * sto_bp_factor_inner) + sto_cp_factor_inner))))))) -> (exists sto_ap_factor_outer sto_an_factor_outer sto_bp_factor_outer sto_bn_factor_outer sto_cp_factor_outer sto_cn_factor_outer. (((((u) = 2 * (sto_ap_factor_outer) /\ (sto_an_factor_outer) = 0) \/ exists ge_signed_half_factor_outerleft. (((u) = 2 * ge_signed_half_factor_outerleft + 1 /\ (sto_ap_factor_outer) = 0) /\ (sto_an_factor_outer) = S ge_signed_half_factor_outerleft))) /\ ((((((r) = 2 * (sto_bp_factor_outer) /\ (sto_bn_factor_outer) = 0) \/ exists ge_signed_half_factor_outerright. (((r) = 2 * ge_signed_half_factor_outerright + 1 /\ (sto_bp_factor_outer) = 0) /\ (sto_bn_factor_outer) = S ge_signed_half_factor_outerright))) /\ ((((((z) = 2 * (sto_cp_factor_outer) /\ (sto_cn_factor_outer) = 0) \/ exists ge_signed_half_factor_outeroutput. (((z) = 2 * ge_signed_half_factor_outeroutput + 1 /\ (sto_cp_factor_outer) = 0) /\ (sto_cn_factor_outer) = S ge_signed_half_factor_outeroutput))) /\ ((sto_ap_factor_outer * sto_bp_factor_outer + sto_an_factor_outer * sto_bn_factor_outer) + sto_cn_factor_outer = (sto_ap_factor_outer * sto_bn_factor_outer + sto_an_factor_outer * sto_bp_factor_outer) + sto_cp_factor_outer))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_factor_result dfg_first_factor_result dfg_last_factor_result dfg_value_factor_result. (((n)=((a)*(e))*dfg_middle_factor_result) /\ (((exists dst_positive_code_factor_resultfirst dst_positive_scale_factor_resultfirst dst_negative_code_factor_resultfirst dst_negative_scale_factor_resultfirst dst_positive_factor_resultfirst dst_negative_factor_resultfirst. (((F) = (((((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) * S ((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) + ((dst_positive_scale_factor_resultfirst) + (dst_positive_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))) * S ((((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) * S ((dst_positive_code_factor_resultfirst) + (dst_positive_scale_factor_resultfirst)) + ((dst_positive_scale_factor_resultfirst) + (dst_positive_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))) + ((((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst))) + (((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) * S ((dst_negative_code_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)) + ((dst_negative_scale_factor_resultfirst) + (dst_negative_scale_factor_resultfirst)))))) /\ (((((exists ff_h_pvs_factor_resultfirstpositive. ff_h_pvs_factor_resultfirstpositive + S (dst_positive_factor_resultfirst) = S ((S (a)) * dst_positive_scale_factor_resultfirst)) /\ exists ff_q_pvs_factor_resultfirstpositive. dst_positive_code_factor_resultfirst = ff_q_pvs_factor_resultfirstpositive * S ((S (a)) * dst_positive_scale_factor_resultfirst) + (dst_positive_factor_resultfirst))) /\ (((((exists ff_h_pvs_factor_resultfirstnegative. ff_h_pvs_factor_resultfirstnegative + S (dst_negative_factor_resultfirst) = S ((S (a)) * dst_negative_scale_factor_resultfirst)) /\ exists ff_q_pvs_factor_resultfirstnegative. dst_negative_code_factor_resultfirst = ff_q_pvs_factor_resultfirstnegative * S ((S (a)) * dst_negative_scale_factor_resultfirst) + (dst_negative_factor_resultfirst))) /\ (exists ge_balance_positive_factor_resultfirstvalue ge_balance_negative_factor_resultfirstvalue. (((((dfg_first_factor_result) = 2 * (ge_balance_positive_factor_resultfirstvalue) /\ (ge_balance_negative_factor_resultfirstvalue) = 0) \/ exists ge_signed_half_factor_resultfirstvaluedecode. (((dfg_first_factor_result) = 2 * ge_signed_half_factor_resultfirstvaluedecode + 1 /\ (ge_balance_positive_factor_resultfirstvalue) = 0) /\ (ge_balance_negative_factor_resultfirstvalue) = S ge_signed_half_factor_resultfirstvaluedecode))) /\ ((dst_positive_factor_resultfirst) + ge_balance_negative_factor_resultfirstvalue = (dst_negative_factor_resultfirst) + ge_balance_positive_factor_resultfirstvalue))))))))) /\ (((exists dst_positive_code_factor_resultlast dst_positive_scale_factor_resultlast dst_negative_code_factor_resultlast dst_negative_scale_factor_resultlast dst_positive_factor_resultlast dst_negative_factor_resultlast. (((H) = (((((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) * S ((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) + ((dst_positive_scale_factor_resultlast) + (dst_positive_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))) * S ((((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) * S ((dst_positive_code_factor_resultlast) + (dst_positive_scale_factor_resultlast)) + ((dst_positive_scale_factor_resultlast) + (dst_positive_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))) + ((((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast))) + (((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) * S ((dst_negative_code_factor_resultlast) + (dst_negative_scale_factor_resultlast)) + ((dst_negative_scale_factor_resultlast) + (dst_negative_scale_factor_resultlast)))))) /\ (((((exists ff_h_pvs_factor_resultlastpositive. ff_h_pvs_factor_resultlastpositive + S (dst_positive_factor_resultlast) = S ((S (e)) * dst_positive_scale_factor_resultlast)) /\ exists ff_q_pvs_factor_resultlastpositive. dst_positive_code_factor_resultlast = ff_q_pvs_factor_resultlastpositive * S ((S (e)) * dst_positive_scale_factor_resultlast) + (dst_positive_factor_resultlast))) /\ (((((exists ff_h_pvs_factor_resultlastnegative. ff_h_pvs_factor_resultlastnegative + S (dst_negative_factor_resultlast) = S ((S (e)) * dst_negative_scale_factor_resultlast)) /\ exists ff_q_pvs_factor_resultlastnegative. dst_negative_code_factor_resultlast = ff_q_pvs_factor_resultlastnegative * S ((S (e)) * dst_negative_scale_factor_resultlast) + (dst_negative_factor_resultlast))) /\ (exists ge_balance_positive_factor_resultlastvalue ge_balance_negative_factor_resultlastvalue. (((((dfg_last_factor_result) = 2 * (ge_balance_positive_factor_resultlastvalue) /\ (ge_balance_negative_factor_resultlastvalue) = 0) \/ exists ge_signed_half_factor_resultlastvaluedecode. (((dfg_last_factor_result) = 2 * ge_signed_half_factor_resultlastvaluedecode + 1 /\ (ge_balance_positive_factor_resultlastvalue) = 0) /\ (ge_balance_negative_factor_resultlastvalue) = S ge_signed_half_factor_resultlastvaluedecode))) /\ ((dst_positive_factor_resultlast) + ge_balance_negative_factor_resultlastvalue = (dst_negative_factor_resultlast) + ge_balance_positive_factor_resultlastvalue))))))))) /\ (((exists dst_positive_code_factor_resultmiddle dst_positive_scale_factor_resultmiddle dst_negative_code_factor_resultmiddle dst_negative_scale_factor_resultmiddle dst_positive_factor_resultmiddle dst_negative_factor_resultmiddle. (((G) = (((((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) * S ((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) + ((dst_positive_scale_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))) * S ((((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) * S ((dst_positive_code_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle)) + ((dst_positive_scale_factor_resultmiddle) + (dst_positive_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))) + ((((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle))) + (((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) * S ((dst_negative_code_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)) + ((dst_negative_scale_factor_resultmiddle) + (dst_negative_scale_factor_resultmiddle)))))) /\ (((((exists ff_h_pvs_factor_resultmiddlepositive. ff_h_pvs_factor_resultmiddlepositive + S (dst_positive_factor_resultmiddle) = S ((S (dfg_middle_factor_result)) * dst_positive_scale_factor_resultmiddle)) /\ exists ff_q_pvs_factor_resultmiddlepositive. dst_positive_code_factor_resultmiddle = ff_q_pvs_factor_resultmiddlepositive * S ((S (dfg_middle_factor_result)) * dst_positive_scale_factor_resultmiddle) + (dst_positive_factor_resultmiddle))) /\ (((((exists ff_h_pvs_factor_resultmiddlenegative. ff_h_pvs_factor_resultmiddlenegative + S (dst_negative_factor_resultmiddle) = S ((S (dfg_middle_factor_result)) * dst_negative_scale_factor_resultmiddle)) /\ exists ff_q_pvs_factor_resultmiddlenegative. dst_negative_code_factor_resultmiddle = ff_q_pvs_factor_resultmiddlenegative * S ((S (dfg_middle_factor_result)) * dst_negative_scale_factor_resultmiddle) + (dst_negative_factor_resultmiddle))) /\ (exists ge_balance_positive_factor_resultmiddlevalue ge_balance_negative_factor_resultmiddlevalue. (((((dfg_value_factor_result) = 2 * (ge_balance_positive_factor_resultmiddlevalue) /\ (ge_balance_negative_factor_resultmiddlevalue) = 0) \/ exists ge_signed_half_factor_resultmiddlevaluedecode. (((dfg_value_factor_result) = 2 * ge_signed_half_factor_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_factor_resultmiddlevalue) = 0) /\ (ge_balance_negative_factor_resultmiddlevalue) = S ge_signed_half_factor_resultmiddlevaluedecode))) /\ ((dst_positive_factor_resultmiddle) + ge_balance_negative_factor_resultmiddlevalue = (dst_negative_factor_resultmiddle) + ge_balance_positive_factor_resultmiddlevalue))))))))) /\ (exists dfg_inner_factor_resultproduct. ((exists sto_ap_factor_resultproductinner sto_an_factor_resultproductinner sto_bp_factor_resultproductinner sto_bn_factor_resultproductinner sto_cp_factor_resultproductinner sto_cn_factor_resultproductinner. (((((dfg_last_factor_result) = 2 * (sto_ap_factor_resultproductinner) /\ (sto_an_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinnerleft. (((dfg_last_factor_result) = 2 * ge_signed_half_factor_resultproductinnerleft + 1 /\ (sto_ap_factor_resultproductinner) = 0) /\ (sto_an_factor_resultproductinner) = S ge_signed_half_factor_resultproductinnerleft))) /\ ((((((dfg_value_factor_result) = 2 * (sto_bp_factor_resultproductinner) /\ (sto_bn_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinnerright. (((dfg_value_factor_result) = 2 * ge_signed_half_factor_resultproductinnerright + 1 /\ (sto_bp_factor_resultproductinner) = 0) /\ (sto_bn_factor_resultproductinner) = S ge_signed_half_factor_resultproductinnerright))) /\ ((((((dfg_inner_factor_resultproduct) = 2 * (sto_cp_factor_resultproductinner) /\ (sto_cn_factor_resultproductinner) = 0) \/ exists ge_signed_half_factor_resultproductinneroutput. (((dfg_inner_factor_resultproduct) = 2 * ge_signed_half_factor_resultproductinneroutput + 1 /\ (sto_cp_factor_resultproductinner) = 0) /\ (sto_cn_factor_resultproductinner) = S ge_signed_half_factor_resultproductinneroutput))) /\ ((sto_ap_factor_resultproductinner * sto_bp_factor_resultproductinner + sto_an_factor_resultproductinner * sto_bn_factor_resultproductinner) + sto_cn_factor_resultproductinner = (sto_ap_factor_resultproductinner * sto_bn_factor_resultproductinner + sto_an_factor_resultproductinner * sto_bp_factor_resultproductinner) + sto_cp_factor_resultproductinner))))))) /\ (exists sto_ap_factor_resultproductouter sto_an_factor_resultproductouter sto_bp_factor_resultproductouter sto_bn_factor_resultproductouter sto_cp_factor_resultproductouter sto_cn_factor_resultproductouter. (((((dfg_first_factor_result) = 2 * (sto_ap_factor_resultproductouter) /\ (sto_an_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouterleft. (((dfg_first_factor_result) = 2 * ge_signed_half_factor_resultproductouterleft + 1 /\ (sto_ap_factor_resultproductouter) = 0) /\ (sto_an_factor_resultproductouter) = S ge_signed_half_factor_resultproductouterleft))) /\ ((((((dfg_inner_factor_resultproduct) = 2 * (sto_bp_factor_resultproductouter) /\ (sto_bn_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouterright. (((dfg_inner_factor_resultproduct) = 2 * ge_signed_half_factor_resultproductouterright + 1 /\ (sto_bp_factor_resultproductouter) = 0) /\ (sto_bn_factor_resultproductouter) = S ge_signed_half_factor_resultproductouterright))) /\ ((((((z) = 2 * (sto_cp_factor_resultproductouter) /\ (sto_cn_factor_resultproductouter) = 0) \/ exists ge_signed_half_factor_resultproductouteroutput. (((z) = 2 * ge_signed_half_factor_resultproductouteroutput + 1 /\ (sto_cp_factor_resultproductouter) = 0) /\ (sto_cn_factor_resultproductouter) = S ge_signed_half_factor_resultproductouteroutput))) /\ ((sto_ap_factor_resultproductouter * sto_bp_factor_resultproductouter + sto_an_factor_resultproductouter * sto_bn_factor_resultproductouter) + sto_cn_factor_resultproductouter = (sto_ap_factor_resultproductouter * sto_bn_factor_resultproductouter + sto_an_factor_resultproductouter * sto_bp_factor_resultproductouter) + sto_cp_factor_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_factor_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_factor_resultomittednondivisor))) /\ ((z)=0))))