dirichlet_factor_row_zero_sum

Exact expanded first-order arithmetic statement

forall F G H n a V z. (((exists dst_positive_code_row_zero_valuestable dst_positive_scale_row_zero_valuestable dst_negative_code_row_zero_valuestable dst_negative_scale_row_zero_valuestable. (((V) = (((((dst_positive_code_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable)) * S ((dst_positive_code_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable)) + ((dst_positive_scale_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable))) + (((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) * S ((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) + ((dst_negative_scale_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)))) * S ((((dst_positive_code_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable)) * S ((dst_positive_code_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable)) + ((dst_positive_scale_row_zero_valuestable) + (dst_positive_scale_row_zero_valuestable))) + (((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) * S ((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) + ((dst_negative_scale_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)))) + ((((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) * S ((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) + ((dst_negative_scale_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable))) + (((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) * S ((dst_negative_code_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)) + ((dst_negative_scale_row_zero_valuestable) + (dst_negative_scale_row_zero_valuestable)))))) /\ (forall dst_index_row_zero_valuestable. (exists pvs_le_gap_row_zero_valuestabledomain. pvs_le_gap_row_zero_valuestabledomain + (dst_index_row_zero_valuestable) = (S (n))) -> exists dst_positive_row_zero_valuestable dst_negative_row_zero_valuestable dst_value_row_zero_valuestable. ((((exists ff_h_pvs_row_zero_valuestableentrypositive. ff_h_pvs_row_zero_valuestableentrypositive + S (dst_positive_row_zero_valuestable) = S ((S (dst_index_row_zero_valuestable)) * dst_positive_scale_row_zero_valuestable)) /\ exists ff_q_pvs_row_zero_valuestableentrypositive. dst_positive_code_row_zero_valuestable = ff_q_pvs_row_zero_valuestableentrypositive * S ((S (dst_index_row_zero_valuestable)) * dst_positive_scale_row_zero_valuestable) + (dst_positive_row_zero_valuestable))) /\ (((((exists ff_h_pvs_row_zero_valuestableentrynegative. ff_h_pvs_row_zero_valuestableentrynegative + S (dst_negative_row_zero_valuestable) = S ((S (dst_index_row_zero_valuestable)) * dst_negative_scale_row_zero_valuestable)) /\ exists ff_q_pvs_row_zero_valuestableentrynegative. dst_negative_code_row_zero_valuestable = ff_q_pvs_row_zero_valuestableentrynegative * S ((S (dst_index_row_zero_valuestable)) * dst_negative_scale_row_zero_valuestable) + (dst_negative_row_zero_valuestable))) /\ (exists ge_balance_positive_row_zero_valuestableentryvalue ge_balance_negative_row_zero_valuestableentryvalue. (((((dst_value_row_zero_valuestable) = 2 * (ge_balance_positive_row_zero_valuestableentryvalue) /\ (ge_balance_negative_row_zero_valuestableentryvalue) = 0) \/ exists ge_signed_half_row_zero_valuestableentryvaluedecode. (((dst_value_row_zero_valuestable) = 2 * ge_signed_half_row_zero_valuestableentryvaluedecode + 1 /\ (ge_balance_positive_row_zero_valuestableentryvalue) = 0) /\ (ge_balance_negative_row_zero_valuestableentryvalue) = S ge_signed_half_row_zero_valuestableentryvaluedecode))) /\ ((dst_positive_row_zero_valuestable) + ge_balance_negative_row_zero_valuestableentryvalue = (dst_negative_row_zero_valuestable) + ge_balance_positive_row_zero_valuestableentryvalue))))))))) /\ (forall dfg_factor_column_row_zero_values dfg_factor_value_row_zero_values. (exists pvs_le_gap_row_zero_valuesbound. pvs_le_gap_row_zero_valuesbound + (dfg_factor_column_row_zero_values) = (n)) -> (exists dst_positive_code_row_zero_valueslookup dst_positive_scale_row_zero_valueslookup dst_negative_code_row_zero_valueslookup dst_negative_scale_row_zero_valueslookup dst_positive_row_zero_valueslookup dst_negative_row_zero_valueslookup. (((V) = (((((dst_positive_code_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup)) * S ((dst_positive_code_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup)) + ((dst_positive_scale_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup))) + (((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) * S ((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) + ((dst_negative_scale_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)))) * S ((((dst_positive_code_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup)) * S ((dst_positive_code_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup)) + ((dst_positive_scale_row_zero_valueslookup) + (dst_positive_scale_row_zero_valueslookup))) + (((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) * S ((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) + ((dst_negative_scale_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)))) + ((((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) * S ((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) + ((dst_negative_scale_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup))) + (((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) * S ((dst_negative_code_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)) + ((dst_negative_scale_row_zero_valueslookup) + (dst_negative_scale_row_zero_valueslookup)))))) /\ (((((exists ff_h_pvs_row_zero_valueslookuppositive. ff_h_pvs_row_zero_valueslookuppositive + S (dst_positive_row_zero_valueslookup) = S ((S (dfg_factor_column_row_zero_values)) * dst_positive_scale_row_zero_valueslookup)) /\ exists ff_q_pvs_row_zero_valueslookuppositive. dst_positive_code_row_zero_valueslookup = ff_q_pvs_row_zero_valueslookuppositive * S ((S (dfg_factor_column_row_zero_values)) * dst_positive_scale_row_zero_valueslookup) + (dst_positive_row_zero_valueslookup))) /\ (((((exists ff_h_pvs_row_zero_valueslookupnegative. ff_h_pvs_row_zero_valueslookupnegative + S (dst_negative_row_zero_valueslookup) = S ((S (dfg_factor_column_row_zero_values)) * dst_negative_scale_row_zero_valueslookup)) /\ exists ff_q_pvs_row_zero_valueslookupnegative. dst_negative_code_row_zero_valueslookup = ff_q_pvs_row_zero_valueslookupnegative * S ((S (dfg_factor_column_row_zero_values)) * dst_negative_scale_row_zero_valueslookup) + (dst_negative_row_zero_valueslookup))) /\ (exists ge_balance_positive_row_zero_valueslookupvalue ge_balance_negative_row_zero_valueslookupvalue. (((((dfg_factor_value_row_zero_values) = 2 * (ge_balance_positive_row_zero_valueslookupvalue) /\ (ge_balance_negative_row_zero_valueslookupvalue) = 0) \/ exists ge_signed_half_row_zero_valueslookupvaluedecode. (((dfg_factor_value_row_zero_values) = 2 * ge_signed_half_row_zero_valueslookupvaluedecode + 1 /\ (ge_balance_positive_row_zero_valueslookupvalue) = 0) /\ (ge_balance_negative_row_zero_valueslookupvalue) = S ge_signed_half_row_zero_valueslookupvaluedecode))) /\ ((dst_positive_row_zero_valueslookup) + ge_balance_negative_row_zero_valueslookupvalue = (dst_negative_row_zero_valueslookup) + ge_balance_positive_row_zero_valueslookupvalue))))))))) -> ((((~((a)=0)) /\ (((~((dfg_factor_column_row_zero_values)=0)) /\ (exists dfg_middle_row_zero_valuesentry dfg_first_row_zero_valuesentry dfg_last_row_zero_valuesentry dfg_value_row_zero_valuesentry. (((n)=((a)*(dfg_factor_column_row_zero_values))*dfg_middle_row_zero_valuesentry) /\ (((exists dst_positive_code_row_zero_valuesentryfirst dst_positive_scale_row_zero_valuesentryfirst dst_negative_code_row_zero_valuesentryfirst dst_negative_scale_row_zero_valuesentryfirst dst_positive_row_zero_valuesentryfirst dst_negative_row_zero_valuesentryfirst. (((F) = (((((dst_positive_code_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst)) * S ((dst_positive_code_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst)) + ((dst_positive_scale_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst))) + (((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) * S ((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) + ((dst_negative_scale_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)))) * S ((((dst_positive_code_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst)) * S ((dst_positive_code_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst)) + ((dst_positive_scale_row_zero_valuesentryfirst) + (dst_positive_scale_row_zero_valuesentryfirst))) + (((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) * S ((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) + ((dst_negative_scale_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)))) + ((((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) * S ((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) + ((dst_negative_scale_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst))) + (((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) * S ((dst_negative_code_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)) + ((dst_negative_scale_row_zero_valuesentryfirst) + (dst_negative_scale_row_zero_valuesentryfirst)))))) /\ (((((exists ff_h_pvs_row_zero_valuesentryfirstpositive. ff_h_pvs_row_zero_valuesentryfirstpositive + S (dst_positive_row_zero_valuesentryfirst) = S ((S (a)) * dst_positive_scale_row_zero_valuesentryfirst)) /\ exists ff_q_pvs_row_zero_valuesentryfirstpositive. dst_positive_code_row_zero_valuesentryfirst = ff_q_pvs_row_zero_valuesentryfirstpositive * S ((S (a)) * dst_positive_scale_row_zero_valuesentryfirst) + (dst_positive_row_zero_valuesentryfirst))) /\ (((((exists ff_h_pvs_row_zero_valuesentryfirstnegative. ff_h_pvs_row_zero_valuesentryfirstnegative + S (dst_negative_row_zero_valuesentryfirst) = S ((S (a)) * dst_negative_scale_row_zero_valuesentryfirst)) /\ exists ff_q_pvs_row_zero_valuesentryfirstnegative. dst_negative_code_row_zero_valuesentryfirst = ff_q_pvs_row_zero_valuesentryfirstnegative * S ((S (a)) * dst_negative_scale_row_zero_valuesentryfirst) + (dst_negative_row_zero_valuesentryfirst))) /\ (exists ge_balance_positive_row_zero_valuesentryfirstvalue ge_balance_negative_row_zero_valuesentryfirstvalue. (((((dfg_first_row_zero_valuesentry) = 2 * (ge_balance_positive_row_zero_valuesentryfirstvalue) /\ (ge_balance_negative_row_zero_valuesentryfirstvalue) = 0) \/ exists ge_signed_half_row_zero_valuesentryfirstvaluedecode. (((dfg_first_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentryfirstvaluedecode + 1 /\ (ge_balance_positive_row_zero_valuesentryfirstvalue) = 0) /\ (ge_balance_negative_row_zero_valuesentryfirstvalue) = S ge_signed_half_row_zero_valuesentryfirstvaluedecode))) /\ ((dst_positive_row_zero_valuesentryfirst) + ge_balance_negative_row_zero_valuesentryfirstvalue = (dst_negative_row_zero_valuesentryfirst) + ge_balance_positive_row_zero_valuesentryfirstvalue))))))))) /\ (((exists dst_positive_code_row_zero_valuesentrylast dst_positive_scale_row_zero_valuesentrylast dst_negative_code_row_zero_valuesentrylast dst_negative_scale_row_zero_valuesentrylast dst_positive_row_zero_valuesentrylast dst_negative_row_zero_valuesentrylast. (((H) = (((((dst_positive_code_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast)) * S ((dst_positive_code_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast)) + ((dst_positive_scale_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast))) + (((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) * S ((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) + ((dst_negative_scale_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)))) * S ((((dst_positive_code_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast)) * S ((dst_positive_code_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast)) + ((dst_positive_scale_row_zero_valuesentrylast) + (dst_positive_scale_row_zero_valuesentrylast))) + (((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) * S ((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) + ((dst_negative_scale_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)))) + ((((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) * S ((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) + ((dst_negative_scale_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast))) + (((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) * S ((dst_negative_code_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)) + ((dst_negative_scale_row_zero_valuesentrylast) + (dst_negative_scale_row_zero_valuesentrylast)))))) /\ (((((exists ff_h_pvs_row_zero_valuesentrylastpositive. ff_h_pvs_row_zero_valuesentrylastpositive + S (dst_positive_row_zero_valuesentrylast) = S ((S (dfg_factor_column_row_zero_values)) * dst_positive_scale_row_zero_valuesentrylast)) /\ exists ff_q_pvs_row_zero_valuesentrylastpositive. dst_positive_code_row_zero_valuesentrylast = ff_q_pvs_row_zero_valuesentrylastpositive * S ((S (dfg_factor_column_row_zero_values)) * dst_positive_scale_row_zero_valuesentrylast) + (dst_positive_row_zero_valuesentrylast))) /\ (((((exists ff_h_pvs_row_zero_valuesentrylastnegative. ff_h_pvs_row_zero_valuesentrylastnegative + S (dst_negative_row_zero_valuesentrylast) = S ((S (dfg_factor_column_row_zero_values)) * dst_negative_scale_row_zero_valuesentrylast)) /\ exists ff_q_pvs_row_zero_valuesentrylastnegative. dst_negative_code_row_zero_valuesentrylast = ff_q_pvs_row_zero_valuesentrylastnegative * S ((S (dfg_factor_column_row_zero_values)) * dst_negative_scale_row_zero_valuesentrylast) + (dst_negative_row_zero_valuesentrylast))) /\ (exists ge_balance_positive_row_zero_valuesentrylastvalue ge_balance_negative_row_zero_valuesentrylastvalue. (((((dfg_last_row_zero_valuesentry) = 2 * (ge_balance_positive_row_zero_valuesentrylastvalue) /\ (ge_balance_negative_row_zero_valuesentrylastvalue) = 0) \/ exists ge_signed_half_row_zero_valuesentrylastvaluedecode. (((dfg_last_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentrylastvaluedecode + 1 /\ (ge_balance_positive_row_zero_valuesentrylastvalue) = 0) /\ (ge_balance_negative_row_zero_valuesentrylastvalue) = S ge_signed_half_row_zero_valuesentrylastvaluedecode))) /\ ((dst_positive_row_zero_valuesentrylast) + ge_balance_negative_row_zero_valuesentrylastvalue = (dst_negative_row_zero_valuesentrylast) + ge_balance_positive_row_zero_valuesentrylastvalue))))))))) /\ (((exists dst_positive_code_row_zero_valuesentrymiddle dst_positive_scale_row_zero_valuesentrymiddle dst_negative_code_row_zero_valuesentrymiddle dst_negative_scale_row_zero_valuesentrymiddle dst_positive_row_zero_valuesentrymiddle dst_negative_row_zero_valuesentrymiddle. (((G) = (((((dst_positive_code_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle)) * S ((dst_positive_code_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle)) + ((dst_positive_scale_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle))) + (((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) * S ((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) + ((dst_negative_scale_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)))) * S ((((dst_positive_code_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle)) * S ((dst_positive_code_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle)) + ((dst_positive_scale_row_zero_valuesentrymiddle) + (dst_positive_scale_row_zero_valuesentrymiddle))) + (((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) * S ((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) + ((dst_negative_scale_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)))) + ((((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) * S ((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) + ((dst_negative_scale_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle))) + (((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) * S ((dst_negative_code_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)) + ((dst_negative_scale_row_zero_valuesentrymiddle) + (dst_negative_scale_row_zero_valuesentrymiddle)))))) /\ (((((exists ff_h_pvs_row_zero_valuesentrymiddlepositive. ff_h_pvs_row_zero_valuesentrymiddlepositive + S (dst_positive_row_zero_valuesentrymiddle) = S ((S (dfg_middle_row_zero_valuesentry)) * dst_positive_scale_row_zero_valuesentrymiddle)) /\ exists ff_q_pvs_row_zero_valuesentrymiddlepositive. dst_positive_code_row_zero_valuesentrymiddle = ff_q_pvs_row_zero_valuesentrymiddlepositive * S ((S (dfg_middle_row_zero_valuesentry)) * dst_positive_scale_row_zero_valuesentrymiddle) + (dst_positive_row_zero_valuesentrymiddle))) /\ (((((exists ff_h_pvs_row_zero_valuesentrymiddlenegative. ff_h_pvs_row_zero_valuesentrymiddlenegative + S (dst_negative_row_zero_valuesentrymiddle) = S ((S (dfg_middle_row_zero_valuesentry)) * dst_negative_scale_row_zero_valuesentrymiddle)) /\ exists ff_q_pvs_row_zero_valuesentrymiddlenegative. dst_negative_code_row_zero_valuesentrymiddle = ff_q_pvs_row_zero_valuesentrymiddlenegative * S ((S (dfg_middle_row_zero_valuesentry)) * dst_negative_scale_row_zero_valuesentrymiddle) + (dst_negative_row_zero_valuesentrymiddle))) /\ (exists ge_balance_positive_row_zero_valuesentrymiddlevalue ge_balance_negative_row_zero_valuesentrymiddlevalue. (((((dfg_value_row_zero_valuesentry) = 2 * (ge_balance_positive_row_zero_valuesentrymiddlevalue) /\ (ge_balance_negative_row_zero_valuesentrymiddlevalue) = 0) \/ exists ge_signed_half_row_zero_valuesentrymiddlevaluedecode. (((dfg_value_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentrymiddlevaluedecode + 1 /\ (ge_balance_positive_row_zero_valuesentrymiddlevalue) = 0) /\ (ge_balance_negative_row_zero_valuesentrymiddlevalue) = S ge_signed_half_row_zero_valuesentrymiddlevaluedecode))) /\ ((dst_positive_row_zero_valuesentrymiddle) + ge_balance_negative_row_zero_valuesentrymiddlevalue = (dst_negative_row_zero_valuesentrymiddle) + ge_balance_positive_row_zero_valuesentrymiddlevalue))))))))) /\ (exists dfg_inner_row_zero_valuesentryproduct. ((exists sto_ap_row_zero_valuesentryproductinner sto_an_row_zero_valuesentryproductinner sto_bp_row_zero_valuesentryproductinner sto_bn_row_zero_valuesentryproductinner sto_cp_row_zero_valuesentryproductinner sto_cn_row_zero_valuesentryproductinner. (((((dfg_last_row_zero_valuesentry) = 2 * (sto_ap_row_zero_valuesentryproductinner) /\ (sto_an_row_zero_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductinnerleft. (((dfg_last_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentryproductinnerleft + 1 /\ (sto_ap_row_zero_valuesentryproductinner) = 0) /\ (sto_an_row_zero_valuesentryproductinner) = S ge_signed_half_row_zero_valuesentryproductinnerleft))) /\ ((((((dfg_value_row_zero_valuesentry) = 2 * (sto_bp_row_zero_valuesentryproductinner) /\ (sto_bn_row_zero_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductinnerright. (((dfg_value_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentryproductinnerright + 1 /\ (sto_bp_row_zero_valuesentryproductinner) = 0) /\ (sto_bn_row_zero_valuesentryproductinner) = S ge_signed_half_row_zero_valuesentryproductinnerright))) /\ ((((((dfg_inner_row_zero_valuesentryproduct) = 2 * (sto_cp_row_zero_valuesentryproductinner) /\ (sto_cn_row_zero_valuesentryproductinner) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductinneroutput. (((dfg_inner_row_zero_valuesentryproduct) = 2 * ge_signed_half_row_zero_valuesentryproductinneroutput + 1 /\ (sto_cp_row_zero_valuesentryproductinner) = 0) /\ (sto_cn_row_zero_valuesentryproductinner) = S ge_signed_half_row_zero_valuesentryproductinneroutput))) /\ ((sto_ap_row_zero_valuesentryproductinner * sto_bp_row_zero_valuesentryproductinner + sto_an_row_zero_valuesentryproductinner * sto_bn_row_zero_valuesentryproductinner) + sto_cn_row_zero_valuesentryproductinner = (sto_ap_row_zero_valuesentryproductinner * sto_bn_row_zero_valuesentryproductinner + sto_an_row_zero_valuesentryproductinner * sto_bp_row_zero_valuesentryproductinner) + sto_cp_row_zero_valuesentryproductinner))))))) /\ (exists sto_ap_row_zero_valuesentryproductouter sto_an_row_zero_valuesentryproductouter sto_bp_row_zero_valuesentryproductouter sto_bn_row_zero_valuesentryproductouter sto_cp_row_zero_valuesentryproductouter sto_cn_row_zero_valuesentryproductouter. (((((dfg_first_row_zero_valuesentry) = 2 * (sto_ap_row_zero_valuesentryproductouter) /\ (sto_an_row_zero_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductouterleft. (((dfg_first_row_zero_valuesentry) = 2 * ge_signed_half_row_zero_valuesentryproductouterleft + 1 /\ (sto_ap_row_zero_valuesentryproductouter) = 0) /\ (sto_an_row_zero_valuesentryproductouter) = S ge_signed_half_row_zero_valuesentryproductouterleft))) /\ ((((((dfg_inner_row_zero_valuesentryproduct) = 2 * (sto_bp_row_zero_valuesentryproductouter) /\ (sto_bn_row_zero_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductouterright. (((dfg_inner_row_zero_valuesentryproduct) = 2 * ge_signed_half_row_zero_valuesentryproductouterright + 1 /\ (sto_bp_row_zero_valuesentryproductouter) = 0) /\ (sto_bn_row_zero_valuesentryproductouter) = S ge_signed_half_row_zero_valuesentryproductouterright))) /\ ((((((dfg_factor_value_row_zero_values) = 2 * (sto_cp_row_zero_valuesentryproductouter) /\ (sto_cn_row_zero_valuesentryproductouter) = 0) \/ exists ge_signed_half_row_zero_valuesentryproductouteroutput. (((dfg_factor_value_row_zero_values) = 2 * ge_signed_half_row_zero_valuesentryproductouteroutput + 1 /\ (sto_cp_row_zero_valuesentryproductouter) = 0) /\ (sto_cn_row_zero_valuesentryproductouter) = S ge_signed_half_row_zero_valuesentryproductouteroutput))) /\ ((sto_ap_row_zero_valuesentryproductouter * sto_bp_row_zero_valuesentryproductouter + sto_an_row_zero_valuesentryproductouter * sto_bn_row_zero_valuesentryproductouter) + sto_cn_row_zero_valuesentryproductouter = (sto_ap_row_zero_valuesentryproductouter * sto_bn_row_zero_valuesentryproductouter + sto_an_row_zero_valuesentryproductouter * sto_bp_row_zero_valuesentryproductouter) + sto_cp_row_zero_valuesentryproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((dfg_factor_column_row_zero_values)=0 \/ ~(exists pvs_factor_row_zero_valuesentryomittednondivisor. (n) = ((a)*(dfg_factor_column_row_zero_values)) * pvs_factor_row_zero_valuesentryomittednondivisor))) /\ ((dfg_factor_value_row_zero_values)=0))))))) -> (a=0 \/ ~(exists pvs_factor_row_zero_guard. (n) = (a) * pvs_factor_row_zero_guard)) -> (exists dst_positive_code_row_zero_sum dst_positive_scale_row_zero_sum dst_negative_code_row_zero_sum dst_negative_scale_row_zero_sum dst_positive_sum_row_zero_sum dst_negative_sum_row_zero_sum. (((V) = (((((dst_positive_code_row_zero_sum) + (dst_positive_scale_row_zero_sum)) * S ((dst_positive_code_row_zero_sum) + (dst_positive_scale_row_zero_sum)) + ((dst_positive_scale_row_zero_sum) + (dst_positive_scale_row_zero_sum))) + (((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) * S ((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) + ((dst_negative_scale_row_zero_sum) + (dst_negative_scale_row_zero_sum)))) * S ((((dst_positive_code_row_zero_sum) + (dst_positive_scale_row_zero_sum)) * S ((dst_positive_code_row_zero_sum) + (dst_positive_scale_row_zero_sum)) + ((dst_positive_scale_row_zero_sum) + (dst_positive_scale_row_zero_sum))) + (((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) * S ((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) + ((dst_negative_scale_row_zero_sum) + (dst_negative_scale_row_zero_sum)))) + ((((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) * S ((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) + ((dst_negative_scale_row_zero_sum) + (dst_negative_scale_row_zero_sum))) + (((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) * S ((dst_negative_code_row_zero_sum) + (dst_negative_scale_row_zero_sum)) + ((dst_negative_scale_row_zero_sum) + (dst_negative_scale_row_zero_sum)))))) /\ (((exists fs_u_dst_row_zero_sumpositive fs_v_dst_row_zero_sumpositive. ((((exists fs_h_dst_row_zero_sumpositive_body_start. fs_h_dst_row_zero_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_row_zero_sumpositive)) /\ exists fs_q_dst_row_zero_sumpositive_body_start. fs_u_dst_row_zero_sumpositive = fs_q_dst_row_zero_sumpositive_body_start * S ((S (0)) * fs_v_dst_row_zero_sumpositive) + (0))) /\ ((((exists fs_h_dst_row_zero_sumpositive_body_terminal. fs_h_dst_row_zero_sumpositive_body_terminal + S (dst_positive_sum_row_zero_sum) = S ((S (S n)) * fs_v_dst_row_zero_sumpositive)) /\ exists fs_q_dst_row_zero_sumpositive_body_terminal. fs_u_dst_row_zero_sumpositive = fs_q_dst_row_zero_sumpositive_body_terminal * S ((S (S n)) * fs_v_dst_row_zero_sumpositive) + (dst_positive_sum_row_zero_sum))) /\ forall fs_i_dst_row_zero_sumpositive_body_steps. (exists fs_lt_dst_row_zero_sumpositive_body_steps_bound. fs_lt_dst_row_zero_sumpositive_body_steps_bound + S fs_i_dst_row_zero_sumpositive_body_steps = S n) -> exists fs_a_dst_row_zero_sumpositive_body_steps fs_r_dst_row_zero_sumpositive_body_steps fs_s_dst_row_zero_sumpositive_body_steps. ((((exists fs_h_dst_row_zero_sumpositive_body_steps_summand. fs_h_dst_row_zero_sumpositive_body_steps_summand + S (fs_a_dst_row_zero_sumpositive_body_steps) = S ((S (fs_i_dst_row_zero_sumpositive_body_steps)) * dst_positive_scale_row_zero_sum)) /\ exists fs_q_dst_row_zero_sumpositive_body_steps_summand. dst_positive_code_row_zero_sum = fs_q_dst_row_zero_sumpositive_body_steps_summand * S ((S (fs_i_dst_row_zero_sumpositive_body_steps)) * dst_positive_scale_row_zero_sum) + (fs_a_dst_row_zero_sumpositive_body_steps))) /\ ((((exists fs_h_dst_row_zero_sumpositive_body_steps_partial. fs_h_dst_row_zero_sumpositive_body_steps_partial + S (fs_r_dst_row_zero_sumpositive_body_steps) = S ((S (fs_i_dst_row_zero_sumpositive_body_steps)) * fs_v_dst_row_zero_sumpositive)) /\ exists fs_q_dst_row_zero_sumpositive_body_steps_partial. fs_u_dst_row_zero_sumpositive = fs_q_dst_row_zero_sumpositive_body_steps_partial * S ((S (fs_i_dst_row_zero_sumpositive_body_steps)) * fs_v_dst_row_zero_sumpositive) + (fs_r_dst_row_zero_sumpositive_body_steps))) /\ ((((exists fs_h_dst_row_zero_sumpositive_body_steps_successor. fs_h_dst_row_zero_sumpositive_body_steps_successor + S (fs_s_dst_row_zero_sumpositive_body_steps) = S ((S (S fs_i_dst_row_zero_sumpositive_body_steps)) * fs_v_dst_row_zero_sumpositive)) /\ exists fs_q_dst_row_zero_sumpositive_body_steps_successor. fs_u_dst_row_zero_sumpositive = fs_q_dst_row_zero_sumpositive_body_steps_successor * S ((S (S fs_i_dst_row_zero_sumpositive_body_steps)) * fs_v_dst_row_zero_sumpositive) + (fs_s_dst_row_zero_sumpositive_body_steps))) /\ fs_s_dst_row_zero_sumpositive_body_steps = fs_r_dst_row_zero_sumpositive_body_steps + fs_a_dst_row_zero_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_row_zero_sumnegative fs_v_dst_row_zero_sumnegative. ((((exists fs_h_dst_row_zero_sumnegative_body_start. fs_h_dst_row_zero_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_row_zero_sumnegative)) /\ exists fs_q_dst_row_zero_sumnegative_body_start. fs_u_dst_row_zero_sumnegative = fs_q_dst_row_zero_sumnegative_body_start * S ((S (0)) * fs_v_dst_row_zero_sumnegative) + (0))) /\ ((((exists fs_h_dst_row_zero_sumnegative_body_terminal. fs_h_dst_row_zero_sumnegative_body_terminal + S (dst_negative_sum_row_zero_sum) = S ((S (S n)) * fs_v_dst_row_zero_sumnegative)) /\ exists fs_q_dst_row_zero_sumnegative_body_terminal. fs_u_dst_row_zero_sumnegative = fs_q_dst_row_zero_sumnegative_body_terminal * S ((S (S n)) * fs_v_dst_row_zero_sumnegative) + (dst_negative_sum_row_zero_sum))) /\ forall fs_i_dst_row_zero_sumnegative_body_steps. (exists fs_lt_dst_row_zero_sumnegative_body_steps_bound. fs_lt_dst_row_zero_sumnegative_body_steps_bound + S fs_i_dst_row_zero_sumnegative_body_steps = S n) -> exists fs_a_dst_row_zero_sumnegative_body_steps fs_r_dst_row_zero_sumnegative_body_steps fs_s_dst_row_zero_sumnegative_body_steps. ((((exists fs_h_dst_row_zero_sumnegative_body_steps_summand. fs_h_dst_row_zero_sumnegative_body_steps_summand + S (fs_a_dst_row_zero_sumnegative_body_steps) = S ((S (fs_i_dst_row_zero_sumnegative_body_steps)) * dst_negative_scale_row_zero_sum)) /\ exists fs_q_dst_row_zero_sumnegative_body_steps_summand. dst_negative_code_row_zero_sum = fs_q_dst_row_zero_sumnegative_body_steps_summand * S ((S (fs_i_dst_row_zero_sumnegative_body_steps)) * dst_negative_scale_row_zero_sum) + (fs_a_dst_row_zero_sumnegative_body_steps))) /\ ((((exists fs_h_dst_row_zero_sumnegative_body_steps_partial. fs_h_dst_row_zero_sumnegative_body_steps_partial + S (fs_r_dst_row_zero_sumnegative_body_steps) = S ((S (fs_i_dst_row_zero_sumnegative_body_steps)) * fs_v_dst_row_zero_sumnegative)) /\ exists fs_q_dst_row_zero_sumnegative_body_steps_partial. fs_u_dst_row_zero_sumnegative = fs_q_dst_row_zero_sumnegative_body_steps_partial * S ((S (fs_i_dst_row_zero_sumnegative_body_steps)) * fs_v_dst_row_zero_sumnegative) + (fs_r_dst_row_zero_sumnegative_body_steps))) /\ ((((exists fs_h_dst_row_zero_sumnegative_body_steps_successor. fs_h_dst_row_zero_sumnegative_body_steps_successor + S (fs_s_dst_row_zero_sumnegative_body_steps) = S ((S (S fs_i_dst_row_zero_sumnegative_body_steps)) * fs_v_dst_row_zero_sumnegative)) /\ exists fs_q_dst_row_zero_sumnegative_body_steps_successor. fs_u_dst_row_zero_sumnegative = fs_q_dst_row_zero_sumnegative_body_steps_successor * S ((S (S fs_i_dst_row_zero_sumnegative_body_steps)) * fs_v_dst_row_zero_sumnegative) + (fs_s_dst_row_zero_sumnegative_body_steps))) /\ fs_s_dst_row_zero_sumnegative_body_steps = fs_r_dst_row_zero_sumnegative_body_steps + fs_a_dst_row_zero_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_row_zero_sumresult ge_balance_negative_row_zero_sumresult. (((((z) = 2 * (ge_balance_positive_row_zero_sumresult) /\ (ge_balance_negative_row_zero_sumresult) = 0) \/ exists ge_signed_half_row_zero_sumresultdecode. (((z) = 2 * ge_signed_half_row_zero_sumresultdecode + 1 /\ (ge_balance_positive_row_zero_sumresult) = 0) /\ (ge_balance_negative_row_zero_sumresult) = S ge_signed_half_row_zero_sumresultdecode))) /\ ((dst_positive_sum_row_zero_sum) + ge_balance_negative_row_zero_sumresult = (dst_negative_sum_row_zero_sum) + ge_balance_positive_row_zero_sumresult))))))))) -> z=0