dirichlet_convolution_associative_tables_exists

forall N F G H. (exists dst_positive_code_assoc_exists_F dst_positive_scale_assoc_exists_F dst_negative_code_assoc_exists_F dst_negative_scale_assoc_exists_F. (((F) = (((((dst_positive_code_assoc_exists_F) + (dst_positive_scale_assoc_exists_F)) * S ((dst_positive_code_assoc_exists_F) + (dst_positive_scale_assoc_exists_F)) + ((dst_positive_scale_assoc_exists_F) + (dst_positive_scale_assoc_exists_F))) + (((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) * S ((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) + ((dst_negative_scale_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)))) * S ((((dst_positive_code_assoc_exists_F) + (dst_positive_scale_assoc_exists_F)) * S ((dst_positive_code_assoc_exists_F) + (dst_positive_scale_assoc_exists_F)) + ((dst_positive_scale_assoc_exists_F) + (dst_positive_scale_assoc_exists_F))) + (((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) * S ((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) + ((dst_negative_scale_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)))) + ((((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) * S ((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) + ((dst_negative_scale_assoc_exists_F) + (dst_negative_scale_assoc_exists_F))) + (((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) * S ((dst_negative_code_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)) + ((dst_negative_scale_assoc_exists_F) + (dst_negative_scale_assoc_exists_F)))))) /\ (forall dst_index_assoc_exists_F. (exists pvs_le_gap_assoc_exists_Fdomain. pvs_le_gap_assoc_exists_Fdomain + (dst_index_assoc_exists_F) = (N)) -> exists dst_positive_assoc_exists_F dst_negative_assoc_exists_F dst_value_assoc_exists_F. ((((exists ff_h_pvs_assoc_exists_Fentrypositive. ff_h_pvs_assoc_exists_Fentrypositive + S (dst_positive_assoc_exists_F) = S ((S (dst_index_assoc_exists_F)) * dst_positive_scale_assoc_exists_F)) /\ exists ff_q_pvs_assoc_exists_Fentrypositive. dst_positive_code_assoc_exists_F = ff_q_pvs_assoc_exists_Fentrypositive * S ((S (dst_index_assoc_exists_F)) * dst_positive_scale_assoc_exists_F) + (dst_positive_assoc_exists_F))) /\ (((((exists ff_h_pvs_assoc_exists_Fentrynegative. ff_h_pvs_assoc_exists_Fentrynegative + S (dst_negative_assoc_exists_F) = S ((S (dst_index_assoc_exists_F)) * dst_negative_scale_assoc_exists_F)) /\ exists ff_q_pvs_assoc_exists_Fentrynegative. dst_negative_code_assoc_exists_F = ff_q_pvs_assoc_exists_Fentrynegative * S ((S (dst_index_assoc_exists_F)) * dst_negative_scale_assoc_exists_F) + (dst_negative_assoc_exists_F))) /\ (exists ge_balance_positive_assoc_exists_Fentryvalue ge_balance_negative_assoc_exists_Fentryvalue. (((((dst_value_assoc_exists_F) = 2 * (ge_balance_positive_assoc_exists_Fentryvalue) /\ (ge_balance_negative_assoc_exists_Fentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Fentryvaluedecode. (((dst_value_assoc_exists_F) = 2 * ge_signed_half_assoc_exists_Fentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Fentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Fentryvalue) = S ge_signed_half_assoc_exists_Fentryvaluedecode))) /\ ((dst_positive_assoc_exists_F) + ge_balance_negative_assoc_exists_Fentryvalue = (dst_negative_assoc_exists_F) + ge_balance_positive_assoc_exists_Fentryvalue))))))))) -> (exists dst_positive_code_assoc_exists_G dst_positive_scale_assoc_exists_G dst_negative_code_assoc_exists_G dst_negative_scale_assoc_exists_G. (((G) = (((((dst_positive_code_assoc_exists_G) + (dst_positive_scale_assoc_exists_G)) * S ((dst_positive_code_assoc_exists_G) + (dst_positive_scale_assoc_exists_G)) + ((dst_positive_scale_assoc_exists_G) + (dst_positive_scale_assoc_exists_G))) + (((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) * S ((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) + ((dst_negative_scale_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)))) * S ((((dst_positive_code_assoc_exists_G) + (dst_positive_scale_assoc_exists_G)) * S ((dst_positive_code_assoc_exists_G) + (dst_positive_scale_assoc_exists_G)) + ((dst_positive_scale_assoc_exists_G) + (dst_positive_scale_assoc_exists_G))) + (((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) * S ((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) + ((dst_negative_scale_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)))) + ((((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) * S ((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) + ((dst_negative_scale_assoc_exists_G) + (dst_negative_scale_assoc_exists_G))) + (((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) * S ((dst_negative_code_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)) + ((dst_negative_scale_assoc_exists_G) + (dst_negative_scale_assoc_exists_G)))))) /\ (forall dst_index_assoc_exists_G. (exists pvs_le_gap_assoc_exists_Gdomain. pvs_le_gap_assoc_exists_Gdomain + (dst_index_assoc_exists_G) = (N)) -> exists dst_positive_assoc_exists_G dst_negative_assoc_exists_G dst_value_assoc_exists_G. ((((exists ff_h_pvs_assoc_exists_Gentrypositive. ff_h_pvs_assoc_exists_Gentrypositive + S (dst_positive_assoc_exists_G) = S ((S (dst_index_assoc_exists_G)) * dst_positive_scale_assoc_exists_G)) /\ exists ff_q_pvs_assoc_exists_Gentrypositive. dst_positive_code_assoc_exists_G = ff_q_pvs_assoc_exists_Gentrypositive * S ((S (dst_index_assoc_exists_G)) * dst_positive_scale_assoc_exists_G) + (dst_positive_assoc_exists_G))) /\ (((((exists ff_h_pvs_assoc_exists_Gentrynegative. ff_h_pvs_assoc_exists_Gentrynegative + S (dst_negative_assoc_exists_G) = S ((S (dst_index_assoc_exists_G)) * dst_negative_scale_assoc_exists_G)) /\ exists ff_q_pvs_assoc_exists_Gentrynegative. dst_negative_code_assoc_exists_G = ff_q_pvs_assoc_exists_Gentrynegative * S ((S (dst_index_assoc_exists_G)) * dst_negative_scale_assoc_exists_G) + (dst_negative_assoc_exists_G))) /\ (exists ge_balance_positive_assoc_exists_Gentryvalue ge_balance_negative_assoc_exists_Gentryvalue. (((((dst_value_assoc_exists_G) = 2 * (ge_balance_positive_assoc_exists_Gentryvalue) /\ (ge_balance_negative_assoc_exists_Gentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Gentryvaluedecode. (((dst_value_assoc_exists_G) = 2 * ge_signed_half_assoc_exists_Gentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Gentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Gentryvalue) = S ge_signed_half_assoc_exists_Gentryvaluedecode))) /\ ((dst_positive_assoc_exists_G) + ge_balance_negative_assoc_exists_Gentryvalue = (dst_negative_assoc_exists_G) + ge_balance_positive_assoc_exists_Gentryvalue))))))))) -> (exists dst_positive_code_assoc_exists_H dst_positive_scale_assoc_exists_H dst_negative_code_assoc_exists_H dst_negative_scale_assoc_exists_H. (((H) = (((((dst_positive_code_assoc_exists_H) + (dst_positive_scale_assoc_exists_H)) * S ((dst_positive_code_assoc_exists_H) + (dst_positive_scale_assoc_exists_H)) + ((dst_positive_scale_assoc_exists_H) + (dst_positive_scale_assoc_exists_H))) + (((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) * S ((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) + ((dst_negative_scale_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)))) * S ((((dst_positive_code_assoc_exists_H) + (dst_positive_scale_assoc_exists_H)) * S ((dst_positive_code_assoc_exists_H) + (dst_positive_scale_assoc_exists_H)) + ((dst_positive_scale_assoc_exists_H) + (dst_positive_scale_assoc_exists_H))) + (((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) * S ((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) + ((dst_negative_scale_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)))) + ((((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) * S ((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) + ((dst_negative_scale_assoc_exists_H) + (dst_negative_scale_assoc_exists_H))) + (((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) * S ((dst_negative_code_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)) + ((dst_negative_scale_assoc_exists_H) + (dst_negative_scale_assoc_exists_H)))))) /\ (forall dst_index_assoc_exists_H. (exists pvs_le_gap_assoc_exists_Hdomain. pvs_le_gap_assoc_exists_Hdomain + (dst_index_assoc_exists_H) = (N)) -> exists dst_positive_assoc_exists_H dst_negative_assoc_exists_H dst_value_assoc_exists_H. ((((exists ff_h_pvs_assoc_exists_Hentrypositive. ff_h_pvs_assoc_exists_Hentrypositive + S (dst_positive_assoc_exists_H) = S ((S (dst_index_assoc_exists_H)) * dst_positive_scale_assoc_exists_H)) /\ exists ff_q_pvs_assoc_exists_Hentrypositive. dst_positive_code_assoc_exists_H = ff_q_pvs_assoc_exists_Hentrypositive * S ((S (dst_index_assoc_exists_H)) * dst_positive_scale_assoc_exists_H) + (dst_positive_assoc_exists_H))) /\ (((((exists ff_h_pvs_assoc_exists_Hentrynegative. ff_h_pvs_assoc_exists_Hentrynegative + S (dst_negative_assoc_exists_H) = S ((S (dst_index_assoc_exists_H)) * dst_negative_scale_assoc_exists_H)) /\ exists ff_q_pvs_assoc_exists_Hentrynegative. dst_negative_code_assoc_exists_H = ff_q_pvs_assoc_exists_Hentrynegative * S ((S (dst_index_assoc_exists_H)) * dst_negative_scale_assoc_exists_H) + (dst_negative_assoc_exists_H))) /\ (exists ge_balance_positive_assoc_exists_Hentryvalue ge_balance_negative_assoc_exists_Hentryvalue. (((((dst_value_assoc_exists_H) = 2 * (ge_balance_positive_assoc_exists_Hentryvalue) /\ (ge_balance_negative_assoc_exists_Hentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Hentryvaluedecode. (((dst_value_assoc_exists_H) = 2 * ge_signed_half_assoc_exists_Hentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Hentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Hentryvalue) = S ge_signed_half_assoc_exists_Hentryvaluedecode))) /\ ((dst_positive_assoc_exists_H) + ge_balance_negative_assoc_exists_Hentryvalue = (dst_negative_assoc_exists_H) + ge_balance_positive_assoc_exists_Hentryvalue))))))))) -> exists A B L R. ((((exists dst_positive_code_assoc_exists_Aleft dst_positive_scale_assoc_exists_Aleft dst_negative_code_assoc_exists_Aleft dst_negative_scale_assoc_exists_Aleft. (((F) = (((((dst_positive_code_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft)) * S ((dst_positive_code_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft)) + ((dst_positive_scale_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft))) + (((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) * S ((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) + ((dst_negative_scale_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)))) * S ((((dst_positive_code_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft)) * S ((dst_positive_code_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft)) + ((dst_positive_scale_assoc_exists_Aleft) + (dst_positive_scale_assoc_exists_Aleft))) + (((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) * S ((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) + ((dst_negative_scale_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)))) + ((((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) * S ((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) + ((dst_negative_scale_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft))) + (((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) * S ((dst_negative_code_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)) + ((dst_negative_scale_assoc_exists_Aleft) + (dst_negative_scale_assoc_exists_Aleft)))))) /\ (forall dst_index_assoc_exists_Aleft. (exists pvs_le_gap_assoc_exists_Aleftdomain. pvs_le_gap_assoc_exists_Aleftdomain + (dst_index_assoc_exists_Aleft) = (N)) -> exists dst_positive_assoc_exists_Aleft dst_negative_assoc_exists_Aleft dst_value_assoc_exists_Aleft. ((((exists ff_h_pvs_assoc_exists_Aleftentrypositive. ff_h_pvs_assoc_exists_Aleftentrypositive + S (dst_positive_assoc_exists_Aleft) = S ((S (dst_index_assoc_exists_Aleft)) * dst_positive_scale_assoc_exists_Aleft)) /\ exists ff_q_pvs_assoc_exists_Aleftentrypositive. dst_positive_code_assoc_exists_Aleft = ff_q_pvs_assoc_exists_Aleftentrypositive * S ((S (dst_index_assoc_exists_Aleft)) * dst_positive_scale_assoc_exists_Aleft) + (dst_positive_assoc_exists_Aleft))) /\ (((((exists ff_h_pvs_assoc_exists_Aleftentrynegative. ff_h_pvs_assoc_exists_Aleftentrynegative + S (dst_negative_assoc_exists_Aleft) = S ((S (dst_index_assoc_exists_Aleft)) * dst_negative_scale_assoc_exists_Aleft)) /\ exists ff_q_pvs_assoc_exists_Aleftentrynegative. dst_negative_code_assoc_exists_Aleft = ff_q_pvs_assoc_exists_Aleftentrynegative * S ((S (dst_index_assoc_exists_Aleft)) * dst_negative_scale_assoc_exists_Aleft) + (dst_negative_assoc_exists_Aleft))) /\ (exists ge_balance_positive_assoc_exists_Aleftentryvalue ge_balance_negative_assoc_exists_Aleftentryvalue. (((((dst_value_assoc_exists_Aleft) = 2 * (ge_balance_positive_assoc_exists_Aleftentryvalue) /\ (ge_balance_negative_assoc_exists_Aleftentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Aleftentryvaluedecode. (((dst_value_assoc_exists_Aleft) = 2 * ge_signed_half_assoc_exists_Aleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Aleftentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Aleftentryvalue) = S ge_signed_half_assoc_exists_Aleftentryvaluedecode))) /\ ((dst_positive_assoc_exists_Aleft) + ge_balance_negative_assoc_exists_Aleftentryvalue = (dst_negative_assoc_exists_Aleft) + ge_balance_positive_assoc_exists_Aleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Aright dst_positive_scale_assoc_exists_Aright dst_negative_code_assoc_exists_Aright dst_negative_scale_assoc_exists_Aright. (((G) = (((((dst_positive_code_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright)) * S ((dst_positive_code_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright)) + ((dst_positive_scale_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright))) + (((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) * S ((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) + ((dst_negative_scale_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)))) * S ((((dst_positive_code_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright)) * S ((dst_positive_code_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright)) + ((dst_positive_scale_assoc_exists_Aright) + (dst_positive_scale_assoc_exists_Aright))) + (((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) * S ((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) + ((dst_negative_scale_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)))) + ((((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) * S ((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) + ((dst_negative_scale_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright))) + (((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) * S ((dst_negative_code_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)) + ((dst_negative_scale_assoc_exists_Aright) + (dst_negative_scale_assoc_exists_Aright)))))) /\ (forall dst_index_assoc_exists_Aright. (exists pvs_le_gap_assoc_exists_Arightdomain. pvs_le_gap_assoc_exists_Arightdomain + (dst_index_assoc_exists_Aright) = (N)) -> exists dst_positive_assoc_exists_Aright dst_negative_assoc_exists_Aright dst_value_assoc_exists_Aright. ((((exists ff_h_pvs_assoc_exists_Arightentrypositive. ff_h_pvs_assoc_exists_Arightentrypositive + S (dst_positive_assoc_exists_Aright) = S ((S (dst_index_assoc_exists_Aright)) * dst_positive_scale_assoc_exists_Aright)) /\ exists ff_q_pvs_assoc_exists_Arightentrypositive. dst_positive_code_assoc_exists_Aright = ff_q_pvs_assoc_exists_Arightentrypositive * S ((S (dst_index_assoc_exists_Aright)) * dst_positive_scale_assoc_exists_Aright) + (dst_positive_assoc_exists_Aright))) /\ (((((exists ff_h_pvs_assoc_exists_Arightentrynegative. ff_h_pvs_assoc_exists_Arightentrynegative + S (dst_negative_assoc_exists_Aright) = S ((S (dst_index_assoc_exists_Aright)) * dst_negative_scale_assoc_exists_Aright)) /\ exists ff_q_pvs_assoc_exists_Arightentrynegative. dst_negative_code_assoc_exists_Aright = ff_q_pvs_assoc_exists_Arightentrynegative * S ((S (dst_index_assoc_exists_Aright)) * dst_negative_scale_assoc_exists_Aright) + (dst_negative_assoc_exists_Aright))) /\ (exists ge_balance_positive_assoc_exists_Arightentryvalue ge_balance_negative_assoc_exists_Arightentryvalue. (((((dst_value_assoc_exists_Aright) = 2 * (ge_balance_positive_assoc_exists_Arightentryvalue) /\ (ge_balance_negative_assoc_exists_Arightentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Arightentryvaluedecode. (((dst_value_assoc_exists_Aright) = 2 * ge_signed_half_assoc_exists_Arightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Arightentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Arightentryvalue) = S ge_signed_half_assoc_exists_Arightentryvaluedecode))) /\ ((dst_positive_assoc_exists_Aright) + ge_balance_negative_assoc_exists_Arightentryvalue = (dst_negative_assoc_exists_Aright) + ge_balance_positive_assoc_exists_Arightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Atable dst_positive_scale_assoc_exists_Atable dst_negative_code_assoc_exists_Atable dst_negative_scale_assoc_exists_Atable. (((A) = (((((dst_positive_code_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable)) * S ((dst_positive_code_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable)) + ((dst_positive_scale_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable))) + (((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) * S ((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) + ((dst_negative_scale_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)))) * S ((((dst_positive_code_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable)) * S ((dst_positive_code_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable)) + ((dst_positive_scale_assoc_exists_Atable) + (dst_positive_scale_assoc_exists_Atable))) + (((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) * S ((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) + ((dst_negative_scale_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)))) + ((((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) * S ((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) + ((dst_negative_scale_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable))) + (((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) * S ((dst_negative_code_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)) + ((dst_negative_scale_assoc_exists_Atable) + (dst_negative_scale_assoc_exists_Atable)))))) /\ (forall dst_index_assoc_exists_Atable. (exists pvs_le_gap_assoc_exists_Atabledomain. pvs_le_gap_assoc_exists_Atabledomain + (dst_index_assoc_exists_Atable) = (N)) -> exists dst_positive_assoc_exists_Atable dst_negative_assoc_exists_Atable dst_value_assoc_exists_Atable. ((((exists ff_h_pvs_assoc_exists_Atableentrypositive. ff_h_pvs_assoc_exists_Atableentrypositive + S (dst_positive_assoc_exists_Atable) = S ((S (dst_index_assoc_exists_Atable)) * dst_positive_scale_assoc_exists_Atable)) /\ exists ff_q_pvs_assoc_exists_Atableentrypositive. dst_positive_code_assoc_exists_Atable = ff_q_pvs_assoc_exists_Atableentrypositive * S ((S (dst_index_assoc_exists_Atable)) * dst_positive_scale_assoc_exists_Atable) + (dst_positive_assoc_exists_Atable))) /\ (((((exists ff_h_pvs_assoc_exists_Atableentrynegative. ff_h_pvs_assoc_exists_Atableentrynegative + S (dst_negative_assoc_exists_Atable) = S ((S (dst_index_assoc_exists_Atable)) * dst_negative_scale_assoc_exists_Atable)) /\ exists ff_q_pvs_assoc_exists_Atableentrynegative. dst_negative_code_assoc_exists_Atable = ff_q_pvs_assoc_exists_Atableentrynegative * S ((S (dst_index_assoc_exists_Atable)) * dst_negative_scale_assoc_exists_Atable) + (dst_negative_assoc_exists_Atable))) /\ (exists ge_balance_positive_assoc_exists_Atableentryvalue ge_balance_negative_assoc_exists_Atableentryvalue. (((((dst_value_assoc_exists_Atable) = 2 * (ge_balance_positive_assoc_exists_Atableentryvalue) /\ (ge_balance_negative_assoc_exists_Atableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Atableentryvaluedecode. (((dst_value_assoc_exists_Atable) = 2 * ge_signed_half_assoc_exists_Atableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Atableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Atableentryvalue) = S ge_signed_half_assoc_exists_Atableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Atable) + ge_balance_negative_assoc_exists_Atableentryvalue = (dst_negative_assoc_exists_Atable) + ge_balance_positive_assoc_exists_Atableentryvalue))))))))) /\ (forall dc_input_assoc_exists_A dc_output_assoc_exists_A. ~(dc_input_assoc_exists_A=0) -> (exists pvs_le_gap_assoc_exists_Adomain. pvs_le_gap_assoc_exists_Adomain + (dc_input_assoc_exists_A) = (N)) -> (exists dst_positive_code_assoc_exists_Alookup dst_positive_scale_assoc_exists_Alookup dst_negative_code_assoc_exists_Alookup dst_negative_scale_assoc_exists_Alookup dst_positive_assoc_exists_Alookup dst_negative_assoc_exists_Alookup. (((A) = (((((dst_positive_code_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup)) * S ((dst_positive_code_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup)) + ((dst_positive_scale_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup))) + (((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) * S ((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) + ((dst_negative_scale_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)))) * S ((((dst_positive_code_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup)) * S ((dst_positive_code_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup)) + ((dst_positive_scale_assoc_exists_Alookup) + (dst_positive_scale_assoc_exists_Alookup))) + (((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) * S ((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) + ((dst_negative_scale_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)))) + ((((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) * S ((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) + ((dst_negative_scale_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup))) + (((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) * S ((dst_negative_code_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)) + ((dst_negative_scale_assoc_exists_Alookup) + (dst_negative_scale_assoc_exists_Alookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Alookuppositive. ff_h_pvs_assoc_exists_Alookuppositive + S (dst_positive_assoc_exists_Alookup) = S ((S (dc_input_assoc_exists_A)) * dst_positive_scale_assoc_exists_Alookup)) /\ exists ff_q_pvs_assoc_exists_Alookuppositive. dst_positive_code_assoc_exists_Alookup = ff_q_pvs_assoc_exists_Alookuppositive * S ((S (dc_input_assoc_exists_A)) * dst_positive_scale_assoc_exists_Alookup) + (dst_positive_assoc_exists_Alookup))) /\ (((((exists ff_h_pvs_assoc_exists_Alookupnegative. ff_h_pvs_assoc_exists_Alookupnegative + S (dst_negative_assoc_exists_Alookup) = S ((S (dc_input_assoc_exists_A)) * dst_negative_scale_assoc_exists_Alookup)) /\ exists ff_q_pvs_assoc_exists_Alookupnegative. dst_negative_code_assoc_exists_Alookup = ff_q_pvs_assoc_exists_Alookupnegative * S ((S (dc_input_assoc_exists_A)) * dst_negative_scale_assoc_exists_Alookup) + (dst_negative_assoc_exists_Alookup))) /\ (exists ge_balance_positive_assoc_exists_Alookupvalue ge_balance_negative_assoc_exists_Alookupvalue. (((((dc_output_assoc_exists_A) = 2 * (ge_balance_positive_assoc_exists_Alookupvalue) /\ (ge_balance_negative_assoc_exists_Alookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Alookupvaluedecode. (((dc_output_assoc_exists_A) = 2 * ge_signed_half_assoc_exists_Alookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Alookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Alookupvalue) = S ge_signed_half_assoc_exists_Alookupvaluedecode))) /\ ((dst_positive_assoc_exists_Alookup) + ge_balance_negative_assoc_exists_Alookupvalue = (dst_negative_assoc_exists_Alookup) + ge_balance_positive_assoc_exists_Alookupvalue))))))))) -> (((~((dc_input_assoc_exists_A)=0)) /\ (exists dc_mask_assoc_exists_Avalue. ((((exists dst_positive_code_assoc_exists_Avaluemasktable dst_positive_scale_assoc_exists_Avaluemasktable dst_negative_code_assoc_exists_Avaluemasktable dst_negative_scale_assoc_exists_Avaluemasktable. (((dc_mask_assoc_exists_Avalue) = (((((dst_positive_code_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable)) * S ((dst_positive_code_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable)) + ((dst_positive_scale_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable))) + (((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) * S ((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) + ((dst_negative_scale_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)))) * S ((((dst_positive_code_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable)) * S ((dst_positive_code_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable)) + ((dst_positive_scale_assoc_exists_Avaluemasktable) + (dst_positive_scale_assoc_exists_Avaluemasktable))) + (((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) * S ((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) + ((dst_negative_scale_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)))) + ((((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) * S ((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) + ((dst_negative_scale_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable))) + (((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) * S ((dst_negative_code_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)) + ((dst_negative_scale_assoc_exists_Avaluemasktable) + (dst_negative_scale_assoc_exists_Avaluemasktable)))))) /\ (forall dst_index_assoc_exists_Avaluemasktable. (exists pvs_le_gap_assoc_exists_Avaluemasktabledomain. pvs_le_gap_assoc_exists_Avaluemasktabledomain + (dst_index_assoc_exists_Avaluemasktable) = (dc_input_assoc_exists_A)) -> exists dst_positive_assoc_exists_Avaluemasktable dst_negative_assoc_exists_Avaluemasktable dst_value_assoc_exists_Avaluemasktable. ((((exists ff_h_pvs_assoc_exists_Avaluemasktableentrypositive. ff_h_pvs_assoc_exists_Avaluemasktableentrypositive + S (dst_positive_assoc_exists_Avaluemasktable) = S ((S (dst_index_assoc_exists_Avaluemasktable)) * dst_positive_scale_assoc_exists_Avaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Avaluemasktableentrypositive. dst_positive_code_assoc_exists_Avaluemasktable = ff_q_pvs_assoc_exists_Avaluemasktableentrypositive * S ((S (dst_index_assoc_exists_Avaluemasktable)) * dst_positive_scale_assoc_exists_Avaluemasktable) + (dst_positive_assoc_exists_Avaluemasktable))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemasktableentrynegative. ff_h_pvs_assoc_exists_Avaluemasktableentrynegative + S (dst_negative_assoc_exists_Avaluemasktable) = S ((S (dst_index_assoc_exists_Avaluemasktable)) * dst_negative_scale_assoc_exists_Avaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Avaluemasktableentrynegative. dst_negative_code_assoc_exists_Avaluemasktable = ff_q_pvs_assoc_exists_Avaluemasktableentrynegative * S ((S (dst_index_assoc_exists_Avaluemasktable)) * dst_negative_scale_assoc_exists_Avaluemasktable) + (dst_negative_assoc_exists_Avaluemasktable))) /\ (exists ge_balance_positive_assoc_exists_Avaluemasktableentryvalue ge_balance_negative_assoc_exists_Avaluemasktableentryvalue. (((((dst_value_assoc_exists_Avaluemasktable) = 2 * (ge_balance_positive_assoc_exists_Avaluemasktableentryvalue) /\ (ge_balance_negative_assoc_exists_Avaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemasktableentryvaluedecode. (((dst_value_assoc_exists_Avaluemasktable) = 2 * ge_signed_half_assoc_exists_Avaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Avaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Avaluemasktableentryvalue) = S ge_signed_half_assoc_exists_Avaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Avaluemasktable) + ge_balance_negative_assoc_exists_Avaluemasktableentryvalue = (dst_negative_assoc_exists_Avaluemasktable) + ge_balance_positive_assoc_exists_Avaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_exists_Avaluemask dc_value_assoc_exists_Avaluemask. (exists pvs_le_gap_assoc_exists_Avaluemaskdomain. pvs_le_gap_assoc_exists_Avaluemaskdomain + (dc_index_assoc_exists_Avaluemask) = (dc_input_assoc_exists_A)) -> (exists dst_positive_code_assoc_exists_Avaluemasklookup dst_positive_scale_assoc_exists_Avaluemasklookup dst_negative_code_assoc_exists_Avaluemasklookup dst_negative_scale_assoc_exists_Avaluemasklookup dst_positive_assoc_exists_Avaluemasklookup dst_negative_assoc_exists_Avaluemasklookup. (((dc_mask_assoc_exists_Avalue) = (((((dst_positive_code_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup)) * S ((dst_positive_code_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup)) + ((dst_positive_scale_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup))) + (((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) * S ((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) + ((dst_negative_scale_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)))) * S ((((dst_positive_code_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup)) * S ((dst_positive_code_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup)) + ((dst_positive_scale_assoc_exists_Avaluemasklookup) + (dst_positive_scale_assoc_exists_Avaluemasklookup))) + (((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) * S ((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) + ((dst_negative_scale_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)))) + ((((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) * S ((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) + ((dst_negative_scale_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup))) + (((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) * S ((dst_negative_code_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)) + ((dst_negative_scale_assoc_exists_Avaluemasklookup) + (dst_negative_scale_assoc_exists_Avaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemasklookuppositive. ff_h_pvs_assoc_exists_Avaluemasklookuppositive + S (dst_positive_assoc_exists_Avaluemasklookup) = S ((S (dc_index_assoc_exists_Avaluemask)) * dst_positive_scale_assoc_exists_Avaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Avaluemasklookuppositive. dst_positive_code_assoc_exists_Avaluemasklookup = ff_q_pvs_assoc_exists_Avaluemasklookuppositive * S ((S (dc_index_assoc_exists_Avaluemask)) * dst_positive_scale_assoc_exists_Avaluemasklookup) + (dst_positive_assoc_exists_Avaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemasklookupnegative. ff_h_pvs_assoc_exists_Avaluemasklookupnegative + S (dst_negative_assoc_exists_Avaluemasklookup) = S ((S (dc_index_assoc_exists_Avaluemask)) * dst_negative_scale_assoc_exists_Avaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Avaluemasklookupnegative. dst_negative_code_assoc_exists_Avaluemasklookup = ff_q_pvs_assoc_exists_Avaluemasklookupnegative * S ((S (dc_index_assoc_exists_Avaluemask)) * dst_negative_scale_assoc_exists_Avaluemasklookup) + (dst_negative_assoc_exists_Avaluemasklookup))) /\ (exists ge_balance_positive_assoc_exists_Avaluemasklookupvalue ge_balance_negative_assoc_exists_Avaluemasklookupvalue. (((((dc_value_assoc_exists_Avaluemask) = 2 * (ge_balance_positive_assoc_exists_Avaluemasklookupvalue) /\ (ge_balance_negative_assoc_exists_Avaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemasklookupvaluedecode. (((dc_value_assoc_exists_Avaluemask) = 2 * ge_signed_half_assoc_exists_Avaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Avaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Avaluemasklookupvalue) = S ge_signed_half_assoc_exists_Avaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_exists_Avaluemasklookup) + ge_balance_negative_assoc_exists_Avaluemasklookupvalue = (dst_negative_assoc_exists_Avaluemasklookup) + ge_balance_positive_assoc_exists_Avaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_exists_Avaluemask)=0)) /\ (exists dc_quotient_assoc_exists_Avaluemaskentry dc_left_assoc_exists_Avaluemaskentry dc_right_assoc_exists_Avaluemaskentry. (((dc_input_assoc_exists_A)=(dc_index_assoc_exists_Avaluemask)*dc_quotient_assoc_exists_Avaluemaskentry) /\ (((exists dst_positive_code_assoc_exists_Avaluemaskentryleft dst_positive_scale_assoc_exists_Avaluemaskentryleft dst_negative_code_assoc_exists_Avaluemaskentryleft dst_negative_scale_assoc_exists_Avaluemaskentryleft dst_positive_assoc_exists_Avaluemaskentryleft dst_negative_assoc_exists_Avaluemaskentryleft. (((F) = (((((dst_positive_code_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)))) * S ((((dst_positive_code_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Avaluemaskentryleft) + (dst_positive_scale_assoc_exists_Avaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)))) + ((((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryleft) + (dst_negative_scale_assoc_exists_Avaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemaskentryleftpositive. ff_h_pvs_assoc_exists_Avaluemaskentryleftpositive + S (dst_positive_assoc_exists_Avaluemaskentryleft) = S ((S (dc_index_assoc_exists_Avaluemask)) * dst_positive_scale_assoc_exists_Avaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Avaluemaskentryleftpositive. dst_positive_code_assoc_exists_Avaluemaskentryleft = ff_q_pvs_assoc_exists_Avaluemaskentryleftpositive * S ((S (dc_index_assoc_exists_Avaluemask)) * dst_positive_scale_assoc_exists_Avaluemaskentryleft) + (dst_positive_assoc_exists_Avaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemaskentryleftnegative. ff_h_pvs_assoc_exists_Avaluemaskentryleftnegative + S (dst_negative_assoc_exists_Avaluemaskentryleft) = S ((S (dc_index_assoc_exists_Avaluemask)) * dst_negative_scale_assoc_exists_Avaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Avaluemaskentryleftnegative. dst_negative_code_assoc_exists_Avaluemaskentryleft = ff_q_pvs_assoc_exists_Avaluemaskentryleftnegative * S ((S (dc_index_assoc_exists_Avaluemask)) * dst_negative_scale_assoc_exists_Avaluemaskentryleft) + (dst_negative_assoc_exists_Avaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_exists_Avaluemaskentryleftvalue ge_balance_negative_assoc_exists_Avaluemaskentryleftvalue. (((((dc_left_assoc_exists_Avaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Avaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_exists_Avaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemaskentryleftvaluedecode. (((dc_left_assoc_exists_Avaluemaskentry) = 2 * ge_signed_half_assoc_exists_Avaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Avaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_exists_Avaluemaskentryleftvalue) = S ge_signed_half_assoc_exists_Avaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_exists_Avaluemaskentryleft) + ge_balance_negative_assoc_exists_Avaluemaskentryleftvalue = (dst_negative_assoc_exists_Avaluemaskentryleft) + ge_balance_positive_assoc_exists_Avaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Avaluemaskentryright dst_positive_scale_assoc_exists_Avaluemaskentryright dst_negative_code_assoc_exists_Avaluemaskentryright dst_negative_scale_assoc_exists_Avaluemaskentryright dst_positive_assoc_exists_Avaluemaskentryright dst_negative_assoc_exists_Avaluemaskentryright. (((G) = (((((dst_positive_code_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright))) + (((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)))) * S ((((dst_positive_code_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Avaluemaskentryright) + (dst_positive_scale_assoc_exists_Avaluemaskentryright))) + (((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)))) + ((((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright))) + (((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Avaluemaskentryright) + (dst_negative_scale_assoc_exists_Avaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemaskentryrightpositive. ff_h_pvs_assoc_exists_Avaluemaskentryrightpositive + S (dst_positive_assoc_exists_Avaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Avaluemaskentry)) * dst_positive_scale_assoc_exists_Avaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Avaluemaskentryrightpositive. dst_positive_code_assoc_exists_Avaluemaskentryright = ff_q_pvs_assoc_exists_Avaluemaskentryrightpositive * S ((S (dc_quotient_assoc_exists_Avaluemaskentry)) * dst_positive_scale_assoc_exists_Avaluemaskentryright) + (dst_positive_assoc_exists_Avaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_exists_Avaluemaskentryrightnegative. ff_h_pvs_assoc_exists_Avaluemaskentryrightnegative + S (dst_negative_assoc_exists_Avaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Avaluemaskentry)) * dst_negative_scale_assoc_exists_Avaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Avaluemaskentryrightnegative. dst_negative_code_assoc_exists_Avaluemaskentryright = ff_q_pvs_assoc_exists_Avaluemaskentryrightnegative * S ((S (dc_quotient_assoc_exists_Avaluemaskentry)) * dst_negative_scale_assoc_exists_Avaluemaskentryright) + (dst_negative_assoc_exists_Avaluemaskentryright))) /\ (exists ge_balance_positive_assoc_exists_Avaluemaskentryrightvalue ge_balance_negative_assoc_exists_Avaluemaskentryrightvalue. (((((dc_right_assoc_exists_Avaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Avaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_exists_Avaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemaskentryrightvaluedecode. (((dc_right_assoc_exists_Avaluemaskentry) = 2 * ge_signed_half_assoc_exists_Avaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Avaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_exists_Avaluemaskentryrightvalue) = S ge_signed_half_assoc_exists_Avaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_exists_Avaluemaskentryright) + ge_balance_negative_assoc_exists_Avaluemaskentryrightvalue = (dst_negative_assoc_exists_Avaluemaskentryright) + ge_balance_positive_assoc_exists_Avaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_exists_Avaluemaskentryproduct sto_an_assoc_exists_Avaluemaskentryproduct sto_bp_assoc_exists_Avaluemaskentryproduct sto_bn_assoc_exists_Avaluemaskentryproduct sto_cp_assoc_exists_Avaluemaskentryproduct sto_cn_assoc_exists_Avaluemaskentryproduct. (((((dc_left_assoc_exists_Avaluemaskentry) = 2 * (sto_ap_assoc_exists_Avaluemaskentryproduct) /\ (sto_an_assoc_exists_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemaskentryproductleft. (((dc_left_assoc_exists_Avaluemaskentry) = 2 * ge_signed_half_assoc_exists_Avaluemaskentryproductleft + 1 /\ (sto_ap_assoc_exists_Avaluemaskentryproduct) = 0) /\ (sto_an_assoc_exists_Avaluemaskentryproduct) = S ge_signed_half_assoc_exists_Avaluemaskentryproductleft))) /\ ((((((dc_right_assoc_exists_Avaluemaskentry) = 2 * (sto_bp_assoc_exists_Avaluemaskentryproduct) /\ (sto_bn_assoc_exists_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemaskentryproductright. (((dc_right_assoc_exists_Avaluemaskentry) = 2 * ge_signed_half_assoc_exists_Avaluemaskentryproductright + 1 /\ (sto_bp_assoc_exists_Avaluemaskentryproduct) = 0) /\ (sto_bn_assoc_exists_Avaluemaskentryproduct) = S ge_signed_half_assoc_exists_Avaluemaskentryproductright))) /\ ((((((dc_value_assoc_exists_Avaluemask) = 2 * (sto_cp_assoc_exists_Avaluemaskentryproduct) /\ (sto_cn_assoc_exists_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Avaluemaskentryproductoutput. (((dc_value_assoc_exists_Avaluemask) = 2 * ge_signed_half_assoc_exists_Avaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_exists_Avaluemaskentryproduct) = 0) /\ (sto_cn_assoc_exists_Avaluemaskentryproduct) = S ge_signed_half_assoc_exists_Avaluemaskentryproductoutput))) /\ ((sto_ap_assoc_exists_Avaluemaskentryproduct * sto_bp_assoc_exists_Avaluemaskentryproduct + sto_an_assoc_exists_Avaluemaskentryproduct * sto_bn_assoc_exists_Avaluemaskentryproduct) + sto_cn_assoc_exists_Avaluemaskentryproduct = (sto_ap_assoc_exists_Avaluemaskentryproduct * sto_bn_assoc_exists_Avaluemaskentryproduct + sto_an_assoc_exists_Avaluemaskentryproduct * sto_bp_assoc_exists_Avaluemaskentryproduct) + sto_cp_assoc_exists_Avaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_exists_Avaluemask)=0 \/ ~(exists pvs_factor_assoc_exists_Avaluemaskentrynondivisor. (dc_input_assoc_exists_A) = (dc_index_assoc_exists_Avaluemask) * pvs_factor_assoc_exists_Avaluemaskentrynondivisor)) /\ ((dc_value_assoc_exists_Avaluemask)=0))))))) /\ (exists dst_positive_code_assoc_exists_Avaluefold dst_positive_scale_assoc_exists_Avaluefold dst_negative_code_assoc_exists_Avaluefold dst_negative_scale_assoc_exists_Avaluefold dst_positive_sum_assoc_exists_Avaluefold dst_negative_sum_assoc_exists_Avaluefold. (((dc_mask_assoc_exists_Avalue) = (((((dst_positive_code_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold)) * S ((dst_positive_code_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold)) + ((dst_positive_scale_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold))) + (((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) * S ((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) + ((dst_negative_scale_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)))) * S ((((dst_positive_code_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold)) * S ((dst_positive_code_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold)) + ((dst_positive_scale_assoc_exists_Avaluefold) + (dst_positive_scale_assoc_exists_Avaluefold))) + (((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) * S ((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) + ((dst_negative_scale_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)))) + ((((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) * S ((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) + ((dst_negative_scale_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold))) + (((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) * S ((dst_negative_code_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)) + ((dst_negative_scale_assoc_exists_Avaluefold) + (dst_negative_scale_assoc_exists_Avaluefold)))))) /\ (((exists fs_u_dst_assoc_exists_Avaluefoldpositive fs_v_dst_assoc_exists_Avaluefoldpositive. ((((exists fs_h_dst_assoc_exists_Avaluefoldpositive_body_start. fs_h_dst_assoc_exists_Avaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Avaluefoldpositive_body_start. fs_u_dst_assoc_exists_Avaluefoldpositive = fs_q_dst_assoc_exists_Avaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Avaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldpositive_body_terminal. fs_h_dst_assoc_exists_Avaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_exists_Avaluefold) = S ((S (S (dc_input_assoc_exists_A))) * fs_v_dst_assoc_exists_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Avaluefoldpositive_body_terminal. fs_u_dst_assoc_exists_Avaluefoldpositive = fs_q_dst_assoc_exists_Avaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_exists_A))) * fs_v_dst_assoc_exists_Avaluefoldpositive) + (dst_positive_sum_assoc_exists_Avaluefold))) /\ forall fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_exists_Avaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_exists_Avaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps = S (dc_input_assoc_exists_A)) -> exists fs_a_dst_assoc_exists_Avaluefoldpositive_body_steps fs_r_dst_assoc_exists_Avaluefoldpositive_body_steps fs_s_dst_assoc_exists_Avaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_summand. fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_exists_Avaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Avaluefold)) /\ exists fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_summand. dst_positive_code_assoc_exists_Avaluefold = fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Avaluefold) + (fs_a_dst_assoc_exists_Avaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_partial. fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_exists_Avaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_partial. fs_u_dst_assoc_exists_Avaluefoldpositive = fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldpositive) + (fs_r_dst_assoc_exists_Avaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_successor. fs_h_dst_assoc_exists_Avaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_exists_Avaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_successor. fs_u_dst_assoc_exists_Avaluefoldpositive = fs_q_dst_assoc_exists_Avaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldpositive) + (fs_s_dst_assoc_exists_Avaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_exists_Avaluefoldpositive_body_steps = fs_r_dst_assoc_exists_Avaluefoldpositive_body_steps + fs_a_dst_assoc_exists_Avaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_exists_Avaluefoldnegative fs_v_dst_assoc_exists_Avaluefoldnegative. ((((exists fs_h_dst_assoc_exists_Avaluefoldnegative_body_start. fs_h_dst_assoc_exists_Avaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Avaluefoldnegative_body_start. fs_u_dst_assoc_exists_Avaluefoldnegative = fs_q_dst_assoc_exists_Avaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Avaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldnegative_body_terminal. fs_h_dst_assoc_exists_Avaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_exists_Avaluefold) = S ((S (S (dc_input_assoc_exists_A))) * fs_v_dst_assoc_exists_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Avaluefoldnegative_body_terminal. fs_u_dst_assoc_exists_Avaluefoldnegative = fs_q_dst_assoc_exists_Avaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_exists_A))) * fs_v_dst_assoc_exists_Avaluefoldnegative) + (dst_negative_sum_assoc_exists_Avaluefold))) /\ forall fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_exists_Avaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_exists_Avaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps = S (dc_input_assoc_exists_A)) -> exists fs_a_dst_assoc_exists_Avaluefoldnegative_body_steps fs_r_dst_assoc_exists_Avaluefoldnegative_body_steps fs_s_dst_assoc_exists_Avaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_summand. fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_exists_Avaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Avaluefold)) /\ exists fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_summand. dst_negative_code_assoc_exists_Avaluefold = fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Avaluefold) + (fs_a_dst_assoc_exists_Avaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_partial. fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_exists_Avaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_partial. fs_u_dst_assoc_exists_Avaluefoldnegative = fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldnegative) + (fs_r_dst_assoc_exists_Avaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_successor. fs_h_dst_assoc_exists_Avaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_exists_Avaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_successor. fs_u_dst_assoc_exists_Avaluefoldnegative = fs_q_dst_assoc_exists_Avaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Avaluefoldnegative) + (fs_s_dst_assoc_exists_Avaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_exists_Avaluefoldnegative_body_steps = fs_r_dst_assoc_exists_Avaluefoldnegative_body_steps + fs_a_dst_assoc_exists_Avaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_exists_Avaluefoldresult ge_balance_negative_assoc_exists_Avaluefoldresult. (((((dc_output_assoc_exists_A) = 2 * (ge_balance_positive_assoc_exists_Avaluefoldresult) /\ (ge_balance_negative_assoc_exists_Avaluefoldresult) = 0) \/ exists ge_signed_half_assoc_exists_Avaluefoldresultdecode. (((dc_output_assoc_exists_A) = 2 * ge_signed_half_assoc_exists_Avaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_exists_Avaluefoldresult) = 0) /\ (ge_balance_negative_assoc_exists_Avaluefoldresult) = S ge_signed_half_assoc_exists_Avaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_exists_Avaluefold) + ge_balance_negative_assoc_exists_Avaluefoldresult = (dst_negative_sum_assoc_exists_Avaluefold) + ge_balance_positive_assoc_exists_Avaluefoldresult)))))))))))))))))))) /\ (((((exists dst_positive_code_assoc_exists_Bleft dst_positive_scale_assoc_exists_Bleft dst_negative_code_assoc_exists_Bleft dst_negative_scale_assoc_exists_Bleft. (((G) = (((((dst_positive_code_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft)) * S ((dst_positive_code_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft)) + ((dst_positive_scale_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft))) + (((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) * S ((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) + ((dst_negative_scale_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)))) * S ((((dst_positive_code_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft)) * S ((dst_positive_code_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft)) + ((dst_positive_scale_assoc_exists_Bleft) + (dst_positive_scale_assoc_exists_Bleft))) + (((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) * S ((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) + ((dst_negative_scale_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)))) + ((((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) * S ((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) + ((dst_negative_scale_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft))) + (((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) * S ((dst_negative_code_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)) + ((dst_negative_scale_assoc_exists_Bleft) + (dst_negative_scale_assoc_exists_Bleft)))))) /\ (forall dst_index_assoc_exists_Bleft. (exists pvs_le_gap_assoc_exists_Bleftdomain. pvs_le_gap_assoc_exists_Bleftdomain + (dst_index_assoc_exists_Bleft) = (N)) -> exists dst_positive_assoc_exists_Bleft dst_negative_assoc_exists_Bleft dst_value_assoc_exists_Bleft. ((((exists ff_h_pvs_assoc_exists_Bleftentrypositive. ff_h_pvs_assoc_exists_Bleftentrypositive + S (dst_positive_assoc_exists_Bleft) = S ((S (dst_index_assoc_exists_Bleft)) * dst_positive_scale_assoc_exists_Bleft)) /\ exists ff_q_pvs_assoc_exists_Bleftentrypositive. dst_positive_code_assoc_exists_Bleft = ff_q_pvs_assoc_exists_Bleftentrypositive * S ((S (dst_index_assoc_exists_Bleft)) * dst_positive_scale_assoc_exists_Bleft) + (dst_positive_assoc_exists_Bleft))) /\ (((((exists ff_h_pvs_assoc_exists_Bleftentrynegative. ff_h_pvs_assoc_exists_Bleftentrynegative + S (dst_negative_assoc_exists_Bleft) = S ((S (dst_index_assoc_exists_Bleft)) * dst_negative_scale_assoc_exists_Bleft)) /\ exists ff_q_pvs_assoc_exists_Bleftentrynegative. dst_negative_code_assoc_exists_Bleft = ff_q_pvs_assoc_exists_Bleftentrynegative * S ((S (dst_index_assoc_exists_Bleft)) * dst_negative_scale_assoc_exists_Bleft) + (dst_negative_assoc_exists_Bleft))) /\ (exists ge_balance_positive_assoc_exists_Bleftentryvalue ge_balance_negative_assoc_exists_Bleftentryvalue. (((((dst_value_assoc_exists_Bleft) = 2 * (ge_balance_positive_assoc_exists_Bleftentryvalue) /\ (ge_balance_negative_assoc_exists_Bleftentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Bleftentryvaluedecode. (((dst_value_assoc_exists_Bleft) = 2 * ge_signed_half_assoc_exists_Bleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Bleftentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Bleftentryvalue) = S ge_signed_half_assoc_exists_Bleftentryvaluedecode))) /\ ((dst_positive_assoc_exists_Bleft) + ge_balance_negative_assoc_exists_Bleftentryvalue = (dst_negative_assoc_exists_Bleft) + ge_balance_positive_assoc_exists_Bleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Bright dst_positive_scale_assoc_exists_Bright dst_negative_code_assoc_exists_Bright dst_negative_scale_assoc_exists_Bright. (((H) = (((((dst_positive_code_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright)) * S ((dst_positive_code_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright)) + ((dst_positive_scale_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright))) + (((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) * S ((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) + ((dst_negative_scale_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)))) * S ((((dst_positive_code_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright)) * S ((dst_positive_code_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright)) + ((dst_positive_scale_assoc_exists_Bright) + (dst_positive_scale_assoc_exists_Bright))) + (((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) * S ((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) + ((dst_negative_scale_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)))) + ((((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) * S ((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) + ((dst_negative_scale_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright))) + (((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) * S ((dst_negative_code_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)) + ((dst_negative_scale_assoc_exists_Bright) + (dst_negative_scale_assoc_exists_Bright)))))) /\ (forall dst_index_assoc_exists_Bright. (exists pvs_le_gap_assoc_exists_Brightdomain. pvs_le_gap_assoc_exists_Brightdomain + (dst_index_assoc_exists_Bright) = (N)) -> exists dst_positive_assoc_exists_Bright dst_negative_assoc_exists_Bright dst_value_assoc_exists_Bright. ((((exists ff_h_pvs_assoc_exists_Brightentrypositive. ff_h_pvs_assoc_exists_Brightentrypositive + S (dst_positive_assoc_exists_Bright) = S ((S (dst_index_assoc_exists_Bright)) * dst_positive_scale_assoc_exists_Bright)) /\ exists ff_q_pvs_assoc_exists_Brightentrypositive. dst_positive_code_assoc_exists_Bright = ff_q_pvs_assoc_exists_Brightentrypositive * S ((S (dst_index_assoc_exists_Bright)) * dst_positive_scale_assoc_exists_Bright) + (dst_positive_assoc_exists_Bright))) /\ (((((exists ff_h_pvs_assoc_exists_Brightentrynegative. ff_h_pvs_assoc_exists_Brightentrynegative + S (dst_negative_assoc_exists_Bright) = S ((S (dst_index_assoc_exists_Bright)) * dst_negative_scale_assoc_exists_Bright)) /\ exists ff_q_pvs_assoc_exists_Brightentrynegative. dst_negative_code_assoc_exists_Bright = ff_q_pvs_assoc_exists_Brightentrynegative * S ((S (dst_index_assoc_exists_Bright)) * dst_negative_scale_assoc_exists_Bright) + (dst_negative_assoc_exists_Bright))) /\ (exists ge_balance_positive_assoc_exists_Brightentryvalue ge_balance_negative_assoc_exists_Brightentryvalue. (((((dst_value_assoc_exists_Bright) = 2 * (ge_balance_positive_assoc_exists_Brightentryvalue) /\ (ge_balance_negative_assoc_exists_Brightentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Brightentryvaluedecode. (((dst_value_assoc_exists_Bright) = 2 * ge_signed_half_assoc_exists_Brightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Brightentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Brightentryvalue) = S ge_signed_half_assoc_exists_Brightentryvaluedecode))) /\ ((dst_positive_assoc_exists_Bright) + ge_balance_negative_assoc_exists_Brightentryvalue = (dst_negative_assoc_exists_Bright) + ge_balance_positive_assoc_exists_Brightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Btable dst_positive_scale_assoc_exists_Btable dst_negative_code_assoc_exists_Btable dst_negative_scale_assoc_exists_Btable. (((B) = (((((dst_positive_code_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable)) * S ((dst_positive_code_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable)) + ((dst_positive_scale_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable))) + (((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) * S ((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) + ((dst_negative_scale_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)))) * S ((((dst_positive_code_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable)) * S ((dst_positive_code_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable)) + ((dst_positive_scale_assoc_exists_Btable) + (dst_positive_scale_assoc_exists_Btable))) + (((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) * S ((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) + ((dst_negative_scale_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)))) + ((((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) * S ((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) + ((dst_negative_scale_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable))) + (((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) * S ((dst_negative_code_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)) + ((dst_negative_scale_assoc_exists_Btable) + (dst_negative_scale_assoc_exists_Btable)))))) /\ (forall dst_index_assoc_exists_Btable. (exists pvs_le_gap_assoc_exists_Btabledomain. pvs_le_gap_assoc_exists_Btabledomain + (dst_index_assoc_exists_Btable) = (N)) -> exists dst_positive_assoc_exists_Btable dst_negative_assoc_exists_Btable dst_value_assoc_exists_Btable. ((((exists ff_h_pvs_assoc_exists_Btableentrypositive. ff_h_pvs_assoc_exists_Btableentrypositive + S (dst_positive_assoc_exists_Btable) = S ((S (dst_index_assoc_exists_Btable)) * dst_positive_scale_assoc_exists_Btable)) /\ exists ff_q_pvs_assoc_exists_Btableentrypositive. dst_positive_code_assoc_exists_Btable = ff_q_pvs_assoc_exists_Btableentrypositive * S ((S (dst_index_assoc_exists_Btable)) * dst_positive_scale_assoc_exists_Btable) + (dst_positive_assoc_exists_Btable))) /\ (((((exists ff_h_pvs_assoc_exists_Btableentrynegative. ff_h_pvs_assoc_exists_Btableentrynegative + S (dst_negative_assoc_exists_Btable) = S ((S (dst_index_assoc_exists_Btable)) * dst_negative_scale_assoc_exists_Btable)) /\ exists ff_q_pvs_assoc_exists_Btableentrynegative. dst_negative_code_assoc_exists_Btable = ff_q_pvs_assoc_exists_Btableentrynegative * S ((S (dst_index_assoc_exists_Btable)) * dst_negative_scale_assoc_exists_Btable) + (dst_negative_assoc_exists_Btable))) /\ (exists ge_balance_positive_assoc_exists_Btableentryvalue ge_balance_negative_assoc_exists_Btableentryvalue. (((((dst_value_assoc_exists_Btable) = 2 * (ge_balance_positive_assoc_exists_Btableentryvalue) /\ (ge_balance_negative_assoc_exists_Btableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Btableentryvaluedecode. (((dst_value_assoc_exists_Btable) = 2 * ge_signed_half_assoc_exists_Btableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Btableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Btableentryvalue) = S ge_signed_half_assoc_exists_Btableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Btable) + ge_balance_negative_assoc_exists_Btableentryvalue = (dst_negative_assoc_exists_Btable) + ge_balance_positive_assoc_exists_Btableentryvalue))))))))) /\ (forall dc_input_assoc_exists_B dc_output_assoc_exists_B. ~(dc_input_assoc_exists_B=0) -> (exists pvs_le_gap_assoc_exists_Bdomain. pvs_le_gap_assoc_exists_Bdomain + (dc_input_assoc_exists_B) = (N)) -> (exists dst_positive_code_assoc_exists_Blookup dst_positive_scale_assoc_exists_Blookup dst_negative_code_assoc_exists_Blookup dst_negative_scale_assoc_exists_Blookup dst_positive_assoc_exists_Blookup dst_negative_assoc_exists_Blookup. (((B) = (((((dst_positive_code_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup)) * S ((dst_positive_code_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup)) + ((dst_positive_scale_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup))) + (((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) * S ((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) + ((dst_negative_scale_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)))) * S ((((dst_positive_code_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup)) * S ((dst_positive_code_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup)) + ((dst_positive_scale_assoc_exists_Blookup) + (dst_positive_scale_assoc_exists_Blookup))) + (((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) * S ((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) + ((dst_negative_scale_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)))) + ((((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) * S ((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) + ((dst_negative_scale_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup))) + (((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) * S ((dst_negative_code_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)) + ((dst_negative_scale_assoc_exists_Blookup) + (dst_negative_scale_assoc_exists_Blookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Blookuppositive. ff_h_pvs_assoc_exists_Blookuppositive + S (dst_positive_assoc_exists_Blookup) = S ((S (dc_input_assoc_exists_B)) * dst_positive_scale_assoc_exists_Blookup)) /\ exists ff_q_pvs_assoc_exists_Blookuppositive. dst_positive_code_assoc_exists_Blookup = ff_q_pvs_assoc_exists_Blookuppositive * S ((S (dc_input_assoc_exists_B)) * dst_positive_scale_assoc_exists_Blookup) + (dst_positive_assoc_exists_Blookup))) /\ (((((exists ff_h_pvs_assoc_exists_Blookupnegative. ff_h_pvs_assoc_exists_Blookupnegative + S (dst_negative_assoc_exists_Blookup) = S ((S (dc_input_assoc_exists_B)) * dst_negative_scale_assoc_exists_Blookup)) /\ exists ff_q_pvs_assoc_exists_Blookupnegative. dst_negative_code_assoc_exists_Blookup = ff_q_pvs_assoc_exists_Blookupnegative * S ((S (dc_input_assoc_exists_B)) * dst_negative_scale_assoc_exists_Blookup) + (dst_negative_assoc_exists_Blookup))) /\ (exists ge_balance_positive_assoc_exists_Blookupvalue ge_balance_negative_assoc_exists_Blookupvalue. (((((dc_output_assoc_exists_B) = 2 * (ge_balance_positive_assoc_exists_Blookupvalue) /\ (ge_balance_negative_assoc_exists_Blookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Blookupvaluedecode. (((dc_output_assoc_exists_B) = 2 * ge_signed_half_assoc_exists_Blookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Blookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Blookupvalue) = S ge_signed_half_assoc_exists_Blookupvaluedecode))) /\ ((dst_positive_assoc_exists_Blookup) + ge_balance_negative_assoc_exists_Blookupvalue = (dst_negative_assoc_exists_Blookup) + ge_balance_positive_assoc_exists_Blookupvalue))))))))) -> (((~((dc_input_assoc_exists_B)=0)) /\ (exists dc_mask_assoc_exists_Bvalue. ((((exists dst_positive_code_assoc_exists_Bvaluemasktable dst_positive_scale_assoc_exists_Bvaluemasktable dst_negative_code_assoc_exists_Bvaluemasktable dst_negative_scale_assoc_exists_Bvaluemasktable. (((dc_mask_assoc_exists_Bvalue) = (((((dst_positive_code_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable)) * S ((dst_positive_code_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable)) + ((dst_positive_scale_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable))) + (((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) * S ((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) + ((dst_negative_scale_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)))) * S ((((dst_positive_code_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable)) * S ((dst_positive_code_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable)) + ((dst_positive_scale_assoc_exists_Bvaluemasktable) + (dst_positive_scale_assoc_exists_Bvaluemasktable))) + (((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) * S ((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) + ((dst_negative_scale_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)))) + ((((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) * S ((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) + ((dst_negative_scale_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable))) + (((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) * S ((dst_negative_code_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)) + ((dst_negative_scale_assoc_exists_Bvaluemasktable) + (dst_negative_scale_assoc_exists_Bvaluemasktable)))))) /\ (forall dst_index_assoc_exists_Bvaluemasktable. (exists pvs_le_gap_assoc_exists_Bvaluemasktabledomain. pvs_le_gap_assoc_exists_Bvaluemasktabledomain + (dst_index_assoc_exists_Bvaluemasktable) = (dc_input_assoc_exists_B)) -> exists dst_positive_assoc_exists_Bvaluemasktable dst_negative_assoc_exists_Bvaluemasktable dst_value_assoc_exists_Bvaluemasktable. ((((exists ff_h_pvs_assoc_exists_Bvaluemasktableentrypositive. ff_h_pvs_assoc_exists_Bvaluemasktableentrypositive + S (dst_positive_assoc_exists_Bvaluemasktable) = S ((S (dst_index_assoc_exists_Bvaluemasktable)) * dst_positive_scale_assoc_exists_Bvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Bvaluemasktableentrypositive. dst_positive_code_assoc_exists_Bvaluemasktable = ff_q_pvs_assoc_exists_Bvaluemasktableentrypositive * S ((S (dst_index_assoc_exists_Bvaluemasktable)) * dst_positive_scale_assoc_exists_Bvaluemasktable) + (dst_positive_assoc_exists_Bvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemasktableentrynegative. ff_h_pvs_assoc_exists_Bvaluemasktableentrynegative + S (dst_negative_assoc_exists_Bvaluemasktable) = S ((S (dst_index_assoc_exists_Bvaluemasktable)) * dst_negative_scale_assoc_exists_Bvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Bvaluemasktableentrynegative. dst_negative_code_assoc_exists_Bvaluemasktable = ff_q_pvs_assoc_exists_Bvaluemasktableentrynegative * S ((S (dst_index_assoc_exists_Bvaluemasktable)) * dst_negative_scale_assoc_exists_Bvaluemasktable) + (dst_negative_assoc_exists_Bvaluemasktable))) /\ (exists ge_balance_positive_assoc_exists_Bvaluemasktableentryvalue ge_balance_negative_assoc_exists_Bvaluemasktableentryvalue. (((((dst_value_assoc_exists_Bvaluemasktable) = 2 * (ge_balance_positive_assoc_exists_Bvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_exists_Bvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemasktableentryvaluedecode. (((dst_value_assoc_exists_Bvaluemasktable) = 2 * ge_signed_half_assoc_exists_Bvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Bvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Bvaluemasktableentryvalue) = S ge_signed_half_assoc_exists_Bvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Bvaluemasktable) + ge_balance_negative_assoc_exists_Bvaluemasktableentryvalue = (dst_negative_assoc_exists_Bvaluemasktable) + ge_balance_positive_assoc_exists_Bvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_exists_Bvaluemask dc_value_assoc_exists_Bvaluemask. (exists pvs_le_gap_assoc_exists_Bvaluemaskdomain. pvs_le_gap_assoc_exists_Bvaluemaskdomain + (dc_index_assoc_exists_Bvaluemask) = (dc_input_assoc_exists_B)) -> (exists dst_positive_code_assoc_exists_Bvaluemasklookup dst_positive_scale_assoc_exists_Bvaluemasklookup dst_negative_code_assoc_exists_Bvaluemasklookup dst_negative_scale_assoc_exists_Bvaluemasklookup dst_positive_assoc_exists_Bvaluemasklookup dst_negative_assoc_exists_Bvaluemasklookup. (((dc_mask_assoc_exists_Bvalue) = (((((dst_positive_code_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup))) + (((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)))) * S ((((dst_positive_code_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Bvaluemasklookup) + (dst_positive_scale_assoc_exists_Bvaluemasklookup))) + (((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)))) + ((((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup))) + (((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Bvaluemasklookup) + (dst_negative_scale_assoc_exists_Bvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemasklookuppositive. ff_h_pvs_assoc_exists_Bvaluemasklookuppositive + S (dst_positive_assoc_exists_Bvaluemasklookup) = S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_positive_scale_assoc_exists_Bvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Bvaluemasklookuppositive. dst_positive_code_assoc_exists_Bvaluemasklookup = ff_q_pvs_assoc_exists_Bvaluemasklookuppositive * S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_positive_scale_assoc_exists_Bvaluemasklookup) + (dst_positive_assoc_exists_Bvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemasklookupnegative. ff_h_pvs_assoc_exists_Bvaluemasklookupnegative + S (dst_negative_assoc_exists_Bvaluemasklookup) = S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_negative_scale_assoc_exists_Bvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Bvaluemasklookupnegative. dst_negative_code_assoc_exists_Bvaluemasklookup = ff_q_pvs_assoc_exists_Bvaluemasklookupnegative * S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_negative_scale_assoc_exists_Bvaluemasklookup) + (dst_negative_assoc_exists_Bvaluemasklookup))) /\ (exists ge_balance_positive_assoc_exists_Bvaluemasklookupvalue ge_balance_negative_assoc_exists_Bvaluemasklookupvalue. (((((dc_value_assoc_exists_Bvaluemask) = 2 * (ge_balance_positive_assoc_exists_Bvaluemasklookupvalue) /\ (ge_balance_negative_assoc_exists_Bvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemasklookupvaluedecode. (((dc_value_assoc_exists_Bvaluemask) = 2 * ge_signed_half_assoc_exists_Bvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Bvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Bvaluemasklookupvalue) = S ge_signed_half_assoc_exists_Bvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_exists_Bvaluemasklookup) + ge_balance_negative_assoc_exists_Bvaluemasklookupvalue = (dst_negative_assoc_exists_Bvaluemasklookup) + ge_balance_positive_assoc_exists_Bvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_exists_Bvaluemask)=0)) /\ (exists dc_quotient_assoc_exists_Bvaluemaskentry dc_left_assoc_exists_Bvaluemaskentry dc_right_assoc_exists_Bvaluemaskentry. (((dc_input_assoc_exists_B)=(dc_index_assoc_exists_Bvaluemask)*dc_quotient_assoc_exists_Bvaluemaskentry) /\ (((exists dst_positive_code_assoc_exists_Bvaluemaskentryleft dst_positive_scale_assoc_exists_Bvaluemaskentryleft dst_negative_code_assoc_exists_Bvaluemaskentryleft dst_negative_scale_assoc_exists_Bvaluemaskentryleft dst_positive_assoc_exists_Bvaluemaskentryleft dst_negative_assoc_exists_Bvaluemaskentryleft. (((G) = (((((dst_positive_code_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Bvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)))) + ((((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Bvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemaskentryleftpositive. ff_h_pvs_assoc_exists_Bvaluemaskentryleftpositive + S (dst_positive_assoc_exists_Bvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_positive_scale_assoc_exists_Bvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Bvaluemaskentryleftpositive. dst_positive_code_assoc_exists_Bvaluemaskentryleft = ff_q_pvs_assoc_exists_Bvaluemaskentryleftpositive * S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_positive_scale_assoc_exists_Bvaluemaskentryleft) + (dst_positive_assoc_exists_Bvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemaskentryleftnegative. ff_h_pvs_assoc_exists_Bvaluemaskentryleftnegative + S (dst_negative_assoc_exists_Bvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_negative_scale_assoc_exists_Bvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Bvaluemaskentryleftnegative. dst_negative_code_assoc_exists_Bvaluemaskentryleft = ff_q_pvs_assoc_exists_Bvaluemaskentryleftnegative * S ((S (dc_index_assoc_exists_Bvaluemask)) * dst_negative_scale_assoc_exists_Bvaluemaskentryleft) + (dst_negative_assoc_exists_Bvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_exists_Bvaluemaskentryleftvalue ge_balance_negative_assoc_exists_Bvaluemaskentryleftvalue. (((((dc_left_assoc_exists_Bvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Bvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_exists_Bvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemaskentryleftvaluedecode. (((dc_left_assoc_exists_Bvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Bvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Bvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_exists_Bvaluemaskentryleftvalue) = S ge_signed_half_assoc_exists_Bvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_exists_Bvaluemaskentryleft) + ge_balance_negative_assoc_exists_Bvaluemaskentryleftvalue = (dst_negative_assoc_exists_Bvaluemaskentryleft) + ge_balance_positive_assoc_exists_Bvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Bvaluemaskentryright dst_positive_scale_assoc_exists_Bvaluemaskentryright dst_negative_code_assoc_exists_Bvaluemaskentryright dst_negative_scale_assoc_exists_Bvaluemaskentryright dst_positive_assoc_exists_Bvaluemaskentryright dst_negative_assoc_exists_Bvaluemaskentryright. (((H) = (((((dst_positive_code_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)))) * S ((((dst_positive_code_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Bvaluemaskentryright) + (dst_positive_scale_assoc_exists_Bvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)))) + ((((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Bvaluemaskentryright) + (dst_negative_scale_assoc_exists_Bvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemaskentryrightpositive. ff_h_pvs_assoc_exists_Bvaluemaskentryrightpositive + S (dst_positive_assoc_exists_Bvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Bvaluemaskentry)) * dst_positive_scale_assoc_exists_Bvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Bvaluemaskentryrightpositive. dst_positive_code_assoc_exists_Bvaluemaskentryright = ff_q_pvs_assoc_exists_Bvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_exists_Bvaluemaskentry)) * dst_positive_scale_assoc_exists_Bvaluemaskentryright) + (dst_positive_assoc_exists_Bvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_exists_Bvaluemaskentryrightnegative. ff_h_pvs_assoc_exists_Bvaluemaskentryrightnegative + S (dst_negative_assoc_exists_Bvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Bvaluemaskentry)) * dst_negative_scale_assoc_exists_Bvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Bvaluemaskentryrightnegative. dst_negative_code_assoc_exists_Bvaluemaskentryright = ff_q_pvs_assoc_exists_Bvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_exists_Bvaluemaskentry)) * dst_negative_scale_assoc_exists_Bvaluemaskentryright) + (dst_negative_assoc_exists_Bvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_exists_Bvaluemaskentryrightvalue ge_balance_negative_assoc_exists_Bvaluemaskentryrightvalue. (((((dc_right_assoc_exists_Bvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Bvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_exists_Bvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemaskentryrightvaluedecode. (((dc_right_assoc_exists_Bvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Bvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Bvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_exists_Bvaluemaskentryrightvalue) = S ge_signed_half_assoc_exists_Bvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_exists_Bvaluemaskentryright) + ge_balance_negative_assoc_exists_Bvaluemaskentryrightvalue = (dst_negative_assoc_exists_Bvaluemaskentryright) + ge_balance_positive_assoc_exists_Bvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_exists_Bvaluemaskentryproduct sto_an_assoc_exists_Bvaluemaskentryproduct sto_bp_assoc_exists_Bvaluemaskentryproduct sto_bn_assoc_exists_Bvaluemaskentryproduct sto_cp_assoc_exists_Bvaluemaskentryproduct sto_cn_assoc_exists_Bvaluemaskentryproduct. (((((dc_left_assoc_exists_Bvaluemaskentry) = 2 * (sto_ap_assoc_exists_Bvaluemaskentryproduct) /\ (sto_an_assoc_exists_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemaskentryproductleft. (((dc_left_assoc_exists_Bvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Bvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_exists_Bvaluemaskentryproduct) = 0) /\ (sto_an_assoc_exists_Bvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Bvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_exists_Bvaluemaskentry) = 2 * (sto_bp_assoc_exists_Bvaluemaskentryproduct) /\ (sto_bn_assoc_exists_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemaskentryproductright. (((dc_right_assoc_exists_Bvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Bvaluemaskentryproductright + 1 /\ (sto_bp_assoc_exists_Bvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_exists_Bvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Bvaluemaskentryproductright))) /\ ((((((dc_value_assoc_exists_Bvaluemask) = 2 * (sto_cp_assoc_exists_Bvaluemaskentryproduct) /\ (sto_cn_assoc_exists_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluemaskentryproductoutput. (((dc_value_assoc_exists_Bvaluemask) = 2 * ge_signed_half_assoc_exists_Bvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_exists_Bvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_exists_Bvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Bvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_exists_Bvaluemaskentryproduct * sto_bp_assoc_exists_Bvaluemaskentryproduct + sto_an_assoc_exists_Bvaluemaskentryproduct * sto_bn_assoc_exists_Bvaluemaskentryproduct) + sto_cn_assoc_exists_Bvaluemaskentryproduct = (sto_ap_assoc_exists_Bvaluemaskentryproduct * sto_bn_assoc_exists_Bvaluemaskentryproduct + sto_an_assoc_exists_Bvaluemaskentryproduct * sto_bp_assoc_exists_Bvaluemaskentryproduct) + sto_cp_assoc_exists_Bvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_exists_Bvaluemask)=0 \/ ~(exists pvs_factor_assoc_exists_Bvaluemaskentrynondivisor. (dc_input_assoc_exists_B) = (dc_index_assoc_exists_Bvaluemask) * pvs_factor_assoc_exists_Bvaluemaskentrynondivisor)) /\ ((dc_value_assoc_exists_Bvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_exists_Bvaluefold dst_positive_scale_assoc_exists_Bvaluefold dst_negative_code_assoc_exists_Bvaluefold dst_negative_scale_assoc_exists_Bvaluefold dst_positive_sum_assoc_exists_Bvaluefold dst_negative_sum_assoc_exists_Bvaluefold. (((dc_mask_assoc_exists_Bvalue) = (((((dst_positive_code_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold)) * S ((dst_positive_code_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold)) + ((dst_positive_scale_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold))) + (((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) * S ((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) + ((dst_negative_scale_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)))) * S ((((dst_positive_code_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold)) * S ((dst_positive_code_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold)) + ((dst_positive_scale_assoc_exists_Bvaluefold) + (dst_positive_scale_assoc_exists_Bvaluefold))) + (((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) * S ((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) + ((dst_negative_scale_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)))) + ((((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) * S ((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) + ((dst_negative_scale_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold))) + (((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) * S ((dst_negative_code_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)) + ((dst_negative_scale_assoc_exists_Bvaluefold) + (dst_negative_scale_assoc_exists_Bvaluefold)))))) /\ (((exists fs_u_dst_assoc_exists_Bvaluefoldpositive fs_v_dst_assoc_exists_Bvaluefoldpositive. ((((exists fs_h_dst_assoc_exists_Bvaluefoldpositive_body_start. fs_h_dst_assoc_exists_Bvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldpositive_body_start. fs_u_dst_assoc_exists_Bvaluefoldpositive = fs_q_dst_assoc_exists_Bvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Bvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldpositive_body_terminal. fs_h_dst_assoc_exists_Bvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_exists_Bvaluefold) = S ((S (S (dc_input_assoc_exists_B))) * fs_v_dst_assoc_exists_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldpositive_body_terminal. fs_u_dst_assoc_exists_Bvaluefoldpositive = fs_q_dst_assoc_exists_Bvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_exists_B))) * fs_v_dst_assoc_exists_Bvaluefoldpositive) + (dst_positive_sum_assoc_exists_Bvaluefold))) /\ forall fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_exists_Bvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_exists_Bvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps = S (dc_input_assoc_exists_B)) -> exists fs_a_dst_assoc_exists_Bvaluefoldpositive_body_steps fs_r_dst_assoc_exists_Bvaluefoldpositive_body_steps fs_s_dst_assoc_exists_Bvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_exists_Bvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Bvaluefold)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_exists_Bvaluefold = fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Bvaluefold) + (fs_a_dst_assoc_exists_Bvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_exists_Bvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_exists_Bvaluefoldpositive = fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldpositive) + (fs_r_dst_assoc_exists_Bvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_exists_Bvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_exists_Bvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_exists_Bvaluefoldpositive = fs_q_dst_assoc_exists_Bvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldpositive) + (fs_s_dst_assoc_exists_Bvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_exists_Bvaluefoldpositive_body_steps = fs_r_dst_assoc_exists_Bvaluefoldpositive_body_steps + fs_a_dst_assoc_exists_Bvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_exists_Bvaluefoldnegative fs_v_dst_assoc_exists_Bvaluefoldnegative. ((((exists fs_h_dst_assoc_exists_Bvaluefoldnegative_body_start. fs_h_dst_assoc_exists_Bvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldnegative_body_start. fs_u_dst_assoc_exists_Bvaluefoldnegative = fs_q_dst_assoc_exists_Bvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Bvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldnegative_body_terminal. fs_h_dst_assoc_exists_Bvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_exists_Bvaluefold) = S ((S (S (dc_input_assoc_exists_B))) * fs_v_dst_assoc_exists_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldnegative_body_terminal. fs_u_dst_assoc_exists_Bvaluefoldnegative = fs_q_dst_assoc_exists_Bvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_exists_B))) * fs_v_dst_assoc_exists_Bvaluefoldnegative) + (dst_negative_sum_assoc_exists_Bvaluefold))) /\ forall fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_exists_Bvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_exists_Bvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps = S (dc_input_assoc_exists_B)) -> exists fs_a_dst_assoc_exists_Bvaluefoldnegative_body_steps fs_r_dst_assoc_exists_Bvaluefoldnegative_body_steps fs_s_dst_assoc_exists_Bvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_exists_Bvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Bvaluefold)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_exists_Bvaluefold = fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Bvaluefold) + (fs_a_dst_assoc_exists_Bvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_exists_Bvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_exists_Bvaluefoldnegative = fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldnegative) + (fs_r_dst_assoc_exists_Bvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_exists_Bvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_exists_Bvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_exists_Bvaluefoldnegative = fs_q_dst_assoc_exists_Bvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Bvaluefoldnegative) + (fs_s_dst_assoc_exists_Bvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_exists_Bvaluefoldnegative_body_steps = fs_r_dst_assoc_exists_Bvaluefoldnegative_body_steps + fs_a_dst_assoc_exists_Bvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_exists_Bvaluefoldresult ge_balance_negative_assoc_exists_Bvaluefoldresult. (((((dc_output_assoc_exists_B) = 2 * (ge_balance_positive_assoc_exists_Bvaluefoldresult) /\ (ge_balance_negative_assoc_exists_Bvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_exists_Bvaluefoldresultdecode. (((dc_output_assoc_exists_B) = 2 * ge_signed_half_assoc_exists_Bvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_exists_Bvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_exists_Bvaluefoldresult) = S ge_signed_half_assoc_exists_Bvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_exists_Bvaluefold) + ge_balance_negative_assoc_exists_Bvaluefoldresult = (dst_negative_sum_assoc_exists_Bvaluefold) + ge_balance_positive_assoc_exists_Bvaluefoldresult)))))))))))))))))))) /\ (((((exists dst_positive_code_assoc_exists_Lleft dst_positive_scale_assoc_exists_Lleft dst_negative_code_assoc_exists_Lleft dst_negative_scale_assoc_exists_Lleft. (((A) = (((((dst_positive_code_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft)) * S ((dst_positive_code_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft)) + ((dst_positive_scale_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft))) + (((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) * S ((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) + ((dst_negative_scale_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)))) * S ((((dst_positive_code_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft)) * S ((dst_positive_code_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft)) + ((dst_positive_scale_assoc_exists_Lleft) + (dst_positive_scale_assoc_exists_Lleft))) + (((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) * S ((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) + ((dst_negative_scale_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)))) + ((((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) * S ((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) + ((dst_negative_scale_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft))) + (((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) * S ((dst_negative_code_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)) + ((dst_negative_scale_assoc_exists_Lleft) + (dst_negative_scale_assoc_exists_Lleft)))))) /\ (forall dst_index_assoc_exists_Lleft. (exists pvs_le_gap_assoc_exists_Lleftdomain. pvs_le_gap_assoc_exists_Lleftdomain + (dst_index_assoc_exists_Lleft) = (N)) -> exists dst_positive_assoc_exists_Lleft dst_negative_assoc_exists_Lleft dst_value_assoc_exists_Lleft. ((((exists ff_h_pvs_assoc_exists_Lleftentrypositive. ff_h_pvs_assoc_exists_Lleftentrypositive + S (dst_positive_assoc_exists_Lleft) = S ((S (dst_index_assoc_exists_Lleft)) * dst_positive_scale_assoc_exists_Lleft)) /\ exists ff_q_pvs_assoc_exists_Lleftentrypositive. dst_positive_code_assoc_exists_Lleft = ff_q_pvs_assoc_exists_Lleftentrypositive * S ((S (dst_index_assoc_exists_Lleft)) * dst_positive_scale_assoc_exists_Lleft) + (dst_positive_assoc_exists_Lleft))) /\ (((((exists ff_h_pvs_assoc_exists_Lleftentrynegative. ff_h_pvs_assoc_exists_Lleftentrynegative + S (dst_negative_assoc_exists_Lleft) = S ((S (dst_index_assoc_exists_Lleft)) * dst_negative_scale_assoc_exists_Lleft)) /\ exists ff_q_pvs_assoc_exists_Lleftentrynegative. dst_negative_code_assoc_exists_Lleft = ff_q_pvs_assoc_exists_Lleftentrynegative * S ((S (dst_index_assoc_exists_Lleft)) * dst_negative_scale_assoc_exists_Lleft) + (dst_negative_assoc_exists_Lleft))) /\ (exists ge_balance_positive_assoc_exists_Lleftentryvalue ge_balance_negative_assoc_exists_Lleftentryvalue. (((((dst_value_assoc_exists_Lleft) = 2 * (ge_balance_positive_assoc_exists_Lleftentryvalue) /\ (ge_balance_negative_assoc_exists_Lleftentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lleftentryvaluedecode. (((dst_value_assoc_exists_Lleft) = 2 * ge_signed_half_assoc_exists_Lleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lleftentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lleftentryvalue) = S ge_signed_half_assoc_exists_Lleftentryvaluedecode))) /\ ((dst_positive_assoc_exists_Lleft) + ge_balance_negative_assoc_exists_Lleftentryvalue = (dst_negative_assoc_exists_Lleft) + ge_balance_positive_assoc_exists_Lleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Lright dst_positive_scale_assoc_exists_Lright dst_negative_code_assoc_exists_Lright dst_negative_scale_assoc_exists_Lright. (((H) = (((((dst_positive_code_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright)) * S ((dst_positive_code_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright)) + ((dst_positive_scale_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright))) + (((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) * S ((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) + ((dst_negative_scale_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)))) * S ((((dst_positive_code_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright)) * S ((dst_positive_code_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright)) + ((dst_positive_scale_assoc_exists_Lright) + (dst_positive_scale_assoc_exists_Lright))) + (((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) * S ((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) + ((dst_negative_scale_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)))) + ((((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) * S ((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) + ((dst_negative_scale_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright))) + (((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) * S ((dst_negative_code_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)) + ((dst_negative_scale_assoc_exists_Lright) + (dst_negative_scale_assoc_exists_Lright)))))) /\ (forall dst_index_assoc_exists_Lright. (exists pvs_le_gap_assoc_exists_Lrightdomain. pvs_le_gap_assoc_exists_Lrightdomain + (dst_index_assoc_exists_Lright) = (N)) -> exists dst_positive_assoc_exists_Lright dst_negative_assoc_exists_Lright dst_value_assoc_exists_Lright. ((((exists ff_h_pvs_assoc_exists_Lrightentrypositive. ff_h_pvs_assoc_exists_Lrightentrypositive + S (dst_positive_assoc_exists_Lright) = S ((S (dst_index_assoc_exists_Lright)) * dst_positive_scale_assoc_exists_Lright)) /\ exists ff_q_pvs_assoc_exists_Lrightentrypositive. dst_positive_code_assoc_exists_Lright = ff_q_pvs_assoc_exists_Lrightentrypositive * S ((S (dst_index_assoc_exists_Lright)) * dst_positive_scale_assoc_exists_Lright) + (dst_positive_assoc_exists_Lright))) /\ (((((exists ff_h_pvs_assoc_exists_Lrightentrynegative. ff_h_pvs_assoc_exists_Lrightentrynegative + S (dst_negative_assoc_exists_Lright) = S ((S (dst_index_assoc_exists_Lright)) * dst_negative_scale_assoc_exists_Lright)) /\ exists ff_q_pvs_assoc_exists_Lrightentrynegative. dst_negative_code_assoc_exists_Lright = ff_q_pvs_assoc_exists_Lrightentrynegative * S ((S (dst_index_assoc_exists_Lright)) * dst_negative_scale_assoc_exists_Lright) + (dst_negative_assoc_exists_Lright))) /\ (exists ge_balance_positive_assoc_exists_Lrightentryvalue ge_balance_negative_assoc_exists_Lrightentryvalue. (((((dst_value_assoc_exists_Lright) = 2 * (ge_balance_positive_assoc_exists_Lrightentryvalue) /\ (ge_balance_negative_assoc_exists_Lrightentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lrightentryvaluedecode. (((dst_value_assoc_exists_Lright) = 2 * ge_signed_half_assoc_exists_Lrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lrightentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lrightentryvalue) = S ge_signed_half_assoc_exists_Lrightentryvaluedecode))) /\ ((dst_positive_assoc_exists_Lright) + ge_balance_negative_assoc_exists_Lrightentryvalue = (dst_negative_assoc_exists_Lright) + ge_balance_positive_assoc_exists_Lrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Ltable dst_positive_scale_assoc_exists_Ltable dst_negative_code_assoc_exists_Ltable dst_negative_scale_assoc_exists_Ltable. (((L) = (((((dst_positive_code_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable)) * S ((dst_positive_code_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable)) + ((dst_positive_scale_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable))) + (((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) * S ((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) + ((dst_negative_scale_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)))) * S ((((dst_positive_code_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable)) * S ((dst_positive_code_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable)) + ((dst_positive_scale_assoc_exists_Ltable) + (dst_positive_scale_assoc_exists_Ltable))) + (((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) * S ((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) + ((dst_negative_scale_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)))) + ((((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) * S ((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) + ((dst_negative_scale_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable))) + (((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) * S ((dst_negative_code_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)) + ((dst_negative_scale_assoc_exists_Ltable) + (dst_negative_scale_assoc_exists_Ltable)))))) /\ (forall dst_index_assoc_exists_Ltable. (exists pvs_le_gap_assoc_exists_Ltabledomain. pvs_le_gap_assoc_exists_Ltabledomain + (dst_index_assoc_exists_Ltable) = (N)) -> exists dst_positive_assoc_exists_Ltable dst_negative_assoc_exists_Ltable dst_value_assoc_exists_Ltable. ((((exists ff_h_pvs_assoc_exists_Ltableentrypositive. ff_h_pvs_assoc_exists_Ltableentrypositive + S (dst_positive_assoc_exists_Ltable) = S ((S (dst_index_assoc_exists_Ltable)) * dst_positive_scale_assoc_exists_Ltable)) /\ exists ff_q_pvs_assoc_exists_Ltableentrypositive. dst_positive_code_assoc_exists_Ltable = ff_q_pvs_assoc_exists_Ltableentrypositive * S ((S (dst_index_assoc_exists_Ltable)) * dst_positive_scale_assoc_exists_Ltable) + (dst_positive_assoc_exists_Ltable))) /\ (((((exists ff_h_pvs_assoc_exists_Ltableentrynegative. ff_h_pvs_assoc_exists_Ltableentrynegative + S (dst_negative_assoc_exists_Ltable) = S ((S (dst_index_assoc_exists_Ltable)) * dst_negative_scale_assoc_exists_Ltable)) /\ exists ff_q_pvs_assoc_exists_Ltableentrynegative. dst_negative_code_assoc_exists_Ltable = ff_q_pvs_assoc_exists_Ltableentrynegative * S ((S (dst_index_assoc_exists_Ltable)) * dst_negative_scale_assoc_exists_Ltable) + (dst_negative_assoc_exists_Ltable))) /\ (exists ge_balance_positive_assoc_exists_Ltableentryvalue ge_balance_negative_assoc_exists_Ltableentryvalue. (((((dst_value_assoc_exists_Ltable) = 2 * (ge_balance_positive_assoc_exists_Ltableentryvalue) /\ (ge_balance_negative_assoc_exists_Ltableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Ltableentryvaluedecode. (((dst_value_assoc_exists_Ltable) = 2 * ge_signed_half_assoc_exists_Ltableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Ltableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Ltableentryvalue) = S ge_signed_half_assoc_exists_Ltableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Ltable) + ge_balance_negative_assoc_exists_Ltableentryvalue = (dst_negative_assoc_exists_Ltable) + ge_balance_positive_assoc_exists_Ltableentryvalue))))))))) /\ (forall dc_input_assoc_exists_L dc_output_assoc_exists_L. ~(dc_input_assoc_exists_L=0) -> (exists pvs_le_gap_assoc_exists_Ldomain. pvs_le_gap_assoc_exists_Ldomain + (dc_input_assoc_exists_L) = (N)) -> (exists dst_positive_code_assoc_exists_Llookup dst_positive_scale_assoc_exists_Llookup dst_negative_code_assoc_exists_Llookup dst_negative_scale_assoc_exists_Llookup dst_positive_assoc_exists_Llookup dst_negative_assoc_exists_Llookup. (((L) = (((((dst_positive_code_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup)) * S ((dst_positive_code_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup)) + ((dst_positive_scale_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup))) + (((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) * S ((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) + ((dst_negative_scale_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)))) * S ((((dst_positive_code_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup)) * S ((dst_positive_code_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup)) + ((dst_positive_scale_assoc_exists_Llookup) + (dst_positive_scale_assoc_exists_Llookup))) + (((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) * S ((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) + ((dst_negative_scale_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)))) + ((((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) * S ((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) + ((dst_negative_scale_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup))) + (((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) * S ((dst_negative_code_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)) + ((dst_negative_scale_assoc_exists_Llookup) + (dst_negative_scale_assoc_exists_Llookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Llookuppositive. ff_h_pvs_assoc_exists_Llookuppositive + S (dst_positive_assoc_exists_Llookup) = S ((S (dc_input_assoc_exists_L)) * dst_positive_scale_assoc_exists_Llookup)) /\ exists ff_q_pvs_assoc_exists_Llookuppositive. dst_positive_code_assoc_exists_Llookup = ff_q_pvs_assoc_exists_Llookuppositive * S ((S (dc_input_assoc_exists_L)) * dst_positive_scale_assoc_exists_Llookup) + (dst_positive_assoc_exists_Llookup))) /\ (((((exists ff_h_pvs_assoc_exists_Llookupnegative. ff_h_pvs_assoc_exists_Llookupnegative + S (dst_negative_assoc_exists_Llookup) = S ((S (dc_input_assoc_exists_L)) * dst_negative_scale_assoc_exists_Llookup)) /\ exists ff_q_pvs_assoc_exists_Llookupnegative. dst_negative_code_assoc_exists_Llookup = ff_q_pvs_assoc_exists_Llookupnegative * S ((S (dc_input_assoc_exists_L)) * dst_negative_scale_assoc_exists_Llookup) + (dst_negative_assoc_exists_Llookup))) /\ (exists ge_balance_positive_assoc_exists_Llookupvalue ge_balance_negative_assoc_exists_Llookupvalue. (((((dc_output_assoc_exists_L) = 2 * (ge_balance_positive_assoc_exists_Llookupvalue) /\ (ge_balance_negative_assoc_exists_Llookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Llookupvaluedecode. (((dc_output_assoc_exists_L) = 2 * ge_signed_half_assoc_exists_Llookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Llookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Llookupvalue) = S ge_signed_half_assoc_exists_Llookupvaluedecode))) /\ ((dst_positive_assoc_exists_Llookup) + ge_balance_negative_assoc_exists_Llookupvalue = (dst_negative_assoc_exists_Llookup) + ge_balance_positive_assoc_exists_Llookupvalue))))))))) -> (((~((dc_input_assoc_exists_L)=0)) /\ (exists dc_mask_assoc_exists_Lvalue. ((((exists dst_positive_code_assoc_exists_Lvaluemasktable dst_positive_scale_assoc_exists_Lvaluemasktable dst_negative_code_assoc_exists_Lvaluemasktable dst_negative_scale_assoc_exists_Lvaluemasktable. (((dc_mask_assoc_exists_Lvalue) = (((((dst_positive_code_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable)) * S ((dst_positive_code_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable)) + ((dst_positive_scale_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable))) + (((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) * S ((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) + ((dst_negative_scale_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)))) * S ((((dst_positive_code_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable)) * S ((dst_positive_code_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable)) + ((dst_positive_scale_assoc_exists_Lvaluemasktable) + (dst_positive_scale_assoc_exists_Lvaluemasktable))) + (((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) * S ((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) + ((dst_negative_scale_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)))) + ((((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) * S ((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) + ((dst_negative_scale_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable))) + (((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) * S ((dst_negative_code_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)) + ((dst_negative_scale_assoc_exists_Lvaluemasktable) + (dst_negative_scale_assoc_exists_Lvaluemasktable)))))) /\ (forall dst_index_assoc_exists_Lvaluemasktable. (exists pvs_le_gap_assoc_exists_Lvaluemasktabledomain. pvs_le_gap_assoc_exists_Lvaluemasktabledomain + (dst_index_assoc_exists_Lvaluemasktable) = (dc_input_assoc_exists_L)) -> exists dst_positive_assoc_exists_Lvaluemasktable dst_negative_assoc_exists_Lvaluemasktable dst_value_assoc_exists_Lvaluemasktable. ((((exists ff_h_pvs_assoc_exists_Lvaluemasktableentrypositive. ff_h_pvs_assoc_exists_Lvaluemasktableentrypositive + S (dst_positive_assoc_exists_Lvaluemasktable) = S ((S (dst_index_assoc_exists_Lvaluemasktable)) * dst_positive_scale_assoc_exists_Lvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Lvaluemasktableentrypositive. dst_positive_code_assoc_exists_Lvaluemasktable = ff_q_pvs_assoc_exists_Lvaluemasktableentrypositive * S ((S (dst_index_assoc_exists_Lvaluemasktable)) * dst_positive_scale_assoc_exists_Lvaluemasktable) + (dst_positive_assoc_exists_Lvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemasktableentrynegative. ff_h_pvs_assoc_exists_Lvaluemasktableentrynegative + S (dst_negative_assoc_exists_Lvaluemasktable) = S ((S (dst_index_assoc_exists_Lvaluemasktable)) * dst_negative_scale_assoc_exists_Lvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Lvaluemasktableentrynegative. dst_negative_code_assoc_exists_Lvaluemasktable = ff_q_pvs_assoc_exists_Lvaluemasktableentrynegative * S ((S (dst_index_assoc_exists_Lvaluemasktable)) * dst_negative_scale_assoc_exists_Lvaluemasktable) + (dst_negative_assoc_exists_Lvaluemasktable))) /\ (exists ge_balance_positive_assoc_exists_Lvaluemasktableentryvalue ge_balance_negative_assoc_exists_Lvaluemasktableentryvalue. (((((dst_value_assoc_exists_Lvaluemasktable) = 2 * (ge_balance_positive_assoc_exists_Lvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_exists_Lvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemasktableentryvaluedecode. (((dst_value_assoc_exists_Lvaluemasktable) = 2 * ge_signed_half_assoc_exists_Lvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lvaluemasktableentryvalue) = S ge_signed_half_assoc_exists_Lvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Lvaluemasktable) + ge_balance_negative_assoc_exists_Lvaluemasktableentryvalue = (dst_negative_assoc_exists_Lvaluemasktable) + ge_balance_positive_assoc_exists_Lvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_exists_Lvaluemask dc_value_assoc_exists_Lvaluemask. (exists pvs_le_gap_assoc_exists_Lvaluemaskdomain. pvs_le_gap_assoc_exists_Lvaluemaskdomain + (dc_index_assoc_exists_Lvaluemask) = (dc_input_assoc_exists_L)) -> (exists dst_positive_code_assoc_exists_Lvaluemasklookup dst_positive_scale_assoc_exists_Lvaluemasklookup dst_negative_code_assoc_exists_Lvaluemasklookup dst_negative_scale_assoc_exists_Lvaluemasklookup dst_positive_assoc_exists_Lvaluemasklookup dst_negative_assoc_exists_Lvaluemasklookup. (((dc_mask_assoc_exists_Lvalue) = (((((dst_positive_code_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup))) + (((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)))) * S ((((dst_positive_code_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Lvaluemasklookup) + (dst_positive_scale_assoc_exists_Lvaluemasklookup))) + (((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)))) + ((((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup))) + (((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Lvaluemasklookup) + (dst_negative_scale_assoc_exists_Lvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemasklookuppositive. ff_h_pvs_assoc_exists_Lvaluemasklookuppositive + S (dst_positive_assoc_exists_Lvaluemasklookup) = S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_positive_scale_assoc_exists_Lvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Lvaluemasklookuppositive. dst_positive_code_assoc_exists_Lvaluemasklookup = ff_q_pvs_assoc_exists_Lvaluemasklookuppositive * S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_positive_scale_assoc_exists_Lvaluemasklookup) + (dst_positive_assoc_exists_Lvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemasklookupnegative. ff_h_pvs_assoc_exists_Lvaluemasklookupnegative + S (dst_negative_assoc_exists_Lvaluemasklookup) = S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_negative_scale_assoc_exists_Lvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Lvaluemasklookupnegative. dst_negative_code_assoc_exists_Lvaluemasklookup = ff_q_pvs_assoc_exists_Lvaluemasklookupnegative * S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_negative_scale_assoc_exists_Lvaluemasklookup) + (dst_negative_assoc_exists_Lvaluemasklookup))) /\ (exists ge_balance_positive_assoc_exists_Lvaluemasklookupvalue ge_balance_negative_assoc_exists_Lvaluemasklookupvalue. (((((dc_value_assoc_exists_Lvaluemask) = 2 * (ge_balance_positive_assoc_exists_Lvaluemasklookupvalue) /\ (ge_balance_negative_assoc_exists_Lvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemasklookupvaluedecode. (((dc_value_assoc_exists_Lvaluemask) = 2 * ge_signed_half_assoc_exists_Lvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lvaluemasklookupvalue) = S ge_signed_half_assoc_exists_Lvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_exists_Lvaluemasklookup) + ge_balance_negative_assoc_exists_Lvaluemasklookupvalue = (dst_negative_assoc_exists_Lvaluemasklookup) + ge_balance_positive_assoc_exists_Lvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_exists_Lvaluemask)=0)) /\ (exists dc_quotient_assoc_exists_Lvaluemaskentry dc_left_assoc_exists_Lvaluemaskentry dc_right_assoc_exists_Lvaluemaskentry. (((dc_input_assoc_exists_L)=(dc_index_assoc_exists_Lvaluemask)*dc_quotient_assoc_exists_Lvaluemaskentry) /\ (((exists dst_positive_code_assoc_exists_Lvaluemaskentryleft dst_positive_scale_assoc_exists_Lvaluemaskentryleft dst_negative_code_assoc_exists_Lvaluemaskentryleft dst_negative_scale_assoc_exists_Lvaluemaskentryleft dst_positive_assoc_exists_Lvaluemaskentryleft dst_negative_assoc_exists_Lvaluemaskentryleft. (((A) = (((((dst_positive_code_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Lvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)))) + ((((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Lvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemaskentryleftpositive. ff_h_pvs_assoc_exists_Lvaluemaskentryleftpositive + S (dst_positive_assoc_exists_Lvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_positive_scale_assoc_exists_Lvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Lvaluemaskentryleftpositive. dst_positive_code_assoc_exists_Lvaluemaskentryleft = ff_q_pvs_assoc_exists_Lvaluemaskentryleftpositive * S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_positive_scale_assoc_exists_Lvaluemaskentryleft) + (dst_positive_assoc_exists_Lvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemaskentryleftnegative. ff_h_pvs_assoc_exists_Lvaluemaskentryleftnegative + S (dst_negative_assoc_exists_Lvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_negative_scale_assoc_exists_Lvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Lvaluemaskentryleftnegative. dst_negative_code_assoc_exists_Lvaluemaskentryleft = ff_q_pvs_assoc_exists_Lvaluemaskentryleftnegative * S ((S (dc_index_assoc_exists_Lvaluemask)) * dst_negative_scale_assoc_exists_Lvaluemaskentryleft) + (dst_negative_assoc_exists_Lvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_exists_Lvaluemaskentryleftvalue ge_balance_negative_assoc_exists_Lvaluemaskentryleftvalue. (((((dc_left_assoc_exists_Lvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Lvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_exists_Lvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemaskentryleftvaluedecode. (((dc_left_assoc_exists_Lvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Lvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lvaluemaskentryleftvalue) = S ge_signed_half_assoc_exists_Lvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_exists_Lvaluemaskentryleft) + ge_balance_negative_assoc_exists_Lvaluemaskentryleftvalue = (dst_negative_assoc_exists_Lvaluemaskentryleft) + ge_balance_positive_assoc_exists_Lvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Lvaluemaskentryright dst_positive_scale_assoc_exists_Lvaluemaskentryright dst_negative_code_assoc_exists_Lvaluemaskentryright dst_negative_scale_assoc_exists_Lvaluemaskentryright dst_positive_assoc_exists_Lvaluemaskentryright dst_negative_assoc_exists_Lvaluemaskentryright. (((H) = (((((dst_positive_code_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)))) * S ((((dst_positive_code_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Lvaluemaskentryright) + (dst_positive_scale_assoc_exists_Lvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)))) + ((((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Lvaluemaskentryright) + (dst_negative_scale_assoc_exists_Lvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemaskentryrightpositive. ff_h_pvs_assoc_exists_Lvaluemaskentryrightpositive + S (dst_positive_assoc_exists_Lvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Lvaluemaskentry)) * dst_positive_scale_assoc_exists_Lvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Lvaluemaskentryrightpositive. dst_positive_code_assoc_exists_Lvaluemaskentryright = ff_q_pvs_assoc_exists_Lvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_exists_Lvaluemaskentry)) * dst_positive_scale_assoc_exists_Lvaluemaskentryright) + (dst_positive_assoc_exists_Lvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_exists_Lvaluemaskentryrightnegative. ff_h_pvs_assoc_exists_Lvaluemaskentryrightnegative + S (dst_negative_assoc_exists_Lvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Lvaluemaskentry)) * dst_negative_scale_assoc_exists_Lvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Lvaluemaskentryrightnegative. dst_negative_code_assoc_exists_Lvaluemaskentryright = ff_q_pvs_assoc_exists_Lvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_exists_Lvaluemaskentry)) * dst_negative_scale_assoc_exists_Lvaluemaskentryright) + (dst_negative_assoc_exists_Lvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_exists_Lvaluemaskentryrightvalue ge_balance_negative_assoc_exists_Lvaluemaskentryrightvalue. (((((dc_right_assoc_exists_Lvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Lvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_exists_Lvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemaskentryrightvaluedecode. (((dc_right_assoc_exists_Lvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Lvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Lvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_exists_Lvaluemaskentryrightvalue) = S ge_signed_half_assoc_exists_Lvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_exists_Lvaluemaskentryright) + ge_balance_negative_assoc_exists_Lvaluemaskentryrightvalue = (dst_negative_assoc_exists_Lvaluemaskentryright) + ge_balance_positive_assoc_exists_Lvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_exists_Lvaluemaskentryproduct sto_an_assoc_exists_Lvaluemaskentryproduct sto_bp_assoc_exists_Lvaluemaskentryproduct sto_bn_assoc_exists_Lvaluemaskentryproduct sto_cp_assoc_exists_Lvaluemaskentryproduct sto_cn_assoc_exists_Lvaluemaskentryproduct. (((((dc_left_assoc_exists_Lvaluemaskentry) = 2 * (sto_ap_assoc_exists_Lvaluemaskentryproduct) /\ (sto_an_assoc_exists_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemaskentryproductleft. (((dc_left_assoc_exists_Lvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Lvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_exists_Lvaluemaskentryproduct) = 0) /\ (sto_an_assoc_exists_Lvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Lvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_exists_Lvaluemaskentry) = 2 * (sto_bp_assoc_exists_Lvaluemaskentryproduct) /\ (sto_bn_assoc_exists_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemaskentryproductright. (((dc_right_assoc_exists_Lvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Lvaluemaskentryproductright + 1 /\ (sto_bp_assoc_exists_Lvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_exists_Lvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Lvaluemaskentryproductright))) /\ ((((((dc_value_assoc_exists_Lvaluemask) = 2 * (sto_cp_assoc_exists_Lvaluemaskentryproduct) /\ (sto_cn_assoc_exists_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluemaskentryproductoutput. (((dc_value_assoc_exists_Lvaluemask) = 2 * ge_signed_half_assoc_exists_Lvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_exists_Lvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_exists_Lvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Lvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_exists_Lvaluemaskentryproduct * sto_bp_assoc_exists_Lvaluemaskentryproduct + sto_an_assoc_exists_Lvaluemaskentryproduct * sto_bn_assoc_exists_Lvaluemaskentryproduct) + sto_cn_assoc_exists_Lvaluemaskentryproduct = (sto_ap_assoc_exists_Lvaluemaskentryproduct * sto_bn_assoc_exists_Lvaluemaskentryproduct + sto_an_assoc_exists_Lvaluemaskentryproduct * sto_bp_assoc_exists_Lvaluemaskentryproduct) + sto_cp_assoc_exists_Lvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_exists_Lvaluemask)=0 \/ ~(exists pvs_factor_assoc_exists_Lvaluemaskentrynondivisor. (dc_input_assoc_exists_L) = (dc_index_assoc_exists_Lvaluemask) * pvs_factor_assoc_exists_Lvaluemaskentrynondivisor)) /\ ((dc_value_assoc_exists_Lvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_exists_Lvaluefold dst_positive_scale_assoc_exists_Lvaluefold dst_negative_code_assoc_exists_Lvaluefold dst_negative_scale_assoc_exists_Lvaluefold dst_positive_sum_assoc_exists_Lvaluefold dst_negative_sum_assoc_exists_Lvaluefold. (((dc_mask_assoc_exists_Lvalue) = (((((dst_positive_code_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold)) * S ((dst_positive_code_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold)) + ((dst_positive_scale_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold))) + (((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) * S ((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) + ((dst_negative_scale_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)))) * S ((((dst_positive_code_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold)) * S ((dst_positive_code_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold)) + ((dst_positive_scale_assoc_exists_Lvaluefold) + (dst_positive_scale_assoc_exists_Lvaluefold))) + (((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) * S ((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) + ((dst_negative_scale_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)))) + ((((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) * S ((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) + ((dst_negative_scale_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold))) + (((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) * S ((dst_negative_code_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)) + ((dst_negative_scale_assoc_exists_Lvaluefold) + (dst_negative_scale_assoc_exists_Lvaluefold)))))) /\ (((exists fs_u_dst_assoc_exists_Lvaluefoldpositive fs_v_dst_assoc_exists_Lvaluefoldpositive. ((((exists fs_h_dst_assoc_exists_Lvaluefoldpositive_body_start. fs_h_dst_assoc_exists_Lvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldpositive_body_start. fs_u_dst_assoc_exists_Lvaluefoldpositive = fs_q_dst_assoc_exists_Lvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Lvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldpositive_body_terminal. fs_h_dst_assoc_exists_Lvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_exists_Lvaluefold) = S ((S (S (dc_input_assoc_exists_L))) * fs_v_dst_assoc_exists_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldpositive_body_terminal. fs_u_dst_assoc_exists_Lvaluefoldpositive = fs_q_dst_assoc_exists_Lvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_exists_L))) * fs_v_dst_assoc_exists_Lvaluefoldpositive) + (dst_positive_sum_assoc_exists_Lvaluefold))) /\ forall fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_exists_Lvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_exists_Lvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps = S (dc_input_assoc_exists_L)) -> exists fs_a_dst_assoc_exists_Lvaluefoldpositive_body_steps fs_r_dst_assoc_exists_Lvaluefoldpositive_body_steps fs_s_dst_assoc_exists_Lvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_exists_Lvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Lvaluefold)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_exists_Lvaluefold = fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Lvaluefold) + (fs_a_dst_assoc_exists_Lvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_exists_Lvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_exists_Lvaluefoldpositive = fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldpositive) + (fs_r_dst_assoc_exists_Lvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_exists_Lvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_exists_Lvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_exists_Lvaluefoldpositive = fs_q_dst_assoc_exists_Lvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldpositive) + (fs_s_dst_assoc_exists_Lvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_exists_Lvaluefoldpositive_body_steps = fs_r_dst_assoc_exists_Lvaluefoldpositive_body_steps + fs_a_dst_assoc_exists_Lvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_exists_Lvaluefoldnegative fs_v_dst_assoc_exists_Lvaluefoldnegative. ((((exists fs_h_dst_assoc_exists_Lvaluefoldnegative_body_start. fs_h_dst_assoc_exists_Lvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldnegative_body_start. fs_u_dst_assoc_exists_Lvaluefoldnegative = fs_q_dst_assoc_exists_Lvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Lvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldnegative_body_terminal. fs_h_dst_assoc_exists_Lvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_exists_Lvaluefold) = S ((S (S (dc_input_assoc_exists_L))) * fs_v_dst_assoc_exists_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldnegative_body_terminal. fs_u_dst_assoc_exists_Lvaluefoldnegative = fs_q_dst_assoc_exists_Lvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_exists_L))) * fs_v_dst_assoc_exists_Lvaluefoldnegative) + (dst_negative_sum_assoc_exists_Lvaluefold))) /\ forall fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_exists_Lvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_exists_Lvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps = S (dc_input_assoc_exists_L)) -> exists fs_a_dst_assoc_exists_Lvaluefoldnegative_body_steps fs_r_dst_assoc_exists_Lvaluefoldnegative_body_steps fs_s_dst_assoc_exists_Lvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_exists_Lvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Lvaluefold)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_exists_Lvaluefold = fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Lvaluefold) + (fs_a_dst_assoc_exists_Lvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_exists_Lvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_exists_Lvaluefoldnegative = fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldnegative) + (fs_r_dst_assoc_exists_Lvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_exists_Lvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_exists_Lvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_exists_Lvaluefoldnegative = fs_q_dst_assoc_exists_Lvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Lvaluefoldnegative) + (fs_s_dst_assoc_exists_Lvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_exists_Lvaluefoldnegative_body_steps = fs_r_dst_assoc_exists_Lvaluefoldnegative_body_steps + fs_a_dst_assoc_exists_Lvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_exists_Lvaluefoldresult ge_balance_negative_assoc_exists_Lvaluefoldresult. (((((dc_output_assoc_exists_L) = 2 * (ge_balance_positive_assoc_exists_Lvaluefoldresult) /\ (ge_balance_negative_assoc_exists_Lvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_exists_Lvaluefoldresultdecode. (((dc_output_assoc_exists_L) = 2 * ge_signed_half_assoc_exists_Lvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_exists_Lvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_exists_Lvaluefoldresult) = S ge_signed_half_assoc_exists_Lvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_exists_Lvaluefold) + ge_balance_negative_assoc_exists_Lvaluefoldresult = (dst_negative_sum_assoc_exists_Lvaluefold) + ge_balance_positive_assoc_exists_Lvaluefoldresult)))))))))))))))))))) /\ (((((exists dst_positive_code_assoc_exists_Rleft dst_positive_scale_assoc_exists_Rleft dst_negative_code_assoc_exists_Rleft dst_negative_scale_assoc_exists_Rleft. (((F) = (((((dst_positive_code_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft)) * S ((dst_positive_code_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft)) + ((dst_positive_scale_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft))) + (((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) * S ((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) + ((dst_negative_scale_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)))) * S ((((dst_positive_code_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft)) * S ((dst_positive_code_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft)) + ((dst_positive_scale_assoc_exists_Rleft) + (dst_positive_scale_assoc_exists_Rleft))) + (((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) * S ((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) + ((dst_negative_scale_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)))) + ((((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) * S ((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) + ((dst_negative_scale_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft))) + (((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) * S ((dst_negative_code_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)) + ((dst_negative_scale_assoc_exists_Rleft) + (dst_negative_scale_assoc_exists_Rleft)))))) /\ (forall dst_index_assoc_exists_Rleft. (exists pvs_le_gap_assoc_exists_Rleftdomain. pvs_le_gap_assoc_exists_Rleftdomain + (dst_index_assoc_exists_Rleft) = (N)) -> exists dst_positive_assoc_exists_Rleft dst_negative_assoc_exists_Rleft dst_value_assoc_exists_Rleft. ((((exists ff_h_pvs_assoc_exists_Rleftentrypositive. ff_h_pvs_assoc_exists_Rleftentrypositive + S (dst_positive_assoc_exists_Rleft) = S ((S (dst_index_assoc_exists_Rleft)) * dst_positive_scale_assoc_exists_Rleft)) /\ exists ff_q_pvs_assoc_exists_Rleftentrypositive. dst_positive_code_assoc_exists_Rleft = ff_q_pvs_assoc_exists_Rleftentrypositive * S ((S (dst_index_assoc_exists_Rleft)) * dst_positive_scale_assoc_exists_Rleft) + (dst_positive_assoc_exists_Rleft))) /\ (((((exists ff_h_pvs_assoc_exists_Rleftentrynegative. ff_h_pvs_assoc_exists_Rleftentrynegative + S (dst_negative_assoc_exists_Rleft) = S ((S (dst_index_assoc_exists_Rleft)) * dst_negative_scale_assoc_exists_Rleft)) /\ exists ff_q_pvs_assoc_exists_Rleftentrynegative. dst_negative_code_assoc_exists_Rleft = ff_q_pvs_assoc_exists_Rleftentrynegative * S ((S (dst_index_assoc_exists_Rleft)) * dst_negative_scale_assoc_exists_Rleft) + (dst_negative_assoc_exists_Rleft))) /\ (exists ge_balance_positive_assoc_exists_Rleftentryvalue ge_balance_negative_assoc_exists_Rleftentryvalue. (((((dst_value_assoc_exists_Rleft) = 2 * (ge_balance_positive_assoc_exists_Rleftentryvalue) /\ (ge_balance_negative_assoc_exists_Rleftentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rleftentryvaluedecode. (((dst_value_assoc_exists_Rleft) = 2 * ge_signed_half_assoc_exists_Rleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rleftentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rleftentryvalue) = S ge_signed_half_assoc_exists_Rleftentryvaluedecode))) /\ ((dst_positive_assoc_exists_Rleft) + ge_balance_negative_assoc_exists_Rleftentryvalue = (dst_negative_assoc_exists_Rleft) + ge_balance_positive_assoc_exists_Rleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Rright dst_positive_scale_assoc_exists_Rright dst_negative_code_assoc_exists_Rright dst_negative_scale_assoc_exists_Rright. (((B) = (((((dst_positive_code_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright)) * S ((dst_positive_code_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright)) + ((dst_positive_scale_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright))) + (((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) * S ((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) + ((dst_negative_scale_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)))) * S ((((dst_positive_code_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright)) * S ((dst_positive_code_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright)) + ((dst_positive_scale_assoc_exists_Rright) + (dst_positive_scale_assoc_exists_Rright))) + (((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) * S ((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) + ((dst_negative_scale_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)))) + ((((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) * S ((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) + ((dst_negative_scale_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright))) + (((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) * S ((dst_negative_code_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)) + ((dst_negative_scale_assoc_exists_Rright) + (dst_negative_scale_assoc_exists_Rright)))))) /\ (forall dst_index_assoc_exists_Rright. (exists pvs_le_gap_assoc_exists_Rrightdomain. pvs_le_gap_assoc_exists_Rrightdomain + (dst_index_assoc_exists_Rright) = (N)) -> exists dst_positive_assoc_exists_Rright dst_negative_assoc_exists_Rright dst_value_assoc_exists_Rright. ((((exists ff_h_pvs_assoc_exists_Rrightentrypositive. ff_h_pvs_assoc_exists_Rrightentrypositive + S (dst_positive_assoc_exists_Rright) = S ((S (dst_index_assoc_exists_Rright)) * dst_positive_scale_assoc_exists_Rright)) /\ exists ff_q_pvs_assoc_exists_Rrightentrypositive. dst_positive_code_assoc_exists_Rright = ff_q_pvs_assoc_exists_Rrightentrypositive * S ((S (dst_index_assoc_exists_Rright)) * dst_positive_scale_assoc_exists_Rright) + (dst_positive_assoc_exists_Rright))) /\ (((((exists ff_h_pvs_assoc_exists_Rrightentrynegative. ff_h_pvs_assoc_exists_Rrightentrynegative + S (dst_negative_assoc_exists_Rright) = S ((S (dst_index_assoc_exists_Rright)) * dst_negative_scale_assoc_exists_Rright)) /\ exists ff_q_pvs_assoc_exists_Rrightentrynegative. dst_negative_code_assoc_exists_Rright = ff_q_pvs_assoc_exists_Rrightentrynegative * S ((S (dst_index_assoc_exists_Rright)) * dst_negative_scale_assoc_exists_Rright) + (dst_negative_assoc_exists_Rright))) /\ (exists ge_balance_positive_assoc_exists_Rrightentryvalue ge_balance_negative_assoc_exists_Rrightentryvalue. (((((dst_value_assoc_exists_Rright) = 2 * (ge_balance_positive_assoc_exists_Rrightentryvalue) /\ (ge_balance_negative_assoc_exists_Rrightentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rrightentryvaluedecode. (((dst_value_assoc_exists_Rright) = 2 * ge_signed_half_assoc_exists_Rrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rrightentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rrightentryvalue) = S ge_signed_half_assoc_exists_Rrightentryvaluedecode))) /\ ((dst_positive_assoc_exists_Rright) + ge_balance_negative_assoc_exists_Rrightentryvalue = (dst_negative_assoc_exists_Rright) + ge_balance_positive_assoc_exists_Rrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Rtable dst_positive_scale_assoc_exists_Rtable dst_negative_code_assoc_exists_Rtable dst_negative_scale_assoc_exists_Rtable. (((R) = (((((dst_positive_code_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable)) * S ((dst_positive_code_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable)) + ((dst_positive_scale_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable))) + (((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) * S ((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) + ((dst_negative_scale_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)))) * S ((((dst_positive_code_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable)) * S ((dst_positive_code_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable)) + ((dst_positive_scale_assoc_exists_Rtable) + (dst_positive_scale_assoc_exists_Rtable))) + (((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) * S ((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) + ((dst_negative_scale_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)))) + ((((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) * S ((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) + ((dst_negative_scale_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable))) + (((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) * S ((dst_negative_code_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)) + ((dst_negative_scale_assoc_exists_Rtable) + (dst_negative_scale_assoc_exists_Rtable)))))) /\ (forall dst_index_assoc_exists_Rtable. (exists pvs_le_gap_assoc_exists_Rtabledomain. pvs_le_gap_assoc_exists_Rtabledomain + (dst_index_assoc_exists_Rtable) = (N)) -> exists dst_positive_assoc_exists_Rtable dst_negative_assoc_exists_Rtable dst_value_assoc_exists_Rtable. ((((exists ff_h_pvs_assoc_exists_Rtableentrypositive. ff_h_pvs_assoc_exists_Rtableentrypositive + S (dst_positive_assoc_exists_Rtable) = S ((S (dst_index_assoc_exists_Rtable)) * dst_positive_scale_assoc_exists_Rtable)) /\ exists ff_q_pvs_assoc_exists_Rtableentrypositive. dst_positive_code_assoc_exists_Rtable = ff_q_pvs_assoc_exists_Rtableentrypositive * S ((S (dst_index_assoc_exists_Rtable)) * dst_positive_scale_assoc_exists_Rtable) + (dst_positive_assoc_exists_Rtable))) /\ (((((exists ff_h_pvs_assoc_exists_Rtableentrynegative. ff_h_pvs_assoc_exists_Rtableentrynegative + S (dst_negative_assoc_exists_Rtable) = S ((S (dst_index_assoc_exists_Rtable)) * dst_negative_scale_assoc_exists_Rtable)) /\ exists ff_q_pvs_assoc_exists_Rtableentrynegative. dst_negative_code_assoc_exists_Rtable = ff_q_pvs_assoc_exists_Rtableentrynegative * S ((S (dst_index_assoc_exists_Rtable)) * dst_negative_scale_assoc_exists_Rtable) + (dst_negative_assoc_exists_Rtable))) /\ (exists ge_balance_positive_assoc_exists_Rtableentryvalue ge_balance_negative_assoc_exists_Rtableentryvalue. (((((dst_value_assoc_exists_Rtable) = 2 * (ge_balance_positive_assoc_exists_Rtableentryvalue) /\ (ge_balance_negative_assoc_exists_Rtableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rtableentryvaluedecode. (((dst_value_assoc_exists_Rtable) = 2 * ge_signed_half_assoc_exists_Rtableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rtableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rtableentryvalue) = S ge_signed_half_assoc_exists_Rtableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Rtable) + ge_balance_negative_assoc_exists_Rtableentryvalue = (dst_negative_assoc_exists_Rtable) + ge_balance_positive_assoc_exists_Rtableentryvalue))))))))) /\ (forall dc_input_assoc_exists_R dc_output_assoc_exists_R. ~(dc_input_assoc_exists_R=0) -> (exists pvs_le_gap_assoc_exists_Rdomain. pvs_le_gap_assoc_exists_Rdomain + (dc_input_assoc_exists_R) = (N)) -> (exists dst_positive_code_assoc_exists_Rlookup dst_positive_scale_assoc_exists_Rlookup dst_negative_code_assoc_exists_Rlookup dst_negative_scale_assoc_exists_Rlookup dst_positive_assoc_exists_Rlookup dst_negative_assoc_exists_Rlookup. (((R) = (((((dst_positive_code_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup)) * S ((dst_positive_code_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup)) + ((dst_positive_scale_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup))) + (((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) * S ((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) + ((dst_negative_scale_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)))) * S ((((dst_positive_code_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup)) * S ((dst_positive_code_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup)) + ((dst_positive_scale_assoc_exists_Rlookup) + (dst_positive_scale_assoc_exists_Rlookup))) + (((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) * S ((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) + ((dst_negative_scale_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)))) + ((((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) * S ((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) + ((dst_negative_scale_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup))) + (((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) * S ((dst_negative_code_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)) + ((dst_negative_scale_assoc_exists_Rlookup) + (dst_negative_scale_assoc_exists_Rlookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Rlookuppositive. ff_h_pvs_assoc_exists_Rlookuppositive + S (dst_positive_assoc_exists_Rlookup) = S ((S (dc_input_assoc_exists_R)) * dst_positive_scale_assoc_exists_Rlookup)) /\ exists ff_q_pvs_assoc_exists_Rlookuppositive. dst_positive_code_assoc_exists_Rlookup = ff_q_pvs_assoc_exists_Rlookuppositive * S ((S (dc_input_assoc_exists_R)) * dst_positive_scale_assoc_exists_Rlookup) + (dst_positive_assoc_exists_Rlookup))) /\ (((((exists ff_h_pvs_assoc_exists_Rlookupnegative. ff_h_pvs_assoc_exists_Rlookupnegative + S (dst_negative_assoc_exists_Rlookup) = S ((S (dc_input_assoc_exists_R)) * dst_negative_scale_assoc_exists_Rlookup)) /\ exists ff_q_pvs_assoc_exists_Rlookupnegative. dst_negative_code_assoc_exists_Rlookup = ff_q_pvs_assoc_exists_Rlookupnegative * S ((S (dc_input_assoc_exists_R)) * dst_negative_scale_assoc_exists_Rlookup) + (dst_negative_assoc_exists_Rlookup))) /\ (exists ge_balance_positive_assoc_exists_Rlookupvalue ge_balance_negative_assoc_exists_Rlookupvalue. (((((dc_output_assoc_exists_R) = 2 * (ge_balance_positive_assoc_exists_Rlookupvalue) /\ (ge_balance_negative_assoc_exists_Rlookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rlookupvaluedecode. (((dc_output_assoc_exists_R) = 2 * ge_signed_half_assoc_exists_Rlookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rlookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rlookupvalue) = S ge_signed_half_assoc_exists_Rlookupvaluedecode))) /\ ((dst_positive_assoc_exists_Rlookup) + ge_balance_negative_assoc_exists_Rlookupvalue = (dst_negative_assoc_exists_Rlookup) + ge_balance_positive_assoc_exists_Rlookupvalue))))))))) -> (((~((dc_input_assoc_exists_R)=0)) /\ (exists dc_mask_assoc_exists_Rvalue. ((((exists dst_positive_code_assoc_exists_Rvaluemasktable dst_positive_scale_assoc_exists_Rvaluemasktable dst_negative_code_assoc_exists_Rvaluemasktable dst_negative_scale_assoc_exists_Rvaluemasktable. (((dc_mask_assoc_exists_Rvalue) = (((((dst_positive_code_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable)) * S ((dst_positive_code_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable)) + ((dst_positive_scale_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable))) + (((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) * S ((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) + ((dst_negative_scale_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)))) * S ((((dst_positive_code_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable)) * S ((dst_positive_code_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable)) + ((dst_positive_scale_assoc_exists_Rvaluemasktable) + (dst_positive_scale_assoc_exists_Rvaluemasktable))) + (((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) * S ((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) + ((dst_negative_scale_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)))) + ((((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) * S ((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) + ((dst_negative_scale_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable))) + (((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) * S ((dst_negative_code_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)) + ((dst_negative_scale_assoc_exists_Rvaluemasktable) + (dst_negative_scale_assoc_exists_Rvaluemasktable)))))) /\ (forall dst_index_assoc_exists_Rvaluemasktable. (exists pvs_le_gap_assoc_exists_Rvaluemasktabledomain. pvs_le_gap_assoc_exists_Rvaluemasktabledomain + (dst_index_assoc_exists_Rvaluemasktable) = (dc_input_assoc_exists_R)) -> exists dst_positive_assoc_exists_Rvaluemasktable dst_negative_assoc_exists_Rvaluemasktable dst_value_assoc_exists_Rvaluemasktable. ((((exists ff_h_pvs_assoc_exists_Rvaluemasktableentrypositive. ff_h_pvs_assoc_exists_Rvaluemasktableentrypositive + S (dst_positive_assoc_exists_Rvaluemasktable) = S ((S (dst_index_assoc_exists_Rvaluemasktable)) * dst_positive_scale_assoc_exists_Rvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Rvaluemasktableentrypositive. dst_positive_code_assoc_exists_Rvaluemasktable = ff_q_pvs_assoc_exists_Rvaluemasktableentrypositive * S ((S (dst_index_assoc_exists_Rvaluemasktable)) * dst_positive_scale_assoc_exists_Rvaluemasktable) + (dst_positive_assoc_exists_Rvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemasktableentrynegative. ff_h_pvs_assoc_exists_Rvaluemasktableentrynegative + S (dst_negative_assoc_exists_Rvaluemasktable) = S ((S (dst_index_assoc_exists_Rvaluemasktable)) * dst_negative_scale_assoc_exists_Rvaluemasktable)) /\ exists ff_q_pvs_assoc_exists_Rvaluemasktableentrynegative. dst_negative_code_assoc_exists_Rvaluemasktable = ff_q_pvs_assoc_exists_Rvaluemasktableentrynegative * S ((S (dst_index_assoc_exists_Rvaluemasktable)) * dst_negative_scale_assoc_exists_Rvaluemasktable) + (dst_negative_assoc_exists_Rvaluemasktable))) /\ (exists ge_balance_positive_assoc_exists_Rvaluemasktableentryvalue ge_balance_negative_assoc_exists_Rvaluemasktableentryvalue. (((((dst_value_assoc_exists_Rvaluemasktable) = 2 * (ge_balance_positive_assoc_exists_Rvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_exists_Rvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemasktableentryvaluedecode. (((dst_value_assoc_exists_Rvaluemasktable) = 2 * ge_signed_half_assoc_exists_Rvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rvaluemasktableentryvalue) = S ge_signed_half_assoc_exists_Rvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_exists_Rvaluemasktable) + ge_balance_negative_assoc_exists_Rvaluemasktableentryvalue = (dst_negative_assoc_exists_Rvaluemasktable) + ge_balance_positive_assoc_exists_Rvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_exists_Rvaluemask dc_value_assoc_exists_Rvaluemask. (exists pvs_le_gap_assoc_exists_Rvaluemaskdomain. pvs_le_gap_assoc_exists_Rvaluemaskdomain + (dc_index_assoc_exists_Rvaluemask) = (dc_input_assoc_exists_R)) -> (exists dst_positive_code_assoc_exists_Rvaluemasklookup dst_positive_scale_assoc_exists_Rvaluemasklookup dst_negative_code_assoc_exists_Rvaluemasklookup dst_negative_scale_assoc_exists_Rvaluemasklookup dst_positive_assoc_exists_Rvaluemasklookup dst_negative_assoc_exists_Rvaluemasklookup. (((dc_mask_assoc_exists_Rvalue) = (((((dst_positive_code_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup))) + (((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)))) * S ((((dst_positive_code_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_positive_code_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup)) + ((dst_positive_scale_assoc_exists_Rvaluemasklookup) + (dst_positive_scale_assoc_exists_Rvaluemasklookup))) + (((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)))) + ((((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup))) + (((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) * S ((dst_negative_code_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)) + ((dst_negative_scale_assoc_exists_Rvaluemasklookup) + (dst_negative_scale_assoc_exists_Rvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemasklookuppositive. ff_h_pvs_assoc_exists_Rvaluemasklookuppositive + S (dst_positive_assoc_exists_Rvaluemasklookup) = S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_positive_scale_assoc_exists_Rvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Rvaluemasklookuppositive. dst_positive_code_assoc_exists_Rvaluemasklookup = ff_q_pvs_assoc_exists_Rvaluemasklookuppositive * S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_positive_scale_assoc_exists_Rvaluemasklookup) + (dst_positive_assoc_exists_Rvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemasklookupnegative. ff_h_pvs_assoc_exists_Rvaluemasklookupnegative + S (dst_negative_assoc_exists_Rvaluemasklookup) = S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_negative_scale_assoc_exists_Rvaluemasklookup)) /\ exists ff_q_pvs_assoc_exists_Rvaluemasklookupnegative. dst_negative_code_assoc_exists_Rvaluemasklookup = ff_q_pvs_assoc_exists_Rvaluemasklookupnegative * S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_negative_scale_assoc_exists_Rvaluemasklookup) + (dst_negative_assoc_exists_Rvaluemasklookup))) /\ (exists ge_balance_positive_assoc_exists_Rvaluemasklookupvalue ge_balance_negative_assoc_exists_Rvaluemasklookupvalue. (((((dc_value_assoc_exists_Rvaluemask) = 2 * (ge_balance_positive_assoc_exists_Rvaluemasklookupvalue) /\ (ge_balance_negative_assoc_exists_Rvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemasklookupvaluedecode. (((dc_value_assoc_exists_Rvaluemask) = 2 * ge_signed_half_assoc_exists_Rvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rvaluemasklookupvalue) = S ge_signed_half_assoc_exists_Rvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_exists_Rvaluemasklookup) + ge_balance_negative_assoc_exists_Rvaluemasklookupvalue = (dst_negative_assoc_exists_Rvaluemasklookup) + ge_balance_positive_assoc_exists_Rvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_exists_Rvaluemask)=0)) /\ (exists dc_quotient_assoc_exists_Rvaluemaskentry dc_left_assoc_exists_Rvaluemaskentry dc_right_assoc_exists_Rvaluemaskentry. (((dc_input_assoc_exists_R)=(dc_index_assoc_exists_Rvaluemask)*dc_quotient_assoc_exists_Rvaluemaskentry) /\ (((exists dst_positive_code_assoc_exists_Rvaluemaskentryleft dst_positive_scale_assoc_exists_Rvaluemaskentryleft dst_negative_code_assoc_exists_Rvaluemaskentryleft dst_negative_scale_assoc_exists_Rvaluemaskentryleft dst_positive_assoc_exists_Rvaluemaskentryleft dst_negative_assoc_exists_Rvaluemaskentryleft. (((F) = (((((dst_positive_code_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_positive_code_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_positive_scale_assoc_exists_Rvaluemaskentryleft) + (dst_positive_scale_assoc_exists_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)))) + ((((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryleft) + (dst_negative_scale_assoc_exists_Rvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemaskentryleftpositive. ff_h_pvs_assoc_exists_Rvaluemaskentryleftpositive + S (dst_positive_assoc_exists_Rvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_positive_scale_assoc_exists_Rvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Rvaluemaskentryleftpositive. dst_positive_code_assoc_exists_Rvaluemaskentryleft = ff_q_pvs_assoc_exists_Rvaluemaskentryleftpositive * S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_positive_scale_assoc_exists_Rvaluemaskentryleft) + (dst_positive_assoc_exists_Rvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemaskentryleftnegative. ff_h_pvs_assoc_exists_Rvaluemaskentryleftnegative + S (dst_negative_assoc_exists_Rvaluemaskentryleft) = S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_negative_scale_assoc_exists_Rvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_exists_Rvaluemaskentryleftnegative. dst_negative_code_assoc_exists_Rvaluemaskentryleft = ff_q_pvs_assoc_exists_Rvaluemaskentryleftnegative * S ((S (dc_index_assoc_exists_Rvaluemask)) * dst_negative_scale_assoc_exists_Rvaluemaskentryleft) + (dst_negative_assoc_exists_Rvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_exists_Rvaluemaskentryleftvalue ge_balance_negative_assoc_exists_Rvaluemaskentryleftvalue. (((((dc_left_assoc_exists_Rvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Rvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_exists_Rvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemaskentryleftvaluedecode. (((dc_left_assoc_exists_Rvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Rvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rvaluemaskentryleftvalue) = S ge_signed_half_assoc_exists_Rvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_exists_Rvaluemaskentryleft) + ge_balance_negative_assoc_exists_Rvaluemaskentryleftvalue = (dst_negative_assoc_exists_Rvaluemaskentryleft) + ge_balance_positive_assoc_exists_Rvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_exists_Rvaluemaskentryright dst_positive_scale_assoc_exists_Rvaluemaskentryright dst_negative_code_assoc_exists_Rvaluemaskentryright dst_negative_scale_assoc_exists_Rvaluemaskentryright dst_positive_assoc_exists_Rvaluemaskentryright dst_negative_assoc_exists_Rvaluemaskentryright. (((B) = (((((dst_positive_code_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)))) * S ((((dst_positive_code_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_positive_code_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_positive_scale_assoc_exists_Rvaluemaskentryright) + (dst_positive_scale_assoc_exists_Rvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)))) + ((((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright))) + (((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_exists_Rvaluemaskentryright) + (dst_negative_scale_assoc_exists_Rvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemaskentryrightpositive. ff_h_pvs_assoc_exists_Rvaluemaskentryrightpositive + S (dst_positive_assoc_exists_Rvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Rvaluemaskentry)) * dst_positive_scale_assoc_exists_Rvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Rvaluemaskentryrightpositive. dst_positive_code_assoc_exists_Rvaluemaskentryright = ff_q_pvs_assoc_exists_Rvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_exists_Rvaluemaskentry)) * dst_positive_scale_assoc_exists_Rvaluemaskentryright) + (dst_positive_assoc_exists_Rvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_exists_Rvaluemaskentryrightnegative. ff_h_pvs_assoc_exists_Rvaluemaskentryrightnegative + S (dst_negative_assoc_exists_Rvaluemaskentryright) = S ((S (dc_quotient_assoc_exists_Rvaluemaskentry)) * dst_negative_scale_assoc_exists_Rvaluemaskentryright)) /\ exists ff_q_pvs_assoc_exists_Rvaluemaskentryrightnegative. dst_negative_code_assoc_exists_Rvaluemaskentryright = ff_q_pvs_assoc_exists_Rvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_exists_Rvaluemaskentry)) * dst_negative_scale_assoc_exists_Rvaluemaskentryright) + (dst_negative_assoc_exists_Rvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_exists_Rvaluemaskentryrightvalue ge_balance_negative_assoc_exists_Rvaluemaskentryrightvalue. (((((dc_right_assoc_exists_Rvaluemaskentry) = 2 * (ge_balance_positive_assoc_exists_Rvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_exists_Rvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemaskentryrightvaluedecode. (((dc_right_assoc_exists_Rvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Rvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_Rvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_exists_Rvaluemaskentryrightvalue) = S ge_signed_half_assoc_exists_Rvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_exists_Rvaluemaskentryright) + ge_balance_negative_assoc_exists_Rvaluemaskentryrightvalue = (dst_negative_assoc_exists_Rvaluemaskentryright) + ge_balance_positive_assoc_exists_Rvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_exists_Rvaluemaskentryproduct sto_an_assoc_exists_Rvaluemaskentryproduct sto_bp_assoc_exists_Rvaluemaskentryproduct sto_bn_assoc_exists_Rvaluemaskentryproduct sto_cp_assoc_exists_Rvaluemaskentryproduct sto_cn_assoc_exists_Rvaluemaskentryproduct. (((((dc_left_assoc_exists_Rvaluemaskentry) = 2 * (sto_ap_assoc_exists_Rvaluemaskentryproduct) /\ (sto_an_assoc_exists_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemaskentryproductleft. (((dc_left_assoc_exists_Rvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Rvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_exists_Rvaluemaskentryproduct) = 0) /\ (sto_an_assoc_exists_Rvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Rvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_exists_Rvaluemaskentry) = 2 * (sto_bp_assoc_exists_Rvaluemaskentryproduct) /\ (sto_bn_assoc_exists_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemaskentryproductright. (((dc_right_assoc_exists_Rvaluemaskentry) = 2 * ge_signed_half_assoc_exists_Rvaluemaskentryproductright + 1 /\ (sto_bp_assoc_exists_Rvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_exists_Rvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Rvaluemaskentryproductright))) /\ ((((((dc_value_assoc_exists_Rvaluemask) = 2 * (sto_cp_assoc_exists_Rvaluemaskentryproduct) /\ (sto_cn_assoc_exists_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluemaskentryproductoutput. (((dc_value_assoc_exists_Rvaluemask) = 2 * ge_signed_half_assoc_exists_Rvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_exists_Rvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_exists_Rvaluemaskentryproduct) = S ge_signed_half_assoc_exists_Rvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_exists_Rvaluemaskentryproduct * sto_bp_assoc_exists_Rvaluemaskentryproduct + sto_an_assoc_exists_Rvaluemaskentryproduct * sto_bn_assoc_exists_Rvaluemaskentryproduct) + sto_cn_assoc_exists_Rvaluemaskentryproduct = (sto_ap_assoc_exists_Rvaluemaskentryproduct * sto_bn_assoc_exists_Rvaluemaskentryproduct + sto_an_assoc_exists_Rvaluemaskentryproduct * sto_bp_assoc_exists_Rvaluemaskentryproduct) + sto_cp_assoc_exists_Rvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_exists_Rvaluemask)=0 \/ ~(exists pvs_factor_assoc_exists_Rvaluemaskentrynondivisor. (dc_input_assoc_exists_R) = (dc_index_assoc_exists_Rvaluemask) * pvs_factor_assoc_exists_Rvaluemaskentrynondivisor)) /\ ((dc_value_assoc_exists_Rvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_exists_Rvaluefold dst_positive_scale_assoc_exists_Rvaluefold dst_negative_code_assoc_exists_Rvaluefold dst_negative_scale_assoc_exists_Rvaluefold dst_positive_sum_assoc_exists_Rvaluefold dst_negative_sum_assoc_exists_Rvaluefold. (((dc_mask_assoc_exists_Rvalue) = (((((dst_positive_code_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold)) * S ((dst_positive_code_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold)) + ((dst_positive_scale_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold))) + (((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) * S ((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) + ((dst_negative_scale_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)))) * S ((((dst_positive_code_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold)) * S ((dst_positive_code_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold)) + ((dst_positive_scale_assoc_exists_Rvaluefold) + (dst_positive_scale_assoc_exists_Rvaluefold))) + (((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) * S ((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) + ((dst_negative_scale_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)))) + ((((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) * S ((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) + ((dst_negative_scale_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold))) + (((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) * S ((dst_negative_code_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)) + ((dst_negative_scale_assoc_exists_Rvaluefold) + (dst_negative_scale_assoc_exists_Rvaluefold)))))) /\ (((exists fs_u_dst_assoc_exists_Rvaluefoldpositive fs_v_dst_assoc_exists_Rvaluefoldpositive. ((((exists fs_h_dst_assoc_exists_Rvaluefoldpositive_body_start. fs_h_dst_assoc_exists_Rvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldpositive_body_start. fs_u_dst_assoc_exists_Rvaluefoldpositive = fs_q_dst_assoc_exists_Rvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Rvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldpositive_body_terminal. fs_h_dst_assoc_exists_Rvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_exists_Rvaluefold) = S ((S (S (dc_input_assoc_exists_R))) * fs_v_dst_assoc_exists_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldpositive_body_terminal. fs_u_dst_assoc_exists_Rvaluefoldpositive = fs_q_dst_assoc_exists_Rvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_exists_R))) * fs_v_dst_assoc_exists_Rvaluefoldpositive) + (dst_positive_sum_assoc_exists_Rvaluefold))) /\ forall fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_exists_Rvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_exists_Rvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps = S (dc_input_assoc_exists_R)) -> exists fs_a_dst_assoc_exists_Rvaluefoldpositive_body_steps fs_r_dst_assoc_exists_Rvaluefoldpositive_body_steps fs_s_dst_assoc_exists_Rvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_exists_Rvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Rvaluefold)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_exists_Rvaluefold = fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_exists_Rvaluefold) + (fs_a_dst_assoc_exists_Rvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_exists_Rvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_exists_Rvaluefoldpositive = fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldpositive) + (fs_r_dst_assoc_exists_Rvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_exists_Rvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_exists_Rvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_exists_Rvaluefoldpositive = fs_q_dst_assoc_exists_Rvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldpositive) + (fs_s_dst_assoc_exists_Rvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_exists_Rvaluefoldpositive_body_steps = fs_r_dst_assoc_exists_Rvaluefoldpositive_body_steps + fs_a_dst_assoc_exists_Rvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_exists_Rvaluefoldnegative fs_v_dst_assoc_exists_Rvaluefoldnegative. ((((exists fs_h_dst_assoc_exists_Rvaluefoldnegative_body_start. fs_h_dst_assoc_exists_Rvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_exists_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldnegative_body_start. fs_u_dst_assoc_exists_Rvaluefoldnegative = fs_q_dst_assoc_exists_Rvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_exists_Rvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldnegative_body_terminal. fs_h_dst_assoc_exists_Rvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_exists_Rvaluefold) = S ((S (S (dc_input_assoc_exists_R))) * fs_v_dst_assoc_exists_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldnegative_body_terminal. fs_u_dst_assoc_exists_Rvaluefoldnegative = fs_q_dst_assoc_exists_Rvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_exists_R))) * fs_v_dst_assoc_exists_Rvaluefoldnegative) + (dst_negative_sum_assoc_exists_Rvaluefold))) /\ forall fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_exists_Rvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_exists_Rvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps = S (dc_input_assoc_exists_R)) -> exists fs_a_dst_assoc_exists_Rvaluefoldnegative_body_steps fs_r_dst_assoc_exists_Rvaluefoldnegative_body_steps fs_s_dst_assoc_exists_Rvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_exists_Rvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Rvaluefold)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_exists_Rvaluefold = fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_exists_Rvaluefold) + (fs_a_dst_assoc_exists_Rvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_exists_Rvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_exists_Rvaluefoldnegative = fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldnegative) + (fs_r_dst_assoc_exists_Rvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_exists_Rvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_exists_Rvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_exists_Rvaluefoldnegative = fs_q_dst_assoc_exists_Rvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_exists_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_exists_Rvaluefoldnegative) + (fs_s_dst_assoc_exists_Rvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_exists_Rvaluefoldnegative_body_steps = fs_r_dst_assoc_exists_Rvaluefoldnegative_body_steps + fs_a_dst_assoc_exists_Rvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_exists_Rvaluefoldresult ge_balance_negative_assoc_exists_Rvaluefoldresult. (((((dc_output_assoc_exists_R) = 2 * (ge_balance_positive_assoc_exists_Rvaluefoldresult) /\ (ge_balance_negative_assoc_exists_Rvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_exists_Rvaluefoldresultdecode. (((dc_output_assoc_exists_R) = 2 * ge_signed_half_assoc_exists_Rvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_exists_Rvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_exists_Rvaluefoldresult) = S ge_signed_half_assoc_exists_Rvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_exists_Rvaluefold) + ge_balance_negative_assoc_exists_Rvaluefoldresult = (dst_negative_sum_assoc_exists_Rvaluefold) + ge_balance_positive_assoc_exists_Rvaluefoldresult)))))))))))))))))))) /\ (forall dm_index_assoc_exists_equal dm_first_value_assoc_exists_equal dm_second_value_assoc_exists_equal. ~(dm_index_assoc_exists_equal=0) -> (exists pvs_le_gap_assoc_exists_equaldomain. pvs_le_gap_assoc_exists_equaldomain + (dm_index_assoc_exists_equal) = (N)) -> (exists dst_positive_code_assoc_exists_equalfirst dst_positive_scale_assoc_exists_equalfirst dst_negative_code_assoc_exists_equalfirst dst_negative_scale_assoc_exists_equalfirst dst_positive_assoc_exists_equalfirst dst_negative_assoc_exists_equalfirst. (((L) = (((((dst_positive_code_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst)) * S ((dst_positive_code_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst)) + ((dst_positive_scale_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst))) + (((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) * S ((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) + ((dst_negative_scale_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)))) * S ((((dst_positive_code_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst)) * S ((dst_positive_code_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst)) + ((dst_positive_scale_assoc_exists_equalfirst) + (dst_positive_scale_assoc_exists_equalfirst))) + (((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) * S ((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) + ((dst_negative_scale_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)))) + ((((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) * S ((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) + ((dst_negative_scale_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst))) + (((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) * S ((dst_negative_code_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)) + ((dst_negative_scale_assoc_exists_equalfirst) + (dst_negative_scale_assoc_exists_equalfirst)))))) /\ (((((exists ff_h_pvs_assoc_exists_equalfirstpositive. ff_h_pvs_assoc_exists_equalfirstpositive + S (dst_positive_assoc_exists_equalfirst) = S ((S (dm_index_assoc_exists_equal)) * dst_positive_scale_assoc_exists_equalfirst)) /\ exists ff_q_pvs_assoc_exists_equalfirstpositive. dst_positive_code_assoc_exists_equalfirst = ff_q_pvs_assoc_exists_equalfirstpositive * S ((S (dm_index_assoc_exists_equal)) * dst_positive_scale_assoc_exists_equalfirst) + (dst_positive_assoc_exists_equalfirst))) /\ (((((exists ff_h_pvs_assoc_exists_equalfirstnegative. ff_h_pvs_assoc_exists_equalfirstnegative + S (dst_negative_assoc_exists_equalfirst) = S ((S (dm_index_assoc_exists_equal)) * dst_negative_scale_assoc_exists_equalfirst)) /\ exists ff_q_pvs_assoc_exists_equalfirstnegative. dst_negative_code_assoc_exists_equalfirst = ff_q_pvs_assoc_exists_equalfirstnegative * S ((S (dm_index_assoc_exists_equal)) * dst_negative_scale_assoc_exists_equalfirst) + (dst_negative_assoc_exists_equalfirst))) /\ (exists ge_balance_positive_assoc_exists_equalfirstvalue ge_balance_negative_assoc_exists_equalfirstvalue. (((((dm_first_value_assoc_exists_equal) = 2 * (ge_balance_positive_assoc_exists_equalfirstvalue) /\ (ge_balance_negative_assoc_exists_equalfirstvalue) = 0) \/ exists ge_signed_half_assoc_exists_equalfirstvaluedecode. (((dm_first_value_assoc_exists_equal) = 2 * ge_signed_half_assoc_exists_equalfirstvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_equalfirstvalue) = 0) /\ (ge_balance_negative_assoc_exists_equalfirstvalue) = S ge_signed_half_assoc_exists_equalfirstvaluedecode))) /\ ((dst_positive_assoc_exists_equalfirst) + ge_balance_negative_assoc_exists_equalfirstvalue = (dst_negative_assoc_exists_equalfirst) + ge_balance_positive_assoc_exists_equalfirstvalue))))))))) -> (exists dst_positive_code_assoc_exists_equalsecond dst_positive_scale_assoc_exists_equalsecond dst_negative_code_assoc_exists_equalsecond dst_negative_scale_assoc_exists_equalsecond dst_positive_assoc_exists_equalsecond dst_negative_assoc_exists_equalsecond. (((R) = (((((dst_positive_code_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond)) * S ((dst_positive_code_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond)) + ((dst_positive_scale_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond))) + (((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) * S ((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) + ((dst_negative_scale_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)))) * S ((((dst_positive_code_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond)) * S ((dst_positive_code_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond)) + ((dst_positive_scale_assoc_exists_equalsecond) + (dst_positive_scale_assoc_exists_equalsecond))) + (((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) * S ((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) + ((dst_negative_scale_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)))) + ((((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) * S ((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) + ((dst_negative_scale_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond))) + (((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) * S ((dst_negative_code_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)) + ((dst_negative_scale_assoc_exists_equalsecond) + (dst_negative_scale_assoc_exists_equalsecond)))))) /\ (((((exists ff_h_pvs_assoc_exists_equalsecondpositive. ff_h_pvs_assoc_exists_equalsecondpositive + S (dst_positive_assoc_exists_equalsecond) = S ((S (dm_index_assoc_exists_equal)) * dst_positive_scale_assoc_exists_equalsecond)) /\ exists ff_q_pvs_assoc_exists_equalsecondpositive. dst_positive_code_assoc_exists_equalsecond = ff_q_pvs_assoc_exists_equalsecondpositive * S ((S (dm_index_assoc_exists_equal)) * dst_positive_scale_assoc_exists_equalsecond) + (dst_positive_assoc_exists_equalsecond))) /\ (((((exists ff_h_pvs_assoc_exists_equalsecondnegative. ff_h_pvs_assoc_exists_equalsecondnegative + S (dst_negative_assoc_exists_equalsecond) = S ((S (dm_index_assoc_exists_equal)) * dst_negative_scale_assoc_exists_equalsecond)) /\ exists ff_q_pvs_assoc_exists_equalsecondnegative. dst_negative_code_assoc_exists_equalsecond = ff_q_pvs_assoc_exists_equalsecondnegative * S ((S (dm_index_assoc_exists_equal)) * dst_negative_scale_assoc_exists_equalsecond) + (dst_negative_assoc_exists_equalsecond))) /\ (exists ge_balance_positive_assoc_exists_equalsecondvalue ge_balance_negative_assoc_exists_equalsecondvalue. (((((dm_second_value_assoc_exists_equal) = 2 * (ge_balance_positive_assoc_exists_equalsecondvalue) /\ (ge_balance_negative_assoc_exists_equalsecondvalue) = 0) \/ exists ge_signed_half_assoc_exists_equalsecondvaluedecode. (((dm_second_value_assoc_exists_equal) = 2 * ge_signed_half_assoc_exists_equalsecondvaluedecode + 1 /\ (ge_balance_positive_assoc_exists_equalsecondvalue) = 0) /\ (ge_balance_negative_assoc_exists_equalsecondvalue) = S ge_signed_half_assoc_exists_equalsecondvaluedecode))) /\ ((dst_positive_assoc_exists_equalsecond) + ge_balance_negative_assoc_exists_equalsecondvalue = (dst_negative_assoc_exists_equalsecond) + ge_balance_positive_assoc_exists_equalsecondvalue))))))))) -> dm_first_value_assoc_exists_equal=dm_second_value_assoc_exists_equal))))))))