dirichlet_convolution_table_lookup

Exact expanded first-order arithmetic statement

forall N F G H n. (((exists dst_positive_code_table_lookup_sourceleft dst_positive_scale_table_lookup_sourceleft dst_negative_code_table_lookup_sourceleft dst_negative_scale_table_lookup_sourceleft. (((F) = (((((dst_positive_code_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft)) * S ((dst_positive_code_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft)) + ((dst_positive_scale_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft))) + (((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) * S ((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) + ((dst_negative_scale_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)))) * S ((((dst_positive_code_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft)) * S ((dst_positive_code_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft)) + ((dst_positive_scale_table_lookup_sourceleft) + (dst_positive_scale_table_lookup_sourceleft))) + (((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) * S ((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) + ((dst_negative_scale_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)))) + ((((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) * S ((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) + ((dst_negative_scale_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft))) + (((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) * S ((dst_negative_code_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)) + ((dst_negative_scale_table_lookup_sourceleft) + (dst_negative_scale_table_lookup_sourceleft)))))) /\ (forall dst_index_table_lookup_sourceleft. (exists pvs_le_gap_table_lookup_sourceleftdomain. pvs_le_gap_table_lookup_sourceleftdomain + (dst_index_table_lookup_sourceleft) = (N)) -> exists dst_positive_table_lookup_sourceleft dst_negative_table_lookup_sourceleft dst_value_table_lookup_sourceleft. ((((exists ff_h_pvs_table_lookup_sourceleftentrypositive. ff_h_pvs_table_lookup_sourceleftentrypositive + S (dst_positive_table_lookup_sourceleft) = S ((S (dst_index_table_lookup_sourceleft)) * dst_positive_scale_table_lookup_sourceleft)) /\ exists ff_q_pvs_table_lookup_sourceleftentrypositive. dst_positive_code_table_lookup_sourceleft = ff_q_pvs_table_lookup_sourceleftentrypositive * S ((S (dst_index_table_lookup_sourceleft)) * dst_positive_scale_table_lookup_sourceleft) + (dst_positive_table_lookup_sourceleft))) /\ (((((exists ff_h_pvs_table_lookup_sourceleftentrynegative. ff_h_pvs_table_lookup_sourceleftentrynegative + S (dst_negative_table_lookup_sourceleft) = S ((S (dst_index_table_lookup_sourceleft)) * dst_negative_scale_table_lookup_sourceleft)) /\ exists ff_q_pvs_table_lookup_sourceleftentrynegative. dst_negative_code_table_lookup_sourceleft = ff_q_pvs_table_lookup_sourceleftentrynegative * S ((S (dst_index_table_lookup_sourceleft)) * dst_negative_scale_table_lookup_sourceleft) + (dst_negative_table_lookup_sourceleft))) /\ (exists ge_balance_positive_table_lookup_sourceleftentryvalue ge_balance_negative_table_lookup_sourceleftentryvalue. (((((dst_value_table_lookup_sourceleft) = 2 * (ge_balance_positive_table_lookup_sourceleftentryvalue) /\ (ge_balance_negative_table_lookup_sourceleftentryvalue) = 0) \/ exists ge_signed_half_table_lookup_sourceleftentryvaluedecode. (((dst_value_table_lookup_sourceleft) = 2 * ge_signed_half_table_lookup_sourceleftentryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourceleftentryvalue) = 0) /\ (ge_balance_negative_table_lookup_sourceleftentryvalue) = S ge_signed_half_table_lookup_sourceleftentryvaluedecode))) /\ ((dst_positive_table_lookup_sourceleft) + ge_balance_negative_table_lookup_sourceleftentryvalue = (dst_negative_table_lookup_sourceleft) + ge_balance_positive_table_lookup_sourceleftentryvalue))))))))) /\ (((exists dst_positive_code_table_lookup_sourceright dst_positive_scale_table_lookup_sourceright dst_negative_code_table_lookup_sourceright dst_negative_scale_table_lookup_sourceright. (((G) = (((((dst_positive_code_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright)) * S ((dst_positive_code_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright)) + ((dst_positive_scale_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright))) + (((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) * S ((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) + ((dst_negative_scale_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)))) * S ((((dst_positive_code_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright)) * S ((dst_positive_code_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright)) + ((dst_positive_scale_table_lookup_sourceright) + (dst_positive_scale_table_lookup_sourceright))) + (((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) * S ((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) + ((dst_negative_scale_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)))) + ((((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) * S ((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) + ((dst_negative_scale_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright))) + (((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) * S ((dst_negative_code_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)) + ((dst_negative_scale_table_lookup_sourceright) + (dst_negative_scale_table_lookup_sourceright)))))) /\ (forall dst_index_table_lookup_sourceright. (exists pvs_le_gap_table_lookup_sourcerightdomain. pvs_le_gap_table_lookup_sourcerightdomain + (dst_index_table_lookup_sourceright) = (N)) -> exists dst_positive_table_lookup_sourceright dst_negative_table_lookup_sourceright dst_value_table_lookup_sourceright. ((((exists ff_h_pvs_table_lookup_sourcerightentrypositive. ff_h_pvs_table_lookup_sourcerightentrypositive + S (dst_positive_table_lookup_sourceright) = S ((S (dst_index_table_lookup_sourceright)) * dst_positive_scale_table_lookup_sourceright)) /\ exists ff_q_pvs_table_lookup_sourcerightentrypositive. dst_positive_code_table_lookup_sourceright = ff_q_pvs_table_lookup_sourcerightentrypositive * S ((S (dst_index_table_lookup_sourceright)) * dst_positive_scale_table_lookup_sourceright) + (dst_positive_table_lookup_sourceright))) /\ (((((exists ff_h_pvs_table_lookup_sourcerightentrynegative. ff_h_pvs_table_lookup_sourcerightentrynegative + S (dst_negative_table_lookup_sourceright) = S ((S (dst_index_table_lookup_sourceright)) * dst_negative_scale_table_lookup_sourceright)) /\ exists ff_q_pvs_table_lookup_sourcerightentrynegative. dst_negative_code_table_lookup_sourceright = ff_q_pvs_table_lookup_sourcerightentrynegative * S ((S (dst_index_table_lookup_sourceright)) * dst_negative_scale_table_lookup_sourceright) + (dst_negative_table_lookup_sourceright))) /\ (exists ge_balance_positive_table_lookup_sourcerightentryvalue ge_balance_negative_table_lookup_sourcerightentryvalue. (((((dst_value_table_lookup_sourceright) = 2 * (ge_balance_positive_table_lookup_sourcerightentryvalue) /\ (ge_balance_negative_table_lookup_sourcerightentryvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcerightentryvaluedecode. (((dst_value_table_lookup_sourceright) = 2 * ge_signed_half_table_lookup_sourcerightentryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcerightentryvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcerightentryvalue) = S ge_signed_half_table_lookup_sourcerightentryvaluedecode))) /\ ((dst_positive_table_lookup_sourceright) + ge_balance_negative_table_lookup_sourcerightentryvalue = (dst_negative_table_lookup_sourceright) + ge_balance_positive_table_lookup_sourcerightentryvalue))))))))) /\ (((exists dst_positive_code_table_lookup_sourcetable dst_positive_scale_table_lookup_sourcetable dst_negative_code_table_lookup_sourcetable dst_negative_scale_table_lookup_sourcetable. (((H) = (((((dst_positive_code_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable)) * S ((dst_positive_code_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable)) + ((dst_positive_scale_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable))) + (((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) * S ((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) + ((dst_negative_scale_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)))) * S ((((dst_positive_code_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable)) * S ((dst_positive_code_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable)) + ((dst_positive_scale_table_lookup_sourcetable) + (dst_positive_scale_table_lookup_sourcetable))) + (((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) * S ((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) + ((dst_negative_scale_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)))) + ((((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) * S ((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) + ((dst_negative_scale_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable))) + (((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) * S ((dst_negative_code_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)) + ((dst_negative_scale_table_lookup_sourcetable) + (dst_negative_scale_table_lookup_sourcetable)))))) /\ (forall dst_index_table_lookup_sourcetable. (exists pvs_le_gap_table_lookup_sourcetabledomain. pvs_le_gap_table_lookup_sourcetabledomain + (dst_index_table_lookup_sourcetable) = (N)) -> exists dst_positive_table_lookup_sourcetable dst_negative_table_lookup_sourcetable dst_value_table_lookup_sourcetable. ((((exists ff_h_pvs_table_lookup_sourcetableentrypositive. ff_h_pvs_table_lookup_sourcetableentrypositive + S (dst_positive_table_lookup_sourcetable) = S ((S (dst_index_table_lookup_sourcetable)) * dst_positive_scale_table_lookup_sourcetable)) /\ exists ff_q_pvs_table_lookup_sourcetableentrypositive. dst_positive_code_table_lookup_sourcetable = ff_q_pvs_table_lookup_sourcetableentrypositive * S ((S (dst_index_table_lookup_sourcetable)) * dst_positive_scale_table_lookup_sourcetable) + (dst_positive_table_lookup_sourcetable))) /\ (((((exists ff_h_pvs_table_lookup_sourcetableentrynegative. ff_h_pvs_table_lookup_sourcetableentrynegative + S (dst_negative_table_lookup_sourcetable) = S ((S (dst_index_table_lookup_sourcetable)) * dst_negative_scale_table_lookup_sourcetable)) /\ exists ff_q_pvs_table_lookup_sourcetableentrynegative. dst_negative_code_table_lookup_sourcetable = ff_q_pvs_table_lookup_sourcetableentrynegative * S ((S (dst_index_table_lookup_sourcetable)) * dst_negative_scale_table_lookup_sourcetable) + (dst_negative_table_lookup_sourcetable))) /\ (exists ge_balance_positive_table_lookup_sourcetableentryvalue ge_balance_negative_table_lookup_sourcetableentryvalue. (((((dst_value_table_lookup_sourcetable) = 2 * (ge_balance_positive_table_lookup_sourcetableentryvalue) /\ (ge_balance_negative_table_lookup_sourcetableentryvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcetableentryvaluedecode. (((dst_value_table_lookup_sourcetable) = 2 * ge_signed_half_table_lookup_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcetableentryvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcetableentryvalue) = S ge_signed_half_table_lookup_sourcetableentryvaluedecode))) /\ ((dst_positive_table_lookup_sourcetable) + ge_balance_negative_table_lookup_sourcetableentryvalue = (dst_negative_table_lookup_sourcetable) + ge_balance_positive_table_lookup_sourcetableentryvalue))))))))) /\ (forall dc_input_table_lookup_source dc_output_table_lookup_source. ~(dc_input_table_lookup_source=0) -> (exists pvs_le_gap_table_lookup_sourcedomain. pvs_le_gap_table_lookup_sourcedomain + (dc_input_table_lookup_source) = (N)) -> (exists dst_positive_code_table_lookup_sourcelookup dst_positive_scale_table_lookup_sourcelookup dst_negative_code_table_lookup_sourcelookup dst_negative_scale_table_lookup_sourcelookup dst_positive_table_lookup_sourcelookup dst_negative_table_lookup_sourcelookup. (((H) = (((((dst_positive_code_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup)) * S ((dst_positive_code_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup)) + ((dst_positive_scale_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup))) + (((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) * S ((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) + ((dst_negative_scale_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)))) * S ((((dst_positive_code_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup)) * S ((dst_positive_code_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup)) + ((dst_positive_scale_table_lookup_sourcelookup) + (dst_positive_scale_table_lookup_sourcelookup))) + (((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) * S ((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) + ((dst_negative_scale_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)))) + ((((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) * S ((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) + ((dst_negative_scale_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup))) + (((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) * S ((dst_negative_code_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)) + ((dst_negative_scale_table_lookup_sourcelookup) + (dst_negative_scale_table_lookup_sourcelookup)))))) /\ (((((exists ff_h_pvs_table_lookup_sourcelookuppositive. ff_h_pvs_table_lookup_sourcelookuppositive + S (dst_positive_table_lookup_sourcelookup) = S ((S (dc_input_table_lookup_source)) * dst_positive_scale_table_lookup_sourcelookup)) /\ exists ff_q_pvs_table_lookup_sourcelookuppositive. dst_positive_code_table_lookup_sourcelookup = ff_q_pvs_table_lookup_sourcelookuppositive * S ((S (dc_input_table_lookup_source)) * dst_positive_scale_table_lookup_sourcelookup) + (dst_positive_table_lookup_sourcelookup))) /\ (((((exists ff_h_pvs_table_lookup_sourcelookupnegative. ff_h_pvs_table_lookup_sourcelookupnegative + S (dst_negative_table_lookup_sourcelookup) = S ((S (dc_input_table_lookup_source)) * dst_negative_scale_table_lookup_sourcelookup)) /\ exists ff_q_pvs_table_lookup_sourcelookupnegative. dst_negative_code_table_lookup_sourcelookup = ff_q_pvs_table_lookup_sourcelookupnegative * S ((S (dc_input_table_lookup_source)) * dst_negative_scale_table_lookup_sourcelookup) + (dst_negative_table_lookup_sourcelookup))) /\ (exists ge_balance_positive_table_lookup_sourcelookupvalue ge_balance_negative_table_lookup_sourcelookupvalue. (((((dc_output_table_lookup_source) = 2 * (ge_balance_positive_table_lookup_sourcelookupvalue) /\ (ge_balance_negative_table_lookup_sourcelookupvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcelookupvaluedecode. (((dc_output_table_lookup_source) = 2 * ge_signed_half_table_lookup_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcelookupvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcelookupvalue) = S ge_signed_half_table_lookup_sourcelookupvaluedecode))) /\ ((dst_positive_table_lookup_sourcelookup) + ge_balance_negative_table_lookup_sourcelookupvalue = (dst_negative_table_lookup_sourcelookup) + ge_balance_positive_table_lookup_sourcelookupvalue))))))))) -> (((~((dc_input_table_lookup_source)=0)) /\ (exists dc_mask_table_lookup_sourcevalue. ((((exists dst_positive_code_table_lookup_sourcevaluemasktable dst_positive_scale_table_lookup_sourcevaluemasktable dst_negative_code_table_lookup_sourcevaluemasktable dst_negative_scale_table_lookup_sourcevaluemasktable. (((dc_mask_table_lookup_sourcevalue) = (((((dst_positive_code_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable)) * S ((dst_positive_code_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable)) + ((dst_positive_scale_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable))) + (((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) * S ((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) + ((dst_negative_scale_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)))) * S ((((dst_positive_code_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable)) * S ((dst_positive_code_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable)) + ((dst_positive_scale_table_lookup_sourcevaluemasktable) + (dst_positive_scale_table_lookup_sourcevaluemasktable))) + (((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) * S ((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) + ((dst_negative_scale_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)))) + ((((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) * S ((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) + ((dst_negative_scale_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable))) + (((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) * S ((dst_negative_code_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)) + ((dst_negative_scale_table_lookup_sourcevaluemasktable) + (dst_negative_scale_table_lookup_sourcevaluemasktable)))))) /\ (forall dst_index_table_lookup_sourcevaluemasktable. (exists pvs_le_gap_table_lookup_sourcevaluemasktabledomain. pvs_le_gap_table_lookup_sourcevaluemasktabledomain + (dst_index_table_lookup_sourcevaluemasktable) = (dc_input_table_lookup_source)) -> exists dst_positive_table_lookup_sourcevaluemasktable dst_negative_table_lookup_sourcevaluemasktable dst_value_table_lookup_sourcevaluemasktable. ((((exists ff_h_pvs_table_lookup_sourcevaluemasktableentrypositive. ff_h_pvs_table_lookup_sourcevaluemasktableentrypositive + S (dst_positive_table_lookup_sourcevaluemasktable) = S ((S (dst_index_table_lookup_sourcevaluemasktable)) * dst_positive_scale_table_lookup_sourcevaluemasktable)) /\ exists ff_q_pvs_table_lookup_sourcevaluemasktableentrypositive. dst_positive_code_table_lookup_sourcevaluemasktable = ff_q_pvs_table_lookup_sourcevaluemasktableentrypositive * S ((S (dst_index_table_lookup_sourcevaluemasktable)) * dst_positive_scale_table_lookup_sourcevaluemasktable) + (dst_positive_table_lookup_sourcevaluemasktable))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemasktableentrynegative. ff_h_pvs_table_lookup_sourcevaluemasktableentrynegative + S (dst_negative_table_lookup_sourcevaluemasktable) = S ((S (dst_index_table_lookup_sourcevaluemasktable)) * dst_negative_scale_table_lookup_sourcevaluemasktable)) /\ exists ff_q_pvs_table_lookup_sourcevaluemasktableentrynegative. dst_negative_code_table_lookup_sourcevaluemasktable = ff_q_pvs_table_lookup_sourcevaluemasktableentrynegative * S ((S (dst_index_table_lookup_sourcevaluemasktable)) * dst_negative_scale_table_lookup_sourcevaluemasktable) + (dst_negative_table_lookup_sourcevaluemasktable))) /\ (exists ge_balance_positive_table_lookup_sourcevaluemasktableentryvalue ge_balance_negative_table_lookup_sourcevaluemasktableentryvalue. (((((dst_value_table_lookup_sourcevaluemasktable) = 2 * (ge_balance_positive_table_lookup_sourcevaluemasktableentryvalue) /\ (ge_balance_negative_table_lookup_sourcevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemasktableentryvaluedecode. (((dst_value_table_lookup_sourcevaluemasktable) = 2 * ge_signed_half_table_lookup_sourcevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcevaluemasktableentryvalue) = S ge_signed_half_table_lookup_sourcevaluemasktableentryvaluedecode))) /\ ((dst_positive_table_lookup_sourcevaluemasktable) + ge_balance_negative_table_lookup_sourcevaluemasktableentryvalue = (dst_negative_table_lookup_sourcevaluemasktable) + ge_balance_positive_table_lookup_sourcevaluemasktableentryvalue))))))))) /\ (forall dc_index_table_lookup_sourcevaluemask dc_value_table_lookup_sourcevaluemask. (exists pvs_le_gap_table_lookup_sourcevaluemaskdomain. pvs_le_gap_table_lookup_sourcevaluemaskdomain + (dc_index_table_lookup_sourcevaluemask) = (dc_input_table_lookup_source)) -> (exists dst_positive_code_table_lookup_sourcevaluemasklookup dst_positive_scale_table_lookup_sourcevaluemasklookup dst_negative_code_table_lookup_sourcevaluemasklookup dst_negative_scale_table_lookup_sourcevaluemasklookup dst_positive_table_lookup_sourcevaluemasklookup dst_negative_table_lookup_sourcevaluemasklookup. (((dc_mask_table_lookup_sourcevalue) = (((((dst_positive_code_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_positive_code_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup)) + ((dst_positive_scale_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup))) + (((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) + ((dst_negative_scale_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)))) * S ((((dst_positive_code_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_positive_code_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup)) + ((dst_positive_scale_table_lookup_sourcevaluemasklookup) + (dst_positive_scale_table_lookup_sourcevaluemasklookup))) + (((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) + ((dst_negative_scale_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)))) + ((((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) + ((dst_negative_scale_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup))) + (((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) * S ((dst_negative_code_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)) + ((dst_negative_scale_table_lookup_sourcevaluemasklookup) + (dst_negative_scale_table_lookup_sourcevaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemasklookuppositive. ff_h_pvs_table_lookup_sourcevaluemasklookuppositive + S (dst_positive_table_lookup_sourcevaluemasklookup) = S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_positive_scale_table_lookup_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_lookup_sourcevaluemasklookuppositive. dst_positive_code_table_lookup_sourcevaluemasklookup = ff_q_pvs_table_lookup_sourcevaluemasklookuppositive * S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_positive_scale_table_lookup_sourcevaluemasklookup) + (dst_positive_table_lookup_sourcevaluemasklookup))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemasklookupnegative. ff_h_pvs_table_lookup_sourcevaluemasklookupnegative + S (dst_negative_table_lookup_sourcevaluemasklookup) = S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_negative_scale_table_lookup_sourcevaluemasklookup)) /\ exists ff_q_pvs_table_lookup_sourcevaluemasklookupnegative. dst_negative_code_table_lookup_sourcevaluemasklookup = ff_q_pvs_table_lookup_sourcevaluemasklookupnegative * S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_negative_scale_table_lookup_sourcevaluemasklookup) + (dst_negative_table_lookup_sourcevaluemasklookup))) /\ (exists ge_balance_positive_table_lookup_sourcevaluemasklookupvalue ge_balance_negative_table_lookup_sourcevaluemasklookupvalue. (((((dc_value_table_lookup_sourcevaluemask) = 2 * (ge_balance_positive_table_lookup_sourcevaluemasklookupvalue) /\ (ge_balance_negative_table_lookup_sourcevaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemasklookupvaluedecode. (((dc_value_table_lookup_sourcevaluemask) = 2 * ge_signed_half_table_lookup_sourcevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcevaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcevaluemasklookupvalue) = S ge_signed_half_table_lookup_sourcevaluemasklookupvaluedecode))) /\ ((dst_positive_table_lookup_sourcevaluemasklookup) + ge_balance_negative_table_lookup_sourcevaluemasklookupvalue = (dst_negative_table_lookup_sourcevaluemasklookup) + ge_balance_positive_table_lookup_sourcevaluemasklookupvalue))))))))) -> ((((~((dc_index_table_lookup_sourcevaluemask)=0)) /\ (exists dc_quotient_table_lookup_sourcevaluemaskentry dc_left_table_lookup_sourcevaluemaskentry dc_right_table_lookup_sourcevaluemaskentry. (((dc_input_table_lookup_source)=(dc_index_table_lookup_sourcevaluemask)*dc_quotient_table_lookup_sourcevaluemaskentry) /\ (((exists dst_positive_code_table_lookup_sourcevaluemaskentryleft dst_positive_scale_table_lookup_sourcevaluemaskentryleft dst_negative_code_table_lookup_sourcevaluemaskentryleft dst_negative_scale_table_lookup_sourcevaluemaskentryleft dst_positive_table_lookup_sourcevaluemaskentryleft dst_negative_table_lookup_sourcevaluemaskentryleft. (((F) = (((((dst_positive_code_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)))) * S ((((dst_positive_code_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_positive_code_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_positive_scale_table_lookup_sourcevaluemaskentryleft) + (dst_positive_scale_table_lookup_sourcevaluemaskentryleft))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)))) + ((((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryleft) + (dst_negative_scale_table_lookup_sourcevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemaskentryleftpositive. ff_h_pvs_table_lookup_sourcevaluemaskentryleftpositive + S (dst_positive_table_lookup_sourcevaluemaskentryleft) = S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_positive_scale_table_lookup_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_lookup_sourcevaluemaskentryleftpositive. dst_positive_code_table_lookup_sourcevaluemaskentryleft = ff_q_pvs_table_lookup_sourcevaluemaskentryleftpositive * S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_positive_scale_table_lookup_sourcevaluemaskentryleft) + (dst_positive_table_lookup_sourcevaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemaskentryleftnegative. ff_h_pvs_table_lookup_sourcevaluemaskentryleftnegative + S (dst_negative_table_lookup_sourcevaluemaskentryleft) = S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_negative_scale_table_lookup_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_table_lookup_sourcevaluemaskentryleftnegative. dst_negative_code_table_lookup_sourcevaluemaskentryleft = ff_q_pvs_table_lookup_sourcevaluemaskentryleftnegative * S ((S (dc_index_table_lookup_sourcevaluemask)) * dst_negative_scale_table_lookup_sourcevaluemaskentryleft) + (dst_negative_table_lookup_sourcevaluemaskentryleft))) /\ (exists ge_balance_positive_table_lookup_sourcevaluemaskentryleftvalue ge_balance_negative_table_lookup_sourcevaluemaskentryleftvalue. (((((dc_left_table_lookup_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_lookup_sourcevaluemaskentryleftvalue) /\ (ge_balance_negative_table_lookup_sourcevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemaskentryleftvaluedecode. (((dc_left_table_lookup_sourcevaluemaskentry) = 2 * ge_signed_half_table_lookup_sourcevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcevaluemaskentryleftvalue) = S ge_signed_half_table_lookup_sourcevaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_lookup_sourcevaluemaskentryleft) + ge_balance_negative_table_lookup_sourcevaluemaskentryleftvalue = (dst_negative_table_lookup_sourcevaluemaskentryleft) + ge_balance_positive_table_lookup_sourcevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_lookup_sourcevaluemaskentryright dst_positive_scale_table_lookup_sourcevaluemaskentryright dst_negative_code_table_lookup_sourcevaluemaskentryright dst_negative_scale_table_lookup_sourcevaluemaskentryright dst_positive_table_lookup_sourcevaluemaskentryright dst_negative_table_lookup_sourcevaluemaskentryright. (((G) = (((((dst_positive_code_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_positive_code_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_positive_scale_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)))) * S ((((dst_positive_code_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_positive_code_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_positive_scale_table_lookup_sourcevaluemaskentryright) + (dst_positive_scale_table_lookup_sourcevaluemaskentryright))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)))) + ((((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright))) + (((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) * S ((dst_negative_code_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)) + ((dst_negative_scale_table_lookup_sourcevaluemaskentryright) + (dst_negative_scale_table_lookup_sourcevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemaskentryrightpositive. ff_h_pvs_table_lookup_sourcevaluemaskentryrightpositive + S (dst_positive_table_lookup_sourcevaluemaskentryright) = S ((S (dc_quotient_table_lookup_sourcevaluemaskentry)) * dst_positive_scale_table_lookup_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_lookup_sourcevaluemaskentryrightpositive. dst_positive_code_table_lookup_sourcevaluemaskentryright = ff_q_pvs_table_lookup_sourcevaluemaskentryrightpositive * S ((S (dc_quotient_table_lookup_sourcevaluemaskentry)) * dst_positive_scale_table_lookup_sourcevaluemaskentryright) + (dst_positive_table_lookup_sourcevaluemaskentryright))) /\ (((((exists ff_h_pvs_table_lookup_sourcevaluemaskentryrightnegative. ff_h_pvs_table_lookup_sourcevaluemaskentryrightnegative + S (dst_negative_table_lookup_sourcevaluemaskentryright) = S ((S (dc_quotient_table_lookup_sourcevaluemaskentry)) * dst_negative_scale_table_lookup_sourcevaluemaskentryright)) /\ exists ff_q_pvs_table_lookup_sourcevaluemaskentryrightnegative. dst_negative_code_table_lookup_sourcevaluemaskentryright = ff_q_pvs_table_lookup_sourcevaluemaskentryrightnegative * S ((S (dc_quotient_table_lookup_sourcevaluemaskentry)) * dst_negative_scale_table_lookup_sourcevaluemaskentryright) + (dst_negative_table_lookup_sourcevaluemaskentryright))) /\ (exists ge_balance_positive_table_lookup_sourcevaluemaskentryrightvalue ge_balance_negative_table_lookup_sourcevaluemaskentryrightvalue. (((((dc_right_table_lookup_sourcevaluemaskentry) = 2 * (ge_balance_positive_table_lookup_sourcevaluemaskentryrightvalue) /\ (ge_balance_negative_table_lookup_sourcevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemaskentryrightvaluedecode. (((dc_right_table_lookup_sourcevaluemaskentry) = 2 * ge_signed_half_table_lookup_sourcevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_lookup_sourcevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_lookup_sourcevaluemaskentryrightvalue) = S ge_signed_half_table_lookup_sourcevaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_lookup_sourcevaluemaskentryright) + ge_balance_negative_table_lookup_sourcevaluemaskentryrightvalue = (dst_negative_table_lookup_sourcevaluemaskentryright) + ge_balance_positive_table_lookup_sourcevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_lookup_sourcevaluemaskentryproduct sto_an_table_lookup_sourcevaluemaskentryproduct sto_bp_table_lookup_sourcevaluemaskentryproduct sto_bn_table_lookup_sourcevaluemaskentryproduct sto_cp_table_lookup_sourcevaluemaskentryproduct sto_cn_table_lookup_sourcevaluemaskentryproduct. (((((dc_left_table_lookup_sourcevaluemaskentry) = 2 * (sto_ap_table_lookup_sourcevaluemaskentryproduct) /\ (sto_an_table_lookup_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemaskentryproductleft. (((dc_left_table_lookup_sourcevaluemaskentry) = 2 * ge_signed_half_table_lookup_sourcevaluemaskentryproductleft + 1 /\ (sto_ap_table_lookup_sourcevaluemaskentryproduct) = 0) /\ (sto_an_table_lookup_sourcevaluemaskentryproduct) = S ge_signed_half_table_lookup_sourcevaluemaskentryproductleft))) /\ ((((((dc_right_table_lookup_sourcevaluemaskentry) = 2 * (sto_bp_table_lookup_sourcevaluemaskentryproduct) /\ (sto_bn_table_lookup_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemaskentryproductright. (((dc_right_table_lookup_sourcevaluemaskentry) = 2 * ge_signed_half_table_lookup_sourcevaluemaskentryproductright + 1 /\ (sto_bp_table_lookup_sourcevaluemaskentryproduct) = 0) /\ (sto_bn_table_lookup_sourcevaluemaskentryproduct) = S ge_signed_half_table_lookup_sourcevaluemaskentryproductright))) /\ ((((((dc_value_table_lookup_sourcevaluemask) = 2 * (sto_cp_table_lookup_sourcevaluemaskentryproduct) /\ (sto_cn_table_lookup_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluemaskentryproductoutput. (((dc_value_table_lookup_sourcevaluemask) = 2 * ge_signed_half_table_lookup_sourcevaluemaskentryproductoutput + 1 /\ (sto_cp_table_lookup_sourcevaluemaskentryproduct) = 0) /\ (sto_cn_table_lookup_sourcevaluemaskentryproduct) = S ge_signed_half_table_lookup_sourcevaluemaskentryproductoutput))) /\ ((sto_ap_table_lookup_sourcevaluemaskentryproduct * sto_bp_table_lookup_sourcevaluemaskentryproduct + sto_an_table_lookup_sourcevaluemaskentryproduct * sto_bn_table_lookup_sourcevaluemaskentryproduct) + sto_cn_table_lookup_sourcevaluemaskentryproduct = (sto_ap_table_lookup_sourcevaluemaskentryproduct * sto_bn_table_lookup_sourcevaluemaskentryproduct + sto_an_table_lookup_sourcevaluemaskentryproduct * sto_bp_table_lookup_sourcevaluemaskentryproduct) + sto_cp_table_lookup_sourcevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_lookup_sourcevaluemask)=0 \/ ~(exists pvs_factor_table_lookup_sourcevaluemaskentrynondivisor. (dc_input_table_lookup_source) = (dc_index_table_lookup_sourcevaluemask) * pvs_factor_table_lookup_sourcevaluemaskentrynondivisor)) /\ ((dc_value_table_lookup_sourcevaluemask)=0))))))) /\ (exists dst_positive_code_table_lookup_sourcevaluefold dst_positive_scale_table_lookup_sourcevaluefold dst_negative_code_table_lookup_sourcevaluefold dst_negative_scale_table_lookup_sourcevaluefold dst_positive_sum_table_lookup_sourcevaluefold dst_negative_sum_table_lookup_sourcevaluefold. (((dc_mask_table_lookup_sourcevalue) = (((((dst_positive_code_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold)) * S ((dst_positive_code_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold)) + ((dst_positive_scale_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold))) + (((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) * S ((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) + ((dst_negative_scale_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)))) * S ((((dst_positive_code_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold)) * S ((dst_positive_code_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold)) + ((dst_positive_scale_table_lookup_sourcevaluefold) + (dst_positive_scale_table_lookup_sourcevaluefold))) + (((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) * S ((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) + ((dst_negative_scale_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)))) + ((((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) * S ((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) + ((dst_negative_scale_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold))) + (((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) * S ((dst_negative_code_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)) + ((dst_negative_scale_table_lookup_sourcevaluefold) + (dst_negative_scale_table_lookup_sourcevaluefold)))))) /\ (((exists fs_u_dst_table_lookup_sourcevaluefoldpositive fs_v_dst_table_lookup_sourcevaluefoldpositive. ((((exists fs_h_dst_table_lookup_sourcevaluefoldpositive_body_start. fs_h_dst_table_lookup_sourcevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_lookup_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldpositive_body_start. fs_u_dst_table_lookup_sourcevaluefoldpositive = fs_q_dst_table_lookup_sourcevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_lookup_sourcevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldpositive_body_terminal. fs_h_dst_table_lookup_sourcevaluefoldpositive_body_terminal + S (dst_positive_sum_table_lookup_sourcevaluefold) = S ((S (S (dc_input_table_lookup_source))) * fs_v_dst_table_lookup_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldpositive_body_terminal. fs_u_dst_table_lookup_sourcevaluefoldpositive = fs_q_dst_table_lookup_sourcevaluefoldpositive_body_terminal * S ((S (S (dc_input_table_lookup_source))) * fs_v_dst_table_lookup_sourcevaluefoldpositive) + (dst_positive_sum_table_lookup_sourcevaluefold))) /\ forall fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps. (exists fs_lt_dst_table_lookup_sourcevaluefoldpositive_body_steps_bound. fs_lt_dst_table_lookup_sourcevaluefoldpositive_body_steps_bound + S fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps = S (dc_input_table_lookup_source)) -> exists fs_a_dst_table_lookup_sourcevaluefoldpositive_body_steps fs_r_dst_table_lookup_sourcevaluefoldpositive_body_steps fs_s_dst_table_lookup_sourcevaluefoldpositive_body_steps. ((((exists fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_summand. fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_summand + S (fs_a_dst_table_lookup_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_lookup_sourcevaluefold)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_summand. dst_positive_code_table_lookup_sourcevaluefold = fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_table_lookup_sourcevaluefold) + (fs_a_dst_table_lookup_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_partial. fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_partial + S (fs_r_dst_table_lookup_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_partial. fs_u_dst_table_lookup_sourcevaluefoldpositive = fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldpositive) + (fs_r_dst_table_lookup_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_successor. fs_h_dst_table_lookup_sourcevaluefoldpositive_body_steps_successor + S (fs_s_dst_table_lookup_sourcevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldpositive)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_successor. fs_u_dst_table_lookup_sourcevaluefoldpositive = fs_q_dst_table_lookup_sourcevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_lookup_sourcevaluefoldpositive_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldpositive) + (fs_s_dst_table_lookup_sourcevaluefoldpositive_body_steps))) /\ fs_s_dst_table_lookup_sourcevaluefoldpositive_body_steps = fs_r_dst_table_lookup_sourcevaluefoldpositive_body_steps + fs_a_dst_table_lookup_sourcevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_lookup_sourcevaluefoldnegative fs_v_dst_table_lookup_sourcevaluefoldnegative. ((((exists fs_h_dst_table_lookup_sourcevaluefoldnegative_body_start. fs_h_dst_table_lookup_sourcevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_lookup_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldnegative_body_start. fs_u_dst_table_lookup_sourcevaluefoldnegative = fs_q_dst_table_lookup_sourcevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_lookup_sourcevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldnegative_body_terminal. fs_h_dst_table_lookup_sourcevaluefoldnegative_body_terminal + S (dst_negative_sum_table_lookup_sourcevaluefold) = S ((S (S (dc_input_table_lookup_source))) * fs_v_dst_table_lookup_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldnegative_body_terminal. fs_u_dst_table_lookup_sourcevaluefoldnegative = fs_q_dst_table_lookup_sourcevaluefoldnegative_body_terminal * S ((S (S (dc_input_table_lookup_source))) * fs_v_dst_table_lookup_sourcevaluefoldnegative) + (dst_negative_sum_table_lookup_sourcevaluefold))) /\ forall fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps. (exists fs_lt_dst_table_lookup_sourcevaluefoldnegative_body_steps_bound. fs_lt_dst_table_lookup_sourcevaluefoldnegative_body_steps_bound + S fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps = S (dc_input_table_lookup_source)) -> exists fs_a_dst_table_lookup_sourcevaluefoldnegative_body_steps fs_r_dst_table_lookup_sourcevaluefoldnegative_body_steps fs_s_dst_table_lookup_sourcevaluefoldnegative_body_steps. ((((exists fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_summand. fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_summand + S (fs_a_dst_table_lookup_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_lookup_sourcevaluefold)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_summand. dst_negative_code_table_lookup_sourcevaluefold = fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_table_lookup_sourcevaluefold) + (fs_a_dst_table_lookup_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_partial. fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_partial + S (fs_r_dst_table_lookup_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_partial. fs_u_dst_table_lookup_sourcevaluefoldnegative = fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldnegative) + (fs_r_dst_table_lookup_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_successor. fs_h_dst_table_lookup_sourcevaluefoldnegative_body_steps_successor + S (fs_s_dst_table_lookup_sourcevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldnegative)) /\ exists fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_successor. fs_u_dst_table_lookup_sourcevaluefoldnegative = fs_q_dst_table_lookup_sourcevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_lookup_sourcevaluefoldnegative_body_steps)) * fs_v_dst_table_lookup_sourcevaluefoldnegative) + (fs_s_dst_table_lookup_sourcevaluefoldnegative_body_steps))) /\ fs_s_dst_table_lookup_sourcevaluefoldnegative_body_steps = fs_r_dst_table_lookup_sourcevaluefoldnegative_body_steps + fs_a_dst_table_lookup_sourcevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_lookup_sourcevaluefoldresult ge_balance_negative_table_lookup_sourcevaluefoldresult. (((((dc_output_table_lookup_source) = 2 * (ge_balance_positive_table_lookup_sourcevaluefoldresult) /\ (ge_balance_negative_table_lookup_sourcevaluefoldresult) = 0) \/ exists ge_signed_half_table_lookup_sourcevaluefoldresultdecode. (((dc_output_table_lookup_source) = 2 * ge_signed_half_table_lookup_sourcevaluefoldresultdecode + 1 /\ (ge_balance_positive_table_lookup_sourcevaluefoldresult) = 0) /\ (ge_balance_negative_table_lookup_sourcevaluefoldresult) = S ge_signed_half_table_lookup_sourcevaluefoldresultdecode))) /\ ((dst_positive_sum_table_lookup_sourcevaluefold) + ge_balance_negative_table_lookup_sourcevaluefoldresult = (dst_negative_sum_table_lookup_sourcevaluefold) + ge_balance_positive_table_lookup_sourcevaluefoldresult)))))))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_table_lookup_bound. pvs_le_gap_table_lookup_bound + (n) = (N)) -> exists z. (exists dst_positive_code_table_lookup_entry dst_positive_scale_table_lookup_entry dst_negative_code_table_lookup_entry dst_negative_scale_table_lookup_entry dst_positive_table_lookup_entry dst_negative_table_lookup_entry. (((H) = (((((dst_positive_code_table_lookup_entry) + (dst_positive_scale_table_lookup_entry)) * S ((dst_positive_code_table_lookup_entry) + (dst_positive_scale_table_lookup_entry)) + ((dst_positive_scale_table_lookup_entry) + (dst_positive_scale_table_lookup_entry))) + (((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) * S ((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) + ((dst_negative_scale_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)))) * S ((((dst_positive_code_table_lookup_entry) + (dst_positive_scale_table_lookup_entry)) * S ((dst_positive_code_table_lookup_entry) + (dst_positive_scale_table_lookup_entry)) + ((dst_positive_scale_table_lookup_entry) + (dst_positive_scale_table_lookup_entry))) + (((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) * S ((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) + ((dst_negative_scale_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)))) + ((((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) * S ((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) + ((dst_negative_scale_table_lookup_entry) + (dst_negative_scale_table_lookup_entry))) + (((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) * S ((dst_negative_code_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)) + ((dst_negative_scale_table_lookup_entry) + (dst_negative_scale_table_lookup_entry)))))) /\ (((((exists ff_h_pvs_table_lookup_entrypositive. ff_h_pvs_table_lookup_entrypositive + S (dst_positive_table_lookup_entry) = S ((S (n)) * dst_positive_scale_table_lookup_entry)) /\ exists ff_q_pvs_table_lookup_entrypositive. dst_positive_code_table_lookup_entry = ff_q_pvs_table_lookup_entrypositive * S ((S (n)) * dst_positive_scale_table_lookup_entry) + (dst_positive_table_lookup_entry))) /\ (((((exists ff_h_pvs_table_lookup_entrynegative. ff_h_pvs_table_lookup_entrynegative + S (dst_negative_table_lookup_entry) = S ((S (n)) * dst_negative_scale_table_lookup_entry)) /\ exists ff_q_pvs_table_lookup_entrynegative. dst_negative_code_table_lookup_entry = ff_q_pvs_table_lookup_entrynegative * S ((S (n)) * dst_negative_scale_table_lookup_entry) + (dst_negative_table_lookup_entry))) /\ (exists ge_balance_positive_table_lookup_entryvalue ge_balance_negative_table_lookup_entryvalue. (((((z) = 2 * (ge_balance_positive_table_lookup_entryvalue) /\ (ge_balance_negative_table_lookup_entryvalue) = 0) \/ exists ge_signed_half_table_lookup_entryvaluedecode. (((z) = 2 * ge_signed_half_table_lookup_entryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_entryvalue) = 0) /\ (ge_balance_negative_table_lookup_entryvalue) = S ge_signed_half_table_lookup_entryvaluedecode))) /\ ((dst_positive_table_lookup_entry) + ge_balance_negative_table_lookup_entryvalue = (dst_negative_table_lookup_entry) + ge_balance_positive_table_lookup_entryvalue))))))))) /\ (((~((n)=0)) /\ (exists dc_mask_table_lookup_value. ((((exists dst_positive_code_table_lookup_valuemasktable dst_positive_scale_table_lookup_valuemasktable dst_negative_code_table_lookup_valuemasktable dst_negative_scale_table_lookup_valuemasktable. (((dc_mask_table_lookup_value) = (((((dst_positive_code_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable)) * S ((dst_positive_code_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable)) + ((dst_positive_scale_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable))) + (((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) * S ((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) + ((dst_negative_scale_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)))) * S ((((dst_positive_code_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable)) * S ((dst_positive_code_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable)) + ((dst_positive_scale_table_lookup_valuemasktable) + (dst_positive_scale_table_lookup_valuemasktable))) + (((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) * S ((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) + ((dst_negative_scale_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)))) + ((((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) * S ((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) + ((dst_negative_scale_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable))) + (((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) * S ((dst_negative_code_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)) + ((dst_negative_scale_table_lookup_valuemasktable) + (dst_negative_scale_table_lookup_valuemasktable)))))) /\ (forall dst_index_table_lookup_valuemasktable. (exists pvs_le_gap_table_lookup_valuemasktabledomain. pvs_le_gap_table_lookup_valuemasktabledomain + (dst_index_table_lookup_valuemasktable) = (n)) -> exists dst_positive_table_lookup_valuemasktable dst_negative_table_lookup_valuemasktable dst_value_table_lookup_valuemasktable. ((((exists ff_h_pvs_table_lookup_valuemasktableentrypositive. ff_h_pvs_table_lookup_valuemasktableentrypositive + S (dst_positive_table_lookup_valuemasktable) = S ((S (dst_index_table_lookup_valuemasktable)) * dst_positive_scale_table_lookup_valuemasktable)) /\ exists ff_q_pvs_table_lookup_valuemasktableentrypositive. dst_positive_code_table_lookup_valuemasktable = ff_q_pvs_table_lookup_valuemasktableentrypositive * S ((S (dst_index_table_lookup_valuemasktable)) * dst_positive_scale_table_lookup_valuemasktable) + (dst_positive_table_lookup_valuemasktable))) /\ (((((exists ff_h_pvs_table_lookup_valuemasktableentrynegative. ff_h_pvs_table_lookup_valuemasktableentrynegative + S (dst_negative_table_lookup_valuemasktable) = S ((S (dst_index_table_lookup_valuemasktable)) * dst_negative_scale_table_lookup_valuemasktable)) /\ exists ff_q_pvs_table_lookup_valuemasktableentrynegative. dst_negative_code_table_lookup_valuemasktable = ff_q_pvs_table_lookup_valuemasktableentrynegative * S ((S (dst_index_table_lookup_valuemasktable)) * dst_negative_scale_table_lookup_valuemasktable) + (dst_negative_table_lookup_valuemasktable))) /\ (exists ge_balance_positive_table_lookup_valuemasktableentryvalue ge_balance_negative_table_lookup_valuemasktableentryvalue. (((((dst_value_table_lookup_valuemasktable) = 2 * (ge_balance_positive_table_lookup_valuemasktableentryvalue) /\ (ge_balance_negative_table_lookup_valuemasktableentryvalue) = 0) \/ exists ge_signed_half_table_lookup_valuemasktableentryvaluedecode. (((dst_value_table_lookup_valuemasktable) = 2 * ge_signed_half_table_lookup_valuemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_lookup_valuemasktableentryvalue) = 0) /\ (ge_balance_negative_table_lookup_valuemasktableentryvalue) = S ge_signed_half_table_lookup_valuemasktableentryvaluedecode))) /\ ((dst_positive_table_lookup_valuemasktable) + ge_balance_negative_table_lookup_valuemasktableentryvalue = (dst_negative_table_lookup_valuemasktable) + ge_balance_positive_table_lookup_valuemasktableentryvalue))))))))) /\ (forall dc_index_table_lookup_valuemask dc_value_table_lookup_valuemask. (exists pvs_le_gap_table_lookup_valuemaskdomain. pvs_le_gap_table_lookup_valuemaskdomain + (dc_index_table_lookup_valuemask) = (n)) -> (exists dst_positive_code_table_lookup_valuemasklookup dst_positive_scale_table_lookup_valuemasklookup dst_negative_code_table_lookup_valuemasklookup dst_negative_scale_table_lookup_valuemasklookup dst_positive_table_lookup_valuemasklookup dst_negative_table_lookup_valuemasklookup. (((dc_mask_table_lookup_value) = (((((dst_positive_code_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup)) * S ((dst_positive_code_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup)) + ((dst_positive_scale_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup))) + (((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) * S ((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) + ((dst_negative_scale_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)))) * S ((((dst_positive_code_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup)) * S ((dst_positive_code_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup)) + ((dst_positive_scale_table_lookup_valuemasklookup) + (dst_positive_scale_table_lookup_valuemasklookup))) + (((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) * S ((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) + ((dst_negative_scale_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)))) + ((((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) * S ((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) + ((dst_negative_scale_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup))) + (((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) * S ((dst_negative_code_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)) + ((dst_negative_scale_table_lookup_valuemasklookup) + (dst_negative_scale_table_lookup_valuemasklookup)))))) /\ (((((exists ff_h_pvs_table_lookup_valuemasklookuppositive. ff_h_pvs_table_lookup_valuemasklookuppositive + S (dst_positive_table_lookup_valuemasklookup) = S ((S (dc_index_table_lookup_valuemask)) * dst_positive_scale_table_lookup_valuemasklookup)) /\ exists ff_q_pvs_table_lookup_valuemasklookuppositive. dst_positive_code_table_lookup_valuemasklookup = ff_q_pvs_table_lookup_valuemasklookuppositive * S ((S (dc_index_table_lookup_valuemask)) * dst_positive_scale_table_lookup_valuemasklookup) + (dst_positive_table_lookup_valuemasklookup))) /\ (((((exists ff_h_pvs_table_lookup_valuemasklookupnegative. ff_h_pvs_table_lookup_valuemasklookupnegative + S (dst_negative_table_lookup_valuemasklookup) = S ((S (dc_index_table_lookup_valuemask)) * dst_negative_scale_table_lookup_valuemasklookup)) /\ exists ff_q_pvs_table_lookup_valuemasklookupnegative. dst_negative_code_table_lookup_valuemasklookup = ff_q_pvs_table_lookup_valuemasklookupnegative * S ((S (dc_index_table_lookup_valuemask)) * dst_negative_scale_table_lookup_valuemasklookup) + (dst_negative_table_lookup_valuemasklookup))) /\ (exists ge_balance_positive_table_lookup_valuemasklookupvalue ge_balance_negative_table_lookup_valuemasklookupvalue. (((((dc_value_table_lookup_valuemask) = 2 * (ge_balance_positive_table_lookup_valuemasklookupvalue) /\ (ge_balance_negative_table_lookup_valuemasklookupvalue) = 0) \/ exists ge_signed_half_table_lookup_valuemasklookupvaluedecode. (((dc_value_table_lookup_valuemask) = 2 * ge_signed_half_table_lookup_valuemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_lookup_valuemasklookupvalue) = 0) /\ (ge_balance_negative_table_lookup_valuemasklookupvalue) = S ge_signed_half_table_lookup_valuemasklookupvaluedecode))) /\ ((dst_positive_table_lookup_valuemasklookup) + ge_balance_negative_table_lookup_valuemasklookupvalue = (dst_negative_table_lookup_valuemasklookup) + ge_balance_positive_table_lookup_valuemasklookupvalue))))))))) -> ((((~((dc_index_table_lookup_valuemask)=0)) /\ (exists dc_quotient_table_lookup_valuemaskentry dc_left_table_lookup_valuemaskentry dc_right_table_lookup_valuemaskentry. (((n)=(dc_index_table_lookup_valuemask)*dc_quotient_table_lookup_valuemaskentry) /\ (((exists dst_positive_code_table_lookup_valuemaskentryleft dst_positive_scale_table_lookup_valuemaskentryleft dst_negative_code_table_lookup_valuemaskentryleft dst_negative_scale_table_lookup_valuemaskentryleft dst_positive_table_lookup_valuemaskentryleft dst_negative_table_lookup_valuemaskentryleft. (((F) = (((((dst_positive_code_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft)) * S ((dst_positive_code_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft)) + ((dst_positive_scale_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft))) + (((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) * S ((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) + ((dst_negative_scale_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)))) * S ((((dst_positive_code_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft)) * S ((dst_positive_code_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft)) + ((dst_positive_scale_table_lookup_valuemaskentryleft) + (dst_positive_scale_table_lookup_valuemaskentryleft))) + (((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) * S ((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) + ((dst_negative_scale_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)))) + ((((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) * S ((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) + ((dst_negative_scale_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft))) + (((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) * S ((dst_negative_code_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)) + ((dst_negative_scale_table_lookup_valuemaskentryleft) + (dst_negative_scale_table_lookup_valuemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_lookup_valuemaskentryleftpositive. ff_h_pvs_table_lookup_valuemaskentryleftpositive + S (dst_positive_table_lookup_valuemaskentryleft) = S ((S (dc_index_table_lookup_valuemask)) * dst_positive_scale_table_lookup_valuemaskentryleft)) /\ exists ff_q_pvs_table_lookup_valuemaskentryleftpositive. dst_positive_code_table_lookup_valuemaskentryleft = ff_q_pvs_table_lookup_valuemaskentryleftpositive * S ((S (dc_index_table_lookup_valuemask)) * dst_positive_scale_table_lookup_valuemaskentryleft) + (dst_positive_table_lookup_valuemaskentryleft))) /\ (((((exists ff_h_pvs_table_lookup_valuemaskentryleftnegative. ff_h_pvs_table_lookup_valuemaskentryleftnegative + S (dst_negative_table_lookup_valuemaskentryleft) = S ((S (dc_index_table_lookup_valuemask)) * dst_negative_scale_table_lookup_valuemaskentryleft)) /\ exists ff_q_pvs_table_lookup_valuemaskentryleftnegative. dst_negative_code_table_lookup_valuemaskentryleft = ff_q_pvs_table_lookup_valuemaskentryleftnegative * S ((S (dc_index_table_lookup_valuemask)) * dst_negative_scale_table_lookup_valuemaskentryleft) + (dst_negative_table_lookup_valuemaskentryleft))) /\ (exists ge_balance_positive_table_lookup_valuemaskentryleftvalue ge_balance_negative_table_lookup_valuemaskentryleftvalue. (((((dc_left_table_lookup_valuemaskentry) = 2 * (ge_balance_positive_table_lookup_valuemaskentryleftvalue) /\ (ge_balance_negative_table_lookup_valuemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_lookup_valuemaskentryleftvaluedecode. (((dc_left_table_lookup_valuemaskentry) = 2 * ge_signed_half_table_lookup_valuemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_lookup_valuemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_lookup_valuemaskentryleftvalue) = S ge_signed_half_table_lookup_valuemaskentryleftvaluedecode))) /\ ((dst_positive_table_lookup_valuemaskentryleft) + ge_balance_negative_table_lookup_valuemaskentryleftvalue = (dst_negative_table_lookup_valuemaskentryleft) + ge_balance_positive_table_lookup_valuemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_lookup_valuemaskentryright dst_positive_scale_table_lookup_valuemaskentryright dst_negative_code_table_lookup_valuemaskentryright dst_negative_scale_table_lookup_valuemaskentryright dst_positive_table_lookup_valuemaskentryright dst_negative_table_lookup_valuemaskentryright. (((G) = (((((dst_positive_code_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright)) * S ((dst_positive_code_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright)) + ((dst_positive_scale_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright))) + (((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) * S ((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) + ((dst_negative_scale_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)))) * S ((((dst_positive_code_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright)) * S ((dst_positive_code_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright)) + ((dst_positive_scale_table_lookup_valuemaskentryright) + (dst_positive_scale_table_lookup_valuemaskentryright))) + (((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) * S ((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) + ((dst_negative_scale_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)))) + ((((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) * S ((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) + ((dst_negative_scale_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright))) + (((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) * S ((dst_negative_code_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)) + ((dst_negative_scale_table_lookup_valuemaskentryright) + (dst_negative_scale_table_lookup_valuemaskentryright)))))) /\ (((((exists ff_h_pvs_table_lookup_valuemaskentryrightpositive. ff_h_pvs_table_lookup_valuemaskentryrightpositive + S (dst_positive_table_lookup_valuemaskentryright) = S ((S (dc_quotient_table_lookup_valuemaskentry)) * dst_positive_scale_table_lookup_valuemaskentryright)) /\ exists ff_q_pvs_table_lookup_valuemaskentryrightpositive. dst_positive_code_table_lookup_valuemaskentryright = ff_q_pvs_table_lookup_valuemaskentryrightpositive * S ((S (dc_quotient_table_lookup_valuemaskentry)) * dst_positive_scale_table_lookup_valuemaskentryright) + (dst_positive_table_lookup_valuemaskentryright))) /\ (((((exists ff_h_pvs_table_lookup_valuemaskentryrightnegative. ff_h_pvs_table_lookup_valuemaskentryrightnegative + S (dst_negative_table_lookup_valuemaskentryright) = S ((S (dc_quotient_table_lookup_valuemaskentry)) * dst_negative_scale_table_lookup_valuemaskentryright)) /\ exists ff_q_pvs_table_lookup_valuemaskentryrightnegative. dst_negative_code_table_lookup_valuemaskentryright = ff_q_pvs_table_lookup_valuemaskentryrightnegative * S ((S (dc_quotient_table_lookup_valuemaskentry)) * dst_negative_scale_table_lookup_valuemaskentryright) + (dst_negative_table_lookup_valuemaskentryright))) /\ (exists ge_balance_positive_table_lookup_valuemaskentryrightvalue ge_balance_negative_table_lookup_valuemaskentryrightvalue. (((((dc_right_table_lookup_valuemaskentry) = 2 * (ge_balance_positive_table_lookup_valuemaskentryrightvalue) /\ (ge_balance_negative_table_lookup_valuemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_lookup_valuemaskentryrightvaluedecode. (((dc_right_table_lookup_valuemaskentry) = 2 * ge_signed_half_table_lookup_valuemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_lookup_valuemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_lookup_valuemaskentryrightvalue) = S ge_signed_half_table_lookup_valuemaskentryrightvaluedecode))) /\ ((dst_positive_table_lookup_valuemaskentryright) + ge_balance_negative_table_lookup_valuemaskentryrightvalue = (dst_negative_table_lookup_valuemaskentryright) + ge_balance_positive_table_lookup_valuemaskentryrightvalue))))))))) /\ (exists sto_ap_table_lookup_valuemaskentryproduct sto_an_table_lookup_valuemaskentryproduct sto_bp_table_lookup_valuemaskentryproduct sto_bn_table_lookup_valuemaskentryproduct sto_cp_table_lookup_valuemaskentryproduct sto_cn_table_lookup_valuemaskentryproduct. (((((dc_left_table_lookup_valuemaskentry) = 2 * (sto_ap_table_lookup_valuemaskentryproduct) /\ (sto_an_table_lookup_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_valuemaskentryproductleft. (((dc_left_table_lookup_valuemaskentry) = 2 * ge_signed_half_table_lookup_valuemaskentryproductleft + 1 /\ (sto_ap_table_lookup_valuemaskentryproduct) = 0) /\ (sto_an_table_lookup_valuemaskentryproduct) = S ge_signed_half_table_lookup_valuemaskentryproductleft))) /\ ((((((dc_right_table_lookup_valuemaskentry) = 2 * (sto_bp_table_lookup_valuemaskentryproduct) /\ (sto_bn_table_lookup_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_valuemaskentryproductright. (((dc_right_table_lookup_valuemaskentry) = 2 * ge_signed_half_table_lookup_valuemaskentryproductright + 1 /\ (sto_bp_table_lookup_valuemaskentryproduct) = 0) /\ (sto_bn_table_lookup_valuemaskentryproduct) = S ge_signed_half_table_lookup_valuemaskentryproductright))) /\ ((((((dc_value_table_lookup_valuemask) = 2 * (sto_cp_table_lookup_valuemaskentryproduct) /\ (sto_cn_table_lookup_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_lookup_valuemaskentryproductoutput. (((dc_value_table_lookup_valuemask) = 2 * ge_signed_half_table_lookup_valuemaskentryproductoutput + 1 /\ (sto_cp_table_lookup_valuemaskentryproduct) = 0) /\ (sto_cn_table_lookup_valuemaskentryproduct) = S ge_signed_half_table_lookup_valuemaskentryproductoutput))) /\ ((sto_ap_table_lookup_valuemaskentryproduct * sto_bp_table_lookup_valuemaskentryproduct + sto_an_table_lookup_valuemaskentryproduct * sto_bn_table_lookup_valuemaskentryproduct) + sto_cn_table_lookup_valuemaskentryproduct = (sto_ap_table_lookup_valuemaskentryproduct * sto_bn_table_lookup_valuemaskentryproduct + sto_an_table_lookup_valuemaskentryproduct * sto_bp_table_lookup_valuemaskentryproduct) + sto_cp_table_lookup_valuemaskentryproduct))))))))))))))) \/ ((((dc_index_table_lookup_valuemask)=0 \/ ~(exists pvs_factor_table_lookup_valuemaskentrynondivisor. (n) = (dc_index_table_lookup_valuemask) * pvs_factor_table_lookup_valuemaskentrynondivisor)) /\ ((dc_value_table_lookup_valuemask)=0))))))) /\ (exists dst_positive_code_table_lookup_valuefold dst_positive_scale_table_lookup_valuefold dst_negative_code_table_lookup_valuefold dst_negative_scale_table_lookup_valuefold dst_positive_sum_table_lookup_valuefold dst_negative_sum_table_lookup_valuefold. (((dc_mask_table_lookup_value) = (((((dst_positive_code_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold)) * S ((dst_positive_code_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold)) + ((dst_positive_scale_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold))) + (((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) * S ((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) + ((dst_negative_scale_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)))) * S ((((dst_positive_code_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold)) * S ((dst_positive_code_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold)) + ((dst_positive_scale_table_lookup_valuefold) + (dst_positive_scale_table_lookup_valuefold))) + (((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) * S ((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) + ((dst_negative_scale_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)))) + ((((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) * S ((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) + ((dst_negative_scale_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold))) + (((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) * S ((dst_negative_code_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)) + ((dst_negative_scale_table_lookup_valuefold) + (dst_negative_scale_table_lookup_valuefold)))))) /\ (((exists fs_u_dst_table_lookup_valuefoldpositive fs_v_dst_table_lookup_valuefoldpositive. ((((exists fs_h_dst_table_lookup_valuefoldpositive_body_start. fs_h_dst_table_lookup_valuefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_lookup_valuefoldpositive)) /\ exists fs_q_dst_table_lookup_valuefoldpositive_body_start. fs_u_dst_table_lookup_valuefoldpositive = fs_q_dst_table_lookup_valuefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_lookup_valuefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_lookup_valuefoldpositive_body_terminal. fs_h_dst_table_lookup_valuefoldpositive_body_terminal + S (dst_positive_sum_table_lookup_valuefold) = S ((S (S (n))) * fs_v_dst_table_lookup_valuefoldpositive)) /\ exists fs_q_dst_table_lookup_valuefoldpositive_body_terminal. fs_u_dst_table_lookup_valuefoldpositive = fs_q_dst_table_lookup_valuefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_table_lookup_valuefoldpositive) + (dst_positive_sum_table_lookup_valuefold))) /\ forall fs_i_dst_table_lookup_valuefoldpositive_body_steps. (exists fs_lt_dst_table_lookup_valuefoldpositive_body_steps_bound. fs_lt_dst_table_lookup_valuefoldpositive_body_steps_bound + S fs_i_dst_table_lookup_valuefoldpositive_body_steps = S (n)) -> exists fs_a_dst_table_lookup_valuefoldpositive_body_steps fs_r_dst_table_lookup_valuefoldpositive_body_steps fs_s_dst_table_lookup_valuefoldpositive_body_steps. ((((exists fs_h_dst_table_lookup_valuefoldpositive_body_steps_summand. fs_h_dst_table_lookup_valuefoldpositive_body_steps_summand + S (fs_a_dst_table_lookup_valuefoldpositive_body_steps) = S ((S (fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * dst_positive_scale_table_lookup_valuefold)) /\ exists fs_q_dst_table_lookup_valuefoldpositive_body_steps_summand. dst_positive_code_table_lookup_valuefold = fs_q_dst_table_lookup_valuefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * dst_positive_scale_table_lookup_valuefold) + (fs_a_dst_table_lookup_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_lookup_valuefoldpositive_body_steps_partial. fs_h_dst_table_lookup_valuefoldpositive_body_steps_partial + S (fs_r_dst_table_lookup_valuefoldpositive_body_steps) = S ((S (fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * fs_v_dst_table_lookup_valuefoldpositive)) /\ exists fs_q_dst_table_lookup_valuefoldpositive_body_steps_partial. fs_u_dst_table_lookup_valuefoldpositive = fs_q_dst_table_lookup_valuefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * fs_v_dst_table_lookup_valuefoldpositive) + (fs_r_dst_table_lookup_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_lookup_valuefoldpositive_body_steps_successor. fs_h_dst_table_lookup_valuefoldpositive_body_steps_successor + S (fs_s_dst_table_lookup_valuefoldpositive_body_steps) = S ((S (S fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * fs_v_dst_table_lookup_valuefoldpositive)) /\ exists fs_q_dst_table_lookup_valuefoldpositive_body_steps_successor. fs_u_dst_table_lookup_valuefoldpositive = fs_q_dst_table_lookup_valuefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_lookup_valuefoldpositive_body_steps)) * fs_v_dst_table_lookup_valuefoldpositive) + (fs_s_dst_table_lookup_valuefoldpositive_body_steps))) /\ fs_s_dst_table_lookup_valuefoldpositive_body_steps = fs_r_dst_table_lookup_valuefoldpositive_body_steps + fs_a_dst_table_lookup_valuefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_lookup_valuefoldnegative fs_v_dst_table_lookup_valuefoldnegative. ((((exists fs_h_dst_table_lookup_valuefoldnegative_body_start. fs_h_dst_table_lookup_valuefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_lookup_valuefoldnegative)) /\ exists fs_q_dst_table_lookup_valuefoldnegative_body_start. fs_u_dst_table_lookup_valuefoldnegative = fs_q_dst_table_lookup_valuefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_lookup_valuefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_lookup_valuefoldnegative_body_terminal. fs_h_dst_table_lookup_valuefoldnegative_body_terminal + S (dst_negative_sum_table_lookup_valuefold) = S ((S (S (n))) * fs_v_dst_table_lookup_valuefoldnegative)) /\ exists fs_q_dst_table_lookup_valuefoldnegative_body_terminal. fs_u_dst_table_lookup_valuefoldnegative = fs_q_dst_table_lookup_valuefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_table_lookup_valuefoldnegative) + (dst_negative_sum_table_lookup_valuefold))) /\ forall fs_i_dst_table_lookup_valuefoldnegative_body_steps. (exists fs_lt_dst_table_lookup_valuefoldnegative_body_steps_bound. fs_lt_dst_table_lookup_valuefoldnegative_body_steps_bound + S fs_i_dst_table_lookup_valuefoldnegative_body_steps = S (n)) -> exists fs_a_dst_table_lookup_valuefoldnegative_body_steps fs_r_dst_table_lookup_valuefoldnegative_body_steps fs_s_dst_table_lookup_valuefoldnegative_body_steps. ((((exists fs_h_dst_table_lookup_valuefoldnegative_body_steps_summand. fs_h_dst_table_lookup_valuefoldnegative_body_steps_summand + S (fs_a_dst_table_lookup_valuefoldnegative_body_steps) = S ((S (fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * dst_negative_scale_table_lookup_valuefold)) /\ exists fs_q_dst_table_lookup_valuefoldnegative_body_steps_summand. dst_negative_code_table_lookup_valuefold = fs_q_dst_table_lookup_valuefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * dst_negative_scale_table_lookup_valuefold) + (fs_a_dst_table_lookup_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_lookup_valuefoldnegative_body_steps_partial. fs_h_dst_table_lookup_valuefoldnegative_body_steps_partial + S (fs_r_dst_table_lookup_valuefoldnegative_body_steps) = S ((S (fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * fs_v_dst_table_lookup_valuefoldnegative)) /\ exists fs_q_dst_table_lookup_valuefoldnegative_body_steps_partial. fs_u_dst_table_lookup_valuefoldnegative = fs_q_dst_table_lookup_valuefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * fs_v_dst_table_lookup_valuefoldnegative) + (fs_r_dst_table_lookup_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_lookup_valuefoldnegative_body_steps_successor. fs_h_dst_table_lookup_valuefoldnegative_body_steps_successor + S (fs_s_dst_table_lookup_valuefoldnegative_body_steps) = S ((S (S fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * fs_v_dst_table_lookup_valuefoldnegative)) /\ exists fs_q_dst_table_lookup_valuefoldnegative_body_steps_successor. fs_u_dst_table_lookup_valuefoldnegative = fs_q_dst_table_lookup_valuefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_lookup_valuefoldnegative_body_steps)) * fs_v_dst_table_lookup_valuefoldnegative) + (fs_s_dst_table_lookup_valuefoldnegative_body_steps))) /\ fs_s_dst_table_lookup_valuefoldnegative_body_steps = fs_r_dst_table_lookup_valuefoldnegative_body_steps + fs_a_dst_table_lookup_valuefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_lookup_valuefoldresult ge_balance_negative_table_lookup_valuefoldresult. (((((z) = 2 * (ge_balance_positive_table_lookup_valuefoldresult) /\ (ge_balance_negative_table_lookup_valuefoldresult) = 0) \/ exists ge_signed_half_table_lookup_valuefoldresultdecode. (((z) = 2 * ge_signed_half_table_lookup_valuefoldresultdecode + 1 /\ (ge_balance_positive_table_lookup_valuefoldresult) = 0) /\ (ge_balance_negative_table_lookup_valuefoldresult) = S ge_signed_half_table_lookup_valuefoldresultdecode))) /\ ((dst_positive_sum_table_lookup_valuefold) + ge_balance_negative_table_lookup_valuefoldresult = (dst_negative_sum_table_lookup_valuefold) + ge_balance_positive_table_lookup_valuefoldresult)))))))))))))