dirichlet_convolution_tables_associative

forall N F G H A B L R. (((exists dst_positive_code_assoc_tables_Aleft dst_positive_scale_assoc_tables_Aleft dst_negative_code_assoc_tables_Aleft dst_negative_scale_assoc_tables_Aleft. (((F) = (((((dst_positive_code_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft)) * S ((dst_positive_code_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft)) + ((dst_positive_scale_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft))) + (((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) * S ((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) + ((dst_negative_scale_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)))) * S ((((dst_positive_code_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft)) * S ((dst_positive_code_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft)) + ((dst_positive_scale_assoc_tables_Aleft) + (dst_positive_scale_assoc_tables_Aleft))) + (((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) * S ((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) + ((dst_negative_scale_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)))) + ((((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) * S ((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) + ((dst_negative_scale_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft))) + (((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) * S ((dst_negative_code_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)) + ((dst_negative_scale_assoc_tables_Aleft) + (dst_negative_scale_assoc_tables_Aleft)))))) /\ (forall dst_index_assoc_tables_Aleft. (exists pvs_le_gap_assoc_tables_Aleftdomain. pvs_le_gap_assoc_tables_Aleftdomain + (dst_index_assoc_tables_Aleft) = (N)) -> exists dst_positive_assoc_tables_Aleft dst_negative_assoc_tables_Aleft dst_value_assoc_tables_Aleft. ((((exists ff_h_pvs_assoc_tables_Aleftentrypositive. ff_h_pvs_assoc_tables_Aleftentrypositive + S (dst_positive_assoc_tables_Aleft) = S ((S (dst_index_assoc_tables_Aleft)) * dst_positive_scale_assoc_tables_Aleft)) /\ exists ff_q_pvs_assoc_tables_Aleftentrypositive. dst_positive_code_assoc_tables_Aleft = ff_q_pvs_assoc_tables_Aleftentrypositive * S ((S (dst_index_assoc_tables_Aleft)) * dst_positive_scale_assoc_tables_Aleft) + (dst_positive_assoc_tables_Aleft))) /\ (((((exists ff_h_pvs_assoc_tables_Aleftentrynegative. ff_h_pvs_assoc_tables_Aleftentrynegative + S (dst_negative_assoc_tables_Aleft) = S ((S (dst_index_assoc_tables_Aleft)) * dst_negative_scale_assoc_tables_Aleft)) /\ exists ff_q_pvs_assoc_tables_Aleftentrynegative. dst_negative_code_assoc_tables_Aleft = ff_q_pvs_assoc_tables_Aleftentrynegative * S ((S (dst_index_assoc_tables_Aleft)) * dst_negative_scale_assoc_tables_Aleft) + (dst_negative_assoc_tables_Aleft))) /\ (exists ge_balance_positive_assoc_tables_Aleftentryvalue ge_balance_negative_assoc_tables_Aleftentryvalue. (((((dst_value_assoc_tables_Aleft) = 2 * (ge_balance_positive_assoc_tables_Aleftentryvalue) /\ (ge_balance_negative_assoc_tables_Aleftentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Aleftentryvaluedecode. (((dst_value_assoc_tables_Aleft) = 2 * ge_signed_half_assoc_tables_Aleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Aleftentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Aleftentryvalue) = S ge_signed_half_assoc_tables_Aleftentryvaluedecode))) /\ ((dst_positive_assoc_tables_Aleft) + ge_balance_negative_assoc_tables_Aleftentryvalue = (dst_negative_assoc_tables_Aleft) + ge_balance_positive_assoc_tables_Aleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Aright dst_positive_scale_assoc_tables_Aright dst_negative_code_assoc_tables_Aright dst_negative_scale_assoc_tables_Aright. (((G) = (((((dst_positive_code_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright)) * S ((dst_positive_code_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright)) + ((dst_positive_scale_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright))) + (((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) * S ((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) + ((dst_negative_scale_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)))) * S ((((dst_positive_code_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright)) * S ((dst_positive_code_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright)) + ((dst_positive_scale_assoc_tables_Aright) + (dst_positive_scale_assoc_tables_Aright))) + (((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) * S ((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) + ((dst_negative_scale_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)))) + ((((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) * S ((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) + ((dst_negative_scale_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright))) + (((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) * S ((dst_negative_code_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)) + ((dst_negative_scale_assoc_tables_Aright) + (dst_negative_scale_assoc_tables_Aright)))))) /\ (forall dst_index_assoc_tables_Aright. (exists pvs_le_gap_assoc_tables_Arightdomain. pvs_le_gap_assoc_tables_Arightdomain + (dst_index_assoc_tables_Aright) = (N)) -> exists dst_positive_assoc_tables_Aright dst_negative_assoc_tables_Aright dst_value_assoc_tables_Aright. ((((exists ff_h_pvs_assoc_tables_Arightentrypositive. ff_h_pvs_assoc_tables_Arightentrypositive + S (dst_positive_assoc_tables_Aright) = S ((S (dst_index_assoc_tables_Aright)) * dst_positive_scale_assoc_tables_Aright)) /\ exists ff_q_pvs_assoc_tables_Arightentrypositive. dst_positive_code_assoc_tables_Aright = ff_q_pvs_assoc_tables_Arightentrypositive * S ((S (dst_index_assoc_tables_Aright)) * dst_positive_scale_assoc_tables_Aright) + (dst_positive_assoc_tables_Aright))) /\ (((((exists ff_h_pvs_assoc_tables_Arightentrynegative. ff_h_pvs_assoc_tables_Arightentrynegative + S (dst_negative_assoc_tables_Aright) = S ((S (dst_index_assoc_tables_Aright)) * dst_negative_scale_assoc_tables_Aright)) /\ exists ff_q_pvs_assoc_tables_Arightentrynegative. dst_negative_code_assoc_tables_Aright = ff_q_pvs_assoc_tables_Arightentrynegative * S ((S (dst_index_assoc_tables_Aright)) * dst_negative_scale_assoc_tables_Aright) + (dst_negative_assoc_tables_Aright))) /\ (exists ge_balance_positive_assoc_tables_Arightentryvalue ge_balance_negative_assoc_tables_Arightentryvalue. (((((dst_value_assoc_tables_Aright) = 2 * (ge_balance_positive_assoc_tables_Arightentryvalue) /\ (ge_balance_negative_assoc_tables_Arightentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Arightentryvaluedecode. (((dst_value_assoc_tables_Aright) = 2 * ge_signed_half_assoc_tables_Arightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Arightentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Arightentryvalue) = S ge_signed_half_assoc_tables_Arightentryvaluedecode))) /\ ((dst_positive_assoc_tables_Aright) + ge_balance_negative_assoc_tables_Arightentryvalue = (dst_negative_assoc_tables_Aright) + ge_balance_positive_assoc_tables_Arightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Atable dst_positive_scale_assoc_tables_Atable dst_negative_code_assoc_tables_Atable dst_negative_scale_assoc_tables_Atable. (((A) = (((((dst_positive_code_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable)) * S ((dst_positive_code_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable)) + ((dst_positive_scale_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable))) + (((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) * S ((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) + ((dst_negative_scale_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)))) * S ((((dst_positive_code_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable)) * S ((dst_positive_code_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable)) + ((dst_positive_scale_assoc_tables_Atable) + (dst_positive_scale_assoc_tables_Atable))) + (((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) * S ((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) + ((dst_negative_scale_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)))) + ((((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) * S ((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) + ((dst_negative_scale_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable))) + (((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) * S ((dst_negative_code_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)) + ((dst_negative_scale_assoc_tables_Atable) + (dst_negative_scale_assoc_tables_Atable)))))) /\ (forall dst_index_assoc_tables_Atable. (exists pvs_le_gap_assoc_tables_Atabledomain. pvs_le_gap_assoc_tables_Atabledomain + (dst_index_assoc_tables_Atable) = (N)) -> exists dst_positive_assoc_tables_Atable dst_negative_assoc_tables_Atable dst_value_assoc_tables_Atable. ((((exists ff_h_pvs_assoc_tables_Atableentrypositive. ff_h_pvs_assoc_tables_Atableentrypositive + S (dst_positive_assoc_tables_Atable) = S ((S (dst_index_assoc_tables_Atable)) * dst_positive_scale_assoc_tables_Atable)) /\ exists ff_q_pvs_assoc_tables_Atableentrypositive. dst_positive_code_assoc_tables_Atable = ff_q_pvs_assoc_tables_Atableentrypositive * S ((S (dst_index_assoc_tables_Atable)) * dst_positive_scale_assoc_tables_Atable) + (dst_positive_assoc_tables_Atable))) /\ (((((exists ff_h_pvs_assoc_tables_Atableentrynegative. ff_h_pvs_assoc_tables_Atableentrynegative + S (dst_negative_assoc_tables_Atable) = S ((S (dst_index_assoc_tables_Atable)) * dst_negative_scale_assoc_tables_Atable)) /\ exists ff_q_pvs_assoc_tables_Atableentrynegative. dst_negative_code_assoc_tables_Atable = ff_q_pvs_assoc_tables_Atableentrynegative * S ((S (dst_index_assoc_tables_Atable)) * dst_negative_scale_assoc_tables_Atable) + (dst_negative_assoc_tables_Atable))) /\ (exists ge_balance_positive_assoc_tables_Atableentryvalue ge_balance_negative_assoc_tables_Atableentryvalue. (((((dst_value_assoc_tables_Atable) = 2 * (ge_balance_positive_assoc_tables_Atableentryvalue) /\ (ge_balance_negative_assoc_tables_Atableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Atableentryvaluedecode. (((dst_value_assoc_tables_Atable) = 2 * ge_signed_half_assoc_tables_Atableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Atableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Atableentryvalue) = S ge_signed_half_assoc_tables_Atableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Atable) + ge_balance_negative_assoc_tables_Atableentryvalue = (dst_negative_assoc_tables_Atable) + ge_balance_positive_assoc_tables_Atableentryvalue))))))))) /\ (forall dc_input_assoc_tables_A dc_output_assoc_tables_A. ~(dc_input_assoc_tables_A=0) -> (exists pvs_le_gap_assoc_tables_Adomain. pvs_le_gap_assoc_tables_Adomain + (dc_input_assoc_tables_A) = (N)) -> (exists dst_positive_code_assoc_tables_Alookup dst_positive_scale_assoc_tables_Alookup dst_negative_code_assoc_tables_Alookup dst_negative_scale_assoc_tables_Alookup dst_positive_assoc_tables_Alookup dst_negative_assoc_tables_Alookup. (((A) = (((((dst_positive_code_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup)) * S ((dst_positive_code_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup)) + ((dst_positive_scale_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup))) + (((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) * S ((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) + ((dst_negative_scale_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)))) * S ((((dst_positive_code_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup)) * S ((dst_positive_code_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup)) + ((dst_positive_scale_assoc_tables_Alookup) + (dst_positive_scale_assoc_tables_Alookup))) + (((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) * S ((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) + ((dst_negative_scale_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)))) + ((((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) * S ((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) + ((dst_negative_scale_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup))) + (((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) * S ((dst_negative_code_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)) + ((dst_negative_scale_assoc_tables_Alookup) + (dst_negative_scale_assoc_tables_Alookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Alookuppositive. ff_h_pvs_assoc_tables_Alookuppositive + S (dst_positive_assoc_tables_Alookup) = S ((S (dc_input_assoc_tables_A)) * dst_positive_scale_assoc_tables_Alookup)) /\ exists ff_q_pvs_assoc_tables_Alookuppositive. dst_positive_code_assoc_tables_Alookup = ff_q_pvs_assoc_tables_Alookuppositive * S ((S (dc_input_assoc_tables_A)) * dst_positive_scale_assoc_tables_Alookup) + (dst_positive_assoc_tables_Alookup))) /\ (((((exists ff_h_pvs_assoc_tables_Alookupnegative. ff_h_pvs_assoc_tables_Alookupnegative + S (dst_negative_assoc_tables_Alookup) = S ((S (dc_input_assoc_tables_A)) * dst_negative_scale_assoc_tables_Alookup)) /\ exists ff_q_pvs_assoc_tables_Alookupnegative. dst_negative_code_assoc_tables_Alookup = ff_q_pvs_assoc_tables_Alookupnegative * S ((S (dc_input_assoc_tables_A)) * dst_negative_scale_assoc_tables_Alookup) + (dst_negative_assoc_tables_Alookup))) /\ (exists ge_balance_positive_assoc_tables_Alookupvalue ge_balance_negative_assoc_tables_Alookupvalue. (((((dc_output_assoc_tables_A) = 2 * (ge_balance_positive_assoc_tables_Alookupvalue) /\ (ge_balance_negative_assoc_tables_Alookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Alookupvaluedecode. (((dc_output_assoc_tables_A) = 2 * ge_signed_half_assoc_tables_Alookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Alookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Alookupvalue) = S ge_signed_half_assoc_tables_Alookupvaluedecode))) /\ ((dst_positive_assoc_tables_Alookup) + ge_balance_negative_assoc_tables_Alookupvalue = (dst_negative_assoc_tables_Alookup) + ge_balance_positive_assoc_tables_Alookupvalue))))))))) -> (((~((dc_input_assoc_tables_A)=0)) /\ (exists dc_mask_assoc_tables_Avalue. ((((exists dst_positive_code_assoc_tables_Avaluemasktable dst_positive_scale_assoc_tables_Avaluemasktable dst_negative_code_assoc_tables_Avaluemasktable dst_negative_scale_assoc_tables_Avaluemasktable. (((dc_mask_assoc_tables_Avalue) = (((((dst_positive_code_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable)) * S ((dst_positive_code_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable)) + ((dst_positive_scale_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable))) + (((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) * S ((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) + ((dst_negative_scale_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)))) * S ((((dst_positive_code_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable)) * S ((dst_positive_code_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable)) + ((dst_positive_scale_assoc_tables_Avaluemasktable) + (dst_positive_scale_assoc_tables_Avaluemasktable))) + (((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) * S ((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) + ((dst_negative_scale_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)))) + ((((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) * S ((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) + ((dst_negative_scale_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable))) + (((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) * S ((dst_negative_code_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)) + ((dst_negative_scale_assoc_tables_Avaluemasktable) + (dst_negative_scale_assoc_tables_Avaluemasktable)))))) /\ (forall dst_index_assoc_tables_Avaluemasktable. (exists pvs_le_gap_assoc_tables_Avaluemasktabledomain. pvs_le_gap_assoc_tables_Avaluemasktabledomain + (dst_index_assoc_tables_Avaluemasktable) = (dc_input_assoc_tables_A)) -> exists dst_positive_assoc_tables_Avaluemasktable dst_negative_assoc_tables_Avaluemasktable dst_value_assoc_tables_Avaluemasktable. ((((exists ff_h_pvs_assoc_tables_Avaluemasktableentrypositive. ff_h_pvs_assoc_tables_Avaluemasktableentrypositive + S (dst_positive_assoc_tables_Avaluemasktable) = S ((S (dst_index_assoc_tables_Avaluemasktable)) * dst_positive_scale_assoc_tables_Avaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Avaluemasktableentrypositive. dst_positive_code_assoc_tables_Avaluemasktable = ff_q_pvs_assoc_tables_Avaluemasktableentrypositive * S ((S (dst_index_assoc_tables_Avaluemasktable)) * dst_positive_scale_assoc_tables_Avaluemasktable) + (dst_positive_assoc_tables_Avaluemasktable))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemasktableentrynegative. ff_h_pvs_assoc_tables_Avaluemasktableentrynegative + S (dst_negative_assoc_tables_Avaluemasktable) = S ((S (dst_index_assoc_tables_Avaluemasktable)) * dst_negative_scale_assoc_tables_Avaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Avaluemasktableentrynegative. dst_negative_code_assoc_tables_Avaluemasktable = ff_q_pvs_assoc_tables_Avaluemasktableentrynegative * S ((S (dst_index_assoc_tables_Avaluemasktable)) * dst_negative_scale_assoc_tables_Avaluemasktable) + (dst_negative_assoc_tables_Avaluemasktable))) /\ (exists ge_balance_positive_assoc_tables_Avaluemasktableentryvalue ge_balance_negative_assoc_tables_Avaluemasktableentryvalue. (((((dst_value_assoc_tables_Avaluemasktable) = 2 * (ge_balance_positive_assoc_tables_Avaluemasktableentryvalue) /\ (ge_balance_negative_assoc_tables_Avaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemasktableentryvaluedecode. (((dst_value_assoc_tables_Avaluemasktable) = 2 * ge_signed_half_assoc_tables_Avaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Avaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Avaluemasktableentryvalue) = S ge_signed_half_assoc_tables_Avaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Avaluemasktable) + ge_balance_negative_assoc_tables_Avaluemasktableentryvalue = (dst_negative_assoc_tables_Avaluemasktable) + ge_balance_positive_assoc_tables_Avaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_tables_Avaluemask dc_value_assoc_tables_Avaluemask. (exists pvs_le_gap_assoc_tables_Avaluemaskdomain. pvs_le_gap_assoc_tables_Avaluemaskdomain + (dc_index_assoc_tables_Avaluemask) = (dc_input_assoc_tables_A)) -> (exists dst_positive_code_assoc_tables_Avaluemasklookup dst_positive_scale_assoc_tables_Avaluemasklookup dst_negative_code_assoc_tables_Avaluemasklookup dst_negative_scale_assoc_tables_Avaluemasklookup dst_positive_assoc_tables_Avaluemasklookup dst_negative_assoc_tables_Avaluemasklookup. (((dc_mask_assoc_tables_Avalue) = (((((dst_positive_code_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup)) * S ((dst_positive_code_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup)) + ((dst_positive_scale_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup))) + (((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) * S ((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) + ((dst_negative_scale_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)))) * S ((((dst_positive_code_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup)) * S ((dst_positive_code_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup)) + ((dst_positive_scale_assoc_tables_Avaluemasklookup) + (dst_positive_scale_assoc_tables_Avaluemasklookup))) + (((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) * S ((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) + ((dst_negative_scale_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)))) + ((((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) * S ((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) + ((dst_negative_scale_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup))) + (((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) * S ((dst_negative_code_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)) + ((dst_negative_scale_assoc_tables_Avaluemasklookup) + (dst_negative_scale_assoc_tables_Avaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemasklookuppositive. ff_h_pvs_assoc_tables_Avaluemasklookuppositive + S (dst_positive_assoc_tables_Avaluemasklookup) = S ((S (dc_index_assoc_tables_Avaluemask)) * dst_positive_scale_assoc_tables_Avaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Avaluemasklookuppositive. dst_positive_code_assoc_tables_Avaluemasklookup = ff_q_pvs_assoc_tables_Avaluemasklookuppositive * S ((S (dc_index_assoc_tables_Avaluemask)) * dst_positive_scale_assoc_tables_Avaluemasklookup) + (dst_positive_assoc_tables_Avaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemasklookupnegative. ff_h_pvs_assoc_tables_Avaluemasklookupnegative + S (dst_negative_assoc_tables_Avaluemasklookup) = S ((S (dc_index_assoc_tables_Avaluemask)) * dst_negative_scale_assoc_tables_Avaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Avaluemasklookupnegative. dst_negative_code_assoc_tables_Avaluemasklookup = ff_q_pvs_assoc_tables_Avaluemasklookupnegative * S ((S (dc_index_assoc_tables_Avaluemask)) * dst_negative_scale_assoc_tables_Avaluemasklookup) + (dst_negative_assoc_tables_Avaluemasklookup))) /\ (exists ge_balance_positive_assoc_tables_Avaluemasklookupvalue ge_balance_negative_assoc_tables_Avaluemasklookupvalue. (((((dc_value_assoc_tables_Avaluemask) = 2 * (ge_balance_positive_assoc_tables_Avaluemasklookupvalue) /\ (ge_balance_negative_assoc_tables_Avaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemasklookupvaluedecode. (((dc_value_assoc_tables_Avaluemask) = 2 * ge_signed_half_assoc_tables_Avaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Avaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Avaluemasklookupvalue) = S ge_signed_half_assoc_tables_Avaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_tables_Avaluemasklookup) + ge_balance_negative_assoc_tables_Avaluemasklookupvalue = (dst_negative_assoc_tables_Avaluemasklookup) + ge_balance_positive_assoc_tables_Avaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_tables_Avaluemask)=0)) /\ (exists dc_quotient_assoc_tables_Avaluemaskentry dc_left_assoc_tables_Avaluemaskentry dc_right_assoc_tables_Avaluemaskentry. (((dc_input_assoc_tables_A)=(dc_index_assoc_tables_Avaluemask)*dc_quotient_assoc_tables_Avaluemaskentry) /\ (((exists dst_positive_code_assoc_tables_Avaluemaskentryleft dst_positive_scale_assoc_tables_Avaluemaskentryleft dst_negative_code_assoc_tables_Avaluemaskentryleft dst_negative_scale_assoc_tables_Avaluemaskentryleft dst_positive_assoc_tables_Avaluemaskentryleft dst_negative_assoc_tables_Avaluemaskentryleft. (((F) = (((((dst_positive_code_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)))) * S ((((dst_positive_code_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Avaluemaskentryleft) + (dst_positive_scale_assoc_tables_Avaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)))) + ((((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryleft) + (dst_negative_scale_assoc_tables_Avaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemaskentryleftpositive. ff_h_pvs_assoc_tables_Avaluemaskentryleftpositive + S (dst_positive_assoc_tables_Avaluemaskentryleft) = S ((S (dc_index_assoc_tables_Avaluemask)) * dst_positive_scale_assoc_tables_Avaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Avaluemaskentryleftpositive. dst_positive_code_assoc_tables_Avaluemaskentryleft = ff_q_pvs_assoc_tables_Avaluemaskentryleftpositive * S ((S (dc_index_assoc_tables_Avaluemask)) * dst_positive_scale_assoc_tables_Avaluemaskentryleft) + (dst_positive_assoc_tables_Avaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemaskentryleftnegative. ff_h_pvs_assoc_tables_Avaluemaskentryleftnegative + S (dst_negative_assoc_tables_Avaluemaskentryleft) = S ((S (dc_index_assoc_tables_Avaluemask)) * dst_negative_scale_assoc_tables_Avaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Avaluemaskentryleftnegative. dst_negative_code_assoc_tables_Avaluemaskentryleft = ff_q_pvs_assoc_tables_Avaluemaskentryleftnegative * S ((S (dc_index_assoc_tables_Avaluemask)) * dst_negative_scale_assoc_tables_Avaluemaskentryleft) + (dst_negative_assoc_tables_Avaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_tables_Avaluemaskentryleftvalue ge_balance_negative_assoc_tables_Avaluemaskentryleftvalue. (((((dc_left_assoc_tables_Avaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Avaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_tables_Avaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemaskentryleftvaluedecode. (((dc_left_assoc_tables_Avaluemaskentry) = 2 * ge_signed_half_assoc_tables_Avaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Avaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_tables_Avaluemaskentryleftvalue) = S ge_signed_half_assoc_tables_Avaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_tables_Avaluemaskentryleft) + ge_balance_negative_assoc_tables_Avaluemaskentryleftvalue = (dst_negative_assoc_tables_Avaluemaskentryleft) + ge_balance_positive_assoc_tables_Avaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Avaluemaskentryright dst_positive_scale_assoc_tables_Avaluemaskentryright dst_negative_code_assoc_tables_Avaluemaskentryright dst_negative_scale_assoc_tables_Avaluemaskentryright dst_positive_assoc_tables_Avaluemaskentryright dst_negative_assoc_tables_Avaluemaskentryright. (((G) = (((((dst_positive_code_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright))) + (((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)))) * S ((((dst_positive_code_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Avaluemaskentryright) + (dst_positive_scale_assoc_tables_Avaluemaskentryright))) + (((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)))) + ((((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright))) + (((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Avaluemaskentryright) + (dst_negative_scale_assoc_tables_Avaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemaskentryrightpositive. ff_h_pvs_assoc_tables_Avaluemaskentryrightpositive + S (dst_positive_assoc_tables_Avaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Avaluemaskentry)) * dst_positive_scale_assoc_tables_Avaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Avaluemaskentryrightpositive. dst_positive_code_assoc_tables_Avaluemaskentryright = ff_q_pvs_assoc_tables_Avaluemaskentryrightpositive * S ((S (dc_quotient_assoc_tables_Avaluemaskentry)) * dst_positive_scale_assoc_tables_Avaluemaskentryright) + (dst_positive_assoc_tables_Avaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_tables_Avaluemaskentryrightnegative. ff_h_pvs_assoc_tables_Avaluemaskentryrightnegative + S (dst_negative_assoc_tables_Avaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Avaluemaskentry)) * dst_negative_scale_assoc_tables_Avaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Avaluemaskentryrightnegative. dst_negative_code_assoc_tables_Avaluemaskentryright = ff_q_pvs_assoc_tables_Avaluemaskentryrightnegative * S ((S (dc_quotient_assoc_tables_Avaluemaskentry)) * dst_negative_scale_assoc_tables_Avaluemaskentryright) + (dst_negative_assoc_tables_Avaluemaskentryright))) /\ (exists ge_balance_positive_assoc_tables_Avaluemaskentryrightvalue ge_balance_negative_assoc_tables_Avaluemaskentryrightvalue. (((((dc_right_assoc_tables_Avaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Avaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_tables_Avaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemaskentryrightvaluedecode. (((dc_right_assoc_tables_Avaluemaskentry) = 2 * ge_signed_half_assoc_tables_Avaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Avaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_tables_Avaluemaskentryrightvalue) = S ge_signed_half_assoc_tables_Avaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_tables_Avaluemaskentryright) + ge_balance_negative_assoc_tables_Avaluemaskentryrightvalue = (dst_negative_assoc_tables_Avaluemaskentryright) + ge_balance_positive_assoc_tables_Avaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_tables_Avaluemaskentryproduct sto_an_assoc_tables_Avaluemaskentryproduct sto_bp_assoc_tables_Avaluemaskentryproduct sto_bn_assoc_tables_Avaluemaskentryproduct sto_cp_assoc_tables_Avaluemaskentryproduct sto_cn_assoc_tables_Avaluemaskentryproduct. (((((dc_left_assoc_tables_Avaluemaskentry) = 2 * (sto_ap_assoc_tables_Avaluemaskentryproduct) /\ (sto_an_assoc_tables_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemaskentryproductleft. (((dc_left_assoc_tables_Avaluemaskentry) = 2 * ge_signed_half_assoc_tables_Avaluemaskentryproductleft + 1 /\ (sto_ap_assoc_tables_Avaluemaskentryproduct) = 0) /\ (sto_an_assoc_tables_Avaluemaskentryproduct) = S ge_signed_half_assoc_tables_Avaluemaskentryproductleft))) /\ ((((((dc_right_assoc_tables_Avaluemaskentry) = 2 * (sto_bp_assoc_tables_Avaluemaskentryproduct) /\ (sto_bn_assoc_tables_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemaskentryproductright. (((dc_right_assoc_tables_Avaluemaskentry) = 2 * ge_signed_half_assoc_tables_Avaluemaskentryproductright + 1 /\ (sto_bp_assoc_tables_Avaluemaskentryproduct) = 0) /\ (sto_bn_assoc_tables_Avaluemaskentryproduct) = S ge_signed_half_assoc_tables_Avaluemaskentryproductright))) /\ ((((((dc_value_assoc_tables_Avaluemask) = 2 * (sto_cp_assoc_tables_Avaluemaskentryproduct) /\ (sto_cn_assoc_tables_Avaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Avaluemaskentryproductoutput. (((dc_value_assoc_tables_Avaluemask) = 2 * ge_signed_half_assoc_tables_Avaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_tables_Avaluemaskentryproduct) = 0) /\ (sto_cn_assoc_tables_Avaluemaskentryproduct) = S ge_signed_half_assoc_tables_Avaluemaskentryproductoutput))) /\ ((sto_ap_assoc_tables_Avaluemaskentryproduct * sto_bp_assoc_tables_Avaluemaskentryproduct + sto_an_assoc_tables_Avaluemaskentryproduct * sto_bn_assoc_tables_Avaluemaskentryproduct) + sto_cn_assoc_tables_Avaluemaskentryproduct = (sto_ap_assoc_tables_Avaluemaskentryproduct * sto_bn_assoc_tables_Avaluemaskentryproduct + sto_an_assoc_tables_Avaluemaskentryproduct * sto_bp_assoc_tables_Avaluemaskentryproduct) + sto_cp_assoc_tables_Avaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_tables_Avaluemask)=0 \/ ~(exists pvs_factor_assoc_tables_Avaluemaskentrynondivisor. (dc_input_assoc_tables_A) = (dc_index_assoc_tables_Avaluemask) * pvs_factor_assoc_tables_Avaluemaskentrynondivisor)) /\ ((dc_value_assoc_tables_Avaluemask)=0))))))) /\ (exists dst_positive_code_assoc_tables_Avaluefold dst_positive_scale_assoc_tables_Avaluefold dst_negative_code_assoc_tables_Avaluefold dst_negative_scale_assoc_tables_Avaluefold dst_positive_sum_assoc_tables_Avaluefold dst_negative_sum_assoc_tables_Avaluefold. (((dc_mask_assoc_tables_Avalue) = (((((dst_positive_code_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold)) * S ((dst_positive_code_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold)) + ((dst_positive_scale_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold))) + (((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) * S ((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) + ((dst_negative_scale_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)))) * S ((((dst_positive_code_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold)) * S ((dst_positive_code_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold)) + ((dst_positive_scale_assoc_tables_Avaluefold) + (dst_positive_scale_assoc_tables_Avaluefold))) + (((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) * S ((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) + ((dst_negative_scale_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)))) + ((((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) * S ((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) + ((dst_negative_scale_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold))) + (((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) * S ((dst_negative_code_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)) + ((dst_negative_scale_assoc_tables_Avaluefold) + (dst_negative_scale_assoc_tables_Avaluefold)))))) /\ (((exists fs_u_dst_assoc_tables_Avaluefoldpositive fs_v_dst_assoc_tables_Avaluefoldpositive. ((((exists fs_h_dst_assoc_tables_Avaluefoldpositive_body_start. fs_h_dst_assoc_tables_Avaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Avaluefoldpositive_body_start. fs_u_dst_assoc_tables_Avaluefoldpositive = fs_q_dst_assoc_tables_Avaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Avaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldpositive_body_terminal. fs_h_dst_assoc_tables_Avaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_tables_Avaluefold) = S ((S (S (dc_input_assoc_tables_A))) * fs_v_dst_assoc_tables_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Avaluefoldpositive_body_terminal. fs_u_dst_assoc_tables_Avaluefoldpositive = fs_q_dst_assoc_tables_Avaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_tables_A))) * fs_v_dst_assoc_tables_Avaluefoldpositive) + (dst_positive_sum_assoc_tables_Avaluefold))) /\ forall fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_tables_Avaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_tables_Avaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps = S (dc_input_assoc_tables_A)) -> exists fs_a_dst_assoc_tables_Avaluefoldpositive_body_steps fs_r_dst_assoc_tables_Avaluefoldpositive_body_steps fs_s_dst_assoc_tables_Avaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_summand. fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_tables_Avaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Avaluefold)) /\ exists fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_summand. dst_positive_code_assoc_tables_Avaluefold = fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Avaluefold) + (fs_a_dst_assoc_tables_Avaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_partial. fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_tables_Avaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_partial. fs_u_dst_assoc_tables_Avaluefoldpositive = fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldpositive) + (fs_r_dst_assoc_tables_Avaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_successor. fs_h_dst_assoc_tables_Avaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_tables_Avaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_successor. fs_u_dst_assoc_tables_Avaluefoldpositive = fs_q_dst_assoc_tables_Avaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Avaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldpositive) + (fs_s_dst_assoc_tables_Avaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_tables_Avaluefoldpositive_body_steps = fs_r_dst_assoc_tables_Avaluefoldpositive_body_steps + fs_a_dst_assoc_tables_Avaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_tables_Avaluefoldnegative fs_v_dst_assoc_tables_Avaluefoldnegative. ((((exists fs_h_dst_assoc_tables_Avaluefoldnegative_body_start. fs_h_dst_assoc_tables_Avaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Avaluefoldnegative_body_start. fs_u_dst_assoc_tables_Avaluefoldnegative = fs_q_dst_assoc_tables_Avaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Avaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldnegative_body_terminal. fs_h_dst_assoc_tables_Avaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_tables_Avaluefold) = S ((S (S (dc_input_assoc_tables_A))) * fs_v_dst_assoc_tables_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Avaluefoldnegative_body_terminal. fs_u_dst_assoc_tables_Avaluefoldnegative = fs_q_dst_assoc_tables_Avaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_tables_A))) * fs_v_dst_assoc_tables_Avaluefoldnegative) + (dst_negative_sum_assoc_tables_Avaluefold))) /\ forall fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_tables_Avaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_tables_Avaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps = S (dc_input_assoc_tables_A)) -> exists fs_a_dst_assoc_tables_Avaluefoldnegative_body_steps fs_r_dst_assoc_tables_Avaluefoldnegative_body_steps fs_s_dst_assoc_tables_Avaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_summand. fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_tables_Avaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Avaluefold)) /\ exists fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_summand. dst_negative_code_assoc_tables_Avaluefold = fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Avaluefold) + (fs_a_dst_assoc_tables_Avaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_partial. fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_tables_Avaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_partial. fs_u_dst_assoc_tables_Avaluefoldnegative = fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldnegative) + (fs_r_dst_assoc_tables_Avaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_successor. fs_h_dst_assoc_tables_Avaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_tables_Avaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_successor. fs_u_dst_assoc_tables_Avaluefoldnegative = fs_q_dst_assoc_tables_Avaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Avaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Avaluefoldnegative) + (fs_s_dst_assoc_tables_Avaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_tables_Avaluefoldnegative_body_steps = fs_r_dst_assoc_tables_Avaluefoldnegative_body_steps + fs_a_dst_assoc_tables_Avaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_tables_Avaluefoldresult ge_balance_negative_assoc_tables_Avaluefoldresult. (((((dc_output_assoc_tables_A) = 2 * (ge_balance_positive_assoc_tables_Avaluefoldresult) /\ (ge_balance_negative_assoc_tables_Avaluefoldresult) = 0) \/ exists ge_signed_half_assoc_tables_Avaluefoldresultdecode. (((dc_output_assoc_tables_A) = 2 * ge_signed_half_assoc_tables_Avaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_tables_Avaluefoldresult) = 0) /\ (ge_balance_negative_assoc_tables_Avaluefoldresult) = S ge_signed_half_assoc_tables_Avaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_tables_Avaluefold) + ge_balance_negative_assoc_tables_Avaluefoldresult = (dst_negative_sum_assoc_tables_Avaluefold) + ge_balance_positive_assoc_tables_Avaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_assoc_tables_Bleft dst_positive_scale_assoc_tables_Bleft dst_negative_code_assoc_tables_Bleft dst_negative_scale_assoc_tables_Bleft. (((G) = (((((dst_positive_code_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft)) * S ((dst_positive_code_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft)) + ((dst_positive_scale_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft))) + (((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) * S ((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) + ((dst_negative_scale_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)))) * S ((((dst_positive_code_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft)) * S ((dst_positive_code_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft)) + ((dst_positive_scale_assoc_tables_Bleft) + (dst_positive_scale_assoc_tables_Bleft))) + (((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) * S ((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) + ((dst_negative_scale_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)))) + ((((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) * S ((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) + ((dst_negative_scale_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft))) + (((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) * S ((dst_negative_code_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)) + ((dst_negative_scale_assoc_tables_Bleft) + (dst_negative_scale_assoc_tables_Bleft)))))) /\ (forall dst_index_assoc_tables_Bleft. (exists pvs_le_gap_assoc_tables_Bleftdomain. pvs_le_gap_assoc_tables_Bleftdomain + (dst_index_assoc_tables_Bleft) = (N)) -> exists dst_positive_assoc_tables_Bleft dst_negative_assoc_tables_Bleft dst_value_assoc_tables_Bleft. ((((exists ff_h_pvs_assoc_tables_Bleftentrypositive. ff_h_pvs_assoc_tables_Bleftentrypositive + S (dst_positive_assoc_tables_Bleft) = S ((S (dst_index_assoc_tables_Bleft)) * dst_positive_scale_assoc_tables_Bleft)) /\ exists ff_q_pvs_assoc_tables_Bleftentrypositive. dst_positive_code_assoc_tables_Bleft = ff_q_pvs_assoc_tables_Bleftentrypositive * S ((S (dst_index_assoc_tables_Bleft)) * dst_positive_scale_assoc_tables_Bleft) + (dst_positive_assoc_tables_Bleft))) /\ (((((exists ff_h_pvs_assoc_tables_Bleftentrynegative. ff_h_pvs_assoc_tables_Bleftentrynegative + S (dst_negative_assoc_tables_Bleft) = S ((S (dst_index_assoc_tables_Bleft)) * dst_negative_scale_assoc_tables_Bleft)) /\ exists ff_q_pvs_assoc_tables_Bleftentrynegative. dst_negative_code_assoc_tables_Bleft = ff_q_pvs_assoc_tables_Bleftentrynegative * S ((S (dst_index_assoc_tables_Bleft)) * dst_negative_scale_assoc_tables_Bleft) + (dst_negative_assoc_tables_Bleft))) /\ (exists ge_balance_positive_assoc_tables_Bleftentryvalue ge_balance_negative_assoc_tables_Bleftentryvalue. (((((dst_value_assoc_tables_Bleft) = 2 * (ge_balance_positive_assoc_tables_Bleftentryvalue) /\ (ge_balance_negative_assoc_tables_Bleftentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Bleftentryvaluedecode. (((dst_value_assoc_tables_Bleft) = 2 * ge_signed_half_assoc_tables_Bleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Bleftentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Bleftentryvalue) = S ge_signed_half_assoc_tables_Bleftentryvaluedecode))) /\ ((dst_positive_assoc_tables_Bleft) + ge_balance_negative_assoc_tables_Bleftentryvalue = (dst_negative_assoc_tables_Bleft) + ge_balance_positive_assoc_tables_Bleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Bright dst_positive_scale_assoc_tables_Bright dst_negative_code_assoc_tables_Bright dst_negative_scale_assoc_tables_Bright. (((H) = (((((dst_positive_code_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright)) * S ((dst_positive_code_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright)) + ((dst_positive_scale_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright))) + (((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) * S ((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) + ((dst_negative_scale_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)))) * S ((((dst_positive_code_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright)) * S ((dst_positive_code_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright)) + ((dst_positive_scale_assoc_tables_Bright) + (dst_positive_scale_assoc_tables_Bright))) + (((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) * S ((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) + ((dst_negative_scale_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)))) + ((((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) * S ((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) + ((dst_negative_scale_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright))) + (((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) * S ((dst_negative_code_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)) + ((dst_negative_scale_assoc_tables_Bright) + (dst_negative_scale_assoc_tables_Bright)))))) /\ (forall dst_index_assoc_tables_Bright. (exists pvs_le_gap_assoc_tables_Brightdomain. pvs_le_gap_assoc_tables_Brightdomain + (dst_index_assoc_tables_Bright) = (N)) -> exists dst_positive_assoc_tables_Bright dst_negative_assoc_tables_Bright dst_value_assoc_tables_Bright. ((((exists ff_h_pvs_assoc_tables_Brightentrypositive. ff_h_pvs_assoc_tables_Brightentrypositive + S (dst_positive_assoc_tables_Bright) = S ((S (dst_index_assoc_tables_Bright)) * dst_positive_scale_assoc_tables_Bright)) /\ exists ff_q_pvs_assoc_tables_Brightentrypositive. dst_positive_code_assoc_tables_Bright = ff_q_pvs_assoc_tables_Brightentrypositive * S ((S (dst_index_assoc_tables_Bright)) * dst_positive_scale_assoc_tables_Bright) + (dst_positive_assoc_tables_Bright))) /\ (((((exists ff_h_pvs_assoc_tables_Brightentrynegative. ff_h_pvs_assoc_tables_Brightentrynegative + S (dst_negative_assoc_tables_Bright) = S ((S (dst_index_assoc_tables_Bright)) * dst_negative_scale_assoc_tables_Bright)) /\ exists ff_q_pvs_assoc_tables_Brightentrynegative. dst_negative_code_assoc_tables_Bright = ff_q_pvs_assoc_tables_Brightentrynegative * S ((S (dst_index_assoc_tables_Bright)) * dst_negative_scale_assoc_tables_Bright) + (dst_negative_assoc_tables_Bright))) /\ (exists ge_balance_positive_assoc_tables_Brightentryvalue ge_balance_negative_assoc_tables_Brightentryvalue. (((((dst_value_assoc_tables_Bright) = 2 * (ge_balance_positive_assoc_tables_Brightentryvalue) /\ (ge_balance_negative_assoc_tables_Brightentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Brightentryvaluedecode. (((dst_value_assoc_tables_Bright) = 2 * ge_signed_half_assoc_tables_Brightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Brightentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Brightentryvalue) = S ge_signed_half_assoc_tables_Brightentryvaluedecode))) /\ ((dst_positive_assoc_tables_Bright) + ge_balance_negative_assoc_tables_Brightentryvalue = (dst_negative_assoc_tables_Bright) + ge_balance_positive_assoc_tables_Brightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Btable dst_positive_scale_assoc_tables_Btable dst_negative_code_assoc_tables_Btable dst_negative_scale_assoc_tables_Btable. (((B) = (((((dst_positive_code_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable)) * S ((dst_positive_code_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable)) + ((dst_positive_scale_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable))) + (((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) * S ((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) + ((dst_negative_scale_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)))) * S ((((dst_positive_code_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable)) * S ((dst_positive_code_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable)) + ((dst_positive_scale_assoc_tables_Btable) + (dst_positive_scale_assoc_tables_Btable))) + (((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) * S ((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) + ((dst_negative_scale_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)))) + ((((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) * S ((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) + ((dst_negative_scale_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable))) + (((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) * S ((dst_negative_code_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)) + ((dst_negative_scale_assoc_tables_Btable) + (dst_negative_scale_assoc_tables_Btable)))))) /\ (forall dst_index_assoc_tables_Btable. (exists pvs_le_gap_assoc_tables_Btabledomain. pvs_le_gap_assoc_tables_Btabledomain + (dst_index_assoc_tables_Btable) = (N)) -> exists dst_positive_assoc_tables_Btable dst_negative_assoc_tables_Btable dst_value_assoc_tables_Btable. ((((exists ff_h_pvs_assoc_tables_Btableentrypositive. ff_h_pvs_assoc_tables_Btableentrypositive + S (dst_positive_assoc_tables_Btable) = S ((S (dst_index_assoc_tables_Btable)) * dst_positive_scale_assoc_tables_Btable)) /\ exists ff_q_pvs_assoc_tables_Btableentrypositive. dst_positive_code_assoc_tables_Btable = ff_q_pvs_assoc_tables_Btableentrypositive * S ((S (dst_index_assoc_tables_Btable)) * dst_positive_scale_assoc_tables_Btable) + (dst_positive_assoc_tables_Btable))) /\ (((((exists ff_h_pvs_assoc_tables_Btableentrynegative. ff_h_pvs_assoc_tables_Btableentrynegative + S (dst_negative_assoc_tables_Btable) = S ((S (dst_index_assoc_tables_Btable)) * dst_negative_scale_assoc_tables_Btable)) /\ exists ff_q_pvs_assoc_tables_Btableentrynegative. dst_negative_code_assoc_tables_Btable = ff_q_pvs_assoc_tables_Btableentrynegative * S ((S (dst_index_assoc_tables_Btable)) * dst_negative_scale_assoc_tables_Btable) + (dst_negative_assoc_tables_Btable))) /\ (exists ge_balance_positive_assoc_tables_Btableentryvalue ge_balance_negative_assoc_tables_Btableentryvalue. (((((dst_value_assoc_tables_Btable) = 2 * (ge_balance_positive_assoc_tables_Btableentryvalue) /\ (ge_balance_negative_assoc_tables_Btableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Btableentryvaluedecode. (((dst_value_assoc_tables_Btable) = 2 * ge_signed_half_assoc_tables_Btableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Btableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Btableentryvalue) = S ge_signed_half_assoc_tables_Btableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Btable) + ge_balance_negative_assoc_tables_Btableentryvalue = (dst_negative_assoc_tables_Btable) + ge_balance_positive_assoc_tables_Btableentryvalue))))))))) /\ (forall dc_input_assoc_tables_B dc_output_assoc_tables_B. ~(dc_input_assoc_tables_B=0) -> (exists pvs_le_gap_assoc_tables_Bdomain. pvs_le_gap_assoc_tables_Bdomain + (dc_input_assoc_tables_B) = (N)) -> (exists dst_positive_code_assoc_tables_Blookup dst_positive_scale_assoc_tables_Blookup dst_negative_code_assoc_tables_Blookup dst_negative_scale_assoc_tables_Blookup dst_positive_assoc_tables_Blookup dst_negative_assoc_tables_Blookup. (((B) = (((((dst_positive_code_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup)) * S ((dst_positive_code_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup)) + ((dst_positive_scale_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup))) + (((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) * S ((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) + ((dst_negative_scale_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)))) * S ((((dst_positive_code_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup)) * S ((dst_positive_code_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup)) + ((dst_positive_scale_assoc_tables_Blookup) + (dst_positive_scale_assoc_tables_Blookup))) + (((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) * S ((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) + ((dst_negative_scale_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)))) + ((((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) * S ((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) + ((dst_negative_scale_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup))) + (((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) * S ((dst_negative_code_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)) + ((dst_negative_scale_assoc_tables_Blookup) + (dst_negative_scale_assoc_tables_Blookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Blookuppositive. ff_h_pvs_assoc_tables_Blookuppositive + S (dst_positive_assoc_tables_Blookup) = S ((S (dc_input_assoc_tables_B)) * dst_positive_scale_assoc_tables_Blookup)) /\ exists ff_q_pvs_assoc_tables_Blookuppositive. dst_positive_code_assoc_tables_Blookup = ff_q_pvs_assoc_tables_Blookuppositive * S ((S (dc_input_assoc_tables_B)) * dst_positive_scale_assoc_tables_Blookup) + (dst_positive_assoc_tables_Blookup))) /\ (((((exists ff_h_pvs_assoc_tables_Blookupnegative. ff_h_pvs_assoc_tables_Blookupnegative + S (dst_negative_assoc_tables_Blookup) = S ((S (dc_input_assoc_tables_B)) * dst_negative_scale_assoc_tables_Blookup)) /\ exists ff_q_pvs_assoc_tables_Blookupnegative. dst_negative_code_assoc_tables_Blookup = ff_q_pvs_assoc_tables_Blookupnegative * S ((S (dc_input_assoc_tables_B)) * dst_negative_scale_assoc_tables_Blookup) + (dst_negative_assoc_tables_Blookup))) /\ (exists ge_balance_positive_assoc_tables_Blookupvalue ge_balance_negative_assoc_tables_Blookupvalue. (((((dc_output_assoc_tables_B) = 2 * (ge_balance_positive_assoc_tables_Blookupvalue) /\ (ge_balance_negative_assoc_tables_Blookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Blookupvaluedecode. (((dc_output_assoc_tables_B) = 2 * ge_signed_half_assoc_tables_Blookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Blookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Blookupvalue) = S ge_signed_half_assoc_tables_Blookupvaluedecode))) /\ ((dst_positive_assoc_tables_Blookup) + ge_balance_negative_assoc_tables_Blookupvalue = (dst_negative_assoc_tables_Blookup) + ge_balance_positive_assoc_tables_Blookupvalue))))))))) -> (((~((dc_input_assoc_tables_B)=0)) /\ (exists dc_mask_assoc_tables_Bvalue. ((((exists dst_positive_code_assoc_tables_Bvaluemasktable dst_positive_scale_assoc_tables_Bvaluemasktable dst_negative_code_assoc_tables_Bvaluemasktable dst_negative_scale_assoc_tables_Bvaluemasktable. (((dc_mask_assoc_tables_Bvalue) = (((((dst_positive_code_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable)) * S ((dst_positive_code_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable)) + ((dst_positive_scale_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable))) + (((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) * S ((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) + ((dst_negative_scale_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)))) * S ((((dst_positive_code_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable)) * S ((dst_positive_code_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable)) + ((dst_positive_scale_assoc_tables_Bvaluemasktable) + (dst_positive_scale_assoc_tables_Bvaluemasktable))) + (((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) * S ((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) + ((dst_negative_scale_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)))) + ((((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) * S ((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) + ((dst_negative_scale_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable))) + (((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) * S ((dst_negative_code_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)) + ((dst_negative_scale_assoc_tables_Bvaluemasktable) + (dst_negative_scale_assoc_tables_Bvaluemasktable)))))) /\ (forall dst_index_assoc_tables_Bvaluemasktable. (exists pvs_le_gap_assoc_tables_Bvaluemasktabledomain. pvs_le_gap_assoc_tables_Bvaluemasktabledomain + (dst_index_assoc_tables_Bvaluemasktable) = (dc_input_assoc_tables_B)) -> exists dst_positive_assoc_tables_Bvaluemasktable dst_negative_assoc_tables_Bvaluemasktable dst_value_assoc_tables_Bvaluemasktable. ((((exists ff_h_pvs_assoc_tables_Bvaluemasktableentrypositive. ff_h_pvs_assoc_tables_Bvaluemasktableentrypositive + S (dst_positive_assoc_tables_Bvaluemasktable) = S ((S (dst_index_assoc_tables_Bvaluemasktable)) * dst_positive_scale_assoc_tables_Bvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Bvaluemasktableentrypositive. dst_positive_code_assoc_tables_Bvaluemasktable = ff_q_pvs_assoc_tables_Bvaluemasktableentrypositive * S ((S (dst_index_assoc_tables_Bvaluemasktable)) * dst_positive_scale_assoc_tables_Bvaluemasktable) + (dst_positive_assoc_tables_Bvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemasktableentrynegative. ff_h_pvs_assoc_tables_Bvaluemasktableentrynegative + S (dst_negative_assoc_tables_Bvaluemasktable) = S ((S (dst_index_assoc_tables_Bvaluemasktable)) * dst_negative_scale_assoc_tables_Bvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Bvaluemasktableentrynegative. dst_negative_code_assoc_tables_Bvaluemasktable = ff_q_pvs_assoc_tables_Bvaluemasktableentrynegative * S ((S (dst_index_assoc_tables_Bvaluemasktable)) * dst_negative_scale_assoc_tables_Bvaluemasktable) + (dst_negative_assoc_tables_Bvaluemasktable))) /\ (exists ge_balance_positive_assoc_tables_Bvaluemasktableentryvalue ge_balance_negative_assoc_tables_Bvaluemasktableentryvalue. (((((dst_value_assoc_tables_Bvaluemasktable) = 2 * (ge_balance_positive_assoc_tables_Bvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_tables_Bvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemasktableentryvaluedecode. (((dst_value_assoc_tables_Bvaluemasktable) = 2 * ge_signed_half_assoc_tables_Bvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Bvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Bvaluemasktableentryvalue) = S ge_signed_half_assoc_tables_Bvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Bvaluemasktable) + ge_balance_negative_assoc_tables_Bvaluemasktableentryvalue = (dst_negative_assoc_tables_Bvaluemasktable) + ge_balance_positive_assoc_tables_Bvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_tables_Bvaluemask dc_value_assoc_tables_Bvaluemask. (exists pvs_le_gap_assoc_tables_Bvaluemaskdomain. pvs_le_gap_assoc_tables_Bvaluemaskdomain + (dc_index_assoc_tables_Bvaluemask) = (dc_input_assoc_tables_B)) -> (exists dst_positive_code_assoc_tables_Bvaluemasklookup dst_positive_scale_assoc_tables_Bvaluemasklookup dst_negative_code_assoc_tables_Bvaluemasklookup dst_negative_scale_assoc_tables_Bvaluemasklookup dst_positive_assoc_tables_Bvaluemasklookup dst_negative_assoc_tables_Bvaluemasklookup. (((dc_mask_assoc_tables_Bvalue) = (((((dst_positive_code_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup))) + (((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)))) * S ((((dst_positive_code_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Bvaluemasklookup) + (dst_positive_scale_assoc_tables_Bvaluemasklookup))) + (((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)))) + ((((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup))) + (((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Bvaluemasklookup) + (dst_negative_scale_assoc_tables_Bvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemasklookuppositive. ff_h_pvs_assoc_tables_Bvaluemasklookuppositive + S (dst_positive_assoc_tables_Bvaluemasklookup) = S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_positive_scale_assoc_tables_Bvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Bvaluemasklookuppositive. dst_positive_code_assoc_tables_Bvaluemasklookup = ff_q_pvs_assoc_tables_Bvaluemasklookuppositive * S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_positive_scale_assoc_tables_Bvaluemasklookup) + (dst_positive_assoc_tables_Bvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemasklookupnegative. ff_h_pvs_assoc_tables_Bvaluemasklookupnegative + S (dst_negative_assoc_tables_Bvaluemasklookup) = S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_negative_scale_assoc_tables_Bvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Bvaluemasklookupnegative. dst_negative_code_assoc_tables_Bvaluemasklookup = ff_q_pvs_assoc_tables_Bvaluemasklookupnegative * S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_negative_scale_assoc_tables_Bvaluemasklookup) + (dst_negative_assoc_tables_Bvaluemasklookup))) /\ (exists ge_balance_positive_assoc_tables_Bvaluemasklookupvalue ge_balance_negative_assoc_tables_Bvaluemasklookupvalue. (((((dc_value_assoc_tables_Bvaluemask) = 2 * (ge_balance_positive_assoc_tables_Bvaluemasklookupvalue) /\ (ge_balance_negative_assoc_tables_Bvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemasklookupvaluedecode. (((dc_value_assoc_tables_Bvaluemask) = 2 * ge_signed_half_assoc_tables_Bvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Bvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Bvaluemasklookupvalue) = S ge_signed_half_assoc_tables_Bvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_tables_Bvaluemasklookup) + ge_balance_negative_assoc_tables_Bvaluemasklookupvalue = (dst_negative_assoc_tables_Bvaluemasklookup) + ge_balance_positive_assoc_tables_Bvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_tables_Bvaluemask)=0)) /\ (exists dc_quotient_assoc_tables_Bvaluemaskentry dc_left_assoc_tables_Bvaluemaskentry dc_right_assoc_tables_Bvaluemaskentry. (((dc_input_assoc_tables_B)=(dc_index_assoc_tables_Bvaluemask)*dc_quotient_assoc_tables_Bvaluemaskentry) /\ (((exists dst_positive_code_assoc_tables_Bvaluemaskentryleft dst_positive_scale_assoc_tables_Bvaluemaskentryleft dst_negative_code_assoc_tables_Bvaluemaskentryleft dst_negative_scale_assoc_tables_Bvaluemaskentryleft dst_positive_assoc_tables_Bvaluemaskentryleft dst_negative_assoc_tables_Bvaluemaskentryleft. (((G) = (((((dst_positive_code_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Bvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)))) + ((((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Bvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemaskentryleftpositive. ff_h_pvs_assoc_tables_Bvaluemaskentryleftpositive + S (dst_positive_assoc_tables_Bvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_positive_scale_assoc_tables_Bvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Bvaluemaskentryleftpositive. dst_positive_code_assoc_tables_Bvaluemaskentryleft = ff_q_pvs_assoc_tables_Bvaluemaskentryleftpositive * S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_positive_scale_assoc_tables_Bvaluemaskentryleft) + (dst_positive_assoc_tables_Bvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemaskentryleftnegative. ff_h_pvs_assoc_tables_Bvaluemaskentryleftnegative + S (dst_negative_assoc_tables_Bvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_negative_scale_assoc_tables_Bvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Bvaluemaskentryleftnegative. dst_negative_code_assoc_tables_Bvaluemaskentryleft = ff_q_pvs_assoc_tables_Bvaluemaskentryleftnegative * S ((S (dc_index_assoc_tables_Bvaluemask)) * dst_negative_scale_assoc_tables_Bvaluemaskentryleft) + (dst_negative_assoc_tables_Bvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_tables_Bvaluemaskentryleftvalue ge_balance_negative_assoc_tables_Bvaluemaskentryleftvalue. (((((dc_left_assoc_tables_Bvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Bvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_tables_Bvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemaskentryleftvaluedecode. (((dc_left_assoc_tables_Bvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Bvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Bvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_tables_Bvaluemaskentryleftvalue) = S ge_signed_half_assoc_tables_Bvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_tables_Bvaluemaskentryleft) + ge_balance_negative_assoc_tables_Bvaluemaskentryleftvalue = (dst_negative_assoc_tables_Bvaluemaskentryleft) + ge_balance_positive_assoc_tables_Bvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Bvaluemaskentryright dst_positive_scale_assoc_tables_Bvaluemaskentryright dst_negative_code_assoc_tables_Bvaluemaskentryright dst_negative_scale_assoc_tables_Bvaluemaskentryright dst_positive_assoc_tables_Bvaluemaskentryright dst_negative_assoc_tables_Bvaluemaskentryright. (((H) = (((((dst_positive_code_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)))) * S ((((dst_positive_code_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Bvaluemaskentryright) + (dst_positive_scale_assoc_tables_Bvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)))) + ((((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Bvaluemaskentryright) + (dst_negative_scale_assoc_tables_Bvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemaskentryrightpositive. ff_h_pvs_assoc_tables_Bvaluemaskentryrightpositive + S (dst_positive_assoc_tables_Bvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Bvaluemaskentry)) * dst_positive_scale_assoc_tables_Bvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Bvaluemaskentryrightpositive. dst_positive_code_assoc_tables_Bvaluemaskentryright = ff_q_pvs_assoc_tables_Bvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_tables_Bvaluemaskentry)) * dst_positive_scale_assoc_tables_Bvaluemaskentryright) + (dst_positive_assoc_tables_Bvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_tables_Bvaluemaskentryrightnegative. ff_h_pvs_assoc_tables_Bvaluemaskentryrightnegative + S (dst_negative_assoc_tables_Bvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Bvaluemaskentry)) * dst_negative_scale_assoc_tables_Bvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Bvaluemaskentryrightnegative. dst_negative_code_assoc_tables_Bvaluemaskentryright = ff_q_pvs_assoc_tables_Bvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_tables_Bvaluemaskentry)) * dst_negative_scale_assoc_tables_Bvaluemaskentryright) + (dst_negative_assoc_tables_Bvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_tables_Bvaluemaskentryrightvalue ge_balance_negative_assoc_tables_Bvaluemaskentryrightvalue. (((((dc_right_assoc_tables_Bvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Bvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_tables_Bvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemaskentryrightvaluedecode. (((dc_right_assoc_tables_Bvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Bvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Bvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_tables_Bvaluemaskentryrightvalue) = S ge_signed_half_assoc_tables_Bvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_tables_Bvaluemaskentryright) + ge_balance_negative_assoc_tables_Bvaluemaskentryrightvalue = (dst_negative_assoc_tables_Bvaluemaskentryright) + ge_balance_positive_assoc_tables_Bvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_tables_Bvaluemaskentryproduct sto_an_assoc_tables_Bvaluemaskentryproduct sto_bp_assoc_tables_Bvaluemaskentryproduct sto_bn_assoc_tables_Bvaluemaskentryproduct sto_cp_assoc_tables_Bvaluemaskentryproduct sto_cn_assoc_tables_Bvaluemaskentryproduct. (((((dc_left_assoc_tables_Bvaluemaskentry) = 2 * (sto_ap_assoc_tables_Bvaluemaskentryproduct) /\ (sto_an_assoc_tables_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemaskentryproductleft. (((dc_left_assoc_tables_Bvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Bvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_tables_Bvaluemaskentryproduct) = 0) /\ (sto_an_assoc_tables_Bvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Bvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_tables_Bvaluemaskentry) = 2 * (sto_bp_assoc_tables_Bvaluemaskentryproduct) /\ (sto_bn_assoc_tables_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemaskentryproductright. (((dc_right_assoc_tables_Bvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Bvaluemaskentryproductright + 1 /\ (sto_bp_assoc_tables_Bvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_tables_Bvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Bvaluemaskentryproductright))) /\ ((((((dc_value_assoc_tables_Bvaluemask) = 2 * (sto_cp_assoc_tables_Bvaluemaskentryproduct) /\ (sto_cn_assoc_tables_Bvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluemaskentryproductoutput. (((dc_value_assoc_tables_Bvaluemask) = 2 * ge_signed_half_assoc_tables_Bvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_tables_Bvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_tables_Bvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Bvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_tables_Bvaluemaskentryproduct * sto_bp_assoc_tables_Bvaluemaskentryproduct + sto_an_assoc_tables_Bvaluemaskentryproduct * sto_bn_assoc_tables_Bvaluemaskentryproduct) + sto_cn_assoc_tables_Bvaluemaskentryproduct = (sto_ap_assoc_tables_Bvaluemaskentryproduct * sto_bn_assoc_tables_Bvaluemaskentryproduct + sto_an_assoc_tables_Bvaluemaskentryproduct * sto_bp_assoc_tables_Bvaluemaskentryproduct) + sto_cp_assoc_tables_Bvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_tables_Bvaluemask)=0 \/ ~(exists pvs_factor_assoc_tables_Bvaluemaskentrynondivisor. (dc_input_assoc_tables_B) = (dc_index_assoc_tables_Bvaluemask) * pvs_factor_assoc_tables_Bvaluemaskentrynondivisor)) /\ ((dc_value_assoc_tables_Bvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_tables_Bvaluefold dst_positive_scale_assoc_tables_Bvaluefold dst_negative_code_assoc_tables_Bvaluefold dst_negative_scale_assoc_tables_Bvaluefold dst_positive_sum_assoc_tables_Bvaluefold dst_negative_sum_assoc_tables_Bvaluefold. (((dc_mask_assoc_tables_Bvalue) = (((((dst_positive_code_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold)) * S ((dst_positive_code_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold)) + ((dst_positive_scale_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold))) + (((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) * S ((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) + ((dst_negative_scale_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)))) * S ((((dst_positive_code_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold)) * S ((dst_positive_code_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold)) + ((dst_positive_scale_assoc_tables_Bvaluefold) + (dst_positive_scale_assoc_tables_Bvaluefold))) + (((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) * S ((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) + ((dst_negative_scale_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)))) + ((((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) * S ((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) + ((dst_negative_scale_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold))) + (((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) * S ((dst_negative_code_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)) + ((dst_negative_scale_assoc_tables_Bvaluefold) + (dst_negative_scale_assoc_tables_Bvaluefold)))))) /\ (((exists fs_u_dst_assoc_tables_Bvaluefoldpositive fs_v_dst_assoc_tables_Bvaluefoldpositive. ((((exists fs_h_dst_assoc_tables_Bvaluefoldpositive_body_start. fs_h_dst_assoc_tables_Bvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldpositive_body_start. fs_u_dst_assoc_tables_Bvaluefoldpositive = fs_q_dst_assoc_tables_Bvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Bvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldpositive_body_terminal. fs_h_dst_assoc_tables_Bvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_tables_Bvaluefold) = S ((S (S (dc_input_assoc_tables_B))) * fs_v_dst_assoc_tables_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldpositive_body_terminal. fs_u_dst_assoc_tables_Bvaluefoldpositive = fs_q_dst_assoc_tables_Bvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_tables_B))) * fs_v_dst_assoc_tables_Bvaluefoldpositive) + (dst_positive_sum_assoc_tables_Bvaluefold))) /\ forall fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_tables_Bvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_tables_Bvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps = S (dc_input_assoc_tables_B)) -> exists fs_a_dst_assoc_tables_Bvaluefoldpositive_body_steps fs_r_dst_assoc_tables_Bvaluefoldpositive_body_steps fs_s_dst_assoc_tables_Bvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_tables_Bvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Bvaluefold)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_tables_Bvaluefold = fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Bvaluefold) + (fs_a_dst_assoc_tables_Bvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_tables_Bvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_tables_Bvaluefoldpositive = fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldpositive) + (fs_r_dst_assoc_tables_Bvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_tables_Bvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_tables_Bvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_tables_Bvaluefoldpositive = fs_q_dst_assoc_tables_Bvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Bvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldpositive) + (fs_s_dst_assoc_tables_Bvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_tables_Bvaluefoldpositive_body_steps = fs_r_dst_assoc_tables_Bvaluefoldpositive_body_steps + fs_a_dst_assoc_tables_Bvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_tables_Bvaluefoldnegative fs_v_dst_assoc_tables_Bvaluefoldnegative. ((((exists fs_h_dst_assoc_tables_Bvaluefoldnegative_body_start. fs_h_dst_assoc_tables_Bvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldnegative_body_start. fs_u_dst_assoc_tables_Bvaluefoldnegative = fs_q_dst_assoc_tables_Bvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Bvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldnegative_body_terminal. fs_h_dst_assoc_tables_Bvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_tables_Bvaluefold) = S ((S (S (dc_input_assoc_tables_B))) * fs_v_dst_assoc_tables_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldnegative_body_terminal. fs_u_dst_assoc_tables_Bvaluefoldnegative = fs_q_dst_assoc_tables_Bvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_tables_B))) * fs_v_dst_assoc_tables_Bvaluefoldnegative) + (dst_negative_sum_assoc_tables_Bvaluefold))) /\ forall fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_tables_Bvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_tables_Bvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps = S (dc_input_assoc_tables_B)) -> exists fs_a_dst_assoc_tables_Bvaluefoldnegative_body_steps fs_r_dst_assoc_tables_Bvaluefoldnegative_body_steps fs_s_dst_assoc_tables_Bvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_tables_Bvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Bvaluefold)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_tables_Bvaluefold = fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Bvaluefold) + (fs_a_dst_assoc_tables_Bvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_tables_Bvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_tables_Bvaluefoldnegative = fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldnegative) + (fs_r_dst_assoc_tables_Bvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_tables_Bvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_tables_Bvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_tables_Bvaluefoldnegative = fs_q_dst_assoc_tables_Bvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Bvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Bvaluefoldnegative) + (fs_s_dst_assoc_tables_Bvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_tables_Bvaluefoldnegative_body_steps = fs_r_dst_assoc_tables_Bvaluefoldnegative_body_steps + fs_a_dst_assoc_tables_Bvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_tables_Bvaluefoldresult ge_balance_negative_assoc_tables_Bvaluefoldresult. (((((dc_output_assoc_tables_B) = 2 * (ge_balance_positive_assoc_tables_Bvaluefoldresult) /\ (ge_balance_negative_assoc_tables_Bvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_tables_Bvaluefoldresultdecode. (((dc_output_assoc_tables_B) = 2 * ge_signed_half_assoc_tables_Bvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_tables_Bvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_tables_Bvaluefoldresult) = S ge_signed_half_assoc_tables_Bvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_tables_Bvaluefold) + ge_balance_negative_assoc_tables_Bvaluefoldresult = (dst_negative_sum_assoc_tables_Bvaluefold) + ge_balance_positive_assoc_tables_Bvaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_assoc_tables_Lleft dst_positive_scale_assoc_tables_Lleft dst_negative_code_assoc_tables_Lleft dst_negative_scale_assoc_tables_Lleft. (((A) = (((((dst_positive_code_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft)) * S ((dst_positive_code_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft)) + ((dst_positive_scale_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft))) + (((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) * S ((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) + ((dst_negative_scale_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)))) * S ((((dst_positive_code_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft)) * S ((dst_positive_code_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft)) + ((dst_positive_scale_assoc_tables_Lleft) + (dst_positive_scale_assoc_tables_Lleft))) + (((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) * S ((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) + ((dst_negative_scale_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)))) + ((((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) * S ((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) + ((dst_negative_scale_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft))) + (((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) * S ((dst_negative_code_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)) + ((dst_negative_scale_assoc_tables_Lleft) + (dst_negative_scale_assoc_tables_Lleft)))))) /\ (forall dst_index_assoc_tables_Lleft. (exists pvs_le_gap_assoc_tables_Lleftdomain. pvs_le_gap_assoc_tables_Lleftdomain + (dst_index_assoc_tables_Lleft) = (N)) -> exists dst_positive_assoc_tables_Lleft dst_negative_assoc_tables_Lleft dst_value_assoc_tables_Lleft. ((((exists ff_h_pvs_assoc_tables_Lleftentrypositive. ff_h_pvs_assoc_tables_Lleftentrypositive + S (dst_positive_assoc_tables_Lleft) = S ((S (dst_index_assoc_tables_Lleft)) * dst_positive_scale_assoc_tables_Lleft)) /\ exists ff_q_pvs_assoc_tables_Lleftentrypositive. dst_positive_code_assoc_tables_Lleft = ff_q_pvs_assoc_tables_Lleftentrypositive * S ((S (dst_index_assoc_tables_Lleft)) * dst_positive_scale_assoc_tables_Lleft) + (dst_positive_assoc_tables_Lleft))) /\ (((((exists ff_h_pvs_assoc_tables_Lleftentrynegative. ff_h_pvs_assoc_tables_Lleftentrynegative + S (dst_negative_assoc_tables_Lleft) = S ((S (dst_index_assoc_tables_Lleft)) * dst_negative_scale_assoc_tables_Lleft)) /\ exists ff_q_pvs_assoc_tables_Lleftentrynegative. dst_negative_code_assoc_tables_Lleft = ff_q_pvs_assoc_tables_Lleftentrynegative * S ((S (dst_index_assoc_tables_Lleft)) * dst_negative_scale_assoc_tables_Lleft) + (dst_negative_assoc_tables_Lleft))) /\ (exists ge_balance_positive_assoc_tables_Lleftentryvalue ge_balance_negative_assoc_tables_Lleftentryvalue. (((((dst_value_assoc_tables_Lleft) = 2 * (ge_balance_positive_assoc_tables_Lleftentryvalue) /\ (ge_balance_negative_assoc_tables_Lleftentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lleftentryvaluedecode. (((dst_value_assoc_tables_Lleft) = 2 * ge_signed_half_assoc_tables_Lleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lleftentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lleftentryvalue) = S ge_signed_half_assoc_tables_Lleftentryvaluedecode))) /\ ((dst_positive_assoc_tables_Lleft) + ge_balance_negative_assoc_tables_Lleftentryvalue = (dst_negative_assoc_tables_Lleft) + ge_balance_positive_assoc_tables_Lleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Lright dst_positive_scale_assoc_tables_Lright dst_negative_code_assoc_tables_Lright dst_negative_scale_assoc_tables_Lright. (((H) = (((((dst_positive_code_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright)) * S ((dst_positive_code_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright)) + ((dst_positive_scale_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright))) + (((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) * S ((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) + ((dst_negative_scale_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)))) * S ((((dst_positive_code_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright)) * S ((dst_positive_code_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright)) + ((dst_positive_scale_assoc_tables_Lright) + (dst_positive_scale_assoc_tables_Lright))) + (((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) * S ((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) + ((dst_negative_scale_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)))) + ((((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) * S ((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) + ((dst_negative_scale_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright))) + (((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) * S ((dst_negative_code_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)) + ((dst_negative_scale_assoc_tables_Lright) + (dst_negative_scale_assoc_tables_Lright)))))) /\ (forall dst_index_assoc_tables_Lright. (exists pvs_le_gap_assoc_tables_Lrightdomain. pvs_le_gap_assoc_tables_Lrightdomain + (dst_index_assoc_tables_Lright) = (N)) -> exists dst_positive_assoc_tables_Lright dst_negative_assoc_tables_Lright dst_value_assoc_tables_Lright. ((((exists ff_h_pvs_assoc_tables_Lrightentrypositive. ff_h_pvs_assoc_tables_Lrightentrypositive + S (dst_positive_assoc_tables_Lright) = S ((S (dst_index_assoc_tables_Lright)) * dst_positive_scale_assoc_tables_Lright)) /\ exists ff_q_pvs_assoc_tables_Lrightentrypositive. dst_positive_code_assoc_tables_Lright = ff_q_pvs_assoc_tables_Lrightentrypositive * S ((S (dst_index_assoc_tables_Lright)) * dst_positive_scale_assoc_tables_Lright) + (dst_positive_assoc_tables_Lright))) /\ (((((exists ff_h_pvs_assoc_tables_Lrightentrynegative. ff_h_pvs_assoc_tables_Lrightentrynegative + S (dst_negative_assoc_tables_Lright) = S ((S (dst_index_assoc_tables_Lright)) * dst_negative_scale_assoc_tables_Lright)) /\ exists ff_q_pvs_assoc_tables_Lrightentrynegative. dst_negative_code_assoc_tables_Lright = ff_q_pvs_assoc_tables_Lrightentrynegative * S ((S (dst_index_assoc_tables_Lright)) * dst_negative_scale_assoc_tables_Lright) + (dst_negative_assoc_tables_Lright))) /\ (exists ge_balance_positive_assoc_tables_Lrightentryvalue ge_balance_negative_assoc_tables_Lrightentryvalue. (((((dst_value_assoc_tables_Lright) = 2 * (ge_balance_positive_assoc_tables_Lrightentryvalue) /\ (ge_balance_negative_assoc_tables_Lrightentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lrightentryvaluedecode. (((dst_value_assoc_tables_Lright) = 2 * ge_signed_half_assoc_tables_Lrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lrightentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lrightentryvalue) = S ge_signed_half_assoc_tables_Lrightentryvaluedecode))) /\ ((dst_positive_assoc_tables_Lright) + ge_balance_negative_assoc_tables_Lrightentryvalue = (dst_negative_assoc_tables_Lright) + ge_balance_positive_assoc_tables_Lrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Ltable dst_positive_scale_assoc_tables_Ltable dst_negative_code_assoc_tables_Ltable dst_negative_scale_assoc_tables_Ltable. (((L) = (((((dst_positive_code_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable)) * S ((dst_positive_code_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable)) + ((dst_positive_scale_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable))) + (((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) * S ((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) + ((dst_negative_scale_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)))) * S ((((dst_positive_code_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable)) * S ((dst_positive_code_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable)) + ((dst_positive_scale_assoc_tables_Ltable) + (dst_positive_scale_assoc_tables_Ltable))) + (((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) * S ((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) + ((dst_negative_scale_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)))) + ((((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) * S ((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) + ((dst_negative_scale_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable))) + (((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) * S ((dst_negative_code_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)) + ((dst_negative_scale_assoc_tables_Ltable) + (dst_negative_scale_assoc_tables_Ltable)))))) /\ (forall dst_index_assoc_tables_Ltable. (exists pvs_le_gap_assoc_tables_Ltabledomain. pvs_le_gap_assoc_tables_Ltabledomain + (dst_index_assoc_tables_Ltable) = (N)) -> exists dst_positive_assoc_tables_Ltable dst_negative_assoc_tables_Ltable dst_value_assoc_tables_Ltable. ((((exists ff_h_pvs_assoc_tables_Ltableentrypositive. ff_h_pvs_assoc_tables_Ltableentrypositive + S (dst_positive_assoc_tables_Ltable) = S ((S (dst_index_assoc_tables_Ltable)) * dst_positive_scale_assoc_tables_Ltable)) /\ exists ff_q_pvs_assoc_tables_Ltableentrypositive. dst_positive_code_assoc_tables_Ltable = ff_q_pvs_assoc_tables_Ltableentrypositive * S ((S (dst_index_assoc_tables_Ltable)) * dst_positive_scale_assoc_tables_Ltable) + (dst_positive_assoc_tables_Ltable))) /\ (((((exists ff_h_pvs_assoc_tables_Ltableentrynegative. ff_h_pvs_assoc_tables_Ltableentrynegative + S (dst_negative_assoc_tables_Ltable) = S ((S (dst_index_assoc_tables_Ltable)) * dst_negative_scale_assoc_tables_Ltable)) /\ exists ff_q_pvs_assoc_tables_Ltableentrynegative. dst_negative_code_assoc_tables_Ltable = ff_q_pvs_assoc_tables_Ltableentrynegative * S ((S (dst_index_assoc_tables_Ltable)) * dst_negative_scale_assoc_tables_Ltable) + (dst_negative_assoc_tables_Ltable))) /\ (exists ge_balance_positive_assoc_tables_Ltableentryvalue ge_balance_negative_assoc_tables_Ltableentryvalue. (((((dst_value_assoc_tables_Ltable) = 2 * (ge_balance_positive_assoc_tables_Ltableentryvalue) /\ (ge_balance_negative_assoc_tables_Ltableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Ltableentryvaluedecode. (((dst_value_assoc_tables_Ltable) = 2 * ge_signed_half_assoc_tables_Ltableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Ltableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Ltableentryvalue) = S ge_signed_half_assoc_tables_Ltableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Ltable) + ge_balance_negative_assoc_tables_Ltableentryvalue = (dst_negative_assoc_tables_Ltable) + ge_balance_positive_assoc_tables_Ltableentryvalue))))))))) /\ (forall dc_input_assoc_tables_L dc_output_assoc_tables_L. ~(dc_input_assoc_tables_L=0) -> (exists pvs_le_gap_assoc_tables_Ldomain. pvs_le_gap_assoc_tables_Ldomain + (dc_input_assoc_tables_L) = (N)) -> (exists dst_positive_code_assoc_tables_Llookup dst_positive_scale_assoc_tables_Llookup dst_negative_code_assoc_tables_Llookup dst_negative_scale_assoc_tables_Llookup dst_positive_assoc_tables_Llookup dst_negative_assoc_tables_Llookup. (((L) = (((((dst_positive_code_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup)) * S ((dst_positive_code_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup)) + ((dst_positive_scale_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup))) + (((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) * S ((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) + ((dst_negative_scale_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)))) * S ((((dst_positive_code_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup)) * S ((dst_positive_code_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup)) + ((dst_positive_scale_assoc_tables_Llookup) + (dst_positive_scale_assoc_tables_Llookup))) + (((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) * S ((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) + ((dst_negative_scale_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)))) + ((((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) * S ((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) + ((dst_negative_scale_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup))) + (((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) * S ((dst_negative_code_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)) + ((dst_negative_scale_assoc_tables_Llookup) + (dst_negative_scale_assoc_tables_Llookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Llookuppositive. ff_h_pvs_assoc_tables_Llookuppositive + S (dst_positive_assoc_tables_Llookup) = S ((S (dc_input_assoc_tables_L)) * dst_positive_scale_assoc_tables_Llookup)) /\ exists ff_q_pvs_assoc_tables_Llookuppositive. dst_positive_code_assoc_tables_Llookup = ff_q_pvs_assoc_tables_Llookuppositive * S ((S (dc_input_assoc_tables_L)) * dst_positive_scale_assoc_tables_Llookup) + (dst_positive_assoc_tables_Llookup))) /\ (((((exists ff_h_pvs_assoc_tables_Llookupnegative. ff_h_pvs_assoc_tables_Llookupnegative + S (dst_negative_assoc_tables_Llookup) = S ((S (dc_input_assoc_tables_L)) * dst_negative_scale_assoc_tables_Llookup)) /\ exists ff_q_pvs_assoc_tables_Llookupnegative. dst_negative_code_assoc_tables_Llookup = ff_q_pvs_assoc_tables_Llookupnegative * S ((S (dc_input_assoc_tables_L)) * dst_negative_scale_assoc_tables_Llookup) + (dst_negative_assoc_tables_Llookup))) /\ (exists ge_balance_positive_assoc_tables_Llookupvalue ge_balance_negative_assoc_tables_Llookupvalue. (((((dc_output_assoc_tables_L) = 2 * (ge_balance_positive_assoc_tables_Llookupvalue) /\ (ge_balance_negative_assoc_tables_Llookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Llookupvaluedecode. (((dc_output_assoc_tables_L) = 2 * ge_signed_half_assoc_tables_Llookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Llookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Llookupvalue) = S ge_signed_half_assoc_tables_Llookupvaluedecode))) /\ ((dst_positive_assoc_tables_Llookup) + ge_balance_negative_assoc_tables_Llookupvalue = (dst_negative_assoc_tables_Llookup) + ge_balance_positive_assoc_tables_Llookupvalue))))))))) -> (((~((dc_input_assoc_tables_L)=0)) /\ (exists dc_mask_assoc_tables_Lvalue. ((((exists dst_positive_code_assoc_tables_Lvaluemasktable dst_positive_scale_assoc_tables_Lvaluemasktable dst_negative_code_assoc_tables_Lvaluemasktable dst_negative_scale_assoc_tables_Lvaluemasktable. (((dc_mask_assoc_tables_Lvalue) = (((((dst_positive_code_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable)) * S ((dst_positive_code_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable)) + ((dst_positive_scale_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable))) + (((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) * S ((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) + ((dst_negative_scale_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)))) * S ((((dst_positive_code_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable)) * S ((dst_positive_code_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable)) + ((dst_positive_scale_assoc_tables_Lvaluemasktable) + (dst_positive_scale_assoc_tables_Lvaluemasktable))) + (((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) * S ((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) + ((dst_negative_scale_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)))) + ((((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) * S ((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) + ((dst_negative_scale_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable))) + (((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) * S ((dst_negative_code_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)) + ((dst_negative_scale_assoc_tables_Lvaluemasktable) + (dst_negative_scale_assoc_tables_Lvaluemasktable)))))) /\ (forall dst_index_assoc_tables_Lvaluemasktable. (exists pvs_le_gap_assoc_tables_Lvaluemasktabledomain. pvs_le_gap_assoc_tables_Lvaluemasktabledomain + (dst_index_assoc_tables_Lvaluemasktable) = (dc_input_assoc_tables_L)) -> exists dst_positive_assoc_tables_Lvaluemasktable dst_negative_assoc_tables_Lvaluemasktable dst_value_assoc_tables_Lvaluemasktable. ((((exists ff_h_pvs_assoc_tables_Lvaluemasktableentrypositive. ff_h_pvs_assoc_tables_Lvaluemasktableentrypositive + S (dst_positive_assoc_tables_Lvaluemasktable) = S ((S (dst_index_assoc_tables_Lvaluemasktable)) * dst_positive_scale_assoc_tables_Lvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Lvaluemasktableentrypositive. dst_positive_code_assoc_tables_Lvaluemasktable = ff_q_pvs_assoc_tables_Lvaluemasktableentrypositive * S ((S (dst_index_assoc_tables_Lvaluemasktable)) * dst_positive_scale_assoc_tables_Lvaluemasktable) + (dst_positive_assoc_tables_Lvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemasktableentrynegative. ff_h_pvs_assoc_tables_Lvaluemasktableentrynegative + S (dst_negative_assoc_tables_Lvaluemasktable) = S ((S (dst_index_assoc_tables_Lvaluemasktable)) * dst_negative_scale_assoc_tables_Lvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Lvaluemasktableentrynegative. dst_negative_code_assoc_tables_Lvaluemasktable = ff_q_pvs_assoc_tables_Lvaluemasktableentrynegative * S ((S (dst_index_assoc_tables_Lvaluemasktable)) * dst_negative_scale_assoc_tables_Lvaluemasktable) + (dst_negative_assoc_tables_Lvaluemasktable))) /\ (exists ge_balance_positive_assoc_tables_Lvaluemasktableentryvalue ge_balance_negative_assoc_tables_Lvaluemasktableentryvalue. (((((dst_value_assoc_tables_Lvaluemasktable) = 2 * (ge_balance_positive_assoc_tables_Lvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_tables_Lvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemasktableentryvaluedecode. (((dst_value_assoc_tables_Lvaluemasktable) = 2 * ge_signed_half_assoc_tables_Lvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lvaluemasktableentryvalue) = S ge_signed_half_assoc_tables_Lvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Lvaluemasktable) + ge_balance_negative_assoc_tables_Lvaluemasktableentryvalue = (dst_negative_assoc_tables_Lvaluemasktable) + ge_balance_positive_assoc_tables_Lvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_tables_Lvaluemask dc_value_assoc_tables_Lvaluemask. (exists pvs_le_gap_assoc_tables_Lvaluemaskdomain. pvs_le_gap_assoc_tables_Lvaluemaskdomain + (dc_index_assoc_tables_Lvaluemask) = (dc_input_assoc_tables_L)) -> (exists dst_positive_code_assoc_tables_Lvaluemasklookup dst_positive_scale_assoc_tables_Lvaluemasklookup dst_negative_code_assoc_tables_Lvaluemasklookup dst_negative_scale_assoc_tables_Lvaluemasklookup dst_positive_assoc_tables_Lvaluemasklookup dst_negative_assoc_tables_Lvaluemasklookup. (((dc_mask_assoc_tables_Lvalue) = (((((dst_positive_code_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup))) + (((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)))) * S ((((dst_positive_code_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Lvaluemasklookup) + (dst_positive_scale_assoc_tables_Lvaluemasklookup))) + (((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)))) + ((((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup))) + (((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Lvaluemasklookup) + (dst_negative_scale_assoc_tables_Lvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemasklookuppositive. ff_h_pvs_assoc_tables_Lvaluemasklookuppositive + S (dst_positive_assoc_tables_Lvaluemasklookup) = S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_positive_scale_assoc_tables_Lvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Lvaluemasklookuppositive. dst_positive_code_assoc_tables_Lvaluemasklookup = ff_q_pvs_assoc_tables_Lvaluemasklookuppositive * S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_positive_scale_assoc_tables_Lvaluemasklookup) + (dst_positive_assoc_tables_Lvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemasklookupnegative. ff_h_pvs_assoc_tables_Lvaluemasklookupnegative + S (dst_negative_assoc_tables_Lvaluemasklookup) = S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_negative_scale_assoc_tables_Lvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Lvaluemasklookupnegative. dst_negative_code_assoc_tables_Lvaluemasklookup = ff_q_pvs_assoc_tables_Lvaluemasklookupnegative * S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_negative_scale_assoc_tables_Lvaluemasklookup) + (dst_negative_assoc_tables_Lvaluemasklookup))) /\ (exists ge_balance_positive_assoc_tables_Lvaluemasklookupvalue ge_balance_negative_assoc_tables_Lvaluemasklookupvalue. (((((dc_value_assoc_tables_Lvaluemask) = 2 * (ge_balance_positive_assoc_tables_Lvaluemasklookupvalue) /\ (ge_balance_negative_assoc_tables_Lvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemasklookupvaluedecode. (((dc_value_assoc_tables_Lvaluemask) = 2 * ge_signed_half_assoc_tables_Lvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lvaluemasklookupvalue) = S ge_signed_half_assoc_tables_Lvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_tables_Lvaluemasklookup) + ge_balance_negative_assoc_tables_Lvaluemasklookupvalue = (dst_negative_assoc_tables_Lvaluemasklookup) + ge_balance_positive_assoc_tables_Lvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_tables_Lvaluemask)=0)) /\ (exists dc_quotient_assoc_tables_Lvaluemaskentry dc_left_assoc_tables_Lvaluemaskentry dc_right_assoc_tables_Lvaluemaskentry. (((dc_input_assoc_tables_L)=(dc_index_assoc_tables_Lvaluemask)*dc_quotient_assoc_tables_Lvaluemaskentry) /\ (((exists dst_positive_code_assoc_tables_Lvaluemaskentryleft dst_positive_scale_assoc_tables_Lvaluemaskentryleft dst_negative_code_assoc_tables_Lvaluemaskentryleft dst_negative_scale_assoc_tables_Lvaluemaskentryleft dst_positive_assoc_tables_Lvaluemaskentryleft dst_negative_assoc_tables_Lvaluemaskentryleft. (((A) = (((((dst_positive_code_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Lvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)))) + ((((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Lvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemaskentryleftpositive. ff_h_pvs_assoc_tables_Lvaluemaskentryleftpositive + S (dst_positive_assoc_tables_Lvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_positive_scale_assoc_tables_Lvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Lvaluemaskentryleftpositive. dst_positive_code_assoc_tables_Lvaluemaskentryleft = ff_q_pvs_assoc_tables_Lvaluemaskentryleftpositive * S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_positive_scale_assoc_tables_Lvaluemaskentryleft) + (dst_positive_assoc_tables_Lvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemaskentryleftnegative. ff_h_pvs_assoc_tables_Lvaluemaskentryleftnegative + S (dst_negative_assoc_tables_Lvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_negative_scale_assoc_tables_Lvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Lvaluemaskentryleftnegative. dst_negative_code_assoc_tables_Lvaluemaskentryleft = ff_q_pvs_assoc_tables_Lvaluemaskentryleftnegative * S ((S (dc_index_assoc_tables_Lvaluemask)) * dst_negative_scale_assoc_tables_Lvaluemaskentryleft) + (dst_negative_assoc_tables_Lvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_tables_Lvaluemaskentryleftvalue ge_balance_negative_assoc_tables_Lvaluemaskentryleftvalue. (((((dc_left_assoc_tables_Lvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Lvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_tables_Lvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemaskentryleftvaluedecode. (((dc_left_assoc_tables_Lvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Lvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lvaluemaskentryleftvalue) = S ge_signed_half_assoc_tables_Lvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_tables_Lvaluemaskentryleft) + ge_balance_negative_assoc_tables_Lvaluemaskentryleftvalue = (dst_negative_assoc_tables_Lvaluemaskentryleft) + ge_balance_positive_assoc_tables_Lvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Lvaluemaskentryright dst_positive_scale_assoc_tables_Lvaluemaskentryright dst_negative_code_assoc_tables_Lvaluemaskentryright dst_negative_scale_assoc_tables_Lvaluemaskentryright dst_positive_assoc_tables_Lvaluemaskentryright dst_negative_assoc_tables_Lvaluemaskentryright. (((H) = (((((dst_positive_code_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)))) * S ((((dst_positive_code_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Lvaluemaskentryright) + (dst_positive_scale_assoc_tables_Lvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)))) + ((((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Lvaluemaskentryright) + (dst_negative_scale_assoc_tables_Lvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemaskentryrightpositive. ff_h_pvs_assoc_tables_Lvaluemaskentryrightpositive + S (dst_positive_assoc_tables_Lvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Lvaluemaskentry)) * dst_positive_scale_assoc_tables_Lvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Lvaluemaskentryrightpositive. dst_positive_code_assoc_tables_Lvaluemaskentryright = ff_q_pvs_assoc_tables_Lvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_tables_Lvaluemaskentry)) * dst_positive_scale_assoc_tables_Lvaluemaskentryright) + (dst_positive_assoc_tables_Lvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_tables_Lvaluemaskentryrightnegative. ff_h_pvs_assoc_tables_Lvaluemaskentryrightnegative + S (dst_negative_assoc_tables_Lvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Lvaluemaskentry)) * dst_negative_scale_assoc_tables_Lvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Lvaluemaskentryrightnegative. dst_negative_code_assoc_tables_Lvaluemaskentryright = ff_q_pvs_assoc_tables_Lvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_tables_Lvaluemaskentry)) * dst_negative_scale_assoc_tables_Lvaluemaskentryright) + (dst_negative_assoc_tables_Lvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_tables_Lvaluemaskentryrightvalue ge_balance_negative_assoc_tables_Lvaluemaskentryrightvalue. (((((dc_right_assoc_tables_Lvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Lvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_tables_Lvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemaskentryrightvaluedecode. (((dc_right_assoc_tables_Lvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Lvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Lvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_tables_Lvaluemaskentryrightvalue) = S ge_signed_half_assoc_tables_Lvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_tables_Lvaluemaskentryright) + ge_balance_negative_assoc_tables_Lvaluemaskentryrightvalue = (dst_negative_assoc_tables_Lvaluemaskentryright) + ge_balance_positive_assoc_tables_Lvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_tables_Lvaluemaskentryproduct sto_an_assoc_tables_Lvaluemaskentryproduct sto_bp_assoc_tables_Lvaluemaskentryproduct sto_bn_assoc_tables_Lvaluemaskentryproduct sto_cp_assoc_tables_Lvaluemaskentryproduct sto_cn_assoc_tables_Lvaluemaskentryproduct. (((((dc_left_assoc_tables_Lvaluemaskentry) = 2 * (sto_ap_assoc_tables_Lvaluemaskentryproduct) /\ (sto_an_assoc_tables_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemaskentryproductleft. (((dc_left_assoc_tables_Lvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Lvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_tables_Lvaluemaskentryproduct) = 0) /\ (sto_an_assoc_tables_Lvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Lvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_tables_Lvaluemaskentry) = 2 * (sto_bp_assoc_tables_Lvaluemaskentryproduct) /\ (sto_bn_assoc_tables_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemaskentryproductright. (((dc_right_assoc_tables_Lvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Lvaluemaskentryproductright + 1 /\ (sto_bp_assoc_tables_Lvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_tables_Lvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Lvaluemaskentryproductright))) /\ ((((((dc_value_assoc_tables_Lvaluemask) = 2 * (sto_cp_assoc_tables_Lvaluemaskentryproduct) /\ (sto_cn_assoc_tables_Lvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluemaskentryproductoutput. (((dc_value_assoc_tables_Lvaluemask) = 2 * ge_signed_half_assoc_tables_Lvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_tables_Lvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_tables_Lvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Lvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_tables_Lvaluemaskentryproduct * sto_bp_assoc_tables_Lvaluemaskentryproduct + sto_an_assoc_tables_Lvaluemaskentryproduct * sto_bn_assoc_tables_Lvaluemaskentryproduct) + sto_cn_assoc_tables_Lvaluemaskentryproduct = (sto_ap_assoc_tables_Lvaluemaskentryproduct * sto_bn_assoc_tables_Lvaluemaskentryproduct + sto_an_assoc_tables_Lvaluemaskentryproduct * sto_bp_assoc_tables_Lvaluemaskentryproduct) + sto_cp_assoc_tables_Lvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_tables_Lvaluemask)=0 \/ ~(exists pvs_factor_assoc_tables_Lvaluemaskentrynondivisor. (dc_input_assoc_tables_L) = (dc_index_assoc_tables_Lvaluemask) * pvs_factor_assoc_tables_Lvaluemaskentrynondivisor)) /\ ((dc_value_assoc_tables_Lvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_tables_Lvaluefold dst_positive_scale_assoc_tables_Lvaluefold dst_negative_code_assoc_tables_Lvaluefold dst_negative_scale_assoc_tables_Lvaluefold dst_positive_sum_assoc_tables_Lvaluefold dst_negative_sum_assoc_tables_Lvaluefold. (((dc_mask_assoc_tables_Lvalue) = (((((dst_positive_code_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold)) * S ((dst_positive_code_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold)) + ((dst_positive_scale_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold))) + (((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) * S ((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) + ((dst_negative_scale_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)))) * S ((((dst_positive_code_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold)) * S ((dst_positive_code_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold)) + ((dst_positive_scale_assoc_tables_Lvaluefold) + (dst_positive_scale_assoc_tables_Lvaluefold))) + (((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) * S ((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) + ((dst_negative_scale_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)))) + ((((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) * S ((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) + ((dst_negative_scale_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold))) + (((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) * S ((dst_negative_code_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)) + ((dst_negative_scale_assoc_tables_Lvaluefold) + (dst_negative_scale_assoc_tables_Lvaluefold)))))) /\ (((exists fs_u_dst_assoc_tables_Lvaluefoldpositive fs_v_dst_assoc_tables_Lvaluefoldpositive. ((((exists fs_h_dst_assoc_tables_Lvaluefoldpositive_body_start. fs_h_dst_assoc_tables_Lvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldpositive_body_start. fs_u_dst_assoc_tables_Lvaluefoldpositive = fs_q_dst_assoc_tables_Lvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Lvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldpositive_body_terminal. fs_h_dst_assoc_tables_Lvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_tables_Lvaluefold) = S ((S (S (dc_input_assoc_tables_L))) * fs_v_dst_assoc_tables_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldpositive_body_terminal. fs_u_dst_assoc_tables_Lvaluefoldpositive = fs_q_dst_assoc_tables_Lvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_tables_L))) * fs_v_dst_assoc_tables_Lvaluefoldpositive) + (dst_positive_sum_assoc_tables_Lvaluefold))) /\ forall fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_tables_Lvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_tables_Lvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps = S (dc_input_assoc_tables_L)) -> exists fs_a_dst_assoc_tables_Lvaluefoldpositive_body_steps fs_r_dst_assoc_tables_Lvaluefoldpositive_body_steps fs_s_dst_assoc_tables_Lvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_tables_Lvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Lvaluefold)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_tables_Lvaluefold = fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Lvaluefold) + (fs_a_dst_assoc_tables_Lvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_tables_Lvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_tables_Lvaluefoldpositive = fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldpositive) + (fs_r_dst_assoc_tables_Lvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_tables_Lvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_tables_Lvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_tables_Lvaluefoldpositive = fs_q_dst_assoc_tables_Lvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Lvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldpositive) + (fs_s_dst_assoc_tables_Lvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_tables_Lvaluefoldpositive_body_steps = fs_r_dst_assoc_tables_Lvaluefoldpositive_body_steps + fs_a_dst_assoc_tables_Lvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_tables_Lvaluefoldnegative fs_v_dst_assoc_tables_Lvaluefoldnegative. ((((exists fs_h_dst_assoc_tables_Lvaluefoldnegative_body_start. fs_h_dst_assoc_tables_Lvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldnegative_body_start. fs_u_dst_assoc_tables_Lvaluefoldnegative = fs_q_dst_assoc_tables_Lvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Lvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldnegative_body_terminal. fs_h_dst_assoc_tables_Lvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_tables_Lvaluefold) = S ((S (S (dc_input_assoc_tables_L))) * fs_v_dst_assoc_tables_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldnegative_body_terminal. fs_u_dst_assoc_tables_Lvaluefoldnegative = fs_q_dst_assoc_tables_Lvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_tables_L))) * fs_v_dst_assoc_tables_Lvaluefoldnegative) + (dst_negative_sum_assoc_tables_Lvaluefold))) /\ forall fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_tables_Lvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_tables_Lvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps = S (dc_input_assoc_tables_L)) -> exists fs_a_dst_assoc_tables_Lvaluefoldnegative_body_steps fs_r_dst_assoc_tables_Lvaluefoldnegative_body_steps fs_s_dst_assoc_tables_Lvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_tables_Lvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Lvaluefold)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_tables_Lvaluefold = fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Lvaluefold) + (fs_a_dst_assoc_tables_Lvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_tables_Lvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_tables_Lvaluefoldnegative = fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldnegative) + (fs_r_dst_assoc_tables_Lvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_tables_Lvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_tables_Lvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_tables_Lvaluefoldnegative = fs_q_dst_assoc_tables_Lvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Lvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Lvaluefoldnegative) + (fs_s_dst_assoc_tables_Lvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_tables_Lvaluefoldnegative_body_steps = fs_r_dst_assoc_tables_Lvaluefoldnegative_body_steps + fs_a_dst_assoc_tables_Lvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_tables_Lvaluefoldresult ge_balance_negative_assoc_tables_Lvaluefoldresult. (((((dc_output_assoc_tables_L) = 2 * (ge_balance_positive_assoc_tables_Lvaluefoldresult) /\ (ge_balance_negative_assoc_tables_Lvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_tables_Lvaluefoldresultdecode. (((dc_output_assoc_tables_L) = 2 * ge_signed_half_assoc_tables_Lvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_tables_Lvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_tables_Lvaluefoldresult) = S ge_signed_half_assoc_tables_Lvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_tables_Lvaluefold) + ge_balance_negative_assoc_tables_Lvaluefoldresult = (dst_negative_sum_assoc_tables_Lvaluefold) + ge_balance_positive_assoc_tables_Lvaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_assoc_tables_Rleft dst_positive_scale_assoc_tables_Rleft dst_negative_code_assoc_tables_Rleft dst_negative_scale_assoc_tables_Rleft. (((F) = (((((dst_positive_code_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft)) * S ((dst_positive_code_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft)) + ((dst_positive_scale_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft))) + (((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) * S ((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) + ((dst_negative_scale_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)))) * S ((((dst_positive_code_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft)) * S ((dst_positive_code_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft)) + ((dst_positive_scale_assoc_tables_Rleft) + (dst_positive_scale_assoc_tables_Rleft))) + (((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) * S ((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) + ((dst_negative_scale_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)))) + ((((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) * S ((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) + ((dst_negative_scale_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft))) + (((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) * S ((dst_negative_code_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)) + ((dst_negative_scale_assoc_tables_Rleft) + (dst_negative_scale_assoc_tables_Rleft)))))) /\ (forall dst_index_assoc_tables_Rleft. (exists pvs_le_gap_assoc_tables_Rleftdomain. pvs_le_gap_assoc_tables_Rleftdomain + (dst_index_assoc_tables_Rleft) = (N)) -> exists dst_positive_assoc_tables_Rleft dst_negative_assoc_tables_Rleft dst_value_assoc_tables_Rleft. ((((exists ff_h_pvs_assoc_tables_Rleftentrypositive. ff_h_pvs_assoc_tables_Rleftentrypositive + S (dst_positive_assoc_tables_Rleft) = S ((S (dst_index_assoc_tables_Rleft)) * dst_positive_scale_assoc_tables_Rleft)) /\ exists ff_q_pvs_assoc_tables_Rleftentrypositive. dst_positive_code_assoc_tables_Rleft = ff_q_pvs_assoc_tables_Rleftentrypositive * S ((S (dst_index_assoc_tables_Rleft)) * dst_positive_scale_assoc_tables_Rleft) + (dst_positive_assoc_tables_Rleft))) /\ (((((exists ff_h_pvs_assoc_tables_Rleftentrynegative. ff_h_pvs_assoc_tables_Rleftentrynegative + S (dst_negative_assoc_tables_Rleft) = S ((S (dst_index_assoc_tables_Rleft)) * dst_negative_scale_assoc_tables_Rleft)) /\ exists ff_q_pvs_assoc_tables_Rleftentrynegative. dst_negative_code_assoc_tables_Rleft = ff_q_pvs_assoc_tables_Rleftentrynegative * S ((S (dst_index_assoc_tables_Rleft)) * dst_negative_scale_assoc_tables_Rleft) + (dst_negative_assoc_tables_Rleft))) /\ (exists ge_balance_positive_assoc_tables_Rleftentryvalue ge_balance_negative_assoc_tables_Rleftentryvalue. (((((dst_value_assoc_tables_Rleft) = 2 * (ge_balance_positive_assoc_tables_Rleftentryvalue) /\ (ge_balance_negative_assoc_tables_Rleftentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rleftentryvaluedecode. (((dst_value_assoc_tables_Rleft) = 2 * ge_signed_half_assoc_tables_Rleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rleftentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rleftentryvalue) = S ge_signed_half_assoc_tables_Rleftentryvaluedecode))) /\ ((dst_positive_assoc_tables_Rleft) + ge_balance_negative_assoc_tables_Rleftentryvalue = (dst_negative_assoc_tables_Rleft) + ge_balance_positive_assoc_tables_Rleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Rright dst_positive_scale_assoc_tables_Rright dst_negative_code_assoc_tables_Rright dst_negative_scale_assoc_tables_Rright. (((B) = (((((dst_positive_code_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright)) * S ((dst_positive_code_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright)) + ((dst_positive_scale_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright))) + (((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) * S ((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) + ((dst_negative_scale_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)))) * S ((((dst_positive_code_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright)) * S ((dst_positive_code_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright)) + ((dst_positive_scale_assoc_tables_Rright) + (dst_positive_scale_assoc_tables_Rright))) + (((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) * S ((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) + ((dst_negative_scale_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)))) + ((((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) * S ((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) + ((dst_negative_scale_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright))) + (((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) * S ((dst_negative_code_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)) + ((dst_negative_scale_assoc_tables_Rright) + (dst_negative_scale_assoc_tables_Rright)))))) /\ (forall dst_index_assoc_tables_Rright. (exists pvs_le_gap_assoc_tables_Rrightdomain. pvs_le_gap_assoc_tables_Rrightdomain + (dst_index_assoc_tables_Rright) = (N)) -> exists dst_positive_assoc_tables_Rright dst_negative_assoc_tables_Rright dst_value_assoc_tables_Rright. ((((exists ff_h_pvs_assoc_tables_Rrightentrypositive. ff_h_pvs_assoc_tables_Rrightentrypositive + S (dst_positive_assoc_tables_Rright) = S ((S (dst_index_assoc_tables_Rright)) * dst_positive_scale_assoc_tables_Rright)) /\ exists ff_q_pvs_assoc_tables_Rrightentrypositive. dst_positive_code_assoc_tables_Rright = ff_q_pvs_assoc_tables_Rrightentrypositive * S ((S (dst_index_assoc_tables_Rright)) * dst_positive_scale_assoc_tables_Rright) + (dst_positive_assoc_tables_Rright))) /\ (((((exists ff_h_pvs_assoc_tables_Rrightentrynegative. ff_h_pvs_assoc_tables_Rrightentrynegative + S (dst_negative_assoc_tables_Rright) = S ((S (dst_index_assoc_tables_Rright)) * dst_negative_scale_assoc_tables_Rright)) /\ exists ff_q_pvs_assoc_tables_Rrightentrynegative. dst_negative_code_assoc_tables_Rright = ff_q_pvs_assoc_tables_Rrightentrynegative * S ((S (dst_index_assoc_tables_Rright)) * dst_negative_scale_assoc_tables_Rright) + (dst_negative_assoc_tables_Rright))) /\ (exists ge_balance_positive_assoc_tables_Rrightentryvalue ge_balance_negative_assoc_tables_Rrightentryvalue. (((((dst_value_assoc_tables_Rright) = 2 * (ge_balance_positive_assoc_tables_Rrightentryvalue) /\ (ge_balance_negative_assoc_tables_Rrightentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rrightentryvaluedecode. (((dst_value_assoc_tables_Rright) = 2 * ge_signed_half_assoc_tables_Rrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rrightentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rrightentryvalue) = S ge_signed_half_assoc_tables_Rrightentryvaluedecode))) /\ ((dst_positive_assoc_tables_Rright) + ge_balance_negative_assoc_tables_Rrightentryvalue = (dst_negative_assoc_tables_Rright) + ge_balance_positive_assoc_tables_Rrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Rtable dst_positive_scale_assoc_tables_Rtable dst_negative_code_assoc_tables_Rtable dst_negative_scale_assoc_tables_Rtable. (((R) = (((((dst_positive_code_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable)) * S ((dst_positive_code_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable)) + ((dst_positive_scale_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable))) + (((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) * S ((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) + ((dst_negative_scale_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)))) * S ((((dst_positive_code_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable)) * S ((dst_positive_code_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable)) + ((dst_positive_scale_assoc_tables_Rtable) + (dst_positive_scale_assoc_tables_Rtable))) + (((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) * S ((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) + ((dst_negative_scale_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)))) + ((((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) * S ((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) + ((dst_negative_scale_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable))) + (((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) * S ((dst_negative_code_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)) + ((dst_negative_scale_assoc_tables_Rtable) + (dst_negative_scale_assoc_tables_Rtable)))))) /\ (forall dst_index_assoc_tables_Rtable. (exists pvs_le_gap_assoc_tables_Rtabledomain. pvs_le_gap_assoc_tables_Rtabledomain + (dst_index_assoc_tables_Rtable) = (N)) -> exists dst_positive_assoc_tables_Rtable dst_negative_assoc_tables_Rtable dst_value_assoc_tables_Rtable. ((((exists ff_h_pvs_assoc_tables_Rtableentrypositive. ff_h_pvs_assoc_tables_Rtableentrypositive + S (dst_positive_assoc_tables_Rtable) = S ((S (dst_index_assoc_tables_Rtable)) * dst_positive_scale_assoc_tables_Rtable)) /\ exists ff_q_pvs_assoc_tables_Rtableentrypositive. dst_positive_code_assoc_tables_Rtable = ff_q_pvs_assoc_tables_Rtableentrypositive * S ((S (dst_index_assoc_tables_Rtable)) * dst_positive_scale_assoc_tables_Rtable) + (dst_positive_assoc_tables_Rtable))) /\ (((((exists ff_h_pvs_assoc_tables_Rtableentrynegative. ff_h_pvs_assoc_tables_Rtableentrynegative + S (dst_negative_assoc_tables_Rtable) = S ((S (dst_index_assoc_tables_Rtable)) * dst_negative_scale_assoc_tables_Rtable)) /\ exists ff_q_pvs_assoc_tables_Rtableentrynegative. dst_negative_code_assoc_tables_Rtable = ff_q_pvs_assoc_tables_Rtableentrynegative * S ((S (dst_index_assoc_tables_Rtable)) * dst_negative_scale_assoc_tables_Rtable) + (dst_negative_assoc_tables_Rtable))) /\ (exists ge_balance_positive_assoc_tables_Rtableentryvalue ge_balance_negative_assoc_tables_Rtableentryvalue. (((((dst_value_assoc_tables_Rtable) = 2 * (ge_balance_positive_assoc_tables_Rtableentryvalue) /\ (ge_balance_negative_assoc_tables_Rtableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rtableentryvaluedecode. (((dst_value_assoc_tables_Rtable) = 2 * ge_signed_half_assoc_tables_Rtableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rtableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rtableentryvalue) = S ge_signed_half_assoc_tables_Rtableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Rtable) + ge_balance_negative_assoc_tables_Rtableentryvalue = (dst_negative_assoc_tables_Rtable) + ge_balance_positive_assoc_tables_Rtableentryvalue))))))))) /\ (forall dc_input_assoc_tables_R dc_output_assoc_tables_R. ~(dc_input_assoc_tables_R=0) -> (exists pvs_le_gap_assoc_tables_Rdomain. pvs_le_gap_assoc_tables_Rdomain + (dc_input_assoc_tables_R) = (N)) -> (exists dst_positive_code_assoc_tables_Rlookup dst_positive_scale_assoc_tables_Rlookup dst_negative_code_assoc_tables_Rlookup dst_negative_scale_assoc_tables_Rlookup dst_positive_assoc_tables_Rlookup dst_negative_assoc_tables_Rlookup. (((R) = (((((dst_positive_code_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup)) * S ((dst_positive_code_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup)) + ((dst_positive_scale_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup))) + (((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) * S ((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) + ((dst_negative_scale_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)))) * S ((((dst_positive_code_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup)) * S ((dst_positive_code_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup)) + ((dst_positive_scale_assoc_tables_Rlookup) + (dst_positive_scale_assoc_tables_Rlookup))) + (((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) * S ((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) + ((dst_negative_scale_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)))) + ((((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) * S ((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) + ((dst_negative_scale_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup))) + (((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) * S ((dst_negative_code_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)) + ((dst_negative_scale_assoc_tables_Rlookup) + (dst_negative_scale_assoc_tables_Rlookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Rlookuppositive. ff_h_pvs_assoc_tables_Rlookuppositive + S (dst_positive_assoc_tables_Rlookup) = S ((S (dc_input_assoc_tables_R)) * dst_positive_scale_assoc_tables_Rlookup)) /\ exists ff_q_pvs_assoc_tables_Rlookuppositive. dst_positive_code_assoc_tables_Rlookup = ff_q_pvs_assoc_tables_Rlookuppositive * S ((S (dc_input_assoc_tables_R)) * dst_positive_scale_assoc_tables_Rlookup) + (dst_positive_assoc_tables_Rlookup))) /\ (((((exists ff_h_pvs_assoc_tables_Rlookupnegative. ff_h_pvs_assoc_tables_Rlookupnegative + S (dst_negative_assoc_tables_Rlookup) = S ((S (dc_input_assoc_tables_R)) * dst_negative_scale_assoc_tables_Rlookup)) /\ exists ff_q_pvs_assoc_tables_Rlookupnegative. dst_negative_code_assoc_tables_Rlookup = ff_q_pvs_assoc_tables_Rlookupnegative * S ((S (dc_input_assoc_tables_R)) * dst_negative_scale_assoc_tables_Rlookup) + (dst_negative_assoc_tables_Rlookup))) /\ (exists ge_balance_positive_assoc_tables_Rlookupvalue ge_balance_negative_assoc_tables_Rlookupvalue. (((((dc_output_assoc_tables_R) = 2 * (ge_balance_positive_assoc_tables_Rlookupvalue) /\ (ge_balance_negative_assoc_tables_Rlookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rlookupvaluedecode. (((dc_output_assoc_tables_R) = 2 * ge_signed_half_assoc_tables_Rlookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rlookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rlookupvalue) = S ge_signed_half_assoc_tables_Rlookupvaluedecode))) /\ ((dst_positive_assoc_tables_Rlookup) + ge_balance_negative_assoc_tables_Rlookupvalue = (dst_negative_assoc_tables_Rlookup) + ge_balance_positive_assoc_tables_Rlookupvalue))))))))) -> (((~((dc_input_assoc_tables_R)=0)) /\ (exists dc_mask_assoc_tables_Rvalue. ((((exists dst_positive_code_assoc_tables_Rvaluemasktable dst_positive_scale_assoc_tables_Rvaluemasktable dst_negative_code_assoc_tables_Rvaluemasktable dst_negative_scale_assoc_tables_Rvaluemasktable. (((dc_mask_assoc_tables_Rvalue) = (((((dst_positive_code_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable)) * S ((dst_positive_code_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable)) + ((dst_positive_scale_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable))) + (((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) * S ((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) + ((dst_negative_scale_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)))) * S ((((dst_positive_code_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable)) * S ((dst_positive_code_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable)) + ((dst_positive_scale_assoc_tables_Rvaluemasktable) + (dst_positive_scale_assoc_tables_Rvaluemasktable))) + (((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) * S ((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) + ((dst_negative_scale_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)))) + ((((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) * S ((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) + ((dst_negative_scale_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable))) + (((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) * S ((dst_negative_code_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)) + ((dst_negative_scale_assoc_tables_Rvaluemasktable) + (dst_negative_scale_assoc_tables_Rvaluemasktable)))))) /\ (forall dst_index_assoc_tables_Rvaluemasktable. (exists pvs_le_gap_assoc_tables_Rvaluemasktabledomain. pvs_le_gap_assoc_tables_Rvaluemasktabledomain + (dst_index_assoc_tables_Rvaluemasktable) = (dc_input_assoc_tables_R)) -> exists dst_positive_assoc_tables_Rvaluemasktable dst_negative_assoc_tables_Rvaluemasktable dst_value_assoc_tables_Rvaluemasktable. ((((exists ff_h_pvs_assoc_tables_Rvaluemasktableentrypositive. ff_h_pvs_assoc_tables_Rvaluemasktableentrypositive + S (dst_positive_assoc_tables_Rvaluemasktable) = S ((S (dst_index_assoc_tables_Rvaluemasktable)) * dst_positive_scale_assoc_tables_Rvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Rvaluemasktableentrypositive. dst_positive_code_assoc_tables_Rvaluemasktable = ff_q_pvs_assoc_tables_Rvaluemasktableentrypositive * S ((S (dst_index_assoc_tables_Rvaluemasktable)) * dst_positive_scale_assoc_tables_Rvaluemasktable) + (dst_positive_assoc_tables_Rvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemasktableentrynegative. ff_h_pvs_assoc_tables_Rvaluemasktableentrynegative + S (dst_negative_assoc_tables_Rvaluemasktable) = S ((S (dst_index_assoc_tables_Rvaluemasktable)) * dst_negative_scale_assoc_tables_Rvaluemasktable)) /\ exists ff_q_pvs_assoc_tables_Rvaluemasktableentrynegative. dst_negative_code_assoc_tables_Rvaluemasktable = ff_q_pvs_assoc_tables_Rvaluemasktableentrynegative * S ((S (dst_index_assoc_tables_Rvaluemasktable)) * dst_negative_scale_assoc_tables_Rvaluemasktable) + (dst_negative_assoc_tables_Rvaluemasktable))) /\ (exists ge_balance_positive_assoc_tables_Rvaluemasktableentryvalue ge_balance_negative_assoc_tables_Rvaluemasktableentryvalue. (((((dst_value_assoc_tables_Rvaluemasktable) = 2 * (ge_balance_positive_assoc_tables_Rvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_tables_Rvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemasktableentryvaluedecode. (((dst_value_assoc_tables_Rvaluemasktable) = 2 * ge_signed_half_assoc_tables_Rvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rvaluemasktableentryvalue) = S ge_signed_half_assoc_tables_Rvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_tables_Rvaluemasktable) + ge_balance_negative_assoc_tables_Rvaluemasktableentryvalue = (dst_negative_assoc_tables_Rvaluemasktable) + ge_balance_positive_assoc_tables_Rvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_tables_Rvaluemask dc_value_assoc_tables_Rvaluemask. (exists pvs_le_gap_assoc_tables_Rvaluemaskdomain. pvs_le_gap_assoc_tables_Rvaluemaskdomain + (dc_index_assoc_tables_Rvaluemask) = (dc_input_assoc_tables_R)) -> (exists dst_positive_code_assoc_tables_Rvaluemasklookup dst_positive_scale_assoc_tables_Rvaluemasklookup dst_negative_code_assoc_tables_Rvaluemasklookup dst_negative_scale_assoc_tables_Rvaluemasklookup dst_positive_assoc_tables_Rvaluemasklookup dst_negative_assoc_tables_Rvaluemasklookup. (((dc_mask_assoc_tables_Rvalue) = (((((dst_positive_code_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup))) + (((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)))) * S ((((dst_positive_code_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_positive_code_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup)) + ((dst_positive_scale_assoc_tables_Rvaluemasklookup) + (dst_positive_scale_assoc_tables_Rvaluemasklookup))) + (((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)))) + ((((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup))) + (((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) * S ((dst_negative_code_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)) + ((dst_negative_scale_assoc_tables_Rvaluemasklookup) + (dst_negative_scale_assoc_tables_Rvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemasklookuppositive. ff_h_pvs_assoc_tables_Rvaluemasklookuppositive + S (dst_positive_assoc_tables_Rvaluemasklookup) = S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_positive_scale_assoc_tables_Rvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Rvaluemasklookuppositive. dst_positive_code_assoc_tables_Rvaluemasklookup = ff_q_pvs_assoc_tables_Rvaluemasklookuppositive * S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_positive_scale_assoc_tables_Rvaluemasklookup) + (dst_positive_assoc_tables_Rvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemasklookupnegative. ff_h_pvs_assoc_tables_Rvaluemasklookupnegative + S (dst_negative_assoc_tables_Rvaluemasklookup) = S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_negative_scale_assoc_tables_Rvaluemasklookup)) /\ exists ff_q_pvs_assoc_tables_Rvaluemasklookupnegative. dst_negative_code_assoc_tables_Rvaluemasklookup = ff_q_pvs_assoc_tables_Rvaluemasklookupnegative * S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_negative_scale_assoc_tables_Rvaluemasklookup) + (dst_negative_assoc_tables_Rvaluemasklookup))) /\ (exists ge_balance_positive_assoc_tables_Rvaluemasklookupvalue ge_balance_negative_assoc_tables_Rvaluemasklookupvalue. (((((dc_value_assoc_tables_Rvaluemask) = 2 * (ge_balance_positive_assoc_tables_Rvaluemasklookupvalue) /\ (ge_balance_negative_assoc_tables_Rvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemasklookupvaluedecode. (((dc_value_assoc_tables_Rvaluemask) = 2 * ge_signed_half_assoc_tables_Rvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rvaluemasklookupvalue) = S ge_signed_half_assoc_tables_Rvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_tables_Rvaluemasklookup) + ge_balance_negative_assoc_tables_Rvaluemasklookupvalue = (dst_negative_assoc_tables_Rvaluemasklookup) + ge_balance_positive_assoc_tables_Rvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_tables_Rvaluemask)=0)) /\ (exists dc_quotient_assoc_tables_Rvaluemaskentry dc_left_assoc_tables_Rvaluemaskentry dc_right_assoc_tables_Rvaluemaskentry. (((dc_input_assoc_tables_R)=(dc_index_assoc_tables_Rvaluemask)*dc_quotient_assoc_tables_Rvaluemaskentry) /\ (((exists dst_positive_code_assoc_tables_Rvaluemaskentryleft dst_positive_scale_assoc_tables_Rvaluemaskentryleft dst_negative_code_assoc_tables_Rvaluemaskentryleft dst_negative_scale_assoc_tables_Rvaluemaskentryleft dst_positive_assoc_tables_Rvaluemaskentryleft dst_negative_assoc_tables_Rvaluemaskentryleft. (((F) = (((((dst_positive_code_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_positive_code_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_positive_scale_assoc_tables_Rvaluemaskentryleft) + (dst_positive_scale_assoc_tables_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)))) + ((((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryleft) + (dst_negative_scale_assoc_tables_Rvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemaskentryleftpositive. ff_h_pvs_assoc_tables_Rvaluemaskentryleftpositive + S (dst_positive_assoc_tables_Rvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_positive_scale_assoc_tables_Rvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Rvaluemaskentryleftpositive. dst_positive_code_assoc_tables_Rvaluemaskentryleft = ff_q_pvs_assoc_tables_Rvaluemaskentryleftpositive * S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_positive_scale_assoc_tables_Rvaluemaskentryleft) + (dst_positive_assoc_tables_Rvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemaskentryleftnegative. ff_h_pvs_assoc_tables_Rvaluemaskentryleftnegative + S (dst_negative_assoc_tables_Rvaluemaskentryleft) = S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_negative_scale_assoc_tables_Rvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_tables_Rvaluemaskentryleftnegative. dst_negative_code_assoc_tables_Rvaluemaskentryleft = ff_q_pvs_assoc_tables_Rvaluemaskentryleftnegative * S ((S (dc_index_assoc_tables_Rvaluemask)) * dst_negative_scale_assoc_tables_Rvaluemaskentryleft) + (dst_negative_assoc_tables_Rvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_tables_Rvaluemaskentryleftvalue ge_balance_negative_assoc_tables_Rvaluemaskentryleftvalue. (((((dc_left_assoc_tables_Rvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Rvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_tables_Rvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemaskentryleftvaluedecode. (((dc_left_assoc_tables_Rvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Rvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rvaluemaskentryleftvalue) = S ge_signed_half_assoc_tables_Rvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_tables_Rvaluemaskentryleft) + ge_balance_negative_assoc_tables_Rvaluemaskentryleftvalue = (dst_negative_assoc_tables_Rvaluemaskentryleft) + ge_balance_positive_assoc_tables_Rvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_tables_Rvaluemaskentryright dst_positive_scale_assoc_tables_Rvaluemaskentryright dst_negative_code_assoc_tables_Rvaluemaskentryright dst_negative_scale_assoc_tables_Rvaluemaskentryright dst_positive_assoc_tables_Rvaluemaskentryright dst_negative_assoc_tables_Rvaluemaskentryright. (((B) = (((((dst_positive_code_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)))) * S ((((dst_positive_code_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_positive_code_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_positive_scale_assoc_tables_Rvaluemaskentryright) + (dst_positive_scale_assoc_tables_Rvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)))) + ((((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright))) + (((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) * S ((dst_negative_code_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)) + ((dst_negative_scale_assoc_tables_Rvaluemaskentryright) + (dst_negative_scale_assoc_tables_Rvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemaskentryrightpositive. ff_h_pvs_assoc_tables_Rvaluemaskentryrightpositive + S (dst_positive_assoc_tables_Rvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Rvaluemaskentry)) * dst_positive_scale_assoc_tables_Rvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Rvaluemaskentryrightpositive. dst_positive_code_assoc_tables_Rvaluemaskentryright = ff_q_pvs_assoc_tables_Rvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_tables_Rvaluemaskentry)) * dst_positive_scale_assoc_tables_Rvaluemaskentryright) + (dst_positive_assoc_tables_Rvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_tables_Rvaluemaskentryrightnegative. ff_h_pvs_assoc_tables_Rvaluemaskentryrightnegative + S (dst_negative_assoc_tables_Rvaluemaskentryright) = S ((S (dc_quotient_assoc_tables_Rvaluemaskentry)) * dst_negative_scale_assoc_tables_Rvaluemaskentryright)) /\ exists ff_q_pvs_assoc_tables_Rvaluemaskentryrightnegative. dst_negative_code_assoc_tables_Rvaluemaskentryright = ff_q_pvs_assoc_tables_Rvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_tables_Rvaluemaskentry)) * dst_negative_scale_assoc_tables_Rvaluemaskentryright) + (dst_negative_assoc_tables_Rvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_tables_Rvaluemaskentryrightvalue ge_balance_negative_assoc_tables_Rvaluemaskentryrightvalue. (((((dc_right_assoc_tables_Rvaluemaskentry) = 2 * (ge_balance_positive_assoc_tables_Rvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_tables_Rvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemaskentryrightvaluedecode. (((dc_right_assoc_tables_Rvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Rvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_Rvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_tables_Rvaluemaskentryrightvalue) = S ge_signed_half_assoc_tables_Rvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_tables_Rvaluemaskentryright) + ge_balance_negative_assoc_tables_Rvaluemaskentryrightvalue = (dst_negative_assoc_tables_Rvaluemaskentryright) + ge_balance_positive_assoc_tables_Rvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_tables_Rvaluemaskentryproduct sto_an_assoc_tables_Rvaluemaskentryproduct sto_bp_assoc_tables_Rvaluemaskentryproduct sto_bn_assoc_tables_Rvaluemaskentryproduct sto_cp_assoc_tables_Rvaluemaskentryproduct sto_cn_assoc_tables_Rvaluemaskentryproduct. (((((dc_left_assoc_tables_Rvaluemaskentry) = 2 * (sto_ap_assoc_tables_Rvaluemaskentryproduct) /\ (sto_an_assoc_tables_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemaskentryproductleft. (((dc_left_assoc_tables_Rvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Rvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_tables_Rvaluemaskentryproduct) = 0) /\ (sto_an_assoc_tables_Rvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Rvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_tables_Rvaluemaskentry) = 2 * (sto_bp_assoc_tables_Rvaluemaskentryproduct) /\ (sto_bn_assoc_tables_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemaskentryproductright. (((dc_right_assoc_tables_Rvaluemaskentry) = 2 * ge_signed_half_assoc_tables_Rvaluemaskentryproductright + 1 /\ (sto_bp_assoc_tables_Rvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_tables_Rvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Rvaluemaskentryproductright))) /\ ((((((dc_value_assoc_tables_Rvaluemask) = 2 * (sto_cp_assoc_tables_Rvaluemaskentryproduct) /\ (sto_cn_assoc_tables_Rvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluemaskentryproductoutput. (((dc_value_assoc_tables_Rvaluemask) = 2 * ge_signed_half_assoc_tables_Rvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_tables_Rvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_tables_Rvaluemaskentryproduct) = S ge_signed_half_assoc_tables_Rvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_tables_Rvaluemaskentryproduct * sto_bp_assoc_tables_Rvaluemaskentryproduct + sto_an_assoc_tables_Rvaluemaskentryproduct * sto_bn_assoc_tables_Rvaluemaskentryproduct) + sto_cn_assoc_tables_Rvaluemaskentryproduct = (sto_ap_assoc_tables_Rvaluemaskentryproduct * sto_bn_assoc_tables_Rvaluemaskentryproduct + sto_an_assoc_tables_Rvaluemaskentryproduct * sto_bp_assoc_tables_Rvaluemaskentryproduct) + sto_cp_assoc_tables_Rvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_tables_Rvaluemask)=0 \/ ~(exists pvs_factor_assoc_tables_Rvaluemaskentrynondivisor. (dc_input_assoc_tables_R) = (dc_index_assoc_tables_Rvaluemask) * pvs_factor_assoc_tables_Rvaluemaskentrynondivisor)) /\ ((dc_value_assoc_tables_Rvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_tables_Rvaluefold dst_positive_scale_assoc_tables_Rvaluefold dst_negative_code_assoc_tables_Rvaluefold dst_negative_scale_assoc_tables_Rvaluefold dst_positive_sum_assoc_tables_Rvaluefold dst_negative_sum_assoc_tables_Rvaluefold. (((dc_mask_assoc_tables_Rvalue) = (((((dst_positive_code_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold)) * S ((dst_positive_code_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold)) + ((dst_positive_scale_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold))) + (((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) * S ((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) + ((dst_negative_scale_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)))) * S ((((dst_positive_code_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold)) * S ((dst_positive_code_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold)) + ((dst_positive_scale_assoc_tables_Rvaluefold) + (dst_positive_scale_assoc_tables_Rvaluefold))) + (((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) * S ((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) + ((dst_negative_scale_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)))) + ((((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) * S ((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) + ((dst_negative_scale_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold))) + (((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) * S ((dst_negative_code_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)) + ((dst_negative_scale_assoc_tables_Rvaluefold) + (dst_negative_scale_assoc_tables_Rvaluefold)))))) /\ (((exists fs_u_dst_assoc_tables_Rvaluefoldpositive fs_v_dst_assoc_tables_Rvaluefoldpositive. ((((exists fs_h_dst_assoc_tables_Rvaluefoldpositive_body_start. fs_h_dst_assoc_tables_Rvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldpositive_body_start. fs_u_dst_assoc_tables_Rvaluefoldpositive = fs_q_dst_assoc_tables_Rvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Rvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldpositive_body_terminal. fs_h_dst_assoc_tables_Rvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_tables_Rvaluefold) = S ((S (S (dc_input_assoc_tables_R))) * fs_v_dst_assoc_tables_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldpositive_body_terminal. fs_u_dst_assoc_tables_Rvaluefoldpositive = fs_q_dst_assoc_tables_Rvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_tables_R))) * fs_v_dst_assoc_tables_Rvaluefoldpositive) + (dst_positive_sum_assoc_tables_Rvaluefold))) /\ forall fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_tables_Rvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_tables_Rvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps = S (dc_input_assoc_tables_R)) -> exists fs_a_dst_assoc_tables_Rvaluefoldpositive_body_steps fs_r_dst_assoc_tables_Rvaluefoldpositive_body_steps fs_s_dst_assoc_tables_Rvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_tables_Rvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Rvaluefold)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_tables_Rvaluefold = fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_tables_Rvaluefold) + (fs_a_dst_assoc_tables_Rvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_tables_Rvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_tables_Rvaluefoldpositive = fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldpositive) + (fs_r_dst_assoc_tables_Rvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_tables_Rvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_tables_Rvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldpositive)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_tables_Rvaluefoldpositive = fs_q_dst_assoc_tables_Rvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Rvaluefoldpositive_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldpositive) + (fs_s_dst_assoc_tables_Rvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_tables_Rvaluefoldpositive_body_steps = fs_r_dst_assoc_tables_Rvaluefoldpositive_body_steps + fs_a_dst_assoc_tables_Rvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_tables_Rvaluefoldnegative fs_v_dst_assoc_tables_Rvaluefoldnegative. ((((exists fs_h_dst_assoc_tables_Rvaluefoldnegative_body_start. fs_h_dst_assoc_tables_Rvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_tables_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldnegative_body_start. fs_u_dst_assoc_tables_Rvaluefoldnegative = fs_q_dst_assoc_tables_Rvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_tables_Rvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldnegative_body_terminal. fs_h_dst_assoc_tables_Rvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_tables_Rvaluefold) = S ((S (S (dc_input_assoc_tables_R))) * fs_v_dst_assoc_tables_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldnegative_body_terminal. fs_u_dst_assoc_tables_Rvaluefoldnegative = fs_q_dst_assoc_tables_Rvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_tables_R))) * fs_v_dst_assoc_tables_Rvaluefoldnegative) + (dst_negative_sum_assoc_tables_Rvaluefold))) /\ forall fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_tables_Rvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_tables_Rvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps = S (dc_input_assoc_tables_R)) -> exists fs_a_dst_assoc_tables_Rvaluefoldnegative_body_steps fs_r_dst_assoc_tables_Rvaluefoldnegative_body_steps fs_s_dst_assoc_tables_Rvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_tables_Rvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Rvaluefold)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_tables_Rvaluefold = fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_tables_Rvaluefold) + (fs_a_dst_assoc_tables_Rvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_tables_Rvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_tables_Rvaluefoldnegative = fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldnegative) + (fs_r_dst_assoc_tables_Rvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_tables_Rvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_tables_Rvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldnegative)) /\ exists fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_tables_Rvaluefoldnegative = fs_q_dst_assoc_tables_Rvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_tables_Rvaluefoldnegative_body_steps)) * fs_v_dst_assoc_tables_Rvaluefoldnegative) + (fs_s_dst_assoc_tables_Rvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_tables_Rvaluefoldnegative_body_steps = fs_r_dst_assoc_tables_Rvaluefoldnegative_body_steps + fs_a_dst_assoc_tables_Rvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_tables_Rvaluefoldresult ge_balance_negative_assoc_tables_Rvaluefoldresult. (((((dc_output_assoc_tables_R) = 2 * (ge_balance_positive_assoc_tables_Rvaluefoldresult) /\ (ge_balance_negative_assoc_tables_Rvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_tables_Rvaluefoldresultdecode. (((dc_output_assoc_tables_R) = 2 * ge_signed_half_assoc_tables_Rvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_tables_Rvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_tables_Rvaluefoldresult) = S ge_signed_half_assoc_tables_Rvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_tables_Rvaluefold) + ge_balance_negative_assoc_tables_Rvaluefoldresult = (dst_negative_sum_assoc_tables_Rvaluefold) + ge_balance_positive_assoc_tables_Rvaluefoldresult)))))))))))))))))))) -> (forall dm_index_assoc_tables_equal dm_first_value_assoc_tables_equal dm_second_value_assoc_tables_equal. ~(dm_index_assoc_tables_equal=0) -> (exists pvs_le_gap_assoc_tables_equaldomain. pvs_le_gap_assoc_tables_equaldomain + (dm_index_assoc_tables_equal) = (N)) -> (exists dst_positive_code_assoc_tables_equalfirst dst_positive_scale_assoc_tables_equalfirst dst_negative_code_assoc_tables_equalfirst dst_negative_scale_assoc_tables_equalfirst dst_positive_assoc_tables_equalfirst dst_negative_assoc_tables_equalfirst. (((L) = (((((dst_positive_code_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst)) * S ((dst_positive_code_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst)) + ((dst_positive_scale_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst))) + (((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) * S ((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) + ((dst_negative_scale_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)))) * S ((((dst_positive_code_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst)) * S ((dst_positive_code_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst)) + ((dst_positive_scale_assoc_tables_equalfirst) + (dst_positive_scale_assoc_tables_equalfirst))) + (((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) * S ((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) + ((dst_negative_scale_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)))) + ((((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) * S ((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) + ((dst_negative_scale_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst))) + (((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) * S ((dst_negative_code_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)) + ((dst_negative_scale_assoc_tables_equalfirst) + (dst_negative_scale_assoc_tables_equalfirst)))))) /\ (((((exists ff_h_pvs_assoc_tables_equalfirstpositive. ff_h_pvs_assoc_tables_equalfirstpositive + S (dst_positive_assoc_tables_equalfirst) = S ((S (dm_index_assoc_tables_equal)) * dst_positive_scale_assoc_tables_equalfirst)) /\ exists ff_q_pvs_assoc_tables_equalfirstpositive. dst_positive_code_assoc_tables_equalfirst = ff_q_pvs_assoc_tables_equalfirstpositive * S ((S (dm_index_assoc_tables_equal)) * dst_positive_scale_assoc_tables_equalfirst) + (dst_positive_assoc_tables_equalfirst))) /\ (((((exists ff_h_pvs_assoc_tables_equalfirstnegative. ff_h_pvs_assoc_tables_equalfirstnegative + S (dst_negative_assoc_tables_equalfirst) = S ((S (dm_index_assoc_tables_equal)) * dst_negative_scale_assoc_tables_equalfirst)) /\ exists ff_q_pvs_assoc_tables_equalfirstnegative. dst_negative_code_assoc_tables_equalfirst = ff_q_pvs_assoc_tables_equalfirstnegative * S ((S (dm_index_assoc_tables_equal)) * dst_negative_scale_assoc_tables_equalfirst) + (dst_negative_assoc_tables_equalfirst))) /\ (exists ge_balance_positive_assoc_tables_equalfirstvalue ge_balance_negative_assoc_tables_equalfirstvalue. (((((dm_first_value_assoc_tables_equal) = 2 * (ge_balance_positive_assoc_tables_equalfirstvalue) /\ (ge_balance_negative_assoc_tables_equalfirstvalue) = 0) \/ exists ge_signed_half_assoc_tables_equalfirstvaluedecode. (((dm_first_value_assoc_tables_equal) = 2 * ge_signed_half_assoc_tables_equalfirstvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_equalfirstvalue) = 0) /\ (ge_balance_negative_assoc_tables_equalfirstvalue) = S ge_signed_half_assoc_tables_equalfirstvaluedecode))) /\ ((dst_positive_assoc_tables_equalfirst) + ge_balance_negative_assoc_tables_equalfirstvalue = (dst_negative_assoc_tables_equalfirst) + ge_balance_positive_assoc_tables_equalfirstvalue))))))))) -> (exists dst_positive_code_assoc_tables_equalsecond dst_positive_scale_assoc_tables_equalsecond dst_negative_code_assoc_tables_equalsecond dst_negative_scale_assoc_tables_equalsecond dst_positive_assoc_tables_equalsecond dst_negative_assoc_tables_equalsecond. (((R) = (((((dst_positive_code_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond)) * S ((dst_positive_code_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond)) + ((dst_positive_scale_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond))) + (((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) * S ((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) + ((dst_negative_scale_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)))) * S ((((dst_positive_code_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond)) * S ((dst_positive_code_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond)) + ((dst_positive_scale_assoc_tables_equalsecond) + (dst_positive_scale_assoc_tables_equalsecond))) + (((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) * S ((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) + ((dst_negative_scale_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)))) + ((((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) * S ((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) + ((dst_negative_scale_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond))) + (((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) * S ((dst_negative_code_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)) + ((dst_negative_scale_assoc_tables_equalsecond) + (dst_negative_scale_assoc_tables_equalsecond)))))) /\ (((((exists ff_h_pvs_assoc_tables_equalsecondpositive. ff_h_pvs_assoc_tables_equalsecondpositive + S (dst_positive_assoc_tables_equalsecond) = S ((S (dm_index_assoc_tables_equal)) * dst_positive_scale_assoc_tables_equalsecond)) /\ exists ff_q_pvs_assoc_tables_equalsecondpositive. dst_positive_code_assoc_tables_equalsecond = ff_q_pvs_assoc_tables_equalsecondpositive * S ((S (dm_index_assoc_tables_equal)) * dst_positive_scale_assoc_tables_equalsecond) + (dst_positive_assoc_tables_equalsecond))) /\ (((((exists ff_h_pvs_assoc_tables_equalsecondnegative. ff_h_pvs_assoc_tables_equalsecondnegative + S (dst_negative_assoc_tables_equalsecond) = S ((S (dm_index_assoc_tables_equal)) * dst_negative_scale_assoc_tables_equalsecond)) /\ exists ff_q_pvs_assoc_tables_equalsecondnegative. dst_negative_code_assoc_tables_equalsecond = ff_q_pvs_assoc_tables_equalsecondnegative * S ((S (dm_index_assoc_tables_equal)) * dst_negative_scale_assoc_tables_equalsecond) + (dst_negative_assoc_tables_equalsecond))) /\ (exists ge_balance_positive_assoc_tables_equalsecondvalue ge_balance_negative_assoc_tables_equalsecondvalue. (((((dm_second_value_assoc_tables_equal) = 2 * (ge_balance_positive_assoc_tables_equalsecondvalue) /\ (ge_balance_negative_assoc_tables_equalsecondvalue) = 0) \/ exists ge_signed_half_assoc_tables_equalsecondvaluedecode. (((dm_second_value_assoc_tables_equal) = 2 * ge_signed_half_assoc_tables_equalsecondvaluedecode + 1 /\ (ge_balance_positive_assoc_tables_equalsecondvalue) = 0) /\ (ge_balance_negative_assoc_tables_equalsecondvalue) = S ge_signed_half_assoc_tables_equalsecondvaluedecode))) /\ ((dst_positive_assoc_tables_equalsecond) + ge_balance_negative_assoc_tables_equalsecondvalue = (dst_negative_assoc_tables_equalsecond) + ge_balance_positive_assoc_tables_equalsecondvalue))))))))) -> dm_first_value_assoc_tables_equal=dm_second_value_assoc_tables_equal)