dirichlet_convolution_table_first_input_append_preserves

forall N F G H K a. (((exists dst_positive_code_tables_sourceleft dst_positive_scale_tables_sourceleft dst_negative_code_tables_sourceleft dst_negative_scale_tables_sourceleft. (((F) = (((((dst_positive_code_tables_sourceleft) + (dst_positive_scale_tables_sourceleft)) * S ((dst_positive_code_tables_sourceleft) + (dst_positive_scale_tables_sourceleft)) + ((dst_positive_scale_tables_sourceleft) + (dst_positive_scale_tables_sourceleft))) + (((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) * S ((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) + ((dst_negative_scale_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)))) * S ((((dst_positive_code_tables_sourceleft) + (dst_positive_scale_tables_sourceleft)) * S ((dst_positive_code_tables_sourceleft) + (dst_positive_scale_tables_sourceleft)) + ((dst_positive_scale_tables_sourceleft) + (dst_positive_scale_tables_sourceleft))) + (((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) * S ((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) + ((dst_negative_scale_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)))) + ((((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) * S ((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) + ((dst_negative_scale_tables_sourceleft) + (dst_negative_scale_tables_sourceleft))) + (((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) * S ((dst_negative_code_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)) + ((dst_negative_scale_tables_sourceleft) + (dst_negative_scale_tables_sourceleft)))))) /\ (forall dst_index_tables_sourceleft. (exists pvs_le_gap_tables_sourceleftdomain. pvs_le_gap_tables_sourceleftdomain + (dst_index_tables_sourceleft) = (N)) -> exists dst_positive_tables_sourceleft dst_negative_tables_sourceleft dst_value_tables_sourceleft. ((((exists ff_h_pvs_tables_sourceleftentrypositive. ff_h_pvs_tables_sourceleftentrypositive + S (dst_positive_tables_sourceleft) = S ((S (dst_index_tables_sourceleft)) * dst_positive_scale_tables_sourceleft)) /\ exists ff_q_pvs_tables_sourceleftentrypositive. dst_positive_code_tables_sourceleft = ff_q_pvs_tables_sourceleftentrypositive * S ((S (dst_index_tables_sourceleft)) * dst_positive_scale_tables_sourceleft) + (dst_positive_tables_sourceleft))) /\ (((((exists ff_h_pvs_tables_sourceleftentrynegative. ff_h_pvs_tables_sourceleftentrynegative + S (dst_negative_tables_sourceleft) = S ((S (dst_index_tables_sourceleft)) * dst_negative_scale_tables_sourceleft)) /\ exists ff_q_pvs_tables_sourceleftentrynegative. dst_negative_code_tables_sourceleft = ff_q_pvs_tables_sourceleftentrynegative * S ((S (dst_index_tables_sourceleft)) * dst_negative_scale_tables_sourceleft) + (dst_negative_tables_sourceleft))) /\ (exists ge_balance_positive_tables_sourceleftentryvalue ge_balance_negative_tables_sourceleftentryvalue. (((((dst_value_tables_sourceleft) = 2 * (ge_balance_positive_tables_sourceleftentryvalue) /\ (ge_balance_negative_tables_sourceleftentryvalue) = 0) \/ exists ge_signed_half_tables_sourceleftentryvaluedecode. (((dst_value_tables_sourceleft) = 2 * ge_signed_half_tables_sourceleftentryvaluedecode + 1 /\ (ge_balance_positive_tables_sourceleftentryvalue) = 0) /\ (ge_balance_negative_tables_sourceleftentryvalue) = S ge_signed_half_tables_sourceleftentryvaluedecode))) /\ ((dst_positive_tables_sourceleft) + ge_balance_negative_tables_sourceleftentryvalue = (dst_negative_tables_sourceleft) + ge_balance_positive_tables_sourceleftentryvalue))))))))) /\ (((exists dst_positive_code_tables_sourceright dst_positive_scale_tables_sourceright dst_negative_code_tables_sourceright dst_negative_scale_tables_sourceright. (((G) = (((((dst_positive_code_tables_sourceright) + (dst_positive_scale_tables_sourceright)) * S ((dst_positive_code_tables_sourceright) + (dst_positive_scale_tables_sourceright)) + ((dst_positive_scale_tables_sourceright) + (dst_positive_scale_tables_sourceright))) + (((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) * S ((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) + ((dst_negative_scale_tables_sourceright) + (dst_negative_scale_tables_sourceright)))) * S ((((dst_positive_code_tables_sourceright) + (dst_positive_scale_tables_sourceright)) * S ((dst_positive_code_tables_sourceright) + (dst_positive_scale_tables_sourceright)) + ((dst_positive_scale_tables_sourceright) + (dst_positive_scale_tables_sourceright))) + (((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) * S ((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) + ((dst_negative_scale_tables_sourceright) + (dst_negative_scale_tables_sourceright)))) + ((((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) * S ((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) + ((dst_negative_scale_tables_sourceright) + (dst_negative_scale_tables_sourceright))) + (((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) * S ((dst_negative_code_tables_sourceright) + (dst_negative_scale_tables_sourceright)) + ((dst_negative_scale_tables_sourceright) + (dst_negative_scale_tables_sourceright)))))) /\ (forall dst_index_tables_sourceright. (exists pvs_le_gap_tables_sourcerightdomain. pvs_le_gap_tables_sourcerightdomain + (dst_index_tables_sourceright) = (N)) -> exists dst_positive_tables_sourceright dst_negative_tables_sourceright dst_value_tables_sourceright. ((((exists ff_h_pvs_tables_sourcerightentrypositive. ff_h_pvs_tables_sourcerightentrypositive + S (dst_positive_tables_sourceright) = S ((S (dst_index_tables_sourceright)) * dst_positive_scale_tables_sourceright)) /\ exists ff_q_pvs_tables_sourcerightentrypositive. dst_positive_code_tables_sourceright = ff_q_pvs_tables_sourcerightentrypositive * S ((S (dst_index_tables_sourceright)) * dst_positive_scale_tables_sourceright) + (dst_positive_tables_sourceright))) /\ (((((exists ff_h_pvs_tables_sourcerightentrynegative. ff_h_pvs_tables_sourcerightentrynegative + S (dst_negative_tables_sourceright) = S ((S (dst_index_tables_sourceright)) * dst_negative_scale_tables_sourceright)) /\ exists ff_q_pvs_tables_sourcerightentrynegative. dst_negative_code_tables_sourceright = ff_q_pvs_tables_sourcerightentrynegative * S ((S (dst_index_tables_sourceright)) * dst_negative_scale_tables_sourceright) + (dst_negative_tables_sourceright))) /\ (exists ge_balance_positive_tables_sourcerightentryvalue ge_balance_negative_tables_sourcerightentryvalue. (((((dst_value_tables_sourceright) = 2 * (ge_balance_positive_tables_sourcerightentryvalue) /\ (ge_balance_negative_tables_sourcerightentryvalue) = 0) \/ exists ge_signed_half_tables_sourcerightentryvaluedecode. (((dst_value_tables_sourceright) = 2 * ge_signed_half_tables_sourcerightentryvaluedecode + 1 /\ (ge_balance_positive_tables_sourcerightentryvalue) = 0) /\ (ge_balance_negative_tables_sourcerightentryvalue) = S ge_signed_half_tables_sourcerightentryvaluedecode))) /\ ((dst_positive_tables_sourceright) + ge_balance_negative_tables_sourcerightentryvalue = (dst_negative_tables_sourceright) + ge_balance_positive_tables_sourcerightentryvalue))))))))) /\ (((exists dst_positive_code_tables_sourcetable dst_positive_scale_tables_sourcetable dst_negative_code_tables_sourcetable dst_negative_scale_tables_sourcetable. (((K) = (((((dst_positive_code_tables_sourcetable) + (dst_positive_scale_tables_sourcetable)) * S ((dst_positive_code_tables_sourcetable) + (dst_positive_scale_tables_sourcetable)) + ((dst_positive_scale_tables_sourcetable) + (dst_positive_scale_tables_sourcetable))) + (((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) * S ((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) + ((dst_negative_scale_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)))) * S ((((dst_positive_code_tables_sourcetable) + (dst_positive_scale_tables_sourcetable)) * S ((dst_positive_code_tables_sourcetable) + (dst_positive_scale_tables_sourcetable)) + ((dst_positive_scale_tables_sourcetable) + (dst_positive_scale_tables_sourcetable))) + (((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) * S ((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) + ((dst_negative_scale_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)))) + ((((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) * S ((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) + ((dst_negative_scale_tables_sourcetable) + (dst_negative_scale_tables_sourcetable))) + (((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) * S ((dst_negative_code_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)) + ((dst_negative_scale_tables_sourcetable) + (dst_negative_scale_tables_sourcetable)))))) /\ (forall dst_index_tables_sourcetable. (exists pvs_le_gap_tables_sourcetabledomain. pvs_le_gap_tables_sourcetabledomain + (dst_index_tables_sourcetable) = (N)) -> exists dst_positive_tables_sourcetable dst_negative_tables_sourcetable dst_value_tables_sourcetable. ((((exists ff_h_pvs_tables_sourcetableentrypositive. ff_h_pvs_tables_sourcetableentrypositive + S (dst_positive_tables_sourcetable) = S ((S (dst_index_tables_sourcetable)) * dst_positive_scale_tables_sourcetable)) /\ exists ff_q_pvs_tables_sourcetableentrypositive. dst_positive_code_tables_sourcetable = ff_q_pvs_tables_sourcetableentrypositive * S ((S (dst_index_tables_sourcetable)) * dst_positive_scale_tables_sourcetable) + (dst_positive_tables_sourcetable))) /\ (((((exists ff_h_pvs_tables_sourcetableentrynegative. ff_h_pvs_tables_sourcetableentrynegative + S (dst_negative_tables_sourcetable) = S ((S (dst_index_tables_sourcetable)) * dst_negative_scale_tables_sourcetable)) /\ exists ff_q_pvs_tables_sourcetableentrynegative. dst_negative_code_tables_sourcetable = ff_q_pvs_tables_sourcetableentrynegative * S ((S (dst_index_tables_sourcetable)) * dst_negative_scale_tables_sourcetable) + (dst_negative_tables_sourcetable))) /\ (exists ge_balance_positive_tables_sourcetableentryvalue ge_balance_negative_tables_sourcetableentryvalue. (((((dst_value_tables_sourcetable) = 2 * (ge_balance_positive_tables_sourcetableentryvalue) /\ (ge_balance_negative_tables_sourcetableentryvalue) = 0) \/ exists ge_signed_half_tables_sourcetableentryvaluedecode. (((dst_value_tables_sourcetable) = 2 * ge_signed_half_tables_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_tables_sourcetableentryvalue) = 0) /\ (ge_balance_negative_tables_sourcetableentryvalue) = S ge_signed_half_tables_sourcetableentryvaluedecode))) /\ ((dst_positive_tables_sourcetable) + ge_balance_negative_tables_sourcetableentryvalue = (dst_negative_tables_sourcetable) + ge_balance_positive_tables_sourcetableentryvalue))))))))) /\ (forall dc_input_tables_source dc_output_tables_source. ~(dc_input_tables_source=0) -> (exists pvs_le_gap_tables_sourcedomain. pvs_le_gap_tables_sourcedomain + (dc_input_tables_source) = (N)) -> (exists dst_positive_code_tables_sourcelookup dst_positive_scale_tables_sourcelookup dst_negative_code_tables_sourcelookup dst_negative_scale_tables_sourcelookup dst_positive_tables_sourcelookup dst_negative_tables_sourcelookup. (((K) = (((((dst_positive_code_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup)) * S ((dst_positive_code_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup)) + ((dst_positive_scale_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup))) + (((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) * S ((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) + ((dst_negative_scale_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)))) * S ((((dst_positive_code_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup)) * S ((dst_positive_code_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup)) + ((dst_positive_scale_tables_sourcelookup) + (dst_positive_scale_tables_sourcelookup))) + (((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) * S ((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) + ((dst_negative_scale_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)))) + ((((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) * S ((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) + ((dst_negative_scale_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup))) + (((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) * S ((dst_negative_code_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)) + ((dst_negative_scale_tables_sourcelookup) + (dst_negative_scale_tables_sourcelookup)))))) /\ (((((exists ff_h_pvs_tables_sourcelookuppositive. ff_h_pvs_tables_sourcelookuppositive + S (dst_positive_tables_sourcelookup) = S ((S (dc_input_tables_source)) * dst_positive_scale_tables_sourcelookup)) /\ exists ff_q_pvs_tables_sourcelookuppositive. dst_positive_code_tables_sourcelookup = ff_q_pvs_tables_sourcelookuppositive * S ((S (dc_input_tables_source)) * dst_positive_scale_tables_sourcelookup) + (dst_positive_tables_sourcelookup))) /\ (((((exists ff_h_pvs_tables_sourcelookupnegative. ff_h_pvs_tables_sourcelookupnegative + S (dst_negative_tables_sourcelookup) = S ((S (dc_input_tables_source)) * dst_negative_scale_tables_sourcelookup)) /\ exists ff_q_pvs_tables_sourcelookupnegative. dst_negative_code_tables_sourcelookup = ff_q_pvs_tables_sourcelookupnegative * S ((S (dc_input_tables_source)) * dst_negative_scale_tables_sourcelookup) + (dst_negative_tables_sourcelookup))) /\ (exists ge_balance_positive_tables_sourcelookupvalue ge_balance_negative_tables_sourcelookupvalue. (((((dc_output_tables_source) = 2 * (ge_balance_positive_tables_sourcelookupvalue) /\ (ge_balance_negative_tables_sourcelookupvalue) = 0) \/ exists ge_signed_half_tables_sourcelookupvaluedecode. (((dc_output_tables_source) = 2 * ge_signed_half_tables_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_tables_sourcelookupvalue) = 0) /\ (ge_balance_negative_tables_sourcelookupvalue) = S ge_signed_half_tables_sourcelookupvaluedecode))) /\ ((dst_positive_tables_sourcelookup) + ge_balance_negative_tables_sourcelookupvalue = (dst_negative_tables_sourcelookup) + ge_balance_positive_tables_sourcelookupvalue))))))))) -> (((~((dc_input_tables_source)=0)) /\ (exists dc_mask_tables_sourcevalue. ((((exists dst_positive_code_tables_sourcevaluemasktable dst_positive_scale_tables_sourcevaluemasktable dst_negative_code_tables_sourcevaluemasktable dst_negative_scale_tables_sourcevaluemasktable. (((dc_mask_tables_sourcevalue) = (((((dst_positive_code_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable)) * S ((dst_positive_code_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable)) + ((dst_positive_scale_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable))) + (((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) * S ((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) + ((dst_negative_scale_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)))) * S ((((dst_positive_code_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable)) * S ((dst_positive_code_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable)) + ((dst_positive_scale_tables_sourcevaluemasktable) + (dst_positive_scale_tables_sourcevaluemasktable))) + (((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) * S ((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) + ((dst_negative_scale_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)))) + ((((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) * S ((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) + ((dst_negative_scale_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable))) + (((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) * S ((dst_negative_code_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)) + ((dst_negative_scale_tables_sourcevaluemasktable) + (dst_negative_scale_tables_sourcevaluemasktable)))))) /\ (forall dst_index_tables_sourcevaluemasktable. (exists pvs_le_gap_tables_sourcevaluemasktabledomain. pvs_le_gap_tables_sourcevaluemasktabledomain + (dst_index_tables_sourcevaluemasktable) = (dc_input_tables_source)) -> exists dst_positive_tables_sourcevaluemasktable dst_negative_tables_sourcevaluemasktable dst_value_tables_sourcevaluemasktable. ((((exists ff_h_pvs_tables_sourcevaluemasktableentrypositive. ff_h_pvs_tables_sourcevaluemasktableentrypositive + S (dst_positive_tables_sourcevaluemasktable) = S ((S (dst_index_tables_sourcevaluemasktable)) * dst_positive_scale_tables_sourcevaluemasktable)) /\ exists ff_q_pvs_tables_sourcevaluemasktableentrypositive. dst_positive_code_tables_sourcevaluemasktable = ff_q_pvs_tables_sourcevaluemasktableentrypositive * S ((S (dst_index_tables_sourcevaluemasktable)) * dst_positive_scale_tables_sourcevaluemasktable) + (dst_positive_tables_sourcevaluemasktable))) /\ (((((exists ff_h_pvs_tables_sourcevaluemasktableentrynegative. ff_h_pvs_tables_sourcevaluemasktableentrynegative + S (dst_negative_tables_sourcevaluemasktable) = S ((S (dst_index_tables_sourcevaluemasktable)) * dst_negative_scale_tables_sourcevaluemasktable)) /\ exists ff_q_pvs_tables_sourcevaluemasktableentrynegative. dst_negative_code_tables_sourcevaluemasktable = ff_q_pvs_tables_sourcevaluemasktableentrynegative * S ((S (dst_index_tables_sourcevaluemasktable)) * dst_negative_scale_tables_sourcevaluemasktable) + (dst_negative_tables_sourcevaluemasktable))) /\ (exists ge_balance_positive_tables_sourcevaluemasktableentryvalue ge_balance_negative_tables_sourcevaluemasktableentryvalue. (((((dst_value_tables_sourcevaluemasktable) = 2 * (ge_balance_positive_tables_sourcevaluemasktableentryvalue) /\ (ge_balance_negative_tables_sourcevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_tables_sourcevaluemasktableentryvaluedecode. (((dst_value_tables_sourcevaluemasktable) = 2 * ge_signed_half_tables_sourcevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_tables_sourcevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_tables_sourcevaluemasktableentryvalue) = S ge_signed_half_tables_sourcevaluemasktableentryvaluedecode))) /\ ((dst_positive_tables_sourcevaluemasktable) + ge_balance_negative_tables_sourcevaluemasktableentryvalue = (dst_negative_tables_sourcevaluemasktable) + ge_balance_positive_tables_sourcevaluemasktableentryvalue))))))))) /\ (forall dc_index_tables_sourcevaluemask dc_value_tables_sourcevaluemask. (exists pvs_le_gap_tables_sourcevaluemaskdomain. pvs_le_gap_tables_sourcevaluemaskdomain + (dc_index_tables_sourcevaluemask) = (dc_input_tables_source)) -> (exists dst_positive_code_tables_sourcevaluemasklookup dst_positive_scale_tables_sourcevaluemasklookup dst_negative_code_tables_sourcevaluemasklookup dst_negative_scale_tables_sourcevaluemasklookup dst_positive_tables_sourcevaluemasklookup dst_negative_tables_sourcevaluemasklookup. (((dc_mask_tables_sourcevalue) = (((((dst_positive_code_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup)) * S ((dst_positive_code_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup)) + ((dst_positive_scale_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup))) + (((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) * S ((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) + ((dst_negative_scale_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)))) * S ((((dst_positive_code_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup)) * S ((dst_positive_code_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup)) + ((dst_positive_scale_tables_sourcevaluemasklookup) + (dst_positive_scale_tables_sourcevaluemasklookup))) + (((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) * S ((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) + ((dst_negative_scale_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)))) + ((((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) * S ((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) + ((dst_negative_scale_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup))) + (((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) * S ((dst_negative_code_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)) + ((dst_negative_scale_tables_sourcevaluemasklookup) + (dst_negative_scale_tables_sourcevaluemasklookup)))))) /\ (((((exists ff_h_pvs_tables_sourcevaluemasklookuppositive. ff_h_pvs_tables_sourcevaluemasklookuppositive + S (dst_positive_tables_sourcevaluemasklookup) = S ((S (dc_index_tables_sourcevaluemask)) * dst_positive_scale_tables_sourcevaluemasklookup)) /\ exists ff_q_pvs_tables_sourcevaluemasklookuppositive. dst_positive_code_tables_sourcevaluemasklookup = ff_q_pvs_tables_sourcevaluemasklookuppositive * S ((S (dc_index_tables_sourcevaluemask)) * dst_positive_scale_tables_sourcevaluemasklookup) + (dst_positive_tables_sourcevaluemasklookup))) /\ (((((exists ff_h_pvs_tables_sourcevaluemasklookupnegative. ff_h_pvs_tables_sourcevaluemasklookupnegative + S (dst_negative_tables_sourcevaluemasklookup) = S ((S (dc_index_tables_sourcevaluemask)) * dst_negative_scale_tables_sourcevaluemasklookup)) /\ exists ff_q_pvs_tables_sourcevaluemasklookupnegative. dst_negative_code_tables_sourcevaluemasklookup = ff_q_pvs_tables_sourcevaluemasklookupnegative * S ((S (dc_index_tables_sourcevaluemask)) * dst_negative_scale_tables_sourcevaluemasklookup) + (dst_negative_tables_sourcevaluemasklookup))) /\ (exists ge_balance_positive_tables_sourcevaluemasklookupvalue ge_balance_negative_tables_sourcevaluemasklookupvalue. (((((dc_value_tables_sourcevaluemask) = 2 * (ge_balance_positive_tables_sourcevaluemasklookupvalue) /\ (ge_balance_negative_tables_sourcevaluemasklookupvalue) = 0) \/ exists ge_signed_half_tables_sourcevaluemasklookupvaluedecode. (((dc_value_tables_sourcevaluemask) = 2 * ge_signed_half_tables_sourcevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_tables_sourcevaluemasklookupvalue) = 0) /\ (ge_balance_negative_tables_sourcevaluemasklookupvalue) = S ge_signed_half_tables_sourcevaluemasklookupvaluedecode))) /\ ((dst_positive_tables_sourcevaluemasklookup) + ge_balance_negative_tables_sourcevaluemasklookupvalue = (dst_negative_tables_sourcevaluemasklookup) + ge_balance_positive_tables_sourcevaluemasklookupvalue))))))))) -> ((((~((dc_index_tables_sourcevaluemask)=0)) /\ (exists dc_quotient_tables_sourcevaluemaskentry dc_left_tables_sourcevaluemaskentry dc_right_tables_sourcevaluemaskentry. (((dc_input_tables_source)=(dc_index_tables_sourcevaluemask)*dc_quotient_tables_sourcevaluemaskentry) /\ (((exists dst_positive_code_tables_sourcevaluemaskentryleft dst_positive_scale_tables_sourcevaluemaskentryleft dst_negative_code_tables_sourcevaluemaskentryleft dst_negative_scale_tables_sourcevaluemaskentryleft dst_positive_tables_sourcevaluemaskentryleft dst_negative_tables_sourcevaluemaskentryleft. (((F) = (((((dst_positive_code_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft)) * S ((dst_positive_code_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft)) + ((dst_positive_scale_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft))) + (((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) * S ((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) + ((dst_negative_scale_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)))) * S ((((dst_positive_code_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft)) * S ((dst_positive_code_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft)) + ((dst_positive_scale_tables_sourcevaluemaskentryleft) + (dst_positive_scale_tables_sourcevaluemaskentryleft))) + (((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) * S ((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) + ((dst_negative_scale_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)))) + ((((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) * S ((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) + ((dst_negative_scale_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft))) + (((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) * S ((dst_negative_code_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)) + ((dst_negative_scale_tables_sourcevaluemaskentryleft) + (dst_negative_scale_tables_sourcevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_tables_sourcevaluemaskentryleftpositive. ff_h_pvs_tables_sourcevaluemaskentryleftpositive + S (dst_positive_tables_sourcevaluemaskentryleft) = S ((S (dc_index_tables_sourcevaluemask)) * dst_positive_scale_tables_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_tables_sourcevaluemaskentryleftpositive. dst_positive_code_tables_sourcevaluemaskentryleft = ff_q_pvs_tables_sourcevaluemaskentryleftpositive * S ((S (dc_index_tables_sourcevaluemask)) * dst_positive_scale_tables_sourcevaluemaskentryleft) + (dst_positive_tables_sourcevaluemaskentryleft))) /\ (((((exists ff_h_pvs_tables_sourcevaluemaskentryleftnegative. ff_h_pvs_tables_sourcevaluemaskentryleftnegative + S (dst_negative_tables_sourcevaluemaskentryleft) = S ((S (dc_index_tables_sourcevaluemask)) * dst_negative_scale_tables_sourcevaluemaskentryleft)) /\ exists ff_q_pvs_tables_sourcevaluemaskentryleftnegative. dst_negative_code_tables_sourcevaluemaskentryleft = ff_q_pvs_tables_sourcevaluemaskentryleftnegative * S ((S (dc_index_tables_sourcevaluemask)) * dst_negative_scale_tables_sourcevaluemaskentryleft) + (dst_negative_tables_sourcevaluemaskentryleft))) /\ (exists ge_balance_positive_tables_sourcevaluemaskentryleftvalue ge_balance_negative_tables_sourcevaluemaskentryleftvalue. (((((dc_left_tables_sourcevaluemaskentry) = 2 * (ge_balance_positive_tables_sourcevaluemaskentryleftvalue) /\ (ge_balance_negative_tables_sourcevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_tables_sourcevaluemaskentryleftvaluedecode. (((dc_left_tables_sourcevaluemaskentry) = 2 * ge_signed_half_tables_sourcevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_tables_sourcevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_tables_sourcevaluemaskentryleftvalue) = S ge_signed_half_tables_sourcevaluemaskentryleftvaluedecode))) /\ ((dst_positive_tables_sourcevaluemaskentryleft) + ge_balance_negative_tables_sourcevaluemaskentryleftvalue = (dst_negative_tables_sourcevaluemaskentryleft) + ge_balance_positive_tables_sourcevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_tables_sourcevaluemaskentryright dst_positive_scale_tables_sourcevaluemaskentryright dst_negative_code_tables_sourcevaluemaskentryright dst_negative_scale_tables_sourcevaluemaskentryright dst_positive_tables_sourcevaluemaskentryright dst_negative_tables_sourcevaluemaskentryright. (((G) = (((((dst_positive_code_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright)) * S ((dst_positive_code_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright)) + ((dst_positive_scale_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright))) + (((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) * S ((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) + ((dst_negative_scale_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)))) * S ((((dst_positive_code_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright)) * S ((dst_positive_code_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright)) + ((dst_positive_scale_tables_sourcevaluemaskentryright) + (dst_positive_scale_tables_sourcevaluemaskentryright))) + (((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) * S ((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) + ((dst_negative_scale_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)))) + ((((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) * S ((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) + ((dst_negative_scale_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright))) + (((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) * S ((dst_negative_code_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)) + ((dst_negative_scale_tables_sourcevaluemaskentryright) + (dst_negative_scale_tables_sourcevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_tables_sourcevaluemaskentryrightpositive. ff_h_pvs_tables_sourcevaluemaskentryrightpositive + S (dst_positive_tables_sourcevaluemaskentryright) = S ((S (dc_quotient_tables_sourcevaluemaskentry)) * dst_positive_scale_tables_sourcevaluemaskentryright)) /\ exists ff_q_pvs_tables_sourcevaluemaskentryrightpositive. dst_positive_code_tables_sourcevaluemaskentryright = ff_q_pvs_tables_sourcevaluemaskentryrightpositive * S ((S (dc_quotient_tables_sourcevaluemaskentry)) * dst_positive_scale_tables_sourcevaluemaskentryright) + (dst_positive_tables_sourcevaluemaskentryright))) /\ (((((exists ff_h_pvs_tables_sourcevaluemaskentryrightnegative. ff_h_pvs_tables_sourcevaluemaskentryrightnegative + S (dst_negative_tables_sourcevaluemaskentryright) = S ((S (dc_quotient_tables_sourcevaluemaskentry)) * dst_negative_scale_tables_sourcevaluemaskentryright)) /\ exists ff_q_pvs_tables_sourcevaluemaskentryrightnegative. dst_negative_code_tables_sourcevaluemaskentryright = ff_q_pvs_tables_sourcevaluemaskentryrightnegative * S ((S (dc_quotient_tables_sourcevaluemaskentry)) * dst_negative_scale_tables_sourcevaluemaskentryright) + (dst_negative_tables_sourcevaluemaskentryright))) /\ (exists ge_balance_positive_tables_sourcevaluemaskentryrightvalue ge_balance_negative_tables_sourcevaluemaskentryrightvalue. (((((dc_right_tables_sourcevaluemaskentry) = 2 * (ge_balance_positive_tables_sourcevaluemaskentryrightvalue) /\ (ge_balance_negative_tables_sourcevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_tables_sourcevaluemaskentryrightvaluedecode. (((dc_right_tables_sourcevaluemaskentry) = 2 * ge_signed_half_tables_sourcevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_tables_sourcevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_tables_sourcevaluemaskentryrightvalue) = S ge_signed_half_tables_sourcevaluemaskentryrightvaluedecode))) /\ ((dst_positive_tables_sourcevaluemaskentryright) + ge_balance_negative_tables_sourcevaluemaskentryrightvalue = (dst_negative_tables_sourcevaluemaskentryright) + ge_balance_positive_tables_sourcevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_tables_sourcevaluemaskentryproduct sto_an_tables_sourcevaluemaskentryproduct sto_bp_tables_sourcevaluemaskentryproduct sto_bn_tables_sourcevaluemaskentryproduct sto_cp_tables_sourcevaluemaskentryproduct sto_cn_tables_sourcevaluemaskentryproduct. (((((dc_left_tables_sourcevaluemaskentry) = 2 * (sto_ap_tables_sourcevaluemaskentryproduct) /\ (sto_an_tables_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_sourcevaluemaskentryproductleft. (((dc_left_tables_sourcevaluemaskentry) = 2 * ge_signed_half_tables_sourcevaluemaskentryproductleft + 1 /\ (sto_ap_tables_sourcevaluemaskentryproduct) = 0) /\ (sto_an_tables_sourcevaluemaskentryproduct) = S ge_signed_half_tables_sourcevaluemaskentryproductleft))) /\ ((((((dc_right_tables_sourcevaluemaskentry) = 2 * (sto_bp_tables_sourcevaluemaskentryproduct) /\ (sto_bn_tables_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_sourcevaluemaskentryproductright. (((dc_right_tables_sourcevaluemaskentry) = 2 * ge_signed_half_tables_sourcevaluemaskentryproductright + 1 /\ (sto_bp_tables_sourcevaluemaskentryproduct) = 0) /\ (sto_bn_tables_sourcevaluemaskentryproduct) = S ge_signed_half_tables_sourcevaluemaskentryproductright))) /\ ((((((dc_value_tables_sourcevaluemask) = 2 * (sto_cp_tables_sourcevaluemaskentryproduct) /\ (sto_cn_tables_sourcevaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_sourcevaluemaskentryproductoutput. (((dc_value_tables_sourcevaluemask) = 2 * ge_signed_half_tables_sourcevaluemaskentryproductoutput + 1 /\ (sto_cp_tables_sourcevaluemaskentryproduct) = 0) /\ (sto_cn_tables_sourcevaluemaskentryproduct) = S ge_signed_half_tables_sourcevaluemaskentryproductoutput))) /\ ((sto_ap_tables_sourcevaluemaskentryproduct * sto_bp_tables_sourcevaluemaskentryproduct + sto_an_tables_sourcevaluemaskentryproduct * sto_bn_tables_sourcevaluemaskentryproduct) + sto_cn_tables_sourcevaluemaskentryproduct = (sto_ap_tables_sourcevaluemaskentryproduct * sto_bn_tables_sourcevaluemaskentryproduct + sto_an_tables_sourcevaluemaskentryproduct * sto_bp_tables_sourcevaluemaskentryproduct) + sto_cp_tables_sourcevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_tables_sourcevaluemask)=0 \/ ~(exists pvs_factor_tables_sourcevaluemaskentrynondivisor. (dc_input_tables_source) = (dc_index_tables_sourcevaluemask) * pvs_factor_tables_sourcevaluemaskentrynondivisor)) /\ ((dc_value_tables_sourcevaluemask)=0))))))) /\ (exists dst_positive_code_tables_sourcevaluefold dst_positive_scale_tables_sourcevaluefold dst_negative_code_tables_sourcevaluefold dst_negative_scale_tables_sourcevaluefold dst_positive_sum_tables_sourcevaluefold dst_negative_sum_tables_sourcevaluefold. (((dc_mask_tables_sourcevalue) = (((((dst_positive_code_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold)) * S ((dst_positive_code_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold)) + ((dst_positive_scale_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold))) + (((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) * S ((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) + ((dst_negative_scale_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)))) * S ((((dst_positive_code_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold)) * S ((dst_positive_code_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold)) + ((dst_positive_scale_tables_sourcevaluefold) + (dst_positive_scale_tables_sourcevaluefold))) + (((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) * S ((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) + ((dst_negative_scale_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)))) + ((((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) * S ((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) + ((dst_negative_scale_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold))) + (((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) * S ((dst_negative_code_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)) + ((dst_negative_scale_tables_sourcevaluefold) + (dst_negative_scale_tables_sourcevaluefold)))))) /\ (((exists fs_u_dst_tables_sourcevaluefoldpositive fs_v_dst_tables_sourcevaluefoldpositive. ((((exists fs_h_dst_tables_sourcevaluefoldpositive_body_start. fs_h_dst_tables_sourcevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tables_sourcevaluefoldpositive)) /\ exists fs_q_dst_tables_sourcevaluefoldpositive_body_start. fs_u_dst_tables_sourcevaluefoldpositive = fs_q_dst_tables_sourcevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_tables_sourcevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldpositive_body_terminal. fs_h_dst_tables_sourcevaluefoldpositive_body_terminal + S (dst_positive_sum_tables_sourcevaluefold) = S ((S (S (dc_input_tables_source))) * fs_v_dst_tables_sourcevaluefoldpositive)) /\ exists fs_q_dst_tables_sourcevaluefoldpositive_body_terminal. fs_u_dst_tables_sourcevaluefoldpositive = fs_q_dst_tables_sourcevaluefoldpositive_body_terminal * S ((S (S (dc_input_tables_source))) * fs_v_dst_tables_sourcevaluefoldpositive) + (dst_positive_sum_tables_sourcevaluefold))) /\ forall fs_i_dst_tables_sourcevaluefoldpositive_body_steps. (exists fs_lt_dst_tables_sourcevaluefoldpositive_body_steps_bound. fs_lt_dst_tables_sourcevaluefoldpositive_body_steps_bound + S fs_i_dst_tables_sourcevaluefoldpositive_body_steps = S (dc_input_tables_source)) -> exists fs_a_dst_tables_sourcevaluefoldpositive_body_steps fs_r_dst_tables_sourcevaluefoldpositive_body_steps fs_s_dst_tables_sourcevaluefoldpositive_body_steps. ((((exists fs_h_dst_tables_sourcevaluefoldpositive_body_steps_summand. fs_h_dst_tables_sourcevaluefoldpositive_body_steps_summand + S (fs_a_dst_tables_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_tables_sourcevaluefold)) /\ exists fs_q_dst_tables_sourcevaluefoldpositive_body_steps_summand. dst_positive_code_tables_sourcevaluefold = fs_q_dst_tables_sourcevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * dst_positive_scale_tables_sourcevaluefold) + (fs_a_dst_tables_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldpositive_body_steps_partial. fs_h_dst_tables_sourcevaluefoldpositive_body_steps_partial + S (fs_r_dst_tables_sourcevaluefoldpositive_body_steps) = S ((S (fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * fs_v_dst_tables_sourcevaluefoldpositive)) /\ exists fs_q_dst_tables_sourcevaluefoldpositive_body_steps_partial. fs_u_dst_tables_sourcevaluefoldpositive = fs_q_dst_tables_sourcevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * fs_v_dst_tables_sourcevaluefoldpositive) + (fs_r_dst_tables_sourcevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldpositive_body_steps_successor. fs_h_dst_tables_sourcevaluefoldpositive_body_steps_successor + S (fs_s_dst_tables_sourcevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * fs_v_dst_tables_sourcevaluefoldpositive)) /\ exists fs_q_dst_tables_sourcevaluefoldpositive_body_steps_successor. fs_u_dst_tables_sourcevaluefoldpositive = fs_q_dst_tables_sourcevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_tables_sourcevaluefoldpositive_body_steps)) * fs_v_dst_tables_sourcevaluefoldpositive) + (fs_s_dst_tables_sourcevaluefoldpositive_body_steps))) /\ fs_s_dst_tables_sourcevaluefoldpositive_body_steps = fs_r_dst_tables_sourcevaluefoldpositive_body_steps + fs_a_dst_tables_sourcevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_tables_sourcevaluefoldnegative fs_v_dst_tables_sourcevaluefoldnegative. ((((exists fs_h_dst_tables_sourcevaluefoldnegative_body_start. fs_h_dst_tables_sourcevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tables_sourcevaluefoldnegative)) /\ exists fs_q_dst_tables_sourcevaluefoldnegative_body_start. fs_u_dst_tables_sourcevaluefoldnegative = fs_q_dst_tables_sourcevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_tables_sourcevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldnegative_body_terminal. fs_h_dst_tables_sourcevaluefoldnegative_body_terminal + S (dst_negative_sum_tables_sourcevaluefold) = S ((S (S (dc_input_tables_source))) * fs_v_dst_tables_sourcevaluefoldnegative)) /\ exists fs_q_dst_tables_sourcevaluefoldnegative_body_terminal. fs_u_dst_tables_sourcevaluefoldnegative = fs_q_dst_tables_sourcevaluefoldnegative_body_terminal * S ((S (S (dc_input_tables_source))) * fs_v_dst_tables_sourcevaluefoldnegative) + (dst_negative_sum_tables_sourcevaluefold))) /\ forall fs_i_dst_tables_sourcevaluefoldnegative_body_steps. (exists fs_lt_dst_tables_sourcevaluefoldnegative_body_steps_bound. fs_lt_dst_tables_sourcevaluefoldnegative_body_steps_bound + S fs_i_dst_tables_sourcevaluefoldnegative_body_steps = S (dc_input_tables_source)) -> exists fs_a_dst_tables_sourcevaluefoldnegative_body_steps fs_r_dst_tables_sourcevaluefoldnegative_body_steps fs_s_dst_tables_sourcevaluefoldnegative_body_steps. ((((exists fs_h_dst_tables_sourcevaluefoldnegative_body_steps_summand. fs_h_dst_tables_sourcevaluefoldnegative_body_steps_summand + S (fs_a_dst_tables_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_tables_sourcevaluefold)) /\ exists fs_q_dst_tables_sourcevaluefoldnegative_body_steps_summand. dst_negative_code_tables_sourcevaluefold = fs_q_dst_tables_sourcevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * dst_negative_scale_tables_sourcevaluefold) + (fs_a_dst_tables_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldnegative_body_steps_partial. fs_h_dst_tables_sourcevaluefoldnegative_body_steps_partial + S (fs_r_dst_tables_sourcevaluefoldnegative_body_steps) = S ((S (fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * fs_v_dst_tables_sourcevaluefoldnegative)) /\ exists fs_q_dst_tables_sourcevaluefoldnegative_body_steps_partial. fs_u_dst_tables_sourcevaluefoldnegative = fs_q_dst_tables_sourcevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * fs_v_dst_tables_sourcevaluefoldnegative) + (fs_r_dst_tables_sourcevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_tables_sourcevaluefoldnegative_body_steps_successor. fs_h_dst_tables_sourcevaluefoldnegative_body_steps_successor + S (fs_s_dst_tables_sourcevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * fs_v_dst_tables_sourcevaluefoldnegative)) /\ exists fs_q_dst_tables_sourcevaluefoldnegative_body_steps_successor. fs_u_dst_tables_sourcevaluefoldnegative = fs_q_dst_tables_sourcevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_tables_sourcevaluefoldnegative_body_steps)) * fs_v_dst_tables_sourcevaluefoldnegative) + (fs_s_dst_tables_sourcevaluefoldnegative_body_steps))) /\ fs_s_dst_tables_sourcevaluefoldnegative_body_steps = fs_r_dst_tables_sourcevaluefoldnegative_body_steps + fs_a_dst_tables_sourcevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_tables_sourcevaluefoldresult ge_balance_negative_tables_sourcevaluefoldresult. (((((dc_output_tables_source) = 2 * (ge_balance_positive_tables_sourcevaluefoldresult) /\ (ge_balance_negative_tables_sourcevaluefoldresult) = 0) \/ exists ge_signed_half_tables_sourcevaluefoldresultdecode. (((dc_output_tables_source) = 2 * ge_signed_half_tables_sourcevaluefoldresultdecode + 1 /\ (ge_balance_positive_tables_sourcevaluefoldresult) = 0) /\ (ge_balance_negative_tables_sourcevaluefoldresult) = S ge_signed_half_tables_sourcevaluefoldresultdecode))) /\ ((dst_positive_sum_tables_sourcevaluefold) + ge_balance_negative_tables_sourcevaluefoldresult = (dst_negative_sum_tables_sourcevaluefold) + ge_balance_positive_tables_sourcevaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_tables_extensiontable dst_positive_scale_tables_extensiontable dst_negative_code_tables_extensiontable dst_negative_scale_tables_extensiontable. (((H) = (((((dst_positive_code_tables_extensiontable) + (dst_positive_scale_tables_extensiontable)) * S ((dst_positive_code_tables_extensiontable) + (dst_positive_scale_tables_extensiontable)) + ((dst_positive_scale_tables_extensiontable) + (dst_positive_scale_tables_extensiontable))) + (((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) * S ((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) + ((dst_negative_scale_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)))) * S ((((dst_positive_code_tables_extensiontable) + (dst_positive_scale_tables_extensiontable)) * S ((dst_positive_code_tables_extensiontable) + (dst_positive_scale_tables_extensiontable)) + ((dst_positive_scale_tables_extensiontable) + (dst_positive_scale_tables_extensiontable))) + (((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) * S ((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) + ((dst_negative_scale_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)))) + ((((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) * S ((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) + ((dst_negative_scale_tables_extensiontable) + (dst_negative_scale_tables_extensiontable))) + (((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) * S ((dst_negative_code_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)) + ((dst_negative_scale_tables_extensiontable) + (dst_negative_scale_tables_extensiontable)))))) /\ (forall dst_index_tables_extensiontable. (exists pvs_le_gap_tables_extensiontabledomain. pvs_le_gap_tables_extensiontabledomain + (dst_index_tables_extensiontable) = (S N)) -> exists dst_positive_tables_extensiontable dst_negative_tables_extensiontable dst_value_tables_extensiontable. ((((exists ff_h_pvs_tables_extensiontableentrypositive. ff_h_pvs_tables_extensiontableentrypositive + S (dst_positive_tables_extensiontable) = S ((S (dst_index_tables_extensiontable)) * dst_positive_scale_tables_extensiontable)) /\ exists ff_q_pvs_tables_extensiontableentrypositive. dst_positive_code_tables_extensiontable = ff_q_pvs_tables_extensiontableentrypositive * S ((S (dst_index_tables_extensiontable)) * dst_positive_scale_tables_extensiontable) + (dst_positive_tables_extensiontable))) /\ (((((exists ff_h_pvs_tables_extensiontableentrynegative. ff_h_pvs_tables_extensiontableentrynegative + S (dst_negative_tables_extensiontable) = S ((S (dst_index_tables_extensiontable)) * dst_negative_scale_tables_extensiontable)) /\ exists ff_q_pvs_tables_extensiontableentrynegative. dst_negative_code_tables_extensiontable = ff_q_pvs_tables_extensiontableentrynegative * S ((S (dst_index_tables_extensiontable)) * dst_negative_scale_tables_extensiontable) + (dst_negative_tables_extensiontable))) /\ (exists ge_balance_positive_tables_extensiontableentryvalue ge_balance_negative_tables_extensiontableentryvalue. (((((dst_value_tables_extensiontable) = 2 * (ge_balance_positive_tables_extensiontableentryvalue) /\ (ge_balance_negative_tables_extensiontableentryvalue) = 0) \/ exists ge_signed_half_tables_extensiontableentryvaluedecode. (((dst_value_tables_extensiontable) = 2 * ge_signed_half_tables_extensiontableentryvaluedecode + 1 /\ (ge_balance_positive_tables_extensiontableentryvalue) = 0) /\ (ge_balance_negative_tables_extensiontableentryvalue) = S ge_signed_half_tables_extensiontableentryvaluedecode))) /\ ((dst_positive_tables_extensiontable) + ge_balance_negative_tables_extensiontableentryvalue = (dst_negative_tables_extensiontable) + ge_balance_positive_tables_extensiontableentryvalue))))))))) /\ (((forall dst_index_tables_extensionprefix dst_first_tables_extensionprefix dst_second_tables_extensionprefix. (exists pvs_gap_tables_extensionprefixbound. pvs_gap_tables_extensionprefixbound + S (dst_index_tables_extensionprefix) = (S N)) -> (exists dst_positive_code_tables_extensionprefixfirst dst_positive_scale_tables_extensionprefixfirst dst_negative_code_tables_extensionprefixfirst dst_negative_scale_tables_extensionprefixfirst dst_positive_tables_extensionprefixfirst dst_negative_tables_extensionprefixfirst. (((F) = (((((dst_positive_code_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst)) * S ((dst_positive_code_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst)) + ((dst_positive_scale_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst))) + (((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) * S ((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) + ((dst_negative_scale_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)))) * S ((((dst_positive_code_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst)) * S ((dst_positive_code_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst)) + ((dst_positive_scale_tables_extensionprefixfirst) + (dst_positive_scale_tables_extensionprefixfirst))) + (((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) * S ((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) + ((dst_negative_scale_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)))) + ((((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) * S ((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) + ((dst_negative_scale_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst))) + (((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) * S ((dst_negative_code_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)) + ((dst_negative_scale_tables_extensionprefixfirst) + (dst_negative_scale_tables_extensionprefixfirst)))))) /\ (((((exists ff_h_pvs_tables_extensionprefixfirstpositive. ff_h_pvs_tables_extensionprefixfirstpositive + S (dst_positive_tables_extensionprefixfirst) = S ((S (dst_index_tables_extensionprefix)) * dst_positive_scale_tables_extensionprefixfirst)) /\ exists ff_q_pvs_tables_extensionprefixfirstpositive. dst_positive_code_tables_extensionprefixfirst = ff_q_pvs_tables_extensionprefixfirstpositive * S ((S (dst_index_tables_extensionprefix)) * dst_positive_scale_tables_extensionprefixfirst) + (dst_positive_tables_extensionprefixfirst))) /\ (((((exists ff_h_pvs_tables_extensionprefixfirstnegative. ff_h_pvs_tables_extensionprefixfirstnegative + S (dst_negative_tables_extensionprefixfirst) = S ((S (dst_index_tables_extensionprefix)) * dst_negative_scale_tables_extensionprefixfirst)) /\ exists ff_q_pvs_tables_extensionprefixfirstnegative. dst_negative_code_tables_extensionprefixfirst = ff_q_pvs_tables_extensionprefixfirstnegative * S ((S (dst_index_tables_extensionprefix)) * dst_negative_scale_tables_extensionprefixfirst) + (dst_negative_tables_extensionprefixfirst))) /\ (exists ge_balance_positive_tables_extensionprefixfirstvalue ge_balance_negative_tables_extensionprefixfirstvalue. (((((dst_first_tables_extensionprefix) = 2 * (ge_balance_positive_tables_extensionprefixfirstvalue) /\ (ge_balance_negative_tables_extensionprefixfirstvalue) = 0) \/ exists ge_signed_half_tables_extensionprefixfirstvaluedecode. (((dst_first_tables_extensionprefix) = 2 * ge_signed_half_tables_extensionprefixfirstvaluedecode + 1 /\ (ge_balance_positive_tables_extensionprefixfirstvalue) = 0) /\ (ge_balance_negative_tables_extensionprefixfirstvalue) = S ge_signed_half_tables_extensionprefixfirstvaluedecode))) /\ ((dst_positive_tables_extensionprefixfirst) + ge_balance_negative_tables_extensionprefixfirstvalue = (dst_negative_tables_extensionprefixfirst) + ge_balance_positive_tables_extensionprefixfirstvalue))))))))) -> (exists dst_positive_code_tables_extensionprefixsecond dst_positive_scale_tables_extensionprefixsecond dst_negative_code_tables_extensionprefixsecond dst_negative_scale_tables_extensionprefixsecond dst_positive_tables_extensionprefixsecond dst_negative_tables_extensionprefixsecond. (((H) = (((((dst_positive_code_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond)) * S ((dst_positive_code_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond)) + ((dst_positive_scale_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond))) + (((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) * S ((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) + ((dst_negative_scale_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)))) * S ((((dst_positive_code_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond)) * S ((dst_positive_code_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond)) + ((dst_positive_scale_tables_extensionprefixsecond) + (dst_positive_scale_tables_extensionprefixsecond))) + (((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) * S ((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) + ((dst_negative_scale_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)))) + ((((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) * S ((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) + ((dst_negative_scale_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond))) + (((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) * S ((dst_negative_code_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)) + ((dst_negative_scale_tables_extensionprefixsecond) + (dst_negative_scale_tables_extensionprefixsecond)))))) /\ (((((exists ff_h_pvs_tables_extensionprefixsecondpositive. ff_h_pvs_tables_extensionprefixsecondpositive + S (dst_positive_tables_extensionprefixsecond) = S ((S (dst_index_tables_extensionprefix)) * dst_positive_scale_tables_extensionprefixsecond)) /\ exists ff_q_pvs_tables_extensionprefixsecondpositive. dst_positive_code_tables_extensionprefixsecond = ff_q_pvs_tables_extensionprefixsecondpositive * S ((S (dst_index_tables_extensionprefix)) * dst_positive_scale_tables_extensionprefixsecond) + (dst_positive_tables_extensionprefixsecond))) /\ (((((exists ff_h_pvs_tables_extensionprefixsecondnegative. ff_h_pvs_tables_extensionprefixsecondnegative + S (dst_negative_tables_extensionprefixsecond) = S ((S (dst_index_tables_extensionprefix)) * dst_negative_scale_tables_extensionprefixsecond)) /\ exists ff_q_pvs_tables_extensionprefixsecondnegative. dst_negative_code_tables_extensionprefixsecond = ff_q_pvs_tables_extensionprefixsecondnegative * S ((S (dst_index_tables_extensionprefix)) * dst_negative_scale_tables_extensionprefixsecond) + (dst_negative_tables_extensionprefixsecond))) /\ (exists ge_balance_positive_tables_extensionprefixsecondvalue ge_balance_negative_tables_extensionprefixsecondvalue. (((((dst_second_tables_extensionprefix) = 2 * (ge_balance_positive_tables_extensionprefixsecondvalue) /\ (ge_balance_negative_tables_extensionprefixsecondvalue) = 0) \/ exists ge_signed_half_tables_extensionprefixsecondvaluedecode. (((dst_second_tables_extensionprefix) = 2 * ge_signed_half_tables_extensionprefixsecondvaluedecode + 1 /\ (ge_balance_positive_tables_extensionprefixsecondvalue) = 0) /\ (ge_balance_negative_tables_extensionprefixsecondvalue) = S ge_signed_half_tables_extensionprefixsecondvaluedecode))) /\ ((dst_positive_tables_extensionprefixsecond) + ge_balance_negative_tables_extensionprefixsecondvalue = (dst_negative_tables_extensionprefixsecond) + ge_balance_positive_tables_extensionprefixsecondvalue))))))))) -> dst_first_tables_extensionprefix = dst_second_tables_extensionprefix) /\ (exists dst_positive_code_tables_extensionlast dst_positive_scale_tables_extensionlast dst_negative_code_tables_extensionlast dst_negative_scale_tables_extensionlast dst_positive_tables_extensionlast dst_negative_tables_extensionlast. (((H) = (((((dst_positive_code_tables_extensionlast) + (dst_positive_scale_tables_extensionlast)) * S ((dst_positive_code_tables_extensionlast) + (dst_positive_scale_tables_extensionlast)) + ((dst_positive_scale_tables_extensionlast) + (dst_positive_scale_tables_extensionlast))) + (((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) * S ((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) + ((dst_negative_scale_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)))) * S ((((dst_positive_code_tables_extensionlast) + (dst_positive_scale_tables_extensionlast)) * S ((dst_positive_code_tables_extensionlast) + (dst_positive_scale_tables_extensionlast)) + ((dst_positive_scale_tables_extensionlast) + (dst_positive_scale_tables_extensionlast))) + (((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) * S ((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) + ((dst_negative_scale_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)))) + ((((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) * S ((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) + ((dst_negative_scale_tables_extensionlast) + (dst_negative_scale_tables_extensionlast))) + (((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) * S ((dst_negative_code_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)) + ((dst_negative_scale_tables_extensionlast) + (dst_negative_scale_tables_extensionlast)))))) /\ (((((exists ff_h_pvs_tables_extensionlastpositive. ff_h_pvs_tables_extensionlastpositive + S (dst_positive_tables_extensionlast) = S ((S (S N)) * dst_positive_scale_tables_extensionlast)) /\ exists ff_q_pvs_tables_extensionlastpositive. dst_positive_code_tables_extensionlast = ff_q_pvs_tables_extensionlastpositive * S ((S (S N)) * dst_positive_scale_tables_extensionlast) + (dst_positive_tables_extensionlast))) /\ (((((exists ff_h_pvs_tables_extensionlastnegative. ff_h_pvs_tables_extensionlastnegative + S (dst_negative_tables_extensionlast) = S ((S (S N)) * dst_negative_scale_tables_extensionlast)) /\ exists ff_q_pvs_tables_extensionlastnegative. dst_negative_code_tables_extensionlast = ff_q_pvs_tables_extensionlastnegative * S ((S (S N)) * dst_negative_scale_tables_extensionlast) + (dst_negative_tables_extensionlast))) /\ (exists ge_balance_positive_tables_extensionlastvalue ge_balance_negative_tables_extensionlastvalue. (((((a) = 2 * (ge_balance_positive_tables_extensionlastvalue) /\ (ge_balance_negative_tables_extensionlastvalue) = 0) \/ exists ge_signed_half_tables_extensionlastvaluedecode. (((a) = 2 * ge_signed_half_tables_extensionlastvaluedecode + 1 /\ (ge_balance_positive_tables_extensionlastvalue) = 0) /\ (ge_balance_negative_tables_extensionlastvalue) = S ge_signed_half_tables_extensionlastvaluedecode))) /\ ((dst_positive_tables_extensionlast) + ge_balance_negative_tables_extensionlastvalue = (dst_negative_tables_extensionlast) + ge_balance_positive_tables_extensionlastvalue))))))))))))) -> (((exists dst_positive_code_tables_resultleft dst_positive_scale_tables_resultleft dst_negative_code_tables_resultleft dst_negative_scale_tables_resultleft. (((H) = (((((dst_positive_code_tables_resultleft) + (dst_positive_scale_tables_resultleft)) * S ((dst_positive_code_tables_resultleft) + (dst_positive_scale_tables_resultleft)) + ((dst_positive_scale_tables_resultleft) + (dst_positive_scale_tables_resultleft))) + (((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) * S ((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) + ((dst_negative_scale_tables_resultleft) + (dst_negative_scale_tables_resultleft)))) * S ((((dst_positive_code_tables_resultleft) + (dst_positive_scale_tables_resultleft)) * S ((dst_positive_code_tables_resultleft) + (dst_positive_scale_tables_resultleft)) + ((dst_positive_scale_tables_resultleft) + (dst_positive_scale_tables_resultleft))) + (((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) * S ((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) + ((dst_negative_scale_tables_resultleft) + (dst_negative_scale_tables_resultleft)))) + ((((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) * S ((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) + ((dst_negative_scale_tables_resultleft) + (dst_negative_scale_tables_resultleft))) + (((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) * S ((dst_negative_code_tables_resultleft) + (dst_negative_scale_tables_resultleft)) + ((dst_negative_scale_tables_resultleft) + (dst_negative_scale_tables_resultleft)))))) /\ (forall dst_index_tables_resultleft. (exists pvs_le_gap_tables_resultleftdomain. pvs_le_gap_tables_resultleftdomain + (dst_index_tables_resultleft) = (N)) -> exists dst_positive_tables_resultleft dst_negative_tables_resultleft dst_value_tables_resultleft. ((((exists ff_h_pvs_tables_resultleftentrypositive. ff_h_pvs_tables_resultleftentrypositive + S (dst_positive_tables_resultleft) = S ((S (dst_index_tables_resultleft)) * dst_positive_scale_tables_resultleft)) /\ exists ff_q_pvs_tables_resultleftentrypositive. dst_positive_code_tables_resultleft = ff_q_pvs_tables_resultleftentrypositive * S ((S (dst_index_tables_resultleft)) * dst_positive_scale_tables_resultleft) + (dst_positive_tables_resultleft))) /\ (((((exists ff_h_pvs_tables_resultleftentrynegative. ff_h_pvs_tables_resultleftentrynegative + S (dst_negative_tables_resultleft) = S ((S (dst_index_tables_resultleft)) * dst_negative_scale_tables_resultleft)) /\ exists ff_q_pvs_tables_resultleftentrynegative. dst_negative_code_tables_resultleft = ff_q_pvs_tables_resultleftentrynegative * S ((S (dst_index_tables_resultleft)) * dst_negative_scale_tables_resultleft) + (dst_negative_tables_resultleft))) /\ (exists ge_balance_positive_tables_resultleftentryvalue ge_balance_negative_tables_resultleftentryvalue. (((((dst_value_tables_resultleft) = 2 * (ge_balance_positive_tables_resultleftentryvalue) /\ (ge_balance_negative_tables_resultleftentryvalue) = 0) \/ exists ge_signed_half_tables_resultleftentryvaluedecode. (((dst_value_tables_resultleft) = 2 * ge_signed_half_tables_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_tables_resultleftentryvalue) = 0) /\ (ge_balance_negative_tables_resultleftentryvalue) = S ge_signed_half_tables_resultleftentryvaluedecode))) /\ ((dst_positive_tables_resultleft) + ge_balance_negative_tables_resultleftentryvalue = (dst_negative_tables_resultleft) + ge_balance_positive_tables_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_tables_resultright dst_positive_scale_tables_resultright dst_negative_code_tables_resultright dst_negative_scale_tables_resultright. (((G) = (((((dst_positive_code_tables_resultright) + (dst_positive_scale_tables_resultright)) * S ((dst_positive_code_tables_resultright) + (dst_positive_scale_tables_resultright)) + ((dst_positive_scale_tables_resultright) + (dst_positive_scale_tables_resultright))) + (((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) * S ((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) + ((dst_negative_scale_tables_resultright) + (dst_negative_scale_tables_resultright)))) * S ((((dst_positive_code_tables_resultright) + (dst_positive_scale_tables_resultright)) * S ((dst_positive_code_tables_resultright) + (dst_positive_scale_tables_resultright)) + ((dst_positive_scale_tables_resultright) + (dst_positive_scale_tables_resultright))) + (((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) * S ((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) + ((dst_negative_scale_tables_resultright) + (dst_negative_scale_tables_resultright)))) + ((((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) * S ((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) + ((dst_negative_scale_tables_resultright) + (dst_negative_scale_tables_resultright))) + (((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) * S ((dst_negative_code_tables_resultright) + (dst_negative_scale_tables_resultright)) + ((dst_negative_scale_tables_resultright) + (dst_negative_scale_tables_resultright)))))) /\ (forall dst_index_tables_resultright. (exists pvs_le_gap_tables_resultrightdomain. pvs_le_gap_tables_resultrightdomain + (dst_index_tables_resultright) = (N)) -> exists dst_positive_tables_resultright dst_negative_tables_resultright dst_value_tables_resultright. ((((exists ff_h_pvs_tables_resultrightentrypositive. ff_h_pvs_tables_resultrightentrypositive + S (dst_positive_tables_resultright) = S ((S (dst_index_tables_resultright)) * dst_positive_scale_tables_resultright)) /\ exists ff_q_pvs_tables_resultrightentrypositive. dst_positive_code_tables_resultright = ff_q_pvs_tables_resultrightentrypositive * S ((S (dst_index_tables_resultright)) * dst_positive_scale_tables_resultright) + (dst_positive_tables_resultright))) /\ (((((exists ff_h_pvs_tables_resultrightentrynegative. ff_h_pvs_tables_resultrightentrynegative + S (dst_negative_tables_resultright) = S ((S (dst_index_tables_resultright)) * dst_negative_scale_tables_resultright)) /\ exists ff_q_pvs_tables_resultrightentrynegative. dst_negative_code_tables_resultright = ff_q_pvs_tables_resultrightentrynegative * S ((S (dst_index_tables_resultright)) * dst_negative_scale_tables_resultright) + (dst_negative_tables_resultright))) /\ (exists ge_balance_positive_tables_resultrightentryvalue ge_balance_negative_tables_resultrightentryvalue. (((((dst_value_tables_resultright) = 2 * (ge_balance_positive_tables_resultrightentryvalue) /\ (ge_balance_negative_tables_resultrightentryvalue) = 0) \/ exists ge_signed_half_tables_resultrightentryvaluedecode. (((dst_value_tables_resultright) = 2 * ge_signed_half_tables_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_tables_resultrightentryvalue) = 0) /\ (ge_balance_negative_tables_resultrightentryvalue) = S ge_signed_half_tables_resultrightentryvaluedecode))) /\ ((dst_positive_tables_resultright) + ge_balance_negative_tables_resultrightentryvalue = (dst_negative_tables_resultright) + ge_balance_positive_tables_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_tables_resulttable dst_positive_scale_tables_resulttable dst_negative_code_tables_resulttable dst_negative_scale_tables_resulttable. (((K) = (((((dst_positive_code_tables_resulttable) + (dst_positive_scale_tables_resulttable)) * S ((dst_positive_code_tables_resulttable) + (dst_positive_scale_tables_resulttable)) + ((dst_positive_scale_tables_resulttable) + (dst_positive_scale_tables_resulttable))) + (((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) * S ((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) + ((dst_negative_scale_tables_resulttable) + (dst_negative_scale_tables_resulttable)))) * S ((((dst_positive_code_tables_resulttable) + (dst_positive_scale_tables_resulttable)) * S ((dst_positive_code_tables_resulttable) + (dst_positive_scale_tables_resulttable)) + ((dst_positive_scale_tables_resulttable) + (dst_positive_scale_tables_resulttable))) + (((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) * S ((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) + ((dst_negative_scale_tables_resulttable) + (dst_negative_scale_tables_resulttable)))) + ((((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) * S ((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) + ((dst_negative_scale_tables_resulttable) + (dst_negative_scale_tables_resulttable))) + (((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) * S ((dst_negative_code_tables_resulttable) + (dst_negative_scale_tables_resulttable)) + ((dst_negative_scale_tables_resulttable) + (dst_negative_scale_tables_resulttable)))))) /\ (forall dst_index_tables_resulttable. (exists pvs_le_gap_tables_resulttabledomain. pvs_le_gap_tables_resulttabledomain + (dst_index_tables_resulttable) = (N)) -> exists dst_positive_tables_resulttable dst_negative_tables_resulttable dst_value_tables_resulttable. ((((exists ff_h_pvs_tables_resulttableentrypositive. ff_h_pvs_tables_resulttableentrypositive + S (dst_positive_tables_resulttable) = S ((S (dst_index_tables_resulttable)) * dst_positive_scale_tables_resulttable)) /\ exists ff_q_pvs_tables_resulttableentrypositive. dst_positive_code_tables_resulttable = ff_q_pvs_tables_resulttableentrypositive * S ((S (dst_index_tables_resulttable)) * dst_positive_scale_tables_resulttable) + (dst_positive_tables_resulttable))) /\ (((((exists ff_h_pvs_tables_resulttableentrynegative. ff_h_pvs_tables_resulttableentrynegative + S (dst_negative_tables_resulttable) = S ((S (dst_index_tables_resulttable)) * dst_negative_scale_tables_resulttable)) /\ exists ff_q_pvs_tables_resulttableentrynegative. dst_negative_code_tables_resulttable = ff_q_pvs_tables_resulttableentrynegative * S ((S (dst_index_tables_resulttable)) * dst_negative_scale_tables_resulttable) + (dst_negative_tables_resulttable))) /\ (exists ge_balance_positive_tables_resulttableentryvalue ge_balance_negative_tables_resulttableentryvalue. (((((dst_value_tables_resulttable) = 2 * (ge_balance_positive_tables_resulttableentryvalue) /\ (ge_balance_negative_tables_resulttableentryvalue) = 0) \/ exists ge_signed_half_tables_resulttableentryvaluedecode. (((dst_value_tables_resulttable) = 2 * ge_signed_half_tables_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_tables_resulttableentryvalue) = 0) /\ (ge_balance_negative_tables_resulttableentryvalue) = S ge_signed_half_tables_resulttableentryvaluedecode))) /\ ((dst_positive_tables_resulttable) + ge_balance_negative_tables_resulttableentryvalue = (dst_negative_tables_resulttable) + ge_balance_positive_tables_resulttableentryvalue))))))))) /\ (forall dc_input_tables_result dc_output_tables_result. ~(dc_input_tables_result=0) -> (exists pvs_le_gap_tables_resultdomain. pvs_le_gap_tables_resultdomain + (dc_input_tables_result) = (N)) -> (exists dst_positive_code_tables_resultlookup dst_positive_scale_tables_resultlookup dst_negative_code_tables_resultlookup dst_negative_scale_tables_resultlookup dst_positive_tables_resultlookup dst_negative_tables_resultlookup. (((K) = (((((dst_positive_code_tables_resultlookup) + (dst_positive_scale_tables_resultlookup)) * S ((dst_positive_code_tables_resultlookup) + (dst_positive_scale_tables_resultlookup)) + ((dst_positive_scale_tables_resultlookup) + (dst_positive_scale_tables_resultlookup))) + (((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) * S ((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) + ((dst_negative_scale_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)))) * S ((((dst_positive_code_tables_resultlookup) + (dst_positive_scale_tables_resultlookup)) * S ((dst_positive_code_tables_resultlookup) + (dst_positive_scale_tables_resultlookup)) + ((dst_positive_scale_tables_resultlookup) + (dst_positive_scale_tables_resultlookup))) + (((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) * S ((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) + ((dst_negative_scale_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)))) + ((((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) * S ((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) + ((dst_negative_scale_tables_resultlookup) + (dst_negative_scale_tables_resultlookup))) + (((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) * S ((dst_negative_code_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)) + ((dst_negative_scale_tables_resultlookup) + (dst_negative_scale_tables_resultlookup)))))) /\ (((((exists ff_h_pvs_tables_resultlookuppositive. ff_h_pvs_tables_resultlookuppositive + S (dst_positive_tables_resultlookup) = S ((S (dc_input_tables_result)) * dst_positive_scale_tables_resultlookup)) /\ exists ff_q_pvs_tables_resultlookuppositive. dst_positive_code_tables_resultlookup = ff_q_pvs_tables_resultlookuppositive * S ((S (dc_input_tables_result)) * dst_positive_scale_tables_resultlookup) + (dst_positive_tables_resultlookup))) /\ (((((exists ff_h_pvs_tables_resultlookupnegative. ff_h_pvs_tables_resultlookupnegative + S (dst_negative_tables_resultlookup) = S ((S (dc_input_tables_result)) * dst_negative_scale_tables_resultlookup)) /\ exists ff_q_pvs_tables_resultlookupnegative. dst_negative_code_tables_resultlookup = ff_q_pvs_tables_resultlookupnegative * S ((S (dc_input_tables_result)) * dst_negative_scale_tables_resultlookup) + (dst_negative_tables_resultlookup))) /\ (exists ge_balance_positive_tables_resultlookupvalue ge_balance_negative_tables_resultlookupvalue. (((((dc_output_tables_result) = 2 * (ge_balance_positive_tables_resultlookupvalue) /\ (ge_balance_negative_tables_resultlookupvalue) = 0) \/ exists ge_signed_half_tables_resultlookupvaluedecode. (((dc_output_tables_result) = 2 * ge_signed_half_tables_resultlookupvaluedecode + 1 /\ (ge_balance_positive_tables_resultlookupvalue) = 0) /\ (ge_balance_negative_tables_resultlookupvalue) = S ge_signed_half_tables_resultlookupvaluedecode))) /\ ((dst_positive_tables_resultlookup) + ge_balance_negative_tables_resultlookupvalue = (dst_negative_tables_resultlookup) + ge_balance_positive_tables_resultlookupvalue))))))))) -> (((~((dc_input_tables_result)=0)) /\ (exists dc_mask_tables_resultvalue. ((((exists dst_positive_code_tables_resultvaluemasktable dst_positive_scale_tables_resultvaluemasktable dst_negative_code_tables_resultvaluemasktable dst_negative_scale_tables_resultvaluemasktable. (((dc_mask_tables_resultvalue) = (((((dst_positive_code_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable)) * S ((dst_positive_code_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable)) + ((dst_positive_scale_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable))) + (((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) * S ((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) + ((dst_negative_scale_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)))) * S ((((dst_positive_code_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable)) * S ((dst_positive_code_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable)) + ((dst_positive_scale_tables_resultvaluemasktable) + (dst_positive_scale_tables_resultvaluemasktable))) + (((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) * S ((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) + ((dst_negative_scale_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)))) + ((((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) * S ((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) + ((dst_negative_scale_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable))) + (((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) * S ((dst_negative_code_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)) + ((dst_negative_scale_tables_resultvaluemasktable) + (dst_negative_scale_tables_resultvaluemasktable)))))) /\ (forall dst_index_tables_resultvaluemasktable. (exists pvs_le_gap_tables_resultvaluemasktabledomain. pvs_le_gap_tables_resultvaluemasktabledomain + (dst_index_tables_resultvaluemasktable) = (dc_input_tables_result)) -> exists dst_positive_tables_resultvaluemasktable dst_negative_tables_resultvaluemasktable dst_value_tables_resultvaluemasktable. ((((exists ff_h_pvs_tables_resultvaluemasktableentrypositive. ff_h_pvs_tables_resultvaluemasktableentrypositive + S (dst_positive_tables_resultvaluemasktable) = S ((S (dst_index_tables_resultvaluemasktable)) * dst_positive_scale_tables_resultvaluemasktable)) /\ exists ff_q_pvs_tables_resultvaluemasktableentrypositive. dst_positive_code_tables_resultvaluemasktable = ff_q_pvs_tables_resultvaluemasktableentrypositive * S ((S (dst_index_tables_resultvaluemasktable)) * dst_positive_scale_tables_resultvaluemasktable) + (dst_positive_tables_resultvaluemasktable))) /\ (((((exists ff_h_pvs_tables_resultvaluemasktableentrynegative. ff_h_pvs_tables_resultvaluemasktableentrynegative + S (dst_negative_tables_resultvaluemasktable) = S ((S (dst_index_tables_resultvaluemasktable)) * dst_negative_scale_tables_resultvaluemasktable)) /\ exists ff_q_pvs_tables_resultvaluemasktableentrynegative. dst_negative_code_tables_resultvaluemasktable = ff_q_pvs_tables_resultvaluemasktableentrynegative * S ((S (dst_index_tables_resultvaluemasktable)) * dst_negative_scale_tables_resultvaluemasktable) + (dst_negative_tables_resultvaluemasktable))) /\ (exists ge_balance_positive_tables_resultvaluemasktableentryvalue ge_balance_negative_tables_resultvaluemasktableentryvalue. (((((dst_value_tables_resultvaluemasktable) = 2 * (ge_balance_positive_tables_resultvaluemasktableentryvalue) /\ (ge_balance_negative_tables_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_tables_resultvaluemasktableentryvaluedecode. (((dst_value_tables_resultvaluemasktable) = 2 * ge_signed_half_tables_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_tables_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_tables_resultvaluemasktableentryvalue) = S ge_signed_half_tables_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_tables_resultvaluemasktable) + ge_balance_negative_tables_resultvaluemasktableentryvalue = (dst_negative_tables_resultvaluemasktable) + ge_balance_positive_tables_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_tables_resultvaluemask dc_value_tables_resultvaluemask. (exists pvs_le_gap_tables_resultvaluemaskdomain. pvs_le_gap_tables_resultvaluemaskdomain + (dc_index_tables_resultvaluemask) = (dc_input_tables_result)) -> (exists dst_positive_code_tables_resultvaluemasklookup dst_positive_scale_tables_resultvaluemasklookup dst_negative_code_tables_resultvaluemasklookup dst_negative_scale_tables_resultvaluemasklookup dst_positive_tables_resultvaluemasklookup dst_negative_tables_resultvaluemasklookup. (((dc_mask_tables_resultvalue) = (((((dst_positive_code_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup)) * S ((dst_positive_code_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup)) + ((dst_positive_scale_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup))) + (((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) * S ((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) + ((dst_negative_scale_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)))) * S ((((dst_positive_code_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup)) * S ((dst_positive_code_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup)) + ((dst_positive_scale_tables_resultvaluemasklookup) + (dst_positive_scale_tables_resultvaluemasklookup))) + (((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) * S ((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) + ((dst_negative_scale_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)))) + ((((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) * S ((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) + ((dst_negative_scale_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup))) + (((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) * S ((dst_negative_code_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)) + ((dst_negative_scale_tables_resultvaluemasklookup) + (dst_negative_scale_tables_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_tables_resultvaluemasklookuppositive. ff_h_pvs_tables_resultvaluemasklookuppositive + S (dst_positive_tables_resultvaluemasklookup) = S ((S (dc_index_tables_resultvaluemask)) * dst_positive_scale_tables_resultvaluemasklookup)) /\ exists ff_q_pvs_tables_resultvaluemasklookuppositive. dst_positive_code_tables_resultvaluemasklookup = ff_q_pvs_tables_resultvaluemasklookuppositive * S ((S (dc_index_tables_resultvaluemask)) * dst_positive_scale_tables_resultvaluemasklookup) + (dst_positive_tables_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_tables_resultvaluemasklookupnegative. ff_h_pvs_tables_resultvaluemasklookupnegative + S (dst_negative_tables_resultvaluemasklookup) = S ((S (dc_index_tables_resultvaluemask)) * dst_negative_scale_tables_resultvaluemasklookup)) /\ exists ff_q_pvs_tables_resultvaluemasklookupnegative. dst_negative_code_tables_resultvaluemasklookup = ff_q_pvs_tables_resultvaluemasklookupnegative * S ((S (dc_index_tables_resultvaluemask)) * dst_negative_scale_tables_resultvaluemasklookup) + (dst_negative_tables_resultvaluemasklookup))) /\ (exists ge_balance_positive_tables_resultvaluemasklookupvalue ge_balance_negative_tables_resultvaluemasklookupvalue. (((((dc_value_tables_resultvaluemask) = 2 * (ge_balance_positive_tables_resultvaluemasklookupvalue) /\ (ge_balance_negative_tables_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_tables_resultvaluemasklookupvaluedecode. (((dc_value_tables_resultvaluemask) = 2 * ge_signed_half_tables_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_tables_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_tables_resultvaluemasklookupvalue) = S ge_signed_half_tables_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_tables_resultvaluemasklookup) + ge_balance_negative_tables_resultvaluemasklookupvalue = (dst_negative_tables_resultvaluemasklookup) + ge_balance_positive_tables_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_tables_resultvaluemask)=0)) /\ (exists dc_quotient_tables_resultvaluemaskentry dc_left_tables_resultvaluemaskentry dc_right_tables_resultvaluemaskentry. (((dc_input_tables_result)=(dc_index_tables_resultvaluemask)*dc_quotient_tables_resultvaluemaskentry) /\ (((exists dst_positive_code_tables_resultvaluemaskentryleft dst_positive_scale_tables_resultvaluemaskentryleft dst_negative_code_tables_resultvaluemaskentryleft dst_negative_scale_tables_resultvaluemaskentryleft dst_positive_tables_resultvaluemaskentryleft dst_negative_tables_resultvaluemaskentryleft. (((H) = (((((dst_positive_code_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft)) * S ((dst_positive_code_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft)) + ((dst_positive_scale_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft))) + (((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) * S ((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) + ((dst_negative_scale_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)))) * S ((((dst_positive_code_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft)) * S ((dst_positive_code_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft)) + ((dst_positive_scale_tables_resultvaluemaskentryleft) + (dst_positive_scale_tables_resultvaluemaskentryleft))) + (((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) * S ((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) + ((dst_negative_scale_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)))) + ((((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) * S ((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) + ((dst_negative_scale_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft))) + (((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) * S ((dst_negative_code_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)) + ((dst_negative_scale_tables_resultvaluemaskentryleft) + (dst_negative_scale_tables_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_tables_resultvaluemaskentryleftpositive. ff_h_pvs_tables_resultvaluemaskentryleftpositive + S (dst_positive_tables_resultvaluemaskentryleft) = S ((S (dc_index_tables_resultvaluemask)) * dst_positive_scale_tables_resultvaluemaskentryleft)) /\ exists ff_q_pvs_tables_resultvaluemaskentryleftpositive. dst_positive_code_tables_resultvaluemaskentryleft = ff_q_pvs_tables_resultvaluemaskentryleftpositive * S ((S (dc_index_tables_resultvaluemask)) * dst_positive_scale_tables_resultvaluemaskentryleft) + (dst_positive_tables_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_tables_resultvaluemaskentryleftnegative. ff_h_pvs_tables_resultvaluemaskentryleftnegative + S (dst_negative_tables_resultvaluemaskentryleft) = S ((S (dc_index_tables_resultvaluemask)) * dst_negative_scale_tables_resultvaluemaskentryleft)) /\ exists ff_q_pvs_tables_resultvaluemaskentryleftnegative. dst_negative_code_tables_resultvaluemaskentryleft = ff_q_pvs_tables_resultvaluemaskentryleftnegative * S ((S (dc_index_tables_resultvaluemask)) * dst_negative_scale_tables_resultvaluemaskentryleft) + (dst_negative_tables_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_tables_resultvaluemaskentryleftvalue ge_balance_negative_tables_resultvaluemaskentryleftvalue. (((((dc_left_tables_resultvaluemaskentry) = 2 * (ge_balance_positive_tables_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_tables_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_tables_resultvaluemaskentryleftvaluedecode. (((dc_left_tables_resultvaluemaskentry) = 2 * ge_signed_half_tables_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_tables_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_tables_resultvaluemaskentryleftvalue) = S ge_signed_half_tables_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_tables_resultvaluemaskentryleft) + ge_balance_negative_tables_resultvaluemaskentryleftvalue = (dst_negative_tables_resultvaluemaskentryleft) + ge_balance_positive_tables_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_tables_resultvaluemaskentryright dst_positive_scale_tables_resultvaluemaskentryright dst_negative_code_tables_resultvaluemaskentryright dst_negative_scale_tables_resultvaluemaskentryright dst_positive_tables_resultvaluemaskentryright dst_negative_tables_resultvaluemaskentryright. (((G) = (((((dst_positive_code_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright)) * S ((dst_positive_code_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright)) + ((dst_positive_scale_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright))) + (((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) * S ((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) + ((dst_negative_scale_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)))) * S ((((dst_positive_code_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright)) * S ((dst_positive_code_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright)) + ((dst_positive_scale_tables_resultvaluemaskentryright) + (dst_positive_scale_tables_resultvaluemaskentryright))) + (((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) * S ((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) + ((dst_negative_scale_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)))) + ((((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) * S ((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) + ((dst_negative_scale_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright))) + (((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) * S ((dst_negative_code_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)) + ((dst_negative_scale_tables_resultvaluemaskentryright) + (dst_negative_scale_tables_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_tables_resultvaluemaskentryrightpositive. ff_h_pvs_tables_resultvaluemaskentryrightpositive + S (dst_positive_tables_resultvaluemaskentryright) = S ((S (dc_quotient_tables_resultvaluemaskentry)) * dst_positive_scale_tables_resultvaluemaskentryright)) /\ exists ff_q_pvs_tables_resultvaluemaskentryrightpositive. dst_positive_code_tables_resultvaluemaskentryright = ff_q_pvs_tables_resultvaluemaskentryrightpositive * S ((S (dc_quotient_tables_resultvaluemaskentry)) * dst_positive_scale_tables_resultvaluemaskentryright) + (dst_positive_tables_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_tables_resultvaluemaskentryrightnegative. ff_h_pvs_tables_resultvaluemaskentryrightnegative + S (dst_negative_tables_resultvaluemaskentryright) = S ((S (dc_quotient_tables_resultvaluemaskentry)) * dst_negative_scale_tables_resultvaluemaskentryright)) /\ exists ff_q_pvs_tables_resultvaluemaskentryrightnegative. dst_negative_code_tables_resultvaluemaskentryright = ff_q_pvs_tables_resultvaluemaskentryrightnegative * S ((S (dc_quotient_tables_resultvaluemaskentry)) * dst_negative_scale_tables_resultvaluemaskentryright) + (dst_negative_tables_resultvaluemaskentryright))) /\ (exists ge_balance_positive_tables_resultvaluemaskentryrightvalue ge_balance_negative_tables_resultvaluemaskentryrightvalue. (((((dc_right_tables_resultvaluemaskentry) = 2 * (ge_balance_positive_tables_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_tables_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_tables_resultvaluemaskentryrightvaluedecode. (((dc_right_tables_resultvaluemaskentry) = 2 * ge_signed_half_tables_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_tables_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_tables_resultvaluemaskentryrightvalue) = S ge_signed_half_tables_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_tables_resultvaluemaskentryright) + ge_balance_negative_tables_resultvaluemaskentryrightvalue = (dst_negative_tables_resultvaluemaskentryright) + ge_balance_positive_tables_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_tables_resultvaluemaskentryproduct sto_an_tables_resultvaluemaskentryproduct sto_bp_tables_resultvaluemaskentryproduct sto_bn_tables_resultvaluemaskentryproduct sto_cp_tables_resultvaluemaskentryproduct sto_cn_tables_resultvaluemaskentryproduct. (((((dc_left_tables_resultvaluemaskentry) = 2 * (sto_ap_tables_resultvaluemaskentryproduct) /\ (sto_an_tables_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_resultvaluemaskentryproductleft. (((dc_left_tables_resultvaluemaskentry) = 2 * ge_signed_half_tables_resultvaluemaskentryproductleft + 1 /\ (sto_ap_tables_resultvaluemaskentryproduct) = 0) /\ (sto_an_tables_resultvaluemaskentryproduct) = S ge_signed_half_tables_resultvaluemaskentryproductleft))) /\ ((((((dc_right_tables_resultvaluemaskentry) = 2 * (sto_bp_tables_resultvaluemaskentryproduct) /\ (sto_bn_tables_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_resultvaluemaskentryproductright. (((dc_right_tables_resultvaluemaskentry) = 2 * ge_signed_half_tables_resultvaluemaskentryproductright + 1 /\ (sto_bp_tables_resultvaluemaskentryproduct) = 0) /\ (sto_bn_tables_resultvaluemaskentryproduct) = S ge_signed_half_tables_resultvaluemaskentryproductright))) /\ ((((((dc_value_tables_resultvaluemask) = 2 * (sto_cp_tables_resultvaluemaskentryproduct) /\ (sto_cn_tables_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_tables_resultvaluemaskentryproductoutput. (((dc_value_tables_resultvaluemask) = 2 * ge_signed_half_tables_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_tables_resultvaluemaskentryproduct) = 0) /\ (sto_cn_tables_resultvaluemaskentryproduct) = S ge_signed_half_tables_resultvaluemaskentryproductoutput))) /\ ((sto_ap_tables_resultvaluemaskentryproduct * sto_bp_tables_resultvaluemaskentryproduct + sto_an_tables_resultvaluemaskentryproduct * sto_bn_tables_resultvaluemaskentryproduct) + sto_cn_tables_resultvaluemaskentryproduct = (sto_ap_tables_resultvaluemaskentryproduct * sto_bn_tables_resultvaluemaskentryproduct + sto_an_tables_resultvaluemaskentryproduct * sto_bp_tables_resultvaluemaskentryproduct) + sto_cp_tables_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_tables_resultvaluemask)=0 \/ ~(exists pvs_factor_tables_resultvaluemaskentrynondivisor. (dc_input_tables_result) = (dc_index_tables_resultvaluemask) * pvs_factor_tables_resultvaluemaskentrynondivisor)) /\ ((dc_value_tables_resultvaluemask)=0))))))) /\ (exists dst_positive_code_tables_resultvaluefold dst_positive_scale_tables_resultvaluefold dst_negative_code_tables_resultvaluefold dst_negative_scale_tables_resultvaluefold dst_positive_sum_tables_resultvaluefold dst_negative_sum_tables_resultvaluefold. (((dc_mask_tables_resultvalue) = (((((dst_positive_code_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold)) * S ((dst_positive_code_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold)) + ((dst_positive_scale_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold))) + (((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) * S ((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) + ((dst_negative_scale_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)))) * S ((((dst_positive_code_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold)) * S ((dst_positive_code_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold)) + ((dst_positive_scale_tables_resultvaluefold) + (dst_positive_scale_tables_resultvaluefold))) + (((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) * S ((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) + ((dst_negative_scale_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)))) + ((((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) * S ((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) + ((dst_negative_scale_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold))) + (((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) * S ((dst_negative_code_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)) + ((dst_negative_scale_tables_resultvaluefold) + (dst_negative_scale_tables_resultvaluefold)))))) /\ (((exists fs_u_dst_tables_resultvaluefoldpositive fs_v_dst_tables_resultvaluefoldpositive. ((((exists fs_h_dst_tables_resultvaluefoldpositive_body_start. fs_h_dst_tables_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tables_resultvaluefoldpositive)) /\ exists fs_q_dst_tables_resultvaluefoldpositive_body_start. fs_u_dst_tables_resultvaluefoldpositive = fs_q_dst_tables_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_tables_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_tables_resultvaluefoldpositive_body_terminal. fs_h_dst_tables_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_tables_resultvaluefold) = S ((S (S (dc_input_tables_result))) * fs_v_dst_tables_resultvaluefoldpositive)) /\ exists fs_q_dst_tables_resultvaluefoldpositive_body_terminal. fs_u_dst_tables_resultvaluefoldpositive = fs_q_dst_tables_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_tables_result))) * fs_v_dst_tables_resultvaluefoldpositive) + (dst_positive_sum_tables_resultvaluefold))) /\ forall fs_i_dst_tables_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_tables_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_tables_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_tables_resultvaluefoldpositive_body_steps = S (dc_input_tables_result)) -> exists fs_a_dst_tables_resultvaluefoldpositive_body_steps fs_r_dst_tables_resultvaluefoldpositive_body_steps fs_s_dst_tables_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_tables_resultvaluefoldpositive_body_steps_summand. fs_h_dst_tables_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_tables_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * dst_positive_scale_tables_resultvaluefold)) /\ exists fs_q_dst_tables_resultvaluefoldpositive_body_steps_summand. dst_positive_code_tables_resultvaluefold = fs_q_dst_tables_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * dst_positive_scale_tables_resultvaluefold) + (fs_a_dst_tables_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_tables_resultvaluefoldpositive_body_steps_partial. fs_h_dst_tables_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_tables_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * fs_v_dst_tables_resultvaluefoldpositive)) /\ exists fs_q_dst_tables_resultvaluefoldpositive_body_steps_partial. fs_u_dst_tables_resultvaluefoldpositive = fs_q_dst_tables_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * fs_v_dst_tables_resultvaluefoldpositive) + (fs_r_dst_tables_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_tables_resultvaluefoldpositive_body_steps_successor. fs_h_dst_tables_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_tables_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * fs_v_dst_tables_resultvaluefoldpositive)) /\ exists fs_q_dst_tables_resultvaluefoldpositive_body_steps_successor. fs_u_dst_tables_resultvaluefoldpositive = fs_q_dst_tables_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_tables_resultvaluefoldpositive_body_steps)) * fs_v_dst_tables_resultvaluefoldpositive) + (fs_s_dst_tables_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_tables_resultvaluefoldpositive_body_steps = fs_r_dst_tables_resultvaluefoldpositive_body_steps + fs_a_dst_tables_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_tables_resultvaluefoldnegative fs_v_dst_tables_resultvaluefoldnegative. ((((exists fs_h_dst_tables_resultvaluefoldnegative_body_start. fs_h_dst_tables_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tables_resultvaluefoldnegative)) /\ exists fs_q_dst_tables_resultvaluefoldnegative_body_start. fs_u_dst_tables_resultvaluefoldnegative = fs_q_dst_tables_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_tables_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_tables_resultvaluefoldnegative_body_terminal. fs_h_dst_tables_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_tables_resultvaluefold) = S ((S (S (dc_input_tables_result))) * fs_v_dst_tables_resultvaluefoldnegative)) /\ exists fs_q_dst_tables_resultvaluefoldnegative_body_terminal. fs_u_dst_tables_resultvaluefoldnegative = fs_q_dst_tables_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_tables_result))) * fs_v_dst_tables_resultvaluefoldnegative) + (dst_negative_sum_tables_resultvaluefold))) /\ forall fs_i_dst_tables_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_tables_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_tables_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_tables_resultvaluefoldnegative_body_steps = S (dc_input_tables_result)) -> exists fs_a_dst_tables_resultvaluefoldnegative_body_steps fs_r_dst_tables_resultvaluefoldnegative_body_steps fs_s_dst_tables_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_tables_resultvaluefoldnegative_body_steps_summand. fs_h_dst_tables_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_tables_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * dst_negative_scale_tables_resultvaluefold)) /\ exists fs_q_dst_tables_resultvaluefoldnegative_body_steps_summand. dst_negative_code_tables_resultvaluefold = fs_q_dst_tables_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * dst_negative_scale_tables_resultvaluefold) + (fs_a_dst_tables_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_tables_resultvaluefoldnegative_body_steps_partial. fs_h_dst_tables_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_tables_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * fs_v_dst_tables_resultvaluefoldnegative)) /\ exists fs_q_dst_tables_resultvaluefoldnegative_body_steps_partial. fs_u_dst_tables_resultvaluefoldnegative = fs_q_dst_tables_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * fs_v_dst_tables_resultvaluefoldnegative) + (fs_r_dst_tables_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_tables_resultvaluefoldnegative_body_steps_successor. fs_h_dst_tables_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_tables_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * fs_v_dst_tables_resultvaluefoldnegative)) /\ exists fs_q_dst_tables_resultvaluefoldnegative_body_steps_successor. fs_u_dst_tables_resultvaluefoldnegative = fs_q_dst_tables_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_tables_resultvaluefoldnegative_body_steps)) * fs_v_dst_tables_resultvaluefoldnegative) + (fs_s_dst_tables_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_tables_resultvaluefoldnegative_body_steps = fs_r_dst_tables_resultvaluefoldnegative_body_steps + fs_a_dst_tables_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_tables_resultvaluefoldresult ge_balance_negative_tables_resultvaluefoldresult. (((((dc_output_tables_result) = 2 * (ge_balance_positive_tables_resultvaluefoldresult) /\ (ge_balance_negative_tables_resultvaluefoldresult) = 0) \/ exists ge_signed_half_tables_resultvaluefoldresultdecode. (((dc_output_tables_result) = 2 * ge_signed_half_tables_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_tables_resultvaluefoldresult) = 0) /\ (ge_balance_negative_tables_resultvaluefoldresult) = S ge_signed_half_tables_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_tables_resultvaluefold) + ge_balance_negative_tables_resultvaluefoldresult = (dst_negative_sum_tables_resultvaluefold) + ge_balance_positive_tables_resultvaluefoldresult))))))))))))))))))))