dirichlet_convolution_first_input_append_step

forall k G F M r H x u y e. (((exists dst_positive_code_append_previoustable dst_positive_scale_append_previoustable dst_negative_code_append_previoustable dst_negative_scale_append_previoustable. (((M) = (((((dst_positive_code_append_previoustable) + (dst_positive_scale_append_previoustable)) * S ((dst_positive_code_append_previoustable) + (dst_positive_scale_append_previoustable)) + ((dst_positive_scale_append_previoustable) + (dst_positive_scale_append_previoustable))) + (((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) * S ((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) + ((dst_negative_scale_append_previoustable) + (dst_negative_scale_append_previoustable)))) * S ((((dst_positive_code_append_previoustable) + (dst_positive_scale_append_previoustable)) * S ((dst_positive_code_append_previoustable) + (dst_positive_scale_append_previoustable)) + ((dst_positive_scale_append_previoustable) + (dst_positive_scale_append_previoustable))) + (((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) * S ((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) + ((dst_negative_scale_append_previoustable) + (dst_negative_scale_append_previoustable)))) + ((((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) * S ((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) + ((dst_negative_scale_append_previoustable) + (dst_negative_scale_append_previoustable))) + (((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) * S ((dst_negative_code_append_previoustable) + (dst_negative_scale_append_previoustable)) + ((dst_negative_scale_append_previoustable) + (dst_negative_scale_append_previoustable)))))) /\ (forall dst_index_append_previoustable. (exists pvs_le_gap_append_previoustabledomain. pvs_le_gap_append_previoustabledomain + (dst_index_append_previoustable) = (k)) -> exists dst_positive_append_previoustable dst_negative_append_previoustable dst_value_append_previoustable. ((((exists ff_h_pvs_append_previoustableentrypositive. ff_h_pvs_append_previoustableentrypositive + S (dst_positive_append_previoustable) = S ((S (dst_index_append_previoustable)) * dst_positive_scale_append_previoustable)) /\ exists ff_q_pvs_append_previoustableentrypositive. dst_positive_code_append_previoustable = ff_q_pvs_append_previoustableentrypositive * S ((S (dst_index_append_previoustable)) * dst_positive_scale_append_previoustable) + (dst_positive_append_previoustable))) /\ (((((exists ff_h_pvs_append_previoustableentrynegative. ff_h_pvs_append_previoustableentrynegative + S (dst_negative_append_previoustable) = S ((S (dst_index_append_previoustable)) * dst_negative_scale_append_previoustable)) /\ exists ff_q_pvs_append_previoustableentrynegative. dst_negative_code_append_previoustable = ff_q_pvs_append_previoustableentrynegative * S ((S (dst_index_append_previoustable)) * dst_negative_scale_append_previoustable) + (dst_negative_append_previoustable))) /\ (exists ge_balance_positive_append_previoustableentryvalue ge_balance_negative_append_previoustableentryvalue. (((((dst_value_append_previoustable) = 2 * (ge_balance_positive_append_previoustableentryvalue) /\ (ge_balance_negative_append_previoustableentryvalue) = 0) \/ exists ge_signed_half_append_previoustableentryvaluedecode. (((dst_value_append_previoustable) = 2 * ge_signed_half_append_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_append_previoustableentryvalue) = 0) /\ (ge_balance_negative_append_previoustableentryvalue) = S ge_signed_half_append_previoustableentryvaluedecode))) /\ ((dst_positive_append_previoustable) + ge_balance_negative_append_previoustableentryvalue = (dst_negative_append_previoustable) + ge_balance_positive_append_previoustableentryvalue))))))))) /\ (forall dc_index_append_previous dc_value_append_previous. (exists pvs_le_gap_append_previousdomain. pvs_le_gap_append_previousdomain + (dc_index_append_previous) = (k)) -> (exists dst_positive_code_append_previouslookup dst_positive_scale_append_previouslookup dst_negative_code_append_previouslookup dst_negative_scale_append_previouslookup dst_positive_append_previouslookup dst_negative_append_previouslookup. (((M) = (((((dst_positive_code_append_previouslookup) + (dst_positive_scale_append_previouslookup)) * S ((dst_positive_code_append_previouslookup) + (dst_positive_scale_append_previouslookup)) + ((dst_positive_scale_append_previouslookup) + (dst_positive_scale_append_previouslookup))) + (((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) * S ((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) + ((dst_negative_scale_append_previouslookup) + (dst_negative_scale_append_previouslookup)))) * S ((((dst_positive_code_append_previouslookup) + (dst_positive_scale_append_previouslookup)) * S ((dst_positive_code_append_previouslookup) + (dst_positive_scale_append_previouslookup)) + ((dst_positive_scale_append_previouslookup) + (dst_positive_scale_append_previouslookup))) + (((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) * S ((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) + ((dst_negative_scale_append_previouslookup) + (dst_negative_scale_append_previouslookup)))) + ((((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) * S ((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) + ((dst_negative_scale_append_previouslookup) + (dst_negative_scale_append_previouslookup))) + (((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) * S ((dst_negative_code_append_previouslookup) + (dst_negative_scale_append_previouslookup)) + ((dst_negative_scale_append_previouslookup) + (dst_negative_scale_append_previouslookup)))))) /\ (((((exists ff_h_pvs_append_previouslookuppositive. ff_h_pvs_append_previouslookuppositive + S (dst_positive_append_previouslookup) = S ((S (dc_index_append_previous)) * dst_positive_scale_append_previouslookup)) /\ exists ff_q_pvs_append_previouslookuppositive. dst_positive_code_append_previouslookup = ff_q_pvs_append_previouslookuppositive * S ((S (dc_index_append_previous)) * dst_positive_scale_append_previouslookup) + (dst_positive_append_previouslookup))) /\ (((((exists ff_h_pvs_append_previouslookupnegative. ff_h_pvs_append_previouslookupnegative + S (dst_negative_append_previouslookup) = S ((S (dc_index_append_previous)) * dst_negative_scale_append_previouslookup)) /\ exists ff_q_pvs_append_previouslookupnegative. dst_negative_code_append_previouslookup = ff_q_pvs_append_previouslookupnegative * S ((S (dc_index_append_previous)) * dst_negative_scale_append_previouslookup) + (dst_negative_append_previouslookup))) /\ (exists ge_balance_positive_append_previouslookupvalue ge_balance_negative_append_previouslookupvalue. (((((dc_value_append_previous) = 2 * (ge_balance_positive_append_previouslookupvalue) /\ (ge_balance_negative_append_previouslookupvalue) = 0) \/ exists ge_signed_half_append_previouslookupvaluedecode. (((dc_value_append_previous) = 2 * ge_signed_half_append_previouslookupvaluedecode + 1 /\ (ge_balance_positive_append_previouslookupvalue) = 0) /\ (ge_balance_negative_append_previouslookupvalue) = S ge_signed_half_append_previouslookupvaluedecode))) /\ ((dst_positive_append_previouslookup) + ge_balance_negative_append_previouslookupvalue = (dst_negative_append_previouslookup) + ge_balance_positive_append_previouslookupvalue))))))))) -> ((((~((dc_index_append_previous)=0)) /\ (exists dc_quotient_append_previousentry dc_left_append_previousentry dc_right_append_previousentry. (((S k)=(dc_index_append_previous)*dc_quotient_append_previousentry) /\ (((exists dst_positive_code_append_previousentryleft dst_positive_scale_append_previousentryleft dst_negative_code_append_previousentryleft dst_negative_scale_append_previousentryleft dst_positive_append_previousentryleft dst_negative_append_previousentryleft. (((G) = (((((dst_positive_code_append_previousentryleft) + (dst_positive_scale_append_previousentryleft)) * S ((dst_positive_code_append_previousentryleft) + (dst_positive_scale_append_previousentryleft)) + ((dst_positive_scale_append_previousentryleft) + (dst_positive_scale_append_previousentryleft))) + (((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) * S ((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) + ((dst_negative_scale_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)))) * S ((((dst_positive_code_append_previousentryleft) + (dst_positive_scale_append_previousentryleft)) * S ((dst_positive_code_append_previousentryleft) + (dst_positive_scale_append_previousentryleft)) + ((dst_positive_scale_append_previousentryleft) + (dst_positive_scale_append_previousentryleft))) + (((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) * S ((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) + ((dst_negative_scale_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)))) + ((((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) * S ((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) + ((dst_negative_scale_append_previousentryleft) + (dst_negative_scale_append_previousentryleft))) + (((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) * S ((dst_negative_code_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)) + ((dst_negative_scale_append_previousentryleft) + (dst_negative_scale_append_previousentryleft)))))) /\ (((((exists ff_h_pvs_append_previousentryleftpositive. ff_h_pvs_append_previousentryleftpositive + S (dst_positive_append_previousentryleft) = S ((S (dc_index_append_previous)) * dst_positive_scale_append_previousentryleft)) /\ exists ff_q_pvs_append_previousentryleftpositive. dst_positive_code_append_previousentryleft = ff_q_pvs_append_previousentryleftpositive * S ((S (dc_index_append_previous)) * dst_positive_scale_append_previousentryleft) + (dst_positive_append_previousentryleft))) /\ (((((exists ff_h_pvs_append_previousentryleftnegative. ff_h_pvs_append_previousentryleftnegative + S (dst_negative_append_previousentryleft) = S ((S (dc_index_append_previous)) * dst_negative_scale_append_previousentryleft)) /\ exists ff_q_pvs_append_previousentryleftnegative. dst_negative_code_append_previousentryleft = ff_q_pvs_append_previousentryleftnegative * S ((S (dc_index_append_previous)) * dst_negative_scale_append_previousentryleft) + (dst_negative_append_previousentryleft))) /\ (exists ge_balance_positive_append_previousentryleftvalue ge_balance_negative_append_previousentryleftvalue. (((((dc_left_append_previousentry) = 2 * (ge_balance_positive_append_previousentryleftvalue) /\ (ge_balance_negative_append_previousentryleftvalue) = 0) \/ exists ge_signed_half_append_previousentryleftvaluedecode. (((dc_left_append_previousentry) = 2 * ge_signed_half_append_previousentryleftvaluedecode + 1 /\ (ge_balance_positive_append_previousentryleftvalue) = 0) /\ (ge_balance_negative_append_previousentryleftvalue) = S ge_signed_half_append_previousentryleftvaluedecode))) /\ ((dst_positive_append_previousentryleft) + ge_balance_negative_append_previousentryleftvalue = (dst_negative_append_previousentryleft) + ge_balance_positive_append_previousentryleftvalue))))))))) /\ (((exists dst_positive_code_append_previousentryright dst_positive_scale_append_previousentryright dst_negative_code_append_previousentryright dst_negative_scale_append_previousentryright dst_positive_append_previousentryright dst_negative_append_previousentryright. (((F) = (((((dst_positive_code_append_previousentryright) + (dst_positive_scale_append_previousentryright)) * S ((dst_positive_code_append_previousentryright) + (dst_positive_scale_append_previousentryright)) + ((dst_positive_scale_append_previousentryright) + (dst_positive_scale_append_previousentryright))) + (((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) * S ((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) + ((dst_negative_scale_append_previousentryright) + (dst_negative_scale_append_previousentryright)))) * S ((((dst_positive_code_append_previousentryright) + (dst_positive_scale_append_previousentryright)) * S ((dst_positive_code_append_previousentryright) + (dst_positive_scale_append_previousentryright)) + ((dst_positive_scale_append_previousentryright) + (dst_positive_scale_append_previousentryright))) + (((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) * S ((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) + ((dst_negative_scale_append_previousentryright) + (dst_negative_scale_append_previousentryright)))) + ((((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) * S ((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) + ((dst_negative_scale_append_previousentryright) + (dst_negative_scale_append_previousentryright))) + (((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) * S ((dst_negative_code_append_previousentryright) + (dst_negative_scale_append_previousentryright)) + ((dst_negative_scale_append_previousentryright) + (dst_negative_scale_append_previousentryright)))))) /\ (((((exists ff_h_pvs_append_previousentryrightpositive. ff_h_pvs_append_previousentryrightpositive + S (dst_positive_append_previousentryright) = S ((S (dc_quotient_append_previousentry)) * dst_positive_scale_append_previousentryright)) /\ exists ff_q_pvs_append_previousentryrightpositive. dst_positive_code_append_previousentryright = ff_q_pvs_append_previousentryrightpositive * S ((S (dc_quotient_append_previousentry)) * dst_positive_scale_append_previousentryright) + (dst_positive_append_previousentryright))) /\ (((((exists ff_h_pvs_append_previousentryrightnegative. ff_h_pvs_append_previousentryrightnegative + S (dst_negative_append_previousentryright) = S ((S (dc_quotient_append_previousentry)) * dst_negative_scale_append_previousentryright)) /\ exists ff_q_pvs_append_previousentryrightnegative. dst_negative_code_append_previousentryright = ff_q_pvs_append_previousentryrightnegative * S ((S (dc_quotient_append_previousentry)) * dst_negative_scale_append_previousentryright) + (dst_negative_append_previousentryright))) /\ (exists ge_balance_positive_append_previousentryrightvalue ge_balance_negative_append_previousentryrightvalue. (((((dc_right_append_previousentry) = 2 * (ge_balance_positive_append_previousentryrightvalue) /\ (ge_balance_negative_append_previousentryrightvalue) = 0) \/ exists ge_signed_half_append_previousentryrightvaluedecode. (((dc_right_append_previousentry) = 2 * ge_signed_half_append_previousentryrightvaluedecode + 1 /\ (ge_balance_positive_append_previousentryrightvalue) = 0) /\ (ge_balance_negative_append_previousentryrightvalue) = S ge_signed_half_append_previousentryrightvaluedecode))) /\ ((dst_positive_append_previousentryright) + ge_balance_negative_append_previousentryrightvalue = (dst_negative_append_previousentryright) + ge_balance_positive_append_previousentryrightvalue))))))))) /\ (exists sto_ap_append_previousentryproduct sto_an_append_previousentryproduct sto_bp_append_previousentryproduct sto_bn_append_previousentryproduct sto_cp_append_previousentryproduct sto_cn_append_previousentryproduct. (((((dc_left_append_previousentry) = 2 * (sto_ap_append_previousentryproduct) /\ (sto_an_append_previousentryproduct) = 0) \/ exists ge_signed_half_append_previousentryproductleft. (((dc_left_append_previousentry) = 2 * ge_signed_half_append_previousentryproductleft + 1 /\ (sto_ap_append_previousentryproduct) = 0) /\ (sto_an_append_previousentryproduct) = S ge_signed_half_append_previousentryproductleft))) /\ ((((((dc_right_append_previousentry) = 2 * (sto_bp_append_previousentryproduct) /\ (sto_bn_append_previousentryproduct) = 0) \/ exists ge_signed_half_append_previousentryproductright. (((dc_right_append_previousentry) = 2 * ge_signed_half_append_previousentryproductright + 1 /\ (sto_bp_append_previousentryproduct) = 0) /\ (sto_bn_append_previousentryproduct) = S ge_signed_half_append_previousentryproductright))) /\ ((((((dc_value_append_previous) = 2 * (sto_cp_append_previousentryproduct) /\ (sto_cn_append_previousentryproduct) = 0) \/ exists ge_signed_half_append_previousentryproductoutput. (((dc_value_append_previous) = 2 * ge_signed_half_append_previousentryproductoutput + 1 /\ (sto_cp_append_previousentryproduct) = 0) /\ (sto_cn_append_previousentryproduct) = S ge_signed_half_append_previousentryproductoutput))) /\ ((sto_ap_append_previousentryproduct * sto_bp_append_previousentryproduct + sto_an_append_previousentryproduct * sto_bn_append_previousentryproduct) + sto_cn_append_previousentryproduct = (sto_ap_append_previousentryproduct * sto_bn_append_previousentryproduct + sto_an_append_previousentryproduct * sto_bp_append_previousentryproduct) + sto_cp_append_previousentryproduct))))))))))))))) \/ ((((dc_index_append_previous)=0 \/ ~(exists pvs_factor_append_previousentrynondivisor. (S k) = (dc_index_append_previous) * pvs_factor_append_previousentrynondivisor)) /\ ((dc_value_append_previous)=0))))))) -> (exists dst_positive_code_append_remainder dst_positive_scale_append_remainder dst_negative_code_append_remainder dst_negative_scale_append_remainder dst_positive_sum_append_remainder dst_negative_sum_append_remainder. (((M) = (((((dst_positive_code_append_remainder) + (dst_positive_scale_append_remainder)) * S ((dst_positive_code_append_remainder) + (dst_positive_scale_append_remainder)) + ((dst_positive_scale_append_remainder) + (dst_positive_scale_append_remainder))) + (((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) * S ((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) + ((dst_negative_scale_append_remainder) + (dst_negative_scale_append_remainder)))) * S ((((dst_positive_code_append_remainder) + (dst_positive_scale_append_remainder)) * S ((dst_positive_code_append_remainder) + (dst_positive_scale_append_remainder)) + ((dst_positive_scale_append_remainder) + (dst_positive_scale_append_remainder))) + (((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) * S ((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) + ((dst_negative_scale_append_remainder) + (dst_negative_scale_append_remainder)))) + ((((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) * S ((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) + ((dst_negative_scale_append_remainder) + (dst_negative_scale_append_remainder))) + (((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) * S ((dst_negative_code_append_remainder) + (dst_negative_scale_append_remainder)) + ((dst_negative_scale_append_remainder) + (dst_negative_scale_append_remainder)))))) /\ (((exists fs_u_dst_append_remainderpositive fs_v_dst_append_remainderpositive. ((((exists fs_h_dst_append_remainderpositive_body_start. fs_h_dst_append_remainderpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_remainderpositive)) /\ exists fs_q_dst_append_remainderpositive_body_start. fs_u_dst_append_remainderpositive = fs_q_dst_append_remainderpositive_body_start * S ((S (0)) * fs_v_dst_append_remainderpositive) + (0))) /\ ((((exists fs_h_dst_append_remainderpositive_body_terminal. fs_h_dst_append_remainderpositive_body_terminal + S (dst_positive_sum_append_remainder) = S ((S (S k)) * fs_v_dst_append_remainderpositive)) /\ exists fs_q_dst_append_remainderpositive_body_terminal. fs_u_dst_append_remainderpositive = fs_q_dst_append_remainderpositive_body_terminal * S ((S (S k)) * fs_v_dst_append_remainderpositive) + (dst_positive_sum_append_remainder))) /\ forall fs_i_dst_append_remainderpositive_body_steps. (exists fs_lt_dst_append_remainderpositive_body_steps_bound. fs_lt_dst_append_remainderpositive_body_steps_bound + S fs_i_dst_append_remainderpositive_body_steps = S k) -> exists fs_a_dst_append_remainderpositive_body_steps fs_r_dst_append_remainderpositive_body_steps fs_s_dst_append_remainderpositive_body_steps. ((((exists fs_h_dst_append_remainderpositive_body_steps_summand. fs_h_dst_append_remainderpositive_body_steps_summand + S (fs_a_dst_append_remainderpositive_body_steps) = S ((S (fs_i_dst_append_remainderpositive_body_steps)) * dst_positive_scale_append_remainder)) /\ exists fs_q_dst_append_remainderpositive_body_steps_summand. dst_positive_code_append_remainder = fs_q_dst_append_remainderpositive_body_steps_summand * S ((S (fs_i_dst_append_remainderpositive_body_steps)) * dst_positive_scale_append_remainder) + (fs_a_dst_append_remainderpositive_body_steps))) /\ ((((exists fs_h_dst_append_remainderpositive_body_steps_partial. fs_h_dst_append_remainderpositive_body_steps_partial + S (fs_r_dst_append_remainderpositive_body_steps) = S ((S (fs_i_dst_append_remainderpositive_body_steps)) * fs_v_dst_append_remainderpositive)) /\ exists fs_q_dst_append_remainderpositive_body_steps_partial. fs_u_dst_append_remainderpositive = fs_q_dst_append_remainderpositive_body_steps_partial * S ((S (fs_i_dst_append_remainderpositive_body_steps)) * fs_v_dst_append_remainderpositive) + (fs_r_dst_append_remainderpositive_body_steps))) /\ ((((exists fs_h_dst_append_remainderpositive_body_steps_successor. fs_h_dst_append_remainderpositive_body_steps_successor + S (fs_s_dst_append_remainderpositive_body_steps) = S ((S (S fs_i_dst_append_remainderpositive_body_steps)) * fs_v_dst_append_remainderpositive)) /\ exists fs_q_dst_append_remainderpositive_body_steps_successor. fs_u_dst_append_remainderpositive = fs_q_dst_append_remainderpositive_body_steps_successor * S ((S (S fs_i_dst_append_remainderpositive_body_steps)) * fs_v_dst_append_remainderpositive) + (fs_s_dst_append_remainderpositive_body_steps))) /\ fs_s_dst_append_remainderpositive_body_steps = fs_r_dst_append_remainderpositive_body_steps + fs_a_dst_append_remainderpositive_body_steps)))))) /\ (((exists fs_u_dst_append_remaindernegative fs_v_dst_append_remaindernegative. ((((exists fs_h_dst_append_remaindernegative_body_start. fs_h_dst_append_remaindernegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_remaindernegative)) /\ exists fs_q_dst_append_remaindernegative_body_start. fs_u_dst_append_remaindernegative = fs_q_dst_append_remaindernegative_body_start * S ((S (0)) * fs_v_dst_append_remaindernegative) + (0))) /\ ((((exists fs_h_dst_append_remaindernegative_body_terminal. fs_h_dst_append_remaindernegative_body_terminal + S (dst_negative_sum_append_remainder) = S ((S (S k)) * fs_v_dst_append_remaindernegative)) /\ exists fs_q_dst_append_remaindernegative_body_terminal. fs_u_dst_append_remaindernegative = fs_q_dst_append_remaindernegative_body_terminal * S ((S (S k)) * fs_v_dst_append_remaindernegative) + (dst_negative_sum_append_remainder))) /\ forall fs_i_dst_append_remaindernegative_body_steps. (exists fs_lt_dst_append_remaindernegative_body_steps_bound. fs_lt_dst_append_remaindernegative_body_steps_bound + S fs_i_dst_append_remaindernegative_body_steps = S k) -> exists fs_a_dst_append_remaindernegative_body_steps fs_r_dst_append_remaindernegative_body_steps fs_s_dst_append_remaindernegative_body_steps. ((((exists fs_h_dst_append_remaindernegative_body_steps_summand. fs_h_dst_append_remaindernegative_body_steps_summand + S (fs_a_dst_append_remaindernegative_body_steps) = S ((S (fs_i_dst_append_remaindernegative_body_steps)) * dst_negative_scale_append_remainder)) /\ exists fs_q_dst_append_remaindernegative_body_steps_summand. dst_negative_code_append_remainder = fs_q_dst_append_remaindernegative_body_steps_summand * S ((S (fs_i_dst_append_remaindernegative_body_steps)) * dst_negative_scale_append_remainder) + (fs_a_dst_append_remaindernegative_body_steps))) /\ ((((exists fs_h_dst_append_remaindernegative_body_steps_partial. fs_h_dst_append_remaindernegative_body_steps_partial + S (fs_r_dst_append_remaindernegative_body_steps) = S ((S (fs_i_dst_append_remaindernegative_body_steps)) * fs_v_dst_append_remaindernegative)) /\ exists fs_q_dst_append_remaindernegative_body_steps_partial. fs_u_dst_append_remaindernegative = fs_q_dst_append_remaindernegative_body_steps_partial * S ((S (fs_i_dst_append_remaindernegative_body_steps)) * fs_v_dst_append_remaindernegative) + (fs_r_dst_append_remaindernegative_body_steps))) /\ ((((exists fs_h_dst_append_remaindernegative_body_steps_successor. fs_h_dst_append_remaindernegative_body_steps_successor + S (fs_s_dst_append_remaindernegative_body_steps) = S ((S (S fs_i_dst_append_remaindernegative_body_steps)) * fs_v_dst_append_remaindernegative)) /\ exists fs_q_dst_append_remaindernegative_body_steps_successor. fs_u_dst_append_remaindernegative = fs_q_dst_append_remaindernegative_body_steps_successor * S ((S (S fs_i_dst_append_remaindernegative_body_steps)) * fs_v_dst_append_remaindernegative) + (fs_s_dst_append_remaindernegative_body_steps))) /\ fs_s_dst_append_remaindernegative_body_steps = fs_r_dst_append_remaindernegative_body_steps + fs_a_dst_append_remaindernegative_body_steps)))))) /\ (exists ge_balance_positive_append_remainderresult ge_balance_negative_append_remainderresult. (((((r) = 2 * (ge_balance_positive_append_remainderresult) /\ (ge_balance_negative_append_remainderresult) = 0) \/ exists ge_signed_half_append_remainderresultdecode. (((r) = 2 * ge_signed_half_append_remainderresultdecode + 1 /\ (ge_balance_positive_append_remainderresult) = 0) /\ (ge_balance_negative_append_remainderresult) = S ge_signed_half_append_remainderresultdecode))) /\ ((dst_positive_sum_append_remainder) + ge_balance_negative_append_remainderresult = (dst_negative_sum_append_remainder) + ge_balance_positive_append_remainderresult))))))))) -> (((exists dst_positive_code_append_inputtable dst_positive_scale_append_inputtable dst_negative_code_append_inputtable dst_negative_scale_append_inputtable. (((H) = (((((dst_positive_code_append_inputtable) + (dst_positive_scale_append_inputtable)) * S ((dst_positive_code_append_inputtable) + (dst_positive_scale_append_inputtable)) + ((dst_positive_scale_append_inputtable) + (dst_positive_scale_append_inputtable))) + (((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) * S ((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) + ((dst_negative_scale_append_inputtable) + (dst_negative_scale_append_inputtable)))) * S ((((dst_positive_code_append_inputtable) + (dst_positive_scale_append_inputtable)) * S ((dst_positive_code_append_inputtable) + (dst_positive_scale_append_inputtable)) + ((dst_positive_scale_append_inputtable) + (dst_positive_scale_append_inputtable))) + (((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) * S ((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) + ((dst_negative_scale_append_inputtable) + (dst_negative_scale_append_inputtable)))) + ((((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) * S ((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) + ((dst_negative_scale_append_inputtable) + (dst_negative_scale_append_inputtable))) + (((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) * S ((dst_negative_code_append_inputtable) + (dst_negative_scale_append_inputtable)) + ((dst_negative_scale_append_inputtable) + (dst_negative_scale_append_inputtable)))))) /\ (forall dst_index_append_inputtable. (exists pvs_le_gap_append_inputtabledomain. pvs_le_gap_append_inputtabledomain + (dst_index_append_inputtable) = (S k)) -> exists dst_positive_append_inputtable dst_negative_append_inputtable dst_value_append_inputtable. ((((exists ff_h_pvs_append_inputtableentrypositive. ff_h_pvs_append_inputtableentrypositive + S (dst_positive_append_inputtable) = S ((S (dst_index_append_inputtable)) * dst_positive_scale_append_inputtable)) /\ exists ff_q_pvs_append_inputtableentrypositive. dst_positive_code_append_inputtable = ff_q_pvs_append_inputtableentrypositive * S ((S (dst_index_append_inputtable)) * dst_positive_scale_append_inputtable) + (dst_positive_append_inputtable))) /\ (((((exists ff_h_pvs_append_inputtableentrynegative. ff_h_pvs_append_inputtableentrynegative + S (dst_negative_append_inputtable) = S ((S (dst_index_append_inputtable)) * dst_negative_scale_append_inputtable)) /\ exists ff_q_pvs_append_inputtableentrynegative. dst_negative_code_append_inputtable = ff_q_pvs_append_inputtableentrynegative * S ((S (dst_index_append_inputtable)) * dst_negative_scale_append_inputtable) + (dst_negative_append_inputtable))) /\ (exists ge_balance_positive_append_inputtableentryvalue ge_balance_negative_append_inputtableentryvalue. (((((dst_value_append_inputtable) = 2 * (ge_balance_positive_append_inputtableentryvalue) /\ (ge_balance_negative_append_inputtableentryvalue) = 0) \/ exists ge_signed_half_append_inputtableentryvaluedecode. (((dst_value_append_inputtable) = 2 * ge_signed_half_append_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_append_inputtableentryvalue) = 0) /\ (ge_balance_negative_append_inputtableentryvalue) = S ge_signed_half_append_inputtableentryvaluedecode))) /\ ((dst_positive_append_inputtable) + ge_balance_negative_append_inputtableentryvalue = (dst_negative_append_inputtable) + ge_balance_positive_append_inputtableentryvalue))))))))) /\ (((forall dst_index_append_inputprefix dst_first_append_inputprefix dst_second_append_inputprefix. (exists pvs_gap_append_inputprefixbound. pvs_gap_append_inputprefixbound + S (dst_index_append_inputprefix) = (S k)) -> (exists dst_positive_code_append_inputprefixfirst dst_positive_scale_append_inputprefixfirst dst_negative_code_append_inputprefixfirst dst_negative_scale_append_inputprefixfirst dst_positive_append_inputprefixfirst dst_negative_append_inputprefixfirst. (((G) = (((((dst_positive_code_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst)) * S ((dst_positive_code_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst)) + ((dst_positive_scale_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst))) + (((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) * S ((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) + ((dst_negative_scale_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)))) * S ((((dst_positive_code_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst)) * S ((dst_positive_code_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst)) + ((dst_positive_scale_append_inputprefixfirst) + (dst_positive_scale_append_inputprefixfirst))) + (((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) * S ((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) + ((dst_negative_scale_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)))) + ((((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) * S ((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) + ((dst_negative_scale_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst))) + (((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) * S ((dst_negative_code_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)) + ((dst_negative_scale_append_inputprefixfirst) + (dst_negative_scale_append_inputprefixfirst)))))) /\ (((((exists ff_h_pvs_append_inputprefixfirstpositive. ff_h_pvs_append_inputprefixfirstpositive + S (dst_positive_append_inputprefixfirst) = S ((S (dst_index_append_inputprefix)) * dst_positive_scale_append_inputprefixfirst)) /\ exists ff_q_pvs_append_inputprefixfirstpositive. dst_positive_code_append_inputprefixfirst = ff_q_pvs_append_inputprefixfirstpositive * S ((S (dst_index_append_inputprefix)) * dst_positive_scale_append_inputprefixfirst) + (dst_positive_append_inputprefixfirst))) /\ (((((exists ff_h_pvs_append_inputprefixfirstnegative. ff_h_pvs_append_inputprefixfirstnegative + S (dst_negative_append_inputprefixfirst) = S ((S (dst_index_append_inputprefix)) * dst_negative_scale_append_inputprefixfirst)) /\ exists ff_q_pvs_append_inputprefixfirstnegative. dst_negative_code_append_inputprefixfirst = ff_q_pvs_append_inputprefixfirstnegative * S ((S (dst_index_append_inputprefix)) * dst_negative_scale_append_inputprefixfirst) + (dst_negative_append_inputprefixfirst))) /\ (exists ge_balance_positive_append_inputprefixfirstvalue ge_balance_negative_append_inputprefixfirstvalue. (((((dst_first_append_inputprefix) = 2 * (ge_balance_positive_append_inputprefixfirstvalue) /\ (ge_balance_negative_append_inputprefixfirstvalue) = 0) \/ exists ge_signed_half_append_inputprefixfirstvaluedecode. (((dst_first_append_inputprefix) = 2 * ge_signed_half_append_inputprefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_inputprefixfirstvalue) = 0) /\ (ge_balance_negative_append_inputprefixfirstvalue) = S ge_signed_half_append_inputprefixfirstvaluedecode))) /\ ((dst_positive_append_inputprefixfirst) + ge_balance_negative_append_inputprefixfirstvalue = (dst_negative_append_inputprefixfirst) + ge_balance_positive_append_inputprefixfirstvalue))))))))) -> (exists dst_positive_code_append_inputprefixsecond dst_positive_scale_append_inputprefixsecond dst_negative_code_append_inputprefixsecond dst_negative_scale_append_inputprefixsecond dst_positive_append_inputprefixsecond dst_negative_append_inputprefixsecond. (((H) = (((((dst_positive_code_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond)) * S ((dst_positive_code_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond)) + ((dst_positive_scale_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond))) + (((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) * S ((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) + ((dst_negative_scale_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)))) * S ((((dst_positive_code_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond)) * S ((dst_positive_code_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond)) + ((dst_positive_scale_append_inputprefixsecond) + (dst_positive_scale_append_inputprefixsecond))) + (((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) * S ((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) + ((dst_negative_scale_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)))) + ((((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) * S ((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) + ((dst_negative_scale_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond))) + (((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) * S ((dst_negative_code_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)) + ((dst_negative_scale_append_inputprefixsecond) + (dst_negative_scale_append_inputprefixsecond)))))) /\ (((((exists ff_h_pvs_append_inputprefixsecondpositive. ff_h_pvs_append_inputprefixsecondpositive + S (dst_positive_append_inputprefixsecond) = S ((S (dst_index_append_inputprefix)) * dst_positive_scale_append_inputprefixsecond)) /\ exists ff_q_pvs_append_inputprefixsecondpositive. dst_positive_code_append_inputprefixsecond = ff_q_pvs_append_inputprefixsecondpositive * S ((S (dst_index_append_inputprefix)) * dst_positive_scale_append_inputprefixsecond) + (dst_positive_append_inputprefixsecond))) /\ (((((exists ff_h_pvs_append_inputprefixsecondnegative. ff_h_pvs_append_inputprefixsecondnegative + S (dst_negative_append_inputprefixsecond) = S ((S (dst_index_append_inputprefix)) * dst_negative_scale_append_inputprefixsecond)) /\ exists ff_q_pvs_append_inputprefixsecondnegative. dst_negative_code_append_inputprefixsecond = ff_q_pvs_append_inputprefixsecondnegative * S ((S (dst_index_append_inputprefix)) * dst_negative_scale_append_inputprefixsecond) + (dst_negative_append_inputprefixsecond))) /\ (exists ge_balance_positive_append_inputprefixsecondvalue ge_balance_negative_append_inputprefixsecondvalue. (((((dst_second_append_inputprefix) = 2 * (ge_balance_positive_append_inputprefixsecondvalue) /\ (ge_balance_negative_append_inputprefixsecondvalue) = 0) \/ exists ge_signed_half_append_inputprefixsecondvaluedecode. (((dst_second_append_inputprefix) = 2 * ge_signed_half_append_inputprefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_inputprefixsecondvalue) = 0) /\ (ge_balance_negative_append_inputprefixsecondvalue) = S ge_signed_half_append_inputprefixsecondvaluedecode))) /\ ((dst_positive_append_inputprefixsecond) + ge_balance_negative_append_inputprefixsecondvalue = (dst_negative_append_inputprefixsecond) + ge_balance_positive_append_inputprefixsecondvalue))))))))) -> dst_first_append_inputprefix = dst_second_append_inputprefix) /\ (exists dst_positive_code_append_inputlast dst_positive_scale_append_inputlast dst_negative_code_append_inputlast dst_negative_scale_append_inputlast dst_positive_append_inputlast dst_negative_append_inputlast. (((H) = (((((dst_positive_code_append_inputlast) + (dst_positive_scale_append_inputlast)) * S ((dst_positive_code_append_inputlast) + (dst_positive_scale_append_inputlast)) + ((dst_positive_scale_append_inputlast) + (dst_positive_scale_append_inputlast))) + (((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) * S ((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) + ((dst_negative_scale_append_inputlast) + (dst_negative_scale_append_inputlast)))) * S ((((dst_positive_code_append_inputlast) + (dst_positive_scale_append_inputlast)) * S ((dst_positive_code_append_inputlast) + (dst_positive_scale_append_inputlast)) + ((dst_positive_scale_append_inputlast) + (dst_positive_scale_append_inputlast))) + (((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) * S ((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) + ((dst_negative_scale_append_inputlast) + (dst_negative_scale_append_inputlast)))) + ((((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) * S ((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) + ((dst_negative_scale_append_inputlast) + (dst_negative_scale_append_inputlast))) + (((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) * S ((dst_negative_code_append_inputlast) + (dst_negative_scale_append_inputlast)) + ((dst_negative_scale_append_inputlast) + (dst_negative_scale_append_inputlast)))))) /\ (((((exists ff_h_pvs_append_inputlastpositive. ff_h_pvs_append_inputlastpositive + S (dst_positive_append_inputlast) = S ((S (S k)) * dst_positive_scale_append_inputlast)) /\ exists ff_q_pvs_append_inputlastpositive. dst_positive_code_append_inputlast = ff_q_pvs_append_inputlastpositive * S ((S (S k)) * dst_positive_scale_append_inputlast) + (dst_positive_append_inputlast))) /\ (((((exists ff_h_pvs_append_inputlastnegative. ff_h_pvs_append_inputlastnegative + S (dst_negative_append_inputlast) = S ((S (S k)) * dst_negative_scale_append_inputlast)) /\ exists ff_q_pvs_append_inputlastnegative. dst_negative_code_append_inputlast = ff_q_pvs_append_inputlastnegative * S ((S (S k)) * dst_negative_scale_append_inputlast) + (dst_negative_append_inputlast))) /\ (exists ge_balance_positive_append_inputlastvalue ge_balance_negative_append_inputlastvalue. (((((x) = 2 * (ge_balance_positive_append_inputlastvalue) /\ (ge_balance_negative_append_inputlastvalue) = 0) \/ exists ge_signed_half_append_inputlastvaluedecode. (((x) = 2 * ge_signed_half_append_inputlastvaluedecode + 1 /\ (ge_balance_positive_append_inputlastvalue) = 0) /\ (ge_balance_negative_append_inputlastvalue) = S ge_signed_half_append_inputlastvaluedecode))) /\ ((dst_positive_append_inputlast) + ge_balance_negative_append_inputlastvalue = (dst_negative_append_inputlast) + ge_balance_positive_append_inputlastvalue))))))))))))) -> (exists dst_positive_code_append_unit_entry dst_positive_scale_append_unit_entry dst_negative_code_append_unit_entry dst_negative_scale_append_unit_entry dst_positive_append_unit_entry dst_negative_append_unit_entry. (((F) = (((((dst_positive_code_append_unit_entry) + (dst_positive_scale_append_unit_entry)) * S ((dst_positive_code_append_unit_entry) + (dst_positive_scale_append_unit_entry)) + ((dst_positive_scale_append_unit_entry) + (dst_positive_scale_append_unit_entry))) + (((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) * S ((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) + ((dst_negative_scale_append_unit_entry) + (dst_negative_scale_append_unit_entry)))) * S ((((dst_positive_code_append_unit_entry) + (dst_positive_scale_append_unit_entry)) * S ((dst_positive_code_append_unit_entry) + (dst_positive_scale_append_unit_entry)) + ((dst_positive_scale_append_unit_entry) + (dst_positive_scale_append_unit_entry))) + (((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) * S ((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) + ((dst_negative_scale_append_unit_entry) + (dst_negative_scale_append_unit_entry)))) + ((((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) * S ((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) + ((dst_negative_scale_append_unit_entry) + (dst_negative_scale_append_unit_entry))) + (((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) * S ((dst_negative_code_append_unit_entry) + (dst_negative_scale_append_unit_entry)) + ((dst_negative_scale_append_unit_entry) + (dst_negative_scale_append_unit_entry)))))) /\ (((((exists ff_h_pvs_append_unit_entrypositive. ff_h_pvs_append_unit_entrypositive + S (dst_positive_append_unit_entry) = S ((S (1)) * dst_positive_scale_append_unit_entry)) /\ exists ff_q_pvs_append_unit_entrypositive. dst_positive_code_append_unit_entry = ff_q_pvs_append_unit_entrypositive * S ((S (1)) * dst_positive_scale_append_unit_entry) + (dst_positive_append_unit_entry))) /\ (((((exists ff_h_pvs_append_unit_entrynegative. ff_h_pvs_append_unit_entrynegative + S (dst_negative_append_unit_entry) = S ((S (1)) * dst_negative_scale_append_unit_entry)) /\ exists ff_q_pvs_append_unit_entrynegative. dst_negative_code_append_unit_entry = ff_q_pvs_append_unit_entrynegative * S ((S (1)) * dst_negative_scale_append_unit_entry) + (dst_negative_append_unit_entry))) /\ (exists ge_balance_positive_append_unit_entryvalue ge_balance_negative_append_unit_entryvalue. (((((u) = 2 * (ge_balance_positive_append_unit_entryvalue) /\ (ge_balance_negative_append_unit_entryvalue) = 0) \/ exists ge_signed_half_append_unit_entryvaluedecode. (((u) = 2 * ge_signed_half_append_unit_entryvaluedecode + 1 /\ (ge_balance_positive_append_unit_entryvalue) = 0) /\ (ge_balance_negative_append_unit_entryvalue) = S ge_signed_half_append_unit_entryvaluedecode))) /\ ((dst_positive_append_unit_entry) + ge_balance_negative_append_unit_entryvalue = (dst_negative_append_unit_entry) + ge_balance_positive_append_unit_entryvalue))))))))) -> (exists sto_ap_append_product sto_an_append_product sto_bp_append_product sto_bn_append_product sto_cp_append_product sto_cn_append_product. (((((x) = 2 * (sto_ap_append_product) /\ (sto_an_append_product) = 0) \/ exists ge_signed_half_append_productleft. (((x) = 2 * ge_signed_half_append_productleft + 1 /\ (sto_ap_append_product) = 0) /\ (sto_an_append_product) = S ge_signed_half_append_productleft))) /\ ((((((u) = 2 * (sto_bp_append_product) /\ (sto_bn_append_product) = 0) \/ exists ge_signed_half_append_productright. (((u) = 2 * ge_signed_half_append_productright + 1 /\ (sto_bp_append_product) = 0) /\ (sto_bn_append_product) = S ge_signed_half_append_productright))) /\ ((((((y) = 2 * (sto_cp_append_product) /\ (sto_cn_append_product) = 0) \/ exists ge_signed_half_append_productoutput. (((y) = 2 * ge_signed_half_append_productoutput + 1 /\ (sto_cp_append_product) = 0) /\ (sto_cn_append_product) = S ge_signed_half_append_productoutput))) /\ ((sto_ap_append_product * sto_bp_append_product + sto_an_append_product * sto_bn_append_product) + sto_cn_append_product = (sto_ap_append_product * sto_bn_append_product + sto_an_append_product * sto_bp_append_product) + sto_cp_append_product))))))) -> (exists dsa_ap_append_add dsa_an_append_add dsa_bp_append_add dsa_bn_append_add dsa_cp_append_add dsa_cn_append_add. (((((r) = 2 * (dsa_ap_append_add) /\ (dsa_an_append_add) = 0) \/ exists ge_signed_half_append_addleft. (((r) = 2 * ge_signed_half_append_addleft + 1 /\ (dsa_ap_append_add) = 0) /\ (dsa_an_append_add) = S ge_signed_half_append_addleft))) /\ ((((((y) = 2 * (dsa_bp_append_add) /\ (dsa_bn_append_add) = 0) \/ exists ge_signed_half_append_addright. (((y) = 2 * ge_signed_half_append_addright + 1 /\ (dsa_bp_append_add) = 0) /\ (dsa_bn_append_add) = S ge_signed_half_append_addright))) /\ ((((((e) = 2 * (dsa_cp_append_add) /\ (dsa_cn_append_add) = 0) \/ exists ge_signed_half_append_addoutput. (((e) = 2 * ge_signed_half_append_addoutput + 1 /\ (dsa_cp_append_add) = 0) /\ (dsa_cn_append_add) = S ge_signed_half_append_addoutput))) /\ ((dsa_ap_append_add + dsa_bp_append_add) + dsa_cn_append_add = (dsa_an_append_add + dsa_bn_append_add) + dsa_cp_append_add))))))) -> (((~((S k)=0)) /\ (exists dc_mask_append_result. ((((exists dst_positive_code_append_resultmasktable dst_positive_scale_append_resultmasktable dst_negative_code_append_resultmasktable dst_negative_scale_append_resultmasktable. (((dc_mask_append_result) = (((((dst_positive_code_append_resultmasktable) + (dst_positive_scale_append_resultmasktable)) * S ((dst_positive_code_append_resultmasktable) + (dst_positive_scale_append_resultmasktable)) + ((dst_positive_scale_append_resultmasktable) + (dst_positive_scale_append_resultmasktable))) + (((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) * S ((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) + ((dst_negative_scale_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)))) * S ((((dst_positive_code_append_resultmasktable) + (dst_positive_scale_append_resultmasktable)) * S ((dst_positive_code_append_resultmasktable) + (dst_positive_scale_append_resultmasktable)) + ((dst_positive_scale_append_resultmasktable) + (dst_positive_scale_append_resultmasktable))) + (((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) * S ((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) + ((dst_negative_scale_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)))) + ((((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) * S ((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) + ((dst_negative_scale_append_resultmasktable) + (dst_negative_scale_append_resultmasktable))) + (((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) * S ((dst_negative_code_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)) + ((dst_negative_scale_append_resultmasktable) + (dst_negative_scale_append_resultmasktable)))))) /\ (forall dst_index_append_resultmasktable. (exists pvs_le_gap_append_resultmasktabledomain. pvs_le_gap_append_resultmasktabledomain + (dst_index_append_resultmasktable) = (S k)) -> exists dst_positive_append_resultmasktable dst_negative_append_resultmasktable dst_value_append_resultmasktable. ((((exists ff_h_pvs_append_resultmasktableentrypositive. ff_h_pvs_append_resultmasktableentrypositive + S (dst_positive_append_resultmasktable) = S ((S (dst_index_append_resultmasktable)) * dst_positive_scale_append_resultmasktable)) /\ exists ff_q_pvs_append_resultmasktableentrypositive. dst_positive_code_append_resultmasktable = ff_q_pvs_append_resultmasktableentrypositive * S ((S (dst_index_append_resultmasktable)) * dst_positive_scale_append_resultmasktable) + (dst_positive_append_resultmasktable))) /\ (((((exists ff_h_pvs_append_resultmasktableentrynegative. ff_h_pvs_append_resultmasktableentrynegative + S (dst_negative_append_resultmasktable) = S ((S (dst_index_append_resultmasktable)) * dst_negative_scale_append_resultmasktable)) /\ exists ff_q_pvs_append_resultmasktableentrynegative. dst_negative_code_append_resultmasktable = ff_q_pvs_append_resultmasktableentrynegative * S ((S (dst_index_append_resultmasktable)) * dst_negative_scale_append_resultmasktable) + (dst_negative_append_resultmasktable))) /\ (exists ge_balance_positive_append_resultmasktableentryvalue ge_balance_negative_append_resultmasktableentryvalue. (((((dst_value_append_resultmasktable) = 2 * (ge_balance_positive_append_resultmasktableentryvalue) /\ (ge_balance_negative_append_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_append_resultmasktableentryvaluedecode. (((dst_value_append_resultmasktable) = 2 * ge_signed_half_append_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_append_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_append_resultmasktableentryvalue) = S ge_signed_half_append_resultmasktableentryvaluedecode))) /\ ((dst_positive_append_resultmasktable) + ge_balance_negative_append_resultmasktableentryvalue = (dst_negative_append_resultmasktable) + ge_balance_positive_append_resultmasktableentryvalue))))))))) /\ (forall dc_index_append_resultmask dc_value_append_resultmask. (exists pvs_le_gap_append_resultmaskdomain. pvs_le_gap_append_resultmaskdomain + (dc_index_append_resultmask) = (S k)) -> (exists dst_positive_code_append_resultmasklookup dst_positive_scale_append_resultmasklookup dst_negative_code_append_resultmasklookup dst_negative_scale_append_resultmasklookup dst_positive_append_resultmasklookup dst_negative_append_resultmasklookup. (((dc_mask_append_result) = (((((dst_positive_code_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup)) * S ((dst_positive_code_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup)) + ((dst_positive_scale_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup))) + (((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) * S ((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) + ((dst_negative_scale_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)))) * S ((((dst_positive_code_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup)) * S ((dst_positive_code_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup)) + ((dst_positive_scale_append_resultmasklookup) + (dst_positive_scale_append_resultmasklookup))) + (((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) * S ((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) + ((dst_negative_scale_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)))) + ((((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) * S ((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) + ((dst_negative_scale_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup))) + (((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) * S ((dst_negative_code_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)) + ((dst_negative_scale_append_resultmasklookup) + (dst_negative_scale_append_resultmasklookup)))))) /\ (((((exists ff_h_pvs_append_resultmasklookuppositive. ff_h_pvs_append_resultmasklookuppositive + S (dst_positive_append_resultmasklookup) = S ((S (dc_index_append_resultmask)) * dst_positive_scale_append_resultmasklookup)) /\ exists ff_q_pvs_append_resultmasklookuppositive. dst_positive_code_append_resultmasklookup = ff_q_pvs_append_resultmasklookuppositive * S ((S (dc_index_append_resultmask)) * dst_positive_scale_append_resultmasklookup) + (dst_positive_append_resultmasklookup))) /\ (((((exists ff_h_pvs_append_resultmasklookupnegative. ff_h_pvs_append_resultmasklookupnegative + S (dst_negative_append_resultmasklookup) = S ((S (dc_index_append_resultmask)) * dst_negative_scale_append_resultmasklookup)) /\ exists ff_q_pvs_append_resultmasklookupnegative. dst_negative_code_append_resultmasklookup = ff_q_pvs_append_resultmasklookupnegative * S ((S (dc_index_append_resultmask)) * dst_negative_scale_append_resultmasklookup) + (dst_negative_append_resultmasklookup))) /\ (exists ge_balance_positive_append_resultmasklookupvalue ge_balance_negative_append_resultmasklookupvalue. (((((dc_value_append_resultmask) = 2 * (ge_balance_positive_append_resultmasklookupvalue) /\ (ge_balance_negative_append_resultmasklookupvalue) = 0) \/ exists ge_signed_half_append_resultmasklookupvaluedecode. (((dc_value_append_resultmask) = 2 * ge_signed_half_append_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_append_resultmasklookupvalue) = 0) /\ (ge_balance_negative_append_resultmasklookupvalue) = S ge_signed_half_append_resultmasklookupvaluedecode))) /\ ((dst_positive_append_resultmasklookup) + ge_balance_negative_append_resultmasklookupvalue = (dst_negative_append_resultmasklookup) + ge_balance_positive_append_resultmasklookupvalue))))))))) -> ((((~((dc_index_append_resultmask)=0)) /\ (exists dc_quotient_append_resultmaskentry dc_left_append_resultmaskentry dc_right_append_resultmaskentry. (((S k)=(dc_index_append_resultmask)*dc_quotient_append_resultmaskentry) /\ (((exists dst_positive_code_append_resultmaskentryleft dst_positive_scale_append_resultmaskentryleft dst_negative_code_append_resultmaskentryleft dst_negative_scale_append_resultmaskentryleft dst_positive_append_resultmaskentryleft dst_negative_append_resultmaskentryleft. (((H) = (((((dst_positive_code_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft)) * S ((dst_positive_code_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft)) + ((dst_positive_scale_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft))) + (((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) * S ((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) + ((dst_negative_scale_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)))) * S ((((dst_positive_code_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft)) * S ((dst_positive_code_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft)) + ((dst_positive_scale_append_resultmaskentryleft) + (dst_positive_scale_append_resultmaskentryleft))) + (((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) * S ((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) + ((dst_negative_scale_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)))) + ((((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) * S ((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) + ((dst_negative_scale_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft))) + (((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) * S ((dst_negative_code_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)) + ((dst_negative_scale_append_resultmaskentryleft) + (dst_negative_scale_append_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_append_resultmaskentryleftpositive. ff_h_pvs_append_resultmaskentryleftpositive + S (dst_positive_append_resultmaskentryleft) = S ((S (dc_index_append_resultmask)) * dst_positive_scale_append_resultmaskentryleft)) /\ exists ff_q_pvs_append_resultmaskentryleftpositive. dst_positive_code_append_resultmaskentryleft = ff_q_pvs_append_resultmaskentryleftpositive * S ((S (dc_index_append_resultmask)) * dst_positive_scale_append_resultmaskentryleft) + (dst_positive_append_resultmaskentryleft))) /\ (((((exists ff_h_pvs_append_resultmaskentryleftnegative. ff_h_pvs_append_resultmaskentryleftnegative + S (dst_negative_append_resultmaskentryleft) = S ((S (dc_index_append_resultmask)) * dst_negative_scale_append_resultmaskentryleft)) /\ exists ff_q_pvs_append_resultmaskentryleftnegative. dst_negative_code_append_resultmaskentryleft = ff_q_pvs_append_resultmaskentryleftnegative * S ((S (dc_index_append_resultmask)) * dst_negative_scale_append_resultmaskentryleft) + (dst_negative_append_resultmaskentryleft))) /\ (exists ge_balance_positive_append_resultmaskentryleftvalue ge_balance_negative_append_resultmaskentryleftvalue. (((((dc_left_append_resultmaskentry) = 2 * (ge_balance_positive_append_resultmaskentryleftvalue) /\ (ge_balance_negative_append_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_append_resultmaskentryleftvaluedecode. (((dc_left_append_resultmaskentry) = 2 * ge_signed_half_append_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_append_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_append_resultmaskentryleftvalue) = S ge_signed_half_append_resultmaskentryleftvaluedecode))) /\ ((dst_positive_append_resultmaskentryleft) + ge_balance_negative_append_resultmaskentryleftvalue = (dst_negative_append_resultmaskentryleft) + ge_balance_positive_append_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_append_resultmaskentryright dst_positive_scale_append_resultmaskentryright dst_negative_code_append_resultmaskentryright dst_negative_scale_append_resultmaskentryright dst_positive_append_resultmaskentryright dst_negative_append_resultmaskentryright. (((F) = (((((dst_positive_code_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright)) * S ((dst_positive_code_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright)) + ((dst_positive_scale_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright))) + (((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) * S ((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) + ((dst_negative_scale_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)))) * S ((((dst_positive_code_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright)) * S ((dst_positive_code_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright)) + ((dst_positive_scale_append_resultmaskentryright) + (dst_positive_scale_append_resultmaskentryright))) + (((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) * S ((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) + ((dst_negative_scale_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)))) + ((((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) * S ((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) + ((dst_negative_scale_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright))) + (((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) * S ((dst_negative_code_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)) + ((dst_negative_scale_append_resultmaskentryright) + (dst_negative_scale_append_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_append_resultmaskentryrightpositive. ff_h_pvs_append_resultmaskentryrightpositive + S (dst_positive_append_resultmaskentryright) = S ((S (dc_quotient_append_resultmaskentry)) * dst_positive_scale_append_resultmaskentryright)) /\ exists ff_q_pvs_append_resultmaskentryrightpositive. dst_positive_code_append_resultmaskentryright = ff_q_pvs_append_resultmaskentryrightpositive * S ((S (dc_quotient_append_resultmaskentry)) * dst_positive_scale_append_resultmaskentryright) + (dst_positive_append_resultmaskentryright))) /\ (((((exists ff_h_pvs_append_resultmaskentryrightnegative. ff_h_pvs_append_resultmaskentryrightnegative + S (dst_negative_append_resultmaskentryright) = S ((S (dc_quotient_append_resultmaskentry)) * dst_negative_scale_append_resultmaskentryright)) /\ exists ff_q_pvs_append_resultmaskentryrightnegative. dst_negative_code_append_resultmaskentryright = ff_q_pvs_append_resultmaskentryrightnegative * S ((S (dc_quotient_append_resultmaskentry)) * dst_negative_scale_append_resultmaskentryright) + (dst_negative_append_resultmaskentryright))) /\ (exists ge_balance_positive_append_resultmaskentryrightvalue ge_balance_negative_append_resultmaskentryrightvalue. (((((dc_right_append_resultmaskentry) = 2 * (ge_balance_positive_append_resultmaskentryrightvalue) /\ (ge_balance_negative_append_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_append_resultmaskentryrightvaluedecode. (((dc_right_append_resultmaskentry) = 2 * ge_signed_half_append_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_append_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_append_resultmaskentryrightvalue) = S ge_signed_half_append_resultmaskentryrightvaluedecode))) /\ ((dst_positive_append_resultmaskentryright) + ge_balance_negative_append_resultmaskentryrightvalue = (dst_negative_append_resultmaskentryright) + ge_balance_positive_append_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_append_resultmaskentryproduct sto_an_append_resultmaskentryproduct sto_bp_append_resultmaskentryproduct sto_bn_append_resultmaskentryproduct sto_cp_append_resultmaskentryproduct sto_cn_append_resultmaskentryproduct. (((((dc_left_append_resultmaskentry) = 2 * (sto_ap_append_resultmaskentryproduct) /\ (sto_an_append_resultmaskentryproduct) = 0) \/ exists ge_signed_half_append_resultmaskentryproductleft. (((dc_left_append_resultmaskentry) = 2 * ge_signed_half_append_resultmaskentryproductleft + 1 /\ (sto_ap_append_resultmaskentryproduct) = 0) /\ (sto_an_append_resultmaskentryproduct) = S ge_signed_half_append_resultmaskentryproductleft))) /\ ((((((dc_right_append_resultmaskentry) = 2 * (sto_bp_append_resultmaskentryproduct) /\ (sto_bn_append_resultmaskentryproduct) = 0) \/ exists ge_signed_half_append_resultmaskentryproductright. (((dc_right_append_resultmaskentry) = 2 * ge_signed_half_append_resultmaskentryproductright + 1 /\ (sto_bp_append_resultmaskentryproduct) = 0) /\ (sto_bn_append_resultmaskentryproduct) = S ge_signed_half_append_resultmaskentryproductright))) /\ ((((((dc_value_append_resultmask) = 2 * (sto_cp_append_resultmaskentryproduct) /\ (sto_cn_append_resultmaskentryproduct) = 0) \/ exists ge_signed_half_append_resultmaskentryproductoutput. (((dc_value_append_resultmask) = 2 * ge_signed_half_append_resultmaskentryproductoutput + 1 /\ (sto_cp_append_resultmaskentryproduct) = 0) /\ (sto_cn_append_resultmaskentryproduct) = S ge_signed_half_append_resultmaskentryproductoutput))) /\ ((sto_ap_append_resultmaskentryproduct * sto_bp_append_resultmaskentryproduct + sto_an_append_resultmaskentryproduct * sto_bn_append_resultmaskentryproduct) + sto_cn_append_resultmaskentryproduct = (sto_ap_append_resultmaskentryproduct * sto_bn_append_resultmaskentryproduct + sto_an_append_resultmaskentryproduct * sto_bp_append_resultmaskentryproduct) + sto_cp_append_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_append_resultmask)=0 \/ ~(exists pvs_factor_append_resultmaskentrynondivisor. (S k) = (dc_index_append_resultmask) * pvs_factor_append_resultmaskentrynondivisor)) /\ ((dc_value_append_resultmask)=0))))))) /\ (exists dst_positive_code_append_resultfold dst_positive_scale_append_resultfold dst_negative_code_append_resultfold dst_negative_scale_append_resultfold dst_positive_sum_append_resultfold dst_negative_sum_append_resultfold. (((dc_mask_append_result) = (((((dst_positive_code_append_resultfold) + (dst_positive_scale_append_resultfold)) * S ((dst_positive_code_append_resultfold) + (dst_positive_scale_append_resultfold)) + ((dst_positive_scale_append_resultfold) + (dst_positive_scale_append_resultfold))) + (((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) * S ((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) + ((dst_negative_scale_append_resultfold) + (dst_negative_scale_append_resultfold)))) * S ((((dst_positive_code_append_resultfold) + (dst_positive_scale_append_resultfold)) * S ((dst_positive_code_append_resultfold) + (dst_positive_scale_append_resultfold)) + ((dst_positive_scale_append_resultfold) + (dst_positive_scale_append_resultfold))) + (((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) * S ((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) + ((dst_negative_scale_append_resultfold) + (dst_negative_scale_append_resultfold)))) + ((((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) * S ((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) + ((dst_negative_scale_append_resultfold) + (dst_negative_scale_append_resultfold))) + (((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) * S ((dst_negative_code_append_resultfold) + (dst_negative_scale_append_resultfold)) + ((dst_negative_scale_append_resultfold) + (dst_negative_scale_append_resultfold)))))) /\ (((exists fs_u_dst_append_resultfoldpositive fs_v_dst_append_resultfoldpositive. ((((exists fs_h_dst_append_resultfoldpositive_body_start. fs_h_dst_append_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_resultfoldpositive)) /\ exists fs_q_dst_append_resultfoldpositive_body_start. fs_u_dst_append_resultfoldpositive = fs_q_dst_append_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_append_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_append_resultfoldpositive_body_terminal. fs_h_dst_append_resultfoldpositive_body_terminal + S (dst_positive_sum_append_resultfold) = S ((S (S (S k))) * fs_v_dst_append_resultfoldpositive)) /\ exists fs_q_dst_append_resultfoldpositive_body_terminal. fs_u_dst_append_resultfoldpositive = fs_q_dst_append_resultfoldpositive_body_terminal * S ((S (S (S k))) * fs_v_dst_append_resultfoldpositive) + (dst_positive_sum_append_resultfold))) /\ forall fs_i_dst_append_resultfoldpositive_body_steps. (exists fs_lt_dst_append_resultfoldpositive_body_steps_bound. fs_lt_dst_append_resultfoldpositive_body_steps_bound + S fs_i_dst_append_resultfoldpositive_body_steps = S (S k)) -> exists fs_a_dst_append_resultfoldpositive_body_steps fs_r_dst_append_resultfoldpositive_body_steps fs_s_dst_append_resultfoldpositive_body_steps. ((((exists fs_h_dst_append_resultfoldpositive_body_steps_summand. fs_h_dst_append_resultfoldpositive_body_steps_summand + S (fs_a_dst_append_resultfoldpositive_body_steps) = S ((S (fs_i_dst_append_resultfoldpositive_body_steps)) * dst_positive_scale_append_resultfold)) /\ exists fs_q_dst_append_resultfoldpositive_body_steps_summand. dst_positive_code_append_resultfold = fs_q_dst_append_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_append_resultfoldpositive_body_steps)) * dst_positive_scale_append_resultfold) + (fs_a_dst_append_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_append_resultfoldpositive_body_steps_partial. fs_h_dst_append_resultfoldpositive_body_steps_partial + S (fs_r_dst_append_resultfoldpositive_body_steps) = S ((S (fs_i_dst_append_resultfoldpositive_body_steps)) * fs_v_dst_append_resultfoldpositive)) /\ exists fs_q_dst_append_resultfoldpositive_body_steps_partial. fs_u_dst_append_resultfoldpositive = fs_q_dst_append_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_append_resultfoldpositive_body_steps)) * fs_v_dst_append_resultfoldpositive) + (fs_r_dst_append_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_append_resultfoldpositive_body_steps_successor. fs_h_dst_append_resultfoldpositive_body_steps_successor + S (fs_s_dst_append_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_append_resultfoldpositive_body_steps)) * fs_v_dst_append_resultfoldpositive)) /\ exists fs_q_dst_append_resultfoldpositive_body_steps_successor. fs_u_dst_append_resultfoldpositive = fs_q_dst_append_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_append_resultfoldpositive_body_steps)) * fs_v_dst_append_resultfoldpositive) + (fs_s_dst_append_resultfoldpositive_body_steps))) /\ fs_s_dst_append_resultfoldpositive_body_steps = fs_r_dst_append_resultfoldpositive_body_steps + fs_a_dst_append_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_append_resultfoldnegative fs_v_dst_append_resultfoldnegative. ((((exists fs_h_dst_append_resultfoldnegative_body_start. fs_h_dst_append_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_resultfoldnegative)) /\ exists fs_q_dst_append_resultfoldnegative_body_start. fs_u_dst_append_resultfoldnegative = fs_q_dst_append_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_append_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_append_resultfoldnegative_body_terminal. fs_h_dst_append_resultfoldnegative_body_terminal + S (dst_negative_sum_append_resultfold) = S ((S (S (S k))) * fs_v_dst_append_resultfoldnegative)) /\ exists fs_q_dst_append_resultfoldnegative_body_terminal. fs_u_dst_append_resultfoldnegative = fs_q_dst_append_resultfoldnegative_body_terminal * S ((S (S (S k))) * fs_v_dst_append_resultfoldnegative) + (dst_negative_sum_append_resultfold))) /\ forall fs_i_dst_append_resultfoldnegative_body_steps. (exists fs_lt_dst_append_resultfoldnegative_body_steps_bound. fs_lt_dst_append_resultfoldnegative_body_steps_bound + S fs_i_dst_append_resultfoldnegative_body_steps = S (S k)) -> exists fs_a_dst_append_resultfoldnegative_body_steps fs_r_dst_append_resultfoldnegative_body_steps fs_s_dst_append_resultfoldnegative_body_steps. ((((exists fs_h_dst_append_resultfoldnegative_body_steps_summand. fs_h_dst_append_resultfoldnegative_body_steps_summand + S (fs_a_dst_append_resultfoldnegative_body_steps) = S ((S (fs_i_dst_append_resultfoldnegative_body_steps)) * dst_negative_scale_append_resultfold)) /\ exists fs_q_dst_append_resultfoldnegative_body_steps_summand. dst_negative_code_append_resultfold = fs_q_dst_append_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_append_resultfoldnegative_body_steps)) * dst_negative_scale_append_resultfold) + (fs_a_dst_append_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_append_resultfoldnegative_body_steps_partial. fs_h_dst_append_resultfoldnegative_body_steps_partial + S (fs_r_dst_append_resultfoldnegative_body_steps) = S ((S (fs_i_dst_append_resultfoldnegative_body_steps)) * fs_v_dst_append_resultfoldnegative)) /\ exists fs_q_dst_append_resultfoldnegative_body_steps_partial. fs_u_dst_append_resultfoldnegative = fs_q_dst_append_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_append_resultfoldnegative_body_steps)) * fs_v_dst_append_resultfoldnegative) + (fs_r_dst_append_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_append_resultfoldnegative_body_steps_successor. fs_h_dst_append_resultfoldnegative_body_steps_successor + S (fs_s_dst_append_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_append_resultfoldnegative_body_steps)) * fs_v_dst_append_resultfoldnegative)) /\ exists fs_q_dst_append_resultfoldnegative_body_steps_successor. fs_u_dst_append_resultfoldnegative = fs_q_dst_append_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_append_resultfoldnegative_body_steps)) * fs_v_dst_append_resultfoldnegative) + (fs_s_dst_append_resultfoldnegative_body_steps))) /\ fs_s_dst_append_resultfoldnegative_body_steps = fs_r_dst_append_resultfoldnegative_body_steps + fs_a_dst_append_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_append_resultfoldresult ge_balance_negative_append_resultfoldresult. (((((e) = 2 * (ge_balance_positive_append_resultfoldresult) /\ (ge_balance_negative_append_resultfoldresult) = 0) \/ exists ge_signed_half_append_resultfoldresultdecode. (((e) = 2 * ge_signed_half_append_resultfoldresultdecode + 1 /\ (ge_balance_positive_append_resultfoldresult) = 0) /\ (ge_balance_negative_append_resultfoldresult) = S ge_signed_half_append_resultfoldresultdecode))) /\ ((dst_positive_sum_append_resultfold) + ge_balance_negative_append_resultfoldresult = (dst_negative_sum_append_resultfold) + ge_balance_positive_append_resultfoldresult)))))))))))))