dirichlet_grid_entry_from_convolution_entry

Exact expanded first-order arithmetic statement

forall F G H n a q u e v z. ~(a=0) -> n=a*q -> (exists dst_positive_code_row_lift_first dst_positive_scale_row_lift_first dst_negative_code_row_lift_first dst_negative_scale_row_lift_first dst_positive_row_lift_first dst_negative_row_lift_first. (((F) = (((((dst_positive_code_row_lift_first) + (dst_positive_scale_row_lift_first)) * S ((dst_positive_code_row_lift_first) + (dst_positive_scale_row_lift_first)) + ((dst_positive_scale_row_lift_first) + (dst_positive_scale_row_lift_first))) + (((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) * S ((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) + ((dst_negative_scale_row_lift_first) + (dst_negative_scale_row_lift_first)))) * S ((((dst_positive_code_row_lift_first) + (dst_positive_scale_row_lift_first)) * S ((dst_positive_code_row_lift_first) + (dst_positive_scale_row_lift_first)) + ((dst_positive_scale_row_lift_first) + (dst_positive_scale_row_lift_first))) + (((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) * S ((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) + ((dst_negative_scale_row_lift_first) + (dst_negative_scale_row_lift_first)))) + ((((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) * S ((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) + ((dst_negative_scale_row_lift_first) + (dst_negative_scale_row_lift_first))) + (((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) * S ((dst_negative_code_row_lift_first) + (dst_negative_scale_row_lift_first)) + ((dst_negative_scale_row_lift_first) + (dst_negative_scale_row_lift_first)))))) /\ (((((exists ff_h_pvs_row_lift_firstpositive. ff_h_pvs_row_lift_firstpositive + S (dst_positive_row_lift_first) = S ((S (a)) * dst_positive_scale_row_lift_first)) /\ exists ff_q_pvs_row_lift_firstpositive. dst_positive_code_row_lift_first = ff_q_pvs_row_lift_firstpositive * S ((S (a)) * dst_positive_scale_row_lift_first) + (dst_positive_row_lift_first))) /\ (((((exists ff_h_pvs_row_lift_firstnegative. ff_h_pvs_row_lift_firstnegative + S (dst_negative_row_lift_first) = S ((S (a)) * dst_negative_scale_row_lift_first)) /\ exists ff_q_pvs_row_lift_firstnegative. dst_negative_code_row_lift_first = ff_q_pvs_row_lift_firstnegative * S ((S (a)) * dst_negative_scale_row_lift_first) + (dst_negative_row_lift_first))) /\ (exists ge_balance_positive_row_lift_firstvalue ge_balance_negative_row_lift_firstvalue. (((((u) = 2 * (ge_balance_positive_row_lift_firstvalue) /\ (ge_balance_negative_row_lift_firstvalue) = 0) \/ exists ge_signed_half_row_lift_firstvaluedecode. (((u) = 2 * ge_signed_half_row_lift_firstvaluedecode + 1 /\ (ge_balance_positive_row_lift_firstvalue) = 0) /\ (ge_balance_negative_row_lift_firstvalue) = S ge_signed_half_row_lift_firstvaluedecode))) /\ ((dst_positive_row_lift_first) + ge_balance_negative_row_lift_firstvalue = (dst_negative_row_lift_first) + ge_balance_positive_row_lift_firstvalue))))))))) -> ((((~((e)=0)) /\ (exists dc_quotient_row_lift_inner dc_left_row_lift_inner dc_right_row_lift_inner. (((q)=(e)*dc_quotient_row_lift_inner) /\ (((exists dst_positive_code_row_lift_innerleft dst_positive_scale_row_lift_innerleft dst_negative_code_row_lift_innerleft dst_negative_scale_row_lift_innerleft dst_positive_row_lift_innerleft dst_negative_row_lift_innerleft. (((H) = (((((dst_positive_code_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft)) * S ((dst_positive_code_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft)) + ((dst_positive_scale_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft))) + (((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) * S ((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) + ((dst_negative_scale_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)))) * S ((((dst_positive_code_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft)) * S ((dst_positive_code_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft)) + ((dst_positive_scale_row_lift_innerleft) + (dst_positive_scale_row_lift_innerleft))) + (((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) * S ((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) + ((dst_negative_scale_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)))) + ((((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) * S ((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) + ((dst_negative_scale_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft))) + (((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) * S ((dst_negative_code_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)) + ((dst_negative_scale_row_lift_innerleft) + (dst_negative_scale_row_lift_innerleft)))))) /\ (((((exists ff_h_pvs_row_lift_innerleftpositive. ff_h_pvs_row_lift_innerleftpositive + S (dst_positive_row_lift_innerleft) = S ((S (e)) * dst_positive_scale_row_lift_innerleft)) /\ exists ff_q_pvs_row_lift_innerleftpositive. dst_positive_code_row_lift_innerleft = ff_q_pvs_row_lift_innerleftpositive * S ((S (e)) * dst_positive_scale_row_lift_innerleft) + (dst_positive_row_lift_innerleft))) /\ (((((exists ff_h_pvs_row_lift_innerleftnegative. ff_h_pvs_row_lift_innerleftnegative + S (dst_negative_row_lift_innerleft) = S ((S (e)) * dst_negative_scale_row_lift_innerleft)) /\ exists ff_q_pvs_row_lift_innerleftnegative. dst_negative_code_row_lift_innerleft = ff_q_pvs_row_lift_innerleftnegative * S ((S (e)) * dst_negative_scale_row_lift_innerleft) + (dst_negative_row_lift_innerleft))) /\ (exists ge_balance_positive_row_lift_innerleftvalue ge_balance_negative_row_lift_innerleftvalue. (((((dc_left_row_lift_inner) = 2 * (ge_balance_positive_row_lift_innerleftvalue) /\ (ge_balance_negative_row_lift_innerleftvalue) = 0) \/ exists ge_signed_half_row_lift_innerleftvaluedecode. (((dc_left_row_lift_inner) = 2 * ge_signed_half_row_lift_innerleftvaluedecode + 1 /\ (ge_balance_positive_row_lift_innerleftvalue) = 0) /\ (ge_balance_negative_row_lift_innerleftvalue) = S ge_signed_half_row_lift_innerleftvaluedecode))) /\ ((dst_positive_row_lift_innerleft) + ge_balance_negative_row_lift_innerleftvalue = (dst_negative_row_lift_innerleft) + ge_balance_positive_row_lift_innerleftvalue))))))))) /\ (((exists dst_positive_code_row_lift_innerright dst_positive_scale_row_lift_innerright dst_negative_code_row_lift_innerright dst_negative_scale_row_lift_innerright dst_positive_row_lift_innerright dst_negative_row_lift_innerright. (((G) = (((((dst_positive_code_row_lift_innerright) + (dst_positive_scale_row_lift_innerright)) * S ((dst_positive_code_row_lift_innerright) + (dst_positive_scale_row_lift_innerright)) + ((dst_positive_scale_row_lift_innerright) + (dst_positive_scale_row_lift_innerright))) + (((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) * S ((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) + ((dst_negative_scale_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)))) * S ((((dst_positive_code_row_lift_innerright) + (dst_positive_scale_row_lift_innerright)) * S ((dst_positive_code_row_lift_innerright) + (dst_positive_scale_row_lift_innerright)) + ((dst_positive_scale_row_lift_innerright) + (dst_positive_scale_row_lift_innerright))) + (((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) * S ((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) + ((dst_negative_scale_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)))) + ((((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) * S ((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) + ((dst_negative_scale_row_lift_innerright) + (dst_negative_scale_row_lift_innerright))) + (((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) * S ((dst_negative_code_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)) + ((dst_negative_scale_row_lift_innerright) + (dst_negative_scale_row_lift_innerright)))))) /\ (((((exists ff_h_pvs_row_lift_innerrightpositive. ff_h_pvs_row_lift_innerrightpositive + S (dst_positive_row_lift_innerright) = S ((S (dc_quotient_row_lift_inner)) * dst_positive_scale_row_lift_innerright)) /\ exists ff_q_pvs_row_lift_innerrightpositive. dst_positive_code_row_lift_innerright = ff_q_pvs_row_lift_innerrightpositive * S ((S (dc_quotient_row_lift_inner)) * dst_positive_scale_row_lift_innerright) + (dst_positive_row_lift_innerright))) /\ (((((exists ff_h_pvs_row_lift_innerrightnegative. ff_h_pvs_row_lift_innerrightnegative + S (dst_negative_row_lift_innerright) = S ((S (dc_quotient_row_lift_inner)) * dst_negative_scale_row_lift_innerright)) /\ exists ff_q_pvs_row_lift_innerrightnegative. dst_negative_code_row_lift_innerright = ff_q_pvs_row_lift_innerrightnegative * S ((S (dc_quotient_row_lift_inner)) * dst_negative_scale_row_lift_innerright) + (dst_negative_row_lift_innerright))) /\ (exists ge_balance_positive_row_lift_innerrightvalue ge_balance_negative_row_lift_innerrightvalue. (((((dc_right_row_lift_inner) = 2 * (ge_balance_positive_row_lift_innerrightvalue) /\ (ge_balance_negative_row_lift_innerrightvalue) = 0) \/ exists ge_signed_half_row_lift_innerrightvaluedecode. (((dc_right_row_lift_inner) = 2 * ge_signed_half_row_lift_innerrightvaluedecode + 1 /\ (ge_balance_positive_row_lift_innerrightvalue) = 0) /\ (ge_balance_negative_row_lift_innerrightvalue) = S ge_signed_half_row_lift_innerrightvaluedecode))) /\ ((dst_positive_row_lift_innerright) + ge_balance_negative_row_lift_innerrightvalue = (dst_negative_row_lift_innerright) + ge_balance_positive_row_lift_innerrightvalue))))))))) /\ (exists sto_ap_row_lift_innerproduct sto_an_row_lift_innerproduct sto_bp_row_lift_innerproduct sto_bn_row_lift_innerproduct sto_cp_row_lift_innerproduct sto_cn_row_lift_innerproduct. (((((dc_left_row_lift_inner) = 2 * (sto_ap_row_lift_innerproduct) /\ (sto_an_row_lift_innerproduct) = 0) \/ exists ge_signed_half_row_lift_innerproductleft. (((dc_left_row_lift_inner) = 2 * ge_signed_half_row_lift_innerproductleft + 1 /\ (sto_ap_row_lift_innerproduct) = 0) /\ (sto_an_row_lift_innerproduct) = S ge_signed_half_row_lift_innerproductleft))) /\ ((((((dc_right_row_lift_inner) = 2 * (sto_bp_row_lift_innerproduct) /\ (sto_bn_row_lift_innerproduct) = 0) \/ exists ge_signed_half_row_lift_innerproductright. (((dc_right_row_lift_inner) = 2 * ge_signed_half_row_lift_innerproductright + 1 /\ (sto_bp_row_lift_innerproduct) = 0) /\ (sto_bn_row_lift_innerproduct) = S ge_signed_half_row_lift_innerproductright))) /\ ((((((v) = 2 * (sto_cp_row_lift_innerproduct) /\ (sto_cn_row_lift_innerproduct) = 0) \/ exists ge_signed_half_row_lift_innerproductoutput. (((v) = 2 * ge_signed_half_row_lift_innerproductoutput + 1 /\ (sto_cp_row_lift_innerproduct) = 0) /\ (sto_cn_row_lift_innerproduct) = S ge_signed_half_row_lift_innerproductoutput))) /\ ((sto_ap_row_lift_innerproduct * sto_bp_row_lift_innerproduct + sto_an_row_lift_innerproduct * sto_bn_row_lift_innerproduct) + sto_cn_row_lift_innerproduct = (sto_ap_row_lift_innerproduct * sto_bn_row_lift_innerproduct + sto_an_row_lift_innerproduct * sto_bp_row_lift_innerproduct) + sto_cp_row_lift_innerproduct))))))))))))))) \/ ((((e)=0 \/ ~(exists pvs_factor_row_lift_innernondivisor. (q) = (e) * pvs_factor_row_lift_innernondivisor)) /\ ((v)=0)))) -> (exists sto_ap_row_lift_product sto_an_row_lift_product sto_bp_row_lift_product sto_bn_row_lift_product sto_cp_row_lift_product sto_cn_row_lift_product. (((((u) = 2 * (sto_ap_row_lift_product) /\ (sto_an_row_lift_product) = 0) \/ exists ge_signed_half_row_lift_productleft. (((u) = 2 * ge_signed_half_row_lift_productleft + 1 /\ (sto_ap_row_lift_product) = 0) /\ (sto_an_row_lift_product) = S ge_signed_half_row_lift_productleft))) /\ ((((((v) = 2 * (sto_bp_row_lift_product) /\ (sto_bn_row_lift_product) = 0) \/ exists ge_signed_half_row_lift_productright. (((v) = 2 * ge_signed_half_row_lift_productright + 1 /\ (sto_bp_row_lift_product) = 0) /\ (sto_bn_row_lift_product) = S ge_signed_half_row_lift_productright))) /\ ((((((z) = 2 * (sto_cp_row_lift_product) /\ (sto_cn_row_lift_product) = 0) \/ exists ge_signed_half_row_lift_productoutput. (((z) = 2 * ge_signed_half_row_lift_productoutput + 1 /\ (sto_cp_row_lift_product) = 0) /\ (sto_cn_row_lift_product) = S ge_signed_half_row_lift_productoutput))) /\ ((sto_ap_row_lift_product * sto_bp_row_lift_product + sto_an_row_lift_product * sto_bn_row_lift_product) + sto_cn_row_lift_product = (sto_ap_row_lift_product * sto_bn_row_lift_product + sto_an_row_lift_product * sto_bp_row_lift_product) + sto_cp_row_lift_product))))))) -> ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_row_lift_result dfg_first_row_lift_result dfg_last_row_lift_result dfg_value_row_lift_result. (((n)=((a)*(e))*dfg_middle_row_lift_result) /\ (((exists dst_positive_code_row_lift_resultfirst dst_positive_scale_row_lift_resultfirst dst_negative_code_row_lift_resultfirst dst_negative_scale_row_lift_resultfirst dst_positive_row_lift_resultfirst dst_negative_row_lift_resultfirst. (((F) = (((((dst_positive_code_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst)) * S ((dst_positive_code_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst)) + ((dst_positive_scale_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst))) + (((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) * S ((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) + ((dst_negative_scale_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)))) * S ((((dst_positive_code_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst)) * S ((dst_positive_code_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst)) + ((dst_positive_scale_row_lift_resultfirst) + (dst_positive_scale_row_lift_resultfirst))) + (((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) * S ((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) + ((dst_negative_scale_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)))) + ((((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) * S ((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) + ((dst_negative_scale_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst))) + (((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) * S ((dst_negative_code_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)) + ((dst_negative_scale_row_lift_resultfirst) + (dst_negative_scale_row_lift_resultfirst)))))) /\ (((((exists ff_h_pvs_row_lift_resultfirstpositive. ff_h_pvs_row_lift_resultfirstpositive + S (dst_positive_row_lift_resultfirst) = S ((S (a)) * dst_positive_scale_row_lift_resultfirst)) /\ exists ff_q_pvs_row_lift_resultfirstpositive. dst_positive_code_row_lift_resultfirst = ff_q_pvs_row_lift_resultfirstpositive * S ((S (a)) * dst_positive_scale_row_lift_resultfirst) + (dst_positive_row_lift_resultfirst))) /\ (((((exists ff_h_pvs_row_lift_resultfirstnegative. ff_h_pvs_row_lift_resultfirstnegative + S (dst_negative_row_lift_resultfirst) = S ((S (a)) * dst_negative_scale_row_lift_resultfirst)) /\ exists ff_q_pvs_row_lift_resultfirstnegative. dst_negative_code_row_lift_resultfirst = ff_q_pvs_row_lift_resultfirstnegative * S ((S (a)) * dst_negative_scale_row_lift_resultfirst) + (dst_negative_row_lift_resultfirst))) /\ (exists ge_balance_positive_row_lift_resultfirstvalue ge_balance_negative_row_lift_resultfirstvalue. (((((dfg_first_row_lift_result) = 2 * (ge_balance_positive_row_lift_resultfirstvalue) /\ (ge_balance_negative_row_lift_resultfirstvalue) = 0) \/ exists ge_signed_half_row_lift_resultfirstvaluedecode. (((dfg_first_row_lift_result) = 2 * ge_signed_half_row_lift_resultfirstvaluedecode + 1 /\ (ge_balance_positive_row_lift_resultfirstvalue) = 0) /\ (ge_balance_negative_row_lift_resultfirstvalue) = S ge_signed_half_row_lift_resultfirstvaluedecode))) /\ ((dst_positive_row_lift_resultfirst) + ge_balance_negative_row_lift_resultfirstvalue = (dst_negative_row_lift_resultfirst) + ge_balance_positive_row_lift_resultfirstvalue))))))))) /\ (((exists dst_positive_code_row_lift_resultlast dst_positive_scale_row_lift_resultlast dst_negative_code_row_lift_resultlast dst_negative_scale_row_lift_resultlast dst_positive_row_lift_resultlast dst_negative_row_lift_resultlast. (((H) = (((((dst_positive_code_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast)) * S ((dst_positive_code_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast)) + ((dst_positive_scale_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast))) + (((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) * S ((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) + ((dst_negative_scale_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)))) * S ((((dst_positive_code_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast)) * S ((dst_positive_code_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast)) + ((dst_positive_scale_row_lift_resultlast) + (dst_positive_scale_row_lift_resultlast))) + (((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) * S ((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) + ((dst_negative_scale_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)))) + ((((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) * S ((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) + ((dst_negative_scale_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast))) + (((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) * S ((dst_negative_code_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)) + ((dst_negative_scale_row_lift_resultlast) + (dst_negative_scale_row_lift_resultlast)))))) /\ (((((exists ff_h_pvs_row_lift_resultlastpositive. ff_h_pvs_row_lift_resultlastpositive + S (dst_positive_row_lift_resultlast) = S ((S (e)) * dst_positive_scale_row_lift_resultlast)) /\ exists ff_q_pvs_row_lift_resultlastpositive. dst_positive_code_row_lift_resultlast = ff_q_pvs_row_lift_resultlastpositive * S ((S (e)) * dst_positive_scale_row_lift_resultlast) + (dst_positive_row_lift_resultlast))) /\ (((((exists ff_h_pvs_row_lift_resultlastnegative. ff_h_pvs_row_lift_resultlastnegative + S (dst_negative_row_lift_resultlast) = S ((S (e)) * dst_negative_scale_row_lift_resultlast)) /\ exists ff_q_pvs_row_lift_resultlastnegative. dst_negative_code_row_lift_resultlast = ff_q_pvs_row_lift_resultlastnegative * S ((S (e)) * dst_negative_scale_row_lift_resultlast) + (dst_negative_row_lift_resultlast))) /\ (exists ge_balance_positive_row_lift_resultlastvalue ge_balance_negative_row_lift_resultlastvalue. (((((dfg_last_row_lift_result) = 2 * (ge_balance_positive_row_lift_resultlastvalue) /\ (ge_balance_negative_row_lift_resultlastvalue) = 0) \/ exists ge_signed_half_row_lift_resultlastvaluedecode. (((dfg_last_row_lift_result) = 2 * ge_signed_half_row_lift_resultlastvaluedecode + 1 /\ (ge_balance_positive_row_lift_resultlastvalue) = 0) /\ (ge_balance_negative_row_lift_resultlastvalue) = S ge_signed_half_row_lift_resultlastvaluedecode))) /\ ((dst_positive_row_lift_resultlast) + ge_balance_negative_row_lift_resultlastvalue = (dst_negative_row_lift_resultlast) + ge_balance_positive_row_lift_resultlastvalue))))))))) /\ (((exists dst_positive_code_row_lift_resultmiddle dst_positive_scale_row_lift_resultmiddle dst_negative_code_row_lift_resultmiddle dst_negative_scale_row_lift_resultmiddle dst_positive_row_lift_resultmiddle dst_negative_row_lift_resultmiddle. (((G) = (((((dst_positive_code_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle)) * S ((dst_positive_code_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle)) + ((dst_positive_scale_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle))) + (((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) * S ((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) + ((dst_negative_scale_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)))) * S ((((dst_positive_code_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle)) * S ((dst_positive_code_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle)) + ((dst_positive_scale_row_lift_resultmiddle) + (dst_positive_scale_row_lift_resultmiddle))) + (((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) * S ((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) + ((dst_negative_scale_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)))) + ((((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) * S ((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) + ((dst_negative_scale_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle))) + (((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) * S ((dst_negative_code_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)) + ((dst_negative_scale_row_lift_resultmiddle) + (dst_negative_scale_row_lift_resultmiddle)))))) /\ (((((exists ff_h_pvs_row_lift_resultmiddlepositive. ff_h_pvs_row_lift_resultmiddlepositive + S (dst_positive_row_lift_resultmiddle) = S ((S (dfg_middle_row_lift_result)) * dst_positive_scale_row_lift_resultmiddle)) /\ exists ff_q_pvs_row_lift_resultmiddlepositive. dst_positive_code_row_lift_resultmiddle = ff_q_pvs_row_lift_resultmiddlepositive * S ((S (dfg_middle_row_lift_result)) * dst_positive_scale_row_lift_resultmiddle) + (dst_positive_row_lift_resultmiddle))) /\ (((((exists ff_h_pvs_row_lift_resultmiddlenegative. ff_h_pvs_row_lift_resultmiddlenegative + S (dst_negative_row_lift_resultmiddle) = S ((S (dfg_middle_row_lift_result)) * dst_negative_scale_row_lift_resultmiddle)) /\ exists ff_q_pvs_row_lift_resultmiddlenegative. dst_negative_code_row_lift_resultmiddle = ff_q_pvs_row_lift_resultmiddlenegative * S ((S (dfg_middle_row_lift_result)) * dst_negative_scale_row_lift_resultmiddle) + (dst_negative_row_lift_resultmiddle))) /\ (exists ge_balance_positive_row_lift_resultmiddlevalue ge_balance_negative_row_lift_resultmiddlevalue. (((((dfg_value_row_lift_result) = 2 * (ge_balance_positive_row_lift_resultmiddlevalue) /\ (ge_balance_negative_row_lift_resultmiddlevalue) = 0) \/ exists ge_signed_half_row_lift_resultmiddlevaluedecode. (((dfg_value_row_lift_result) = 2 * ge_signed_half_row_lift_resultmiddlevaluedecode + 1 /\ (ge_balance_positive_row_lift_resultmiddlevalue) = 0) /\ (ge_balance_negative_row_lift_resultmiddlevalue) = S ge_signed_half_row_lift_resultmiddlevaluedecode))) /\ ((dst_positive_row_lift_resultmiddle) + ge_balance_negative_row_lift_resultmiddlevalue = (dst_negative_row_lift_resultmiddle) + ge_balance_positive_row_lift_resultmiddlevalue))))))))) /\ (exists dfg_inner_row_lift_resultproduct. ((exists sto_ap_row_lift_resultproductinner sto_an_row_lift_resultproductinner sto_bp_row_lift_resultproductinner sto_bn_row_lift_resultproductinner sto_cp_row_lift_resultproductinner sto_cn_row_lift_resultproductinner. (((((dfg_last_row_lift_result) = 2 * (sto_ap_row_lift_resultproductinner) /\ (sto_an_row_lift_resultproductinner) = 0) \/ exists ge_signed_half_row_lift_resultproductinnerleft. (((dfg_last_row_lift_result) = 2 * ge_signed_half_row_lift_resultproductinnerleft + 1 /\ (sto_ap_row_lift_resultproductinner) = 0) /\ (sto_an_row_lift_resultproductinner) = S ge_signed_half_row_lift_resultproductinnerleft))) /\ ((((((dfg_value_row_lift_result) = 2 * (sto_bp_row_lift_resultproductinner) /\ (sto_bn_row_lift_resultproductinner) = 0) \/ exists ge_signed_half_row_lift_resultproductinnerright. (((dfg_value_row_lift_result) = 2 * ge_signed_half_row_lift_resultproductinnerright + 1 /\ (sto_bp_row_lift_resultproductinner) = 0) /\ (sto_bn_row_lift_resultproductinner) = S ge_signed_half_row_lift_resultproductinnerright))) /\ ((((((dfg_inner_row_lift_resultproduct) = 2 * (sto_cp_row_lift_resultproductinner) /\ (sto_cn_row_lift_resultproductinner) = 0) \/ exists ge_signed_half_row_lift_resultproductinneroutput. (((dfg_inner_row_lift_resultproduct) = 2 * ge_signed_half_row_lift_resultproductinneroutput + 1 /\ (sto_cp_row_lift_resultproductinner) = 0) /\ (sto_cn_row_lift_resultproductinner) = S ge_signed_half_row_lift_resultproductinneroutput))) /\ ((sto_ap_row_lift_resultproductinner * sto_bp_row_lift_resultproductinner + sto_an_row_lift_resultproductinner * sto_bn_row_lift_resultproductinner) + sto_cn_row_lift_resultproductinner = (sto_ap_row_lift_resultproductinner * sto_bn_row_lift_resultproductinner + sto_an_row_lift_resultproductinner * sto_bp_row_lift_resultproductinner) + sto_cp_row_lift_resultproductinner))))))) /\ (exists sto_ap_row_lift_resultproductouter sto_an_row_lift_resultproductouter sto_bp_row_lift_resultproductouter sto_bn_row_lift_resultproductouter sto_cp_row_lift_resultproductouter sto_cn_row_lift_resultproductouter. (((((dfg_first_row_lift_result) = 2 * (sto_ap_row_lift_resultproductouter) /\ (sto_an_row_lift_resultproductouter) = 0) \/ exists ge_signed_half_row_lift_resultproductouterleft. (((dfg_first_row_lift_result) = 2 * ge_signed_half_row_lift_resultproductouterleft + 1 /\ (sto_ap_row_lift_resultproductouter) = 0) /\ (sto_an_row_lift_resultproductouter) = S ge_signed_half_row_lift_resultproductouterleft))) /\ ((((((dfg_inner_row_lift_resultproduct) = 2 * (sto_bp_row_lift_resultproductouter) /\ (sto_bn_row_lift_resultproductouter) = 0) \/ exists ge_signed_half_row_lift_resultproductouterright. (((dfg_inner_row_lift_resultproduct) = 2 * ge_signed_half_row_lift_resultproductouterright + 1 /\ (sto_bp_row_lift_resultproductouter) = 0) /\ (sto_bn_row_lift_resultproductouter) = S ge_signed_half_row_lift_resultproductouterright))) /\ ((((((z) = 2 * (sto_cp_row_lift_resultproductouter) /\ (sto_cn_row_lift_resultproductouter) = 0) \/ exists ge_signed_half_row_lift_resultproductouteroutput. (((z) = 2 * ge_signed_half_row_lift_resultproductouteroutput + 1 /\ (sto_cp_row_lift_resultproductouter) = 0) /\ (sto_cn_row_lift_resultproductouter) = S ge_signed_half_row_lift_resultproductouteroutput))) /\ ((sto_ap_row_lift_resultproductouter * sto_bp_row_lift_resultproductouter + sto_an_row_lift_resultproductouter * sto_bn_row_lift_resultproductouter) + sto_cn_row_lift_resultproductouter = (sto_ap_row_lift_resultproductouter * sto_bn_row_lift_resultproductouter + sto_an_row_lift_resultproductouter * sto_bp_row_lift_resultproductouter) + sto_cp_row_lift_resultproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_row_lift_resultomittednondivisor. (n) = ((a)*(e)) * pvs_factor_row_lift_resultomittednondivisor))) /\ ((z)=0))))