DF0020 — dirichlet_convolution_associative_tables_exists

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

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))))))))

Constructive proof overview

Generated structural guide

Construct all four actual intermediate/output beta tables and prove their positive-domain associativity, including the vacuous N=0 boundary.

The unchanged tactic script uses 2 declared prerequisites and contains 70 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

dirichlet_convolution_table_exists Alpha theorem; checked-use authorized DF001F dirichlet_convolution_tables_associative

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

70 script commands · 23 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)

dirichlet convolution tables associative

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

L1
intro N
L2
intro F
L3
intro G
L4
intro H
L5
intro hF
L6
intro hG
L7
intro hH

02Establish hAL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution table exists.

L8
have hA : ∃ A. DirichletTable(N,F,G,A)Definitions: DirichletTable
L9
specialize dirichlet_convolution_table_exists (N)
L10
specialize dirichlet_convolution_table_exists (F)
L11
specialize dirichlet_convolution_table_exists (G)
L12
apply dirichlet_convolution_table_exists
L13
exact hF
L14
exact hG

03Separate the logical casesL15–15