dirichlet_unit_equation_construct

Exact expanded first-order arithmetic statement

forall N F T u w. (exists dst_positive_code_solve_construct_F dst_positive_scale_solve_construct_F dst_negative_code_solve_construct_F dst_negative_scale_solve_construct_F. (((F) = (((((dst_positive_code_solve_construct_F) + (dst_positive_scale_solve_construct_F)) * S ((dst_positive_code_solve_construct_F) + (dst_positive_scale_solve_construct_F)) + ((dst_positive_scale_solve_construct_F) + (dst_positive_scale_solve_construct_F))) + (((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) * S ((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) + ((dst_negative_scale_solve_construct_F) + (dst_negative_scale_solve_construct_F)))) * S ((((dst_positive_code_solve_construct_F) + (dst_positive_scale_solve_construct_F)) * S ((dst_positive_code_solve_construct_F) + (dst_positive_scale_solve_construct_F)) + ((dst_positive_scale_solve_construct_F) + (dst_positive_scale_solve_construct_F))) + (((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) * S ((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) + ((dst_negative_scale_solve_construct_F) + (dst_negative_scale_solve_construct_F)))) + ((((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) * S ((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) + ((dst_negative_scale_solve_construct_F) + (dst_negative_scale_solve_construct_F))) + (((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) * S ((dst_negative_code_solve_construct_F) + (dst_negative_scale_solve_construct_F)) + ((dst_negative_scale_solve_construct_F) + (dst_negative_scale_solve_construct_F)))))) /\ (forall dst_index_solve_construct_F. (exists pvs_le_gap_solve_construct_Fdomain. pvs_le_gap_solve_construct_Fdomain + (dst_index_solve_construct_F) = (N)) -> exists dst_positive_solve_construct_F dst_negative_solve_construct_F dst_value_solve_construct_F. ((((exists ff_h_pvs_solve_construct_Fentrypositive. ff_h_pvs_solve_construct_Fentrypositive + S (dst_positive_solve_construct_F) = S ((S (dst_index_solve_construct_F)) * dst_positive_scale_solve_construct_F)) /\ exists ff_q_pvs_solve_construct_Fentrypositive. dst_positive_code_solve_construct_F = ff_q_pvs_solve_construct_Fentrypositive * S ((S (dst_index_solve_construct_F)) * dst_positive_scale_solve_construct_F) + (dst_positive_solve_construct_F))) /\ (((((exists ff_h_pvs_solve_construct_Fentrynegative. ff_h_pvs_solve_construct_Fentrynegative + S (dst_negative_solve_construct_F) = S ((S (dst_index_solve_construct_F)) * dst_negative_scale_solve_construct_F)) /\ exists ff_q_pvs_solve_construct_Fentrynegative. dst_negative_code_solve_construct_F = ff_q_pvs_solve_construct_Fentrynegative * S ((S (dst_index_solve_construct_F)) * dst_negative_scale_solve_construct_F) + (dst_negative_solve_construct_F))) /\ (exists ge_balance_positive_solve_construct_Fentryvalue ge_balance_negative_solve_construct_Fentryvalue. (((((dst_value_solve_construct_F) = 2 * (ge_balance_positive_solve_construct_Fentryvalue) /\ (ge_balance_negative_solve_construct_Fentryvalue) = 0) \/ exists ge_signed_half_solve_construct_Fentryvaluedecode. (((dst_value_solve_construct_F) = 2 * ge_signed_half_solve_construct_Fentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_Fentryvalue) = 0) /\ (ge_balance_negative_solve_construct_Fentryvalue) = S ge_signed_half_solve_construct_Fentryvaluedecode))) /\ ((dst_positive_solve_construct_F) + ge_balance_negative_solve_construct_Fentryvalue = (dst_negative_solve_construct_F) + ge_balance_positive_solve_construct_Fentryvalue))))))))) -> (exists dst_positive_code_solve_construct_T dst_positive_scale_solve_construct_T dst_negative_code_solve_construct_T dst_negative_scale_solve_construct_T. (((T) = (((((dst_positive_code_solve_construct_T) + (dst_positive_scale_solve_construct_T)) * S ((dst_positive_code_solve_construct_T) + (dst_positive_scale_solve_construct_T)) + ((dst_positive_scale_solve_construct_T) + (dst_positive_scale_solve_construct_T))) + (((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) * S ((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) + ((dst_negative_scale_solve_construct_T) + (dst_negative_scale_solve_construct_T)))) * S ((((dst_positive_code_solve_construct_T) + (dst_positive_scale_solve_construct_T)) * S ((dst_positive_code_solve_construct_T) + (dst_positive_scale_solve_construct_T)) + ((dst_positive_scale_solve_construct_T) + (dst_positive_scale_solve_construct_T))) + (((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) * S ((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) + ((dst_negative_scale_solve_construct_T) + (dst_negative_scale_solve_construct_T)))) + ((((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) * S ((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) + ((dst_negative_scale_solve_construct_T) + (dst_negative_scale_solve_construct_T))) + (((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) * S ((dst_negative_code_solve_construct_T) + (dst_negative_scale_solve_construct_T)) + ((dst_negative_scale_solve_construct_T) + (dst_negative_scale_solve_construct_T)))))) /\ (forall dst_index_solve_construct_T. (exists pvs_le_gap_solve_construct_Tdomain. pvs_le_gap_solve_construct_Tdomain + (dst_index_solve_construct_T) = (N)) -> exists dst_positive_solve_construct_T dst_negative_solve_construct_T dst_value_solve_construct_T. ((((exists ff_h_pvs_solve_construct_Tentrypositive. ff_h_pvs_solve_construct_Tentrypositive + S (dst_positive_solve_construct_T) = S ((S (dst_index_solve_construct_T)) * dst_positive_scale_solve_construct_T)) /\ exists ff_q_pvs_solve_construct_Tentrypositive. dst_positive_code_solve_construct_T = ff_q_pvs_solve_construct_Tentrypositive * S ((S (dst_index_solve_construct_T)) * dst_positive_scale_solve_construct_T) + (dst_positive_solve_construct_T))) /\ (((((exists ff_h_pvs_solve_construct_Tentrynegative. ff_h_pvs_solve_construct_Tentrynegative + S (dst_negative_solve_construct_T) = S ((S (dst_index_solve_construct_T)) * dst_negative_scale_solve_construct_T)) /\ exists ff_q_pvs_solve_construct_Tentrynegative. dst_negative_code_solve_construct_T = ff_q_pvs_solve_construct_Tentrynegative * S ((S (dst_index_solve_construct_T)) * dst_negative_scale_solve_construct_T) + (dst_negative_solve_construct_T))) /\ (exists ge_balance_positive_solve_construct_Tentryvalue ge_balance_negative_solve_construct_Tentryvalue. (((((dst_value_solve_construct_T) = 2 * (ge_balance_positive_solve_construct_Tentryvalue) /\ (ge_balance_negative_solve_construct_Tentryvalue) = 0) \/ exists ge_signed_half_solve_construct_Tentryvaluedecode. (((dst_value_solve_construct_T) = 2 * ge_signed_half_solve_construct_Tentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_Tentryvalue) = 0) /\ (ge_balance_negative_solve_construct_Tentryvalue) = S ge_signed_half_solve_construct_Tentryvaluedecode))) /\ ((dst_positive_solve_construct_T) + ge_balance_negative_solve_construct_Tentryvalue = (dst_negative_solve_construct_T) + ge_balance_positive_solve_construct_Tentryvalue))))))))) -> (exists dst_positive_code_solve_construct_coefficient dst_positive_scale_solve_construct_coefficient dst_negative_code_solve_construct_coefficient dst_negative_scale_solve_construct_coefficient dst_positive_solve_construct_coefficient dst_negative_solve_construct_coefficient. (((F) = (((((dst_positive_code_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient)) * S ((dst_positive_code_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient)) + ((dst_positive_scale_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient))) + (((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) * S ((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) + ((dst_negative_scale_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)))) * S ((((dst_positive_code_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient)) * S ((dst_positive_code_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient)) + ((dst_positive_scale_solve_construct_coefficient) + (dst_positive_scale_solve_construct_coefficient))) + (((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) * S ((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) + ((dst_negative_scale_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)))) + ((((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) * S ((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) + ((dst_negative_scale_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient))) + (((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) * S ((dst_negative_code_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)) + ((dst_negative_scale_solve_construct_coefficient) + (dst_negative_scale_solve_construct_coefficient)))))) /\ (((((exists ff_h_pvs_solve_construct_coefficientpositive. ff_h_pvs_solve_construct_coefficientpositive + S (dst_positive_solve_construct_coefficient) = S ((S (1)) * dst_positive_scale_solve_construct_coefficient)) /\ exists ff_q_pvs_solve_construct_coefficientpositive. dst_positive_code_solve_construct_coefficient = ff_q_pvs_solve_construct_coefficientpositive * S ((S (1)) * dst_positive_scale_solve_construct_coefficient) + (dst_positive_solve_construct_coefficient))) /\ (((((exists ff_h_pvs_solve_construct_coefficientnegative. ff_h_pvs_solve_construct_coefficientnegative + S (dst_negative_solve_construct_coefficient) = S ((S (1)) * dst_negative_scale_solve_construct_coefficient)) /\ exists ff_q_pvs_solve_construct_coefficientnegative. dst_negative_code_solve_construct_coefficient = ff_q_pvs_solve_construct_coefficientnegative * S ((S (1)) * dst_negative_scale_solve_construct_coefficient) + (dst_negative_solve_construct_coefficient))) /\ (exists ge_balance_positive_solve_construct_coefficientvalue ge_balance_negative_solve_construct_coefficientvalue. (((((u) = 2 * (ge_balance_positive_solve_construct_coefficientvalue) /\ (ge_balance_negative_solve_construct_coefficientvalue) = 0) \/ exists ge_signed_half_solve_construct_coefficientvaluedecode. (((u) = 2 * ge_signed_half_solve_construct_coefficientvaluedecode + 1 /\ (ge_balance_positive_solve_construct_coefficientvalue) = 0) /\ (ge_balance_negative_solve_construct_coefficientvalue) = S ge_signed_half_solve_construct_coefficientvaluedecode))) /\ ((dst_positive_solve_construct_coefficient) + ge_balance_negative_solve_construct_coefficientvalue = (dst_negative_solve_construct_coefficient) + ge_balance_positive_solve_construct_coefficientvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> exists G. ((((exists dst_positive_code_solve_construct_resultleft dst_positive_scale_solve_construct_resultleft dst_negative_code_solve_construct_resultleft dst_negative_scale_solve_construct_resultleft. (((G) = (((((dst_positive_code_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft)) * S ((dst_positive_code_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft)) + ((dst_positive_scale_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft))) + (((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) * S ((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) + ((dst_negative_scale_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)))) * S ((((dst_positive_code_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft)) * S ((dst_positive_code_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft)) + ((dst_positive_scale_solve_construct_resultleft) + (dst_positive_scale_solve_construct_resultleft))) + (((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) * S ((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) + ((dst_negative_scale_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)))) + ((((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) * S ((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) + ((dst_negative_scale_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft))) + (((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) * S ((dst_negative_code_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)) + ((dst_negative_scale_solve_construct_resultleft) + (dst_negative_scale_solve_construct_resultleft)))))) /\ (forall dst_index_solve_construct_resultleft. (exists pvs_le_gap_solve_construct_resultleftdomain. pvs_le_gap_solve_construct_resultleftdomain + (dst_index_solve_construct_resultleft) = (N)) -> exists dst_positive_solve_construct_resultleft dst_negative_solve_construct_resultleft dst_value_solve_construct_resultleft. ((((exists ff_h_pvs_solve_construct_resultleftentrypositive. ff_h_pvs_solve_construct_resultleftentrypositive + S (dst_positive_solve_construct_resultleft) = S ((S (dst_index_solve_construct_resultleft)) * dst_positive_scale_solve_construct_resultleft)) /\ exists ff_q_pvs_solve_construct_resultleftentrypositive. dst_positive_code_solve_construct_resultleft = ff_q_pvs_solve_construct_resultleftentrypositive * S ((S (dst_index_solve_construct_resultleft)) * dst_positive_scale_solve_construct_resultleft) + (dst_positive_solve_construct_resultleft))) /\ (((((exists ff_h_pvs_solve_construct_resultleftentrynegative. ff_h_pvs_solve_construct_resultleftentrynegative + S (dst_negative_solve_construct_resultleft) = S ((S (dst_index_solve_construct_resultleft)) * dst_negative_scale_solve_construct_resultleft)) /\ exists ff_q_pvs_solve_construct_resultleftentrynegative. dst_negative_code_solve_construct_resultleft = ff_q_pvs_solve_construct_resultleftentrynegative * S ((S (dst_index_solve_construct_resultleft)) * dst_negative_scale_solve_construct_resultleft) + (dst_negative_solve_construct_resultleft))) /\ (exists ge_balance_positive_solve_construct_resultleftentryvalue ge_balance_negative_solve_construct_resultleftentryvalue. (((((dst_value_solve_construct_resultleft) = 2 * (ge_balance_positive_solve_construct_resultleftentryvalue) /\ (ge_balance_negative_solve_construct_resultleftentryvalue) = 0) \/ exists ge_signed_half_solve_construct_resultleftentryvaluedecode. (((dst_value_solve_construct_resultleft) = 2 * ge_signed_half_solve_construct_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultleftentryvalue) = 0) /\ (ge_balance_negative_solve_construct_resultleftentryvalue) = S ge_signed_half_solve_construct_resultleftentryvaluedecode))) /\ ((dst_positive_solve_construct_resultleft) + ge_balance_negative_solve_construct_resultleftentryvalue = (dst_negative_solve_construct_resultleft) + ge_balance_positive_solve_construct_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_solve_construct_resultright dst_positive_scale_solve_construct_resultright dst_negative_code_solve_construct_resultright dst_negative_scale_solve_construct_resultright. (((F) = (((((dst_positive_code_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright)) * S ((dst_positive_code_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright)) + ((dst_positive_scale_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright))) + (((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) * S ((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) + ((dst_negative_scale_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)))) * S ((((dst_positive_code_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright)) * S ((dst_positive_code_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright)) + ((dst_positive_scale_solve_construct_resultright) + (dst_positive_scale_solve_construct_resultright))) + (((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) * S ((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) + ((dst_negative_scale_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)))) + ((((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) * S ((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) + ((dst_negative_scale_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright))) + (((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) * S ((dst_negative_code_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)) + ((dst_negative_scale_solve_construct_resultright) + (dst_negative_scale_solve_construct_resultright)))))) /\ (forall dst_index_solve_construct_resultright. (exists pvs_le_gap_solve_construct_resultrightdomain. pvs_le_gap_solve_construct_resultrightdomain + (dst_index_solve_construct_resultright) = (N)) -> exists dst_positive_solve_construct_resultright dst_negative_solve_construct_resultright dst_value_solve_construct_resultright. ((((exists ff_h_pvs_solve_construct_resultrightentrypositive. ff_h_pvs_solve_construct_resultrightentrypositive + S (dst_positive_solve_construct_resultright) = S ((S (dst_index_solve_construct_resultright)) * dst_positive_scale_solve_construct_resultright)) /\ exists ff_q_pvs_solve_construct_resultrightentrypositive. dst_positive_code_solve_construct_resultright = ff_q_pvs_solve_construct_resultrightentrypositive * S ((S (dst_index_solve_construct_resultright)) * dst_positive_scale_solve_construct_resultright) + (dst_positive_solve_construct_resultright))) /\ (((((exists ff_h_pvs_solve_construct_resultrightentrynegative. ff_h_pvs_solve_construct_resultrightentrynegative + S (dst_negative_solve_construct_resultright) = S ((S (dst_index_solve_construct_resultright)) * dst_negative_scale_solve_construct_resultright)) /\ exists ff_q_pvs_solve_construct_resultrightentrynegative. dst_negative_code_solve_construct_resultright = ff_q_pvs_solve_construct_resultrightentrynegative * S ((S (dst_index_solve_construct_resultright)) * dst_negative_scale_solve_construct_resultright) + (dst_negative_solve_construct_resultright))) /\ (exists ge_balance_positive_solve_construct_resultrightentryvalue ge_balance_negative_solve_construct_resultrightentryvalue. (((((dst_value_solve_construct_resultright) = 2 * (ge_balance_positive_solve_construct_resultrightentryvalue) /\ (ge_balance_negative_solve_construct_resultrightentryvalue) = 0) \/ exists ge_signed_half_solve_construct_resultrightentryvaluedecode. (((dst_value_solve_construct_resultright) = 2 * ge_signed_half_solve_construct_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultrightentryvalue) = 0) /\ (ge_balance_negative_solve_construct_resultrightentryvalue) = S ge_signed_half_solve_construct_resultrightentryvaluedecode))) /\ ((dst_positive_solve_construct_resultright) + ge_balance_negative_solve_construct_resultrightentryvalue = (dst_negative_solve_construct_resultright) + ge_balance_positive_solve_construct_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_solve_construct_resulttable dst_positive_scale_solve_construct_resulttable dst_negative_code_solve_construct_resulttable dst_negative_scale_solve_construct_resulttable. (((T) = (((((dst_positive_code_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable)) * S ((dst_positive_code_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable)) + ((dst_positive_scale_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable))) + (((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) * S ((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) + ((dst_negative_scale_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)))) * S ((((dst_positive_code_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable)) * S ((dst_positive_code_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable)) + ((dst_positive_scale_solve_construct_resulttable) + (dst_positive_scale_solve_construct_resulttable))) + (((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) * S ((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) + ((dst_negative_scale_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)))) + ((((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) * S ((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) + ((dst_negative_scale_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable))) + (((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) * S ((dst_negative_code_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)) + ((dst_negative_scale_solve_construct_resulttable) + (dst_negative_scale_solve_construct_resulttable)))))) /\ (forall dst_index_solve_construct_resulttable. (exists pvs_le_gap_solve_construct_resulttabledomain. pvs_le_gap_solve_construct_resulttabledomain + (dst_index_solve_construct_resulttable) = (N)) -> exists dst_positive_solve_construct_resulttable dst_negative_solve_construct_resulttable dst_value_solve_construct_resulttable. ((((exists ff_h_pvs_solve_construct_resulttableentrypositive. ff_h_pvs_solve_construct_resulttableentrypositive + S (dst_positive_solve_construct_resulttable) = S ((S (dst_index_solve_construct_resulttable)) * dst_positive_scale_solve_construct_resulttable)) /\ exists ff_q_pvs_solve_construct_resulttableentrypositive. dst_positive_code_solve_construct_resulttable = ff_q_pvs_solve_construct_resulttableentrypositive * S ((S (dst_index_solve_construct_resulttable)) * dst_positive_scale_solve_construct_resulttable) + (dst_positive_solve_construct_resulttable))) /\ (((((exists ff_h_pvs_solve_construct_resulttableentrynegative. ff_h_pvs_solve_construct_resulttableentrynegative + S (dst_negative_solve_construct_resulttable) = S ((S (dst_index_solve_construct_resulttable)) * dst_negative_scale_solve_construct_resulttable)) /\ exists ff_q_pvs_solve_construct_resulttableentrynegative. dst_negative_code_solve_construct_resulttable = ff_q_pvs_solve_construct_resulttableentrynegative * S ((S (dst_index_solve_construct_resulttable)) * dst_negative_scale_solve_construct_resulttable) + (dst_negative_solve_construct_resulttable))) /\ (exists ge_balance_positive_solve_construct_resulttableentryvalue ge_balance_negative_solve_construct_resulttableentryvalue. (((((dst_value_solve_construct_resulttable) = 2 * (ge_balance_positive_solve_construct_resulttableentryvalue) /\ (ge_balance_negative_solve_construct_resulttableentryvalue) = 0) \/ exists ge_signed_half_solve_construct_resulttableentryvaluedecode. (((dst_value_solve_construct_resulttable) = 2 * ge_signed_half_solve_construct_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resulttableentryvalue) = 0) /\ (ge_balance_negative_solve_construct_resulttableentryvalue) = S ge_signed_half_solve_construct_resulttableentryvaluedecode))) /\ ((dst_positive_solve_construct_resulttable) + ge_balance_negative_solve_construct_resulttableentryvalue = (dst_negative_solve_construct_resulttable) + ge_balance_positive_solve_construct_resulttableentryvalue))))))))) /\ (forall dc_input_solve_construct_result dc_output_solve_construct_result. ~(dc_input_solve_construct_result=0) -> (exists pvs_le_gap_solve_construct_resultdomain. pvs_le_gap_solve_construct_resultdomain + (dc_input_solve_construct_result) = (N)) -> (exists dst_positive_code_solve_construct_resultlookup dst_positive_scale_solve_construct_resultlookup dst_negative_code_solve_construct_resultlookup dst_negative_scale_solve_construct_resultlookup dst_positive_solve_construct_resultlookup dst_negative_solve_construct_resultlookup. (((T) = (((((dst_positive_code_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup)) * S ((dst_positive_code_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup)) + ((dst_positive_scale_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup))) + (((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) * S ((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) + ((dst_negative_scale_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)))) * S ((((dst_positive_code_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup)) * S ((dst_positive_code_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup)) + ((dst_positive_scale_solve_construct_resultlookup) + (dst_positive_scale_solve_construct_resultlookup))) + (((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) * S ((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) + ((dst_negative_scale_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)))) + ((((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) * S ((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) + ((dst_negative_scale_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup))) + (((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) * S ((dst_negative_code_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)) + ((dst_negative_scale_solve_construct_resultlookup) + (dst_negative_scale_solve_construct_resultlookup)))))) /\ (((((exists ff_h_pvs_solve_construct_resultlookuppositive. ff_h_pvs_solve_construct_resultlookuppositive + S (dst_positive_solve_construct_resultlookup) = S ((S (dc_input_solve_construct_result)) * dst_positive_scale_solve_construct_resultlookup)) /\ exists ff_q_pvs_solve_construct_resultlookuppositive. dst_positive_code_solve_construct_resultlookup = ff_q_pvs_solve_construct_resultlookuppositive * S ((S (dc_input_solve_construct_result)) * dst_positive_scale_solve_construct_resultlookup) + (dst_positive_solve_construct_resultlookup))) /\ (((((exists ff_h_pvs_solve_construct_resultlookupnegative. ff_h_pvs_solve_construct_resultlookupnegative + S (dst_negative_solve_construct_resultlookup) = S ((S (dc_input_solve_construct_result)) * dst_negative_scale_solve_construct_resultlookup)) /\ exists ff_q_pvs_solve_construct_resultlookupnegative. dst_negative_code_solve_construct_resultlookup = ff_q_pvs_solve_construct_resultlookupnegative * S ((S (dc_input_solve_construct_result)) * dst_negative_scale_solve_construct_resultlookup) + (dst_negative_solve_construct_resultlookup))) /\ (exists ge_balance_positive_solve_construct_resultlookupvalue ge_balance_negative_solve_construct_resultlookupvalue. (((((dc_output_solve_construct_result) = 2 * (ge_balance_positive_solve_construct_resultlookupvalue) /\ (ge_balance_negative_solve_construct_resultlookupvalue) = 0) \/ exists ge_signed_half_solve_construct_resultlookupvaluedecode. (((dc_output_solve_construct_result) = 2 * ge_signed_half_solve_construct_resultlookupvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultlookupvalue) = 0) /\ (ge_balance_negative_solve_construct_resultlookupvalue) = S ge_signed_half_solve_construct_resultlookupvaluedecode))) /\ ((dst_positive_solve_construct_resultlookup) + ge_balance_negative_solve_construct_resultlookupvalue = (dst_negative_solve_construct_resultlookup) + ge_balance_positive_solve_construct_resultlookupvalue))))))))) -> (((~((dc_input_solve_construct_result)=0)) /\ (exists dc_mask_solve_construct_resultvalue. ((((exists dst_positive_code_solve_construct_resultvaluemasktable dst_positive_scale_solve_construct_resultvaluemasktable dst_negative_code_solve_construct_resultvaluemasktable dst_negative_scale_solve_construct_resultvaluemasktable. (((dc_mask_solve_construct_resultvalue) = (((((dst_positive_code_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable)) * S ((dst_positive_code_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable)) + ((dst_positive_scale_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable))) + (((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) * S ((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) + ((dst_negative_scale_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)))) * S ((((dst_positive_code_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable)) * S ((dst_positive_code_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable)) + ((dst_positive_scale_solve_construct_resultvaluemasktable) + (dst_positive_scale_solve_construct_resultvaluemasktable))) + (((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) * S ((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) + ((dst_negative_scale_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)))) + ((((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) * S ((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) + ((dst_negative_scale_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable))) + (((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) * S ((dst_negative_code_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)) + ((dst_negative_scale_solve_construct_resultvaluemasktable) + (dst_negative_scale_solve_construct_resultvaluemasktable)))))) /\ (forall dst_index_solve_construct_resultvaluemasktable. (exists pvs_le_gap_solve_construct_resultvaluemasktabledomain. pvs_le_gap_solve_construct_resultvaluemasktabledomain + (dst_index_solve_construct_resultvaluemasktable) = (dc_input_solve_construct_result)) -> exists dst_positive_solve_construct_resultvaluemasktable dst_negative_solve_construct_resultvaluemasktable dst_value_solve_construct_resultvaluemasktable. ((((exists ff_h_pvs_solve_construct_resultvaluemasktableentrypositive. ff_h_pvs_solve_construct_resultvaluemasktableentrypositive + S (dst_positive_solve_construct_resultvaluemasktable) = S ((S (dst_index_solve_construct_resultvaluemasktable)) * dst_positive_scale_solve_construct_resultvaluemasktable)) /\ exists ff_q_pvs_solve_construct_resultvaluemasktableentrypositive. dst_positive_code_solve_construct_resultvaluemasktable = ff_q_pvs_solve_construct_resultvaluemasktableentrypositive * S ((S (dst_index_solve_construct_resultvaluemasktable)) * dst_positive_scale_solve_construct_resultvaluemasktable) + (dst_positive_solve_construct_resultvaluemasktable))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemasktableentrynegative. ff_h_pvs_solve_construct_resultvaluemasktableentrynegative + S (dst_negative_solve_construct_resultvaluemasktable) = S ((S (dst_index_solve_construct_resultvaluemasktable)) * dst_negative_scale_solve_construct_resultvaluemasktable)) /\ exists ff_q_pvs_solve_construct_resultvaluemasktableentrynegative. dst_negative_code_solve_construct_resultvaluemasktable = ff_q_pvs_solve_construct_resultvaluemasktableentrynegative * S ((S (dst_index_solve_construct_resultvaluemasktable)) * dst_negative_scale_solve_construct_resultvaluemasktable) + (dst_negative_solve_construct_resultvaluemasktable))) /\ (exists ge_balance_positive_solve_construct_resultvaluemasktableentryvalue ge_balance_negative_solve_construct_resultvaluemasktableentryvalue. (((((dst_value_solve_construct_resultvaluemasktable) = 2 * (ge_balance_positive_solve_construct_resultvaluemasktableentryvalue) /\ (ge_balance_negative_solve_construct_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemasktableentryvaluedecode. (((dst_value_solve_construct_resultvaluemasktable) = 2 * ge_signed_half_solve_construct_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_solve_construct_resultvaluemasktableentryvalue) = S ge_signed_half_solve_construct_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_solve_construct_resultvaluemasktable) + ge_balance_negative_solve_construct_resultvaluemasktableentryvalue = (dst_negative_solve_construct_resultvaluemasktable) + ge_balance_positive_solve_construct_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_solve_construct_resultvaluemask dc_value_solve_construct_resultvaluemask. (exists pvs_le_gap_solve_construct_resultvaluemaskdomain. pvs_le_gap_solve_construct_resultvaluemaskdomain + (dc_index_solve_construct_resultvaluemask) = (dc_input_solve_construct_result)) -> (exists dst_positive_code_solve_construct_resultvaluemasklookup dst_positive_scale_solve_construct_resultvaluemasklookup dst_negative_code_solve_construct_resultvaluemasklookup dst_negative_scale_solve_construct_resultvaluemasklookup dst_positive_solve_construct_resultvaluemasklookup dst_negative_solve_construct_resultvaluemasklookup. (((dc_mask_solve_construct_resultvalue) = (((((dst_positive_code_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup)) * S ((dst_positive_code_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup)) + ((dst_positive_scale_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup))) + (((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) * S ((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) + ((dst_negative_scale_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)))) * S ((((dst_positive_code_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup)) * S ((dst_positive_code_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup)) + ((dst_positive_scale_solve_construct_resultvaluemasklookup) + (dst_positive_scale_solve_construct_resultvaluemasklookup))) + (((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) * S ((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) + ((dst_negative_scale_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)))) + ((((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) * S ((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) + ((dst_negative_scale_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup))) + (((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) * S ((dst_negative_code_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)) + ((dst_negative_scale_solve_construct_resultvaluemasklookup) + (dst_negative_scale_solve_construct_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemasklookuppositive. ff_h_pvs_solve_construct_resultvaluemasklookuppositive + S (dst_positive_solve_construct_resultvaluemasklookup) = S ((S (dc_index_solve_construct_resultvaluemask)) * dst_positive_scale_solve_construct_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_construct_resultvaluemasklookuppositive. dst_positive_code_solve_construct_resultvaluemasklookup = ff_q_pvs_solve_construct_resultvaluemasklookuppositive * S ((S (dc_index_solve_construct_resultvaluemask)) * dst_positive_scale_solve_construct_resultvaluemasklookup) + (dst_positive_solve_construct_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemasklookupnegative. ff_h_pvs_solve_construct_resultvaluemasklookupnegative + S (dst_negative_solve_construct_resultvaluemasklookup) = S ((S (dc_index_solve_construct_resultvaluemask)) * dst_negative_scale_solve_construct_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_construct_resultvaluemasklookupnegative. dst_negative_code_solve_construct_resultvaluemasklookup = ff_q_pvs_solve_construct_resultvaluemasklookupnegative * S ((S (dc_index_solve_construct_resultvaluemask)) * dst_negative_scale_solve_construct_resultvaluemasklookup) + (dst_negative_solve_construct_resultvaluemasklookup))) /\ (exists ge_balance_positive_solve_construct_resultvaluemasklookupvalue ge_balance_negative_solve_construct_resultvaluemasklookupvalue. (((((dc_value_solve_construct_resultvaluemask) = 2 * (ge_balance_positive_solve_construct_resultvaluemasklookupvalue) /\ (ge_balance_negative_solve_construct_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemasklookupvaluedecode. (((dc_value_solve_construct_resultvaluemask) = 2 * ge_signed_half_solve_construct_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_solve_construct_resultvaluemasklookupvalue) = S ge_signed_half_solve_construct_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_solve_construct_resultvaluemasklookup) + ge_balance_negative_solve_construct_resultvaluemasklookupvalue = (dst_negative_solve_construct_resultvaluemasklookup) + ge_balance_positive_solve_construct_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_solve_construct_resultvaluemask)=0)) /\ (exists dc_quotient_solve_construct_resultvaluemaskentry dc_left_solve_construct_resultvaluemaskentry dc_right_solve_construct_resultvaluemaskentry. (((dc_input_solve_construct_result)=(dc_index_solve_construct_resultvaluemask)*dc_quotient_solve_construct_resultvaluemaskentry) /\ (((exists dst_positive_code_solve_construct_resultvaluemaskentryleft dst_positive_scale_solve_construct_resultvaluemaskentryleft dst_negative_code_solve_construct_resultvaluemaskentryleft dst_negative_scale_solve_construct_resultvaluemaskentryleft dst_positive_solve_construct_resultvaluemaskentryleft dst_negative_solve_construct_resultvaluemaskentryleft. (((G) = (((((dst_positive_code_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft))) + (((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)))) * S ((((dst_positive_code_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_construct_resultvaluemaskentryleft) + (dst_positive_scale_solve_construct_resultvaluemaskentryleft))) + (((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)))) + ((((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft))) + (((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryleft) + (dst_negative_scale_solve_construct_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemaskentryleftpositive. ff_h_pvs_solve_construct_resultvaluemaskentryleftpositive + S (dst_positive_solve_construct_resultvaluemaskentryleft) = S ((S (dc_index_solve_construct_resultvaluemask)) * dst_positive_scale_solve_construct_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_construct_resultvaluemaskentryleftpositive. dst_positive_code_solve_construct_resultvaluemaskentryleft = ff_q_pvs_solve_construct_resultvaluemaskentryleftpositive * S ((S (dc_index_solve_construct_resultvaluemask)) * dst_positive_scale_solve_construct_resultvaluemaskentryleft) + (dst_positive_solve_construct_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemaskentryleftnegative. ff_h_pvs_solve_construct_resultvaluemaskentryleftnegative + S (dst_negative_solve_construct_resultvaluemaskentryleft) = S ((S (dc_index_solve_construct_resultvaluemask)) * dst_negative_scale_solve_construct_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_construct_resultvaluemaskentryleftnegative. dst_negative_code_solve_construct_resultvaluemaskentryleft = ff_q_pvs_solve_construct_resultvaluemaskentryleftnegative * S ((S (dc_index_solve_construct_resultvaluemask)) * dst_negative_scale_solve_construct_resultvaluemaskentryleft) + (dst_negative_solve_construct_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_solve_construct_resultvaluemaskentryleftvalue ge_balance_negative_solve_construct_resultvaluemaskentryleftvalue. (((((dc_left_solve_construct_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_construct_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_solve_construct_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemaskentryleftvaluedecode. (((dc_left_solve_construct_resultvaluemaskentry) = 2 * ge_signed_half_solve_construct_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_solve_construct_resultvaluemaskentryleftvalue) = S ge_signed_half_solve_construct_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_solve_construct_resultvaluemaskentryleft) + ge_balance_negative_solve_construct_resultvaluemaskentryleftvalue = (dst_negative_solve_construct_resultvaluemaskentryleft) + ge_balance_positive_solve_construct_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_solve_construct_resultvaluemaskentryright dst_positive_scale_solve_construct_resultvaluemaskentryright dst_negative_code_solve_construct_resultvaluemaskentryright dst_negative_scale_solve_construct_resultvaluemaskentryright dst_positive_solve_construct_resultvaluemaskentryright dst_negative_solve_construct_resultvaluemaskentryright. (((F) = (((((dst_positive_code_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_positive_code_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright)) + ((dst_positive_scale_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright))) + (((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)))) * S ((((dst_positive_code_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_positive_code_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright)) + ((dst_positive_scale_solve_construct_resultvaluemaskentryright) + (dst_positive_scale_solve_construct_resultvaluemaskentryright))) + (((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)))) + ((((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright))) + (((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) * S ((dst_negative_code_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)) + ((dst_negative_scale_solve_construct_resultvaluemaskentryright) + (dst_negative_scale_solve_construct_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemaskentryrightpositive. ff_h_pvs_solve_construct_resultvaluemaskentryrightpositive + S (dst_positive_solve_construct_resultvaluemaskentryright) = S ((S (dc_quotient_solve_construct_resultvaluemaskentry)) * dst_positive_scale_solve_construct_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_construct_resultvaluemaskentryrightpositive. dst_positive_code_solve_construct_resultvaluemaskentryright = ff_q_pvs_solve_construct_resultvaluemaskentryrightpositive * S ((S (dc_quotient_solve_construct_resultvaluemaskentry)) * dst_positive_scale_solve_construct_resultvaluemaskentryright) + (dst_positive_solve_construct_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_solve_construct_resultvaluemaskentryrightnegative. ff_h_pvs_solve_construct_resultvaluemaskentryrightnegative + S (dst_negative_solve_construct_resultvaluemaskentryright) = S ((S (dc_quotient_solve_construct_resultvaluemaskentry)) * dst_negative_scale_solve_construct_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_construct_resultvaluemaskentryrightnegative. dst_negative_code_solve_construct_resultvaluemaskentryright = ff_q_pvs_solve_construct_resultvaluemaskentryrightnegative * S ((S (dc_quotient_solve_construct_resultvaluemaskentry)) * dst_negative_scale_solve_construct_resultvaluemaskentryright) + (dst_negative_solve_construct_resultvaluemaskentryright))) /\ (exists ge_balance_positive_solve_construct_resultvaluemaskentryrightvalue ge_balance_negative_solve_construct_resultvaluemaskentryrightvalue. (((((dc_right_solve_construct_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_construct_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_solve_construct_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemaskentryrightvaluedecode. (((dc_right_solve_construct_resultvaluemaskentry) = 2 * ge_signed_half_solve_construct_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_solve_construct_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_solve_construct_resultvaluemaskentryrightvalue) = S ge_signed_half_solve_construct_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_solve_construct_resultvaluemaskentryright) + ge_balance_negative_solve_construct_resultvaluemaskentryrightvalue = (dst_negative_solve_construct_resultvaluemaskentryright) + ge_balance_positive_solve_construct_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_solve_construct_resultvaluemaskentryproduct sto_an_solve_construct_resultvaluemaskentryproduct sto_bp_solve_construct_resultvaluemaskentryproduct sto_bn_solve_construct_resultvaluemaskentryproduct sto_cp_solve_construct_resultvaluemaskentryproduct sto_cn_solve_construct_resultvaluemaskentryproduct. (((((dc_left_solve_construct_resultvaluemaskentry) = 2 * (sto_ap_solve_construct_resultvaluemaskentryproduct) /\ (sto_an_solve_construct_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemaskentryproductleft. (((dc_left_solve_construct_resultvaluemaskentry) = 2 * ge_signed_half_solve_construct_resultvaluemaskentryproductleft + 1 /\ (sto_ap_solve_construct_resultvaluemaskentryproduct) = 0) /\ (sto_an_solve_construct_resultvaluemaskentryproduct) = S ge_signed_half_solve_construct_resultvaluemaskentryproductleft))) /\ ((((((dc_right_solve_construct_resultvaluemaskentry) = 2 * (sto_bp_solve_construct_resultvaluemaskentryproduct) /\ (sto_bn_solve_construct_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemaskentryproductright. (((dc_right_solve_construct_resultvaluemaskentry) = 2 * ge_signed_half_solve_construct_resultvaluemaskentryproductright + 1 /\ (sto_bp_solve_construct_resultvaluemaskentryproduct) = 0) /\ (sto_bn_solve_construct_resultvaluemaskentryproduct) = S ge_signed_half_solve_construct_resultvaluemaskentryproductright))) /\ ((((((dc_value_solve_construct_resultvaluemask) = 2 * (sto_cp_solve_construct_resultvaluemaskentryproduct) /\ (sto_cn_solve_construct_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_construct_resultvaluemaskentryproductoutput. (((dc_value_solve_construct_resultvaluemask) = 2 * ge_signed_half_solve_construct_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_solve_construct_resultvaluemaskentryproduct) = 0) /\ (sto_cn_solve_construct_resultvaluemaskentryproduct) = S ge_signed_half_solve_construct_resultvaluemaskentryproductoutput))) /\ ((sto_ap_solve_construct_resultvaluemaskentryproduct * sto_bp_solve_construct_resultvaluemaskentryproduct + sto_an_solve_construct_resultvaluemaskentryproduct * sto_bn_solve_construct_resultvaluemaskentryproduct) + sto_cn_solve_construct_resultvaluemaskentryproduct = (sto_ap_solve_construct_resultvaluemaskentryproduct * sto_bn_solve_construct_resultvaluemaskentryproduct + sto_an_solve_construct_resultvaluemaskentryproduct * sto_bp_solve_construct_resultvaluemaskentryproduct) + sto_cp_solve_construct_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_solve_construct_resultvaluemask)=0 \/ ~(exists pvs_factor_solve_construct_resultvaluemaskentrynondivisor. (dc_input_solve_construct_result) = (dc_index_solve_construct_resultvaluemask) * pvs_factor_solve_construct_resultvaluemaskentrynondivisor)) /\ ((dc_value_solve_construct_resultvaluemask)=0))))))) /\ (exists dst_positive_code_solve_construct_resultvaluefold dst_positive_scale_solve_construct_resultvaluefold dst_negative_code_solve_construct_resultvaluefold dst_negative_scale_solve_construct_resultvaluefold dst_positive_sum_solve_construct_resultvaluefold dst_negative_sum_solve_construct_resultvaluefold. (((dc_mask_solve_construct_resultvalue) = (((((dst_positive_code_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold)) * S ((dst_positive_code_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold)) + ((dst_positive_scale_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold))) + (((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) * S ((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) + ((dst_negative_scale_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)))) * S ((((dst_positive_code_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold)) * S ((dst_positive_code_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold)) + ((dst_positive_scale_solve_construct_resultvaluefold) + (dst_positive_scale_solve_construct_resultvaluefold))) + (((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) * S ((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) + ((dst_negative_scale_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)))) + ((((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) * S ((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) + ((dst_negative_scale_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold))) + (((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) * S ((dst_negative_code_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)) + ((dst_negative_scale_solve_construct_resultvaluefold) + (dst_negative_scale_solve_construct_resultvaluefold)))))) /\ (((exists fs_u_dst_solve_construct_resultvaluefoldpositive fs_v_dst_solve_construct_resultvaluefoldpositive. ((((exists fs_h_dst_solve_construct_resultvaluefoldpositive_body_start. fs_h_dst_solve_construct_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_construct_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_construct_resultvaluefoldpositive_body_start. fs_u_dst_solve_construct_resultvaluefoldpositive = fs_q_dst_solve_construct_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_solve_construct_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldpositive_body_terminal. fs_h_dst_solve_construct_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_solve_construct_resultvaluefold) = S ((S (S (dc_input_solve_construct_result))) * fs_v_dst_solve_construct_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_construct_resultvaluefoldpositive_body_terminal. fs_u_dst_solve_construct_resultvaluefoldpositive = fs_q_dst_solve_construct_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_solve_construct_result))) * fs_v_dst_solve_construct_resultvaluefoldpositive) + (dst_positive_sum_solve_construct_resultvaluefold))) /\ forall fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_solve_construct_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_solve_construct_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps = S (dc_input_solve_construct_result)) -> exists fs_a_dst_solve_construct_resultvaluefoldpositive_body_steps fs_r_dst_solve_construct_resultvaluefoldpositive_body_steps fs_s_dst_solve_construct_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_summand. fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_solve_construct_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_construct_resultvaluefold)) /\ exists fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_summand. dst_positive_code_solve_construct_resultvaluefold = fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_construct_resultvaluefold) + (fs_a_dst_solve_construct_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_partial. fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_solve_construct_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_partial. fs_u_dst_solve_construct_resultvaluefoldpositive = fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldpositive) + (fs_r_dst_solve_construct_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_successor. fs_h_dst_solve_construct_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_solve_construct_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_successor. fs_u_dst_solve_construct_resultvaluefoldpositive = fs_q_dst_solve_construct_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_solve_construct_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldpositive) + (fs_s_dst_solve_construct_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_solve_construct_resultvaluefoldpositive_body_steps = fs_r_dst_solve_construct_resultvaluefoldpositive_body_steps + fs_a_dst_solve_construct_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_solve_construct_resultvaluefoldnegative fs_v_dst_solve_construct_resultvaluefoldnegative. ((((exists fs_h_dst_solve_construct_resultvaluefoldnegative_body_start. fs_h_dst_solve_construct_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_construct_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_construct_resultvaluefoldnegative_body_start. fs_u_dst_solve_construct_resultvaluefoldnegative = fs_q_dst_solve_construct_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_solve_construct_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldnegative_body_terminal. fs_h_dst_solve_construct_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_solve_construct_resultvaluefold) = S ((S (S (dc_input_solve_construct_result))) * fs_v_dst_solve_construct_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_construct_resultvaluefoldnegative_body_terminal. fs_u_dst_solve_construct_resultvaluefoldnegative = fs_q_dst_solve_construct_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_solve_construct_result))) * fs_v_dst_solve_construct_resultvaluefoldnegative) + (dst_negative_sum_solve_construct_resultvaluefold))) /\ forall fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_solve_construct_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_solve_construct_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps = S (dc_input_solve_construct_result)) -> exists fs_a_dst_solve_construct_resultvaluefoldnegative_body_steps fs_r_dst_solve_construct_resultvaluefoldnegative_body_steps fs_s_dst_solve_construct_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_summand. fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_solve_construct_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_construct_resultvaluefold)) /\ exists fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_summand. dst_negative_code_solve_construct_resultvaluefold = fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_construct_resultvaluefold) + (fs_a_dst_solve_construct_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_partial. fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_solve_construct_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_partial. fs_u_dst_solve_construct_resultvaluefoldnegative = fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldnegative) + (fs_r_dst_solve_construct_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_successor. fs_h_dst_solve_construct_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_solve_construct_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_successor. fs_u_dst_solve_construct_resultvaluefoldnegative = fs_q_dst_solve_construct_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_solve_construct_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_construct_resultvaluefoldnegative) + (fs_s_dst_solve_construct_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_solve_construct_resultvaluefoldnegative_body_steps = fs_r_dst_solve_construct_resultvaluefoldnegative_body_steps + fs_a_dst_solve_construct_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_solve_construct_resultvaluefoldresult ge_balance_negative_solve_construct_resultvaluefoldresult. (((((dc_output_solve_construct_result) = 2 * (ge_balance_positive_solve_construct_resultvaluefoldresult) /\ (ge_balance_negative_solve_construct_resultvaluefoldresult) = 0) \/ exists ge_signed_half_solve_construct_resultvaluefoldresultdecode. (((dc_output_solve_construct_result) = 2 * ge_signed_half_solve_construct_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_solve_construct_resultvaluefoldresult) = 0) /\ (ge_balance_negative_solve_construct_resultvaluefoldresult) = S ge_signed_half_solve_construct_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_solve_construct_resultvaluefold) + ge_balance_negative_solve_construct_resultvaluefoldresult = (dst_negative_sum_solve_construct_resultvaluefold) + ge_balance_positive_solve_construct_resultvaluefoldresult)))))))))))))))))))) /\ (exists dst_positive_code_solve_construct_zero dst_positive_scale_solve_construct_zero dst_negative_code_solve_construct_zero dst_negative_scale_solve_construct_zero dst_positive_solve_construct_zero dst_negative_solve_construct_zero. (((G) = (((((dst_positive_code_solve_construct_zero) + (dst_positive_scale_solve_construct_zero)) * S ((dst_positive_code_solve_construct_zero) + (dst_positive_scale_solve_construct_zero)) + ((dst_positive_scale_solve_construct_zero) + (dst_positive_scale_solve_construct_zero))) + (((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) * S ((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) + ((dst_negative_scale_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)))) * S ((((dst_positive_code_solve_construct_zero) + (dst_positive_scale_solve_construct_zero)) * S ((dst_positive_code_solve_construct_zero) + (dst_positive_scale_solve_construct_zero)) + ((dst_positive_scale_solve_construct_zero) + (dst_positive_scale_solve_construct_zero))) + (((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) * S ((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) + ((dst_negative_scale_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)))) + ((((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) * S ((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) + ((dst_negative_scale_solve_construct_zero) + (dst_negative_scale_solve_construct_zero))) + (((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) * S ((dst_negative_code_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)) + ((dst_negative_scale_solve_construct_zero) + (dst_negative_scale_solve_construct_zero)))))) /\ (((((exists ff_h_pvs_solve_construct_zeropositive. ff_h_pvs_solve_construct_zeropositive + S (dst_positive_solve_construct_zero) = S ((S (0)) * dst_positive_scale_solve_construct_zero)) /\ exists ff_q_pvs_solve_construct_zeropositive. dst_positive_code_solve_construct_zero = ff_q_pvs_solve_construct_zeropositive * S ((S (0)) * dst_positive_scale_solve_construct_zero) + (dst_positive_solve_construct_zero))) /\ (((((exists ff_h_pvs_solve_construct_zeronegative. ff_h_pvs_solve_construct_zeronegative + S (dst_negative_solve_construct_zero) = S ((S (0)) * dst_negative_scale_solve_construct_zero)) /\ exists ff_q_pvs_solve_construct_zeronegative. dst_negative_code_solve_construct_zero = ff_q_pvs_solve_construct_zeronegative * S ((S (0)) * dst_negative_scale_solve_construct_zero) + (dst_negative_solve_construct_zero))) /\ (exists ge_balance_positive_solve_construct_zerovalue ge_balance_negative_solve_construct_zerovalue. (((((w) = 2 * (ge_balance_positive_solve_construct_zerovalue) /\ (ge_balance_negative_solve_construct_zerovalue) = 0) \/ exists ge_signed_half_solve_construct_zerovaluedecode. (((w) = 2 * ge_signed_half_solve_construct_zerovaluedecode + 1 /\ (ge_balance_positive_solve_construct_zerovalue) = 0) /\ (ge_balance_negative_solve_construct_zerovalue) = S ge_signed_half_solve_construct_zerovaluedecode))) /\ ((dst_positive_solve_construct_zero) + ge_balance_negative_solve_construct_zerovalue = (dst_negative_solve_construct_zero) + ge_balance_positive_solve_construct_zerovalue))))))))))