dirichlet_grid_entry_transpose

Exact expanded first-order arithmetic statement

forall F G H n a e z. ((((~((a)=0)) /\ (((~((e)=0)) /\ (exists dfg_middle_transpose_source dfg_first_transpose_source dfg_last_transpose_source dfg_value_transpose_source. (((n)=((a)*(e))*dfg_middle_transpose_source) /\ (((exists dst_positive_code_transpose_sourcefirst dst_positive_scale_transpose_sourcefirst dst_negative_code_transpose_sourcefirst dst_negative_scale_transpose_sourcefirst dst_positive_transpose_sourcefirst dst_negative_transpose_sourcefirst. (((F) = (((((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) * S ((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) + ((dst_positive_scale_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))) * S ((((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) * S ((dst_positive_code_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst)) + ((dst_positive_scale_transpose_sourcefirst) + (dst_positive_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))) + ((((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst))) + (((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) * S ((dst_negative_code_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)) + ((dst_negative_scale_transpose_sourcefirst) + (dst_negative_scale_transpose_sourcefirst)))))) /\ (((((exists ff_h_pvs_transpose_sourcefirstpositive. ff_h_pvs_transpose_sourcefirstpositive + S (dst_positive_transpose_sourcefirst) = S ((S (a)) * dst_positive_scale_transpose_sourcefirst)) /\ exists ff_q_pvs_transpose_sourcefirstpositive. dst_positive_code_transpose_sourcefirst = ff_q_pvs_transpose_sourcefirstpositive * S ((S (a)) * dst_positive_scale_transpose_sourcefirst) + (dst_positive_transpose_sourcefirst))) /\ (((((exists ff_h_pvs_transpose_sourcefirstnegative. ff_h_pvs_transpose_sourcefirstnegative + S (dst_negative_transpose_sourcefirst) = S ((S (a)) * dst_negative_scale_transpose_sourcefirst)) /\ exists ff_q_pvs_transpose_sourcefirstnegative. dst_negative_code_transpose_sourcefirst = ff_q_pvs_transpose_sourcefirstnegative * S ((S (a)) * dst_negative_scale_transpose_sourcefirst) + (dst_negative_transpose_sourcefirst))) /\ (exists ge_balance_positive_transpose_sourcefirstvalue ge_balance_negative_transpose_sourcefirstvalue. (((((dfg_first_transpose_source) = 2 * (ge_balance_positive_transpose_sourcefirstvalue) /\ (ge_balance_negative_transpose_sourcefirstvalue) = 0) \/ exists ge_signed_half_transpose_sourcefirstvaluedecode. (((dfg_first_transpose_source) = 2 * ge_signed_half_transpose_sourcefirstvaluedecode + 1 /\ (ge_balance_positive_transpose_sourcefirstvalue) = 0) /\ (ge_balance_negative_transpose_sourcefirstvalue) = S ge_signed_half_transpose_sourcefirstvaluedecode))) /\ ((dst_positive_transpose_sourcefirst) + ge_balance_negative_transpose_sourcefirstvalue = (dst_negative_transpose_sourcefirst) + ge_balance_positive_transpose_sourcefirstvalue))))))))) /\ (((exists dst_positive_code_transpose_sourcelast dst_positive_scale_transpose_sourcelast dst_negative_code_transpose_sourcelast dst_negative_scale_transpose_sourcelast dst_positive_transpose_sourcelast dst_negative_transpose_sourcelast. (((H) = (((((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) * S ((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) + ((dst_positive_scale_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))) * S ((((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) * S ((dst_positive_code_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast)) + ((dst_positive_scale_transpose_sourcelast) + (dst_positive_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))) + ((((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast))) + (((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) * S ((dst_negative_code_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)) + ((dst_negative_scale_transpose_sourcelast) + (dst_negative_scale_transpose_sourcelast)))))) /\ (((((exists ff_h_pvs_transpose_sourcelastpositive. ff_h_pvs_transpose_sourcelastpositive + S (dst_positive_transpose_sourcelast) = S ((S (e)) * dst_positive_scale_transpose_sourcelast)) /\ exists ff_q_pvs_transpose_sourcelastpositive. dst_positive_code_transpose_sourcelast = ff_q_pvs_transpose_sourcelastpositive * S ((S (e)) * dst_positive_scale_transpose_sourcelast) + (dst_positive_transpose_sourcelast))) /\ (((((exists ff_h_pvs_transpose_sourcelastnegative. ff_h_pvs_transpose_sourcelastnegative + S (dst_negative_transpose_sourcelast) = S ((S (e)) * dst_negative_scale_transpose_sourcelast)) /\ exists ff_q_pvs_transpose_sourcelastnegative. dst_negative_code_transpose_sourcelast = ff_q_pvs_transpose_sourcelastnegative * S ((S (e)) * dst_negative_scale_transpose_sourcelast) + (dst_negative_transpose_sourcelast))) /\ (exists ge_balance_positive_transpose_sourcelastvalue ge_balance_negative_transpose_sourcelastvalue. (((((dfg_last_transpose_source) = 2 * (ge_balance_positive_transpose_sourcelastvalue) /\ (ge_balance_negative_transpose_sourcelastvalue) = 0) \/ exists ge_signed_half_transpose_sourcelastvaluedecode. (((dfg_last_transpose_source) = 2 * ge_signed_half_transpose_sourcelastvaluedecode + 1 /\ (ge_balance_positive_transpose_sourcelastvalue) = 0) /\ (ge_balance_negative_transpose_sourcelastvalue) = S ge_signed_half_transpose_sourcelastvaluedecode))) /\ ((dst_positive_transpose_sourcelast) + ge_balance_negative_transpose_sourcelastvalue = (dst_negative_transpose_sourcelast) + ge_balance_positive_transpose_sourcelastvalue))))))))) /\ (((exists dst_positive_code_transpose_sourcemiddle dst_positive_scale_transpose_sourcemiddle dst_negative_code_transpose_sourcemiddle dst_negative_scale_transpose_sourcemiddle dst_positive_transpose_sourcemiddle dst_negative_transpose_sourcemiddle. (((G) = (((((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) * S ((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) + ((dst_positive_scale_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))) * S ((((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) * S ((dst_positive_code_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle)) + ((dst_positive_scale_transpose_sourcemiddle) + (dst_positive_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))) + ((((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle))) + (((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) * S ((dst_negative_code_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)) + ((dst_negative_scale_transpose_sourcemiddle) + (dst_negative_scale_transpose_sourcemiddle)))))) /\ (((((exists ff_h_pvs_transpose_sourcemiddlepositive. ff_h_pvs_transpose_sourcemiddlepositive + S (dst_positive_transpose_sourcemiddle) = S ((S (dfg_middle_transpose_source)) * dst_positive_scale_transpose_sourcemiddle)) /\ exists ff_q_pvs_transpose_sourcemiddlepositive. dst_positive_code_transpose_sourcemiddle = ff_q_pvs_transpose_sourcemiddlepositive * S ((S (dfg_middle_transpose_source)) * dst_positive_scale_transpose_sourcemiddle) + (dst_positive_transpose_sourcemiddle))) /\ (((((exists ff_h_pvs_transpose_sourcemiddlenegative. ff_h_pvs_transpose_sourcemiddlenegative + S (dst_negative_transpose_sourcemiddle) = S ((S (dfg_middle_transpose_source)) * dst_negative_scale_transpose_sourcemiddle)) /\ exists ff_q_pvs_transpose_sourcemiddlenegative. dst_negative_code_transpose_sourcemiddle = ff_q_pvs_transpose_sourcemiddlenegative * S ((S (dfg_middle_transpose_source)) * dst_negative_scale_transpose_sourcemiddle) + (dst_negative_transpose_sourcemiddle))) /\ (exists ge_balance_positive_transpose_sourcemiddlevalue ge_balance_negative_transpose_sourcemiddlevalue. (((((dfg_value_transpose_source) = 2 * (ge_balance_positive_transpose_sourcemiddlevalue) /\ (ge_balance_negative_transpose_sourcemiddlevalue) = 0) \/ exists ge_signed_half_transpose_sourcemiddlevaluedecode. (((dfg_value_transpose_source) = 2 * ge_signed_half_transpose_sourcemiddlevaluedecode + 1 /\ (ge_balance_positive_transpose_sourcemiddlevalue) = 0) /\ (ge_balance_negative_transpose_sourcemiddlevalue) = S ge_signed_half_transpose_sourcemiddlevaluedecode))) /\ ((dst_positive_transpose_sourcemiddle) + ge_balance_negative_transpose_sourcemiddlevalue = (dst_negative_transpose_sourcemiddle) + ge_balance_positive_transpose_sourcemiddlevalue))))))))) /\ (exists dfg_inner_transpose_sourceproduct. ((exists sto_ap_transpose_sourceproductinner sto_an_transpose_sourceproductinner sto_bp_transpose_sourceproductinner sto_bn_transpose_sourceproductinner sto_cp_transpose_sourceproductinner sto_cn_transpose_sourceproductinner. (((((dfg_last_transpose_source) = 2 * (sto_ap_transpose_sourceproductinner) /\ (sto_an_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinnerleft. (((dfg_last_transpose_source) = 2 * ge_signed_half_transpose_sourceproductinnerleft + 1 /\ (sto_ap_transpose_sourceproductinner) = 0) /\ (sto_an_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinnerleft))) /\ ((((((dfg_value_transpose_source) = 2 * (sto_bp_transpose_sourceproductinner) /\ (sto_bn_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinnerright. (((dfg_value_transpose_source) = 2 * ge_signed_half_transpose_sourceproductinnerright + 1 /\ (sto_bp_transpose_sourceproductinner) = 0) /\ (sto_bn_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinnerright))) /\ ((((((dfg_inner_transpose_sourceproduct) = 2 * (sto_cp_transpose_sourceproductinner) /\ (sto_cn_transpose_sourceproductinner) = 0) \/ exists ge_signed_half_transpose_sourceproductinneroutput. (((dfg_inner_transpose_sourceproduct) = 2 * ge_signed_half_transpose_sourceproductinneroutput + 1 /\ (sto_cp_transpose_sourceproductinner) = 0) /\ (sto_cn_transpose_sourceproductinner) = S ge_signed_half_transpose_sourceproductinneroutput))) /\ ((sto_ap_transpose_sourceproductinner * sto_bp_transpose_sourceproductinner + sto_an_transpose_sourceproductinner * sto_bn_transpose_sourceproductinner) + sto_cn_transpose_sourceproductinner = (sto_ap_transpose_sourceproductinner * sto_bn_transpose_sourceproductinner + sto_an_transpose_sourceproductinner * sto_bp_transpose_sourceproductinner) + sto_cp_transpose_sourceproductinner))))))) /\ (exists sto_ap_transpose_sourceproductouter sto_an_transpose_sourceproductouter sto_bp_transpose_sourceproductouter sto_bn_transpose_sourceproductouter sto_cp_transpose_sourceproductouter sto_cn_transpose_sourceproductouter. (((((dfg_first_transpose_source) = 2 * (sto_ap_transpose_sourceproductouter) /\ (sto_an_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouterleft. (((dfg_first_transpose_source) = 2 * ge_signed_half_transpose_sourceproductouterleft + 1 /\ (sto_ap_transpose_sourceproductouter) = 0) /\ (sto_an_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouterleft))) /\ ((((((dfg_inner_transpose_sourceproduct) = 2 * (sto_bp_transpose_sourceproductouter) /\ (sto_bn_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouterright. (((dfg_inner_transpose_sourceproduct) = 2 * ge_signed_half_transpose_sourceproductouterright + 1 /\ (sto_bp_transpose_sourceproductouter) = 0) /\ (sto_bn_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouterright))) /\ ((((((z) = 2 * (sto_cp_transpose_sourceproductouter) /\ (sto_cn_transpose_sourceproductouter) = 0) \/ exists ge_signed_half_transpose_sourceproductouteroutput. (((z) = 2 * ge_signed_half_transpose_sourceproductouteroutput + 1 /\ (sto_cp_transpose_sourceproductouter) = 0) /\ (sto_cn_transpose_sourceproductouter) = S ge_signed_half_transpose_sourceproductouteroutput))) /\ ((sto_ap_transpose_sourceproductouter * sto_bp_transpose_sourceproductouter + sto_an_transpose_sourceproductouter * sto_bn_transpose_sourceproductouter) + sto_cn_transpose_sourceproductouter = (sto_ap_transpose_sourceproductouter * sto_bn_transpose_sourceproductouter + sto_an_transpose_sourceproductouter * sto_bp_transpose_sourceproductouter) + sto_cp_transpose_sourceproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((e)=0 \/ ~(exists pvs_factor_transpose_sourceomittednondivisor. (n) = ((a)*(e)) * pvs_factor_transpose_sourceomittednondivisor))) /\ ((z)=0)))) -> ((((~((e)=0)) /\ (((~((a)=0)) /\ (exists dfg_middle_transpose_target dfg_first_transpose_target dfg_last_transpose_target dfg_value_transpose_target. (((n)=((e)*(a))*dfg_middle_transpose_target) /\ (((exists dst_positive_code_transpose_targetfirst dst_positive_scale_transpose_targetfirst dst_negative_code_transpose_targetfirst dst_negative_scale_transpose_targetfirst dst_positive_transpose_targetfirst dst_negative_transpose_targetfirst. (((H) = (((((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) * S ((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) + ((dst_positive_scale_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))) * S ((((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) * S ((dst_positive_code_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst)) + ((dst_positive_scale_transpose_targetfirst) + (dst_positive_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))) + ((((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst))) + (((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) * S ((dst_negative_code_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)) + ((dst_negative_scale_transpose_targetfirst) + (dst_negative_scale_transpose_targetfirst)))))) /\ (((((exists ff_h_pvs_transpose_targetfirstpositive. ff_h_pvs_transpose_targetfirstpositive + S (dst_positive_transpose_targetfirst) = S ((S (e)) * dst_positive_scale_transpose_targetfirst)) /\ exists ff_q_pvs_transpose_targetfirstpositive. dst_positive_code_transpose_targetfirst = ff_q_pvs_transpose_targetfirstpositive * S ((S (e)) * dst_positive_scale_transpose_targetfirst) + (dst_positive_transpose_targetfirst))) /\ (((((exists ff_h_pvs_transpose_targetfirstnegative. ff_h_pvs_transpose_targetfirstnegative + S (dst_negative_transpose_targetfirst) = S ((S (e)) * dst_negative_scale_transpose_targetfirst)) /\ exists ff_q_pvs_transpose_targetfirstnegative. dst_negative_code_transpose_targetfirst = ff_q_pvs_transpose_targetfirstnegative * S ((S (e)) * dst_negative_scale_transpose_targetfirst) + (dst_negative_transpose_targetfirst))) /\ (exists ge_balance_positive_transpose_targetfirstvalue ge_balance_negative_transpose_targetfirstvalue. (((((dfg_first_transpose_target) = 2 * (ge_balance_positive_transpose_targetfirstvalue) /\ (ge_balance_negative_transpose_targetfirstvalue) = 0) \/ exists ge_signed_half_transpose_targetfirstvaluedecode. (((dfg_first_transpose_target) = 2 * ge_signed_half_transpose_targetfirstvaluedecode + 1 /\ (ge_balance_positive_transpose_targetfirstvalue) = 0) /\ (ge_balance_negative_transpose_targetfirstvalue) = S ge_signed_half_transpose_targetfirstvaluedecode))) /\ ((dst_positive_transpose_targetfirst) + ge_balance_negative_transpose_targetfirstvalue = (dst_negative_transpose_targetfirst) + ge_balance_positive_transpose_targetfirstvalue))))))))) /\ (((exists dst_positive_code_transpose_targetlast dst_positive_scale_transpose_targetlast dst_negative_code_transpose_targetlast dst_negative_scale_transpose_targetlast dst_positive_transpose_targetlast dst_negative_transpose_targetlast. (((F) = (((((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) * S ((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) + ((dst_positive_scale_transpose_targetlast) + (dst_positive_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))) * S ((((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) * S ((dst_positive_code_transpose_targetlast) + (dst_positive_scale_transpose_targetlast)) + ((dst_positive_scale_transpose_targetlast) + (dst_positive_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))) + ((((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast))) + (((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) * S ((dst_negative_code_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)) + ((dst_negative_scale_transpose_targetlast) + (dst_negative_scale_transpose_targetlast)))))) /\ (((((exists ff_h_pvs_transpose_targetlastpositive. ff_h_pvs_transpose_targetlastpositive + S (dst_positive_transpose_targetlast) = S ((S (a)) * dst_positive_scale_transpose_targetlast)) /\ exists ff_q_pvs_transpose_targetlastpositive. dst_positive_code_transpose_targetlast = ff_q_pvs_transpose_targetlastpositive * S ((S (a)) * dst_positive_scale_transpose_targetlast) + (dst_positive_transpose_targetlast))) /\ (((((exists ff_h_pvs_transpose_targetlastnegative. ff_h_pvs_transpose_targetlastnegative + S (dst_negative_transpose_targetlast) = S ((S (a)) * dst_negative_scale_transpose_targetlast)) /\ exists ff_q_pvs_transpose_targetlastnegative. dst_negative_code_transpose_targetlast = ff_q_pvs_transpose_targetlastnegative * S ((S (a)) * dst_negative_scale_transpose_targetlast) + (dst_negative_transpose_targetlast))) /\ (exists ge_balance_positive_transpose_targetlastvalue ge_balance_negative_transpose_targetlastvalue. (((((dfg_last_transpose_target) = 2 * (ge_balance_positive_transpose_targetlastvalue) /\ (ge_balance_negative_transpose_targetlastvalue) = 0) \/ exists ge_signed_half_transpose_targetlastvaluedecode. (((dfg_last_transpose_target) = 2 * ge_signed_half_transpose_targetlastvaluedecode + 1 /\ (ge_balance_positive_transpose_targetlastvalue) = 0) /\ (ge_balance_negative_transpose_targetlastvalue) = S ge_signed_half_transpose_targetlastvaluedecode))) /\ ((dst_positive_transpose_targetlast) + ge_balance_negative_transpose_targetlastvalue = (dst_negative_transpose_targetlast) + ge_balance_positive_transpose_targetlastvalue))))))))) /\ (((exists dst_positive_code_transpose_targetmiddle dst_positive_scale_transpose_targetmiddle dst_negative_code_transpose_targetmiddle dst_negative_scale_transpose_targetmiddle dst_positive_transpose_targetmiddle dst_negative_transpose_targetmiddle. (((G) = (((((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) * S ((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) + ((dst_positive_scale_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))) * S ((((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) * S ((dst_positive_code_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle)) + ((dst_positive_scale_transpose_targetmiddle) + (dst_positive_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))) + ((((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle))) + (((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) * S ((dst_negative_code_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)) + ((dst_negative_scale_transpose_targetmiddle) + (dst_negative_scale_transpose_targetmiddle)))))) /\ (((((exists ff_h_pvs_transpose_targetmiddlepositive. ff_h_pvs_transpose_targetmiddlepositive + S (dst_positive_transpose_targetmiddle) = S ((S (dfg_middle_transpose_target)) * dst_positive_scale_transpose_targetmiddle)) /\ exists ff_q_pvs_transpose_targetmiddlepositive. dst_positive_code_transpose_targetmiddle = ff_q_pvs_transpose_targetmiddlepositive * S ((S (dfg_middle_transpose_target)) * dst_positive_scale_transpose_targetmiddle) + (dst_positive_transpose_targetmiddle))) /\ (((((exists ff_h_pvs_transpose_targetmiddlenegative. ff_h_pvs_transpose_targetmiddlenegative + S (dst_negative_transpose_targetmiddle) = S ((S (dfg_middle_transpose_target)) * dst_negative_scale_transpose_targetmiddle)) /\ exists ff_q_pvs_transpose_targetmiddlenegative. dst_negative_code_transpose_targetmiddle = ff_q_pvs_transpose_targetmiddlenegative * S ((S (dfg_middle_transpose_target)) * dst_negative_scale_transpose_targetmiddle) + (dst_negative_transpose_targetmiddle))) /\ (exists ge_balance_positive_transpose_targetmiddlevalue ge_balance_negative_transpose_targetmiddlevalue. (((((dfg_value_transpose_target) = 2 * (ge_balance_positive_transpose_targetmiddlevalue) /\ (ge_balance_negative_transpose_targetmiddlevalue) = 0) \/ exists ge_signed_half_transpose_targetmiddlevaluedecode. (((dfg_value_transpose_target) = 2 * ge_signed_half_transpose_targetmiddlevaluedecode + 1 /\ (ge_balance_positive_transpose_targetmiddlevalue) = 0) /\ (ge_balance_negative_transpose_targetmiddlevalue) = S ge_signed_half_transpose_targetmiddlevaluedecode))) /\ ((dst_positive_transpose_targetmiddle) + ge_balance_negative_transpose_targetmiddlevalue = (dst_negative_transpose_targetmiddle) + ge_balance_positive_transpose_targetmiddlevalue))))))))) /\ (exists dfg_inner_transpose_targetproduct. ((exists sto_ap_transpose_targetproductinner sto_an_transpose_targetproductinner sto_bp_transpose_targetproductinner sto_bn_transpose_targetproductinner sto_cp_transpose_targetproductinner sto_cn_transpose_targetproductinner. (((((dfg_last_transpose_target) = 2 * (sto_ap_transpose_targetproductinner) /\ (sto_an_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinnerleft. (((dfg_last_transpose_target) = 2 * ge_signed_half_transpose_targetproductinnerleft + 1 /\ (sto_ap_transpose_targetproductinner) = 0) /\ (sto_an_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinnerleft))) /\ ((((((dfg_value_transpose_target) = 2 * (sto_bp_transpose_targetproductinner) /\ (sto_bn_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinnerright. (((dfg_value_transpose_target) = 2 * ge_signed_half_transpose_targetproductinnerright + 1 /\ (sto_bp_transpose_targetproductinner) = 0) /\ (sto_bn_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinnerright))) /\ ((((((dfg_inner_transpose_targetproduct) = 2 * (sto_cp_transpose_targetproductinner) /\ (sto_cn_transpose_targetproductinner) = 0) \/ exists ge_signed_half_transpose_targetproductinneroutput. (((dfg_inner_transpose_targetproduct) = 2 * ge_signed_half_transpose_targetproductinneroutput + 1 /\ (sto_cp_transpose_targetproductinner) = 0) /\ (sto_cn_transpose_targetproductinner) = S ge_signed_half_transpose_targetproductinneroutput))) /\ ((sto_ap_transpose_targetproductinner * sto_bp_transpose_targetproductinner + sto_an_transpose_targetproductinner * sto_bn_transpose_targetproductinner) + sto_cn_transpose_targetproductinner = (sto_ap_transpose_targetproductinner * sto_bn_transpose_targetproductinner + sto_an_transpose_targetproductinner * sto_bp_transpose_targetproductinner) + sto_cp_transpose_targetproductinner))))))) /\ (exists sto_ap_transpose_targetproductouter sto_an_transpose_targetproductouter sto_bp_transpose_targetproductouter sto_bn_transpose_targetproductouter sto_cp_transpose_targetproductouter sto_cn_transpose_targetproductouter. (((((dfg_first_transpose_target) = 2 * (sto_ap_transpose_targetproductouter) /\ (sto_an_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouterleft. (((dfg_first_transpose_target) = 2 * ge_signed_half_transpose_targetproductouterleft + 1 /\ (sto_ap_transpose_targetproductouter) = 0) /\ (sto_an_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouterleft))) /\ ((((((dfg_inner_transpose_targetproduct) = 2 * (sto_bp_transpose_targetproductouter) /\ (sto_bn_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouterright. (((dfg_inner_transpose_targetproduct) = 2 * ge_signed_half_transpose_targetproductouterright + 1 /\ (sto_bp_transpose_targetproductouter) = 0) /\ (sto_bn_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouterright))) /\ ((((((z) = 2 * (sto_cp_transpose_targetproductouter) /\ (sto_cn_transpose_targetproductouter) = 0) \/ exists ge_signed_half_transpose_targetproductouteroutput. (((z) = 2 * ge_signed_half_transpose_targetproductouteroutput + 1 /\ (sto_cp_transpose_targetproductouter) = 0) /\ (sto_cn_transpose_targetproductouter) = S ge_signed_half_transpose_targetproductouteroutput))) /\ ((sto_ap_transpose_targetproductouter * sto_bp_transpose_targetproductouter + sto_an_transpose_targetproductouter * sto_bn_transpose_targetproductouter) + sto_cn_transpose_targetproductouter = (sto_ap_transpose_targetproductouter * sto_bn_transpose_targetproductouter + sto_an_transpose_targetproductouter * sto_bp_transpose_targetproductouter) + sto_cp_transpose_targetproductouter))))))))))))))))))))) \/ ((((e)=0 \/ ((a)=0 \/ ~(exists pvs_factor_transpose_targetomittednondivisor. (n) = ((e)*(a)) * pvs_factor_transpose_targetomittednondivisor))) /\ ((z)=0))))