arithmetic_signed_sum_append_transport

forall F G l a b c. (exists dst_positive_code_append_sum_valid dst_positive_scale_append_sum_valid dst_negative_code_append_sum_valid dst_negative_scale_append_sum_valid. (((G) = (((((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) * S ((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) + ((dst_positive_scale_append_sum_valid) + (dst_positive_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))) * S ((((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) * S ((dst_positive_code_append_sum_valid) + (dst_positive_scale_append_sum_valid)) + ((dst_positive_scale_append_sum_valid) + (dst_positive_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))) + ((((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid))) + (((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) * S ((dst_negative_code_append_sum_valid) + (dst_negative_scale_append_sum_valid)) + ((dst_negative_scale_append_sum_valid) + (dst_negative_scale_append_sum_valid)))))) /\ (forall dst_index_append_sum_valid. (exists pvs_le_gap_append_sum_validdomain. pvs_le_gap_append_sum_validdomain + (dst_index_append_sum_valid) = (l)) -> exists dst_positive_append_sum_valid dst_negative_append_sum_valid dst_value_append_sum_valid. ((((exists ff_h_pvs_append_sum_validentrypositive. ff_h_pvs_append_sum_validentrypositive + S (dst_positive_append_sum_valid) = S ((S (dst_index_append_sum_valid)) * dst_positive_scale_append_sum_valid)) /\ exists ff_q_pvs_append_sum_validentrypositive. dst_positive_code_append_sum_valid = ff_q_pvs_append_sum_validentrypositive * S ((S (dst_index_append_sum_valid)) * dst_positive_scale_append_sum_valid) + (dst_positive_append_sum_valid))) /\ (((((exists ff_h_pvs_append_sum_validentrynegative. ff_h_pvs_append_sum_validentrynegative + S (dst_negative_append_sum_valid) = S ((S (dst_index_append_sum_valid)) * dst_negative_scale_append_sum_valid)) /\ exists ff_q_pvs_append_sum_validentrynegative. dst_negative_code_append_sum_valid = ff_q_pvs_append_sum_validentrynegative * S ((S (dst_index_append_sum_valid)) * dst_negative_scale_append_sum_valid) + (dst_negative_append_sum_valid))) /\ (exists ge_balance_positive_append_sum_validentryvalue ge_balance_negative_append_sum_validentryvalue. (((((dst_value_append_sum_valid) = 2 * (ge_balance_positive_append_sum_validentryvalue) /\ (ge_balance_negative_append_sum_validentryvalue) = 0) \/ exists ge_signed_half_append_sum_validentryvaluedecode. (((dst_value_append_sum_valid) = 2 * ge_signed_half_append_sum_validentryvaluedecode + 1 /\ (ge_balance_positive_append_sum_validentryvalue) = 0) /\ (ge_balance_negative_append_sum_validentryvalue) = S ge_signed_half_append_sum_validentryvaluedecode))) /\ ((dst_positive_append_sum_valid) + ge_balance_negative_append_sum_validentryvalue = (dst_negative_append_sum_valid) + ge_balance_positive_append_sum_validentryvalue))))))))) -> (forall dst_index_append_sum_prefix dst_first_append_sum_prefix dst_second_append_sum_prefix. (exists pvs_gap_append_sum_prefixbound. pvs_gap_append_sum_prefixbound + S (dst_index_append_sum_prefix) = (l)) -> (exists dst_positive_code_append_sum_prefixfirst dst_positive_scale_append_sum_prefixfirst dst_negative_code_append_sum_prefixfirst dst_negative_scale_append_sum_prefixfirst dst_positive_append_sum_prefixfirst dst_negative_append_sum_prefixfirst. (((F) = (((((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) * S ((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) + ((dst_positive_scale_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))) * S ((((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) * S ((dst_positive_code_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst)) + ((dst_positive_scale_append_sum_prefixfirst) + (dst_positive_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))) + ((((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst))) + (((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) * S ((dst_negative_code_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)) + ((dst_negative_scale_append_sum_prefixfirst) + (dst_negative_scale_append_sum_prefixfirst)))))) /\ (((((exists ff_h_pvs_append_sum_prefixfirstpositive. ff_h_pvs_append_sum_prefixfirstpositive + S (dst_positive_append_sum_prefixfirst) = S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixfirst)) /\ exists ff_q_pvs_append_sum_prefixfirstpositive. dst_positive_code_append_sum_prefixfirst = ff_q_pvs_append_sum_prefixfirstpositive * S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixfirst) + (dst_positive_append_sum_prefixfirst))) /\ (((((exists ff_h_pvs_append_sum_prefixfirstnegative. ff_h_pvs_append_sum_prefixfirstnegative + S (dst_negative_append_sum_prefixfirst) = S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixfirst)) /\ exists ff_q_pvs_append_sum_prefixfirstnegative. dst_negative_code_append_sum_prefixfirst = ff_q_pvs_append_sum_prefixfirstnegative * S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixfirst) + (dst_negative_append_sum_prefixfirst))) /\ (exists ge_balance_positive_append_sum_prefixfirstvalue ge_balance_negative_append_sum_prefixfirstvalue. (((((dst_first_append_sum_prefix) = 2 * (ge_balance_positive_append_sum_prefixfirstvalue) /\ (ge_balance_negative_append_sum_prefixfirstvalue) = 0) \/ exists ge_signed_half_append_sum_prefixfirstvaluedecode. (((dst_first_append_sum_prefix) = 2 * ge_signed_half_append_sum_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_sum_prefixfirstvalue) = 0) /\ (ge_balance_negative_append_sum_prefixfirstvalue) = S ge_signed_half_append_sum_prefixfirstvaluedecode))) /\ ((dst_positive_append_sum_prefixfirst) + ge_balance_negative_append_sum_prefixfirstvalue = (dst_negative_append_sum_prefixfirst) + ge_balance_positive_append_sum_prefixfirstvalue))))))))) -> (exists dst_positive_code_append_sum_prefixsecond dst_positive_scale_append_sum_prefixsecond dst_negative_code_append_sum_prefixsecond dst_negative_scale_append_sum_prefixsecond dst_positive_append_sum_prefixsecond dst_negative_append_sum_prefixsecond. (((G) = (((((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) * S ((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) + ((dst_positive_scale_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))) * S ((((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) * S ((dst_positive_code_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond)) + ((dst_positive_scale_append_sum_prefixsecond) + (dst_positive_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))) + ((((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond))) + (((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) * S ((dst_negative_code_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)) + ((dst_negative_scale_append_sum_prefixsecond) + (dst_negative_scale_append_sum_prefixsecond)))))) /\ (((((exists ff_h_pvs_append_sum_prefixsecondpositive. ff_h_pvs_append_sum_prefixsecondpositive + S (dst_positive_append_sum_prefixsecond) = S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixsecond)) /\ exists ff_q_pvs_append_sum_prefixsecondpositive. dst_positive_code_append_sum_prefixsecond = ff_q_pvs_append_sum_prefixsecondpositive * S ((S (dst_index_append_sum_prefix)) * dst_positive_scale_append_sum_prefixsecond) + (dst_positive_append_sum_prefixsecond))) /\ (((((exists ff_h_pvs_append_sum_prefixsecondnegative. ff_h_pvs_append_sum_prefixsecondnegative + S (dst_negative_append_sum_prefixsecond) = S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixsecond)) /\ exists ff_q_pvs_append_sum_prefixsecondnegative. dst_negative_code_append_sum_prefixsecond = ff_q_pvs_append_sum_prefixsecondnegative * S ((S (dst_index_append_sum_prefix)) * dst_negative_scale_append_sum_prefixsecond) + (dst_negative_append_sum_prefixsecond))) /\ (exists ge_balance_positive_append_sum_prefixsecondvalue ge_balance_negative_append_sum_prefixsecondvalue. (((((dst_second_append_sum_prefix) = 2 * (ge_balance_positive_append_sum_prefixsecondvalue) /\ (ge_balance_negative_append_sum_prefixsecondvalue) = 0) \/ exists ge_signed_half_append_sum_prefixsecondvaluedecode. (((dst_second_append_sum_prefix) = 2 * ge_signed_half_append_sum_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_sum_prefixsecondvalue) = 0) /\ (ge_balance_negative_append_sum_prefixsecondvalue) = S ge_signed_half_append_sum_prefixsecondvaluedecode))) /\ ((dst_positive_append_sum_prefixsecond) + ge_balance_negative_append_sum_prefixsecondvalue = (dst_negative_append_sum_prefixsecond) + ge_balance_positive_append_sum_prefixsecondvalue))))))))) -> dst_first_append_sum_prefix = dst_second_append_sum_prefix) -> (exists dst_positive_code_append_sum_before dst_positive_scale_append_sum_before dst_negative_code_append_sum_before dst_negative_scale_append_sum_before dst_positive_sum_append_sum_before dst_negative_sum_append_sum_before. (((F) = (((((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) * S ((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) + ((dst_positive_scale_append_sum_before) + (dst_positive_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))) * S ((((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) * S ((dst_positive_code_append_sum_before) + (dst_positive_scale_append_sum_before)) + ((dst_positive_scale_append_sum_before) + (dst_positive_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))) + ((((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before))) + (((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) * S ((dst_negative_code_append_sum_before) + (dst_negative_scale_append_sum_before)) + ((dst_negative_scale_append_sum_before) + (dst_negative_scale_append_sum_before)))))) /\ (((exists fs_u_dst_append_sum_beforepositive fs_v_dst_append_sum_beforepositive. ((((exists fs_h_dst_append_sum_beforepositive_body_start. fs_h_dst_append_sum_beforepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_start. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_start * S ((S (0)) * fs_v_dst_append_sum_beforepositive) + (0))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_terminal. fs_h_dst_append_sum_beforepositive_body_terminal + S (dst_positive_sum_append_sum_before) = S ((S (l)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_terminal. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_terminal * S ((S (l)) * fs_v_dst_append_sum_beforepositive) + (dst_positive_sum_append_sum_before))) /\ forall fs_i_dst_append_sum_beforepositive_body_steps. (exists fs_lt_dst_append_sum_beforepositive_body_steps_bound. fs_lt_dst_append_sum_beforepositive_body_steps_bound + S fs_i_dst_append_sum_beforepositive_body_steps = l) -> exists fs_a_dst_append_sum_beforepositive_body_steps fs_r_dst_append_sum_beforepositive_body_steps fs_s_dst_append_sum_beforepositive_body_steps. ((((exists fs_h_dst_append_sum_beforepositive_body_steps_summand. fs_h_dst_append_sum_beforepositive_body_steps_summand + S (fs_a_dst_append_sum_beforepositive_body_steps) = S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * dst_positive_scale_append_sum_before)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_summand. dst_positive_code_append_sum_before = fs_q_dst_append_sum_beforepositive_body_steps_summand * S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * dst_positive_scale_append_sum_before) + (fs_a_dst_append_sum_beforepositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_steps_partial. fs_h_dst_append_sum_beforepositive_body_steps_partial + S (fs_r_dst_append_sum_beforepositive_body_steps) = S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_partial. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_steps_partial * S ((S (fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive) + (fs_r_dst_append_sum_beforepositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforepositive_body_steps_successor. fs_h_dst_append_sum_beforepositive_body_steps_successor + S (fs_s_dst_append_sum_beforepositive_body_steps) = S ((S (S fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive)) /\ exists fs_q_dst_append_sum_beforepositive_body_steps_successor. fs_u_dst_append_sum_beforepositive = fs_q_dst_append_sum_beforepositive_body_steps_successor * S ((S (S fs_i_dst_append_sum_beforepositive_body_steps)) * fs_v_dst_append_sum_beforepositive) + (fs_s_dst_append_sum_beforepositive_body_steps))) /\ fs_s_dst_append_sum_beforepositive_body_steps = fs_r_dst_append_sum_beforepositive_body_steps + fs_a_dst_append_sum_beforepositive_body_steps)))))) /\ (((exists fs_u_dst_append_sum_beforenegative fs_v_dst_append_sum_beforenegative. ((((exists fs_h_dst_append_sum_beforenegative_body_start. fs_h_dst_append_sum_beforenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_start. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_start * S ((S (0)) * fs_v_dst_append_sum_beforenegative) + (0))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_terminal. fs_h_dst_append_sum_beforenegative_body_terminal + S (dst_negative_sum_append_sum_before) = S ((S (l)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_terminal. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_terminal * S ((S (l)) * fs_v_dst_append_sum_beforenegative) + (dst_negative_sum_append_sum_before))) /\ forall fs_i_dst_append_sum_beforenegative_body_steps. (exists fs_lt_dst_append_sum_beforenegative_body_steps_bound. fs_lt_dst_append_sum_beforenegative_body_steps_bound + S fs_i_dst_append_sum_beforenegative_body_steps = l) -> exists fs_a_dst_append_sum_beforenegative_body_steps fs_r_dst_append_sum_beforenegative_body_steps fs_s_dst_append_sum_beforenegative_body_steps. ((((exists fs_h_dst_append_sum_beforenegative_body_steps_summand. fs_h_dst_append_sum_beforenegative_body_steps_summand + S (fs_a_dst_append_sum_beforenegative_body_steps) = S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * dst_negative_scale_append_sum_before)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_summand. dst_negative_code_append_sum_before = fs_q_dst_append_sum_beforenegative_body_steps_summand * S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * dst_negative_scale_append_sum_before) + (fs_a_dst_append_sum_beforenegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_steps_partial. fs_h_dst_append_sum_beforenegative_body_steps_partial + S (fs_r_dst_append_sum_beforenegative_body_steps) = S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_partial. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_steps_partial * S ((S (fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative) + (fs_r_dst_append_sum_beforenegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_beforenegative_body_steps_successor. fs_h_dst_append_sum_beforenegative_body_steps_successor + S (fs_s_dst_append_sum_beforenegative_body_steps) = S ((S (S fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative)) /\ exists fs_q_dst_append_sum_beforenegative_body_steps_successor. fs_u_dst_append_sum_beforenegative = fs_q_dst_append_sum_beforenegative_body_steps_successor * S ((S (S fs_i_dst_append_sum_beforenegative_body_steps)) * fs_v_dst_append_sum_beforenegative) + (fs_s_dst_append_sum_beforenegative_body_steps))) /\ fs_s_dst_append_sum_beforenegative_body_steps = fs_r_dst_append_sum_beforenegative_body_steps + fs_a_dst_append_sum_beforenegative_body_steps)))))) /\ (exists ge_balance_positive_append_sum_beforeresult ge_balance_negative_append_sum_beforeresult. (((((a) = 2 * (ge_balance_positive_append_sum_beforeresult) /\ (ge_balance_negative_append_sum_beforeresult) = 0) \/ exists ge_signed_half_append_sum_beforeresultdecode. (((a) = 2 * ge_signed_half_append_sum_beforeresultdecode + 1 /\ (ge_balance_positive_append_sum_beforeresult) = 0) /\ (ge_balance_negative_append_sum_beforeresult) = S ge_signed_half_append_sum_beforeresultdecode))) /\ ((dst_positive_sum_append_sum_before) + ge_balance_negative_append_sum_beforeresult = (dst_negative_sum_append_sum_before) + ge_balance_positive_append_sum_beforeresult))))))))) -> (exists dst_positive_code_append_sum_entry dst_positive_scale_append_sum_entry dst_negative_code_append_sum_entry dst_negative_scale_append_sum_entry dst_positive_append_sum_entry dst_negative_append_sum_entry. (((G) = (((((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) * S ((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) + ((dst_positive_scale_append_sum_entry) + (dst_positive_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))) * S ((((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) * S ((dst_positive_code_append_sum_entry) + (dst_positive_scale_append_sum_entry)) + ((dst_positive_scale_append_sum_entry) + (dst_positive_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))) + ((((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry))) + (((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) * S ((dst_negative_code_append_sum_entry) + (dst_negative_scale_append_sum_entry)) + ((dst_negative_scale_append_sum_entry) + (dst_negative_scale_append_sum_entry)))))) /\ (((((exists ff_h_pvs_append_sum_entrypositive. ff_h_pvs_append_sum_entrypositive + S (dst_positive_append_sum_entry) = S ((S (l)) * dst_positive_scale_append_sum_entry)) /\ exists ff_q_pvs_append_sum_entrypositive. dst_positive_code_append_sum_entry = ff_q_pvs_append_sum_entrypositive * S ((S (l)) * dst_positive_scale_append_sum_entry) + (dst_positive_append_sum_entry))) /\ (((((exists ff_h_pvs_append_sum_entrynegative. ff_h_pvs_append_sum_entrynegative + S (dst_negative_append_sum_entry) = S ((S (l)) * dst_negative_scale_append_sum_entry)) /\ exists ff_q_pvs_append_sum_entrynegative. dst_negative_code_append_sum_entry = ff_q_pvs_append_sum_entrynegative * S ((S (l)) * dst_negative_scale_append_sum_entry) + (dst_negative_append_sum_entry))) /\ (exists ge_balance_positive_append_sum_entryvalue ge_balance_negative_append_sum_entryvalue. (((((b) = 2 * (ge_balance_positive_append_sum_entryvalue) /\ (ge_balance_negative_append_sum_entryvalue) = 0) \/ exists ge_signed_half_append_sum_entryvaluedecode. (((b) = 2 * ge_signed_half_append_sum_entryvaluedecode + 1 /\ (ge_balance_positive_append_sum_entryvalue) = 0) /\ (ge_balance_negative_append_sum_entryvalue) = S ge_signed_half_append_sum_entryvaluedecode))) /\ ((dst_positive_append_sum_entry) + ge_balance_negative_append_sum_entryvalue = (dst_negative_append_sum_entry) + ge_balance_positive_append_sum_entryvalue))))))))) -> (exists dsa_ap_append_sum_add dsa_an_append_sum_add dsa_bp_append_sum_add dsa_bn_append_sum_add dsa_cp_append_sum_add dsa_cn_append_sum_add. (((((a) = 2 * (dsa_ap_append_sum_add) /\ (dsa_an_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addleft. (((a) = 2 * ge_signed_half_append_sum_addleft + 1 /\ (dsa_ap_append_sum_add) = 0) /\ (dsa_an_append_sum_add) = S ge_signed_half_append_sum_addleft))) /\ ((((((b) = 2 * (dsa_bp_append_sum_add) /\ (dsa_bn_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addright. (((b) = 2 * ge_signed_half_append_sum_addright + 1 /\ (dsa_bp_append_sum_add) = 0) /\ (dsa_bn_append_sum_add) = S ge_signed_half_append_sum_addright))) /\ ((((((c) = 2 * (dsa_cp_append_sum_add) /\ (dsa_cn_append_sum_add) = 0) \/ exists ge_signed_half_append_sum_addoutput. (((c) = 2 * ge_signed_half_append_sum_addoutput + 1 /\ (dsa_cp_append_sum_add) = 0) /\ (dsa_cn_append_sum_add) = S ge_signed_half_append_sum_addoutput))) /\ ((dsa_ap_append_sum_add + dsa_bp_append_sum_add) + dsa_cn_append_sum_add = (dsa_an_append_sum_add + dsa_bn_append_sum_add) + dsa_cp_append_sum_add))))))) -> (exists dst_positive_code_append_sum_result dst_positive_scale_append_sum_result dst_negative_code_append_sum_result dst_negative_scale_append_sum_result dst_positive_sum_append_sum_result dst_negative_sum_append_sum_result. (((G) = (((((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) * S ((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) + ((dst_positive_scale_append_sum_result) + (dst_positive_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))) * S ((((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) * S ((dst_positive_code_append_sum_result) + (dst_positive_scale_append_sum_result)) + ((dst_positive_scale_append_sum_result) + (dst_positive_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))) + ((((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result))) + (((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) * S ((dst_negative_code_append_sum_result) + (dst_negative_scale_append_sum_result)) + ((dst_negative_scale_append_sum_result) + (dst_negative_scale_append_sum_result)))))) /\ (((exists fs_u_dst_append_sum_resultpositive fs_v_dst_append_sum_resultpositive. ((((exists fs_h_dst_append_sum_resultpositive_body_start. fs_h_dst_append_sum_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_start. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_start * S ((S (0)) * fs_v_dst_append_sum_resultpositive) + (0))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_terminal. fs_h_dst_append_sum_resultpositive_body_terminal + S (dst_positive_sum_append_sum_result) = S ((S (S l)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_terminal. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_terminal * S ((S (S l)) * fs_v_dst_append_sum_resultpositive) + (dst_positive_sum_append_sum_result))) /\ forall fs_i_dst_append_sum_resultpositive_body_steps. (exists fs_lt_dst_append_sum_resultpositive_body_steps_bound. fs_lt_dst_append_sum_resultpositive_body_steps_bound + S fs_i_dst_append_sum_resultpositive_body_steps = S l) -> exists fs_a_dst_append_sum_resultpositive_body_steps fs_r_dst_append_sum_resultpositive_body_steps fs_s_dst_append_sum_resultpositive_body_steps. ((((exists fs_h_dst_append_sum_resultpositive_body_steps_summand. fs_h_dst_append_sum_resultpositive_body_steps_summand + S (fs_a_dst_append_sum_resultpositive_body_steps) = S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * dst_positive_scale_append_sum_result)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_summand. dst_positive_code_append_sum_result = fs_q_dst_append_sum_resultpositive_body_steps_summand * S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * dst_positive_scale_append_sum_result) + (fs_a_dst_append_sum_resultpositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_steps_partial. fs_h_dst_append_sum_resultpositive_body_steps_partial + S (fs_r_dst_append_sum_resultpositive_body_steps) = S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_partial. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_steps_partial * S ((S (fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive) + (fs_r_dst_append_sum_resultpositive_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultpositive_body_steps_successor. fs_h_dst_append_sum_resultpositive_body_steps_successor + S (fs_s_dst_append_sum_resultpositive_body_steps) = S ((S (S fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive)) /\ exists fs_q_dst_append_sum_resultpositive_body_steps_successor. fs_u_dst_append_sum_resultpositive = fs_q_dst_append_sum_resultpositive_body_steps_successor * S ((S (S fs_i_dst_append_sum_resultpositive_body_steps)) * fs_v_dst_append_sum_resultpositive) + (fs_s_dst_append_sum_resultpositive_body_steps))) /\ fs_s_dst_append_sum_resultpositive_body_steps = fs_r_dst_append_sum_resultpositive_body_steps + fs_a_dst_append_sum_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_append_sum_resultnegative fs_v_dst_append_sum_resultnegative. ((((exists fs_h_dst_append_sum_resultnegative_body_start. fs_h_dst_append_sum_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_start. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_start * S ((S (0)) * fs_v_dst_append_sum_resultnegative) + (0))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_terminal. fs_h_dst_append_sum_resultnegative_body_terminal + S (dst_negative_sum_append_sum_result) = S ((S (S l)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_terminal. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_terminal * S ((S (S l)) * fs_v_dst_append_sum_resultnegative) + (dst_negative_sum_append_sum_result))) /\ forall fs_i_dst_append_sum_resultnegative_body_steps. (exists fs_lt_dst_append_sum_resultnegative_body_steps_bound. fs_lt_dst_append_sum_resultnegative_body_steps_bound + S fs_i_dst_append_sum_resultnegative_body_steps = S l) -> exists fs_a_dst_append_sum_resultnegative_body_steps fs_r_dst_append_sum_resultnegative_body_steps fs_s_dst_append_sum_resultnegative_body_steps. ((((exists fs_h_dst_append_sum_resultnegative_body_steps_summand. fs_h_dst_append_sum_resultnegative_body_steps_summand + S (fs_a_dst_append_sum_resultnegative_body_steps) = S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * dst_negative_scale_append_sum_result)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_summand. dst_negative_code_append_sum_result = fs_q_dst_append_sum_resultnegative_body_steps_summand * S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * dst_negative_scale_append_sum_result) + (fs_a_dst_append_sum_resultnegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_steps_partial. fs_h_dst_append_sum_resultnegative_body_steps_partial + S (fs_r_dst_append_sum_resultnegative_body_steps) = S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_partial. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_steps_partial * S ((S (fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative) + (fs_r_dst_append_sum_resultnegative_body_steps))) /\ ((((exists fs_h_dst_append_sum_resultnegative_body_steps_successor. fs_h_dst_append_sum_resultnegative_body_steps_successor + S (fs_s_dst_append_sum_resultnegative_body_steps) = S ((S (S fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative)) /\ exists fs_q_dst_append_sum_resultnegative_body_steps_successor. fs_u_dst_append_sum_resultnegative = fs_q_dst_append_sum_resultnegative_body_steps_successor * S ((S (S fs_i_dst_append_sum_resultnegative_body_steps)) * fs_v_dst_append_sum_resultnegative) + (fs_s_dst_append_sum_resultnegative_body_steps))) /\ fs_s_dst_append_sum_resultnegative_body_steps = fs_r_dst_append_sum_resultnegative_body_steps + fs_a_dst_append_sum_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_append_sum_resultresult ge_balance_negative_append_sum_resultresult. (((((c) = 2 * (ge_balance_positive_append_sum_resultresult) /\ (ge_balance_negative_append_sum_resultresult) = 0) \/ exists ge_signed_half_append_sum_resultresultdecode. (((c) = 2 * ge_signed_half_append_sum_resultresultdecode + 1 /\ (ge_balance_positive_append_sum_resultresult) = 0) /\ (ge_balance_negative_append_sum_resultresult) = S ge_signed_half_append_sum_resultresultdecode))) /\ ((dst_positive_sum_append_sum_result) + ge_balance_negative_append_sum_resultresult = (dst_negative_sum_append_sum_result) + ge_balance_positive_append_sum_resultresult)))))))))