dirichlet_unit_equation_append

Exact expanded first-order arithmetic statement

forall N F T G u. (exists dst_positive_code_solve_append_F dst_positive_scale_solve_append_F dst_negative_code_solve_append_F dst_negative_scale_solve_append_F. (((F) = (((((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) * S ((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) + ((dst_positive_scale_solve_append_F) + (dst_positive_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))) * S ((((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) * S ((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) + ((dst_positive_scale_solve_append_F) + (dst_positive_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))) + ((((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))))) /\ (forall dst_index_solve_append_F. (exists pvs_le_gap_solve_append_Fdomain. pvs_le_gap_solve_append_Fdomain + (dst_index_solve_append_F) = (S N)) -> exists dst_positive_solve_append_F dst_negative_solve_append_F dst_value_solve_append_F. ((((exists ff_h_pvs_solve_append_Fentrypositive. ff_h_pvs_solve_append_Fentrypositive + S (dst_positive_solve_append_F) = S ((S (dst_index_solve_append_F)) * dst_positive_scale_solve_append_F)) /\ exists ff_q_pvs_solve_append_Fentrypositive. dst_positive_code_solve_append_F = ff_q_pvs_solve_append_Fentrypositive * S ((S (dst_index_solve_append_F)) * dst_positive_scale_solve_append_F) + (dst_positive_solve_append_F))) /\ (((((exists ff_h_pvs_solve_append_Fentrynegative. ff_h_pvs_solve_append_Fentrynegative + S (dst_negative_solve_append_F) = S ((S (dst_index_solve_append_F)) * dst_negative_scale_solve_append_F)) /\ exists ff_q_pvs_solve_append_Fentrynegative. dst_negative_code_solve_append_F = ff_q_pvs_solve_append_Fentrynegative * S ((S (dst_index_solve_append_F)) * dst_negative_scale_solve_append_F) + (dst_negative_solve_append_F))) /\ (exists ge_balance_positive_solve_append_Fentryvalue ge_balance_negative_solve_append_Fentryvalue. (((((dst_value_solve_append_F) = 2 * (ge_balance_positive_solve_append_Fentryvalue) /\ (ge_balance_negative_solve_append_Fentryvalue) = 0) \/ exists ge_signed_half_solve_append_Fentryvaluedecode. (((dst_value_solve_append_F) = 2 * ge_signed_half_solve_append_Fentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_Fentryvalue) = 0) /\ (ge_balance_negative_solve_append_Fentryvalue) = S ge_signed_half_solve_append_Fentryvaluedecode))) /\ ((dst_positive_solve_append_F) + ge_balance_negative_solve_append_Fentryvalue = (dst_negative_solve_append_F) + ge_balance_positive_solve_append_Fentryvalue))))))))) -> (exists dst_positive_code_solve_append_T dst_positive_scale_solve_append_T dst_negative_code_solve_append_T dst_negative_scale_solve_append_T. (((T) = (((((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) * S ((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) + ((dst_positive_scale_solve_append_T) + (dst_positive_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))) * S ((((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) * S ((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) + ((dst_positive_scale_solve_append_T) + (dst_positive_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))) + ((((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))))) /\ (forall dst_index_solve_append_T. (exists pvs_le_gap_solve_append_Tdomain. pvs_le_gap_solve_append_Tdomain + (dst_index_solve_append_T) = (S N)) -> exists dst_positive_solve_append_T dst_negative_solve_append_T dst_value_solve_append_T. ((((exists ff_h_pvs_solve_append_Tentrypositive. ff_h_pvs_solve_append_Tentrypositive + S (dst_positive_solve_append_T) = S ((S (dst_index_solve_append_T)) * dst_positive_scale_solve_append_T)) /\ exists ff_q_pvs_solve_append_Tentrypositive. dst_positive_code_solve_append_T = ff_q_pvs_solve_append_Tentrypositive * S ((S (dst_index_solve_append_T)) * dst_positive_scale_solve_append_T) + (dst_positive_solve_append_T))) /\ (((((exists ff_h_pvs_solve_append_Tentrynegative. ff_h_pvs_solve_append_Tentrynegative + S (dst_negative_solve_append_T) = S ((S (dst_index_solve_append_T)) * dst_negative_scale_solve_append_T)) /\ exists ff_q_pvs_solve_append_Tentrynegative. dst_negative_code_solve_append_T = ff_q_pvs_solve_append_Tentrynegative * S ((S (dst_index_solve_append_T)) * dst_negative_scale_solve_append_T) + (dst_negative_solve_append_T))) /\ (exists ge_balance_positive_solve_append_Tentryvalue ge_balance_negative_solve_append_Tentryvalue. (((((dst_value_solve_append_T) = 2 * (ge_balance_positive_solve_append_Tentryvalue) /\ (ge_balance_negative_solve_append_Tentryvalue) = 0) \/ exists ge_signed_half_solve_append_Tentryvaluedecode. (((dst_value_solve_append_T) = 2 * ge_signed_half_solve_append_Tentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_Tentryvalue) = 0) /\ (ge_balance_negative_solve_append_Tentryvalue) = S ge_signed_half_solve_append_Tentryvaluedecode))) /\ ((dst_positive_solve_append_T) + ge_balance_negative_solve_append_Tentryvalue = (dst_negative_solve_append_T) + ge_balance_positive_solve_append_Tentryvalue))))))))) -> (exists dst_positive_code_solve_append_coefficient dst_positive_scale_solve_append_coefficient dst_negative_code_solve_append_coefficient dst_negative_scale_solve_append_coefficient dst_positive_solve_append_coefficient dst_negative_solve_append_coefficient. (((F) = (((((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) * S ((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) + ((dst_positive_scale_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))) * S ((((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) * S ((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) + ((dst_positive_scale_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))) + ((((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))))) /\ (((((exists ff_h_pvs_solve_append_coefficientpositive. ff_h_pvs_solve_append_coefficientpositive + S (dst_positive_solve_append_coefficient) = S ((S (1)) * dst_positive_scale_solve_append_coefficient)) /\ exists ff_q_pvs_solve_append_coefficientpositive. dst_positive_code_solve_append_coefficient = ff_q_pvs_solve_append_coefficientpositive * S ((S (1)) * dst_positive_scale_solve_append_coefficient) + (dst_positive_solve_append_coefficient))) /\ (((((exists ff_h_pvs_solve_append_coefficientnegative. ff_h_pvs_solve_append_coefficientnegative + S (dst_negative_solve_append_coefficient) = S ((S (1)) * dst_negative_scale_solve_append_coefficient)) /\ exists ff_q_pvs_solve_append_coefficientnegative. dst_negative_code_solve_append_coefficient = ff_q_pvs_solve_append_coefficientnegative * S ((S (1)) * dst_negative_scale_solve_append_coefficient) + (dst_negative_solve_append_coefficient))) /\ (exists ge_balance_positive_solve_append_coefficientvalue ge_balance_negative_solve_append_coefficientvalue. (((((u) = 2 * (ge_balance_positive_solve_append_coefficientvalue) /\ (ge_balance_negative_solve_append_coefficientvalue) = 0) \/ exists ge_signed_half_solve_append_coefficientvaluedecode. (((u) = 2 * ge_signed_half_solve_append_coefficientvaluedecode + 1 /\ (ge_balance_positive_solve_append_coefficientvalue) = 0) /\ (ge_balance_negative_solve_append_coefficientvalue) = S ge_signed_half_solve_append_coefficientvaluedecode))) /\ ((dst_positive_solve_append_coefficient) + ge_balance_negative_solve_append_coefficientvalue = (dst_negative_solve_append_coefficient) + ge_balance_positive_solve_append_coefficientvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> (((exists dst_positive_code_solve_append_previousleft dst_positive_scale_solve_append_previousleft dst_negative_code_solve_append_previousleft dst_negative_scale_solve_append_previousleft. (((G) = (((((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) * S ((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) + ((dst_positive_scale_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))) * S ((((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) * S ((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) + ((dst_positive_scale_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))) + ((((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))))) /\ (forall dst_index_solve_append_previousleft. (exists pvs_le_gap_solve_append_previousleftdomain. pvs_le_gap_solve_append_previousleftdomain + (dst_index_solve_append_previousleft) = (N)) -> exists dst_positive_solve_append_previousleft dst_negative_solve_append_previousleft dst_value_solve_append_previousleft. ((((exists ff_h_pvs_solve_append_previousleftentrypositive. ff_h_pvs_solve_append_previousleftentrypositive + S (dst_positive_solve_append_previousleft) = S ((S (dst_index_solve_append_previousleft)) * dst_positive_scale_solve_append_previousleft)) /\ exists ff_q_pvs_solve_append_previousleftentrypositive. dst_positive_code_solve_append_previousleft = ff_q_pvs_solve_append_previousleftentrypositive * S ((S (dst_index_solve_append_previousleft)) * dst_positive_scale_solve_append_previousleft) + (dst_positive_solve_append_previousleft))) /\ (((((exists ff_h_pvs_solve_append_previousleftentrynegative. ff_h_pvs_solve_append_previousleftentrynegative + S (dst_negative_solve_append_previousleft) = S ((S (dst_index_solve_append_previousleft)) * dst_negative_scale_solve_append_previousleft)) /\ exists ff_q_pvs_solve_append_previousleftentrynegative. dst_negative_code_solve_append_previousleft = ff_q_pvs_solve_append_previousleftentrynegative * S ((S (dst_index_solve_append_previousleft)) * dst_negative_scale_solve_append_previousleft) + (dst_negative_solve_append_previousleft))) /\ (exists ge_balance_positive_solve_append_previousleftentryvalue ge_balance_negative_solve_append_previousleftentryvalue. (((((dst_value_solve_append_previousleft) = 2 * (ge_balance_positive_solve_append_previousleftentryvalue) /\ (ge_balance_negative_solve_append_previousleftentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousleftentryvaluedecode. (((dst_value_solve_append_previousleft) = 2 * ge_signed_half_solve_append_previousleftentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousleftentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousleftentryvalue) = S ge_signed_half_solve_append_previousleftentryvaluedecode))) /\ ((dst_positive_solve_append_previousleft) + ge_balance_negative_solve_append_previousleftentryvalue = (dst_negative_solve_append_previousleft) + ge_balance_positive_solve_append_previousleftentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_previousright dst_positive_scale_solve_append_previousright dst_negative_code_solve_append_previousright dst_negative_scale_solve_append_previousright. (((F) = (((((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) * S ((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) + ((dst_positive_scale_solve_append_previousright) + (dst_positive_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))) * S ((((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) * S ((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) + ((dst_positive_scale_solve_append_previousright) + (dst_positive_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))) + ((((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))))) /\ (forall dst_index_solve_append_previousright. (exists pvs_le_gap_solve_append_previousrightdomain. pvs_le_gap_solve_append_previousrightdomain + (dst_index_solve_append_previousright) = (N)) -> exists dst_positive_solve_append_previousright dst_negative_solve_append_previousright dst_value_solve_append_previousright. ((((exists ff_h_pvs_solve_append_previousrightentrypositive. ff_h_pvs_solve_append_previousrightentrypositive + S (dst_positive_solve_append_previousright) = S ((S (dst_index_solve_append_previousright)) * dst_positive_scale_solve_append_previousright)) /\ exists ff_q_pvs_solve_append_previousrightentrypositive. dst_positive_code_solve_append_previousright = ff_q_pvs_solve_append_previousrightentrypositive * S ((S (dst_index_solve_append_previousright)) * dst_positive_scale_solve_append_previousright) + (dst_positive_solve_append_previousright))) /\ (((((exists ff_h_pvs_solve_append_previousrightentrynegative. ff_h_pvs_solve_append_previousrightentrynegative + S (dst_negative_solve_append_previousright) = S ((S (dst_index_solve_append_previousright)) * dst_negative_scale_solve_append_previousright)) /\ exists ff_q_pvs_solve_append_previousrightentrynegative. dst_negative_code_solve_append_previousright = ff_q_pvs_solve_append_previousrightentrynegative * S ((S (dst_index_solve_append_previousright)) * dst_negative_scale_solve_append_previousright) + (dst_negative_solve_append_previousright))) /\ (exists ge_balance_positive_solve_append_previousrightentryvalue ge_balance_negative_solve_append_previousrightentryvalue. (((((dst_value_solve_append_previousright) = 2 * (ge_balance_positive_solve_append_previousrightentryvalue) /\ (ge_balance_negative_solve_append_previousrightentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousrightentryvaluedecode. (((dst_value_solve_append_previousright) = 2 * ge_signed_half_solve_append_previousrightentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousrightentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousrightentryvalue) = S ge_signed_half_solve_append_previousrightentryvaluedecode))) /\ ((dst_positive_solve_append_previousright) + ge_balance_negative_solve_append_previousrightentryvalue = (dst_negative_solve_append_previousright) + ge_balance_positive_solve_append_previousrightentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_previoustable dst_positive_scale_solve_append_previoustable dst_negative_code_solve_append_previoustable dst_negative_scale_solve_append_previoustable. (((T) = (((((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) * S ((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) + ((dst_positive_scale_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))) * S ((((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) * S ((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) + ((dst_positive_scale_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))) + ((((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))))) /\ (forall dst_index_solve_append_previoustable. (exists pvs_le_gap_solve_append_previoustabledomain. pvs_le_gap_solve_append_previoustabledomain + (dst_index_solve_append_previoustable) = (N)) -> exists dst_positive_solve_append_previoustable dst_negative_solve_append_previoustable dst_value_solve_append_previoustable. ((((exists ff_h_pvs_solve_append_previoustableentrypositive. ff_h_pvs_solve_append_previoustableentrypositive + S (dst_positive_solve_append_previoustable) = S ((S (dst_index_solve_append_previoustable)) * dst_positive_scale_solve_append_previoustable)) /\ exists ff_q_pvs_solve_append_previoustableentrypositive. dst_positive_code_solve_append_previoustable = ff_q_pvs_solve_append_previoustableentrypositive * S ((S (dst_index_solve_append_previoustable)) * dst_positive_scale_solve_append_previoustable) + (dst_positive_solve_append_previoustable))) /\ (((((exists ff_h_pvs_solve_append_previoustableentrynegative. ff_h_pvs_solve_append_previoustableentrynegative + S (dst_negative_solve_append_previoustable) = S ((S (dst_index_solve_append_previoustable)) * dst_negative_scale_solve_append_previoustable)) /\ exists ff_q_pvs_solve_append_previoustableentrynegative. dst_negative_code_solve_append_previoustable = ff_q_pvs_solve_append_previoustableentrynegative * S ((S (dst_index_solve_append_previoustable)) * dst_negative_scale_solve_append_previoustable) + (dst_negative_solve_append_previoustable))) /\ (exists ge_balance_positive_solve_append_previoustableentryvalue ge_balance_negative_solve_append_previoustableentryvalue. (((((dst_value_solve_append_previoustable) = 2 * (ge_balance_positive_solve_append_previoustableentryvalue) /\ (ge_balance_negative_solve_append_previoustableentryvalue) = 0) \/ exists ge_signed_half_solve_append_previoustableentryvaluedecode. (((dst_value_solve_append_previoustable) = 2 * ge_signed_half_solve_append_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previoustableentryvalue) = 0) /\ (ge_balance_negative_solve_append_previoustableentryvalue) = S ge_signed_half_solve_append_previoustableentryvaluedecode))) /\ ((dst_positive_solve_append_previoustable) + ge_balance_negative_solve_append_previoustableentryvalue = (dst_negative_solve_append_previoustable) + ge_balance_positive_solve_append_previoustableentryvalue))))))))) /\ (forall dc_input_solve_append_previous dc_output_solve_append_previous. ~(dc_input_solve_append_previous=0) -> (exists pvs_le_gap_solve_append_previousdomain. pvs_le_gap_solve_append_previousdomain + (dc_input_solve_append_previous) = (N)) -> (exists dst_positive_code_solve_append_previouslookup dst_positive_scale_solve_append_previouslookup dst_negative_code_solve_append_previouslookup dst_negative_scale_solve_append_previouslookup dst_positive_solve_append_previouslookup dst_negative_solve_append_previouslookup. (((T) = (((((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) * S ((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) + ((dst_positive_scale_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))) * S ((((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) * S ((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) + ((dst_positive_scale_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))) + ((((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))))) /\ (((((exists ff_h_pvs_solve_append_previouslookuppositive. ff_h_pvs_solve_append_previouslookuppositive + S (dst_positive_solve_append_previouslookup) = S ((S (dc_input_solve_append_previous)) * dst_positive_scale_solve_append_previouslookup)) /\ exists ff_q_pvs_solve_append_previouslookuppositive. dst_positive_code_solve_append_previouslookup = ff_q_pvs_solve_append_previouslookuppositive * S ((S (dc_input_solve_append_previous)) * dst_positive_scale_solve_append_previouslookup) + (dst_positive_solve_append_previouslookup))) /\ (((((exists ff_h_pvs_solve_append_previouslookupnegative. ff_h_pvs_solve_append_previouslookupnegative + S (dst_negative_solve_append_previouslookup) = S ((S (dc_input_solve_append_previous)) * dst_negative_scale_solve_append_previouslookup)) /\ exists ff_q_pvs_solve_append_previouslookupnegative. dst_negative_code_solve_append_previouslookup = ff_q_pvs_solve_append_previouslookupnegative * S ((S (dc_input_solve_append_previous)) * dst_negative_scale_solve_append_previouslookup) + (dst_negative_solve_append_previouslookup))) /\ (exists ge_balance_positive_solve_append_previouslookupvalue ge_balance_negative_solve_append_previouslookupvalue. (((((dc_output_solve_append_previous) = 2 * (ge_balance_positive_solve_append_previouslookupvalue) /\ (ge_balance_negative_solve_append_previouslookupvalue) = 0) \/ exists ge_signed_half_solve_append_previouslookupvaluedecode. (((dc_output_solve_append_previous) = 2 * ge_signed_half_solve_append_previouslookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_previouslookupvalue) = 0) /\ (ge_balance_negative_solve_append_previouslookupvalue) = S ge_signed_half_solve_append_previouslookupvaluedecode))) /\ ((dst_positive_solve_append_previouslookup) + ge_balance_negative_solve_append_previouslookupvalue = (dst_negative_solve_append_previouslookup) + ge_balance_positive_solve_append_previouslookupvalue))))))))) -> (((~((dc_input_solve_append_previous)=0)) /\ (exists dc_mask_solve_append_previousvalue. ((((exists dst_positive_code_solve_append_previousvaluemasktable dst_positive_scale_solve_append_previousvaluemasktable dst_negative_code_solve_append_previousvaluemasktable dst_negative_scale_solve_append_previousvaluemasktable. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) * S ((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) + ((dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))) * S ((((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) * S ((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) + ((dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))) + ((((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))))) /\ (forall dst_index_solve_append_previousvaluemasktable. (exists pvs_le_gap_solve_append_previousvaluemasktabledomain. pvs_le_gap_solve_append_previousvaluemasktabledomain + (dst_index_solve_append_previousvaluemasktable) = (dc_input_solve_append_previous)) -> exists dst_positive_solve_append_previousvaluemasktable dst_negative_solve_append_previousvaluemasktable dst_value_solve_append_previousvaluemasktable. ((((exists ff_h_pvs_solve_append_previousvaluemasktableentrypositive. ff_h_pvs_solve_append_previousvaluemasktableentrypositive + S (dst_positive_solve_append_previousvaluemasktable) = S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_positive_scale_solve_append_previousvaluemasktable)) /\ exists ff_q_pvs_solve_append_previousvaluemasktableentrypositive. dst_positive_code_solve_append_previousvaluemasktable = ff_q_pvs_solve_append_previousvaluemasktableentrypositive * S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_solve_append_previousvaluemasktable))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasktableentrynegative. ff_h_pvs_solve_append_previousvaluemasktableentrynegative + S (dst_negative_solve_append_previousvaluemasktable) = S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_negative_scale_solve_append_previousvaluemasktable)) /\ exists ff_q_pvs_solve_append_previousvaluemasktableentrynegative. dst_negative_code_solve_append_previousvaluemasktable = ff_q_pvs_solve_append_previousvaluemasktableentrynegative * S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_solve_append_previousvaluemasktable))) /\ (exists ge_balance_positive_solve_append_previousvaluemasktableentryvalue ge_balance_negative_solve_append_previousvaluemasktableentryvalue. (((((dst_value_solve_append_previousvaluemasktable) = 2 * (ge_balance_positive_solve_append_previousvaluemasktableentryvalue) /\ (ge_balance_negative_solve_append_previousvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode. (((dst_value_solve_append_previousvaluemasktable) = 2 * ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemasktableentryvalue) = S ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemasktable) + ge_balance_negative_solve_append_previousvaluemasktableentryvalue = (dst_negative_solve_append_previousvaluemasktable) + ge_balance_positive_solve_append_previousvaluemasktableentryvalue))))))))) /\ (forall dc_index_solve_append_previousvaluemask dc_value_solve_append_previousvaluemask. (exists pvs_le_gap_solve_append_previousvaluemaskdomain. pvs_le_gap_solve_append_previousvaluemaskdomain + (dc_index_solve_append_previousvaluemask) = (dc_input_solve_append_previous)) -> (exists dst_positive_code_solve_append_previousvaluemasklookup dst_positive_scale_solve_append_previousvaluemasklookup dst_negative_code_solve_append_previousvaluemasklookup dst_negative_scale_solve_append_previousvaluemasklookup dst_positive_solve_append_previousvaluemasklookup dst_negative_solve_append_previousvaluemasklookup. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) * S ((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) + ((dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))) * S ((((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) * S ((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) + ((dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))) + ((((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasklookuppositive. ff_h_pvs_solve_append_previousvaluemasklookuppositive + S (dst_positive_solve_append_previousvaluemasklookup) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemasklookup)) /\ exists ff_q_pvs_solve_append_previousvaluemasklookuppositive. dst_positive_code_solve_append_previousvaluemasklookup = ff_q_pvs_solve_append_previousvaluemasklookuppositive * S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_solve_append_previousvaluemasklookup))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasklookupnegative. ff_h_pvs_solve_append_previousvaluemasklookupnegative + S (dst_negative_solve_append_previousvaluemasklookup) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemasklookup)) /\ exists ff_q_pvs_solve_append_previousvaluemasklookupnegative. dst_negative_code_solve_append_previousvaluemasklookup = ff_q_pvs_solve_append_previousvaluemasklookupnegative * S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_solve_append_previousvaluemasklookup))) /\ (exists ge_balance_positive_solve_append_previousvaluemasklookupvalue ge_balance_negative_solve_append_previousvaluemasklookupvalue. (((((dc_value_solve_append_previousvaluemask) = 2 * (ge_balance_positive_solve_append_previousvaluemasklookupvalue) /\ (ge_balance_negative_solve_append_previousvaluemasklookupvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemasklookupvaluedecode. (((dc_value_solve_append_previousvaluemask) = 2 * ge_signed_half_solve_append_previousvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemasklookupvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemasklookupvalue) = S ge_signed_half_solve_append_previousvaluemasklookupvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemasklookup) + ge_balance_negative_solve_append_previousvaluemasklookupvalue = (dst_negative_solve_append_previousvaluemasklookup) + ge_balance_positive_solve_append_previousvaluemasklookupvalue))))))))) -> ((((~((dc_index_solve_append_previousvaluemask)=0)) /\ (exists dc_quotient_solve_append_previousvaluemaskentry dc_left_solve_append_previousvaluemaskentry dc_right_solve_append_previousvaluemaskentry. (((dc_input_solve_append_previous)=(dc_index_solve_append_previousvaluemask)*dc_quotient_solve_append_previousvaluemaskentry) /\ (((exists dst_positive_code_solve_append_previousvaluemaskentryleft dst_positive_scale_solve_append_previousvaluemaskentryleft dst_negative_code_solve_append_previousvaluemaskentryleft dst_negative_scale_solve_append_previousvaluemaskentryleft dst_positive_solve_append_previousvaluemaskentryleft dst_negative_solve_append_previousvaluemaskentryleft. (((G) = (((((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) + ((dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))) * S ((((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) + ((dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))) + ((((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryleftpositive. ff_h_pvs_solve_append_previousvaluemaskentryleftpositive + S (dst_positive_solve_append_previousvaluemaskentryleft) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryleftpositive. dst_positive_code_solve_append_previousvaluemaskentryleft = ff_q_pvs_solve_append_previousvaluemaskentryleftpositive * S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_solve_append_previousvaluemaskentryleft))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryleftnegative. ff_h_pvs_solve_append_previousvaluemaskentryleftnegative + S (dst_negative_solve_append_previousvaluemaskentryleft) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryleftnegative. dst_negative_code_solve_append_previousvaluemaskentryleft = ff_q_pvs_solve_append_previousvaluemaskentryleftnegative * S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_solve_append_previousvaluemaskentryleft))) /\ (exists ge_balance_positive_solve_append_previousvaluemaskentryleftvalue ge_balance_negative_solve_append_previousvaluemaskentryleftvalue. (((((dc_left_solve_append_previousvaluemaskentry) = 2 * (ge_balance_positive_solve_append_previousvaluemaskentryleftvalue) /\ (ge_balance_negative_solve_append_previousvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode. (((dc_left_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemaskentryleftvalue) = S ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemaskentryleft) + ge_balance_negative_solve_append_previousvaluemaskentryleftvalue = (dst_negative_solve_append_previousvaluemaskentryleft) + ge_balance_positive_solve_append_previousvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_solve_append_previousvaluemaskentryright dst_positive_scale_solve_append_previousvaluemaskentryright dst_negative_code_solve_append_previousvaluemaskentryright dst_negative_scale_solve_append_previousvaluemaskentryright dst_positive_solve_append_previousvaluemaskentryright dst_negative_solve_append_previousvaluemaskentryright. (((F) = (((((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) * S ((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) + ((dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))) * S ((((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) * S ((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) + ((dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))) + ((((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryrightpositive. ff_h_pvs_solve_append_previousvaluemaskentryrightpositive + S (dst_positive_solve_append_previousvaluemaskentryright) = S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_positive_scale_solve_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryrightpositive. dst_positive_code_solve_append_previousvaluemaskentryright = ff_q_pvs_solve_append_previousvaluemaskentryrightpositive * S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_solve_append_previousvaluemaskentryright))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryrightnegative. ff_h_pvs_solve_append_previousvaluemaskentryrightnegative + S (dst_negative_solve_append_previousvaluemaskentryright) = S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_negative_scale_solve_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryrightnegative. dst_negative_code_solve_append_previousvaluemaskentryright = ff_q_pvs_solve_append_previousvaluemaskentryrightnegative * S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_solve_append_previousvaluemaskentryright))) /\ (exists ge_balance_positive_solve_append_previousvaluemaskentryrightvalue ge_balance_negative_solve_append_previousvaluemaskentryrightvalue. (((((dc_right_solve_append_previousvaluemaskentry) = 2 * (ge_balance_positive_solve_append_previousvaluemaskentryrightvalue) /\ (ge_balance_negative_solve_append_previousvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode. (((dc_right_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemaskentryrightvalue) = S ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemaskentryright) + ge_balance_negative_solve_append_previousvaluemaskentryrightvalue = (dst_negative_solve_append_previousvaluemaskentryright) + ge_balance_positive_solve_append_previousvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_solve_append_previousvaluemaskentryproduct sto_an_solve_append_previousvaluemaskentryproduct sto_bp_solve_append_previousvaluemaskentryproduct sto_bn_solve_append_previousvaluemaskentryproduct sto_cp_solve_append_previousvaluemaskentryproduct sto_cn_solve_append_previousvaluemaskentryproduct. (((((dc_left_solve_append_previousvaluemaskentry) = 2 * (sto_ap_solve_append_previousvaluemaskentryproduct) /\ (sto_an_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductleft. (((dc_left_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductleft + 1 /\ (sto_ap_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_an_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductleft))) /\ ((((((dc_right_solve_append_previousvaluemaskentry) = 2 * (sto_bp_solve_append_previousvaluemaskentryproduct) /\ (sto_bn_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductright. (((dc_right_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductright + 1 /\ (sto_bp_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_bn_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductright))) /\ ((((((dc_value_solve_append_previousvaluemask) = 2 * (sto_cp_solve_append_previousvaluemaskentryproduct) /\ (sto_cn_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductoutput. (((dc_value_solve_append_previousvaluemask) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductoutput + 1 /\ (sto_cp_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_cn_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductoutput))) /\ ((sto_ap_solve_append_previousvaluemaskentryproduct * sto_bp_solve_append_previousvaluemaskentryproduct + sto_an_solve_append_previousvaluemaskentryproduct * sto_bn_solve_append_previousvaluemaskentryproduct) + sto_cn_solve_append_previousvaluemaskentryproduct = (sto_ap_solve_append_previousvaluemaskentryproduct * sto_bn_solve_append_previousvaluemaskentryproduct + sto_an_solve_append_previousvaluemaskentryproduct * sto_bp_solve_append_previousvaluemaskentryproduct) + sto_cp_solve_append_previousvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_solve_append_previousvaluemask)=0 \/ ~(exists pvs_factor_solve_append_previousvaluemaskentrynondivisor. (dc_input_solve_append_previous) = (dc_index_solve_append_previousvaluemask) * pvs_factor_solve_append_previousvaluemaskentrynondivisor)) /\ ((dc_value_solve_append_previousvaluemask)=0))))))) /\ (exists dst_positive_code_solve_append_previousvaluefold dst_positive_scale_solve_append_previousvaluefold dst_negative_code_solve_append_previousvaluefold dst_negative_scale_solve_append_previousvaluefold dst_positive_sum_solve_append_previousvaluefold dst_negative_sum_solve_append_previousvaluefold. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) * S ((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) + ((dst_positive_scale_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))) * S ((((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) * S ((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) + ((dst_positive_scale_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))) + ((((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))))) /\ (((exists fs_u_dst_solve_append_previousvaluefoldpositive fs_v_dst_solve_append_previousvaluefoldpositive. ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_start. fs_h_dst_solve_append_previousvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_start. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_terminal. fs_h_dst_solve_append_previousvaluefoldpositive_body_terminal + S (dst_positive_sum_solve_append_previousvaluefold) = S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_terminal. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_terminal * S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldpositive) + (dst_positive_sum_solve_append_previousvaluefold))) /\ forall fs_i_dst_solve_append_previousvaluefoldpositive_body_steps. (exists fs_lt_dst_solve_append_previousvaluefoldpositive_body_steps_bound. fs_lt_dst_solve_append_previousvaluefoldpositive_body_steps_bound + S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps = S (dc_input_solve_append_previous)) -> exists fs_a_dst_solve_append_previousvaluefoldpositive_body_steps fs_r_dst_solve_append_previousvaluefoldpositive_body_steps fs_s_dst_solve_append_previousvaluefoldpositive_body_steps. ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_summand. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_summand + S (fs_a_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_previousvaluefold)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_summand. dst_positive_code_solve_append_previousvaluefold = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_previousvaluefold) + (fs_a_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_partial. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_partial + S (fs_r_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_partial. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (fs_r_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_successor. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_successor + S (fs_s_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_successor. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (fs_s_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ fs_s_dst_solve_append_previousvaluefoldpositive_body_steps = fs_r_dst_solve_append_previousvaluefoldpositive_body_steps + fs_a_dst_solve_append_previousvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_solve_append_previousvaluefoldnegative fs_v_dst_solve_append_previousvaluefoldnegative. ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_start. fs_h_dst_solve_append_previousvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_start. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_terminal. fs_h_dst_solve_append_previousvaluefoldnegative_body_terminal + S (dst_negative_sum_solve_append_previousvaluefold) = S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_terminal. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_terminal * S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldnegative) + (dst_negative_sum_solve_append_previousvaluefold))) /\ forall fs_i_dst_solve_append_previousvaluefoldnegative_body_steps. (exists fs_lt_dst_solve_append_previousvaluefoldnegative_body_steps_bound. fs_lt_dst_solve_append_previousvaluefoldnegative_body_steps_bound + S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps = S (dc_input_solve_append_previous)) -> exists fs_a_dst_solve_append_previousvaluefoldnegative_body_steps fs_r_dst_solve_append_previousvaluefoldnegative_body_steps fs_s_dst_solve_append_previousvaluefoldnegative_body_steps. ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_summand. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_summand + S (fs_a_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_previousvaluefold)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_summand. dst_negative_code_solve_append_previousvaluefold = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_previousvaluefold) + (fs_a_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_partial. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_partial + S (fs_r_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_partial. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (fs_r_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_successor. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_successor + S (fs_s_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_successor. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (fs_s_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ fs_s_dst_solve_append_previousvaluefoldnegative_body_steps = fs_r_dst_solve_append_previousvaluefoldnegative_body_steps + fs_a_dst_solve_append_previousvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_solve_append_previousvaluefoldresult ge_balance_negative_solve_append_previousvaluefoldresult. (((((dc_output_solve_append_previous) = 2 * (ge_balance_positive_solve_append_previousvaluefoldresult) /\ (ge_balance_negative_solve_append_previousvaluefoldresult) = 0) \/ exists ge_signed_half_solve_append_previousvaluefoldresultdecode. (((dc_output_solve_append_previous) = 2 * ge_signed_half_solve_append_previousvaluefoldresultdecode + 1 /\ (ge_balance_positive_solve_append_previousvaluefoldresult) = 0) /\ (ge_balance_negative_solve_append_previousvaluefoldresult) = S ge_signed_half_solve_append_previousvaluefoldresultdecode))) /\ ((dst_positive_sum_solve_append_previousvaluefold) + ge_balance_negative_solve_append_previousvaluefoldresult = (dst_negative_sum_solve_append_previousvaluefold) + ge_balance_positive_solve_append_previousvaluefoldresult)))))))))))))))))))) -> exists H. ((((exists dst_positive_code_solve_append_resultleft dst_positive_scale_solve_append_resultleft dst_negative_code_solve_append_resultleft dst_negative_scale_solve_append_resultleft. (((H) = (((((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) * S ((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) + ((dst_positive_scale_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))) * S ((((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) * S ((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) + ((dst_positive_scale_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))) + ((((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))))) /\ (forall dst_index_solve_append_resultleft. (exists pvs_le_gap_solve_append_resultleftdomain. pvs_le_gap_solve_append_resultleftdomain + (dst_index_solve_append_resultleft) = (S N)) -> exists dst_positive_solve_append_resultleft dst_negative_solve_append_resultleft dst_value_solve_append_resultleft. ((((exists ff_h_pvs_solve_append_resultleftentrypositive. ff_h_pvs_solve_append_resultleftentrypositive + S (dst_positive_solve_append_resultleft) = S ((S (dst_index_solve_append_resultleft)) * dst_positive_scale_solve_append_resultleft)) /\ exists ff_q_pvs_solve_append_resultleftentrypositive. dst_positive_code_solve_append_resultleft = ff_q_pvs_solve_append_resultleftentrypositive * S ((S (dst_index_solve_append_resultleft)) * dst_positive_scale_solve_append_resultleft) + (dst_positive_solve_append_resultleft))) /\ (((((exists ff_h_pvs_solve_append_resultleftentrynegative. ff_h_pvs_solve_append_resultleftentrynegative + S (dst_negative_solve_append_resultleft) = S ((S (dst_index_solve_append_resultleft)) * dst_negative_scale_solve_append_resultleft)) /\ exists ff_q_pvs_solve_append_resultleftentrynegative. dst_negative_code_solve_append_resultleft = ff_q_pvs_solve_append_resultleftentrynegative * S ((S (dst_index_solve_append_resultleft)) * dst_negative_scale_solve_append_resultleft) + (dst_negative_solve_append_resultleft))) /\ (exists ge_balance_positive_solve_append_resultleftentryvalue ge_balance_negative_solve_append_resultleftentryvalue. (((((dst_value_solve_append_resultleft) = 2 * (ge_balance_positive_solve_append_resultleftentryvalue) /\ (ge_balance_negative_solve_append_resultleftentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultleftentryvaluedecode. (((dst_value_solve_append_resultleft) = 2 * ge_signed_half_solve_append_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultleftentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultleftentryvalue) = S ge_signed_half_solve_append_resultleftentryvaluedecode))) /\ ((dst_positive_solve_append_resultleft) + ge_balance_negative_solve_append_resultleftentryvalue = (dst_negative_solve_append_resultleft) + ge_balance_positive_solve_append_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_resultright dst_positive_scale_solve_append_resultright dst_negative_code_solve_append_resultright dst_negative_scale_solve_append_resultright. (((F) = (((((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) * S ((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) + ((dst_positive_scale_solve_append_resultright) + (dst_positive_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))) * S ((((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) * S ((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) + ((dst_positive_scale_solve_append_resultright) + (dst_positive_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))) + ((((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))))) /\ (forall dst_index_solve_append_resultright. (exists pvs_le_gap_solve_append_resultrightdomain. pvs_le_gap_solve_append_resultrightdomain + (dst_index_solve_append_resultright) = (S N)) -> exists dst_positive_solve_append_resultright dst_negative_solve_append_resultright dst_value_solve_append_resultright. ((((exists ff_h_pvs_solve_append_resultrightentrypositive. ff_h_pvs_solve_append_resultrightentrypositive + S (dst_positive_solve_append_resultright) = S ((S (dst_index_solve_append_resultright)) * dst_positive_scale_solve_append_resultright)) /\ exists ff_q_pvs_solve_append_resultrightentrypositive. dst_positive_code_solve_append_resultright = ff_q_pvs_solve_append_resultrightentrypositive * S ((S (dst_index_solve_append_resultright)) * dst_positive_scale_solve_append_resultright) + (dst_positive_solve_append_resultright))) /\ (((((exists ff_h_pvs_solve_append_resultrightentrynegative. ff_h_pvs_solve_append_resultrightentrynegative + S (dst_negative_solve_append_resultright) = S ((S (dst_index_solve_append_resultright)) * dst_negative_scale_solve_append_resultright)) /\ exists ff_q_pvs_solve_append_resultrightentrynegative. dst_negative_code_solve_append_resultright = ff_q_pvs_solve_append_resultrightentrynegative * S ((S (dst_index_solve_append_resultright)) * dst_negative_scale_solve_append_resultright) + (dst_negative_solve_append_resultright))) /\ (exists ge_balance_positive_solve_append_resultrightentryvalue ge_balance_negative_solve_append_resultrightentryvalue. (((((dst_value_solve_append_resultright) = 2 * (ge_balance_positive_solve_append_resultrightentryvalue) /\ (ge_balance_negative_solve_append_resultrightentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultrightentryvaluedecode. (((dst_value_solve_append_resultright) = 2 * ge_signed_half_solve_append_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultrightentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultrightentryvalue) = S ge_signed_half_solve_append_resultrightentryvaluedecode))) /\ ((dst_positive_solve_append_resultright) + ge_balance_negative_solve_append_resultrightentryvalue = (dst_negative_solve_append_resultright) + ge_balance_positive_solve_append_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_resulttable dst_positive_scale_solve_append_resulttable dst_negative_code_solve_append_resulttable dst_negative_scale_solve_append_resulttable. (((T) = (((((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) * S ((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) + ((dst_positive_scale_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))) * S ((((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) * S ((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) + ((dst_positive_scale_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))) + ((((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))))) /\ (forall dst_index_solve_append_resulttable. (exists pvs_le_gap_solve_append_resulttabledomain. pvs_le_gap_solve_append_resulttabledomain + (dst_index_solve_append_resulttable) = (S N)) -> exists dst_positive_solve_append_resulttable dst_negative_solve_append_resulttable dst_value_solve_append_resulttable. ((((exists ff_h_pvs_solve_append_resulttableentrypositive. ff_h_pvs_solve_append_resulttableentrypositive + S (dst_positive_solve_append_resulttable) = S ((S (dst_index_solve_append_resulttable)) * dst_positive_scale_solve_append_resulttable)) /\ exists ff_q_pvs_solve_append_resulttableentrypositive. dst_positive_code_solve_append_resulttable = ff_q_pvs_solve_append_resulttableentrypositive * S ((S (dst_index_solve_append_resulttable)) * dst_positive_scale_solve_append_resulttable) + (dst_positive_solve_append_resulttable))) /\ (((((exists ff_h_pvs_solve_append_resulttableentrynegative. ff_h_pvs_solve_append_resulttableentrynegative + S (dst_negative_solve_append_resulttable) = S ((S (dst_index_solve_append_resulttable)) * dst_negative_scale_solve_append_resulttable)) /\ exists ff_q_pvs_solve_append_resulttableentrynegative. dst_negative_code_solve_append_resulttable = ff_q_pvs_solve_append_resulttableentrynegative * S ((S (dst_index_solve_append_resulttable)) * dst_negative_scale_solve_append_resulttable) + (dst_negative_solve_append_resulttable))) /\ (exists ge_balance_positive_solve_append_resulttableentryvalue ge_balance_negative_solve_append_resulttableentryvalue. (((((dst_value_solve_append_resulttable) = 2 * (ge_balance_positive_solve_append_resulttableentryvalue) /\ (ge_balance_negative_solve_append_resulttableentryvalue) = 0) \/ exists ge_signed_half_solve_append_resulttableentryvaluedecode. (((dst_value_solve_append_resulttable) = 2 * ge_signed_half_solve_append_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resulttableentryvalue) = 0) /\ (ge_balance_negative_solve_append_resulttableentryvalue) = S ge_signed_half_solve_append_resulttableentryvaluedecode))) /\ ((dst_positive_solve_append_resulttable) + ge_balance_negative_solve_append_resulttableentryvalue = (dst_negative_solve_append_resulttable) + ge_balance_positive_solve_append_resulttableentryvalue))))))))) /\ (forall dc_input_solve_append_result dc_output_solve_append_result. ~(dc_input_solve_append_result=0) -> (exists pvs_le_gap_solve_append_resultdomain. pvs_le_gap_solve_append_resultdomain + (dc_input_solve_append_result) = (S N)) -> (exists dst_positive_code_solve_append_resultlookup dst_positive_scale_solve_append_resultlookup dst_negative_code_solve_append_resultlookup dst_negative_scale_solve_append_resultlookup dst_positive_solve_append_resultlookup dst_negative_solve_append_resultlookup. (((T) = (((((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) * S ((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) + ((dst_positive_scale_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))) * S ((((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) * S ((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) + ((dst_positive_scale_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))) + ((((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))))) /\ (((((exists ff_h_pvs_solve_append_resultlookuppositive. ff_h_pvs_solve_append_resultlookuppositive + S (dst_positive_solve_append_resultlookup) = S ((S (dc_input_solve_append_result)) * dst_positive_scale_solve_append_resultlookup)) /\ exists ff_q_pvs_solve_append_resultlookuppositive. dst_positive_code_solve_append_resultlookup = ff_q_pvs_solve_append_resultlookuppositive * S ((S (dc_input_solve_append_result)) * dst_positive_scale_solve_append_resultlookup) + (dst_positive_solve_append_resultlookup))) /\ (((((exists ff_h_pvs_solve_append_resultlookupnegative. ff_h_pvs_solve_append_resultlookupnegative + S (dst_negative_solve_append_resultlookup) = S ((S (dc_input_solve_append_result)) * dst_negative_scale_solve_append_resultlookup)) /\ exists ff_q_pvs_solve_append_resultlookupnegative. dst_negative_code_solve_append_resultlookup = ff_q_pvs_solve_append_resultlookupnegative * S ((S (dc_input_solve_append_result)) * dst_negative_scale_solve_append_resultlookup) + (dst_negative_solve_append_resultlookup))) /\ (exists ge_balance_positive_solve_append_resultlookupvalue ge_balance_negative_solve_append_resultlookupvalue. (((((dc_output_solve_append_result) = 2 * (ge_balance_positive_solve_append_resultlookupvalue) /\ (ge_balance_negative_solve_append_resultlookupvalue) = 0) \/ exists ge_signed_half_solve_append_resultlookupvaluedecode. (((dc_output_solve_append_result) = 2 * ge_signed_half_solve_append_resultlookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultlookupvalue) = 0) /\ (ge_balance_negative_solve_append_resultlookupvalue) = S ge_signed_half_solve_append_resultlookupvaluedecode))) /\ ((dst_positive_solve_append_resultlookup) + ge_balance_negative_solve_append_resultlookupvalue = (dst_negative_solve_append_resultlookup) + ge_balance_positive_solve_append_resultlookupvalue))))))))) -> (((~((dc_input_solve_append_result)=0)) /\ (exists dc_mask_solve_append_resultvalue. ((((exists dst_positive_code_solve_append_resultvaluemasktable dst_positive_scale_solve_append_resultvaluemasktable dst_negative_code_solve_append_resultvaluemasktable dst_negative_scale_solve_append_resultvaluemasktable. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) * S ((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) + ((dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))) * S ((((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) * S ((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) + ((dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))) + ((((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))))) /\ (forall dst_index_solve_append_resultvaluemasktable. (exists pvs_le_gap_solve_append_resultvaluemasktabledomain. pvs_le_gap_solve_append_resultvaluemasktabledomain + (dst_index_solve_append_resultvaluemasktable) = (dc_input_solve_append_result)) -> exists dst_positive_solve_append_resultvaluemasktable dst_negative_solve_append_resultvaluemasktable dst_value_solve_append_resultvaluemasktable. ((((exists ff_h_pvs_solve_append_resultvaluemasktableentrypositive. ff_h_pvs_solve_append_resultvaluemasktableentrypositive + S (dst_positive_solve_append_resultvaluemasktable) = S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_positive_scale_solve_append_resultvaluemasktable)) /\ exists ff_q_pvs_solve_append_resultvaluemasktableentrypositive. dst_positive_code_solve_append_resultvaluemasktable = ff_q_pvs_solve_append_resultvaluemasktableentrypositive * S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_solve_append_resultvaluemasktable))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasktableentrynegative. ff_h_pvs_solve_append_resultvaluemasktableentrynegative + S (dst_negative_solve_append_resultvaluemasktable) = S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_negative_scale_solve_append_resultvaluemasktable)) /\ exists ff_q_pvs_solve_append_resultvaluemasktableentrynegative. dst_negative_code_solve_append_resultvaluemasktable = ff_q_pvs_solve_append_resultvaluemasktableentrynegative * S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_solve_append_resultvaluemasktable))) /\ (exists ge_balance_positive_solve_append_resultvaluemasktableentryvalue ge_balance_negative_solve_append_resultvaluemasktableentryvalue. (((((dst_value_solve_append_resultvaluemasktable) = 2 * (ge_balance_positive_solve_append_resultvaluemasktableentryvalue) /\ (ge_balance_negative_solve_append_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode. (((dst_value_solve_append_resultvaluemasktable) = 2 * ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemasktableentryvalue) = S ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemasktable) + ge_balance_negative_solve_append_resultvaluemasktableentryvalue = (dst_negative_solve_append_resultvaluemasktable) + ge_balance_positive_solve_append_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_solve_append_resultvaluemask dc_value_solve_append_resultvaluemask. (exists pvs_le_gap_solve_append_resultvaluemaskdomain. pvs_le_gap_solve_append_resultvaluemaskdomain + (dc_index_solve_append_resultvaluemask) = (dc_input_solve_append_result)) -> (exists dst_positive_code_solve_append_resultvaluemasklookup dst_positive_scale_solve_append_resultvaluemasklookup dst_negative_code_solve_append_resultvaluemasklookup dst_negative_scale_solve_append_resultvaluemasklookup dst_positive_solve_append_resultvaluemasklookup dst_negative_solve_append_resultvaluemasklookup. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) * S ((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) + ((dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))) * S ((((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) * S ((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) + ((dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))) + ((((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasklookuppositive. ff_h_pvs_solve_append_resultvaluemasklookuppositive + S (dst_positive_solve_append_resultvaluemasklookup) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_append_resultvaluemasklookuppositive. dst_positive_code_solve_append_resultvaluemasklookup = ff_q_pvs_solve_append_resultvaluemasklookuppositive * S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_solve_append_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasklookupnegative. ff_h_pvs_solve_append_resultvaluemasklookupnegative + S (dst_negative_solve_append_resultvaluemasklookup) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_append_resultvaluemasklookupnegative. dst_negative_code_solve_append_resultvaluemasklookup = ff_q_pvs_solve_append_resultvaluemasklookupnegative * S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_solve_append_resultvaluemasklookup))) /\ (exists ge_balance_positive_solve_append_resultvaluemasklookupvalue ge_balance_negative_solve_append_resultvaluemasklookupvalue. (((((dc_value_solve_append_resultvaluemask) = 2 * (ge_balance_positive_solve_append_resultvaluemasklookupvalue) /\ (ge_balance_negative_solve_append_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemasklookupvaluedecode. (((dc_value_solve_append_resultvaluemask) = 2 * ge_signed_half_solve_append_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemasklookupvalue) = S ge_signed_half_solve_append_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemasklookup) + ge_balance_negative_solve_append_resultvaluemasklookupvalue = (dst_negative_solve_append_resultvaluemasklookup) + ge_balance_positive_solve_append_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_solve_append_resultvaluemask)=0)) /\ (exists dc_quotient_solve_append_resultvaluemaskentry dc_left_solve_append_resultvaluemaskentry dc_right_solve_append_resultvaluemaskentry. (((dc_input_solve_append_result)=(dc_index_solve_append_resultvaluemask)*dc_quotient_solve_append_resultvaluemaskentry) /\ (((exists dst_positive_code_solve_append_resultvaluemaskentryleft dst_positive_scale_solve_append_resultvaluemaskentryleft dst_negative_code_solve_append_resultvaluemaskentryleft dst_negative_scale_solve_append_resultvaluemaskentryleft dst_positive_solve_append_resultvaluemaskentryleft dst_negative_solve_append_resultvaluemaskentryleft. (((H) = (((((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))) * S ((((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))) + ((((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryleftpositive. ff_h_pvs_solve_append_resultvaluemaskentryleftpositive + S (dst_positive_solve_append_resultvaluemaskentryleft) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryleftpositive. dst_positive_code_solve_append_resultvaluemaskentryleft = ff_q_pvs_solve_append_resultvaluemaskentryleftpositive * S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_solve_append_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryleftnegative. ff_h_pvs_solve_append_resultvaluemaskentryleftnegative + S (dst_negative_solve_append_resultvaluemaskentryleft) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryleftnegative. dst_negative_code_solve_append_resultvaluemaskentryleft = ff_q_pvs_solve_append_resultvaluemaskentryleftnegative * S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_solve_append_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_solve_append_resultvaluemaskentryleftvalue ge_balance_negative_solve_append_resultvaluemaskentryleftvalue. (((((dc_left_solve_append_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_append_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_solve_append_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode. (((dc_left_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemaskentryleftvalue) = S ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemaskentryleft) + ge_balance_negative_solve_append_resultvaluemaskentryleftvalue = (dst_negative_solve_append_resultvaluemaskentryleft) + ge_balance_positive_solve_append_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_solve_append_resultvaluemaskentryright dst_positive_scale_solve_append_resultvaluemaskentryright dst_negative_code_solve_append_resultvaluemaskentryright dst_negative_scale_solve_append_resultvaluemaskentryright dst_positive_solve_append_resultvaluemaskentryright dst_negative_solve_append_resultvaluemaskentryright. (((F) = (((((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) * S ((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) + ((dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))) * S ((((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) * S ((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) + ((dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))) + ((((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryrightpositive. ff_h_pvs_solve_append_resultvaluemaskentryrightpositive + S (dst_positive_solve_append_resultvaluemaskentryright) = S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_positive_scale_solve_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryrightpositive. dst_positive_code_solve_append_resultvaluemaskentryright = ff_q_pvs_solve_append_resultvaluemaskentryrightpositive * S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_solve_append_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryrightnegative. ff_h_pvs_solve_append_resultvaluemaskentryrightnegative + S (dst_negative_solve_append_resultvaluemaskentryright) = S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_negative_scale_solve_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryrightnegative. dst_negative_code_solve_append_resultvaluemaskentryright = ff_q_pvs_solve_append_resultvaluemaskentryrightnegative * S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_solve_append_resultvaluemaskentryright))) /\ (exists ge_balance_positive_solve_append_resultvaluemaskentryrightvalue ge_balance_negative_solve_append_resultvaluemaskentryrightvalue. (((((dc_right_solve_append_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_append_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_solve_append_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode. (((dc_right_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemaskentryrightvalue) = S ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemaskentryright) + ge_balance_negative_solve_append_resultvaluemaskentryrightvalue = (dst_negative_solve_append_resultvaluemaskentryright) + ge_balance_positive_solve_append_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_solve_append_resultvaluemaskentryproduct sto_an_solve_append_resultvaluemaskentryproduct sto_bp_solve_append_resultvaluemaskentryproduct sto_bn_solve_append_resultvaluemaskentryproduct sto_cp_solve_append_resultvaluemaskentryproduct sto_cn_solve_append_resultvaluemaskentryproduct. (((((dc_left_solve_append_resultvaluemaskentry) = 2 * (sto_ap_solve_append_resultvaluemaskentryproduct) /\ (sto_an_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductleft. (((dc_left_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductleft + 1 /\ (sto_ap_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_an_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductleft))) /\ ((((((dc_right_solve_append_resultvaluemaskentry) = 2 * (sto_bp_solve_append_resultvaluemaskentryproduct) /\ (sto_bn_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductright. (((dc_right_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductright + 1 /\ (sto_bp_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_bn_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductright))) /\ ((((((dc_value_solve_append_resultvaluemask) = 2 * (sto_cp_solve_append_resultvaluemaskentryproduct) /\ (sto_cn_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductoutput. (((dc_value_solve_append_resultvaluemask) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_cn_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductoutput))) /\ ((sto_ap_solve_append_resultvaluemaskentryproduct * sto_bp_solve_append_resultvaluemaskentryproduct + sto_an_solve_append_resultvaluemaskentryproduct * sto_bn_solve_append_resultvaluemaskentryproduct) + sto_cn_solve_append_resultvaluemaskentryproduct = (sto_ap_solve_append_resultvaluemaskentryproduct * sto_bn_solve_append_resultvaluemaskentryproduct + sto_an_solve_append_resultvaluemaskentryproduct * sto_bp_solve_append_resultvaluemaskentryproduct) + sto_cp_solve_append_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_solve_append_resultvaluemask)=0 \/ ~(exists pvs_factor_solve_append_resultvaluemaskentrynondivisor. (dc_input_solve_append_result) = (dc_index_solve_append_resultvaluemask) * pvs_factor_solve_append_resultvaluemaskentrynondivisor)) /\ ((dc_value_solve_append_resultvaluemask)=0))))))) /\ (exists dst_positive_code_solve_append_resultvaluefold dst_positive_scale_solve_append_resultvaluefold dst_negative_code_solve_append_resultvaluefold dst_negative_scale_solve_append_resultvaluefold dst_positive_sum_solve_append_resultvaluefold dst_negative_sum_solve_append_resultvaluefold. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) * S ((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) + ((dst_positive_scale_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))) * S ((((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) * S ((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) + ((dst_positive_scale_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))) + ((((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))))) /\ (((exists fs_u_dst_solve_append_resultvaluefoldpositive fs_v_dst_solve_append_resultvaluefoldpositive. ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_start. fs_h_dst_solve_append_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_start. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_terminal. fs_h_dst_solve_append_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_solve_append_resultvaluefold) = S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_terminal. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldpositive) + (dst_positive_sum_solve_append_resultvaluefold))) /\ forall fs_i_dst_solve_append_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_solve_append_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_solve_append_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps = S (dc_input_solve_append_result)) -> exists fs_a_dst_solve_append_resultvaluefoldpositive_body_steps fs_r_dst_solve_append_resultvaluefoldpositive_body_steps fs_s_dst_solve_append_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_summand. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_resultvaluefold)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_summand. dst_positive_code_solve_append_resultvaluefold = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_resultvaluefold) + (fs_a_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_partial. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_partial. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (fs_r_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_successor. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_successor. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (fs_s_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_solve_append_resultvaluefoldpositive_body_steps = fs_r_dst_solve_append_resultvaluefoldpositive_body_steps + fs_a_dst_solve_append_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_solve_append_resultvaluefoldnegative fs_v_dst_solve_append_resultvaluefoldnegative. ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_start. fs_h_dst_solve_append_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_start. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_terminal. fs_h_dst_solve_append_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_solve_append_resultvaluefold) = S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_terminal. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldnegative) + (dst_negative_sum_solve_append_resultvaluefold))) /\ forall fs_i_dst_solve_append_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_solve_append_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_solve_append_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps = S (dc_input_solve_append_result)) -> exists fs_a_dst_solve_append_resultvaluefoldnegative_body_steps fs_r_dst_solve_append_resultvaluefoldnegative_body_steps fs_s_dst_solve_append_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_summand. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_resultvaluefold)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_summand. dst_negative_code_solve_append_resultvaluefold = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_resultvaluefold) + (fs_a_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_partial. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_partial. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (fs_r_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_successor. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_successor. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (fs_s_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_solve_append_resultvaluefoldnegative_body_steps = fs_r_dst_solve_append_resultvaluefoldnegative_body_steps + fs_a_dst_solve_append_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_solve_append_resultvaluefoldresult ge_balance_negative_solve_append_resultvaluefoldresult. (((((dc_output_solve_append_result) = 2 * (ge_balance_positive_solve_append_resultvaluefoldresult) /\ (ge_balance_negative_solve_append_resultvaluefoldresult) = 0) \/ exists ge_signed_half_solve_append_resultvaluefoldresultdecode. (((dc_output_solve_append_result) = 2 * ge_signed_half_solve_append_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_solve_append_resultvaluefoldresult) = 0) /\ (ge_balance_negative_solve_append_resultvaluefoldresult) = S ge_signed_half_solve_append_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_solve_append_resultvaluefold) + ge_balance_negative_solve_append_resultvaluefoldresult = (dst_negative_sum_solve_append_resultvaluefold) + ge_balance_positive_solve_append_resultvaluefoldresult)))))))))))))))))))) /\ (forall dst_index_solve_append_preserved dst_first_solve_append_preserved dst_second_solve_append_preserved. (exists pvs_gap_solve_append_preservedbound. pvs_gap_solve_append_preservedbound + S (dst_index_solve_append_preserved) = (S N)) -> (exists dst_positive_code_solve_append_preservedfirst dst_positive_scale_solve_append_preservedfirst dst_negative_code_solve_append_preservedfirst dst_negative_scale_solve_append_preservedfirst dst_positive_solve_append_preservedfirst dst_negative_solve_append_preservedfirst. (((G) = (((((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) * S ((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) + ((dst_positive_scale_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))) * S ((((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) * S ((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) + ((dst_positive_scale_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))) + ((((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))))) /\ (((((exists ff_h_pvs_solve_append_preservedfirstpositive. ff_h_pvs_solve_append_preservedfirstpositive + S (dst_positive_solve_append_preservedfirst) = S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedfirst)) /\ exists ff_q_pvs_solve_append_preservedfirstpositive. dst_positive_code_solve_append_preservedfirst = ff_q_pvs_solve_append_preservedfirstpositive * S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedfirst) + (dst_positive_solve_append_preservedfirst))) /\ (((((exists ff_h_pvs_solve_append_preservedfirstnegative. ff_h_pvs_solve_append_preservedfirstnegative + S (dst_negative_solve_append_preservedfirst) = S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedfirst)) /\ exists ff_q_pvs_solve_append_preservedfirstnegative. dst_negative_code_solve_append_preservedfirst = ff_q_pvs_solve_append_preservedfirstnegative * S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedfirst) + (dst_negative_solve_append_preservedfirst))) /\ (exists ge_balance_positive_solve_append_preservedfirstvalue ge_balance_negative_solve_append_preservedfirstvalue. (((((dst_first_solve_append_preserved) = 2 * (ge_balance_positive_solve_append_preservedfirstvalue) /\ (ge_balance_negative_solve_append_preservedfirstvalue) = 0) \/ exists ge_signed_half_solve_append_preservedfirstvaluedecode. (((dst_first_solve_append_preserved) = 2 * ge_signed_half_solve_append_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_solve_append_preservedfirstvalue) = 0) /\ (ge_balance_negative_solve_append_preservedfirstvalue) = S ge_signed_half_solve_append_preservedfirstvaluedecode))) /\ ((dst_positive_solve_append_preservedfirst) + ge_balance_negative_solve_append_preservedfirstvalue = (dst_negative_solve_append_preservedfirst) + ge_balance_positive_solve_append_preservedfirstvalue))))))))) -> (exists dst_positive_code_solve_append_preservedsecond dst_positive_scale_solve_append_preservedsecond dst_negative_code_solve_append_preservedsecond dst_negative_scale_solve_append_preservedsecond dst_positive_solve_append_preservedsecond dst_negative_solve_append_preservedsecond. (((H) = (((((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) * S ((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) + ((dst_positive_scale_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))) * S ((((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) * S ((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) + ((dst_positive_scale_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))) + ((((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))))) /\ (((((exists ff_h_pvs_solve_append_preservedsecondpositive. ff_h_pvs_solve_append_preservedsecondpositive + S (dst_positive_solve_append_preservedsecond) = S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedsecond)) /\ exists ff_q_pvs_solve_append_preservedsecondpositive. dst_positive_code_solve_append_preservedsecond = ff_q_pvs_solve_append_preservedsecondpositive * S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedsecond) + (dst_positive_solve_append_preservedsecond))) /\ (((((exists ff_h_pvs_solve_append_preservedsecondnegative. ff_h_pvs_solve_append_preservedsecondnegative + S (dst_negative_solve_append_preservedsecond) = S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedsecond)) /\ exists ff_q_pvs_solve_append_preservedsecondnegative. dst_negative_code_solve_append_preservedsecond = ff_q_pvs_solve_append_preservedsecondnegative * S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedsecond) + (dst_negative_solve_append_preservedsecond))) /\ (exists ge_balance_positive_solve_append_preservedsecondvalue ge_balance_negative_solve_append_preservedsecondvalue. (((((dst_second_solve_append_preserved) = 2 * (ge_balance_positive_solve_append_preservedsecondvalue) /\ (ge_balance_negative_solve_append_preservedsecondvalue) = 0) \/ exists ge_signed_half_solve_append_preservedsecondvaluedecode. (((dst_second_solve_append_preserved) = 2 * ge_signed_half_solve_append_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_solve_append_preservedsecondvalue) = 0) /\ (ge_balance_negative_solve_append_preservedsecondvalue) = S ge_signed_half_solve_append_preservedsecondvaluedecode))) /\ ((dst_positive_solve_append_preservedsecond) + ge_balance_negative_solve_append_preservedsecondvalue = (dst_negative_solve_append_preservedsecond) + ge_balance_positive_solve_append_preservedsecondvalue))))))))) -> dst_first_solve_append_preserved = dst_second_solve_append_preserved))