dirichlet_convolution_prefix_last_step

Exact expanded first-order arithmetic statement

forall F G k M r a b y z. (((exists dst_positive_code_step_previoustable dst_positive_scale_step_previoustable dst_negative_code_step_previoustable dst_negative_scale_step_previoustable. (((M) = (((((dst_positive_code_step_previoustable) + (dst_positive_scale_step_previoustable)) * S ((dst_positive_code_step_previoustable) + (dst_positive_scale_step_previoustable)) + ((dst_positive_scale_step_previoustable) + (dst_positive_scale_step_previoustable))) + (((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) * S ((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) + ((dst_negative_scale_step_previoustable) + (dst_negative_scale_step_previoustable)))) * S ((((dst_positive_code_step_previoustable) + (dst_positive_scale_step_previoustable)) * S ((dst_positive_code_step_previoustable) + (dst_positive_scale_step_previoustable)) + ((dst_positive_scale_step_previoustable) + (dst_positive_scale_step_previoustable))) + (((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) * S ((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) + ((dst_negative_scale_step_previoustable) + (dst_negative_scale_step_previoustable)))) + ((((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) * S ((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) + ((dst_negative_scale_step_previoustable) + (dst_negative_scale_step_previoustable))) + (((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) * S ((dst_negative_code_step_previoustable) + (dst_negative_scale_step_previoustable)) + ((dst_negative_scale_step_previoustable) + (dst_negative_scale_step_previoustable)))))) /\ (forall dst_index_step_previoustable. (exists pvs_le_gap_step_previoustabledomain. pvs_le_gap_step_previoustabledomain + (dst_index_step_previoustable) = (k)) -> exists dst_positive_step_previoustable dst_negative_step_previoustable dst_value_step_previoustable. ((((exists ff_h_pvs_step_previoustableentrypositive. ff_h_pvs_step_previoustableentrypositive + S (dst_positive_step_previoustable) = S ((S (dst_index_step_previoustable)) * dst_positive_scale_step_previoustable)) /\ exists ff_q_pvs_step_previoustableentrypositive. dst_positive_code_step_previoustable = ff_q_pvs_step_previoustableentrypositive * S ((S (dst_index_step_previoustable)) * dst_positive_scale_step_previoustable) + (dst_positive_step_previoustable))) /\ (((((exists ff_h_pvs_step_previoustableentrynegative. ff_h_pvs_step_previoustableentrynegative + S (dst_negative_step_previoustable) = S ((S (dst_index_step_previoustable)) * dst_negative_scale_step_previoustable)) /\ exists ff_q_pvs_step_previoustableentrynegative. dst_negative_code_step_previoustable = ff_q_pvs_step_previoustableentrynegative * S ((S (dst_index_step_previoustable)) * dst_negative_scale_step_previoustable) + (dst_negative_step_previoustable))) /\ (exists ge_balance_positive_step_previoustableentryvalue ge_balance_negative_step_previoustableentryvalue. (((((dst_value_step_previoustable) = 2 * (ge_balance_positive_step_previoustableentryvalue) /\ (ge_balance_negative_step_previoustableentryvalue) = 0) \/ exists ge_signed_half_step_previoustableentryvaluedecode. (((dst_value_step_previoustable) = 2 * ge_signed_half_step_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_step_previoustableentryvalue) = 0) /\ (ge_balance_negative_step_previoustableentryvalue) = S ge_signed_half_step_previoustableentryvaluedecode))) /\ ((dst_positive_step_previoustable) + ge_balance_negative_step_previoustableentryvalue = (dst_negative_step_previoustable) + ge_balance_positive_step_previoustableentryvalue))))))))) /\ (forall dc_index_step_previous dc_value_step_previous. (exists pvs_le_gap_step_previousdomain. pvs_le_gap_step_previousdomain + (dc_index_step_previous) = (k)) -> (exists dst_positive_code_step_previouslookup dst_positive_scale_step_previouslookup dst_negative_code_step_previouslookup dst_negative_scale_step_previouslookup dst_positive_step_previouslookup dst_negative_step_previouslookup. (((M) = (((((dst_positive_code_step_previouslookup) + (dst_positive_scale_step_previouslookup)) * S ((dst_positive_code_step_previouslookup) + (dst_positive_scale_step_previouslookup)) + ((dst_positive_scale_step_previouslookup) + (dst_positive_scale_step_previouslookup))) + (((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) * S ((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) + ((dst_negative_scale_step_previouslookup) + (dst_negative_scale_step_previouslookup)))) * S ((((dst_positive_code_step_previouslookup) + (dst_positive_scale_step_previouslookup)) * S ((dst_positive_code_step_previouslookup) + (dst_positive_scale_step_previouslookup)) + ((dst_positive_scale_step_previouslookup) + (dst_positive_scale_step_previouslookup))) + (((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) * S ((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) + ((dst_negative_scale_step_previouslookup) + (dst_negative_scale_step_previouslookup)))) + ((((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) * S ((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) + ((dst_negative_scale_step_previouslookup) + (dst_negative_scale_step_previouslookup))) + (((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) * S ((dst_negative_code_step_previouslookup) + (dst_negative_scale_step_previouslookup)) + ((dst_negative_scale_step_previouslookup) + (dst_negative_scale_step_previouslookup)))))) /\ (((((exists ff_h_pvs_step_previouslookuppositive. ff_h_pvs_step_previouslookuppositive + S (dst_positive_step_previouslookup) = S ((S (dc_index_step_previous)) * dst_positive_scale_step_previouslookup)) /\ exists ff_q_pvs_step_previouslookuppositive. dst_positive_code_step_previouslookup = ff_q_pvs_step_previouslookuppositive * S ((S (dc_index_step_previous)) * dst_positive_scale_step_previouslookup) + (dst_positive_step_previouslookup))) /\ (((((exists ff_h_pvs_step_previouslookupnegative. ff_h_pvs_step_previouslookupnegative + S (dst_negative_step_previouslookup) = S ((S (dc_index_step_previous)) * dst_negative_scale_step_previouslookup)) /\ exists ff_q_pvs_step_previouslookupnegative. dst_negative_code_step_previouslookup = ff_q_pvs_step_previouslookupnegative * S ((S (dc_index_step_previous)) * dst_negative_scale_step_previouslookup) + (dst_negative_step_previouslookup))) /\ (exists ge_balance_positive_step_previouslookupvalue ge_balance_negative_step_previouslookupvalue. (((((dc_value_step_previous) = 2 * (ge_balance_positive_step_previouslookupvalue) /\ (ge_balance_negative_step_previouslookupvalue) = 0) \/ exists ge_signed_half_step_previouslookupvaluedecode. (((dc_value_step_previous) = 2 * ge_signed_half_step_previouslookupvaluedecode + 1 /\ (ge_balance_positive_step_previouslookupvalue) = 0) /\ (ge_balance_negative_step_previouslookupvalue) = S ge_signed_half_step_previouslookupvaluedecode))) /\ ((dst_positive_step_previouslookup) + ge_balance_negative_step_previouslookupvalue = (dst_negative_step_previouslookup) + ge_balance_positive_step_previouslookupvalue))))))))) -> ((((~((dc_index_step_previous)=0)) /\ (exists dc_quotient_step_previousentry dc_left_step_previousentry dc_right_step_previousentry. (((S k)=(dc_index_step_previous)*dc_quotient_step_previousentry) /\ (((exists dst_positive_code_step_previousentryleft dst_positive_scale_step_previousentryleft dst_negative_code_step_previousentryleft dst_negative_scale_step_previousentryleft dst_positive_step_previousentryleft dst_negative_step_previousentryleft. (((F) = (((((dst_positive_code_step_previousentryleft) + (dst_positive_scale_step_previousentryleft)) * S ((dst_positive_code_step_previousentryleft) + (dst_positive_scale_step_previousentryleft)) + ((dst_positive_scale_step_previousentryleft) + (dst_positive_scale_step_previousentryleft))) + (((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) * S ((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) + ((dst_negative_scale_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)))) * S ((((dst_positive_code_step_previousentryleft) + (dst_positive_scale_step_previousentryleft)) * S ((dst_positive_code_step_previousentryleft) + (dst_positive_scale_step_previousentryleft)) + ((dst_positive_scale_step_previousentryleft) + (dst_positive_scale_step_previousentryleft))) + (((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) * S ((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) + ((dst_negative_scale_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)))) + ((((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) * S ((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) + ((dst_negative_scale_step_previousentryleft) + (dst_negative_scale_step_previousentryleft))) + (((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) * S ((dst_negative_code_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)) + ((dst_negative_scale_step_previousentryleft) + (dst_negative_scale_step_previousentryleft)))))) /\ (((((exists ff_h_pvs_step_previousentryleftpositive. ff_h_pvs_step_previousentryleftpositive + S (dst_positive_step_previousentryleft) = S ((S (dc_index_step_previous)) * dst_positive_scale_step_previousentryleft)) /\ exists ff_q_pvs_step_previousentryleftpositive. dst_positive_code_step_previousentryleft = ff_q_pvs_step_previousentryleftpositive * S ((S (dc_index_step_previous)) * dst_positive_scale_step_previousentryleft) + (dst_positive_step_previousentryleft))) /\ (((((exists ff_h_pvs_step_previousentryleftnegative. ff_h_pvs_step_previousentryleftnegative + S (dst_negative_step_previousentryleft) = S ((S (dc_index_step_previous)) * dst_negative_scale_step_previousentryleft)) /\ exists ff_q_pvs_step_previousentryleftnegative. dst_negative_code_step_previousentryleft = ff_q_pvs_step_previousentryleftnegative * S ((S (dc_index_step_previous)) * dst_negative_scale_step_previousentryleft) + (dst_negative_step_previousentryleft))) /\ (exists ge_balance_positive_step_previousentryleftvalue ge_balance_negative_step_previousentryleftvalue. (((((dc_left_step_previousentry) = 2 * (ge_balance_positive_step_previousentryleftvalue) /\ (ge_balance_negative_step_previousentryleftvalue) = 0) \/ exists ge_signed_half_step_previousentryleftvaluedecode. (((dc_left_step_previousentry) = 2 * ge_signed_half_step_previousentryleftvaluedecode + 1 /\ (ge_balance_positive_step_previousentryleftvalue) = 0) /\ (ge_balance_negative_step_previousentryleftvalue) = S ge_signed_half_step_previousentryleftvaluedecode))) /\ ((dst_positive_step_previousentryleft) + ge_balance_negative_step_previousentryleftvalue = (dst_negative_step_previousentryleft) + ge_balance_positive_step_previousentryleftvalue))))))))) /\ (((exists dst_positive_code_step_previousentryright dst_positive_scale_step_previousentryright dst_negative_code_step_previousentryright dst_negative_scale_step_previousentryright dst_positive_step_previousentryright dst_negative_step_previousentryright. (((G) = (((((dst_positive_code_step_previousentryright) + (dst_positive_scale_step_previousentryright)) * S ((dst_positive_code_step_previousentryright) + (dst_positive_scale_step_previousentryright)) + ((dst_positive_scale_step_previousentryright) + (dst_positive_scale_step_previousentryright))) + (((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) * S ((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) + ((dst_negative_scale_step_previousentryright) + (dst_negative_scale_step_previousentryright)))) * S ((((dst_positive_code_step_previousentryright) + (dst_positive_scale_step_previousentryright)) * S ((dst_positive_code_step_previousentryright) + (dst_positive_scale_step_previousentryright)) + ((dst_positive_scale_step_previousentryright) + (dst_positive_scale_step_previousentryright))) + (((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) * S ((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) + ((dst_negative_scale_step_previousentryright) + (dst_negative_scale_step_previousentryright)))) + ((((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) * S ((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) + ((dst_negative_scale_step_previousentryright) + (dst_negative_scale_step_previousentryright))) + (((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) * S ((dst_negative_code_step_previousentryright) + (dst_negative_scale_step_previousentryright)) + ((dst_negative_scale_step_previousentryright) + (dst_negative_scale_step_previousentryright)))))) /\ (((((exists ff_h_pvs_step_previousentryrightpositive. ff_h_pvs_step_previousentryrightpositive + S (dst_positive_step_previousentryright) = S ((S (dc_quotient_step_previousentry)) * dst_positive_scale_step_previousentryright)) /\ exists ff_q_pvs_step_previousentryrightpositive. dst_positive_code_step_previousentryright = ff_q_pvs_step_previousentryrightpositive * S ((S (dc_quotient_step_previousentry)) * dst_positive_scale_step_previousentryright) + (dst_positive_step_previousentryright))) /\ (((((exists ff_h_pvs_step_previousentryrightnegative. ff_h_pvs_step_previousentryrightnegative + S (dst_negative_step_previousentryright) = S ((S (dc_quotient_step_previousentry)) * dst_negative_scale_step_previousentryright)) /\ exists ff_q_pvs_step_previousentryrightnegative. dst_negative_code_step_previousentryright = ff_q_pvs_step_previousentryrightnegative * S ((S (dc_quotient_step_previousentry)) * dst_negative_scale_step_previousentryright) + (dst_negative_step_previousentryright))) /\ (exists ge_balance_positive_step_previousentryrightvalue ge_balance_negative_step_previousentryrightvalue. (((((dc_right_step_previousentry) = 2 * (ge_balance_positive_step_previousentryrightvalue) /\ (ge_balance_negative_step_previousentryrightvalue) = 0) \/ exists ge_signed_half_step_previousentryrightvaluedecode. (((dc_right_step_previousentry) = 2 * ge_signed_half_step_previousentryrightvaluedecode + 1 /\ (ge_balance_positive_step_previousentryrightvalue) = 0) /\ (ge_balance_negative_step_previousentryrightvalue) = S ge_signed_half_step_previousentryrightvaluedecode))) /\ ((dst_positive_step_previousentryright) + ge_balance_negative_step_previousentryrightvalue = (dst_negative_step_previousentryright) + ge_balance_positive_step_previousentryrightvalue))))))))) /\ (exists sto_ap_step_previousentryproduct sto_an_step_previousentryproduct sto_bp_step_previousentryproduct sto_bn_step_previousentryproduct sto_cp_step_previousentryproduct sto_cn_step_previousentryproduct. (((((dc_left_step_previousentry) = 2 * (sto_ap_step_previousentryproduct) /\ (sto_an_step_previousentryproduct) = 0) \/ exists ge_signed_half_step_previousentryproductleft. (((dc_left_step_previousentry) = 2 * ge_signed_half_step_previousentryproductleft + 1 /\ (sto_ap_step_previousentryproduct) = 0) /\ (sto_an_step_previousentryproduct) = S ge_signed_half_step_previousentryproductleft))) /\ ((((((dc_right_step_previousentry) = 2 * (sto_bp_step_previousentryproduct) /\ (sto_bn_step_previousentryproduct) = 0) \/ exists ge_signed_half_step_previousentryproductright. (((dc_right_step_previousentry) = 2 * ge_signed_half_step_previousentryproductright + 1 /\ (sto_bp_step_previousentryproduct) = 0) /\ (sto_bn_step_previousentryproduct) = S ge_signed_half_step_previousentryproductright))) /\ ((((((dc_value_step_previous) = 2 * (sto_cp_step_previousentryproduct) /\ (sto_cn_step_previousentryproduct) = 0) \/ exists ge_signed_half_step_previousentryproductoutput. (((dc_value_step_previous) = 2 * ge_signed_half_step_previousentryproductoutput + 1 /\ (sto_cp_step_previousentryproduct) = 0) /\ (sto_cn_step_previousentryproduct) = S ge_signed_half_step_previousentryproductoutput))) /\ ((sto_ap_step_previousentryproduct * sto_bp_step_previousentryproduct + sto_an_step_previousentryproduct * sto_bn_step_previousentryproduct) + sto_cn_step_previousentryproduct = (sto_ap_step_previousentryproduct * sto_bn_step_previousentryproduct + sto_an_step_previousentryproduct * sto_bp_step_previousentryproduct) + sto_cp_step_previousentryproduct))))))))))))))) \/ ((((dc_index_step_previous)=0 \/ ~(exists pvs_factor_step_previousentrynondivisor. (S k) = (dc_index_step_previous) * pvs_factor_step_previousentrynondivisor)) /\ ((dc_value_step_previous)=0))))))) -> (exists dst_positive_code_step_remainder dst_positive_scale_step_remainder dst_negative_code_step_remainder dst_negative_scale_step_remainder dst_positive_sum_step_remainder dst_negative_sum_step_remainder. (((M) = (((((dst_positive_code_step_remainder) + (dst_positive_scale_step_remainder)) * S ((dst_positive_code_step_remainder) + (dst_positive_scale_step_remainder)) + ((dst_positive_scale_step_remainder) + (dst_positive_scale_step_remainder))) + (((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) * S ((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) + ((dst_negative_scale_step_remainder) + (dst_negative_scale_step_remainder)))) * S ((((dst_positive_code_step_remainder) + (dst_positive_scale_step_remainder)) * S ((dst_positive_code_step_remainder) + (dst_positive_scale_step_remainder)) + ((dst_positive_scale_step_remainder) + (dst_positive_scale_step_remainder))) + (((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) * S ((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) + ((dst_negative_scale_step_remainder) + (dst_negative_scale_step_remainder)))) + ((((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) * S ((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) + ((dst_negative_scale_step_remainder) + (dst_negative_scale_step_remainder))) + (((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) * S ((dst_negative_code_step_remainder) + (dst_negative_scale_step_remainder)) + ((dst_negative_scale_step_remainder) + (dst_negative_scale_step_remainder)))))) /\ (((exists fs_u_dst_step_remainderpositive fs_v_dst_step_remainderpositive. ((((exists fs_h_dst_step_remainderpositive_body_start. fs_h_dst_step_remainderpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_step_remainderpositive)) /\ exists fs_q_dst_step_remainderpositive_body_start. fs_u_dst_step_remainderpositive = fs_q_dst_step_remainderpositive_body_start * S ((S (0)) * fs_v_dst_step_remainderpositive) + (0))) /\ ((((exists fs_h_dst_step_remainderpositive_body_terminal. fs_h_dst_step_remainderpositive_body_terminal + S (dst_positive_sum_step_remainder) = S ((S (S k)) * fs_v_dst_step_remainderpositive)) /\ exists fs_q_dst_step_remainderpositive_body_terminal. fs_u_dst_step_remainderpositive = fs_q_dst_step_remainderpositive_body_terminal * S ((S (S k)) * fs_v_dst_step_remainderpositive) + (dst_positive_sum_step_remainder))) /\ forall fs_i_dst_step_remainderpositive_body_steps. (exists fs_lt_dst_step_remainderpositive_body_steps_bound. fs_lt_dst_step_remainderpositive_body_steps_bound + S fs_i_dst_step_remainderpositive_body_steps = S k) -> exists fs_a_dst_step_remainderpositive_body_steps fs_r_dst_step_remainderpositive_body_steps fs_s_dst_step_remainderpositive_body_steps. ((((exists fs_h_dst_step_remainderpositive_body_steps_summand. fs_h_dst_step_remainderpositive_body_steps_summand + S (fs_a_dst_step_remainderpositive_body_steps) = S ((S (fs_i_dst_step_remainderpositive_body_steps)) * dst_positive_scale_step_remainder)) /\ exists fs_q_dst_step_remainderpositive_body_steps_summand. dst_positive_code_step_remainder = fs_q_dst_step_remainderpositive_body_steps_summand * S ((S (fs_i_dst_step_remainderpositive_body_steps)) * dst_positive_scale_step_remainder) + (fs_a_dst_step_remainderpositive_body_steps))) /\ ((((exists fs_h_dst_step_remainderpositive_body_steps_partial. fs_h_dst_step_remainderpositive_body_steps_partial + S (fs_r_dst_step_remainderpositive_body_steps) = S ((S (fs_i_dst_step_remainderpositive_body_steps)) * fs_v_dst_step_remainderpositive)) /\ exists fs_q_dst_step_remainderpositive_body_steps_partial. fs_u_dst_step_remainderpositive = fs_q_dst_step_remainderpositive_body_steps_partial * S ((S (fs_i_dst_step_remainderpositive_body_steps)) * fs_v_dst_step_remainderpositive) + (fs_r_dst_step_remainderpositive_body_steps))) /\ ((((exists fs_h_dst_step_remainderpositive_body_steps_successor. fs_h_dst_step_remainderpositive_body_steps_successor + S (fs_s_dst_step_remainderpositive_body_steps) = S ((S (S fs_i_dst_step_remainderpositive_body_steps)) * fs_v_dst_step_remainderpositive)) /\ exists fs_q_dst_step_remainderpositive_body_steps_successor. fs_u_dst_step_remainderpositive = fs_q_dst_step_remainderpositive_body_steps_successor * S ((S (S fs_i_dst_step_remainderpositive_body_steps)) * fs_v_dst_step_remainderpositive) + (fs_s_dst_step_remainderpositive_body_steps))) /\ fs_s_dst_step_remainderpositive_body_steps = fs_r_dst_step_remainderpositive_body_steps + fs_a_dst_step_remainderpositive_body_steps)))))) /\ (((exists fs_u_dst_step_remaindernegative fs_v_dst_step_remaindernegative. ((((exists fs_h_dst_step_remaindernegative_body_start. fs_h_dst_step_remaindernegative_body_start + S (0) = S ((S (0)) * fs_v_dst_step_remaindernegative)) /\ exists fs_q_dst_step_remaindernegative_body_start. fs_u_dst_step_remaindernegative = fs_q_dst_step_remaindernegative_body_start * S ((S (0)) * fs_v_dst_step_remaindernegative) + (0))) /\ ((((exists fs_h_dst_step_remaindernegative_body_terminal. fs_h_dst_step_remaindernegative_body_terminal + S (dst_negative_sum_step_remainder) = S ((S (S k)) * fs_v_dst_step_remaindernegative)) /\ exists fs_q_dst_step_remaindernegative_body_terminal. fs_u_dst_step_remaindernegative = fs_q_dst_step_remaindernegative_body_terminal * S ((S (S k)) * fs_v_dst_step_remaindernegative) + (dst_negative_sum_step_remainder))) /\ forall fs_i_dst_step_remaindernegative_body_steps. (exists fs_lt_dst_step_remaindernegative_body_steps_bound. fs_lt_dst_step_remaindernegative_body_steps_bound + S fs_i_dst_step_remaindernegative_body_steps = S k) -> exists fs_a_dst_step_remaindernegative_body_steps fs_r_dst_step_remaindernegative_body_steps fs_s_dst_step_remaindernegative_body_steps. ((((exists fs_h_dst_step_remaindernegative_body_steps_summand. fs_h_dst_step_remaindernegative_body_steps_summand + S (fs_a_dst_step_remaindernegative_body_steps) = S ((S (fs_i_dst_step_remaindernegative_body_steps)) * dst_negative_scale_step_remainder)) /\ exists fs_q_dst_step_remaindernegative_body_steps_summand. dst_negative_code_step_remainder = fs_q_dst_step_remaindernegative_body_steps_summand * S ((S (fs_i_dst_step_remaindernegative_body_steps)) * dst_negative_scale_step_remainder) + (fs_a_dst_step_remaindernegative_body_steps))) /\ ((((exists fs_h_dst_step_remaindernegative_body_steps_partial. fs_h_dst_step_remaindernegative_body_steps_partial + S (fs_r_dst_step_remaindernegative_body_steps) = S ((S (fs_i_dst_step_remaindernegative_body_steps)) * fs_v_dst_step_remaindernegative)) /\ exists fs_q_dst_step_remaindernegative_body_steps_partial. fs_u_dst_step_remaindernegative = fs_q_dst_step_remaindernegative_body_steps_partial * S ((S (fs_i_dst_step_remaindernegative_body_steps)) * fs_v_dst_step_remaindernegative) + (fs_r_dst_step_remaindernegative_body_steps))) /\ ((((exists fs_h_dst_step_remaindernegative_body_steps_successor. fs_h_dst_step_remaindernegative_body_steps_successor + S (fs_s_dst_step_remaindernegative_body_steps) = S ((S (S fs_i_dst_step_remaindernegative_body_steps)) * fs_v_dst_step_remaindernegative)) /\ exists fs_q_dst_step_remaindernegative_body_steps_successor. fs_u_dst_step_remaindernegative = fs_q_dst_step_remaindernegative_body_steps_successor * S ((S (S fs_i_dst_step_remaindernegative_body_steps)) * fs_v_dst_step_remaindernegative) + (fs_s_dst_step_remaindernegative_body_steps))) /\ fs_s_dst_step_remaindernegative_body_steps = fs_r_dst_step_remaindernegative_body_steps + fs_a_dst_step_remaindernegative_body_steps)))))) /\ (exists ge_balance_positive_step_remainderresult ge_balance_negative_step_remainderresult. (((((r) = 2 * (ge_balance_positive_step_remainderresult) /\ (ge_balance_negative_step_remainderresult) = 0) \/ exists ge_signed_half_step_remainderresultdecode. (((r) = 2 * ge_signed_half_step_remainderresultdecode + 1 /\ (ge_balance_positive_step_remainderresult) = 0) /\ (ge_balance_negative_step_remainderresult) = S ge_signed_half_step_remainderresultdecode))) /\ ((dst_positive_sum_step_remainder) + ge_balance_negative_step_remainderresult = (dst_negative_sum_step_remainder) + ge_balance_positive_step_remainderresult))))))))) -> (exists dst_positive_code_step_first dst_positive_scale_step_first dst_negative_code_step_first dst_negative_scale_step_first dst_positive_step_first dst_negative_step_first. (((F) = (((((dst_positive_code_step_first) + (dst_positive_scale_step_first)) * S ((dst_positive_code_step_first) + (dst_positive_scale_step_first)) + ((dst_positive_scale_step_first) + (dst_positive_scale_step_first))) + (((dst_negative_code_step_first) + (dst_negative_scale_step_first)) * S ((dst_negative_code_step_first) + (dst_negative_scale_step_first)) + ((dst_negative_scale_step_first) + (dst_negative_scale_step_first)))) * S ((((dst_positive_code_step_first) + (dst_positive_scale_step_first)) * S ((dst_positive_code_step_first) + (dst_positive_scale_step_first)) + ((dst_positive_scale_step_first) + (dst_positive_scale_step_first))) + (((dst_negative_code_step_first) + (dst_negative_scale_step_first)) * S ((dst_negative_code_step_first) + (dst_negative_scale_step_first)) + ((dst_negative_scale_step_first) + (dst_negative_scale_step_first)))) + ((((dst_negative_code_step_first) + (dst_negative_scale_step_first)) * S ((dst_negative_code_step_first) + (dst_negative_scale_step_first)) + ((dst_negative_scale_step_first) + (dst_negative_scale_step_first))) + (((dst_negative_code_step_first) + (dst_negative_scale_step_first)) * S ((dst_negative_code_step_first) + (dst_negative_scale_step_first)) + ((dst_negative_scale_step_first) + (dst_negative_scale_step_first)))))) /\ (((((exists ff_h_pvs_step_firstpositive. ff_h_pvs_step_firstpositive + S (dst_positive_step_first) = S ((S (S k)) * dst_positive_scale_step_first)) /\ exists ff_q_pvs_step_firstpositive. dst_positive_code_step_first = ff_q_pvs_step_firstpositive * S ((S (S k)) * dst_positive_scale_step_first) + (dst_positive_step_first))) /\ (((((exists ff_h_pvs_step_firstnegative. ff_h_pvs_step_firstnegative + S (dst_negative_step_first) = S ((S (S k)) * dst_negative_scale_step_first)) /\ exists ff_q_pvs_step_firstnegative. dst_negative_code_step_first = ff_q_pvs_step_firstnegative * S ((S (S k)) * dst_negative_scale_step_first) + (dst_negative_step_first))) /\ (exists ge_balance_positive_step_firstvalue ge_balance_negative_step_firstvalue. (((((a) = 2 * (ge_balance_positive_step_firstvalue) /\ (ge_balance_negative_step_firstvalue) = 0) \/ exists ge_signed_half_step_firstvaluedecode. (((a) = 2 * ge_signed_half_step_firstvaluedecode + 1 /\ (ge_balance_positive_step_firstvalue) = 0) /\ (ge_balance_negative_step_firstvalue) = S ge_signed_half_step_firstvaluedecode))) /\ ((dst_positive_step_first) + ge_balance_negative_step_firstvalue = (dst_negative_step_first) + ge_balance_positive_step_firstvalue))))))))) -> (exists dst_positive_code_step_second dst_positive_scale_step_second dst_negative_code_step_second dst_negative_scale_step_second dst_positive_step_second dst_negative_step_second. (((G) = (((((dst_positive_code_step_second) + (dst_positive_scale_step_second)) * S ((dst_positive_code_step_second) + (dst_positive_scale_step_second)) + ((dst_positive_scale_step_second) + (dst_positive_scale_step_second))) + (((dst_negative_code_step_second) + (dst_negative_scale_step_second)) * S ((dst_negative_code_step_second) + (dst_negative_scale_step_second)) + ((dst_negative_scale_step_second) + (dst_negative_scale_step_second)))) * S ((((dst_positive_code_step_second) + (dst_positive_scale_step_second)) * S ((dst_positive_code_step_second) + (dst_positive_scale_step_second)) + ((dst_positive_scale_step_second) + (dst_positive_scale_step_second))) + (((dst_negative_code_step_second) + (dst_negative_scale_step_second)) * S ((dst_negative_code_step_second) + (dst_negative_scale_step_second)) + ((dst_negative_scale_step_second) + (dst_negative_scale_step_second)))) + ((((dst_negative_code_step_second) + (dst_negative_scale_step_second)) * S ((dst_negative_code_step_second) + (dst_negative_scale_step_second)) + ((dst_negative_scale_step_second) + (dst_negative_scale_step_second))) + (((dst_negative_code_step_second) + (dst_negative_scale_step_second)) * S ((dst_negative_code_step_second) + (dst_negative_scale_step_second)) + ((dst_negative_scale_step_second) + (dst_negative_scale_step_second)))))) /\ (((((exists ff_h_pvs_step_secondpositive. ff_h_pvs_step_secondpositive + S (dst_positive_step_second) = S ((S (1)) * dst_positive_scale_step_second)) /\ exists ff_q_pvs_step_secondpositive. dst_positive_code_step_second = ff_q_pvs_step_secondpositive * S ((S (1)) * dst_positive_scale_step_second) + (dst_positive_step_second))) /\ (((((exists ff_h_pvs_step_secondnegative. ff_h_pvs_step_secondnegative + S (dst_negative_step_second) = S ((S (1)) * dst_negative_scale_step_second)) /\ exists ff_q_pvs_step_secondnegative. dst_negative_code_step_second = ff_q_pvs_step_secondnegative * S ((S (1)) * dst_negative_scale_step_second) + (dst_negative_step_second))) /\ (exists ge_balance_positive_step_secondvalue ge_balance_negative_step_secondvalue. (((((b) = 2 * (ge_balance_positive_step_secondvalue) /\ (ge_balance_negative_step_secondvalue) = 0) \/ exists ge_signed_half_step_secondvaluedecode. (((b) = 2 * ge_signed_half_step_secondvaluedecode + 1 /\ (ge_balance_positive_step_secondvalue) = 0) /\ (ge_balance_negative_step_secondvalue) = S ge_signed_half_step_secondvaluedecode))) /\ ((dst_positive_step_second) + ge_balance_negative_step_secondvalue = (dst_negative_step_second) + ge_balance_positive_step_secondvalue))))))))) -> (exists sto_ap_step_product sto_an_step_product sto_bp_step_product sto_bn_step_product sto_cp_step_product sto_cn_step_product. (((((a) = 2 * (sto_ap_step_product) /\ (sto_an_step_product) = 0) \/ exists ge_signed_half_step_productleft. (((a) = 2 * ge_signed_half_step_productleft + 1 /\ (sto_ap_step_product) = 0) /\ (sto_an_step_product) = S ge_signed_half_step_productleft))) /\ ((((((b) = 2 * (sto_bp_step_product) /\ (sto_bn_step_product) = 0) \/ exists ge_signed_half_step_productright. (((b) = 2 * ge_signed_half_step_productright + 1 /\ (sto_bp_step_product) = 0) /\ (sto_bn_step_product) = S ge_signed_half_step_productright))) /\ ((((((y) = 2 * (sto_cp_step_product) /\ (sto_cn_step_product) = 0) \/ exists ge_signed_half_step_productoutput. (((y) = 2 * ge_signed_half_step_productoutput + 1 /\ (sto_cp_step_product) = 0) /\ (sto_cn_step_product) = S ge_signed_half_step_productoutput))) /\ ((sto_ap_step_product * sto_bp_step_product + sto_an_step_product * sto_bn_step_product) + sto_cn_step_product = (sto_ap_step_product * sto_bn_step_product + sto_an_step_product * sto_bp_step_product) + sto_cp_step_product))))))) -> (exists dsa_ap_step_add dsa_an_step_add dsa_bp_step_add dsa_bn_step_add dsa_cp_step_add dsa_cn_step_add. (((((r) = 2 * (dsa_ap_step_add) /\ (dsa_an_step_add) = 0) \/ exists ge_signed_half_step_addleft. (((r) = 2 * ge_signed_half_step_addleft + 1 /\ (dsa_ap_step_add) = 0) /\ (dsa_an_step_add) = S ge_signed_half_step_addleft))) /\ ((((((y) = 2 * (dsa_bp_step_add) /\ (dsa_bn_step_add) = 0) \/ exists ge_signed_half_step_addright. (((y) = 2 * ge_signed_half_step_addright + 1 /\ (dsa_bp_step_add) = 0) /\ (dsa_bn_step_add) = S ge_signed_half_step_addright))) /\ ((((((z) = 2 * (dsa_cp_step_add) /\ (dsa_cn_step_add) = 0) \/ exists ge_signed_half_step_addoutput. (((z) = 2 * ge_signed_half_step_addoutput + 1 /\ (dsa_cp_step_add) = 0) /\ (dsa_cn_step_add) = S ge_signed_half_step_addoutput))) /\ ((dsa_ap_step_add + dsa_bp_step_add) + dsa_cn_step_add = (dsa_an_step_add + dsa_bn_step_add) + dsa_cp_step_add))))))) -> (((~((S k)=0)) /\ (exists dc_mask_step_result. ((((exists dst_positive_code_step_resultmasktable dst_positive_scale_step_resultmasktable dst_negative_code_step_resultmasktable dst_negative_scale_step_resultmasktable. (((dc_mask_step_result) = (((((dst_positive_code_step_resultmasktable) + (dst_positive_scale_step_resultmasktable)) * S ((dst_positive_code_step_resultmasktable) + (dst_positive_scale_step_resultmasktable)) + ((dst_positive_scale_step_resultmasktable) + (dst_positive_scale_step_resultmasktable))) + (((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) * S ((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) + ((dst_negative_scale_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)))) * S ((((dst_positive_code_step_resultmasktable) + (dst_positive_scale_step_resultmasktable)) * S ((dst_positive_code_step_resultmasktable) + (dst_positive_scale_step_resultmasktable)) + ((dst_positive_scale_step_resultmasktable) + (dst_positive_scale_step_resultmasktable))) + (((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) * S ((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) + ((dst_negative_scale_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)))) + ((((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) * S ((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) + ((dst_negative_scale_step_resultmasktable) + (dst_negative_scale_step_resultmasktable))) + (((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) * S ((dst_negative_code_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)) + ((dst_negative_scale_step_resultmasktable) + (dst_negative_scale_step_resultmasktable)))))) /\ (forall dst_index_step_resultmasktable. (exists pvs_le_gap_step_resultmasktabledomain. pvs_le_gap_step_resultmasktabledomain + (dst_index_step_resultmasktable) = (S k)) -> exists dst_positive_step_resultmasktable dst_negative_step_resultmasktable dst_value_step_resultmasktable. ((((exists ff_h_pvs_step_resultmasktableentrypositive. ff_h_pvs_step_resultmasktableentrypositive + S (dst_positive_step_resultmasktable) = S ((S (dst_index_step_resultmasktable)) * dst_positive_scale_step_resultmasktable)) /\ exists ff_q_pvs_step_resultmasktableentrypositive. dst_positive_code_step_resultmasktable = ff_q_pvs_step_resultmasktableentrypositive * S ((S (dst_index_step_resultmasktable)) * dst_positive_scale_step_resultmasktable) + (dst_positive_step_resultmasktable))) /\ (((((exists ff_h_pvs_step_resultmasktableentrynegative. ff_h_pvs_step_resultmasktableentrynegative + S (dst_negative_step_resultmasktable) = S ((S (dst_index_step_resultmasktable)) * dst_negative_scale_step_resultmasktable)) /\ exists ff_q_pvs_step_resultmasktableentrynegative. dst_negative_code_step_resultmasktable = ff_q_pvs_step_resultmasktableentrynegative * S ((S (dst_index_step_resultmasktable)) * dst_negative_scale_step_resultmasktable) + (dst_negative_step_resultmasktable))) /\ (exists ge_balance_positive_step_resultmasktableentryvalue ge_balance_negative_step_resultmasktableentryvalue. (((((dst_value_step_resultmasktable) = 2 * (ge_balance_positive_step_resultmasktableentryvalue) /\ (ge_balance_negative_step_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_step_resultmasktableentryvaluedecode. (((dst_value_step_resultmasktable) = 2 * ge_signed_half_step_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_step_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_step_resultmasktableentryvalue) = S ge_signed_half_step_resultmasktableentryvaluedecode))) /\ ((dst_positive_step_resultmasktable) + ge_balance_negative_step_resultmasktableentryvalue = (dst_negative_step_resultmasktable) + ge_balance_positive_step_resultmasktableentryvalue))))))))) /\ (forall dc_index_step_resultmask dc_value_step_resultmask. (exists pvs_le_gap_step_resultmaskdomain. pvs_le_gap_step_resultmaskdomain + (dc_index_step_resultmask) = (S k)) -> (exists dst_positive_code_step_resultmasklookup dst_positive_scale_step_resultmasklookup dst_negative_code_step_resultmasklookup dst_negative_scale_step_resultmasklookup dst_positive_step_resultmasklookup dst_negative_step_resultmasklookup. (((dc_mask_step_result) = (((((dst_positive_code_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup)) * S ((dst_positive_code_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup)) + ((dst_positive_scale_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup))) + (((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) * S ((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) + ((dst_negative_scale_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)))) * S ((((dst_positive_code_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup)) * S ((dst_positive_code_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup)) + ((dst_positive_scale_step_resultmasklookup) + (dst_positive_scale_step_resultmasklookup))) + (((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) * S ((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) + ((dst_negative_scale_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)))) + ((((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) * S ((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) + ((dst_negative_scale_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup))) + (((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) * S ((dst_negative_code_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)) + ((dst_negative_scale_step_resultmasklookup) + (dst_negative_scale_step_resultmasklookup)))))) /\ (((((exists ff_h_pvs_step_resultmasklookuppositive. ff_h_pvs_step_resultmasklookuppositive + S (dst_positive_step_resultmasklookup) = S ((S (dc_index_step_resultmask)) * dst_positive_scale_step_resultmasklookup)) /\ exists ff_q_pvs_step_resultmasklookuppositive. dst_positive_code_step_resultmasklookup = ff_q_pvs_step_resultmasklookuppositive * S ((S (dc_index_step_resultmask)) * dst_positive_scale_step_resultmasklookup) + (dst_positive_step_resultmasklookup))) /\ (((((exists ff_h_pvs_step_resultmasklookupnegative. ff_h_pvs_step_resultmasklookupnegative + S (dst_negative_step_resultmasklookup) = S ((S (dc_index_step_resultmask)) * dst_negative_scale_step_resultmasklookup)) /\ exists ff_q_pvs_step_resultmasklookupnegative. dst_negative_code_step_resultmasklookup = ff_q_pvs_step_resultmasklookupnegative * S ((S (dc_index_step_resultmask)) * dst_negative_scale_step_resultmasklookup) + (dst_negative_step_resultmasklookup))) /\ (exists ge_balance_positive_step_resultmasklookupvalue ge_balance_negative_step_resultmasklookupvalue. (((((dc_value_step_resultmask) = 2 * (ge_balance_positive_step_resultmasklookupvalue) /\ (ge_balance_negative_step_resultmasklookupvalue) = 0) \/ exists ge_signed_half_step_resultmasklookupvaluedecode. (((dc_value_step_resultmask) = 2 * ge_signed_half_step_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_step_resultmasklookupvalue) = 0) /\ (ge_balance_negative_step_resultmasklookupvalue) = S ge_signed_half_step_resultmasklookupvaluedecode))) /\ ((dst_positive_step_resultmasklookup) + ge_balance_negative_step_resultmasklookupvalue = (dst_negative_step_resultmasklookup) + ge_balance_positive_step_resultmasklookupvalue))))))))) -> ((((~((dc_index_step_resultmask)=0)) /\ (exists dc_quotient_step_resultmaskentry dc_left_step_resultmaskentry dc_right_step_resultmaskentry. (((S k)=(dc_index_step_resultmask)*dc_quotient_step_resultmaskentry) /\ (((exists dst_positive_code_step_resultmaskentryleft dst_positive_scale_step_resultmaskentryleft dst_negative_code_step_resultmaskentryleft dst_negative_scale_step_resultmaskentryleft dst_positive_step_resultmaskentryleft dst_negative_step_resultmaskentryleft. (((F) = (((((dst_positive_code_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft)) * S ((dst_positive_code_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft)) + ((dst_positive_scale_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft))) + (((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) * S ((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) + ((dst_negative_scale_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)))) * S ((((dst_positive_code_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft)) * S ((dst_positive_code_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft)) + ((dst_positive_scale_step_resultmaskentryleft) + (dst_positive_scale_step_resultmaskentryleft))) + (((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) * S ((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) + ((dst_negative_scale_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)))) + ((((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) * S ((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) + ((dst_negative_scale_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft))) + (((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) * S ((dst_negative_code_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)) + ((dst_negative_scale_step_resultmaskentryleft) + (dst_negative_scale_step_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_step_resultmaskentryleftpositive. ff_h_pvs_step_resultmaskentryleftpositive + S (dst_positive_step_resultmaskentryleft) = S ((S (dc_index_step_resultmask)) * dst_positive_scale_step_resultmaskentryleft)) /\ exists ff_q_pvs_step_resultmaskentryleftpositive. dst_positive_code_step_resultmaskentryleft = ff_q_pvs_step_resultmaskentryleftpositive * S ((S (dc_index_step_resultmask)) * dst_positive_scale_step_resultmaskentryleft) + (dst_positive_step_resultmaskentryleft))) /\ (((((exists ff_h_pvs_step_resultmaskentryleftnegative. ff_h_pvs_step_resultmaskentryleftnegative + S (dst_negative_step_resultmaskentryleft) = S ((S (dc_index_step_resultmask)) * dst_negative_scale_step_resultmaskentryleft)) /\ exists ff_q_pvs_step_resultmaskentryleftnegative. dst_negative_code_step_resultmaskentryleft = ff_q_pvs_step_resultmaskentryleftnegative * S ((S (dc_index_step_resultmask)) * dst_negative_scale_step_resultmaskentryleft) + (dst_negative_step_resultmaskentryleft))) /\ (exists ge_balance_positive_step_resultmaskentryleftvalue ge_balance_negative_step_resultmaskentryleftvalue. (((((dc_left_step_resultmaskentry) = 2 * (ge_balance_positive_step_resultmaskentryleftvalue) /\ (ge_balance_negative_step_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_step_resultmaskentryleftvaluedecode. (((dc_left_step_resultmaskentry) = 2 * ge_signed_half_step_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_step_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_step_resultmaskentryleftvalue) = S ge_signed_half_step_resultmaskentryleftvaluedecode))) /\ ((dst_positive_step_resultmaskentryleft) + ge_balance_negative_step_resultmaskentryleftvalue = (dst_negative_step_resultmaskentryleft) + ge_balance_positive_step_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_step_resultmaskentryright dst_positive_scale_step_resultmaskentryright dst_negative_code_step_resultmaskentryright dst_negative_scale_step_resultmaskentryright dst_positive_step_resultmaskentryright dst_negative_step_resultmaskentryright. (((G) = (((((dst_positive_code_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright)) * S ((dst_positive_code_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright)) + ((dst_positive_scale_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright))) + (((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) * S ((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) + ((dst_negative_scale_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)))) * S ((((dst_positive_code_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright)) * S ((dst_positive_code_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright)) + ((dst_positive_scale_step_resultmaskentryright) + (dst_positive_scale_step_resultmaskentryright))) + (((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) * S ((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) + ((dst_negative_scale_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)))) + ((((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) * S ((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) + ((dst_negative_scale_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright))) + (((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) * S ((dst_negative_code_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)) + ((dst_negative_scale_step_resultmaskentryright) + (dst_negative_scale_step_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_step_resultmaskentryrightpositive. ff_h_pvs_step_resultmaskentryrightpositive + S (dst_positive_step_resultmaskentryright) = S ((S (dc_quotient_step_resultmaskentry)) * dst_positive_scale_step_resultmaskentryright)) /\ exists ff_q_pvs_step_resultmaskentryrightpositive. dst_positive_code_step_resultmaskentryright = ff_q_pvs_step_resultmaskentryrightpositive * S ((S (dc_quotient_step_resultmaskentry)) * dst_positive_scale_step_resultmaskentryright) + (dst_positive_step_resultmaskentryright))) /\ (((((exists ff_h_pvs_step_resultmaskentryrightnegative. ff_h_pvs_step_resultmaskentryrightnegative + S (dst_negative_step_resultmaskentryright) = S ((S (dc_quotient_step_resultmaskentry)) * dst_negative_scale_step_resultmaskentryright)) /\ exists ff_q_pvs_step_resultmaskentryrightnegative. dst_negative_code_step_resultmaskentryright = ff_q_pvs_step_resultmaskentryrightnegative * S ((S (dc_quotient_step_resultmaskentry)) * dst_negative_scale_step_resultmaskentryright) + (dst_negative_step_resultmaskentryright))) /\ (exists ge_balance_positive_step_resultmaskentryrightvalue ge_balance_negative_step_resultmaskentryrightvalue. (((((dc_right_step_resultmaskentry) = 2 * (ge_balance_positive_step_resultmaskentryrightvalue) /\ (ge_balance_negative_step_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_step_resultmaskentryrightvaluedecode. (((dc_right_step_resultmaskentry) = 2 * ge_signed_half_step_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_step_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_step_resultmaskentryrightvalue) = S ge_signed_half_step_resultmaskentryrightvaluedecode))) /\ ((dst_positive_step_resultmaskentryright) + ge_balance_negative_step_resultmaskentryrightvalue = (dst_negative_step_resultmaskentryright) + ge_balance_positive_step_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_step_resultmaskentryproduct sto_an_step_resultmaskentryproduct sto_bp_step_resultmaskentryproduct sto_bn_step_resultmaskentryproduct sto_cp_step_resultmaskentryproduct sto_cn_step_resultmaskentryproduct. (((((dc_left_step_resultmaskentry) = 2 * (sto_ap_step_resultmaskentryproduct) /\ (sto_an_step_resultmaskentryproduct) = 0) \/ exists ge_signed_half_step_resultmaskentryproductleft. (((dc_left_step_resultmaskentry) = 2 * ge_signed_half_step_resultmaskentryproductleft + 1 /\ (sto_ap_step_resultmaskentryproduct) = 0) /\ (sto_an_step_resultmaskentryproduct) = S ge_signed_half_step_resultmaskentryproductleft))) /\ ((((((dc_right_step_resultmaskentry) = 2 * (sto_bp_step_resultmaskentryproduct) /\ (sto_bn_step_resultmaskentryproduct) = 0) \/ exists ge_signed_half_step_resultmaskentryproductright. (((dc_right_step_resultmaskentry) = 2 * ge_signed_half_step_resultmaskentryproductright + 1 /\ (sto_bp_step_resultmaskentryproduct) = 0) /\ (sto_bn_step_resultmaskentryproduct) = S ge_signed_half_step_resultmaskentryproductright))) /\ ((((((dc_value_step_resultmask) = 2 * (sto_cp_step_resultmaskentryproduct) /\ (sto_cn_step_resultmaskentryproduct) = 0) \/ exists ge_signed_half_step_resultmaskentryproductoutput. (((dc_value_step_resultmask) = 2 * ge_signed_half_step_resultmaskentryproductoutput + 1 /\ (sto_cp_step_resultmaskentryproduct) = 0) /\ (sto_cn_step_resultmaskentryproduct) = S ge_signed_half_step_resultmaskentryproductoutput))) /\ ((sto_ap_step_resultmaskentryproduct * sto_bp_step_resultmaskentryproduct + sto_an_step_resultmaskentryproduct * sto_bn_step_resultmaskentryproduct) + sto_cn_step_resultmaskentryproduct = (sto_ap_step_resultmaskentryproduct * sto_bn_step_resultmaskentryproduct + sto_an_step_resultmaskentryproduct * sto_bp_step_resultmaskentryproduct) + sto_cp_step_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_step_resultmask)=0 \/ ~(exists pvs_factor_step_resultmaskentrynondivisor. (S k) = (dc_index_step_resultmask) * pvs_factor_step_resultmaskentrynondivisor)) /\ ((dc_value_step_resultmask)=0))))))) /\ (exists dst_positive_code_step_resultfold dst_positive_scale_step_resultfold dst_negative_code_step_resultfold dst_negative_scale_step_resultfold dst_positive_sum_step_resultfold dst_negative_sum_step_resultfold. (((dc_mask_step_result) = (((((dst_positive_code_step_resultfold) + (dst_positive_scale_step_resultfold)) * S ((dst_positive_code_step_resultfold) + (dst_positive_scale_step_resultfold)) + ((dst_positive_scale_step_resultfold) + (dst_positive_scale_step_resultfold))) + (((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) * S ((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) + ((dst_negative_scale_step_resultfold) + (dst_negative_scale_step_resultfold)))) * S ((((dst_positive_code_step_resultfold) + (dst_positive_scale_step_resultfold)) * S ((dst_positive_code_step_resultfold) + (dst_positive_scale_step_resultfold)) + ((dst_positive_scale_step_resultfold) + (dst_positive_scale_step_resultfold))) + (((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) * S ((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) + ((dst_negative_scale_step_resultfold) + (dst_negative_scale_step_resultfold)))) + ((((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) * S ((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) + ((dst_negative_scale_step_resultfold) + (dst_negative_scale_step_resultfold))) + (((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) * S ((dst_negative_code_step_resultfold) + (dst_negative_scale_step_resultfold)) + ((dst_negative_scale_step_resultfold) + (dst_negative_scale_step_resultfold)))))) /\ (((exists fs_u_dst_step_resultfoldpositive fs_v_dst_step_resultfoldpositive. ((((exists fs_h_dst_step_resultfoldpositive_body_start. fs_h_dst_step_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_step_resultfoldpositive)) /\ exists fs_q_dst_step_resultfoldpositive_body_start. fs_u_dst_step_resultfoldpositive = fs_q_dst_step_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_step_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_step_resultfoldpositive_body_terminal. fs_h_dst_step_resultfoldpositive_body_terminal + S (dst_positive_sum_step_resultfold) = S ((S (S (S k))) * fs_v_dst_step_resultfoldpositive)) /\ exists fs_q_dst_step_resultfoldpositive_body_terminal. fs_u_dst_step_resultfoldpositive = fs_q_dst_step_resultfoldpositive_body_terminal * S ((S (S (S k))) * fs_v_dst_step_resultfoldpositive) + (dst_positive_sum_step_resultfold))) /\ forall fs_i_dst_step_resultfoldpositive_body_steps. (exists fs_lt_dst_step_resultfoldpositive_body_steps_bound. fs_lt_dst_step_resultfoldpositive_body_steps_bound + S fs_i_dst_step_resultfoldpositive_body_steps = S (S k)) -> exists fs_a_dst_step_resultfoldpositive_body_steps fs_r_dst_step_resultfoldpositive_body_steps fs_s_dst_step_resultfoldpositive_body_steps. ((((exists fs_h_dst_step_resultfoldpositive_body_steps_summand. fs_h_dst_step_resultfoldpositive_body_steps_summand + S (fs_a_dst_step_resultfoldpositive_body_steps) = S ((S (fs_i_dst_step_resultfoldpositive_body_steps)) * dst_positive_scale_step_resultfold)) /\ exists fs_q_dst_step_resultfoldpositive_body_steps_summand. dst_positive_code_step_resultfold = fs_q_dst_step_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_step_resultfoldpositive_body_steps)) * dst_positive_scale_step_resultfold) + (fs_a_dst_step_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_step_resultfoldpositive_body_steps_partial. fs_h_dst_step_resultfoldpositive_body_steps_partial + S (fs_r_dst_step_resultfoldpositive_body_steps) = S ((S (fs_i_dst_step_resultfoldpositive_body_steps)) * fs_v_dst_step_resultfoldpositive)) /\ exists fs_q_dst_step_resultfoldpositive_body_steps_partial. fs_u_dst_step_resultfoldpositive = fs_q_dst_step_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_step_resultfoldpositive_body_steps)) * fs_v_dst_step_resultfoldpositive) + (fs_r_dst_step_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_step_resultfoldpositive_body_steps_successor. fs_h_dst_step_resultfoldpositive_body_steps_successor + S (fs_s_dst_step_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_step_resultfoldpositive_body_steps)) * fs_v_dst_step_resultfoldpositive)) /\ exists fs_q_dst_step_resultfoldpositive_body_steps_successor. fs_u_dst_step_resultfoldpositive = fs_q_dst_step_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_step_resultfoldpositive_body_steps)) * fs_v_dst_step_resultfoldpositive) + (fs_s_dst_step_resultfoldpositive_body_steps))) /\ fs_s_dst_step_resultfoldpositive_body_steps = fs_r_dst_step_resultfoldpositive_body_steps + fs_a_dst_step_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_step_resultfoldnegative fs_v_dst_step_resultfoldnegative. ((((exists fs_h_dst_step_resultfoldnegative_body_start. fs_h_dst_step_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_step_resultfoldnegative)) /\ exists fs_q_dst_step_resultfoldnegative_body_start. fs_u_dst_step_resultfoldnegative = fs_q_dst_step_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_step_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_step_resultfoldnegative_body_terminal. fs_h_dst_step_resultfoldnegative_body_terminal + S (dst_negative_sum_step_resultfold) = S ((S (S (S k))) * fs_v_dst_step_resultfoldnegative)) /\ exists fs_q_dst_step_resultfoldnegative_body_terminal. fs_u_dst_step_resultfoldnegative = fs_q_dst_step_resultfoldnegative_body_terminal * S ((S (S (S k))) * fs_v_dst_step_resultfoldnegative) + (dst_negative_sum_step_resultfold))) /\ forall fs_i_dst_step_resultfoldnegative_body_steps. (exists fs_lt_dst_step_resultfoldnegative_body_steps_bound. fs_lt_dst_step_resultfoldnegative_body_steps_bound + S fs_i_dst_step_resultfoldnegative_body_steps = S (S k)) -> exists fs_a_dst_step_resultfoldnegative_body_steps fs_r_dst_step_resultfoldnegative_body_steps fs_s_dst_step_resultfoldnegative_body_steps. ((((exists fs_h_dst_step_resultfoldnegative_body_steps_summand. fs_h_dst_step_resultfoldnegative_body_steps_summand + S (fs_a_dst_step_resultfoldnegative_body_steps) = S ((S (fs_i_dst_step_resultfoldnegative_body_steps)) * dst_negative_scale_step_resultfold)) /\ exists fs_q_dst_step_resultfoldnegative_body_steps_summand. dst_negative_code_step_resultfold = fs_q_dst_step_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_step_resultfoldnegative_body_steps)) * dst_negative_scale_step_resultfold) + (fs_a_dst_step_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_step_resultfoldnegative_body_steps_partial. fs_h_dst_step_resultfoldnegative_body_steps_partial + S (fs_r_dst_step_resultfoldnegative_body_steps) = S ((S (fs_i_dst_step_resultfoldnegative_body_steps)) * fs_v_dst_step_resultfoldnegative)) /\ exists fs_q_dst_step_resultfoldnegative_body_steps_partial. fs_u_dst_step_resultfoldnegative = fs_q_dst_step_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_step_resultfoldnegative_body_steps)) * fs_v_dst_step_resultfoldnegative) + (fs_r_dst_step_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_step_resultfoldnegative_body_steps_successor. fs_h_dst_step_resultfoldnegative_body_steps_successor + S (fs_s_dst_step_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_step_resultfoldnegative_body_steps)) * fs_v_dst_step_resultfoldnegative)) /\ exists fs_q_dst_step_resultfoldnegative_body_steps_successor. fs_u_dst_step_resultfoldnegative = fs_q_dst_step_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_step_resultfoldnegative_body_steps)) * fs_v_dst_step_resultfoldnegative) + (fs_s_dst_step_resultfoldnegative_body_steps))) /\ fs_s_dst_step_resultfoldnegative_body_steps = fs_r_dst_step_resultfoldnegative_body_steps + fs_a_dst_step_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_step_resultfoldresult ge_balance_negative_step_resultfoldresult. (((((z) = 2 * (ge_balance_positive_step_resultfoldresult) /\ (ge_balance_negative_step_resultfoldresult) = 0) \/ exists ge_signed_half_step_resultfoldresultdecode. (((z) = 2 * ge_signed_half_step_resultfoldresultdecode + 1 /\ (ge_balance_positive_step_resultfoldresult) = 0) /\ (ge_balance_negative_step_resultfoldresult) = S ge_signed_half_step_resultfoldresultdecode))) /\ ((dst_positive_sum_step_resultfold) + ge_balance_negative_step_resultfoldresult = (dst_negative_sum_step_resultfold) + ge_balance_positive_step_resultfoldresult)))))))))))))