dirichlet_delta_unit_exists

forall N F w. (exists dst_positive_code_unit_exists_input dst_positive_scale_unit_exists_input dst_negative_code_unit_exists_input dst_negative_scale_unit_exists_input. (((F) = (((((dst_positive_code_unit_exists_input) + (dst_positive_scale_unit_exists_input)) * S ((dst_positive_code_unit_exists_input) + (dst_positive_scale_unit_exists_input)) + ((dst_positive_scale_unit_exists_input) + (dst_positive_scale_unit_exists_input))) + (((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) * S ((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) + ((dst_negative_scale_unit_exists_input) + (dst_negative_scale_unit_exists_input)))) * S ((((dst_positive_code_unit_exists_input) + (dst_positive_scale_unit_exists_input)) * S ((dst_positive_code_unit_exists_input) + (dst_positive_scale_unit_exists_input)) + ((dst_positive_scale_unit_exists_input) + (dst_positive_scale_unit_exists_input))) + (((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) * S ((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) + ((dst_negative_scale_unit_exists_input) + (dst_negative_scale_unit_exists_input)))) + ((((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) * S ((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) + ((dst_negative_scale_unit_exists_input) + (dst_negative_scale_unit_exists_input))) + (((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) * S ((dst_negative_code_unit_exists_input) + (dst_negative_scale_unit_exists_input)) + ((dst_negative_scale_unit_exists_input) + (dst_negative_scale_unit_exists_input)))))) /\ (forall dst_index_unit_exists_input. (exists pvs_le_gap_unit_exists_inputdomain. pvs_le_gap_unit_exists_inputdomain + (dst_index_unit_exists_input) = (N)) -> exists dst_positive_unit_exists_input dst_negative_unit_exists_input dst_value_unit_exists_input. ((((exists ff_h_pvs_unit_exists_inputentrypositive. ff_h_pvs_unit_exists_inputentrypositive + S (dst_positive_unit_exists_input) = S ((S (dst_index_unit_exists_input)) * dst_positive_scale_unit_exists_input)) /\ exists ff_q_pvs_unit_exists_inputentrypositive. dst_positive_code_unit_exists_input = ff_q_pvs_unit_exists_inputentrypositive * S ((S (dst_index_unit_exists_input)) * dst_positive_scale_unit_exists_input) + (dst_positive_unit_exists_input))) /\ (((((exists ff_h_pvs_unit_exists_inputentrynegative. ff_h_pvs_unit_exists_inputentrynegative + S (dst_negative_unit_exists_input) = S ((S (dst_index_unit_exists_input)) * dst_negative_scale_unit_exists_input)) /\ exists ff_q_pvs_unit_exists_inputentrynegative. dst_negative_code_unit_exists_input = ff_q_pvs_unit_exists_inputentrynegative * S ((S (dst_index_unit_exists_input)) * dst_negative_scale_unit_exists_input) + (dst_negative_unit_exists_input))) /\ (exists ge_balance_positive_unit_exists_inputentryvalue ge_balance_negative_unit_exists_inputentryvalue. (((((dst_value_unit_exists_input) = 2 * (ge_balance_positive_unit_exists_inputentryvalue) /\ (ge_balance_negative_unit_exists_inputentryvalue) = 0) \/ exists ge_signed_half_unit_exists_inputentryvaluedecode. (((dst_value_unit_exists_input) = 2 * ge_signed_half_unit_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_inputentryvalue) = 0) /\ (ge_balance_negative_unit_exists_inputentryvalue) = S ge_signed_half_unit_exists_inputentryvaluedecode))) /\ ((dst_positive_unit_exists_input) + ge_balance_negative_unit_exists_inputentryvalue = (dst_negative_unit_exists_input) + ge_balance_positive_unit_exists_inputentryvalue))))))))) -> exists E. ((((exists dst_positive_code_unit_exists_resulttable dst_positive_scale_unit_exists_resulttable dst_negative_code_unit_exists_resulttable dst_negative_scale_unit_exists_resulttable. (((E) = (((((dst_positive_code_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable)) * S ((dst_positive_code_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable)) + ((dst_positive_scale_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable))) + (((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) * S ((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) + ((dst_negative_scale_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)))) * S ((((dst_positive_code_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable)) * S ((dst_positive_code_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable)) + ((dst_positive_scale_unit_exists_resulttable) + (dst_positive_scale_unit_exists_resulttable))) + (((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) * S ((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) + ((dst_negative_scale_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)))) + ((((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) * S ((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) + ((dst_negative_scale_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable))) + (((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) * S ((dst_negative_code_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)) + ((dst_negative_scale_unit_exists_resulttable) + (dst_negative_scale_unit_exists_resulttable)))))) /\ (forall dst_index_unit_exists_resulttable. (exists pvs_le_gap_unit_exists_resulttabledomain. pvs_le_gap_unit_exists_resulttabledomain + (dst_index_unit_exists_resulttable) = (N)) -> exists dst_positive_unit_exists_resulttable dst_negative_unit_exists_resulttable dst_value_unit_exists_resulttable. ((((exists ff_h_pvs_unit_exists_resulttableentrypositive. ff_h_pvs_unit_exists_resulttableentrypositive + S (dst_positive_unit_exists_resulttable) = S ((S (dst_index_unit_exists_resulttable)) * dst_positive_scale_unit_exists_resulttable)) /\ exists ff_q_pvs_unit_exists_resulttableentrypositive. dst_positive_code_unit_exists_resulttable = ff_q_pvs_unit_exists_resulttableentrypositive * S ((S (dst_index_unit_exists_resulttable)) * dst_positive_scale_unit_exists_resulttable) + (dst_positive_unit_exists_resulttable))) /\ (((((exists ff_h_pvs_unit_exists_resulttableentrynegative. ff_h_pvs_unit_exists_resulttableentrynegative + S (dst_negative_unit_exists_resulttable) = S ((S (dst_index_unit_exists_resulttable)) * dst_negative_scale_unit_exists_resulttable)) /\ exists ff_q_pvs_unit_exists_resulttableentrynegative. dst_negative_code_unit_exists_resulttable = ff_q_pvs_unit_exists_resulttableentrynegative * S ((S (dst_index_unit_exists_resulttable)) * dst_negative_scale_unit_exists_resulttable) + (dst_negative_unit_exists_resulttable))) /\ (exists ge_balance_positive_unit_exists_resulttableentryvalue ge_balance_negative_unit_exists_resulttableentryvalue. (((((dst_value_unit_exists_resulttable) = 2 * (ge_balance_positive_unit_exists_resulttableentryvalue) /\ (ge_balance_negative_unit_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_unit_exists_resulttableentryvaluedecode. (((dst_value_unit_exists_resulttable) = 2 * ge_signed_half_unit_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_unit_exists_resulttableentryvalue) = S ge_signed_half_unit_exists_resulttableentryvaluedecode))) /\ ((dst_positive_unit_exists_resulttable) + ge_balance_negative_unit_exists_resulttableentryvalue = (dst_negative_unit_exists_resulttable) + ge_balance_positive_unit_exists_resulttableentryvalue))))))))) /\ (forall du_index_unit_exists_result du_value_unit_exists_result. ~(du_index_unit_exists_result=0) -> (exists pvs_le_gap_unit_exists_resultbound. pvs_le_gap_unit_exists_resultbound + (du_index_unit_exists_result) = (N)) -> (exists dst_positive_code_unit_exists_resultentry dst_positive_scale_unit_exists_resultentry dst_negative_code_unit_exists_resultentry dst_negative_scale_unit_exists_resultentry dst_positive_unit_exists_resultentry dst_negative_unit_exists_resultentry. (((E) = (((((dst_positive_code_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry)) * S ((dst_positive_code_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry)) + ((dst_positive_scale_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry))) + (((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) * S ((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) + ((dst_negative_scale_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)))) * S ((((dst_positive_code_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry)) * S ((dst_positive_code_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry)) + ((dst_positive_scale_unit_exists_resultentry) + (dst_positive_scale_unit_exists_resultentry))) + (((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) * S ((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) + ((dst_negative_scale_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)))) + ((((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) * S ((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) + ((dst_negative_scale_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry))) + (((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) * S ((dst_negative_code_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)) + ((dst_negative_scale_unit_exists_resultentry) + (dst_negative_scale_unit_exists_resultentry)))))) /\ (((((exists ff_h_pvs_unit_exists_resultentrypositive. ff_h_pvs_unit_exists_resultentrypositive + S (dst_positive_unit_exists_resultentry) = S ((S (du_index_unit_exists_result)) * dst_positive_scale_unit_exists_resultentry)) /\ exists ff_q_pvs_unit_exists_resultentrypositive. dst_positive_code_unit_exists_resultentry = ff_q_pvs_unit_exists_resultentrypositive * S ((S (du_index_unit_exists_result)) * dst_positive_scale_unit_exists_resultentry) + (dst_positive_unit_exists_resultentry))) /\ (((((exists ff_h_pvs_unit_exists_resultentrynegative. ff_h_pvs_unit_exists_resultentrynegative + S (dst_negative_unit_exists_resultentry) = S ((S (du_index_unit_exists_result)) * dst_negative_scale_unit_exists_resultentry)) /\ exists ff_q_pvs_unit_exists_resultentrynegative. dst_negative_code_unit_exists_resultentry = ff_q_pvs_unit_exists_resultentrynegative * S ((S (du_index_unit_exists_result)) * dst_negative_scale_unit_exists_resultentry) + (dst_negative_unit_exists_resultentry))) /\ (exists ge_balance_positive_unit_exists_resultentryvalue ge_balance_negative_unit_exists_resultentryvalue. (((((du_value_unit_exists_result) = 2 * (ge_balance_positive_unit_exists_resultentryvalue) /\ (ge_balance_negative_unit_exists_resultentryvalue) = 0) \/ exists ge_signed_half_unit_exists_resultentryvaluedecode. (((du_value_unit_exists_result) = 2 * ge_signed_half_unit_exists_resultentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_resultentryvalue) = 0) /\ (ge_balance_negative_unit_exists_resultentryvalue) = S ge_signed_half_unit_exists_resultentryvaluedecode))) /\ ((dst_positive_unit_exists_resultentry) + ge_balance_negative_unit_exists_resultentryvalue = (dst_negative_unit_exists_resultentry) + ge_balance_positive_unit_exists_resultentryvalue))))))))) -> ((((du_index_unit_exists_result)=1 -> (du_value_unit_exists_result)=2) /\ (~((du_index_unit_exists_result)=1) -> (du_value_unit_exists_result)=0)))))) /\ (((exists dst_positive_code_unit_exists_prescribed_zero dst_positive_scale_unit_exists_prescribed_zero dst_negative_code_unit_exists_prescribed_zero dst_negative_scale_unit_exists_prescribed_zero dst_positive_unit_exists_prescribed_zero dst_negative_unit_exists_prescribed_zero. (((E) = (((((dst_positive_code_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero)) * S ((dst_positive_code_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero)) + ((dst_positive_scale_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero))) + (((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) * S ((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) + ((dst_negative_scale_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)))) * S ((((dst_positive_code_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero)) * S ((dst_positive_code_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero)) + ((dst_positive_scale_unit_exists_prescribed_zero) + (dst_positive_scale_unit_exists_prescribed_zero))) + (((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) * S ((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) + ((dst_negative_scale_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)))) + ((((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) * S ((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) + ((dst_negative_scale_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero))) + (((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) * S ((dst_negative_code_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)) + ((dst_negative_scale_unit_exists_prescribed_zero) + (dst_negative_scale_unit_exists_prescribed_zero)))))) /\ (((((exists ff_h_pvs_unit_exists_prescribed_zeropositive. ff_h_pvs_unit_exists_prescribed_zeropositive + S (dst_positive_unit_exists_prescribed_zero) = S ((S (0)) * dst_positive_scale_unit_exists_prescribed_zero)) /\ exists ff_q_pvs_unit_exists_prescribed_zeropositive. dst_positive_code_unit_exists_prescribed_zero = ff_q_pvs_unit_exists_prescribed_zeropositive * S ((S (0)) * dst_positive_scale_unit_exists_prescribed_zero) + (dst_positive_unit_exists_prescribed_zero))) /\ (((((exists ff_h_pvs_unit_exists_prescribed_zeronegative. ff_h_pvs_unit_exists_prescribed_zeronegative + S (dst_negative_unit_exists_prescribed_zero) = S ((S (0)) * dst_negative_scale_unit_exists_prescribed_zero)) /\ exists ff_q_pvs_unit_exists_prescribed_zeronegative. dst_negative_code_unit_exists_prescribed_zero = ff_q_pvs_unit_exists_prescribed_zeronegative * S ((S (0)) * dst_negative_scale_unit_exists_prescribed_zero) + (dst_negative_unit_exists_prescribed_zero))) /\ (exists ge_balance_positive_unit_exists_prescribed_zerovalue ge_balance_negative_unit_exists_prescribed_zerovalue. (((((w) = 2 * (ge_balance_positive_unit_exists_prescribed_zerovalue) /\ (ge_balance_negative_unit_exists_prescribed_zerovalue) = 0) \/ exists ge_signed_half_unit_exists_prescribed_zerovaluedecode. (((w) = 2 * ge_signed_half_unit_exists_prescribed_zerovaluedecode + 1 /\ (ge_balance_positive_unit_exists_prescribed_zerovalue) = 0) /\ (ge_balance_negative_unit_exists_prescribed_zerovalue) = S ge_signed_half_unit_exists_prescribed_zerovaluedecode))) /\ ((dst_positive_unit_exists_prescribed_zero) + ge_balance_negative_unit_exists_prescribed_zerovalue = (dst_negative_unit_exists_prescribed_zero) + ge_balance_positive_unit_exists_prescribed_zerovalue))))))))) /\ (((((exists dst_positive_code_unit_exists_rightleft dst_positive_scale_unit_exists_rightleft dst_negative_code_unit_exists_rightleft dst_negative_scale_unit_exists_rightleft. (((F) = (((((dst_positive_code_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft)) * S ((dst_positive_code_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft)) + ((dst_positive_scale_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft))) + (((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) * S ((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) + ((dst_negative_scale_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)))) * S ((((dst_positive_code_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft)) * S ((dst_positive_code_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft)) + ((dst_positive_scale_unit_exists_rightleft) + (dst_positive_scale_unit_exists_rightleft))) + (((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) * S ((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) + ((dst_negative_scale_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)))) + ((((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) * S ((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) + ((dst_negative_scale_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft))) + (((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) * S ((dst_negative_code_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)) + ((dst_negative_scale_unit_exists_rightleft) + (dst_negative_scale_unit_exists_rightleft)))))) /\ (forall dst_index_unit_exists_rightleft. (exists pvs_le_gap_unit_exists_rightleftdomain. pvs_le_gap_unit_exists_rightleftdomain + (dst_index_unit_exists_rightleft) = (N)) -> exists dst_positive_unit_exists_rightleft dst_negative_unit_exists_rightleft dst_value_unit_exists_rightleft. ((((exists ff_h_pvs_unit_exists_rightleftentrypositive. ff_h_pvs_unit_exists_rightleftentrypositive + S (dst_positive_unit_exists_rightleft) = S ((S (dst_index_unit_exists_rightleft)) * dst_positive_scale_unit_exists_rightleft)) /\ exists ff_q_pvs_unit_exists_rightleftentrypositive. dst_positive_code_unit_exists_rightleft = ff_q_pvs_unit_exists_rightleftentrypositive * S ((S (dst_index_unit_exists_rightleft)) * dst_positive_scale_unit_exists_rightleft) + (dst_positive_unit_exists_rightleft))) /\ (((((exists ff_h_pvs_unit_exists_rightleftentrynegative. ff_h_pvs_unit_exists_rightleftentrynegative + S (dst_negative_unit_exists_rightleft) = S ((S (dst_index_unit_exists_rightleft)) * dst_negative_scale_unit_exists_rightleft)) /\ exists ff_q_pvs_unit_exists_rightleftentrynegative. dst_negative_code_unit_exists_rightleft = ff_q_pvs_unit_exists_rightleftentrynegative * S ((S (dst_index_unit_exists_rightleft)) * dst_negative_scale_unit_exists_rightleft) + (dst_negative_unit_exists_rightleft))) /\ (exists ge_balance_positive_unit_exists_rightleftentryvalue ge_balance_negative_unit_exists_rightleftentryvalue. (((((dst_value_unit_exists_rightleft) = 2 * (ge_balance_positive_unit_exists_rightleftentryvalue) /\ (ge_balance_negative_unit_exists_rightleftentryvalue) = 0) \/ exists ge_signed_half_unit_exists_rightleftentryvaluedecode. (((dst_value_unit_exists_rightleft) = 2 * ge_signed_half_unit_exists_rightleftentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightleftentryvalue) = 0) /\ (ge_balance_negative_unit_exists_rightleftentryvalue) = S ge_signed_half_unit_exists_rightleftentryvaluedecode))) /\ ((dst_positive_unit_exists_rightleft) + ge_balance_negative_unit_exists_rightleftentryvalue = (dst_negative_unit_exists_rightleft) + ge_balance_positive_unit_exists_rightleftentryvalue))))))))) /\ (((exists dst_positive_code_unit_exists_rightright dst_positive_scale_unit_exists_rightright dst_negative_code_unit_exists_rightright dst_negative_scale_unit_exists_rightright. (((E) = (((((dst_positive_code_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright)) * S ((dst_positive_code_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright)) + ((dst_positive_scale_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright))) + (((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) * S ((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) + ((dst_negative_scale_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)))) * S ((((dst_positive_code_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright)) * S ((dst_positive_code_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright)) + ((dst_positive_scale_unit_exists_rightright) + (dst_positive_scale_unit_exists_rightright))) + (((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) * S ((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) + ((dst_negative_scale_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)))) + ((((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) * S ((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) + ((dst_negative_scale_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright))) + (((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) * S ((dst_negative_code_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)) + ((dst_negative_scale_unit_exists_rightright) + (dst_negative_scale_unit_exists_rightright)))))) /\ (forall dst_index_unit_exists_rightright. (exists pvs_le_gap_unit_exists_rightrightdomain. pvs_le_gap_unit_exists_rightrightdomain + (dst_index_unit_exists_rightright) = (N)) -> exists dst_positive_unit_exists_rightright dst_negative_unit_exists_rightright dst_value_unit_exists_rightright. ((((exists ff_h_pvs_unit_exists_rightrightentrypositive. ff_h_pvs_unit_exists_rightrightentrypositive + S (dst_positive_unit_exists_rightright) = S ((S (dst_index_unit_exists_rightright)) * dst_positive_scale_unit_exists_rightright)) /\ exists ff_q_pvs_unit_exists_rightrightentrypositive. dst_positive_code_unit_exists_rightright = ff_q_pvs_unit_exists_rightrightentrypositive * S ((S (dst_index_unit_exists_rightright)) * dst_positive_scale_unit_exists_rightright) + (dst_positive_unit_exists_rightright))) /\ (((((exists ff_h_pvs_unit_exists_rightrightentrynegative. ff_h_pvs_unit_exists_rightrightentrynegative + S (dst_negative_unit_exists_rightright) = S ((S (dst_index_unit_exists_rightright)) * dst_negative_scale_unit_exists_rightright)) /\ exists ff_q_pvs_unit_exists_rightrightentrynegative. dst_negative_code_unit_exists_rightright = ff_q_pvs_unit_exists_rightrightentrynegative * S ((S (dst_index_unit_exists_rightright)) * dst_negative_scale_unit_exists_rightright) + (dst_negative_unit_exists_rightright))) /\ (exists ge_balance_positive_unit_exists_rightrightentryvalue ge_balance_negative_unit_exists_rightrightentryvalue. (((((dst_value_unit_exists_rightright) = 2 * (ge_balance_positive_unit_exists_rightrightentryvalue) /\ (ge_balance_negative_unit_exists_rightrightentryvalue) = 0) \/ exists ge_signed_half_unit_exists_rightrightentryvaluedecode. (((dst_value_unit_exists_rightright) = 2 * ge_signed_half_unit_exists_rightrightentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightrightentryvalue) = 0) /\ (ge_balance_negative_unit_exists_rightrightentryvalue) = S ge_signed_half_unit_exists_rightrightentryvaluedecode))) /\ ((dst_positive_unit_exists_rightright) + ge_balance_negative_unit_exists_rightrightentryvalue = (dst_negative_unit_exists_rightright) + ge_balance_positive_unit_exists_rightrightentryvalue))))))))) /\ (((exists dst_positive_code_unit_exists_righttable dst_positive_scale_unit_exists_righttable dst_negative_code_unit_exists_righttable dst_negative_scale_unit_exists_righttable. (((F) = (((((dst_positive_code_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable)) * S ((dst_positive_code_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable)) + ((dst_positive_scale_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable))) + (((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) * S ((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) + ((dst_negative_scale_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)))) * S ((((dst_positive_code_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable)) * S ((dst_positive_code_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable)) + ((dst_positive_scale_unit_exists_righttable) + (dst_positive_scale_unit_exists_righttable))) + (((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) * S ((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) + ((dst_negative_scale_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)))) + ((((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) * S ((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) + ((dst_negative_scale_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable))) + (((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) * S ((dst_negative_code_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)) + ((dst_negative_scale_unit_exists_righttable) + (dst_negative_scale_unit_exists_righttable)))))) /\ (forall dst_index_unit_exists_righttable. (exists pvs_le_gap_unit_exists_righttabledomain. pvs_le_gap_unit_exists_righttabledomain + (dst_index_unit_exists_righttable) = (N)) -> exists dst_positive_unit_exists_righttable dst_negative_unit_exists_righttable dst_value_unit_exists_righttable. ((((exists ff_h_pvs_unit_exists_righttableentrypositive. ff_h_pvs_unit_exists_righttableentrypositive + S (dst_positive_unit_exists_righttable) = S ((S (dst_index_unit_exists_righttable)) * dst_positive_scale_unit_exists_righttable)) /\ exists ff_q_pvs_unit_exists_righttableentrypositive. dst_positive_code_unit_exists_righttable = ff_q_pvs_unit_exists_righttableentrypositive * S ((S (dst_index_unit_exists_righttable)) * dst_positive_scale_unit_exists_righttable) + (dst_positive_unit_exists_righttable))) /\ (((((exists ff_h_pvs_unit_exists_righttableentrynegative. ff_h_pvs_unit_exists_righttableentrynegative + S (dst_negative_unit_exists_righttable) = S ((S (dst_index_unit_exists_righttable)) * dst_negative_scale_unit_exists_righttable)) /\ exists ff_q_pvs_unit_exists_righttableentrynegative. dst_negative_code_unit_exists_righttable = ff_q_pvs_unit_exists_righttableentrynegative * S ((S (dst_index_unit_exists_righttable)) * dst_negative_scale_unit_exists_righttable) + (dst_negative_unit_exists_righttable))) /\ (exists ge_balance_positive_unit_exists_righttableentryvalue ge_balance_negative_unit_exists_righttableentryvalue. (((((dst_value_unit_exists_righttable) = 2 * (ge_balance_positive_unit_exists_righttableentryvalue) /\ (ge_balance_negative_unit_exists_righttableentryvalue) = 0) \/ exists ge_signed_half_unit_exists_righttableentryvaluedecode. (((dst_value_unit_exists_righttable) = 2 * ge_signed_half_unit_exists_righttableentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_righttableentryvalue) = 0) /\ (ge_balance_negative_unit_exists_righttableentryvalue) = S ge_signed_half_unit_exists_righttableentryvaluedecode))) /\ ((dst_positive_unit_exists_righttable) + ge_balance_negative_unit_exists_righttableentryvalue = (dst_negative_unit_exists_righttable) + ge_balance_positive_unit_exists_righttableentryvalue))))))))) /\ (forall dc_input_unit_exists_right dc_output_unit_exists_right. ~(dc_input_unit_exists_right=0) -> (exists pvs_le_gap_unit_exists_rightdomain. pvs_le_gap_unit_exists_rightdomain + (dc_input_unit_exists_right) = (N)) -> (exists dst_positive_code_unit_exists_rightlookup dst_positive_scale_unit_exists_rightlookup dst_negative_code_unit_exists_rightlookup dst_negative_scale_unit_exists_rightlookup dst_positive_unit_exists_rightlookup dst_negative_unit_exists_rightlookup. (((F) = (((((dst_positive_code_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup)) * S ((dst_positive_code_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup)) + ((dst_positive_scale_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup))) + (((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) * S ((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) + ((dst_negative_scale_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)))) * S ((((dst_positive_code_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup)) * S ((dst_positive_code_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup)) + ((dst_positive_scale_unit_exists_rightlookup) + (dst_positive_scale_unit_exists_rightlookup))) + (((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) * S ((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) + ((dst_negative_scale_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)))) + ((((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) * S ((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) + ((dst_negative_scale_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup))) + (((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) * S ((dst_negative_code_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)) + ((dst_negative_scale_unit_exists_rightlookup) + (dst_negative_scale_unit_exists_rightlookup)))))) /\ (((((exists ff_h_pvs_unit_exists_rightlookuppositive. ff_h_pvs_unit_exists_rightlookuppositive + S (dst_positive_unit_exists_rightlookup) = S ((S (dc_input_unit_exists_right)) * dst_positive_scale_unit_exists_rightlookup)) /\ exists ff_q_pvs_unit_exists_rightlookuppositive. dst_positive_code_unit_exists_rightlookup = ff_q_pvs_unit_exists_rightlookuppositive * S ((S (dc_input_unit_exists_right)) * dst_positive_scale_unit_exists_rightlookup) + (dst_positive_unit_exists_rightlookup))) /\ (((((exists ff_h_pvs_unit_exists_rightlookupnegative. ff_h_pvs_unit_exists_rightlookupnegative + S (dst_negative_unit_exists_rightlookup) = S ((S (dc_input_unit_exists_right)) * dst_negative_scale_unit_exists_rightlookup)) /\ exists ff_q_pvs_unit_exists_rightlookupnegative. dst_negative_code_unit_exists_rightlookup = ff_q_pvs_unit_exists_rightlookupnegative * S ((S (dc_input_unit_exists_right)) * dst_negative_scale_unit_exists_rightlookup) + (dst_negative_unit_exists_rightlookup))) /\ (exists ge_balance_positive_unit_exists_rightlookupvalue ge_balance_negative_unit_exists_rightlookupvalue. (((((dc_output_unit_exists_right) = 2 * (ge_balance_positive_unit_exists_rightlookupvalue) /\ (ge_balance_negative_unit_exists_rightlookupvalue) = 0) \/ exists ge_signed_half_unit_exists_rightlookupvaluedecode. (((dc_output_unit_exists_right) = 2 * ge_signed_half_unit_exists_rightlookupvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightlookupvalue) = 0) /\ (ge_balance_negative_unit_exists_rightlookupvalue) = S ge_signed_half_unit_exists_rightlookupvaluedecode))) /\ ((dst_positive_unit_exists_rightlookup) + ge_balance_negative_unit_exists_rightlookupvalue = (dst_negative_unit_exists_rightlookup) + ge_balance_positive_unit_exists_rightlookupvalue))))))))) -> (((~((dc_input_unit_exists_right)=0)) /\ (exists dc_mask_unit_exists_rightvalue. ((((exists dst_positive_code_unit_exists_rightvaluemasktable dst_positive_scale_unit_exists_rightvaluemasktable dst_negative_code_unit_exists_rightvaluemasktable dst_negative_scale_unit_exists_rightvaluemasktable. (((dc_mask_unit_exists_rightvalue) = (((((dst_positive_code_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable)) * S ((dst_positive_code_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable)) + ((dst_positive_scale_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable))) + (((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) * S ((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) + ((dst_negative_scale_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)))) * S ((((dst_positive_code_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable)) * S ((dst_positive_code_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable)) + ((dst_positive_scale_unit_exists_rightvaluemasktable) + (dst_positive_scale_unit_exists_rightvaluemasktable))) + (((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) * S ((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) + ((dst_negative_scale_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)))) + ((((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) * S ((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) + ((dst_negative_scale_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable))) + (((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) * S ((dst_negative_code_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)) + ((dst_negative_scale_unit_exists_rightvaluemasktable) + (dst_negative_scale_unit_exists_rightvaluemasktable)))))) /\ (forall dst_index_unit_exists_rightvaluemasktable. (exists pvs_le_gap_unit_exists_rightvaluemasktabledomain. pvs_le_gap_unit_exists_rightvaluemasktabledomain + (dst_index_unit_exists_rightvaluemasktable) = (dc_input_unit_exists_right)) -> exists dst_positive_unit_exists_rightvaluemasktable dst_negative_unit_exists_rightvaluemasktable dst_value_unit_exists_rightvaluemasktable. ((((exists ff_h_pvs_unit_exists_rightvaluemasktableentrypositive. ff_h_pvs_unit_exists_rightvaluemasktableentrypositive + S (dst_positive_unit_exists_rightvaluemasktable) = S ((S (dst_index_unit_exists_rightvaluemasktable)) * dst_positive_scale_unit_exists_rightvaluemasktable)) /\ exists ff_q_pvs_unit_exists_rightvaluemasktableentrypositive. dst_positive_code_unit_exists_rightvaluemasktable = ff_q_pvs_unit_exists_rightvaluemasktableentrypositive * S ((S (dst_index_unit_exists_rightvaluemasktable)) * dst_positive_scale_unit_exists_rightvaluemasktable) + (dst_positive_unit_exists_rightvaluemasktable))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemasktableentrynegative. ff_h_pvs_unit_exists_rightvaluemasktableentrynegative + S (dst_negative_unit_exists_rightvaluemasktable) = S ((S (dst_index_unit_exists_rightvaluemasktable)) * dst_negative_scale_unit_exists_rightvaluemasktable)) /\ exists ff_q_pvs_unit_exists_rightvaluemasktableentrynegative. dst_negative_code_unit_exists_rightvaluemasktable = ff_q_pvs_unit_exists_rightvaluemasktableentrynegative * S ((S (dst_index_unit_exists_rightvaluemasktable)) * dst_negative_scale_unit_exists_rightvaluemasktable) + (dst_negative_unit_exists_rightvaluemasktable))) /\ (exists ge_balance_positive_unit_exists_rightvaluemasktableentryvalue ge_balance_negative_unit_exists_rightvaluemasktableentryvalue. (((((dst_value_unit_exists_rightvaluemasktable) = 2 * (ge_balance_positive_unit_exists_rightvaluemasktableentryvalue) /\ (ge_balance_negative_unit_exists_rightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemasktableentryvaluedecode. (((dst_value_unit_exists_rightvaluemasktable) = 2 * ge_signed_half_unit_exists_rightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_unit_exists_rightvaluemasktableentryvalue) = S ge_signed_half_unit_exists_rightvaluemasktableentryvaluedecode))) /\ ((dst_positive_unit_exists_rightvaluemasktable) + ge_balance_negative_unit_exists_rightvaluemasktableentryvalue = (dst_negative_unit_exists_rightvaluemasktable) + ge_balance_positive_unit_exists_rightvaluemasktableentryvalue))))))))) /\ (forall dc_index_unit_exists_rightvaluemask dc_value_unit_exists_rightvaluemask. (exists pvs_le_gap_unit_exists_rightvaluemaskdomain. pvs_le_gap_unit_exists_rightvaluemaskdomain + (dc_index_unit_exists_rightvaluemask) = (dc_input_unit_exists_right)) -> (exists dst_positive_code_unit_exists_rightvaluemasklookup dst_positive_scale_unit_exists_rightvaluemasklookup dst_negative_code_unit_exists_rightvaluemasklookup dst_negative_scale_unit_exists_rightvaluemasklookup dst_positive_unit_exists_rightvaluemasklookup dst_negative_unit_exists_rightvaluemasklookup. (((dc_mask_unit_exists_rightvalue) = (((((dst_positive_code_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup)) * S ((dst_positive_code_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup)) + ((dst_positive_scale_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup))) + (((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) * S ((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) + ((dst_negative_scale_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)))) * S ((((dst_positive_code_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup)) * S ((dst_positive_code_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup)) + ((dst_positive_scale_unit_exists_rightvaluemasklookup) + (dst_positive_scale_unit_exists_rightvaluemasklookup))) + (((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) * S ((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) + ((dst_negative_scale_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)))) + ((((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) * S ((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) + ((dst_negative_scale_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup))) + (((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) * S ((dst_negative_code_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)) + ((dst_negative_scale_unit_exists_rightvaluemasklookup) + (dst_negative_scale_unit_exists_rightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemasklookuppositive. ff_h_pvs_unit_exists_rightvaluemasklookuppositive + S (dst_positive_unit_exists_rightvaluemasklookup) = S ((S (dc_index_unit_exists_rightvaluemask)) * dst_positive_scale_unit_exists_rightvaluemasklookup)) /\ exists ff_q_pvs_unit_exists_rightvaluemasklookuppositive. dst_positive_code_unit_exists_rightvaluemasklookup = ff_q_pvs_unit_exists_rightvaluemasklookuppositive * S ((S (dc_index_unit_exists_rightvaluemask)) * dst_positive_scale_unit_exists_rightvaluemasklookup) + (dst_positive_unit_exists_rightvaluemasklookup))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemasklookupnegative. ff_h_pvs_unit_exists_rightvaluemasklookupnegative + S (dst_negative_unit_exists_rightvaluemasklookup) = S ((S (dc_index_unit_exists_rightvaluemask)) * dst_negative_scale_unit_exists_rightvaluemasklookup)) /\ exists ff_q_pvs_unit_exists_rightvaluemasklookupnegative. dst_negative_code_unit_exists_rightvaluemasklookup = ff_q_pvs_unit_exists_rightvaluemasklookupnegative * S ((S (dc_index_unit_exists_rightvaluemask)) * dst_negative_scale_unit_exists_rightvaluemasklookup) + (dst_negative_unit_exists_rightvaluemasklookup))) /\ (exists ge_balance_positive_unit_exists_rightvaluemasklookupvalue ge_balance_negative_unit_exists_rightvaluemasklookupvalue. (((((dc_value_unit_exists_rightvaluemask) = 2 * (ge_balance_positive_unit_exists_rightvaluemasklookupvalue) /\ (ge_balance_negative_unit_exists_rightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemasklookupvaluedecode. (((dc_value_unit_exists_rightvaluemask) = 2 * ge_signed_half_unit_exists_rightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_unit_exists_rightvaluemasklookupvalue) = S ge_signed_half_unit_exists_rightvaluemasklookupvaluedecode))) /\ ((dst_positive_unit_exists_rightvaluemasklookup) + ge_balance_negative_unit_exists_rightvaluemasklookupvalue = (dst_negative_unit_exists_rightvaluemasklookup) + ge_balance_positive_unit_exists_rightvaluemasklookupvalue))))))))) -> ((((~((dc_index_unit_exists_rightvaluemask)=0)) /\ (exists dc_quotient_unit_exists_rightvaluemaskentry dc_left_unit_exists_rightvaluemaskentry dc_right_unit_exists_rightvaluemaskentry. (((dc_input_unit_exists_right)=(dc_index_unit_exists_rightvaluemask)*dc_quotient_unit_exists_rightvaluemaskentry) /\ (((exists dst_positive_code_unit_exists_rightvaluemaskentryleft dst_positive_scale_unit_exists_rightvaluemaskentryleft dst_negative_code_unit_exists_rightvaluemaskentryleft dst_negative_scale_unit_exists_rightvaluemaskentryleft dst_positive_unit_exists_rightvaluemaskentryleft dst_negative_unit_exists_rightvaluemaskentryleft. (((F) = (((((dst_positive_code_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_positive_code_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_positive_scale_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft))) + (((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)))) * S ((((dst_positive_code_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_positive_code_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_positive_scale_unit_exists_rightvaluemaskentryleft) + (dst_positive_scale_unit_exists_rightvaluemaskentryleft))) + (((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)))) + ((((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft))) + (((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryleft) + (dst_negative_scale_unit_exists_rightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemaskentryleftpositive. ff_h_pvs_unit_exists_rightvaluemaskentryleftpositive + S (dst_positive_unit_exists_rightvaluemaskentryleft) = S ((S (dc_index_unit_exists_rightvaluemask)) * dst_positive_scale_unit_exists_rightvaluemaskentryleft)) /\ exists ff_q_pvs_unit_exists_rightvaluemaskentryleftpositive. dst_positive_code_unit_exists_rightvaluemaskentryleft = ff_q_pvs_unit_exists_rightvaluemaskentryleftpositive * S ((S (dc_index_unit_exists_rightvaluemask)) * dst_positive_scale_unit_exists_rightvaluemaskentryleft) + (dst_positive_unit_exists_rightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemaskentryleftnegative. ff_h_pvs_unit_exists_rightvaluemaskentryleftnegative + S (dst_negative_unit_exists_rightvaluemaskentryleft) = S ((S (dc_index_unit_exists_rightvaluemask)) * dst_negative_scale_unit_exists_rightvaluemaskentryleft)) /\ exists ff_q_pvs_unit_exists_rightvaluemaskentryleftnegative. dst_negative_code_unit_exists_rightvaluemaskentryleft = ff_q_pvs_unit_exists_rightvaluemaskentryleftnegative * S ((S (dc_index_unit_exists_rightvaluemask)) * dst_negative_scale_unit_exists_rightvaluemaskentryleft) + (dst_negative_unit_exists_rightvaluemaskentryleft))) /\ (exists ge_balance_positive_unit_exists_rightvaluemaskentryleftvalue ge_balance_negative_unit_exists_rightvaluemaskentryleftvalue. (((((dc_left_unit_exists_rightvaluemaskentry) = 2 * (ge_balance_positive_unit_exists_rightvaluemaskentryleftvalue) /\ (ge_balance_negative_unit_exists_rightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemaskentryleftvaluedecode. (((dc_left_unit_exists_rightvaluemaskentry) = 2 * ge_signed_half_unit_exists_rightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_unit_exists_rightvaluemaskentryleftvalue) = S ge_signed_half_unit_exists_rightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_unit_exists_rightvaluemaskentryleft) + ge_balance_negative_unit_exists_rightvaluemaskentryleftvalue = (dst_negative_unit_exists_rightvaluemaskentryleft) + ge_balance_positive_unit_exists_rightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_unit_exists_rightvaluemaskentryright dst_positive_scale_unit_exists_rightvaluemaskentryright dst_negative_code_unit_exists_rightvaluemaskentryright dst_negative_scale_unit_exists_rightvaluemaskentryright dst_positive_unit_exists_rightvaluemaskentryright dst_negative_unit_exists_rightvaluemaskentryright. (((E) = (((((dst_positive_code_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_positive_code_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright)) + ((dst_positive_scale_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright))) + (((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)))) * S ((((dst_positive_code_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_positive_code_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright)) + ((dst_positive_scale_unit_exists_rightvaluemaskentryright) + (dst_positive_scale_unit_exists_rightvaluemaskentryright))) + (((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)))) + ((((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright))) + (((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) * S ((dst_negative_code_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)) + ((dst_negative_scale_unit_exists_rightvaluemaskentryright) + (dst_negative_scale_unit_exists_rightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemaskentryrightpositive. ff_h_pvs_unit_exists_rightvaluemaskentryrightpositive + S (dst_positive_unit_exists_rightvaluemaskentryright) = S ((S (dc_quotient_unit_exists_rightvaluemaskentry)) * dst_positive_scale_unit_exists_rightvaluemaskentryright)) /\ exists ff_q_pvs_unit_exists_rightvaluemaskentryrightpositive. dst_positive_code_unit_exists_rightvaluemaskentryright = ff_q_pvs_unit_exists_rightvaluemaskentryrightpositive * S ((S (dc_quotient_unit_exists_rightvaluemaskentry)) * dst_positive_scale_unit_exists_rightvaluemaskentryright) + (dst_positive_unit_exists_rightvaluemaskentryright))) /\ (((((exists ff_h_pvs_unit_exists_rightvaluemaskentryrightnegative. ff_h_pvs_unit_exists_rightvaluemaskentryrightnegative + S (dst_negative_unit_exists_rightvaluemaskentryright) = S ((S (dc_quotient_unit_exists_rightvaluemaskentry)) * dst_negative_scale_unit_exists_rightvaluemaskentryright)) /\ exists ff_q_pvs_unit_exists_rightvaluemaskentryrightnegative. dst_negative_code_unit_exists_rightvaluemaskentryright = ff_q_pvs_unit_exists_rightvaluemaskentryrightnegative * S ((S (dc_quotient_unit_exists_rightvaluemaskentry)) * dst_negative_scale_unit_exists_rightvaluemaskentryright) + (dst_negative_unit_exists_rightvaluemaskentryright))) /\ (exists ge_balance_positive_unit_exists_rightvaluemaskentryrightvalue ge_balance_negative_unit_exists_rightvaluemaskentryrightvalue. (((((dc_right_unit_exists_rightvaluemaskentry) = 2 * (ge_balance_positive_unit_exists_rightvaluemaskentryrightvalue) /\ (ge_balance_negative_unit_exists_rightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemaskentryrightvaluedecode. (((dc_right_unit_exists_rightvaluemaskentry) = 2 * ge_signed_half_unit_exists_rightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_unit_exists_rightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_unit_exists_rightvaluemaskentryrightvalue) = S ge_signed_half_unit_exists_rightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_unit_exists_rightvaluemaskentryright) + ge_balance_negative_unit_exists_rightvaluemaskentryrightvalue = (dst_negative_unit_exists_rightvaluemaskentryright) + ge_balance_positive_unit_exists_rightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_unit_exists_rightvaluemaskentryproduct sto_an_unit_exists_rightvaluemaskentryproduct sto_bp_unit_exists_rightvaluemaskentryproduct sto_bn_unit_exists_rightvaluemaskentryproduct sto_cp_unit_exists_rightvaluemaskentryproduct sto_cn_unit_exists_rightvaluemaskentryproduct. (((((dc_left_unit_exists_rightvaluemaskentry) = 2 * (sto_ap_unit_exists_rightvaluemaskentryproduct) /\ (sto_an_unit_exists_rightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemaskentryproductleft. (((dc_left_unit_exists_rightvaluemaskentry) = 2 * ge_signed_half_unit_exists_rightvaluemaskentryproductleft + 1 /\ (sto_ap_unit_exists_rightvaluemaskentryproduct) = 0) /\ (sto_an_unit_exists_rightvaluemaskentryproduct) = S ge_signed_half_unit_exists_rightvaluemaskentryproductleft))) /\ ((((((dc_right_unit_exists_rightvaluemaskentry) = 2 * (sto_bp_unit_exists_rightvaluemaskentryproduct) /\ (sto_bn_unit_exists_rightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemaskentryproductright. (((dc_right_unit_exists_rightvaluemaskentry) = 2 * ge_signed_half_unit_exists_rightvaluemaskentryproductright + 1 /\ (sto_bp_unit_exists_rightvaluemaskentryproduct) = 0) /\ (sto_bn_unit_exists_rightvaluemaskentryproduct) = S ge_signed_half_unit_exists_rightvaluemaskentryproductright))) /\ ((((((dc_value_unit_exists_rightvaluemask) = 2 * (sto_cp_unit_exists_rightvaluemaskentryproduct) /\ (sto_cn_unit_exists_rightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_rightvaluemaskentryproductoutput. (((dc_value_unit_exists_rightvaluemask) = 2 * ge_signed_half_unit_exists_rightvaluemaskentryproductoutput + 1 /\ (sto_cp_unit_exists_rightvaluemaskentryproduct) = 0) /\ (sto_cn_unit_exists_rightvaluemaskentryproduct) = S ge_signed_half_unit_exists_rightvaluemaskentryproductoutput))) /\ ((sto_ap_unit_exists_rightvaluemaskentryproduct * sto_bp_unit_exists_rightvaluemaskentryproduct + sto_an_unit_exists_rightvaluemaskentryproduct * sto_bn_unit_exists_rightvaluemaskentryproduct) + sto_cn_unit_exists_rightvaluemaskentryproduct = (sto_ap_unit_exists_rightvaluemaskentryproduct * sto_bn_unit_exists_rightvaluemaskentryproduct + sto_an_unit_exists_rightvaluemaskentryproduct * sto_bp_unit_exists_rightvaluemaskentryproduct) + sto_cp_unit_exists_rightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_unit_exists_rightvaluemask)=0 \/ ~(exists pvs_factor_unit_exists_rightvaluemaskentrynondivisor. (dc_input_unit_exists_right) = (dc_index_unit_exists_rightvaluemask) * pvs_factor_unit_exists_rightvaluemaskentrynondivisor)) /\ ((dc_value_unit_exists_rightvaluemask)=0))))))) /\ (exists dst_positive_code_unit_exists_rightvaluefold dst_positive_scale_unit_exists_rightvaluefold dst_negative_code_unit_exists_rightvaluefold dst_negative_scale_unit_exists_rightvaluefold dst_positive_sum_unit_exists_rightvaluefold dst_negative_sum_unit_exists_rightvaluefold. (((dc_mask_unit_exists_rightvalue) = (((((dst_positive_code_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold)) * S ((dst_positive_code_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold)) + ((dst_positive_scale_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold))) + (((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) * S ((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) + ((dst_negative_scale_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)))) * S ((((dst_positive_code_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold)) * S ((dst_positive_code_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold)) + ((dst_positive_scale_unit_exists_rightvaluefold) + (dst_positive_scale_unit_exists_rightvaluefold))) + (((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) * S ((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) + ((dst_negative_scale_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)))) + ((((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) * S ((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) + ((dst_negative_scale_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold))) + (((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) * S ((dst_negative_code_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)) + ((dst_negative_scale_unit_exists_rightvaluefold) + (dst_negative_scale_unit_exists_rightvaluefold)))))) /\ (((exists fs_u_dst_unit_exists_rightvaluefoldpositive fs_v_dst_unit_exists_rightvaluefoldpositive. ((((exists fs_h_dst_unit_exists_rightvaluefoldpositive_body_start. fs_h_dst_unit_exists_rightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_exists_rightvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_rightvaluefoldpositive_body_start. fs_u_dst_unit_exists_rightvaluefoldpositive = fs_q_dst_unit_exists_rightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_unit_exists_rightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldpositive_body_terminal. fs_h_dst_unit_exists_rightvaluefoldpositive_body_terminal + S (dst_positive_sum_unit_exists_rightvaluefold) = S ((S (S (dc_input_unit_exists_right))) * fs_v_dst_unit_exists_rightvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_rightvaluefoldpositive_body_terminal. fs_u_dst_unit_exists_rightvaluefoldpositive = fs_q_dst_unit_exists_rightvaluefoldpositive_body_terminal * S ((S (S (dc_input_unit_exists_right))) * fs_v_dst_unit_exists_rightvaluefoldpositive) + (dst_positive_sum_unit_exists_rightvaluefold))) /\ forall fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps. (exists fs_lt_dst_unit_exists_rightvaluefoldpositive_body_steps_bound. fs_lt_dst_unit_exists_rightvaluefoldpositive_body_steps_bound + S fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps = S (dc_input_unit_exists_right)) -> exists fs_a_dst_unit_exists_rightvaluefoldpositive_body_steps fs_r_dst_unit_exists_rightvaluefoldpositive_body_steps fs_s_dst_unit_exists_rightvaluefoldpositive_body_steps. ((((exists fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_summand. fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_summand + S (fs_a_dst_unit_exists_rightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * dst_positive_scale_unit_exists_rightvaluefold)) /\ exists fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_summand. dst_positive_code_unit_exists_rightvaluefold = fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * dst_positive_scale_unit_exists_rightvaluefold) + (fs_a_dst_unit_exists_rightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_partial. fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_partial + S (fs_r_dst_unit_exists_rightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_partial. fs_u_dst_unit_exists_rightvaluefoldpositive = fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldpositive) + (fs_r_dst_unit_exists_rightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_successor. fs_h_dst_unit_exists_rightvaluefoldpositive_body_steps_successor + S (fs_s_dst_unit_exists_rightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_successor. fs_u_dst_unit_exists_rightvaluefoldpositive = fs_q_dst_unit_exists_rightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_unit_exists_rightvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldpositive) + (fs_s_dst_unit_exists_rightvaluefoldpositive_body_steps))) /\ fs_s_dst_unit_exists_rightvaluefoldpositive_body_steps = fs_r_dst_unit_exists_rightvaluefoldpositive_body_steps + fs_a_dst_unit_exists_rightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_exists_rightvaluefoldnegative fs_v_dst_unit_exists_rightvaluefoldnegative. ((((exists fs_h_dst_unit_exists_rightvaluefoldnegative_body_start. fs_h_dst_unit_exists_rightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_exists_rightvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_rightvaluefoldnegative_body_start. fs_u_dst_unit_exists_rightvaluefoldnegative = fs_q_dst_unit_exists_rightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_unit_exists_rightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldnegative_body_terminal. fs_h_dst_unit_exists_rightvaluefoldnegative_body_terminal + S (dst_negative_sum_unit_exists_rightvaluefold) = S ((S (S (dc_input_unit_exists_right))) * fs_v_dst_unit_exists_rightvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_rightvaluefoldnegative_body_terminal. fs_u_dst_unit_exists_rightvaluefoldnegative = fs_q_dst_unit_exists_rightvaluefoldnegative_body_terminal * S ((S (S (dc_input_unit_exists_right))) * fs_v_dst_unit_exists_rightvaluefoldnegative) + (dst_negative_sum_unit_exists_rightvaluefold))) /\ forall fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps. (exists fs_lt_dst_unit_exists_rightvaluefoldnegative_body_steps_bound. fs_lt_dst_unit_exists_rightvaluefoldnegative_body_steps_bound + S fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps = S (dc_input_unit_exists_right)) -> exists fs_a_dst_unit_exists_rightvaluefoldnegative_body_steps fs_r_dst_unit_exists_rightvaluefoldnegative_body_steps fs_s_dst_unit_exists_rightvaluefoldnegative_body_steps. ((((exists fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_summand. fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_summand + S (fs_a_dst_unit_exists_rightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * dst_negative_scale_unit_exists_rightvaluefold)) /\ exists fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_summand. dst_negative_code_unit_exists_rightvaluefold = fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * dst_negative_scale_unit_exists_rightvaluefold) + (fs_a_dst_unit_exists_rightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_partial. fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_partial + S (fs_r_dst_unit_exists_rightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_partial. fs_u_dst_unit_exists_rightvaluefoldnegative = fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldnegative) + (fs_r_dst_unit_exists_rightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_successor. fs_h_dst_unit_exists_rightvaluefoldnegative_body_steps_successor + S (fs_s_dst_unit_exists_rightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_successor. fs_u_dst_unit_exists_rightvaluefoldnegative = fs_q_dst_unit_exists_rightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_unit_exists_rightvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_rightvaluefoldnegative) + (fs_s_dst_unit_exists_rightvaluefoldnegative_body_steps))) /\ fs_s_dst_unit_exists_rightvaluefoldnegative_body_steps = fs_r_dst_unit_exists_rightvaluefoldnegative_body_steps + fs_a_dst_unit_exists_rightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_exists_rightvaluefoldresult ge_balance_negative_unit_exists_rightvaluefoldresult. (((((dc_output_unit_exists_right) = 2 * (ge_balance_positive_unit_exists_rightvaluefoldresult) /\ (ge_balance_negative_unit_exists_rightvaluefoldresult) = 0) \/ exists ge_signed_half_unit_exists_rightvaluefoldresultdecode. (((dc_output_unit_exists_right) = 2 * ge_signed_half_unit_exists_rightvaluefoldresultdecode + 1 /\ (ge_balance_positive_unit_exists_rightvaluefoldresult) = 0) /\ (ge_balance_negative_unit_exists_rightvaluefoldresult) = S ge_signed_half_unit_exists_rightvaluefoldresultdecode))) /\ ((dst_positive_sum_unit_exists_rightvaluefold) + ge_balance_negative_unit_exists_rightvaluefoldresult = (dst_negative_sum_unit_exists_rightvaluefold) + ge_balance_positive_unit_exists_rightvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_unit_exists_leftleft dst_positive_scale_unit_exists_leftleft dst_negative_code_unit_exists_leftleft dst_negative_scale_unit_exists_leftleft. (((E) = (((((dst_positive_code_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft)) * S ((dst_positive_code_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft)) + ((dst_positive_scale_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft))) + (((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) * S ((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) + ((dst_negative_scale_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)))) * S ((((dst_positive_code_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft)) * S ((dst_positive_code_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft)) + ((dst_positive_scale_unit_exists_leftleft) + (dst_positive_scale_unit_exists_leftleft))) + (((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) * S ((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) + ((dst_negative_scale_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)))) + ((((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) * S ((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) + ((dst_negative_scale_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft))) + (((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) * S ((dst_negative_code_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)) + ((dst_negative_scale_unit_exists_leftleft) + (dst_negative_scale_unit_exists_leftleft)))))) /\ (forall dst_index_unit_exists_leftleft. (exists pvs_le_gap_unit_exists_leftleftdomain. pvs_le_gap_unit_exists_leftleftdomain + (dst_index_unit_exists_leftleft) = (N)) -> exists dst_positive_unit_exists_leftleft dst_negative_unit_exists_leftleft dst_value_unit_exists_leftleft. ((((exists ff_h_pvs_unit_exists_leftleftentrypositive. ff_h_pvs_unit_exists_leftleftentrypositive + S (dst_positive_unit_exists_leftleft) = S ((S (dst_index_unit_exists_leftleft)) * dst_positive_scale_unit_exists_leftleft)) /\ exists ff_q_pvs_unit_exists_leftleftentrypositive. dst_positive_code_unit_exists_leftleft = ff_q_pvs_unit_exists_leftleftentrypositive * S ((S (dst_index_unit_exists_leftleft)) * dst_positive_scale_unit_exists_leftleft) + (dst_positive_unit_exists_leftleft))) /\ (((((exists ff_h_pvs_unit_exists_leftleftentrynegative. ff_h_pvs_unit_exists_leftleftentrynegative + S (dst_negative_unit_exists_leftleft) = S ((S (dst_index_unit_exists_leftleft)) * dst_negative_scale_unit_exists_leftleft)) /\ exists ff_q_pvs_unit_exists_leftleftentrynegative. dst_negative_code_unit_exists_leftleft = ff_q_pvs_unit_exists_leftleftentrynegative * S ((S (dst_index_unit_exists_leftleft)) * dst_negative_scale_unit_exists_leftleft) + (dst_negative_unit_exists_leftleft))) /\ (exists ge_balance_positive_unit_exists_leftleftentryvalue ge_balance_negative_unit_exists_leftleftentryvalue. (((((dst_value_unit_exists_leftleft) = 2 * (ge_balance_positive_unit_exists_leftleftentryvalue) /\ (ge_balance_negative_unit_exists_leftleftentryvalue) = 0) \/ exists ge_signed_half_unit_exists_leftleftentryvaluedecode. (((dst_value_unit_exists_leftleft) = 2 * ge_signed_half_unit_exists_leftleftentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftleftentryvalue) = 0) /\ (ge_balance_negative_unit_exists_leftleftentryvalue) = S ge_signed_half_unit_exists_leftleftentryvaluedecode))) /\ ((dst_positive_unit_exists_leftleft) + ge_balance_negative_unit_exists_leftleftentryvalue = (dst_negative_unit_exists_leftleft) + ge_balance_positive_unit_exists_leftleftentryvalue))))))))) /\ (((exists dst_positive_code_unit_exists_leftright dst_positive_scale_unit_exists_leftright dst_negative_code_unit_exists_leftright dst_negative_scale_unit_exists_leftright. (((F) = (((((dst_positive_code_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright)) * S ((dst_positive_code_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright)) + ((dst_positive_scale_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright))) + (((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) * S ((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) + ((dst_negative_scale_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)))) * S ((((dst_positive_code_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright)) * S ((dst_positive_code_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright)) + ((dst_positive_scale_unit_exists_leftright) + (dst_positive_scale_unit_exists_leftright))) + (((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) * S ((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) + ((dst_negative_scale_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)))) + ((((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) * S ((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) + ((dst_negative_scale_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright))) + (((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) * S ((dst_negative_code_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)) + ((dst_negative_scale_unit_exists_leftright) + (dst_negative_scale_unit_exists_leftright)))))) /\ (forall dst_index_unit_exists_leftright. (exists pvs_le_gap_unit_exists_leftrightdomain. pvs_le_gap_unit_exists_leftrightdomain + (dst_index_unit_exists_leftright) = (N)) -> exists dst_positive_unit_exists_leftright dst_negative_unit_exists_leftright dst_value_unit_exists_leftright. ((((exists ff_h_pvs_unit_exists_leftrightentrypositive. ff_h_pvs_unit_exists_leftrightentrypositive + S (dst_positive_unit_exists_leftright) = S ((S (dst_index_unit_exists_leftright)) * dst_positive_scale_unit_exists_leftright)) /\ exists ff_q_pvs_unit_exists_leftrightentrypositive. dst_positive_code_unit_exists_leftright = ff_q_pvs_unit_exists_leftrightentrypositive * S ((S (dst_index_unit_exists_leftright)) * dst_positive_scale_unit_exists_leftright) + (dst_positive_unit_exists_leftright))) /\ (((((exists ff_h_pvs_unit_exists_leftrightentrynegative. ff_h_pvs_unit_exists_leftrightentrynegative + S (dst_negative_unit_exists_leftright) = S ((S (dst_index_unit_exists_leftright)) * dst_negative_scale_unit_exists_leftright)) /\ exists ff_q_pvs_unit_exists_leftrightentrynegative. dst_negative_code_unit_exists_leftright = ff_q_pvs_unit_exists_leftrightentrynegative * S ((S (dst_index_unit_exists_leftright)) * dst_negative_scale_unit_exists_leftright) + (dst_negative_unit_exists_leftright))) /\ (exists ge_balance_positive_unit_exists_leftrightentryvalue ge_balance_negative_unit_exists_leftrightentryvalue. (((((dst_value_unit_exists_leftright) = 2 * (ge_balance_positive_unit_exists_leftrightentryvalue) /\ (ge_balance_negative_unit_exists_leftrightentryvalue) = 0) \/ exists ge_signed_half_unit_exists_leftrightentryvaluedecode. (((dst_value_unit_exists_leftright) = 2 * ge_signed_half_unit_exists_leftrightentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftrightentryvalue) = 0) /\ (ge_balance_negative_unit_exists_leftrightentryvalue) = S ge_signed_half_unit_exists_leftrightentryvaluedecode))) /\ ((dst_positive_unit_exists_leftright) + ge_balance_negative_unit_exists_leftrightentryvalue = (dst_negative_unit_exists_leftright) + ge_balance_positive_unit_exists_leftrightentryvalue))))))))) /\ (((exists dst_positive_code_unit_exists_lefttable dst_positive_scale_unit_exists_lefttable dst_negative_code_unit_exists_lefttable dst_negative_scale_unit_exists_lefttable. (((F) = (((((dst_positive_code_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable)) * S ((dst_positive_code_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable)) + ((dst_positive_scale_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable))) + (((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) * S ((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) + ((dst_negative_scale_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)))) * S ((((dst_positive_code_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable)) * S ((dst_positive_code_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable)) + ((dst_positive_scale_unit_exists_lefttable) + (dst_positive_scale_unit_exists_lefttable))) + (((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) * S ((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) + ((dst_negative_scale_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)))) + ((((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) * S ((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) + ((dst_negative_scale_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable))) + (((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) * S ((dst_negative_code_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)) + ((dst_negative_scale_unit_exists_lefttable) + (dst_negative_scale_unit_exists_lefttable)))))) /\ (forall dst_index_unit_exists_lefttable. (exists pvs_le_gap_unit_exists_lefttabledomain. pvs_le_gap_unit_exists_lefttabledomain + (dst_index_unit_exists_lefttable) = (N)) -> exists dst_positive_unit_exists_lefttable dst_negative_unit_exists_lefttable dst_value_unit_exists_lefttable. ((((exists ff_h_pvs_unit_exists_lefttableentrypositive. ff_h_pvs_unit_exists_lefttableentrypositive + S (dst_positive_unit_exists_lefttable) = S ((S (dst_index_unit_exists_lefttable)) * dst_positive_scale_unit_exists_lefttable)) /\ exists ff_q_pvs_unit_exists_lefttableentrypositive. dst_positive_code_unit_exists_lefttable = ff_q_pvs_unit_exists_lefttableentrypositive * S ((S (dst_index_unit_exists_lefttable)) * dst_positive_scale_unit_exists_lefttable) + (dst_positive_unit_exists_lefttable))) /\ (((((exists ff_h_pvs_unit_exists_lefttableentrynegative. ff_h_pvs_unit_exists_lefttableentrynegative + S (dst_negative_unit_exists_lefttable) = S ((S (dst_index_unit_exists_lefttable)) * dst_negative_scale_unit_exists_lefttable)) /\ exists ff_q_pvs_unit_exists_lefttableentrynegative. dst_negative_code_unit_exists_lefttable = ff_q_pvs_unit_exists_lefttableentrynegative * S ((S (dst_index_unit_exists_lefttable)) * dst_negative_scale_unit_exists_lefttable) + (dst_negative_unit_exists_lefttable))) /\ (exists ge_balance_positive_unit_exists_lefttableentryvalue ge_balance_negative_unit_exists_lefttableentryvalue. (((((dst_value_unit_exists_lefttable) = 2 * (ge_balance_positive_unit_exists_lefttableentryvalue) /\ (ge_balance_negative_unit_exists_lefttableentryvalue) = 0) \/ exists ge_signed_half_unit_exists_lefttableentryvaluedecode. (((dst_value_unit_exists_lefttable) = 2 * ge_signed_half_unit_exists_lefttableentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_lefttableentryvalue) = 0) /\ (ge_balance_negative_unit_exists_lefttableentryvalue) = S ge_signed_half_unit_exists_lefttableentryvaluedecode))) /\ ((dst_positive_unit_exists_lefttable) + ge_balance_negative_unit_exists_lefttableentryvalue = (dst_negative_unit_exists_lefttable) + ge_balance_positive_unit_exists_lefttableentryvalue))))))))) /\ (forall dc_input_unit_exists_left dc_output_unit_exists_left. ~(dc_input_unit_exists_left=0) -> (exists pvs_le_gap_unit_exists_leftdomain. pvs_le_gap_unit_exists_leftdomain + (dc_input_unit_exists_left) = (N)) -> (exists dst_positive_code_unit_exists_leftlookup dst_positive_scale_unit_exists_leftlookup dst_negative_code_unit_exists_leftlookup dst_negative_scale_unit_exists_leftlookup dst_positive_unit_exists_leftlookup dst_negative_unit_exists_leftlookup. (((F) = (((((dst_positive_code_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup)) * S ((dst_positive_code_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup)) + ((dst_positive_scale_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup))) + (((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) * S ((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) + ((dst_negative_scale_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)))) * S ((((dst_positive_code_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup)) * S ((dst_positive_code_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup)) + ((dst_positive_scale_unit_exists_leftlookup) + (dst_positive_scale_unit_exists_leftlookup))) + (((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) * S ((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) + ((dst_negative_scale_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)))) + ((((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) * S ((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) + ((dst_negative_scale_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup))) + (((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) * S ((dst_negative_code_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)) + ((dst_negative_scale_unit_exists_leftlookup) + (dst_negative_scale_unit_exists_leftlookup)))))) /\ (((((exists ff_h_pvs_unit_exists_leftlookuppositive. ff_h_pvs_unit_exists_leftlookuppositive + S (dst_positive_unit_exists_leftlookup) = S ((S (dc_input_unit_exists_left)) * dst_positive_scale_unit_exists_leftlookup)) /\ exists ff_q_pvs_unit_exists_leftlookuppositive. dst_positive_code_unit_exists_leftlookup = ff_q_pvs_unit_exists_leftlookuppositive * S ((S (dc_input_unit_exists_left)) * dst_positive_scale_unit_exists_leftlookup) + (dst_positive_unit_exists_leftlookup))) /\ (((((exists ff_h_pvs_unit_exists_leftlookupnegative. ff_h_pvs_unit_exists_leftlookupnegative + S (dst_negative_unit_exists_leftlookup) = S ((S (dc_input_unit_exists_left)) * dst_negative_scale_unit_exists_leftlookup)) /\ exists ff_q_pvs_unit_exists_leftlookupnegative. dst_negative_code_unit_exists_leftlookup = ff_q_pvs_unit_exists_leftlookupnegative * S ((S (dc_input_unit_exists_left)) * dst_negative_scale_unit_exists_leftlookup) + (dst_negative_unit_exists_leftlookup))) /\ (exists ge_balance_positive_unit_exists_leftlookupvalue ge_balance_negative_unit_exists_leftlookupvalue. (((((dc_output_unit_exists_left) = 2 * (ge_balance_positive_unit_exists_leftlookupvalue) /\ (ge_balance_negative_unit_exists_leftlookupvalue) = 0) \/ exists ge_signed_half_unit_exists_leftlookupvaluedecode. (((dc_output_unit_exists_left) = 2 * ge_signed_half_unit_exists_leftlookupvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftlookupvalue) = 0) /\ (ge_balance_negative_unit_exists_leftlookupvalue) = S ge_signed_half_unit_exists_leftlookupvaluedecode))) /\ ((dst_positive_unit_exists_leftlookup) + ge_balance_negative_unit_exists_leftlookupvalue = (dst_negative_unit_exists_leftlookup) + ge_balance_positive_unit_exists_leftlookupvalue))))))))) -> (((~((dc_input_unit_exists_left)=0)) /\ (exists dc_mask_unit_exists_leftvalue. ((((exists dst_positive_code_unit_exists_leftvaluemasktable dst_positive_scale_unit_exists_leftvaluemasktable dst_negative_code_unit_exists_leftvaluemasktable dst_negative_scale_unit_exists_leftvaluemasktable. (((dc_mask_unit_exists_leftvalue) = (((((dst_positive_code_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable)) * S ((dst_positive_code_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable)) + ((dst_positive_scale_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable))) + (((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) * S ((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) + ((dst_negative_scale_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)))) * S ((((dst_positive_code_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable)) * S ((dst_positive_code_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable)) + ((dst_positive_scale_unit_exists_leftvaluemasktable) + (dst_positive_scale_unit_exists_leftvaluemasktable))) + (((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) * S ((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) + ((dst_negative_scale_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)))) + ((((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) * S ((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) + ((dst_negative_scale_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable))) + (((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) * S ((dst_negative_code_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)) + ((dst_negative_scale_unit_exists_leftvaluemasktable) + (dst_negative_scale_unit_exists_leftvaluemasktable)))))) /\ (forall dst_index_unit_exists_leftvaluemasktable. (exists pvs_le_gap_unit_exists_leftvaluemasktabledomain. pvs_le_gap_unit_exists_leftvaluemasktabledomain + (dst_index_unit_exists_leftvaluemasktable) = (dc_input_unit_exists_left)) -> exists dst_positive_unit_exists_leftvaluemasktable dst_negative_unit_exists_leftvaluemasktable dst_value_unit_exists_leftvaluemasktable. ((((exists ff_h_pvs_unit_exists_leftvaluemasktableentrypositive. ff_h_pvs_unit_exists_leftvaluemasktableentrypositive + S (dst_positive_unit_exists_leftvaluemasktable) = S ((S (dst_index_unit_exists_leftvaluemasktable)) * dst_positive_scale_unit_exists_leftvaluemasktable)) /\ exists ff_q_pvs_unit_exists_leftvaluemasktableentrypositive. dst_positive_code_unit_exists_leftvaluemasktable = ff_q_pvs_unit_exists_leftvaluemasktableentrypositive * S ((S (dst_index_unit_exists_leftvaluemasktable)) * dst_positive_scale_unit_exists_leftvaluemasktable) + (dst_positive_unit_exists_leftvaluemasktable))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemasktableentrynegative. ff_h_pvs_unit_exists_leftvaluemasktableentrynegative + S (dst_negative_unit_exists_leftvaluemasktable) = S ((S (dst_index_unit_exists_leftvaluemasktable)) * dst_negative_scale_unit_exists_leftvaluemasktable)) /\ exists ff_q_pvs_unit_exists_leftvaluemasktableentrynegative. dst_negative_code_unit_exists_leftvaluemasktable = ff_q_pvs_unit_exists_leftvaluemasktableentrynegative * S ((S (dst_index_unit_exists_leftvaluemasktable)) * dst_negative_scale_unit_exists_leftvaluemasktable) + (dst_negative_unit_exists_leftvaluemasktable))) /\ (exists ge_balance_positive_unit_exists_leftvaluemasktableentryvalue ge_balance_negative_unit_exists_leftvaluemasktableentryvalue. (((((dst_value_unit_exists_leftvaluemasktable) = 2 * (ge_balance_positive_unit_exists_leftvaluemasktableentryvalue) /\ (ge_balance_negative_unit_exists_leftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemasktableentryvaluedecode. (((dst_value_unit_exists_leftvaluemasktable) = 2 * ge_signed_half_unit_exists_leftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_unit_exists_leftvaluemasktableentryvalue) = S ge_signed_half_unit_exists_leftvaluemasktableentryvaluedecode))) /\ ((dst_positive_unit_exists_leftvaluemasktable) + ge_balance_negative_unit_exists_leftvaluemasktableentryvalue = (dst_negative_unit_exists_leftvaluemasktable) + ge_balance_positive_unit_exists_leftvaluemasktableentryvalue))))))))) /\ (forall dc_index_unit_exists_leftvaluemask dc_value_unit_exists_leftvaluemask. (exists pvs_le_gap_unit_exists_leftvaluemaskdomain. pvs_le_gap_unit_exists_leftvaluemaskdomain + (dc_index_unit_exists_leftvaluemask) = (dc_input_unit_exists_left)) -> (exists dst_positive_code_unit_exists_leftvaluemasklookup dst_positive_scale_unit_exists_leftvaluemasklookup dst_negative_code_unit_exists_leftvaluemasklookup dst_negative_scale_unit_exists_leftvaluemasklookup dst_positive_unit_exists_leftvaluemasklookup dst_negative_unit_exists_leftvaluemasklookup. (((dc_mask_unit_exists_leftvalue) = (((((dst_positive_code_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup)) * S ((dst_positive_code_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup)) + ((dst_positive_scale_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup))) + (((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) * S ((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) + ((dst_negative_scale_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)))) * S ((((dst_positive_code_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup)) * S ((dst_positive_code_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup)) + ((dst_positive_scale_unit_exists_leftvaluemasklookup) + (dst_positive_scale_unit_exists_leftvaluemasklookup))) + (((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) * S ((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) + ((dst_negative_scale_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)))) + ((((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) * S ((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) + ((dst_negative_scale_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup))) + (((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) * S ((dst_negative_code_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)) + ((dst_negative_scale_unit_exists_leftvaluemasklookup) + (dst_negative_scale_unit_exists_leftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemasklookuppositive. ff_h_pvs_unit_exists_leftvaluemasklookuppositive + S (dst_positive_unit_exists_leftvaluemasklookup) = S ((S (dc_index_unit_exists_leftvaluemask)) * dst_positive_scale_unit_exists_leftvaluemasklookup)) /\ exists ff_q_pvs_unit_exists_leftvaluemasklookuppositive. dst_positive_code_unit_exists_leftvaluemasklookup = ff_q_pvs_unit_exists_leftvaluemasklookuppositive * S ((S (dc_index_unit_exists_leftvaluemask)) * dst_positive_scale_unit_exists_leftvaluemasklookup) + (dst_positive_unit_exists_leftvaluemasklookup))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemasklookupnegative. ff_h_pvs_unit_exists_leftvaluemasklookupnegative + S (dst_negative_unit_exists_leftvaluemasklookup) = S ((S (dc_index_unit_exists_leftvaluemask)) * dst_negative_scale_unit_exists_leftvaluemasklookup)) /\ exists ff_q_pvs_unit_exists_leftvaluemasklookupnegative. dst_negative_code_unit_exists_leftvaluemasklookup = ff_q_pvs_unit_exists_leftvaluemasklookupnegative * S ((S (dc_index_unit_exists_leftvaluemask)) * dst_negative_scale_unit_exists_leftvaluemasklookup) + (dst_negative_unit_exists_leftvaluemasklookup))) /\ (exists ge_balance_positive_unit_exists_leftvaluemasklookupvalue ge_balance_negative_unit_exists_leftvaluemasklookupvalue. (((((dc_value_unit_exists_leftvaluemask) = 2 * (ge_balance_positive_unit_exists_leftvaluemasklookupvalue) /\ (ge_balance_negative_unit_exists_leftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemasklookupvaluedecode. (((dc_value_unit_exists_leftvaluemask) = 2 * ge_signed_half_unit_exists_leftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_unit_exists_leftvaluemasklookupvalue) = S ge_signed_half_unit_exists_leftvaluemasklookupvaluedecode))) /\ ((dst_positive_unit_exists_leftvaluemasklookup) + ge_balance_negative_unit_exists_leftvaluemasklookupvalue = (dst_negative_unit_exists_leftvaluemasklookup) + ge_balance_positive_unit_exists_leftvaluemasklookupvalue))))))))) -> ((((~((dc_index_unit_exists_leftvaluemask)=0)) /\ (exists dc_quotient_unit_exists_leftvaluemaskentry dc_left_unit_exists_leftvaluemaskentry dc_right_unit_exists_leftvaluemaskentry. (((dc_input_unit_exists_left)=(dc_index_unit_exists_leftvaluemask)*dc_quotient_unit_exists_leftvaluemaskentry) /\ (((exists dst_positive_code_unit_exists_leftvaluemaskentryleft dst_positive_scale_unit_exists_leftvaluemaskentryleft dst_negative_code_unit_exists_leftvaluemaskentryleft dst_negative_scale_unit_exists_leftvaluemaskentryleft dst_positive_unit_exists_leftvaluemaskentryleft dst_negative_unit_exists_leftvaluemaskentryleft. (((E) = (((((dst_positive_code_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_positive_code_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_positive_scale_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft))) + (((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)))) * S ((((dst_positive_code_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_positive_code_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_positive_scale_unit_exists_leftvaluemaskentryleft) + (dst_positive_scale_unit_exists_leftvaluemaskentryleft))) + (((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)))) + ((((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft))) + (((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryleft) + (dst_negative_scale_unit_exists_leftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemaskentryleftpositive. ff_h_pvs_unit_exists_leftvaluemaskentryleftpositive + S (dst_positive_unit_exists_leftvaluemaskentryleft) = S ((S (dc_index_unit_exists_leftvaluemask)) * dst_positive_scale_unit_exists_leftvaluemaskentryleft)) /\ exists ff_q_pvs_unit_exists_leftvaluemaskentryleftpositive. dst_positive_code_unit_exists_leftvaluemaskentryleft = ff_q_pvs_unit_exists_leftvaluemaskentryleftpositive * S ((S (dc_index_unit_exists_leftvaluemask)) * dst_positive_scale_unit_exists_leftvaluemaskentryleft) + (dst_positive_unit_exists_leftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemaskentryleftnegative. ff_h_pvs_unit_exists_leftvaluemaskentryleftnegative + S (dst_negative_unit_exists_leftvaluemaskentryleft) = S ((S (dc_index_unit_exists_leftvaluemask)) * dst_negative_scale_unit_exists_leftvaluemaskentryleft)) /\ exists ff_q_pvs_unit_exists_leftvaluemaskentryleftnegative. dst_negative_code_unit_exists_leftvaluemaskentryleft = ff_q_pvs_unit_exists_leftvaluemaskentryleftnegative * S ((S (dc_index_unit_exists_leftvaluemask)) * dst_negative_scale_unit_exists_leftvaluemaskentryleft) + (dst_negative_unit_exists_leftvaluemaskentryleft))) /\ (exists ge_balance_positive_unit_exists_leftvaluemaskentryleftvalue ge_balance_negative_unit_exists_leftvaluemaskentryleftvalue. (((((dc_left_unit_exists_leftvaluemaskentry) = 2 * (ge_balance_positive_unit_exists_leftvaluemaskentryleftvalue) /\ (ge_balance_negative_unit_exists_leftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemaskentryleftvaluedecode. (((dc_left_unit_exists_leftvaluemaskentry) = 2 * ge_signed_half_unit_exists_leftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_unit_exists_leftvaluemaskentryleftvalue) = S ge_signed_half_unit_exists_leftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_unit_exists_leftvaluemaskentryleft) + ge_balance_negative_unit_exists_leftvaluemaskentryleftvalue = (dst_negative_unit_exists_leftvaluemaskentryleft) + ge_balance_positive_unit_exists_leftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_unit_exists_leftvaluemaskentryright dst_positive_scale_unit_exists_leftvaluemaskentryright dst_negative_code_unit_exists_leftvaluemaskentryright dst_negative_scale_unit_exists_leftvaluemaskentryright dst_positive_unit_exists_leftvaluemaskentryright dst_negative_unit_exists_leftvaluemaskentryright. (((F) = (((((dst_positive_code_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_positive_code_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright)) + ((dst_positive_scale_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright))) + (((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)))) * S ((((dst_positive_code_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_positive_code_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright)) + ((dst_positive_scale_unit_exists_leftvaluemaskentryright) + (dst_positive_scale_unit_exists_leftvaluemaskentryright))) + (((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)))) + ((((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright))) + (((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) * S ((dst_negative_code_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)) + ((dst_negative_scale_unit_exists_leftvaluemaskentryright) + (dst_negative_scale_unit_exists_leftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemaskentryrightpositive. ff_h_pvs_unit_exists_leftvaluemaskentryrightpositive + S (dst_positive_unit_exists_leftvaluemaskentryright) = S ((S (dc_quotient_unit_exists_leftvaluemaskentry)) * dst_positive_scale_unit_exists_leftvaluemaskentryright)) /\ exists ff_q_pvs_unit_exists_leftvaluemaskentryrightpositive. dst_positive_code_unit_exists_leftvaluemaskentryright = ff_q_pvs_unit_exists_leftvaluemaskentryrightpositive * S ((S (dc_quotient_unit_exists_leftvaluemaskentry)) * dst_positive_scale_unit_exists_leftvaluemaskentryright) + (dst_positive_unit_exists_leftvaluemaskentryright))) /\ (((((exists ff_h_pvs_unit_exists_leftvaluemaskentryrightnegative. ff_h_pvs_unit_exists_leftvaluemaskentryrightnegative + S (dst_negative_unit_exists_leftvaluemaskentryright) = S ((S (dc_quotient_unit_exists_leftvaluemaskentry)) * dst_negative_scale_unit_exists_leftvaluemaskentryright)) /\ exists ff_q_pvs_unit_exists_leftvaluemaskentryrightnegative. dst_negative_code_unit_exists_leftvaluemaskentryright = ff_q_pvs_unit_exists_leftvaluemaskentryrightnegative * S ((S (dc_quotient_unit_exists_leftvaluemaskentry)) * dst_negative_scale_unit_exists_leftvaluemaskentryright) + (dst_negative_unit_exists_leftvaluemaskentryright))) /\ (exists ge_balance_positive_unit_exists_leftvaluemaskentryrightvalue ge_balance_negative_unit_exists_leftvaluemaskentryrightvalue. (((((dc_right_unit_exists_leftvaluemaskentry) = 2 * (ge_balance_positive_unit_exists_leftvaluemaskentryrightvalue) /\ (ge_balance_negative_unit_exists_leftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemaskentryrightvaluedecode. (((dc_right_unit_exists_leftvaluemaskentry) = 2 * ge_signed_half_unit_exists_leftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_unit_exists_leftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_unit_exists_leftvaluemaskentryrightvalue) = S ge_signed_half_unit_exists_leftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_unit_exists_leftvaluemaskentryright) + ge_balance_negative_unit_exists_leftvaluemaskentryrightvalue = (dst_negative_unit_exists_leftvaluemaskentryright) + ge_balance_positive_unit_exists_leftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_unit_exists_leftvaluemaskentryproduct sto_an_unit_exists_leftvaluemaskentryproduct sto_bp_unit_exists_leftvaluemaskentryproduct sto_bn_unit_exists_leftvaluemaskentryproduct sto_cp_unit_exists_leftvaluemaskentryproduct sto_cn_unit_exists_leftvaluemaskentryproduct. (((((dc_left_unit_exists_leftvaluemaskentry) = 2 * (sto_ap_unit_exists_leftvaluemaskentryproduct) /\ (sto_an_unit_exists_leftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemaskentryproductleft. (((dc_left_unit_exists_leftvaluemaskentry) = 2 * ge_signed_half_unit_exists_leftvaluemaskentryproductleft + 1 /\ (sto_ap_unit_exists_leftvaluemaskentryproduct) = 0) /\ (sto_an_unit_exists_leftvaluemaskentryproduct) = S ge_signed_half_unit_exists_leftvaluemaskentryproductleft))) /\ ((((((dc_right_unit_exists_leftvaluemaskentry) = 2 * (sto_bp_unit_exists_leftvaluemaskentryproduct) /\ (sto_bn_unit_exists_leftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemaskentryproductright. (((dc_right_unit_exists_leftvaluemaskentry) = 2 * ge_signed_half_unit_exists_leftvaluemaskentryproductright + 1 /\ (sto_bp_unit_exists_leftvaluemaskentryproduct) = 0) /\ (sto_bn_unit_exists_leftvaluemaskentryproduct) = S ge_signed_half_unit_exists_leftvaluemaskentryproductright))) /\ ((((((dc_value_unit_exists_leftvaluemask) = 2 * (sto_cp_unit_exists_leftvaluemaskentryproduct) /\ (sto_cn_unit_exists_leftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_exists_leftvaluemaskentryproductoutput. (((dc_value_unit_exists_leftvaluemask) = 2 * ge_signed_half_unit_exists_leftvaluemaskentryproductoutput + 1 /\ (sto_cp_unit_exists_leftvaluemaskentryproduct) = 0) /\ (sto_cn_unit_exists_leftvaluemaskentryproduct) = S ge_signed_half_unit_exists_leftvaluemaskentryproductoutput))) /\ ((sto_ap_unit_exists_leftvaluemaskentryproduct * sto_bp_unit_exists_leftvaluemaskentryproduct + sto_an_unit_exists_leftvaluemaskentryproduct * sto_bn_unit_exists_leftvaluemaskentryproduct) + sto_cn_unit_exists_leftvaluemaskentryproduct = (sto_ap_unit_exists_leftvaluemaskentryproduct * sto_bn_unit_exists_leftvaluemaskentryproduct + sto_an_unit_exists_leftvaluemaskentryproduct * sto_bp_unit_exists_leftvaluemaskentryproduct) + sto_cp_unit_exists_leftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_unit_exists_leftvaluemask)=0 \/ ~(exists pvs_factor_unit_exists_leftvaluemaskentrynondivisor. (dc_input_unit_exists_left) = (dc_index_unit_exists_leftvaluemask) * pvs_factor_unit_exists_leftvaluemaskentrynondivisor)) /\ ((dc_value_unit_exists_leftvaluemask)=0))))))) /\ (exists dst_positive_code_unit_exists_leftvaluefold dst_positive_scale_unit_exists_leftvaluefold dst_negative_code_unit_exists_leftvaluefold dst_negative_scale_unit_exists_leftvaluefold dst_positive_sum_unit_exists_leftvaluefold dst_negative_sum_unit_exists_leftvaluefold. (((dc_mask_unit_exists_leftvalue) = (((((dst_positive_code_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold)) * S ((dst_positive_code_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold)) + ((dst_positive_scale_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold))) + (((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) * S ((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) + ((dst_negative_scale_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)))) * S ((((dst_positive_code_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold)) * S ((dst_positive_code_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold)) + ((dst_positive_scale_unit_exists_leftvaluefold) + (dst_positive_scale_unit_exists_leftvaluefold))) + (((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) * S ((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) + ((dst_negative_scale_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)))) + ((((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) * S ((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) + ((dst_negative_scale_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold))) + (((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) * S ((dst_negative_code_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)) + ((dst_negative_scale_unit_exists_leftvaluefold) + (dst_negative_scale_unit_exists_leftvaluefold)))))) /\ (((exists fs_u_dst_unit_exists_leftvaluefoldpositive fs_v_dst_unit_exists_leftvaluefoldpositive. ((((exists fs_h_dst_unit_exists_leftvaluefoldpositive_body_start. fs_h_dst_unit_exists_leftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_exists_leftvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_leftvaluefoldpositive_body_start. fs_u_dst_unit_exists_leftvaluefoldpositive = fs_q_dst_unit_exists_leftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_unit_exists_leftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldpositive_body_terminal. fs_h_dst_unit_exists_leftvaluefoldpositive_body_terminal + S (dst_positive_sum_unit_exists_leftvaluefold) = S ((S (S (dc_input_unit_exists_left))) * fs_v_dst_unit_exists_leftvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_leftvaluefoldpositive_body_terminal. fs_u_dst_unit_exists_leftvaluefoldpositive = fs_q_dst_unit_exists_leftvaluefoldpositive_body_terminal * S ((S (S (dc_input_unit_exists_left))) * fs_v_dst_unit_exists_leftvaluefoldpositive) + (dst_positive_sum_unit_exists_leftvaluefold))) /\ forall fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps. (exists fs_lt_dst_unit_exists_leftvaluefoldpositive_body_steps_bound. fs_lt_dst_unit_exists_leftvaluefoldpositive_body_steps_bound + S fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps = S (dc_input_unit_exists_left)) -> exists fs_a_dst_unit_exists_leftvaluefoldpositive_body_steps fs_r_dst_unit_exists_leftvaluefoldpositive_body_steps fs_s_dst_unit_exists_leftvaluefoldpositive_body_steps. ((((exists fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_summand. fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_summand + S (fs_a_dst_unit_exists_leftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * dst_positive_scale_unit_exists_leftvaluefold)) /\ exists fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_summand. dst_positive_code_unit_exists_leftvaluefold = fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * dst_positive_scale_unit_exists_leftvaluefold) + (fs_a_dst_unit_exists_leftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_partial. fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_partial + S (fs_r_dst_unit_exists_leftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_partial. fs_u_dst_unit_exists_leftvaluefoldpositive = fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldpositive) + (fs_r_dst_unit_exists_leftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_successor. fs_h_dst_unit_exists_leftvaluefoldpositive_body_steps_successor + S (fs_s_dst_unit_exists_leftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldpositive)) /\ exists fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_successor. fs_u_dst_unit_exists_leftvaluefoldpositive = fs_q_dst_unit_exists_leftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_unit_exists_leftvaluefoldpositive_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldpositive) + (fs_s_dst_unit_exists_leftvaluefoldpositive_body_steps))) /\ fs_s_dst_unit_exists_leftvaluefoldpositive_body_steps = fs_r_dst_unit_exists_leftvaluefoldpositive_body_steps + fs_a_dst_unit_exists_leftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_exists_leftvaluefoldnegative fs_v_dst_unit_exists_leftvaluefoldnegative. ((((exists fs_h_dst_unit_exists_leftvaluefoldnegative_body_start. fs_h_dst_unit_exists_leftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_exists_leftvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_leftvaluefoldnegative_body_start. fs_u_dst_unit_exists_leftvaluefoldnegative = fs_q_dst_unit_exists_leftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_unit_exists_leftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldnegative_body_terminal. fs_h_dst_unit_exists_leftvaluefoldnegative_body_terminal + S (dst_negative_sum_unit_exists_leftvaluefold) = S ((S (S (dc_input_unit_exists_left))) * fs_v_dst_unit_exists_leftvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_leftvaluefoldnegative_body_terminal. fs_u_dst_unit_exists_leftvaluefoldnegative = fs_q_dst_unit_exists_leftvaluefoldnegative_body_terminal * S ((S (S (dc_input_unit_exists_left))) * fs_v_dst_unit_exists_leftvaluefoldnegative) + (dst_negative_sum_unit_exists_leftvaluefold))) /\ forall fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps. (exists fs_lt_dst_unit_exists_leftvaluefoldnegative_body_steps_bound. fs_lt_dst_unit_exists_leftvaluefoldnegative_body_steps_bound + S fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps = S (dc_input_unit_exists_left)) -> exists fs_a_dst_unit_exists_leftvaluefoldnegative_body_steps fs_r_dst_unit_exists_leftvaluefoldnegative_body_steps fs_s_dst_unit_exists_leftvaluefoldnegative_body_steps. ((((exists fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_summand. fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_summand + S (fs_a_dst_unit_exists_leftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * dst_negative_scale_unit_exists_leftvaluefold)) /\ exists fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_summand. dst_negative_code_unit_exists_leftvaluefold = fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * dst_negative_scale_unit_exists_leftvaluefold) + (fs_a_dst_unit_exists_leftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_partial. fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_partial + S (fs_r_dst_unit_exists_leftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_partial. fs_u_dst_unit_exists_leftvaluefoldnegative = fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldnegative) + (fs_r_dst_unit_exists_leftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_successor. fs_h_dst_unit_exists_leftvaluefoldnegative_body_steps_successor + S (fs_s_dst_unit_exists_leftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldnegative)) /\ exists fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_successor. fs_u_dst_unit_exists_leftvaluefoldnegative = fs_q_dst_unit_exists_leftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_unit_exists_leftvaluefoldnegative_body_steps)) * fs_v_dst_unit_exists_leftvaluefoldnegative) + (fs_s_dst_unit_exists_leftvaluefoldnegative_body_steps))) /\ fs_s_dst_unit_exists_leftvaluefoldnegative_body_steps = fs_r_dst_unit_exists_leftvaluefoldnegative_body_steps + fs_a_dst_unit_exists_leftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_exists_leftvaluefoldresult ge_balance_negative_unit_exists_leftvaluefoldresult. (((((dc_output_unit_exists_left) = 2 * (ge_balance_positive_unit_exists_leftvaluefoldresult) /\ (ge_balance_negative_unit_exists_leftvaluefoldresult) = 0) \/ exists ge_signed_half_unit_exists_leftvaluefoldresultdecode. (((dc_output_unit_exists_left) = 2 * ge_signed_half_unit_exists_leftvaluefoldresultdecode + 1 /\ (ge_balance_positive_unit_exists_leftvaluefoldresult) = 0) /\ (ge_balance_negative_unit_exists_leftvaluefoldresult) = S ge_signed_half_unit_exists_leftvaluefoldresultdecode))) /\ ((dst_positive_sum_unit_exists_leftvaluefold) + ge_balance_negative_unit_exists_leftvaluefoldresult = (dst_negative_sum_unit_exists_leftvaluefold) + ge_balance_positive_unit_exists_leftvaluefoldresult)))))))))))))))))))))))))