dirichlet_convolution_from_padded_prefix

Exact expanded first-order arithmetic statement

forall F G n L M z. ~(n=0) -> (exists pvs_le_gap_padded_bound. pvs_le_gap_padded_bound + (n) = (L)) -> (((exists dst_positive_code_padded_prefixtable dst_positive_scale_padded_prefixtable dst_negative_code_padded_prefixtable dst_negative_scale_padded_prefixtable. (((M) = (((((dst_positive_code_padded_prefixtable) + (dst_positive_scale_padded_prefixtable)) * S ((dst_positive_code_padded_prefixtable) + (dst_positive_scale_padded_prefixtable)) + ((dst_positive_scale_padded_prefixtable) + (dst_positive_scale_padded_prefixtable))) + (((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) * S ((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) + ((dst_negative_scale_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)))) * S ((((dst_positive_code_padded_prefixtable) + (dst_positive_scale_padded_prefixtable)) * S ((dst_positive_code_padded_prefixtable) + (dst_positive_scale_padded_prefixtable)) + ((dst_positive_scale_padded_prefixtable) + (dst_positive_scale_padded_prefixtable))) + (((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) * S ((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) + ((dst_negative_scale_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)))) + ((((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) * S ((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) + ((dst_negative_scale_padded_prefixtable) + (dst_negative_scale_padded_prefixtable))) + (((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) * S ((dst_negative_code_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)) + ((dst_negative_scale_padded_prefixtable) + (dst_negative_scale_padded_prefixtable)))))) /\ (forall dst_index_padded_prefixtable. (exists pvs_le_gap_padded_prefixtabledomain. pvs_le_gap_padded_prefixtabledomain + (dst_index_padded_prefixtable) = (L)) -> exists dst_positive_padded_prefixtable dst_negative_padded_prefixtable dst_value_padded_prefixtable. ((((exists ff_h_pvs_padded_prefixtableentrypositive. ff_h_pvs_padded_prefixtableentrypositive + S (dst_positive_padded_prefixtable) = S ((S (dst_index_padded_prefixtable)) * dst_positive_scale_padded_prefixtable)) /\ exists ff_q_pvs_padded_prefixtableentrypositive. dst_positive_code_padded_prefixtable = ff_q_pvs_padded_prefixtableentrypositive * S ((S (dst_index_padded_prefixtable)) * dst_positive_scale_padded_prefixtable) + (dst_positive_padded_prefixtable))) /\ (((((exists ff_h_pvs_padded_prefixtableentrynegative. ff_h_pvs_padded_prefixtableentrynegative + S (dst_negative_padded_prefixtable) = S ((S (dst_index_padded_prefixtable)) * dst_negative_scale_padded_prefixtable)) /\ exists ff_q_pvs_padded_prefixtableentrynegative. dst_negative_code_padded_prefixtable = ff_q_pvs_padded_prefixtableentrynegative * S ((S (dst_index_padded_prefixtable)) * dst_negative_scale_padded_prefixtable) + (dst_negative_padded_prefixtable))) /\ (exists ge_balance_positive_padded_prefixtableentryvalue ge_balance_negative_padded_prefixtableentryvalue. (((((dst_value_padded_prefixtable) = 2 * (ge_balance_positive_padded_prefixtableentryvalue) /\ (ge_balance_negative_padded_prefixtableentryvalue) = 0) \/ exists ge_signed_half_padded_prefixtableentryvaluedecode. (((dst_value_padded_prefixtable) = 2 * ge_signed_half_padded_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_padded_prefixtableentryvalue) = 0) /\ (ge_balance_negative_padded_prefixtableentryvalue) = S ge_signed_half_padded_prefixtableentryvaluedecode))) /\ ((dst_positive_padded_prefixtable) + ge_balance_negative_padded_prefixtableentryvalue = (dst_negative_padded_prefixtable) + ge_balance_positive_padded_prefixtableentryvalue))))))))) /\ (forall dc_index_padded_prefix dc_value_padded_prefix. (exists pvs_le_gap_padded_prefixdomain. pvs_le_gap_padded_prefixdomain + (dc_index_padded_prefix) = (L)) -> (exists dst_positive_code_padded_prefixlookup dst_positive_scale_padded_prefixlookup dst_negative_code_padded_prefixlookup dst_negative_scale_padded_prefixlookup dst_positive_padded_prefixlookup dst_negative_padded_prefixlookup. (((M) = (((((dst_positive_code_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup)) * S ((dst_positive_code_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup)) + ((dst_positive_scale_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup))) + (((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) * S ((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) + ((dst_negative_scale_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)))) * S ((((dst_positive_code_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup)) * S ((dst_positive_code_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup)) + ((dst_positive_scale_padded_prefixlookup) + (dst_positive_scale_padded_prefixlookup))) + (((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) * S ((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) + ((dst_negative_scale_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)))) + ((((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) * S ((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) + ((dst_negative_scale_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup))) + (((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) * S ((dst_negative_code_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)) + ((dst_negative_scale_padded_prefixlookup) + (dst_negative_scale_padded_prefixlookup)))))) /\ (((((exists ff_h_pvs_padded_prefixlookuppositive. ff_h_pvs_padded_prefixlookuppositive + S (dst_positive_padded_prefixlookup) = S ((S (dc_index_padded_prefix)) * dst_positive_scale_padded_prefixlookup)) /\ exists ff_q_pvs_padded_prefixlookuppositive. dst_positive_code_padded_prefixlookup = ff_q_pvs_padded_prefixlookuppositive * S ((S (dc_index_padded_prefix)) * dst_positive_scale_padded_prefixlookup) + (dst_positive_padded_prefixlookup))) /\ (((((exists ff_h_pvs_padded_prefixlookupnegative. ff_h_pvs_padded_prefixlookupnegative + S (dst_negative_padded_prefixlookup) = S ((S (dc_index_padded_prefix)) * dst_negative_scale_padded_prefixlookup)) /\ exists ff_q_pvs_padded_prefixlookupnegative. dst_negative_code_padded_prefixlookup = ff_q_pvs_padded_prefixlookupnegative * S ((S (dc_index_padded_prefix)) * dst_negative_scale_padded_prefixlookup) + (dst_negative_padded_prefixlookup))) /\ (exists ge_balance_positive_padded_prefixlookupvalue ge_balance_negative_padded_prefixlookupvalue. (((((dc_value_padded_prefix) = 2 * (ge_balance_positive_padded_prefixlookupvalue) /\ (ge_balance_negative_padded_prefixlookupvalue) = 0) \/ exists ge_signed_half_padded_prefixlookupvaluedecode. (((dc_value_padded_prefix) = 2 * ge_signed_half_padded_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_padded_prefixlookupvalue) = 0) /\ (ge_balance_negative_padded_prefixlookupvalue) = S ge_signed_half_padded_prefixlookupvaluedecode))) /\ ((dst_positive_padded_prefixlookup) + ge_balance_negative_padded_prefixlookupvalue = (dst_negative_padded_prefixlookup) + ge_balance_positive_padded_prefixlookupvalue))))))))) -> ((((~((dc_index_padded_prefix)=0)) /\ (exists dc_quotient_padded_prefixentry dc_left_padded_prefixentry dc_right_padded_prefixentry. (((n)=(dc_index_padded_prefix)*dc_quotient_padded_prefixentry) /\ (((exists dst_positive_code_padded_prefixentryleft dst_positive_scale_padded_prefixentryleft dst_negative_code_padded_prefixentryleft dst_negative_scale_padded_prefixentryleft dst_positive_padded_prefixentryleft dst_negative_padded_prefixentryleft. (((F) = (((((dst_positive_code_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft)) * S ((dst_positive_code_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft)) + ((dst_positive_scale_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft))) + (((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) * S ((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) + ((dst_negative_scale_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)))) * S ((((dst_positive_code_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft)) * S ((dst_positive_code_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft)) + ((dst_positive_scale_padded_prefixentryleft) + (dst_positive_scale_padded_prefixentryleft))) + (((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) * S ((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) + ((dst_negative_scale_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)))) + ((((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) * S ((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) + ((dst_negative_scale_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft))) + (((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) * S ((dst_negative_code_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)) + ((dst_negative_scale_padded_prefixentryleft) + (dst_negative_scale_padded_prefixentryleft)))))) /\ (((((exists ff_h_pvs_padded_prefixentryleftpositive. ff_h_pvs_padded_prefixentryleftpositive + S (dst_positive_padded_prefixentryleft) = S ((S (dc_index_padded_prefix)) * dst_positive_scale_padded_prefixentryleft)) /\ exists ff_q_pvs_padded_prefixentryleftpositive. dst_positive_code_padded_prefixentryleft = ff_q_pvs_padded_prefixentryleftpositive * S ((S (dc_index_padded_prefix)) * dst_positive_scale_padded_prefixentryleft) + (dst_positive_padded_prefixentryleft))) /\ (((((exists ff_h_pvs_padded_prefixentryleftnegative. ff_h_pvs_padded_prefixentryleftnegative + S (dst_negative_padded_prefixentryleft) = S ((S (dc_index_padded_prefix)) * dst_negative_scale_padded_prefixentryleft)) /\ exists ff_q_pvs_padded_prefixentryleftnegative. dst_negative_code_padded_prefixentryleft = ff_q_pvs_padded_prefixentryleftnegative * S ((S (dc_index_padded_prefix)) * dst_negative_scale_padded_prefixentryleft) + (dst_negative_padded_prefixentryleft))) /\ (exists ge_balance_positive_padded_prefixentryleftvalue ge_balance_negative_padded_prefixentryleftvalue. (((((dc_left_padded_prefixentry) = 2 * (ge_balance_positive_padded_prefixentryleftvalue) /\ (ge_balance_negative_padded_prefixentryleftvalue) = 0) \/ exists ge_signed_half_padded_prefixentryleftvaluedecode. (((dc_left_padded_prefixentry) = 2 * ge_signed_half_padded_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_padded_prefixentryleftvalue) = 0) /\ (ge_balance_negative_padded_prefixentryleftvalue) = S ge_signed_half_padded_prefixentryleftvaluedecode))) /\ ((dst_positive_padded_prefixentryleft) + ge_balance_negative_padded_prefixentryleftvalue = (dst_negative_padded_prefixentryleft) + ge_balance_positive_padded_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_padded_prefixentryright dst_positive_scale_padded_prefixentryright dst_negative_code_padded_prefixentryright dst_negative_scale_padded_prefixentryright dst_positive_padded_prefixentryright dst_negative_padded_prefixentryright. (((G) = (((((dst_positive_code_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright)) * S ((dst_positive_code_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright)) + ((dst_positive_scale_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright))) + (((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) * S ((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) + ((dst_negative_scale_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)))) * S ((((dst_positive_code_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright)) * S ((dst_positive_code_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright)) + ((dst_positive_scale_padded_prefixentryright) + (dst_positive_scale_padded_prefixentryright))) + (((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) * S ((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) + ((dst_negative_scale_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)))) + ((((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) * S ((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) + ((dst_negative_scale_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright))) + (((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) * S ((dst_negative_code_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)) + ((dst_negative_scale_padded_prefixentryright) + (dst_negative_scale_padded_prefixentryright)))))) /\ (((((exists ff_h_pvs_padded_prefixentryrightpositive. ff_h_pvs_padded_prefixentryrightpositive + S (dst_positive_padded_prefixentryright) = S ((S (dc_quotient_padded_prefixentry)) * dst_positive_scale_padded_prefixentryright)) /\ exists ff_q_pvs_padded_prefixentryrightpositive. dst_positive_code_padded_prefixentryright = ff_q_pvs_padded_prefixentryrightpositive * S ((S (dc_quotient_padded_prefixentry)) * dst_positive_scale_padded_prefixentryright) + (dst_positive_padded_prefixentryright))) /\ (((((exists ff_h_pvs_padded_prefixentryrightnegative. ff_h_pvs_padded_prefixentryrightnegative + S (dst_negative_padded_prefixentryright) = S ((S (dc_quotient_padded_prefixentry)) * dst_negative_scale_padded_prefixentryright)) /\ exists ff_q_pvs_padded_prefixentryrightnegative. dst_negative_code_padded_prefixentryright = ff_q_pvs_padded_prefixentryrightnegative * S ((S (dc_quotient_padded_prefixentry)) * dst_negative_scale_padded_prefixentryright) + (dst_negative_padded_prefixentryright))) /\ (exists ge_balance_positive_padded_prefixentryrightvalue ge_balance_negative_padded_prefixentryrightvalue. (((((dc_right_padded_prefixentry) = 2 * (ge_balance_positive_padded_prefixentryrightvalue) /\ (ge_balance_negative_padded_prefixentryrightvalue) = 0) \/ exists ge_signed_half_padded_prefixentryrightvaluedecode. (((dc_right_padded_prefixentry) = 2 * ge_signed_half_padded_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_padded_prefixentryrightvalue) = 0) /\ (ge_balance_negative_padded_prefixentryrightvalue) = S ge_signed_half_padded_prefixentryrightvaluedecode))) /\ ((dst_positive_padded_prefixentryright) + ge_balance_negative_padded_prefixentryrightvalue = (dst_negative_padded_prefixentryright) + ge_balance_positive_padded_prefixentryrightvalue))))))))) /\ (exists sto_ap_padded_prefixentryproduct sto_an_padded_prefixentryproduct sto_bp_padded_prefixentryproduct sto_bn_padded_prefixentryproduct sto_cp_padded_prefixentryproduct sto_cn_padded_prefixentryproduct. (((((dc_left_padded_prefixentry) = 2 * (sto_ap_padded_prefixentryproduct) /\ (sto_an_padded_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_prefixentryproductleft. (((dc_left_padded_prefixentry) = 2 * ge_signed_half_padded_prefixentryproductleft + 1 /\ (sto_ap_padded_prefixentryproduct) = 0) /\ (sto_an_padded_prefixentryproduct) = S ge_signed_half_padded_prefixentryproductleft))) /\ ((((((dc_right_padded_prefixentry) = 2 * (sto_bp_padded_prefixentryproduct) /\ (sto_bn_padded_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_prefixentryproductright. (((dc_right_padded_prefixentry) = 2 * ge_signed_half_padded_prefixentryproductright + 1 /\ (sto_bp_padded_prefixentryproduct) = 0) /\ (sto_bn_padded_prefixentryproduct) = S ge_signed_half_padded_prefixentryproductright))) /\ ((((((dc_value_padded_prefix) = 2 * (sto_cp_padded_prefixentryproduct) /\ (sto_cn_padded_prefixentryproduct) = 0) \/ exists ge_signed_half_padded_prefixentryproductoutput. (((dc_value_padded_prefix) = 2 * ge_signed_half_padded_prefixentryproductoutput + 1 /\ (sto_cp_padded_prefixentryproduct) = 0) /\ (sto_cn_padded_prefixentryproduct) = S ge_signed_half_padded_prefixentryproductoutput))) /\ ((sto_ap_padded_prefixentryproduct * sto_bp_padded_prefixentryproduct + sto_an_padded_prefixentryproduct * sto_bn_padded_prefixentryproduct) + sto_cn_padded_prefixentryproduct = (sto_ap_padded_prefixentryproduct * sto_bn_padded_prefixentryproduct + sto_an_padded_prefixentryproduct * sto_bp_padded_prefixentryproduct) + sto_cp_padded_prefixentryproduct))))))))))))))) \/ ((((dc_index_padded_prefix)=0 \/ ~(exists pvs_factor_padded_prefixentrynondivisor. (n) = (dc_index_padded_prefix) * pvs_factor_padded_prefixentrynondivisor)) /\ ((dc_value_padded_prefix)=0))))))) -> (exists dst_positive_code_padded_sum dst_positive_scale_padded_sum dst_negative_code_padded_sum dst_negative_scale_padded_sum dst_positive_sum_padded_sum dst_negative_sum_padded_sum. (((M) = (((((dst_positive_code_padded_sum) + (dst_positive_scale_padded_sum)) * S ((dst_positive_code_padded_sum) + (dst_positive_scale_padded_sum)) + ((dst_positive_scale_padded_sum) + (dst_positive_scale_padded_sum))) + (((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) * S ((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) + ((dst_negative_scale_padded_sum) + (dst_negative_scale_padded_sum)))) * S ((((dst_positive_code_padded_sum) + (dst_positive_scale_padded_sum)) * S ((dst_positive_code_padded_sum) + (dst_positive_scale_padded_sum)) + ((dst_positive_scale_padded_sum) + (dst_positive_scale_padded_sum))) + (((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) * S ((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) + ((dst_negative_scale_padded_sum) + (dst_negative_scale_padded_sum)))) + ((((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) * S ((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) + ((dst_negative_scale_padded_sum) + (dst_negative_scale_padded_sum))) + (((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) * S ((dst_negative_code_padded_sum) + (dst_negative_scale_padded_sum)) + ((dst_negative_scale_padded_sum) + (dst_negative_scale_padded_sum)))))) /\ (((exists fs_u_dst_padded_sumpositive fs_v_dst_padded_sumpositive. ((((exists fs_h_dst_padded_sumpositive_body_start. fs_h_dst_padded_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_sumpositive)) /\ exists fs_q_dst_padded_sumpositive_body_start. fs_u_dst_padded_sumpositive = fs_q_dst_padded_sumpositive_body_start * S ((S (0)) * fs_v_dst_padded_sumpositive) + (0))) /\ ((((exists fs_h_dst_padded_sumpositive_body_terminal. fs_h_dst_padded_sumpositive_body_terminal + S (dst_positive_sum_padded_sum) = S ((S (S L)) * fs_v_dst_padded_sumpositive)) /\ exists fs_q_dst_padded_sumpositive_body_terminal. fs_u_dst_padded_sumpositive = fs_q_dst_padded_sumpositive_body_terminal * S ((S (S L)) * fs_v_dst_padded_sumpositive) + (dst_positive_sum_padded_sum))) /\ forall fs_i_dst_padded_sumpositive_body_steps. (exists fs_lt_dst_padded_sumpositive_body_steps_bound. fs_lt_dst_padded_sumpositive_body_steps_bound + S fs_i_dst_padded_sumpositive_body_steps = S L) -> exists fs_a_dst_padded_sumpositive_body_steps fs_r_dst_padded_sumpositive_body_steps fs_s_dst_padded_sumpositive_body_steps. ((((exists fs_h_dst_padded_sumpositive_body_steps_summand. fs_h_dst_padded_sumpositive_body_steps_summand + S (fs_a_dst_padded_sumpositive_body_steps) = S ((S (fs_i_dst_padded_sumpositive_body_steps)) * dst_positive_scale_padded_sum)) /\ exists fs_q_dst_padded_sumpositive_body_steps_summand. dst_positive_code_padded_sum = fs_q_dst_padded_sumpositive_body_steps_summand * S ((S (fs_i_dst_padded_sumpositive_body_steps)) * dst_positive_scale_padded_sum) + (fs_a_dst_padded_sumpositive_body_steps))) /\ ((((exists fs_h_dst_padded_sumpositive_body_steps_partial. fs_h_dst_padded_sumpositive_body_steps_partial + S (fs_r_dst_padded_sumpositive_body_steps) = S ((S (fs_i_dst_padded_sumpositive_body_steps)) * fs_v_dst_padded_sumpositive)) /\ exists fs_q_dst_padded_sumpositive_body_steps_partial. fs_u_dst_padded_sumpositive = fs_q_dst_padded_sumpositive_body_steps_partial * S ((S (fs_i_dst_padded_sumpositive_body_steps)) * fs_v_dst_padded_sumpositive) + (fs_r_dst_padded_sumpositive_body_steps))) /\ ((((exists fs_h_dst_padded_sumpositive_body_steps_successor. fs_h_dst_padded_sumpositive_body_steps_successor + S (fs_s_dst_padded_sumpositive_body_steps) = S ((S (S fs_i_dst_padded_sumpositive_body_steps)) * fs_v_dst_padded_sumpositive)) /\ exists fs_q_dst_padded_sumpositive_body_steps_successor. fs_u_dst_padded_sumpositive = fs_q_dst_padded_sumpositive_body_steps_successor * S ((S (S fs_i_dst_padded_sumpositive_body_steps)) * fs_v_dst_padded_sumpositive) + (fs_s_dst_padded_sumpositive_body_steps))) /\ fs_s_dst_padded_sumpositive_body_steps = fs_r_dst_padded_sumpositive_body_steps + fs_a_dst_padded_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_sumnegative fs_v_dst_padded_sumnegative. ((((exists fs_h_dst_padded_sumnegative_body_start. fs_h_dst_padded_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_sumnegative)) /\ exists fs_q_dst_padded_sumnegative_body_start. fs_u_dst_padded_sumnegative = fs_q_dst_padded_sumnegative_body_start * S ((S (0)) * fs_v_dst_padded_sumnegative) + (0))) /\ ((((exists fs_h_dst_padded_sumnegative_body_terminal. fs_h_dst_padded_sumnegative_body_terminal + S (dst_negative_sum_padded_sum) = S ((S (S L)) * fs_v_dst_padded_sumnegative)) /\ exists fs_q_dst_padded_sumnegative_body_terminal. fs_u_dst_padded_sumnegative = fs_q_dst_padded_sumnegative_body_terminal * S ((S (S L)) * fs_v_dst_padded_sumnegative) + (dst_negative_sum_padded_sum))) /\ forall fs_i_dst_padded_sumnegative_body_steps. (exists fs_lt_dst_padded_sumnegative_body_steps_bound. fs_lt_dst_padded_sumnegative_body_steps_bound + S fs_i_dst_padded_sumnegative_body_steps = S L) -> exists fs_a_dst_padded_sumnegative_body_steps fs_r_dst_padded_sumnegative_body_steps fs_s_dst_padded_sumnegative_body_steps. ((((exists fs_h_dst_padded_sumnegative_body_steps_summand. fs_h_dst_padded_sumnegative_body_steps_summand + S (fs_a_dst_padded_sumnegative_body_steps) = S ((S (fs_i_dst_padded_sumnegative_body_steps)) * dst_negative_scale_padded_sum)) /\ exists fs_q_dst_padded_sumnegative_body_steps_summand. dst_negative_code_padded_sum = fs_q_dst_padded_sumnegative_body_steps_summand * S ((S (fs_i_dst_padded_sumnegative_body_steps)) * dst_negative_scale_padded_sum) + (fs_a_dst_padded_sumnegative_body_steps))) /\ ((((exists fs_h_dst_padded_sumnegative_body_steps_partial. fs_h_dst_padded_sumnegative_body_steps_partial + S (fs_r_dst_padded_sumnegative_body_steps) = S ((S (fs_i_dst_padded_sumnegative_body_steps)) * fs_v_dst_padded_sumnegative)) /\ exists fs_q_dst_padded_sumnegative_body_steps_partial. fs_u_dst_padded_sumnegative = fs_q_dst_padded_sumnegative_body_steps_partial * S ((S (fs_i_dst_padded_sumnegative_body_steps)) * fs_v_dst_padded_sumnegative) + (fs_r_dst_padded_sumnegative_body_steps))) /\ ((((exists fs_h_dst_padded_sumnegative_body_steps_successor. fs_h_dst_padded_sumnegative_body_steps_successor + S (fs_s_dst_padded_sumnegative_body_steps) = S ((S (S fs_i_dst_padded_sumnegative_body_steps)) * fs_v_dst_padded_sumnegative)) /\ exists fs_q_dst_padded_sumnegative_body_steps_successor. fs_u_dst_padded_sumnegative = fs_q_dst_padded_sumnegative_body_steps_successor * S ((S (S fs_i_dst_padded_sumnegative_body_steps)) * fs_v_dst_padded_sumnegative) + (fs_s_dst_padded_sumnegative_body_steps))) /\ fs_s_dst_padded_sumnegative_body_steps = fs_r_dst_padded_sumnegative_body_steps + fs_a_dst_padded_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_sumresult ge_balance_negative_padded_sumresult. (((((z) = 2 * (ge_balance_positive_padded_sumresult) /\ (ge_balance_negative_padded_sumresult) = 0) \/ exists ge_signed_half_padded_sumresultdecode. (((z) = 2 * ge_signed_half_padded_sumresultdecode + 1 /\ (ge_balance_positive_padded_sumresult) = 0) /\ (ge_balance_negative_padded_sumresult) = S ge_signed_half_padded_sumresultdecode))) /\ ((dst_positive_sum_padded_sum) + ge_balance_negative_padded_sumresult = (dst_negative_sum_padded_sum) + ge_balance_positive_padded_sumresult))))))))) -> (((~((n)=0)) /\ (exists dc_mask_padded_result. ((((exists dst_positive_code_padded_resultmasktable dst_positive_scale_padded_resultmasktable dst_negative_code_padded_resultmasktable dst_negative_scale_padded_resultmasktable. (((dc_mask_padded_result) = (((((dst_positive_code_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable)) * S ((dst_positive_code_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable)) + ((dst_positive_scale_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable))) + (((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) * S ((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) + ((dst_negative_scale_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)))) * S ((((dst_positive_code_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable)) * S ((dst_positive_code_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable)) + ((dst_positive_scale_padded_resultmasktable) + (dst_positive_scale_padded_resultmasktable))) + (((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) * S ((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) + ((dst_negative_scale_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)))) + ((((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) * S ((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) + ((dst_negative_scale_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable))) + (((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) * S ((dst_negative_code_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)) + ((dst_negative_scale_padded_resultmasktable) + (dst_negative_scale_padded_resultmasktable)))))) /\ (forall dst_index_padded_resultmasktable. (exists pvs_le_gap_padded_resultmasktabledomain. pvs_le_gap_padded_resultmasktabledomain + (dst_index_padded_resultmasktable) = (n)) -> exists dst_positive_padded_resultmasktable dst_negative_padded_resultmasktable dst_value_padded_resultmasktable. ((((exists ff_h_pvs_padded_resultmasktableentrypositive. ff_h_pvs_padded_resultmasktableentrypositive + S (dst_positive_padded_resultmasktable) = S ((S (dst_index_padded_resultmasktable)) * dst_positive_scale_padded_resultmasktable)) /\ exists ff_q_pvs_padded_resultmasktableentrypositive. dst_positive_code_padded_resultmasktable = ff_q_pvs_padded_resultmasktableentrypositive * S ((S (dst_index_padded_resultmasktable)) * dst_positive_scale_padded_resultmasktable) + (dst_positive_padded_resultmasktable))) /\ (((((exists ff_h_pvs_padded_resultmasktableentrynegative. ff_h_pvs_padded_resultmasktableentrynegative + S (dst_negative_padded_resultmasktable) = S ((S (dst_index_padded_resultmasktable)) * dst_negative_scale_padded_resultmasktable)) /\ exists ff_q_pvs_padded_resultmasktableentrynegative. dst_negative_code_padded_resultmasktable = ff_q_pvs_padded_resultmasktableentrynegative * S ((S (dst_index_padded_resultmasktable)) * dst_negative_scale_padded_resultmasktable) + (dst_negative_padded_resultmasktable))) /\ (exists ge_balance_positive_padded_resultmasktableentryvalue ge_balance_negative_padded_resultmasktableentryvalue. (((((dst_value_padded_resultmasktable) = 2 * (ge_balance_positive_padded_resultmasktableentryvalue) /\ (ge_balance_negative_padded_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_padded_resultmasktableentryvaluedecode. (((dst_value_padded_resultmasktable) = 2 * ge_signed_half_padded_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_padded_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_padded_resultmasktableentryvalue) = S ge_signed_half_padded_resultmasktableentryvaluedecode))) /\ ((dst_positive_padded_resultmasktable) + ge_balance_negative_padded_resultmasktableentryvalue = (dst_negative_padded_resultmasktable) + ge_balance_positive_padded_resultmasktableentryvalue))))))))) /\ (forall dc_index_padded_resultmask dc_value_padded_resultmask. (exists pvs_le_gap_padded_resultmaskdomain. pvs_le_gap_padded_resultmaskdomain + (dc_index_padded_resultmask) = (n)) -> (exists dst_positive_code_padded_resultmasklookup dst_positive_scale_padded_resultmasklookup dst_negative_code_padded_resultmasklookup dst_negative_scale_padded_resultmasklookup dst_positive_padded_resultmasklookup dst_negative_padded_resultmasklookup. (((dc_mask_padded_result) = (((((dst_positive_code_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup)) * S ((dst_positive_code_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup)) + ((dst_positive_scale_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup))) + (((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) * S ((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) + ((dst_negative_scale_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)))) * S ((((dst_positive_code_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup)) * S ((dst_positive_code_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup)) + ((dst_positive_scale_padded_resultmasklookup) + (dst_positive_scale_padded_resultmasklookup))) + (((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) * S ((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) + ((dst_negative_scale_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)))) + ((((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) * S ((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) + ((dst_negative_scale_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup))) + (((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) * S ((dst_negative_code_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)) + ((dst_negative_scale_padded_resultmasklookup) + (dst_negative_scale_padded_resultmasklookup)))))) /\ (((((exists ff_h_pvs_padded_resultmasklookuppositive. ff_h_pvs_padded_resultmasklookuppositive + S (dst_positive_padded_resultmasklookup) = S ((S (dc_index_padded_resultmask)) * dst_positive_scale_padded_resultmasklookup)) /\ exists ff_q_pvs_padded_resultmasklookuppositive. dst_positive_code_padded_resultmasklookup = ff_q_pvs_padded_resultmasklookuppositive * S ((S (dc_index_padded_resultmask)) * dst_positive_scale_padded_resultmasklookup) + (dst_positive_padded_resultmasklookup))) /\ (((((exists ff_h_pvs_padded_resultmasklookupnegative. ff_h_pvs_padded_resultmasklookupnegative + S (dst_negative_padded_resultmasklookup) = S ((S (dc_index_padded_resultmask)) * dst_negative_scale_padded_resultmasklookup)) /\ exists ff_q_pvs_padded_resultmasklookupnegative. dst_negative_code_padded_resultmasklookup = ff_q_pvs_padded_resultmasklookupnegative * S ((S (dc_index_padded_resultmask)) * dst_negative_scale_padded_resultmasklookup) + (dst_negative_padded_resultmasklookup))) /\ (exists ge_balance_positive_padded_resultmasklookupvalue ge_balance_negative_padded_resultmasklookupvalue. (((((dc_value_padded_resultmask) = 2 * (ge_balance_positive_padded_resultmasklookupvalue) /\ (ge_balance_negative_padded_resultmasklookupvalue) = 0) \/ exists ge_signed_half_padded_resultmasklookupvaluedecode. (((dc_value_padded_resultmask) = 2 * ge_signed_half_padded_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_padded_resultmasklookupvalue) = 0) /\ (ge_balance_negative_padded_resultmasklookupvalue) = S ge_signed_half_padded_resultmasklookupvaluedecode))) /\ ((dst_positive_padded_resultmasklookup) + ge_balance_negative_padded_resultmasklookupvalue = (dst_negative_padded_resultmasklookup) + ge_balance_positive_padded_resultmasklookupvalue))))))))) -> ((((~((dc_index_padded_resultmask)=0)) /\ (exists dc_quotient_padded_resultmaskentry dc_left_padded_resultmaskentry dc_right_padded_resultmaskentry. (((n)=(dc_index_padded_resultmask)*dc_quotient_padded_resultmaskentry) /\ (((exists dst_positive_code_padded_resultmaskentryleft dst_positive_scale_padded_resultmaskentryleft dst_negative_code_padded_resultmaskentryleft dst_negative_scale_padded_resultmaskentryleft dst_positive_padded_resultmaskentryleft dst_negative_padded_resultmaskentryleft. (((F) = (((((dst_positive_code_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft)) * S ((dst_positive_code_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft)) + ((dst_positive_scale_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft))) + (((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) * S ((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) + ((dst_negative_scale_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)))) * S ((((dst_positive_code_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft)) * S ((dst_positive_code_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft)) + ((dst_positive_scale_padded_resultmaskentryleft) + (dst_positive_scale_padded_resultmaskentryleft))) + (((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) * S ((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) + ((dst_negative_scale_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)))) + ((((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) * S ((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) + ((dst_negative_scale_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft))) + (((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) * S ((dst_negative_code_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)) + ((dst_negative_scale_padded_resultmaskentryleft) + (dst_negative_scale_padded_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_padded_resultmaskentryleftpositive. ff_h_pvs_padded_resultmaskentryleftpositive + S (dst_positive_padded_resultmaskentryleft) = S ((S (dc_index_padded_resultmask)) * dst_positive_scale_padded_resultmaskentryleft)) /\ exists ff_q_pvs_padded_resultmaskentryleftpositive. dst_positive_code_padded_resultmaskentryleft = ff_q_pvs_padded_resultmaskentryleftpositive * S ((S (dc_index_padded_resultmask)) * dst_positive_scale_padded_resultmaskentryleft) + (dst_positive_padded_resultmaskentryleft))) /\ (((((exists ff_h_pvs_padded_resultmaskentryleftnegative. ff_h_pvs_padded_resultmaskentryleftnegative + S (dst_negative_padded_resultmaskentryleft) = S ((S (dc_index_padded_resultmask)) * dst_negative_scale_padded_resultmaskentryleft)) /\ exists ff_q_pvs_padded_resultmaskentryleftnegative. dst_negative_code_padded_resultmaskentryleft = ff_q_pvs_padded_resultmaskentryleftnegative * S ((S (dc_index_padded_resultmask)) * dst_negative_scale_padded_resultmaskentryleft) + (dst_negative_padded_resultmaskentryleft))) /\ (exists ge_balance_positive_padded_resultmaskentryleftvalue ge_balance_negative_padded_resultmaskentryleftvalue. (((((dc_left_padded_resultmaskentry) = 2 * (ge_balance_positive_padded_resultmaskentryleftvalue) /\ (ge_balance_negative_padded_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_padded_resultmaskentryleftvaluedecode. (((dc_left_padded_resultmaskentry) = 2 * ge_signed_half_padded_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_padded_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_padded_resultmaskentryleftvalue) = S ge_signed_half_padded_resultmaskentryleftvaluedecode))) /\ ((dst_positive_padded_resultmaskentryleft) + ge_balance_negative_padded_resultmaskentryleftvalue = (dst_negative_padded_resultmaskentryleft) + ge_balance_positive_padded_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_padded_resultmaskentryright dst_positive_scale_padded_resultmaskentryright dst_negative_code_padded_resultmaskentryright dst_negative_scale_padded_resultmaskentryright dst_positive_padded_resultmaskentryright dst_negative_padded_resultmaskentryright. (((G) = (((((dst_positive_code_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright)) * S ((dst_positive_code_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright)) + ((dst_positive_scale_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright))) + (((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) * S ((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) + ((dst_negative_scale_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)))) * S ((((dst_positive_code_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright)) * S ((dst_positive_code_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright)) + ((dst_positive_scale_padded_resultmaskentryright) + (dst_positive_scale_padded_resultmaskentryright))) + (((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) * S ((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) + ((dst_negative_scale_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)))) + ((((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) * S ((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) + ((dst_negative_scale_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright))) + (((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) * S ((dst_negative_code_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)) + ((dst_negative_scale_padded_resultmaskentryright) + (dst_negative_scale_padded_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_padded_resultmaskentryrightpositive. ff_h_pvs_padded_resultmaskentryrightpositive + S (dst_positive_padded_resultmaskentryright) = S ((S (dc_quotient_padded_resultmaskentry)) * dst_positive_scale_padded_resultmaskentryright)) /\ exists ff_q_pvs_padded_resultmaskentryrightpositive. dst_positive_code_padded_resultmaskentryright = ff_q_pvs_padded_resultmaskentryrightpositive * S ((S (dc_quotient_padded_resultmaskentry)) * dst_positive_scale_padded_resultmaskentryright) + (dst_positive_padded_resultmaskentryright))) /\ (((((exists ff_h_pvs_padded_resultmaskentryrightnegative. ff_h_pvs_padded_resultmaskentryrightnegative + S (dst_negative_padded_resultmaskentryright) = S ((S (dc_quotient_padded_resultmaskentry)) * dst_negative_scale_padded_resultmaskentryright)) /\ exists ff_q_pvs_padded_resultmaskentryrightnegative. dst_negative_code_padded_resultmaskentryright = ff_q_pvs_padded_resultmaskentryrightnegative * S ((S (dc_quotient_padded_resultmaskentry)) * dst_negative_scale_padded_resultmaskentryright) + (dst_negative_padded_resultmaskentryright))) /\ (exists ge_balance_positive_padded_resultmaskentryrightvalue ge_balance_negative_padded_resultmaskentryrightvalue. (((((dc_right_padded_resultmaskentry) = 2 * (ge_balance_positive_padded_resultmaskentryrightvalue) /\ (ge_balance_negative_padded_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_padded_resultmaskentryrightvaluedecode. (((dc_right_padded_resultmaskentry) = 2 * ge_signed_half_padded_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_padded_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_padded_resultmaskentryrightvalue) = S ge_signed_half_padded_resultmaskentryrightvaluedecode))) /\ ((dst_positive_padded_resultmaskentryright) + ge_balance_negative_padded_resultmaskentryrightvalue = (dst_negative_padded_resultmaskentryright) + ge_balance_positive_padded_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_padded_resultmaskentryproduct sto_an_padded_resultmaskentryproduct sto_bp_padded_resultmaskentryproduct sto_bn_padded_resultmaskentryproduct sto_cp_padded_resultmaskentryproduct sto_cn_padded_resultmaskentryproduct. (((((dc_left_padded_resultmaskentry) = 2 * (sto_ap_padded_resultmaskentryproduct) /\ (sto_an_padded_resultmaskentryproduct) = 0) \/ exists ge_signed_half_padded_resultmaskentryproductleft. (((dc_left_padded_resultmaskentry) = 2 * ge_signed_half_padded_resultmaskentryproductleft + 1 /\ (sto_ap_padded_resultmaskentryproduct) = 0) /\ (sto_an_padded_resultmaskentryproduct) = S ge_signed_half_padded_resultmaskentryproductleft))) /\ ((((((dc_right_padded_resultmaskentry) = 2 * (sto_bp_padded_resultmaskentryproduct) /\ (sto_bn_padded_resultmaskentryproduct) = 0) \/ exists ge_signed_half_padded_resultmaskentryproductright. (((dc_right_padded_resultmaskentry) = 2 * ge_signed_half_padded_resultmaskentryproductright + 1 /\ (sto_bp_padded_resultmaskentryproduct) = 0) /\ (sto_bn_padded_resultmaskentryproduct) = S ge_signed_half_padded_resultmaskentryproductright))) /\ ((((((dc_value_padded_resultmask) = 2 * (sto_cp_padded_resultmaskentryproduct) /\ (sto_cn_padded_resultmaskentryproduct) = 0) \/ exists ge_signed_half_padded_resultmaskentryproductoutput. (((dc_value_padded_resultmask) = 2 * ge_signed_half_padded_resultmaskentryproductoutput + 1 /\ (sto_cp_padded_resultmaskentryproduct) = 0) /\ (sto_cn_padded_resultmaskentryproduct) = S ge_signed_half_padded_resultmaskentryproductoutput))) /\ ((sto_ap_padded_resultmaskentryproduct * sto_bp_padded_resultmaskentryproduct + sto_an_padded_resultmaskentryproduct * sto_bn_padded_resultmaskentryproduct) + sto_cn_padded_resultmaskentryproduct = (sto_ap_padded_resultmaskentryproduct * sto_bn_padded_resultmaskentryproduct + sto_an_padded_resultmaskentryproduct * sto_bp_padded_resultmaskentryproduct) + sto_cp_padded_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_padded_resultmask)=0 \/ ~(exists pvs_factor_padded_resultmaskentrynondivisor. (n) = (dc_index_padded_resultmask) * pvs_factor_padded_resultmaskentrynondivisor)) /\ ((dc_value_padded_resultmask)=0))))))) /\ (exists dst_positive_code_padded_resultfold dst_positive_scale_padded_resultfold dst_negative_code_padded_resultfold dst_negative_scale_padded_resultfold dst_positive_sum_padded_resultfold dst_negative_sum_padded_resultfold. (((dc_mask_padded_result) = (((((dst_positive_code_padded_resultfold) + (dst_positive_scale_padded_resultfold)) * S ((dst_positive_code_padded_resultfold) + (dst_positive_scale_padded_resultfold)) + ((dst_positive_scale_padded_resultfold) + (dst_positive_scale_padded_resultfold))) + (((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) * S ((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) + ((dst_negative_scale_padded_resultfold) + (dst_negative_scale_padded_resultfold)))) * S ((((dst_positive_code_padded_resultfold) + (dst_positive_scale_padded_resultfold)) * S ((dst_positive_code_padded_resultfold) + (dst_positive_scale_padded_resultfold)) + ((dst_positive_scale_padded_resultfold) + (dst_positive_scale_padded_resultfold))) + (((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) * S ((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) + ((dst_negative_scale_padded_resultfold) + (dst_negative_scale_padded_resultfold)))) + ((((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) * S ((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) + ((dst_negative_scale_padded_resultfold) + (dst_negative_scale_padded_resultfold))) + (((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) * S ((dst_negative_code_padded_resultfold) + (dst_negative_scale_padded_resultfold)) + ((dst_negative_scale_padded_resultfold) + (dst_negative_scale_padded_resultfold)))))) /\ (((exists fs_u_dst_padded_resultfoldpositive fs_v_dst_padded_resultfoldpositive. ((((exists fs_h_dst_padded_resultfoldpositive_body_start. fs_h_dst_padded_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_resultfoldpositive)) /\ exists fs_q_dst_padded_resultfoldpositive_body_start. fs_u_dst_padded_resultfoldpositive = fs_q_dst_padded_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_padded_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_padded_resultfoldpositive_body_terminal. fs_h_dst_padded_resultfoldpositive_body_terminal + S (dst_positive_sum_padded_resultfold) = S ((S (S (n))) * fs_v_dst_padded_resultfoldpositive)) /\ exists fs_q_dst_padded_resultfoldpositive_body_terminal. fs_u_dst_padded_resultfoldpositive = fs_q_dst_padded_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_padded_resultfoldpositive) + (dst_positive_sum_padded_resultfold))) /\ forall fs_i_dst_padded_resultfoldpositive_body_steps. (exists fs_lt_dst_padded_resultfoldpositive_body_steps_bound. fs_lt_dst_padded_resultfoldpositive_body_steps_bound + S fs_i_dst_padded_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_padded_resultfoldpositive_body_steps fs_r_dst_padded_resultfoldpositive_body_steps fs_s_dst_padded_resultfoldpositive_body_steps. ((((exists fs_h_dst_padded_resultfoldpositive_body_steps_summand. fs_h_dst_padded_resultfoldpositive_body_steps_summand + S (fs_a_dst_padded_resultfoldpositive_body_steps) = S ((S (fs_i_dst_padded_resultfoldpositive_body_steps)) * dst_positive_scale_padded_resultfold)) /\ exists fs_q_dst_padded_resultfoldpositive_body_steps_summand. dst_positive_code_padded_resultfold = fs_q_dst_padded_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_padded_resultfoldpositive_body_steps)) * dst_positive_scale_padded_resultfold) + (fs_a_dst_padded_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_resultfoldpositive_body_steps_partial. fs_h_dst_padded_resultfoldpositive_body_steps_partial + S (fs_r_dst_padded_resultfoldpositive_body_steps) = S ((S (fs_i_dst_padded_resultfoldpositive_body_steps)) * fs_v_dst_padded_resultfoldpositive)) /\ exists fs_q_dst_padded_resultfoldpositive_body_steps_partial. fs_u_dst_padded_resultfoldpositive = fs_q_dst_padded_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_padded_resultfoldpositive_body_steps)) * fs_v_dst_padded_resultfoldpositive) + (fs_r_dst_padded_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_padded_resultfoldpositive_body_steps_successor. fs_h_dst_padded_resultfoldpositive_body_steps_successor + S (fs_s_dst_padded_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_padded_resultfoldpositive_body_steps)) * fs_v_dst_padded_resultfoldpositive)) /\ exists fs_q_dst_padded_resultfoldpositive_body_steps_successor. fs_u_dst_padded_resultfoldpositive = fs_q_dst_padded_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_padded_resultfoldpositive_body_steps)) * fs_v_dst_padded_resultfoldpositive) + (fs_s_dst_padded_resultfoldpositive_body_steps))) /\ fs_s_dst_padded_resultfoldpositive_body_steps = fs_r_dst_padded_resultfoldpositive_body_steps + fs_a_dst_padded_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_padded_resultfoldnegative fs_v_dst_padded_resultfoldnegative. ((((exists fs_h_dst_padded_resultfoldnegative_body_start. fs_h_dst_padded_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_padded_resultfoldnegative)) /\ exists fs_q_dst_padded_resultfoldnegative_body_start. fs_u_dst_padded_resultfoldnegative = fs_q_dst_padded_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_padded_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_padded_resultfoldnegative_body_terminal. fs_h_dst_padded_resultfoldnegative_body_terminal + S (dst_negative_sum_padded_resultfold) = S ((S (S (n))) * fs_v_dst_padded_resultfoldnegative)) /\ exists fs_q_dst_padded_resultfoldnegative_body_terminal. fs_u_dst_padded_resultfoldnegative = fs_q_dst_padded_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_padded_resultfoldnegative) + (dst_negative_sum_padded_resultfold))) /\ forall fs_i_dst_padded_resultfoldnegative_body_steps. (exists fs_lt_dst_padded_resultfoldnegative_body_steps_bound. fs_lt_dst_padded_resultfoldnegative_body_steps_bound + S fs_i_dst_padded_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_padded_resultfoldnegative_body_steps fs_r_dst_padded_resultfoldnegative_body_steps fs_s_dst_padded_resultfoldnegative_body_steps. ((((exists fs_h_dst_padded_resultfoldnegative_body_steps_summand. fs_h_dst_padded_resultfoldnegative_body_steps_summand + S (fs_a_dst_padded_resultfoldnegative_body_steps) = S ((S (fs_i_dst_padded_resultfoldnegative_body_steps)) * dst_negative_scale_padded_resultfold)) /\ exists fs_q_dst_padded_resultfoldnegative_body_steps_summand. dst_negative_code_padded_resultfold = fs_q_dst_padded_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_padded_resultfoldnegative_body_steps)) * dst_negative_scale_padded_resultfold) + (fs_a_dst_padded_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_resultfoldnegative_body_steps_partial. fs_h_dst_padded_resultfoldnegative_body_steps_partial + S (fs_r_dst_padded_resultfoldnegative_body_steps) = S ((S (fs_i_dst_padded_resultfoldnegative_body_steps)) * fs_v_dst_padded_resultfoldnegative)) /\ exists fs_q_dst_padded_resultfoldnegative_body_steps_partial. fs_u_dst_padded_resultfoldnegative = fs_q_dst_padded_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_padded_resultfoldnegative_body_steps)) * fs_v_dst_padded_resultfoldnegative) + (fs_r_dst_padded_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_padded_resultfoldnegative_body_steps_successor. fs_h_dst_padded_resultfoldnegative_body_steps_successor + S (fs_s_dst_padded_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_padded_resultfoldnegative_body_steps)) * fs_v_dst_padded_resultfoldnegative)) /\ exists fs_q_dst_padded_resultfoldnegative_body_steps_successor. fs_u_dst_padded_resultfoldnegative = fs_q_dst_padded_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_padded_resultfoldnegative_body_steps)) * fs_v_dst_padded_resultfoldnegative) + (fs_s_dst_padded_resultfoldnegative_body_steps))) /\ fs_s_dst_padded_resultfoldnegative_body_steps = fs_r_dst_padded_resultfoldnegative_body_steps + fs_a_dst_padded_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_padded_resultfoldresult ge_balance_negative_padded_resultfoldresult. (((((z) = 2 * (ge_balance_positive_padded_resultfoldresult) /\ (ge_balance_negative_padded_resultfoldresult) = 0) \/ exists ge_signed_half_padded_resultfoldresultdecode. (((z) = 2 * ge_signed_half_padded_resultfoldresultdecode + 1 /\ (ge_balance_positive_padded_resultfoldresult) = 0) /\ (ge_balance_negative_padded_resultfoldresult) = S ge_signed_half_padded_resultfoldresultdecode))) /\ ((dst_positive_sum_padded_resultfold) + ge_balance_negative_padded_resultfoldresult = (dst_negative_sum_padded_resultfold) + ge_balance_positive_padded_resultfoldresult)))))))))))))