dirichlet_factor_row_scalar

forall F G H n a q u V P. ~(a=0) -> n=a*q -> (exists dst_positive_code_row_scalar_first dst_positive_scale_row_scalar_first dst_negative_code_row_scalar_first dst_negative_scale_row_scalar_first dst_positive_row_scalar_first dst_negative_row_scalar_first. (((F) = (((((dst_positive_code_row_scalar_first) + (dst_positive_scale_row_scalar_first)) * S ((dst_positive_code_row_scalar_first) + (dst_positive_scale_row_scalar_first)) + ((dst_positive_scale_row_scalar_first) + (dst_positive_scale_row_scalar_first))) + (((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) * S ((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) + ((dst_negative_scale_row_scalar_first) + (dst_negative_scale_row_scalar_first)))) * S ((((dst_positive_code_row_scalar_first) + (dst_positive_scale_row_scalar_first)) * S ((dst_positive_code_row_scalar_first) + (dst_positive_scale_row_scalar_first)) + ((dst_positive_scale_row_scalar_first) + (dst_positive_scale_row_scalar_first))) + (((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) * S ((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) + ((dst_negative_scale_row_scalar_first) + (dst_negative_scale_row_scalar_first)))) + ((((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) * S ((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) + ((dst_negative_scale_row_scalar_first) + (dst_negative_scale_row_scalar_first))) + (((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) * S ((dst_negative_code_row_scalar_first) + (dst_negative_scale_row_scalar_first)) + ((dst_negative_scale_row_scalar_first) + (dst_negative_scale_row_scalar_first)))))) /\ (((((exists ff_h_pvs_row_scalar_firstpositive. ff_h_pvs_row_scalar_firstpositive + S (dst_positive_row_scalar_first) = S ((S (a)) * dst_positive_scale_row_scalar_first)) /\ exists ff_q_pvs_row_scalar_firstpositive. dst_positive_code_row_scalar_first = ff_q_pvs_row_scalar_firstpositive * S ((S (a)) * dst_positive_scale_row_scalar_first) + (dst_positive_row_scalar_first))) /\ (((((exists ff_h_pvs_row_scalar_firstnegative. ff_h_pvs_row_scalar_firstnegative + S (dst_negative_row_scalar_first) = S ((S (a)) * dst_negative_scale_row_scalar_first)) /\ exists ff_q_pvs_row_scalar_firstnegative. dst_negative_code_row_scalar_first = ff_q_pvs_row_scalar_firstnegative * S ((S (a)) * dst_negative_scale_row_scalar_first) + (dst_negative_row_scalar_first))) /\ (exists ge_balance_positive_row_scalar_firstvalue ge_balance_negative_row_scalar_firstvalue. (((((u) = 2 * (ge_balance_positive_row_scalar_firstvalue) /\ (ge_balance_negative_row_scalar_firstvalue) = 0) \/ exists ge_signed_half_row_scalar_firstvaluedecode. (((u) = 2 * ge_signed_half_row_scalar_firstvaluedecode + 1 /\ (ge_balance_positive_row_scalar_firstvalue) = 0) /\ (ge_balance_negative_row_scalar_firstvalue) = S ge_signed_half_row_scalar_firstvaluedecode))) /\ ((dst_positive_row_scalar_first) + ge_balance_negative_row_scalar_firstvalue = (dst_negative_row_scalar_first) + ge_balance_positive_row_scalar_firstvalue))))))))) -> (((exists dst_positive_code_row_scalar_prefixtable dst_positive_scale_row_scalar_prefixtable dst_negative_code_row_scalar_prefixtable dst_negative_scale_row_scalar_prefixtable. (((P) = (((((dst_positive_code_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable)) * S ((dst_positive_code_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable)) + ((dst_positive_scale_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable))) + (((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) * S ((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) + ((dst_negative_scale_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)))) * S ((((dst_positive_code_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable)) * S ((dst_positive_code_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable)) + ((dst_positive_scale_row_scalar_prefixtable) + (dst_positive_scale_row_scalar_prefixtable))) + (((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) * S ((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) + ((dst_negative_scale_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)))) + ((((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) * S ((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) + ((dst_negative_scale_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable))) + (((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) * S ((dst_negative_code_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)) + ((dst_negative_scale_row_scalar_prefixtable) + (dst_negative_scale_row_scalar_prefixtable)))))) /\ (forall dst_index_row_scalar_prefixtable. (exists pvs_le_gap_row_scalar_prefixtabledomain. pvs_le_gap_row_scalar_prefixtabledomain + (dst_index_row_scalar_prefixtable) = (n)) -> exists dst_positive_row_scalar_prefixtable dst_negative_row_scalar_prefixtable dst_value_row_scalar_prefixtable. ((((exists ff_h_pvs_row_scalar_prefixtableentrypositive. ff_h_pvs_row_scalar_prefixtableentrypositive + S (dst_positive_row_scalar_prefixtable) = S ((S (dst_index_row_scalar_prefixtable)) * dst_positive_scale_row_scalar_prefixtable)) /\ exists ff_q_pvs_row_scalar_prefixtableentrypositive. dst_positive_code_row_scalar_prefixtable = ff_q_pvs_row_scalar_prefixtableentrypositive * S ((S (dst_index_row_scalar_prefixtable)) * dst_positive_scale_row_scalar_prefixtable) + (dst_positive_row_scalar_prefixtable))) /\ (((((exists ff_h_pvs_row_scalar_prefixtableentrynegative. ff_h_pvs_row_scalar_prefixtableentrynegative + S (dst_negative_row_scalar_prefixtable) = S ((S (dst_index_row_scalar_prefixtable)) * dst_negative_scale_row_scalar_prefixtable)) /\ exists ff_q_pvs_row_scalar_prefixtableentrynegative. dst_negative_code_row_scalar_prefixtable = ff_q_pvs_row_scalar_prefixtableentrynegative * S ((S (dst_index_row_scalar_prefixtable)) * dst_negative_scale_row_scalar_prefixtable) + (dst_negative_row_scalar_prefixtable))) /\ (exists ge_balance_positive_row_scalar_prefixtableentryvalue ge_balance_negative_row_scalar_prefixtableentryvalue. (((((dst_value_row_scalar_prefixtable) = 2 * (ge_balance_positive_row_scalar_prefixtableentryvalue) /\ (ge_balance_negative_row_scalar_prefixtableentryvalue) = 0) \/ exists ge_signed_half_row_scalar_prefixtableentryvaluedecode. (((dst_value_row_scalar_prefixtable) = 2 * ge_signed_half_row_scalar_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_row_scalar_prefixtableentryvalue) = 0) /\ (ge_balance_negative_row_scalar_prefixtableentryvalue) = S ge_signed_half_row_scalar_prefixtableentryvaluedecode))) /\ ((dst_positive_row_scalar_prefixtable) + ge_balance_negative_row_scalar_prefixtableentryvalue = (dst_negative_row_scalar_prefixtable) + ge_balance_positive_row_scalar_prefixtableentryvalue))))))))) /\ (forall dc_index_row_scalar_prefix dc_value_row_scalar_prefix. (exists pvs_le_gap_row_scalar_prefixdomain. pvs_le_gap_row_scalar_prefixdomain + (dc_index_row_scalar_prefix) = (n)) -> (exists dst_positive_code_row_scalar_prefixlookup dst_positive_scale_row_scalar_prefixlookup dst_negative_code_row_scalar_prefixlookup dst_negative_scale_row_scalar_prefixlookup dst_positive_row_scalar_prefixlookup dst_negative_row_scalar_prefixlookup. (((P) = (((((dst_positive_code_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup)) * S ((dst_positive_code_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup)) + ((dst_positive_scale_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup))) + (((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) * S ((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) + ((dst_negative_scale_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)))) * S ((((dst_positive_code_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup)) * S ((dst_positive_code_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup)) + ((dst_positive_scale_row_scalar_prefixlookup) + (dst_positive_scale_row_scalar_prefixlookup))) + (((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) * S ((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) + ((dst_negative_scale_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)))) + ((((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) * S ((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) + ((dst_negative_scale_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup))) + (((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) * S ((dst_negative_code_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)) + ((dst_negative_scale_row_scalar_prefixlookup) + (dst_negative_scale_row_scalar_prefixlookup)))))) /\ (((((exists ff_h_pvs_row_scalar_prefixlookuppositive. ff_h_pvs_row_scalar_prefixlookuppositive + S (dst_positive_row_scalar_prefixlookup) = S ((S (dc_index_row_scalar_prefix)) * dst_positive_scale_row_scalar_prefixlookup)) /\ exists ff_q_pvs_row_scalar_prefixlookuppositive. dst_positive_code_row_scalar_prefixlookup = ff_q_pvs_row_scalar_prefixlookuppositive * S ((S (dc_index_row_scalar_prefix)) * dst_positive_scale_row_scalar_prefixlookup) + (dst_positive_row_scalar_prefixlookup))) /\ (((((exists ff_h_pvs_row_scalar_prefixlookupnegative. ff_h_pvs_row_scalar_prefixlookupnegative + S (dst_negative_row_scalar_prefixlookup) = S ((S (dc_index_row_scalar_prefix)) * dst_negative_scale_row_scalar_prefixlookup)) /\ exists ff_q_pvs_row_scalar_prefixlookupnegative. dst_negative_code_row_scalar_prefixlookup = ff_q_pvs_row_scalar_prefixlookupnegative * S ((S (dc_index_row_scalar_prefix)) * dst_negative_scale_row_scalar_prefixlookup) + (dst_negative_row_scalar_prefixlookup))) /\ (exists ge_balance_positive_row_scalar_prefixlookupvalue ge_balance_negative_row_scalar_prefixlookupvalue. (((((dc_value_row_scalar_prefix) = 2 * (ge_balance_positive_row_scalar_prefixlookupvalue) /\ (ge_balance_negative_row_scalar_prefixlookupvalue) = 0) \/ exists ge_signed_half_row_scalar_prefixlookupvaluedecode. (((dc_value_row_scalar_prefix) = 2 * ge_signed_half_row_scalar_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_row_scalar_prefixlookupvalue) = 0) /\ (ge_balance_negative_row_scalar_prefixlookupvalue) = S ge_signed_half_row_scalar_prefixlookupvaluedecode))) /\ ((dst_positive_row_scalar_prefixlookup) + ge_balance_negative_row_scalar_prefixlookupvalue = (dst_negative_row_scalar_prefixlookup) + ge_balance_positive_row_scalar_prefixlookupvalue))))))))) -> ((((~((dc_index_row_scalar_prefix)=0)) /\ (exists dc_quotient_row_scalar_prefixentry dc_left_row_scalar_prefixentry dc_right_row_scalar_prefixentry. (((q)=(dc_index_row_scalar_prefix)*dc_quotient_row_scalar_prefixentry) /\ (((exists dst_positive_code_row_scalar_prefixentryleft dst_positive_scale_row_scalar_prefixentryleft dst_negative_code_row_scalar_prefixentryleft dst_negative_scale_row_scalar_prefixentryleft dst_positive_row_scalar_prefixentryleft dst_negative_row_scalar_prefixentryleft. (((H) = (((((dst_positive_code_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft)) * S ((dst_positive_code_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft)) + ((dst_positive_scale_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft))) + (((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) * S ((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) + ((dst_negative_scale_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)))) * S ((((dst_positive_code_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft)) * S ((dst_positive_code_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft)) + ((dst_positive_scale_row_scalar_prefixentryleft) + (dst_positive_scale_row_scalar_prefixentryleft))) + (((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) * S ((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) + ((dst_negative_scale_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)))) + ((((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) * S ((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) + ((dst_negative_scale_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft))) + (((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) * S ((dst_negative_code_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)) + ((dst_negative_scale_row_scalar_prefixentryleft) + (dst_negative_scale_row_scalar_prefixentryleft)))))) /\ (((((exists ff_h_pvs_row_scalar_prefixentryleftpositive. ff_h_pvs_row_scalar_prefixentryleftpositive + S (dst_positive_row_scalar_prefixentryleft) = S ((S (dc_index_row_scalar_prefix)) * dst_positive_scale_row_scalar_prefixentryleft)) /\ exists ff_q_pvs_row_scalar_prefixentryleftpositive. dst_positive_code_row_scalar_prefixentryleft = ff_q_pvs_row_scalar_prefixentryleftpositive * S ((S (dc_index_row_scalar_prefix)) * dst_positive_scale_row_scalar_prefixentryleft) + (dst_positive_row_scalar_prefixentryleft))) /\ (((((exists ff_h_pvs_row_scalar_prefixentryleftnegative. ff_h_pvs_row_scalar_prefixentryleftnegative + S (dst_negative_row_scalar_prefixentryleft) = S ((S (dc_index_row_scalar_prefix)) * dst_negative_scale_row_scalar_prefixentryleft)) /\ exists ff_q_pvs_row_scalar_prefixentryleftnegative. dst_negative_code_row_scalar_prefixentryleft = ff_q_pvs_row_scalar_prefixentryleftnegative * S ((S (dc_index_row_scalar_prefix)) * dst_negative_scale_row_scalar_prefixentryleft) + (dst_negative_row_scalar_prefixentryleft))) /\ (exists ge_balance_positive_row_scalar_prefixentryleftvalue ge_balance_negative_row_scalar_prefixentryleftvalue. (((((dc_left_row_scalar_prefixentry) = 2 * (ge_balance_positive_row_scalar_prefixentryleftvalue) /\ (ge_balance_negative_row_scalar_prefixentryleftvalue) = 0) \/ exists ge_signed_half_row_scalar_prefixentryleftvaluedecode. (((dc_left_row_scalar_prefixentry) = 2 * ge_signed_half_row_scalar_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_row_scalar_prefixentryleftvalue) = 0) /\ (ge_balance_negative_row_scalar_prefixentryleftvalue) = S ge_signed_half_row_scalar_prefixentryleftvaluedecode))) /\ ((dst_positive_row_scalar_prefixentryleft) + ge_balance_negative_row_scalar_prefixentryleftvalue = (dst_negative_row_scalar_prefixentryleft) + ge_balance_positive_row_scalar_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_row_scalar_prefixentryright dst_positive_scale_row_scalar_prefixentryright dst_negative_code_row_scalar_prefixentryright dst_negative_scale_row_scalar_prefixentryright dst_positive_row_scalar_prefixentryright dst_negative_row_scalar_prefixentryright. (((G) = (((((dst_positive_code_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright)) * S ((dst_positive_code_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright)) + ((dst_positive_scale_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright))) + (((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) * S ((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) + ((dst_negative_scale_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)))) * S ((((dst_positive_code_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright)) * S ((dst_positive_code_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright)) + ((dst_positive_scale_row_scalar_prefixentryright) + (dst_positive_scale_row_scalar_prefixentryright))) + (((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) * S ((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) + ((dst_negative_scale_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)))) + ((((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) * S ((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) + ((dst_negative_scale_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright))) + (((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) * S ((dst_negative_code_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)) + ((dst_negative_scale_row_scalar_prefixentryright) + (dst_negative_scale_row_scalar_prefixentryright)))))) /\ (((((exists ff_h_pvs_row_scalar_prefixentryrightpositive. ff_h_pvs_row_scalar_prefixentryrightpositive + S (dst_positive_row_scalar_prefixentryright) = S ((S (dc_quotient_row_scalar_prefixentry)) * dst_positive_scale_row_scalar_prefixentryright)) /\ exists ff_q_pvs_row_scalar_prefixentryrightpositive. dst_positive_code_row_scalar_prefixentryright = ff_q_pvs_row_scalar_prefixentryrightpositive * S ((S (dc_quotient_row_scalar_prefixentry)) * dst_positive_scale_row_scalar_prefixentryright) + (dst_positive_row_scalar_prefixentryright))) /\ (((((exists ff_h_pvs_row_scalar_prefixentryrightnegative. ff_h_pvs_row_scalar_prefixentryrightnegative + S (dst_negative_row_scalar_prefixentryright) = S ((S (dc_quotient_row_scalar_prefixentry)) * dst_negative_scale_row_scalar_prefixentryright)) /\ exists ff_q_pvs_row_scalar_prefixentryrightnegative. dst_negative_code_row_scalar_prefixentryright = ff_q_pvs_row_scalar_prefixentryrightnegative * S ((S (dc_quotient_row_scalar_prefixentry)) * dst_negative_scale_row_scalar_prefixentryright) + (dst_negative_row_scalar_prefixentryright))) /\ (exists ge_balance_positive_row_scalar_prefixentryrightvalue ge_balance_negative_row_scalar_prefixentryrightvalue. (((((dc_right_row_scalar_prefixentry) = 2 * (ge_balance_positive_row_scalar_prefixentryrightvalue) /\ (ge_balance_negative_row_scalar_prefixentryrightvalue) = 0) \/ exists ge_signed_half_row_scalar_prefixentryrightvaluedecode. (((dc_right_row_scalar_prefixentry) = 2 * ge_signed_half_row_scalar_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_row_scalar_prefixentryrightvalue) = 0) /\ (ge_balance_negative_row_scalar_prefixentryrightvalue) = S ge_signed_half_row_scalar_prefixentryrightvaluedecode))) /\ ((dst_positive_row_scalar_prefixentryright) + ge_balance_negative_row_scalar_prefixentryrightvalue = (dst_negative_row_scalar_prefixentryright) + ge_balance_positive_row_scalar_prefixentryrightvalue))))))))) /\ (exists sto_ap_row_scalar_prefixentryproduct sto_an_row_scalar_prefixentryproduct sto_bp_row_scalar_prefixentryproduct sto_bn_row_scalar_prefixentryproduct sto_cp_row_scalar_prefixentryproduct sto_cn_row_scalar_prefixentryproduct. (((((dc_left_row_scalar_prefixentry) = 2 * (sto_ap_row_scalar_prefixentryproduct) /\ (sto_an_row_scalar_prefixentryproduct) = 0) \/ exists ge_signed_half_row_scalar_prefixentryproductleft. (((dc_left_row_scalar_prefixentry) = 2 * ge_signed_half_row_scalar_prefixentryproductleft + 1 /\ (sto_ap_row_scalar_prefixentryproduct) = 0) /\ (sto_an_row_scalar_prefixentryproduct) = S ge_signed_half_row_scalar_prefixentryproductleft))) /\ ((((((dc_right_row_scalar_prefixentry) = 2 * (sto_bp_row_scalar_prefixentryproduct) /\ (sto_bn_row_scalar_prefixentryproduct) = 0) \/ exists ge_signed_half_row_scalar_prefixentryproductright. (((dc_right_row_scalar_prefixentry) = 2 * ge_signed_half_row_scalar_prefixentryproductright + 1 /\ (sto_bp_row_scalar_prefixentryproduct) = 0) /\ (sto_bn_row_scalar_prefixentryproduct) = S ge_signed_half_row_scalar_prefixentryproductright))) /\ ((((((dc_value_row_scalar_prefix) = 2 * (sto_cp_row_scalar_prefixentryproduct) /\ (sto_cn_row_scalar_prefixentryproduct) = 0) \/ exists ge_signed_half_row_scalar_prefixentryproductoutput. (((dc_value_row_scalar_prefix) = 2 * ge_signed_half_row_scalar_prefixentryproductoutput + 1 /\ (sto_cp_row_scalar_prefixentryproduct) = 0) /\ (sto_cn_row_scalar_prefixentryproduct) = S ge_signed_half_row_scalar_prefixentryproductoutput))) /\ ((sto_ap_row_scalar_prefixentryproduct * sto_bp_row_scalar_prefixentryproduct + sto_an_row_scalar_prefixentryproduct * sto_bn_row_scalar_prefixentryproduct) + sto_cn_row_scalar_prefixentryproduct = (sto_ap_row_scalar_prefixentryproduct * sto_bn_row_scalar_prefixentryproduct + sto_an_row_scalar_prefixentryproduct * sto_bp_row_scalar_prefixentryproduct) + sto_cp_row_scalar_prefixentryproduct))))))))))))))) \/ ((((dc_index_row_scalar_prefix)=0 \/ ~(exists pvs_factor_row_scalar_prefixentrynondivisor. (q) = (dc_index_row_scalar_prefix) * pvs_factor_row_scalar_prefixentrynondivisor)) /\ ((dc_value_row_scalar_prefix)=0))))))) -> (((exists dst_positive_code_row_scalar_cellstable dst_positive_scale_row_scalar_cellstable dst_negative_code_row_scalar_cellstable dst_negative_scale_row_scalar_cellstable. (((V) = (((((dst_positive_code_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable)) * S ((dst_positive_code_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable)) + ((dst_positive_scale_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable))) + (((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) * S ((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) + ((dst_negative_scale_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)))) * S ((((dst_positive_code_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable)) * S ((dst_positive_code_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable)) + ((dst_positive_scale_row_scalar_cellstable) + (dst_positive_scale_row_scalar_cellstable))) + (((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) * S ((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) + ((dst_negative_scale_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)))) + ((((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) * S ((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) + ((dst_negative_scale_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable))) + (((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) * S ((dst_negative_code_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)) + ((dst_negative_scale_row_scalar_cellstable) + (dst_negative_scale_row_scalar_cellstable)))))) /\ (forall dst_index_row_scalar_cellstable. (exists pvs_le_gap_row_scalar_cellstabledomain. pvs_le_gap_row_scalar_cellstabledomain + (dst_index_row_scalar_cellstable) = (S (n))) -> exists dst_positive_row_scalar_cellstable dst_negative_row_scalar_cellstable dst_value_row_scalar_cellstable. ((((exists ff_h_pvs_row_scalar_cellstableentrypositive. ff_h_pvs_row_scalar_cellstableentrypositive + S (dst_positive_row_scalar_cellstable) = S ((S (dst_index_row_scalar_cellstable)) * dst_positive_scale_row_scalar_cellstable)) /\ exists ff_q_pvs_row_scalar_cellstableentrypositive. dst_positive_code_row_scalar_cellstable = ff_q_pvs_row_scalar_cellstableentrypositive * S ((S (dst_index_row_scalar_cellstable)) * dst_positive_scale_row_scalar_cellstable) + (dst_positive_row_scalar_cellstable))) /\ (((((exists ff_h_pvs_row_scalar_cellstableentrynegative. ff_h_pvs_row_scalar_cellstableentrynegative + S (dst_negative_row_scalar_cellstable) = S ((S (dst_index_row_scalar_cellstable)) * dst_negative_scale_row_scalar_cellstable)) /\ exists ff_q_pvs_row_scalar_cellstableentrynegative. dst_negative_code_row_scalar_cellstable = ff_q_pvs_row_scalar_cellstableentrynegative * S ((S (dst_index_row_scalar_cellstable)) * dst_negative_scale_row_scalar_cellstable) + (dst_negative_row_scalar_cellstable))) /\ (exists ge_balance_positive_row_scalar_cellstableentryvalue ge_balance_negative_row_scalar_cellstableentryvalue. (((((dst_value_row_scalar_cellstable) = 2 * (ge_balance_positive_row_scalar_cellstableentryvalue) /\ (ge_balance_negative_row_scalar_cellstableentryvalue) = 0) \/ exists ge_signed_half_row_scalar_cellstableentryvaluedecode. (((dst_value_row_scalar_cellstable) = 2 * ge_signed_half_row_scalar_cellstableentryvaluedecode + 1 /\ (ge_balance_positive_row_scalar_cellstableentryvalue) = 0) /\ (ge_balance_negative_row_scalar_cellstableentryvalue) = S ge_signed_half_row_scalar_cellstableentryvaluedecode))) /\ ((dst_positive_row_scalar_cellstable) + ge_balance_negative_row_scalar_cellstableentryvalue = (dst_negative_row_scalar_cellstable) + ge_balance_positive_row_scalar_cellstableentryvalue))))))))) /\ (forall dfg_factor_column_row_scalar_cells dfg_factor_value_row_scalar_cells. (exists pvs_le_gap_row_scalar_cellsbound. pvs_le_gap_row_scalar_cellsbound + (dfg_factor_column_row_scalar_cells) = (n)) -> (exists dst_positive_code_row_scalar_cellslookup dst_positive_scale_row_scalar_cellslookup dst_negative_code_row_scalar_cellslookup dst_negative_scale_row_scalar_cellslookup dst_positive_row_scalar_cellslookup dst_negative_row_scalar_cellslookup. (((V) = (((((dst_positive_code_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup)) * S ((dst_positive_code_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup)) + ((dst_positive_scale_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup))) + (((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) * S ((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) + ((dst_negative_scale_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)))) * S ((((dst_positive_code_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup)) * S ((dst_positive_code_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup)) + ((dst_positive_scale_row_scalar_cellslookup) + (dst_positive_scale_row_scalar_cellslookup))) + (((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) * S ((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) + ((dst_negative_scale_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)))) + ((((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) * S ((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) + ((dst_negative_scale_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup))) + (((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) * S ((dst_negative_code_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)) + ((dst_negative_scale_row_scalar_cellslookup) + (dst_negative_scale_row_scalar_cellslookup)))))) /\ (((((exists ff_h_pvs_row_scalar_cellslookuppositive. ff_h_pvs_row_scalar_cellslookuppositive + S (dst_positive_row_scalar_cellslookup) = S ((S (dfg_factor_column_row_scalar_cells)) * dst_positive_scale_row_scalar_cellslookup)) /\ exists ff_q_pvs_row_scalar_cellslookuppositive. dst_positive_code_row_scalar_cellslookup = ff_q_pvs_row_scalar_cellslookuppositive * S ((S (dfg_factor_column_row_scalar_cells)) * dst_positive_scale_row_scalar_cellslookup) + (dst_positive_row_scalar_cellslookup))) /\ (((((exists ff_h_pvs_row_scalar_cellslookupnegative. ff_h_pvs_row_scalar_cellslookupnegative + S (dst_negative_row_scalar_cellslookup) = S ((S (dfg_factor_column_row_scalar_cells)) * dst_negative_scale_row_scalar_cellslookup)) /\ exists ff_q_pvs_row_scalar_cellslookupnegative. dst_negative_code_row_scalar_cellslookup = ff_q_pvs_row_scalar_cellslookupnegative * S ((S (dfg_factor_column_row_scalar_cells)) * dst_negative_scale_row_scalar_cellslookup) + (dst_negative_row_scalar_cellslookup))) /\ (exists ge_balance_positive_row_scalar_cellslookupvalue ge_balance_negative_row_scalar_cellslookupvalue. (((((dfg_factor_value_row_scalar_cells) = 2 * (ge_balance_positive_row_scalar_cellslookupvalue) /\ (ge_balance_negative_row_scalar_cellslookupvalue) = 0) \/ exists ge_signed_half_row_scalar_cellslookupvaluedecode. (((dfg_factor_value_row_scalar_cells) = 2 * ge_signed_half_row_scalar_cellslookupvaluedecode + 1 /\ (ge_balance_positive_row_scalar_cellslookupvalue) = 0) /\ (ge_balance_negative_row_scalar_cellslookupvalue) = S ge_signed_half_row_scalar_cellslookupvaluedecode))) /\ ((dst_positive_row_scalar_cellslookup) + ge_balance_negative_row_scalar_cellslookupvalue = (dst_negative_row_scalar_cellslookup) + ge_balance_positive_row_scalar_cellslookupvalue))))))))) -> ((((~((a)=0)) /\ (((~((dfg_factor_column_row_scalar_cells)=0)) /\ (exists dfg_middle_row_scalar_cellsentry dfg_first_row_scalar_cellsentry dfg_last_row_scalar_cellsentry dfg_value_row_scalar_cellsentry. (((n)=((a)*(dfg_factor_column_row_scalar_cells))*dfg_middle_row_scalar_cellsentry) /\ (((exists dst_positive_code_row_scalar_cellsentryfirst dst_positive_scale_row_scalar_cellsentryfirst dst_negative_code_row_scalar_cellsentryfirst dst_negative_scale_row_scalar_cellsentryfirst dst_positive_row_scalar_cellsentryfirst dst_negative_row_scalar_cellsentryfirst. (((F) = (((((dst_positive_code_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst)) * S ((dst_positive_code_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst)) + ((dst_positive_scale_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst))) + (((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) * S ((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) + ((dst_negative_scale_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)))) * S ((((dst_positive_code_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst)) * S ((dst_positive_code_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst)) + ((dst_positive_scale_row_scalar_cellsentryfirst) + (dst_positive_scale_row_scalar_cellsentryfirst))) + (((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) * S ((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) + ((dst_negative_scale_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)))) + ((((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) * S ((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) + ((dst_negative_scale_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst))) + (((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) * S ((dst_negative_code_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)) + ((dst_negative_scale_row_scalar_cellsentryfirst) + (dst_negative_scale_row_scalar_cellsentryfirst)))))) /\ (((((exists ff_h_pvs_row_scalar_cellsentryfirstpositive. ff_h_pvs_row_scalar_cellsentryfirstpositive + S (dst_positive_row_scalar_cellsentryfirst) = S ((S (a)) * dst_positive_scale_row_scalar_cellsentryfirst)) /\ exists ff_q_pvs_row_scalar_cellsentryfirstpositive. dst_positive_code_row_scalar_cellsentryfirst = ff_q_pvs_row_scalar_cellsentryfirstpositive * S ((S (a)) * dst_positive_scale_row_scalar_cellsentryfirst) + (dst_positive_row_scalar_cellsentryfirst))) /\ (((((exists ff_h_pvs_row_scalar_cellsentryfirstnegative. ff_h_pvs_row_scalar_cellsentryfirstnegative + S (dst_negative_row_scalar_cellsentryfirst) = S ((S (a)) * dst_negative_scale_row_scalar_cellsentryfirst)) /\ exists ff_q_pvs_row_scalar_cellsentryfirstnegative. dst_negative_code_row_scalar_cellsentryfirst = ff_q_pvs_row_scalar_cellsentryfirstnegative * S ((S (a)) * dst_negative_scale_row_scalar_cellsentryfirst) + (dst_negative_row_scalar_cellsentryfirst))) /\ (exists ge_balance_positive_row_scalar_cellsentryfirstvalue ge_balance_negative_row_scalar_cellsentryfirstvalue. (((((dfg_first_row_scalar_cellsentry) = 2 * (ge_balance_positive_row_scalar_cellsentryfirstvalue) /\ (ge_balance_negative_row_scalar_cellsentryfirstvalue) = 0) \/ exists ge_signed_half_row_scalar_cellsentryfirstvaluedecode. (((dfg_first_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentryfirstvaluedecode + 1 /\ (ge_balance_positive_row_scalar_cellsentryfirstvalue) = 0) /\ (ge_balance_negative_row_scalar_cellsentryfirstvalue) = S ge_signed_half_row_scalar_cellsentryfirstvaluedecode))) /\ ((dst_positive_row_scalar_cellsentryfirst) + ge_balance_negative_row_scalar_cellsentryfirstvalue = (dst_negative_row_scalar_cellsentryfirst) + ge_balance_positive_row_scalar_cellsentryfirstvalue))))))))) /\ (((exists dst_positive_code_row_scalar_cellsentrylast dst_positive_scale_row_scalar_cellsentrylast dst_negative_code_row_scalar_cellsentrylast dst_negative_scale_row_scalar_cellsentrylast dst_positive_row_scalar_cellsentrylast dst_negative_row_scalar_cellsentrylast. (((H) = (((((dst_positive_code_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast)) * S ((dst_positive_code_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast)) + ((dst_positive_scale_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast))) + (((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) * S ((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) + ((dst_negative_scale_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)))) * S ((((dst_positive_code_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast)) * S ((dst_positive_code_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast)) + ((dst_positive_scale_row_scalar_cellsentrylast) + (dst_positive_scale_row_scalar_cellsentrylast))) + (((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) * S ((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) + ((dst_negative_scale_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)))) + ((((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) * S ((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) + ((dst_negative_scale_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast))) + (((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) * S ((dst_negative_code_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)) + ((dst_negative_scale_row_scalar_cellsentrylast) + (dst_negative_scale_row_scalar_cellsentrylast)))))) /\ (((((exists ff_h_pvs_row_scalar_cellsentrylastpositive. ff_h_pvs_row_scalar_cellsentrylastpositive + S (dst_positive_row_scalar_cellsentrylast) = S ((S (dfg_factor_column_row_scalar_cells)) * dst_positive_scale_row_scalar_cellsentrylast)) /\ exists ff_q_pvs_row_scalar_cellsentrylastpositive. dst_positive_code_row_scalar_cellsentrylast = ff_q_pvs_row_scalar_cellsentrylastpositive * S ((S (dfg_factor_column_row_scalar_cells)) * dst_positive_scale_row_scalar_cellsentrylast) + (dst_positive_row_scalar_cellsentrylast))) /\ (((((exists ff_h_pvs_row_scalar_cellsentrylastnegative. ff_h_pvs_row_scalar_cellsentrylastnegative + S (dst_negative_row_scalar_cellsentrylast) = S ((S (dfg_factor_column_row_scalar_cells)) * dst_negative_scale_row_scalar_cellsentrylast)) /\ exists ff_q_pvs_row_scalar_cellsentrylastnegative. dst_negative_code_row_scalar_cellsentrylast = ff_q_pvs_row_scalar_cellsentrylastnegative * S ((S (dfg_factor_column_row_scalar_cells)) * dst_negative_scale_row_scalar_cellsentrylast) + (dst_negative_row_scalar_cellsentrylast))) /\ (exists ge_balance_positive_row_scalar_cellsentrylastvalue ge_balance_negative_row_scalar_cellsentrylastvalue. (((((dfg_last_row_scalar_cellsentry) = 2 * (ge_balance_positive_row_scalar_cellsentrylastvalue) /\ (ge_balance_negative_row_scalar_cellsentrylastvalue) = 0) \/ exists ge_signed_half_row_scalar_cellsentrylastvaluedecode. (((dfg_last_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentrylastvaluedecode + 1 /\ (ge_balance_positive_row_scalar_cellsentrylastvalue) = 0) /\ (ge_balance_negative_row_scalar_cellsentrylastvalue) = S ge_signed_half_row_scalar_cellsentrylastvaluedecode))) /\ ((dst_positive_row_scalar_cellsentrylast) + ge_balance_negative_row_scalar_cellsentrylastvalue = (dst_negative_row_scalar_cellsentrylast) + ge_balance_positive_row_scalar_cellsentrylastvalue))))))))) /\ (((exists dst_positive_code_row_scalar_cellsentrymiddle dst_positive_scale_row_scalar_cellsentrymiddle dst_negative_code_row_scalar_cellsentrymiddle dst_negative_scale_row_scalar_cellsentrymiddle dst_positive_row_scalar_cellsentrymiddle dst_negative_row_scalar_cellsentrymiddle. (((G) = (((((dst_positive_code_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle)) * S ((dst_positive_code_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle)) + ((dst_positive_scale_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle))) + (((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) * S ((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) + ((dst_negative_scale_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)))) * S ((((dst_positive_code_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle)) * S ((dst_positive_code_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle)) + ((dst_positive_scale_row_scalar_cellsentrymiddle) + (dst_positive_scale_row_scalar_cellsentrymiddle))) + (((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) * S ((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) + ((dst_negative_scale_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)))) + ((((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) * S ((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) + ((dst_negative_scale_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle))) + (((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) * S ((dst_negative_code_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)) + ((dst_negative_scale_row_scalar_cellsentrymiddle) + (dst_negative_scale_row_scalar_cellsentrymiddle)))))) /\ (((((exists ff_h_pvs_row_scalar_cellsentrymiddlepositive. ff_h_pvs_row_scalar_cellsentrymiddlepositive + S (dst_positive_row_scalar_cellsentrymiddle) = S ((S (dfg_middle_row_scalar_cellsentry)) * dst_positive_scale_row_scalar_cellsentrymiddle)) /\ exists ff_q_pvs_row_scalar_cellsentrymiddlepositive. dst_positive_code_row_scalar_cellsentrymiddle = ff_q_pvs_row_scalar_cellsentrymiddlepositive * S ((S (dfg_middle_row_scalar_cellsentry)) * dst_positive_scale_row_scalar_cellsentrymiddle) + (dst_positive_row_scalar_cellsentrymiddle))) /\ (((((exists ff_h_pvs_row_scalar_cellsentrymiddlenegative. ff_h_pvs_row_scalar_cellsentrymiddlenegative + S (dst_negative_row_scalar_cellsentrymiddle) = S ((S (dfg_middle_row_scalar_cellsentry)) * dst_negative_scale_row_scalar_cellsentrymiddle)) /\ exists ff_q_pvs_row_scalar_cellsentrymiddlenegative. dst_negative_code_row_scalar_cellsentrymiddle = ff_q_pvs_row_scalar_cellsentrymiddlenegative * S ((S (dfg_middle_row_scalar_cellsentry)) * dst_negative_scale_row_scalar_cellsentrymiddle) + (dst_negative_row_scalar_cellsentrymiddle))) /\ (exists ge_balance_positive_row_scalar_cellsentrymiddlevalue ge_balance_negative_row_scalar_cellsentrymiddlevalue. (((((dfg_value_row_scalar_cellsentry) = 2 * (ge_balance_positive_row_scalar_cellsentrymiddlevalue) /\ (ge_balance_negative_row_scalar_cellsentrymiddlevalue) = 0) \/ exists ge_signed_half_row_scalar_cellsentrymiddlevaluedecode. (((dfg_value_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentrymiddlevaluedecode + 1 /\ (ge_balance_positive_row_scalar_cellsentrymiddlevalue) = 0) /\ (ge_balance_negative_row_scalar_cellsentrymiddlevalue) = S ge_signed_half_row_scalar_cellsentrymiddlevaluedecode))) /\ ((dst_positive_row_scalar_cellsentrymiddle) + ge_balance_negative_row_scalar_cellsentrymiddlevalue = (dst_negative_row_scalar_cellsentrymiddle) + ge_balance_positive_row_scalar_cellsentrymiddlevalue))))))))) /\ (exists dfg_inner_row_scalar_cellsentryproduct. ((exists sto_ap_row_scalar_cellsentryproductinner sto_an_row_scalar_cellsentryproductinner sto_bp_row_scalar_cellsentryproductinner sto_bn_row_scalar_cellsentryproductinner sto_cp_row_scalar_cellsentryproductinner sto_cn_row_scalar_cellsentryproductinner. (((((dfg_last_row_scalar_cellsentry) = 2 * (sto_ap_row_scalar_cellsentryproductinner) /\ (sto_an_row_scalar_cellsentryproductinner) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductinnerleft. (((dfg_last_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentryproductinnerleft + 1 /\ (sto_ap_row_scalar_cellsentryproductinner) = 0) /\ (sto_an_row_scalar_cellsentryproductinner) = S ge_signed_half_row_scalar_cellsentryproductinnerleft))) /\ ((((((dfg_value_row_scalar_cellsentry) = 2 * (sto_bp_row_scalar_cellsentryproductinner) /\ (sto_bn_row_scalar_cellsentryproductinner) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductinnerright. (((dfg_value_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentryproductinnerright + 1 /\ (sto_bp_row_scalar_cellsentryproductinner) = 0) /\ (sto_bn_row_scalar_cellsentryproductinner) = S ge_signed_half_row_scalar_cellsentryproductinnerright))) /\ ((((((dfg_inner_row_scalar_cellsentryproduct) = 2 * (sto_cp_row_scalar_cellsentryproductinner) /\ (sto_cn_row_scalar_cellsentryproductinner) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductinneroutput. (((dfg_inner_row_scalar_cellsentryproduct) = 2 * ge_signed_half_row_scalar_cellsentryproductinneroutput + 1 /\ (sto_cp_row_scalar_cellsentryproductinner) = 0) /\ (sto_cn_row_scalar_cellsentryproductinner) = S ge_signed_half_row_scalar_cellsentryproductinneroutput))) /\ ((sto_ap_row_scalar_cellsentryproductinner * sto_bp_row_scalar_cellsentryproductinner + sto_an_row_scalar_cellsentryproductinner * sto_bn_row_scalar_cellsentryproductinner) + sto_cn_row_scalar_cellsentryproductinner = (sto_ap_row_scalar_cellsentryproductinner * sto_bn_row_scalar_cellsentryproductinner + sto_an_row_scalar_cellsentryproductinner * sto_bp_row_scalar_cellsentryproductinner) + sto_cp_row_scalar_cellsentryproductinner))))))) /\ (exists sto_ap_row_scalar_cellsentryproductouter sto_an_row_scalar_cellsentryproductouter sto_bp_row_scalar_cellsentryproductouter sto_bn_row_scalar_cellsentryproductouter sto_cp_row_scalar_cellsentryproductouter sto_cn_row_scalar_cellsentryproductouter. (((((dfg_first_row_scalar_cellsentry) = 2 * (sto_ap_row_scalar_cellsentryproductouter) /\ (sto_an_row_scalar_cellsentryproductouter) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductouterleft. (((dfg_first_row_scalar_cellsentry) = 2 * ge_signed_half_row_scalar_cellsentryproductouterleft + 1 /\ (sto_ap_row_scalar_cellsentryproductouter) = 0) /\ (sto_an_row_scalar_cellsentryproductouter) = S ge_signed_half_row_scalar_cellsentryproductouterleft))) /\ ((((((dfg_inner_row_scalar_cellsentryproduct) = 2 * (sto_bp_row_scalar_cellsentryproductouter) /\ (sto_bn_row_scalar_cellsentryproductouter) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductouterright. (((dfg_inner_row_scalar_cellsentryproduct) = 2 * ge_signed_half_row_scalar_cellsentryproductouterright + 1 /\ (sto_bp_row_scalar_cellsentryproductouter) = 0) /\ (sto_bn_row_scalar_cellsentryproductouter) = S ge_signed_half_row_scalar_cellsentryproductouterright))) /\ ((((((dfg_factor_value_row_scalar_cells) = 2 * (sto_cp_row_scalar_cellsentryproductouter) /\ (sto_cn_row_scalar_cellsentryproductouter) = 0) \/ exists ge_signed_half_row_scalar_cellsentryproductouteroutput. (((dfg_factor_value_row_scalar_cells) = 2 * ge_signed_half_row_scalar_cellsentryproductouteroutput + 1 /\ (sto_cp_row_scalar_cellsentryproductouter) = 0) /\ (sto_cn_row_scalar_cellsentryproductouter) = S ge_signed_half_row_scalar_cellsentryproductouteroutput))) /\ ((sto_ap_row_scalar_cellsentryproductouter * sto_bp_row_scalar_cellsentryproductouter + sto_an_row_scalar_cellsentryproductouter * sto_bn_row_scalar_cellsentryproductouter) + sto_cn_row_scalar_cellsentryproductouter = (sto_ap_row_scalar_cellsentryproductouter * sto_bn_row_scalar_cellsentryproductouter + sto_an_row_scalar_cellsentryproductouter * sto_bp_row_scalar_cellsentryproductouter) + sto_cp_row_scalar_cellsentryproductouter))))))))))))))))))))) \/ ((((a)=0 \/ ((dfg_factor_column_row_scalar_cells)=0 \/ ~(exists pvs_factor_row_scalar_cellsentryomittednondivisor. (n) = ((a)*(dfg_factor_column_row_scalar_cells)) * pvs_factor_row_scalar_cellsentryomittednondivisor))) /\ ((dfg_factor_value_row_scalar_cells)=0))))))) -> (((exists dst_positive_code_row_scalar_resultinput_table dst_positive_scale_row_scalar_resultinput_table dst_negative_code_row_scalar_resultinput_table dst_negative_scale_row_scalar_resultinput_table. (((P) = (((((dst_positive_code_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table)) * S ((dst_positive_code_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table)) + ((dst_positive_scale_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table))) + (((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) * S ((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) + ((dst_negative_scale_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)))) * S ((((dst_positive_code_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table)) * S ((dst_positive_code_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table)) + ((dst_positive_scale_row_scalar_resultinput_table) + (dst_positive_scale_row_scalar_resultinput_table))) + (((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) * S ((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) + ((dst_negative_scale_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)))) + ((((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) * S ((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) + ((dst_negative_scale_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table))) + (((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) * S ((dst_negative_code_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)) + ((dst_negative_scale_row_scalar_resultinput_table) + (dst_negative_scale_row_scalar_resultinput_table)))))) /\ (forall dst_index_row_scalar_resultinput_table. (exists pvs_le_gap_row_scalar_resultinput_tabledomain. pvs_le_gap_row_scalar_resultinput_tabledomain + (dst_index_row_scalar_resultinput_table) = (S n)) -> exists dst_positive_row_scalar_resultinput_table dst_negative_row_scalar_resultinput_table dst_value_row_scalar_resultinput_table. ((((exists ff_h_pvs_row_scalar_resultinput_tableentrypositive. ff_h_pvs_row_scalar_resultinput_tableentrypositive + S (dst_positive_row_scalar_resultinput_table) = S ((S (dst_index_row_scalar_resultinput_table)) * dst_positive_scale_row_scalar_resultinput_table)) /\ exists ff_q_pvs_row_scalar_resultinput_tableentrypositive. dst_positive_code_row_scalar_resultinput_table = ff_q_pvs_row_scalar_resultinput_tableentrypositive * S ((S (dst_index_row_scalar_resultinput_table)) * dst_positive_scale_row_scalar_resultinput_table) + (dst_positive_row_scalar_resultinput_table))) /\ (((((exists ff_h_pvs_row_scalar_resultinput_tableentrynegative. ff_h_pvs_row_scalar_resultinput_tableentrynegative + S (dst_negative_row_scalar_resultinput_table) = S ((S (dst_index_row_scalar_resultinput_table)) * dst_negative_scale_row_scalar_resultinput_table)) /\ exists ff_q_pvs_row_scalar_resultinput_tableentrynegative. dst_negative_code_row_scalar_resultinput_table = ff_q_pvs_row_scalar_resultinput_tableentrynegative * S ((S (dst_index_row_scalar_resultinput_table)) * dst_negative_scale_row_scalar_resultinput_table) + (dst_negative_row_scalar_resultinput_table))) /\ (exists ge_balance_positive_row_scalar_resultinput_tableentryvalue ge_balance_negative_row_scalar_resultinput_tableentryvalue. (((((dst_value_row_scalar_resultinput_table) = 2 * (ge_balance_positive_row_scalar_resultinput_tableentryvalue) /\ (ge_balance_negative_row_scalar_resultinput_tableentryvalue) = 0) \/ exists ge_signed_half_row_scalar_resultinput_tableentryvaluedecode. (((dst_value_row_scalar_resultinput_table) = 2 * ge_signed_half_row_scalar_resultinput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_scalar_resultinput_tableentryvalue) = 0) /\ (ge_balance_negative_row_scalar_resultinput_tableentryvalue) = S ge_signed_half_row_scalar_resultinput_tableentryvaluedecode))) /\ ((dst_positive_row_scalar_resultinput_table) + ge_balance_negative_row_scalar_resultinput_tableentryvalue = (dst_negative_row_scalar_resultinput_table) + ge_balance_positive_row_scalar_resultinput_tableentryvalue))))))))) /\ (((exists dst_positive_code_row_scalar_resultoutput_table dst_positive_scale_row_scalar_resultoutput_table dst_negative_code_row_scalar_resultoutput_table dst_negative_scale_row_scalar_resultoutput_table. (((V) = (((((dst_positive_code_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table)) * S ((dst_positive_code_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table)) + ((dst_positive_scale_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table))) + (((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) * S ((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) + ((dst_negative_scale_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)))) * S ((((dst_positive_code_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table)) * S ((dst_positive_code_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table)) + ((dst_positive_scale_row_scalar_resultoutput_table) + (dst_positive_scale_row_scalar_resultoutput_table))) + (((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) * S ((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) + ((dst_negative_scale_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)))) + ((((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) * S ((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) + ((dst_negative_scale_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table))) + (((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) * S ((dst_negative_code_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)) + ((dst_negative_scale_row_scalar_resultoutput_table) + (dst_negative_scale_row_scalar_resultoutput_table)))))) /\ (forall dst_index_row_scalar_resultoutput_table. (exists pvs_le_gap_row_scalar_resultoutput_tabledomain. pvs_le_gap_row_scalar_resultoutput_tabledomain + (dst_index_row_scalar_resultoutput_table) = (S n)) -> exists dst_positive_row_scalar_resultoutput_table dst_negative_row_scalar_resultoutput_table dst_value_row_scalar_resultoutput_table. ((((exists ff_h_pvs_row_scalar_resultoutput_tableentrypositive. ff_h_pvs_row_scalar_resultoutput_tableentrypositive + S (dst_positive_row_scalar_resultoutput_table) = S ((S (dst_index_row_scalar_resultoutput_table)) * dst_positive_scale_row_scalar_resultoutput_table)) /\ exists ff_q_pvs_row_scalar_resultoutput_tableentrypositive. dst_positive_code_row_scalar_resultoutput_table = ff_q_pvs_row_scalar_resultoutput_tableentrypositive * S ((S (dst_index_row_scalar_resultoutput_table)) * dst_positive_scale_row_scalar_resultoutput_table) + (dst_positive_row_scalar_resultoutput_table))) /\ (((((exists ff_h_pvs_row_scalar_resultoutput_tableentrynegative. ff_h_pvs_row_scalar_resultoutput_tableentrynegative + S (dst_negative_row_scalar_resultoutput_table) = S ((S (dst_index_row_scalar_resultoutput_table)) * dst_negative_scale_row_scalar_resultoutput_table)) /\ exists ff_q_pvs_row_scalar_resultoutput_tableentrynegative. dst_negative_code_row_scalar_resultoutput_table = ff_q_pvs_row_scalar_resultoutput_tableentrynegative * S ((S (dst_index_row_scalar_resultoutput_table)) * dst_negative_scale_row_scalar_resultoutput_table) + (dst_negative_row_scalar_resultoutput_table))) /\ (exists ge_balance_positive_row_scalar_resultoutput_tableentryvalue ge_balance_negative_row_scalar_resultoutput_tableentryvalue. (((((dst_value_row_scalar_resultoutput_table) = 2 * (ge_balance_positive_row_scalar_resultoutput_tableentryvalue) /\ (ge_balance_negative_row_scalar_resultoutput_tableentryvalue) = 0) \/ exists ge_signed_half_row_scalar_resultoutput_tableentryvaluedecode. (((dst_value_row_scalar_resultoutput_table) = 2 * ge_signed_half_row_scalar_resultoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_row_scalar_resultoutput_tableentryvalue) = 0) /\ (ge_balance_negative_row_scalar_resultoutput_tableentryvalue) = S ge_signed_half_row_scalar_resultoutput_tableentryvaluedecode))) /\ ((dst_positive_row_scalar_resultoutput_table) + ge_balance_negative_row_scalar_resultoutput_tableentryvalue = (dst_negative_row_scalar_resultoutput_table) + ge_balance_positive_row_scalar_resultoutput_tableentryvalue))))))))) /\ (forall sto_index_row_scalar_resultentries. (exists pvs_gap_row_scalar_resultentriesbound. pvs_gap_row_scalar_resultentriesbound + S (sto_index_row_scalar_resultentries) = (S n)) -> exists sto_input_row_scalar_resultentries sto_output_row_scalar_resultentries. ((exists dst_positive_code_row_scalar_resultentriesentryinput dst_positive_scale_row_scalar_resultentriesentryinput dst_negative_code_row_scalar_resultentriesentryinput dst_negative_scale_row_scalar_resultentriesentryinput dst_positive_row_scalar_resultentriesentryinput dst_negative_row_scalar_resultentriesentryinput. (((P) = (((((dst_positive_code_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput)) * S ((dst_positive_code_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput)) + ((dst_positive_scale_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput))) + (((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) * S ((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) + ((dst_negative_scale_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)))) * S ((((dst_positive_code_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput)) * S ((dst_positive_code_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput)) + ((dst_positive_scale_row_scalar_resultentriesentryinput) + (dst_positive_scale_row_scalar_resultentriesentryinput))) + (((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) * S ((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) + ((dst_negative_scale_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)))) + ((((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) * S ((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) + ((dst_negative_scale_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput))) + (((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) * S ((dst_negative_code_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)) + ((dst_negative_scale_row_scalar_resultentriesentryinput) + (dst_negative_scale_row_scalar_resultentriesentryinput)))))) /\ (((((exists ff_h_pvs_row_scalar_resultentriesentryinputpositive. ff_h_pvs_row_scalar_resultentriesentryinputpositive + S (dst_positive_row_scalar_resultentriesentryinput) = S ((S (sto_index_row_scalar_resultentries)) * dst_positive_scale_row_scalar_resultentriesentryinput)) /\ exists ff_q_pvs_row_scalar_resultentriesentryinputpositive. dst_positive_code_row_scalar_resultentriesentryinput = ff_q_pvs_row_scalar_resultentriesentryinputpositive * S ((S (sto_index_row_scalar_resultentries)) * dst_positive_scale_row_scalar_resultentriesentryinput) + (dst_positive_row_scalar_resultentriesentryinput))) /\ (((((exists ff_h_pvs_row_scalar_resultentriesentryinputnegative. ff_h_pvs_row_scalar_resultentriesentryinputnegative + S (dst_negative_row_scalar_resultentriesentryinput) = S ((S (sto_index_row_scalar_resultentries)) * dst_negative_scale_row_scalar_resultentriesentryinput)) /\ exists ff_q_pvs_row_scalar_resultentriesentryinputnegative. dst_negative_code_row_scalar_resultentriesentryinput = ff_q_pvs_row_scalar_resultentriesentryinputnegative * S ((S (sto_index_row_scalar_resultentries)) * dst_negative_scale_row_scalar_resultentriesentryinput) + (dst_negative_row_scalar_resultentriesentryinput))) /\ (exists ge_balance_positive_row_scalar_resultentriesentryinputvalue ge_balance_negative_row_scalar_resultentriesentryinputvalue. (((((sto_input_row_scalar_resultentries) = 2 * (ge_balance_positive_row_scalar_resultentriesentryinputvalue) /\ (ge_balance_negative_row_scalar_resultentriesentryinputvalue) = 0) \/ exists ge_signed_half_row_scalar_resultentriesentryinputvaluedecode. (((sto_input_row_scalar_resultentries) = 2 * ge_signed_half_row_scalar_resultentriesentryinputvaluedecode + 1 /\ (ge_balance_positive_row_scalar_resultentriesentryinputvalue) = 0) /\ (ge_balance_negative_row_scalar_resultentriesentryinputvalue) = S ge_signed_half_row_scalar_resultentriesentryinputvaluedecode))) /\ ((dst_positive_row_scalar_resultentriesentryinput) + ge_balance_negative_row_scalar_resultentriesentryinputvalue = (dst_negative_row_scalar_resultentriesentryinput) + ge_balance_positive_row_scalar_resultentriesentryinputvalue))))))))) /\ (((exists dst_positive_code_row_scalar_resultentriesentryoutput dst_positive_scale_row_scalar_resultentriesentryoutput dst_negative_code_row_scalar_resultentriesentryoutput dst_negative_scale_row_scalar_resultentriesentryoutput dst_positive_row_scalar_resultentriesentryoutput dst_negative_row_scalar_resultentriesentryoutput. (((V) = (((((dst_positive_code_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput)) * S ((dst_positive_code_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput)) + ((dst_positive_scale_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput))) + (((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) * S ((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) + ((dst_negative_scale_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)))) * S ((((dst_positive_code_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput)) * S ((dst_positive_code_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput)) + ((dst_positive_scale_row_scalar_resultentriesentryoutput) + (dst_positive_scale_row_scalar_resultentriesentryoutput))) + (((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) * S ((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) + ((dst_negative_scale_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)))) + ((((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) * S ((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) + ((dst_negative_scale_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput))) + (((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) * S ((dst_negative_code_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)) + ((dst_negative_scale_row_scalar_resultentriesentryoutput) + (dst_negative_scale_row_scalar_resultentriesentryoutput)))))) /\ (((((exists ff_h_pvs_row_scalar_resultentriesentryoutputpositive. ff_h_pvs_row_scalar_resultentriesentryoutputpositive + S (dst_positive_row_scalar_resultentriesentryoutput) = S ((S (sto_index_row_scalar_resultentries)) * dst_positive_scale_row_scalar_resultentriesentryoutput)) /\ exists ff_q_pvs_row_scalar_resultentriesentryoutputpositive. dst_positive_code_row_scalar_resultentriesentryoutput = ff_q_pvs_row_scalar_resultentriesentryoutputpositive * S ((S (sto_index_row_scalar_resultentries)) * dst_positive_scale_row_scalar_resultentriesentryoutput) + (dst_positive_row_scalar_resultentriesentryoutput))) /\ (((((exists ff_h_pvs_row_scalar_resultentriesentryoutputnegative. ff_h_pvs_row_scalar_resultentriesentryoutputnegative + S (dst_negative_row_scalar_resultentriesentryoutput) = S ((S (sto_index_row_scalar_resultentries)) * dst_negative_scale_row_scalar_resultentriesentryoutput)) /\ exists ff_q_pvs_row_scalar_resultentriesentryoutputnegative. dst_negative_code_row_scalar_resultentriesentryoutput = ff_q_pvs_row_scalar_resultentriesentryoutputnegative * S ((S (sto_index_row_scalar_resultentries)) * dst_negative_scale_row_scalar_resultentriesentryoutput) + (dst_negative_row_scalar_resultentriesentryoutput))) /\ (exists ge_balance_positive_row_scalar_resultentriesentryoutputvalue ge_balance_negative_row_scalar_resultentriesentryoutputvalue. (((((sto_output_row_scalar_resultentries) = 2 * (ge_balance_positive_row_scalar_resultentriesentryoutputvalue) /\ (ge_balance_negative_row_scalar_resultentriesentryoutputvalue) = 0) \/ exists ge_signed_half_row_scalar_resultentriesentryoutputvaluedecode. (((sto_output_row_scalar_resultentries) = 2 * ge_signed_half_row_scalar_resultentriesentryoutputvaluedecode + 1 /\ (ge_balance_positive_row_scalar_resultentriesentryoutputvalue) = 0) /\ (ge_balance_negative_row_scalar_resultentriesentryoutputvalue) = S ge_signed_half_row_scalar_resultentriesentryoutputvaluedecode))) /\ ((dst_positive_row_scalar_resultentriesentryoutput) + ge_balance_negative_row_scalar_resultentriesentryoutputvalue = (dst_negative_row_scalar_resultentriesentryoutput) + ge_balance_positive_row_scalar_resultentriesentryoutputvalue))))))))) /\ (exists sto_ap_row_scalar_resultentriesentryoperation sto_an_row_scalar_resultentriesentryoperation sto_bp_row_scalar_resultentriesentryoperation sto_bn_row_scalar_resultentriesentryoperation sto_cp_row_scalar_resultentriesentryoperation sto_cn_row_scalar_resultentriesentryoperation. (((((u) = 2 * (sto_ap_row_scalar_resultentriesentryoperation) /\ (sto_an_row_scalar_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_scalar_resultentriesentryoperationleft. (((u) = 2 * ge_signed_half_row_scalar_resultentriesentryoperationleft + 1 /\ (sto_ap_row_scalar_resultentriesentryoperation) = 0) /\ (sto_an_row_scalar_resultentriesentryoperation) = S ge_signed_half_row_scalar_resultentriesentryoperationleft))) /\ ((((((sto_input_row_scalar_resultentries) = 2 * (sto_bp_row_scalar_resultentriesentryoperation) /\ (sto_bn_row_scalar_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_scalar_resultentriesentryoperationright. (((sto_input_row_scalar_resultentries) = 2 * ge_signed_half_row_scalar_resultentriesentryoperationright + 1 /\ (sto_bp_row_scalar_resultentriesentryoperation) = 0) /\ (sto_bn_row_scalar_resultentriesentryoperation) = S ge_signed_half_row_scalar_resultentriesentryoperationright))) /\ ((((((sto_output_row_scalar_resultentries) = 2 * (sto_cp_row_scalar_resultentriesentryoperation) /\ (sto_cn_row_scalar_resultentriesentryoperation) = 0) \/ exists ge_signed_half_row_scalar_resultentriesentryoperationoutput. (((sto_output_row_scalar_resultentries) = 2 * ge_signed_half_row_scalar_resultentriesentryoperationoutput + 1 /\ (sto_cp_row_scalar_resultentriesentryoperation) = 0) /\ (sto_cn_row_scalar_resultentriesentryoperation) = S ge_signed_half_row_scalar_resultentriesentryoperationoutput))) /\ ((sto_ap_row_scalar_resultentriesentryoperation * sto_bp_row_scalar_resultentriesentryoperation + sto_an_row_scalar_resultentriesentryoperation * sto_bn_row_scalar_resultentriesentryoperation) + sto_cn_row_scalar_resultentriesentryoperation = (sto_ap_row_scalar_resultentriesentryoperation * sto_bn_row_scalar_resultentriesentryoperation + sto_an_row_scalar_resultentriesentryoperation * sto_bp_row_scalar_resultentriesentryoperation) + sto_cp_row_scalar_resultentriesentryoperation)))))))))))))))