dirichlet_convolution_table_zero_constructor

Exact expanded first-order arithmetic statement

forall F G H. (exists dst_positive_code_table_zero_left dst_positive_scale_table_zero_left dst_negative_code_table_zero_left dst_negative_scale_table_zero_left. (((F) = (((((dst_positive_code_table_zero_left) + (dst_positive_scale_table_zero_left)) * S ((dst_positive_code_table_zero_left) + (dst_positive_scale_table_zero_left)) + ((dst_positive_scale_table_zero_left) + (dst_positive_scale_table_zero_left))) + (((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) * S ((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) + ((dst_negative_scale_table_zero_left) + (dst_negative_scale_table_zero_left)))) * S ((((dst_positive_code_table_zero_left) + (dst_positive_scale_table_zero_left)) * S ((dst_positive_code_table_zero_left) + (dst_positive_scale_table_zero_left)) + ((dst_positive_scale_table_zero_left) + (dst_positive_scale_table_zero_left))) + (((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) * S ((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) + ((dst_negative_scale_table_zero_left) + (dst_negative_scale_table_zero_left)))) + ((((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) * S ((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) + ((dst_negative_scale_table_zero_left) + (dst_negative_scale_table_zero_left))) + (((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) * S ((dst_negative_code_table_zero_left) + (dst_negative_scale_table_zero_left)) + ((dst_negative_scale_table_zero_left) + (dst_negative_scale_table_zero_left)))))) /\ (forall dst_index_table_zero_left. (exists pvs_le_gap_table_zero_leftdomain. pvs_le_gap_table_zero_leftdomain + (dst_index_table_zero_left) = (0)) -> exists dst_positive_table_zero_left dst_negative_table_zero_left dst_value_table_zero_left. ((((exists ff_h_pvs_table_zero_leftentrypositive. ff_h_pvs_table_zero_leftentrypositive + S (dst_positive_table_zero_left) = S ((S (dst_index_table_zero_left)) * dst_positive_scale_table_zero_left)) /\ exists ff_q_pvs_table_zero_leftentrypositive. dst_positive_code_table_zero_left = ff_q_pvs_table_zero_leftentrypositive * S ((S (dst_index_table_zero_left)) * dst_positive_scale_table_zero_left) + (dst_positive_table_zero_left))) /\ (((((exists ff_h_pvs_table_zero_leftentrynegative. ff_h_pvs_table_zero_leftentrynegative + S (dst_negative_table_zero_left) = S ((S (dst_index_table_zero_left)) * dst_negative_scale_table_zero_left)) /\ exists ff_q_pvs_table_zero_leftentrynegative. dst_negative_code_table_zero_left = ff_q_pvs_table_zero_leftentrynegative * S ((S (dst_index_table_zero_left)) * dst_negative_scale_table_zero_left) + (dst_negative_table_zero_left))) /\ (exists ge_balance_positive_table_zero_leftentryvalue ge_balance_negative_table_zero_leftentryvalue. (((((dst_value_table_zero_left) = 2 * (ge_balance_positive_table_zero_leftentryvalue) /\ (ge_balance_negative_table_zero_leftentryvalue) = 0) \/ exists ge_signed_half_table_zero_leftentryvaluedecode. (((dst_value_table_zero_left) = 2 * ge_signed_half_table_zero_leftentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_leftentryvalue) = 0) /\ (ge_balance_negative_table_zero_leftentryvalue) = S ge_signed_half_table_zero_leftentryvaluedecode))) /\ ((dst_positive_table_zero_left) + ge_balance_negative_table_zero_leftentryvalue = (dst_negative_table_zero_left) + ge_balance_positive_table_zero_leftentryvalue))))))))) -> (exists dst_positive_code_table_zero_right dst_positive_scale_table_zero_right dst_negative_code_table_zero_right dst_negative_scale_table_zero_right. (((G) = (((((dst_positive_code_table_zero_right) + (dst_positive_scale_table_zero_right)) * S ((dst_positive_code_table_zero_right) + (dst_positive_scale_table_zero_right)) + ((dst_positive_scale_table_zero_right) + (dst_positive_scale_table_zero_right))) + (((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) * S ((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) + ((dst_negative_scale_table_zero_right) + (dst_negative_scale_table_zero_right)))) * S ((((dst_positive_code_table_zero_right) + (dst_positive_scale_table_zero_right)) * S ((dst_positive_code_table_zero_right) + (dst_positive_scale_table_zero_right)) + ((dst_positive_scale_table_zero_right) + (dst_positive_scale_table_zero_right))) + (((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) * S ((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) + ((dst_negative_scale_table_zero_right) + (dst_negative_scale_table_zero_right)))) + ((((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) * S ((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) + ((dst_negative_scale_table_zero_right) + (dst_negative_scale_table_zero_right))) + (((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) * S ((dst_negative_code_table_zero_right) + (dst_negative_scale_table_zero_right)) + ((dst_negative_scale_table_zero_right) + (dst_negative_scale_table_zero_right)))))) /\ (forall dst_index_table_zero_right. (exists pvs_le_gap_table_zero_rightdomain. pvs_le_gap_table_zero_rightdomain + (dst_index_table_zero_right) = (0)) -> exists dst_positive_table_zero_right dst_negative_table_zero_right dst_value_table_zero_right. ((((exists ff_h_pvs_table_zero_rightentrypositive. ff_h_pvs_table_zero_rightentrypositive + S (dst_positive_table_zero_right) = S ((S (dst_index_table_zero_right)) * dst_positive_scale_table_zero_right)) /\ exists ff_q_pvs_table_zero_rightentrypositive. dst_positive_code_table_zero_right = ff_q_pvs_table_zero_rightentrypositive * S ((S (dst_index_table_zero_right)) * dst_positive_scale_table_zero_right) + (dst_positive_table_zero_right))) /\ (((((exists ff_h_pvs_table_zero_rightentrynegative. ff_h_pvs_table_zero_rightentrynegative + S (dst_negative_table_zero_right) = S ((S (dst_index_table_zero_right)) * dst_negative_scale_table_zero_right)) /\ exists ff_q_pvs_table_zero_rightentrynegative. dst_negative_code_table_zero_right = ff_q_pvs_table_zero_rightentrynegative * S ((S (dst_index_table_zero_right)) * dst_negative_scale_table_zero_right) + (dst_negative_table_zero_right))) /\ (exists ge_balance_positive_table_zero_rightentryvalue ge_balance_negative_table_zero_rightentryvalue. (((((dst_value_table_zero_right) = 2 * (ge_balance_positive_table_zero_rightentryvalue) /\ (ge_balance_negative_table_zero_rightentryvalue) = 0) \/ exists ge_signed_half_table_zero_rightentryvaluedecode. (((dst_value_table_zero_right) = 2 * ge_signed_half_table_zero_rightentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_rightentryvalue) = 0) /\ (ge_balance_negative_table_zero_rightentryvalue) = S ge_signed_half_table_zero_rightentryvaluedecode))) /\ ((dst_positive_table_zero_right) + ge_balance_negative_table_zero_rightentryvalue = (dst_negative_table_zero_right) + ge_balance_positive_table_zero_rightentryvalue))))))))) -> (exists dst_positive_code_table_zero_output dst_positive_scale_table_zero_output dst_negative_code_table_zero_output dst_negative_scale_table_zero_output. (((H) = (((((dst_positive_code_table_zero_output) + (dst_positive_scale_table_zero_output)) * S ((dst_positive_code_table_zero_output) + (dst_positive_scale_table_zero_output)) + ((dst_positive_scale_table_zero_output) + (dst_positive_scale_table_zero_output))) + (((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) * S ((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) + ((dst_negative_scale_table_zero_output) + (dst_negative_scale_table_zero_output)))) * S ((((dst_positive_code_table_zero_output) + (dst_positive_scale_table_zero_output)) * S ((dst_positive_code_table_zero_output) + (dst_positive_scale_table_zero_output)) + ((dst_positive_scale_table_zero_output) + (dst_positive_scale_table_zero_output))) + (((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) * S ((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) + ((dst_negative_scale_table_zero_output) + (dst_negative_scale_table_zero_output)))) + ((((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) * S ((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) + ((dst_negative_scale_table_zero_output) + (dst_negative_scale_table_zero_output))) + (((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) * S ((dst_negative_code_table_zero_output) + (dst_negative_scale_table_zero_output)) + ((dst_negative_scale_table_zero_output) + (dst_negative_scale_table_zero_output)))))) /\ (forall dst_index_table_zero_output. (exists pvs_le_gap_table_zero_outputdomain. pvs_le_gap_table_zero_outputdomain + (dst_index_table_zero_output) = (0)) -> exists dst_positive_table_zero_output dst_negative_table_zero_output dst_value_table_zero_output. ((((exists ff_h_pvs_table_zero_outputentrypositive. ff_h_pvs_table_zero_outputentrypositive + S (dst_positive_table_zero_output) = S ((S (dst_index_table_zero_output)) * dst_positive_scale_table_zero_output)) /\ exists ff_q_pvs_table_zero_outputentrypositive. dst_positive_code_table_zero_output = ff_q_pvs_table_zero_outputentrypositive * S ((S (dst_index_table_zero_output)) * dst_positive_scale_table_zero_output) + (dst_positive_table_zero_output))) /\ (((((exists ff_h_pvs_table_zero_outputentrynegative. ff_h_pvs_table_zero_outputentrynegative + S (dst_negative_table_zero_output) = S ((S (dst_index_table_zero_output)) * dst_negative_scale_table_zero_output)) /\ exists ff_q_pvs_table_zero_outputentrynegative. dst_negative_code_table_zero_output = ff_q_pvs_table_zero_outputentrynegative * S ((S (dst_index_table_zero_output)) * dst_negative_scale_table_zero_output) + (dst_negative_table_zero_output))) /\ (exists ge_balance_positive_table_zero_outputentryvalue ge_balance_negative_table_zero_outputentryvalue. (((((dst_value_table_zero_output) = 2 * (ge_balance_positive_table_zero_outputentryvalue) /\ (ge_balance_negative_table_zero_outputentryvalue) = 0) \/ exists ge_signed_half_table_zero_outputentryvaluedecode. (((dst_value_table_zero_output) = 2 * ge_signed_half_table_zero_outputentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_outputentryvalue) = 0) /\ (ge_balance_negative_table_zero_outputentryvalue) = S ge_signed_half_table_zero_outputentryvaluedecode))) /\ ((dst_positive_table_zero_output) + ge_balance_negative_table_zero_outputentryvalue = (dst_negative_table_zero_output) + ge_balance_positive_table_zero_outputentryvalue))))))))) -> (((exists dst_positive_code_table_zero_resultleft dst_positive_scale_table_zero_resultleft dst_negative_code_table_zero_resultleft dst_negative_scale_table_zero_resultleft. (((F) = (((((dst_positive_code_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft)) * S ((dst_positive_code_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft)) + ((dst_positive_scale_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft))) + (((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) * S ((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) + ((dst_negative_scale_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)))) * S ((((dst_positive_code_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft)) * S ((dst_positive_code_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft)) + ((dst_positive_scale_table_zero_resultleft) + (dst_positive_scale_table_zero_resultleft))) + (((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) * S ((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) + ((dst_negative_scale_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)))) + ((((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) * S ((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) + ((dst_negative_scale_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft))) + (((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) * S ((dst_negative_code_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)) + ((dst_negative_scale_table_zero_resultleft) + (dst_negative_scale_table_zero_resultleft)))))) /\ (forall dst_index_table_zero_resultleft. (exists pvs_le_gap_table_zero_resultleftdomain. pvs_le_gap_table_zero_resultleftdomain + (dst_index_table_zero_resultleft) = (0)) -> exists dst_positive_table_zero_resultleft dst_negative_table_zero_resultleft dst_value_table_zero_resultleft. ((((exists ff_h_pvs_table_zero_resultleftentrypositive. ff_h_pvs_table_zero_resultleftentrypositive + S (dst_positive_table_zero_resultleft) = S ((S (dst_index_table_zero_resultleft)) * dst_positive_scale_table_zero_resultleft)) /\ exists ff_q_pvs_table_zero_resultleftentrypositive. dst_positive_code_table_zero_resultleft = ff_q_pvs_table_zero_resultleftentrypositive * S ((S (dst_index_table_zero_resultleft)) * dst_positive_scale_table_zero_resultleft) + (dst_positive_table_zero_resultleft))) /\ (((((exists ff_h_pvs_table_zero_resultleftentrynegative. ff_h_pvs_table_zero_resultleftentrynegative + S (dst_negative_table_zero_resultleft) = S ((S (dst_index_table_zero_resultleft)) * dst_negative_scale_table_zero_resultleft)) /\ exists ff_q_pvs_table_zero_resultleftentrynegative. dst_negative_code_table_zero_resultleft = ff_q_pvs_table_zero_resultleftentrynegative * S ((S (dst_index_table_zero_resultleft)) * dst_negative_scale_table_zero_resultleft) + (dst_negative_table_zero_resultleft))) /\ (exists ge_balance_positive_table_zero_resultleftentryvalue ge_balance_negative_table_zero_resultleftentryvalue. (((((dst_value_table_zero_resultleft) = 2 * (ge_balance_positive_table_zero_resultleftentryvalue) /\ (ge_balance_negative_table_zero_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_zero_resultleftentryvaluedecode. (((dst_value_table_zero_resultleft) = 2 * ge_signed_half_table_zero_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_zero_resultleftentryvalue) = S ge_signed_half_table_zero_resultleftentryvaluedecode))) /\ ((dst_positive_table_zero_resultleft) + ge_balance_negative_table_zero_resultleftentryvalue = (dst_negative_table_zero_resultleft) + ge_balance_positive_table_zero_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_zero_resultright dst_positive_scale_table_zero_resultright dst_negative_code_table_zero_resultright dst_negative_scale_table_zero_resultright. (((G) = (((((dst_positive_code_table_zero_resultright) + (dst_positive_scale_table_zero_resultright)) * S ((dst_positive_code_table_zero_resultright) + (dst_positive_scale_table_zero_resultright)) + ((dst_positive_scale_table_zero_resultright) + (dst_positive_scale_table_zero_resultright))) + (((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) * S ((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) + ((dst_negative_scale_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)))) * S ((((dst_positive_code_table_zero_resultright) + (dst_positive_scale_table_zero_resultright)) * S ((dst_positive_code_table_zero_resultright) + (dst_positive_scale_table_zero_resultright)) + ((dst_positive_scale_table_zero_resultright) + (dst_positive_scale_table_zero_resultright))) + (((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) * S ((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) + ((dst_negative_scale_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)))) + ((((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) * S ((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) + ((dst_negative_scale_table_zero_resultright) + (dst_negative_scale_table_zero_resultright))) + (((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) * S ((dst_negative_code_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)) + ((dst_negative_scale_table_zero_resultright) + (dst_negative_scale_table_zero_resultright)))))) /\ (forall dst_index_table_zero_resultright. (exists pvs_le_gap_table_zero_resultrightdomain. pvs_le_gap_table_zero_resultrightdomain + (dst_index_table_zero_resultright) = (0)) -> exists dst_positive_table_zero_resultright dst_negative_table_zero_resultright dst_value_table_zero_resultright. ((((exists ff_h_pvs_table_zero_resultrightentrypositive. ff_h_pvs_table_zero_resultrightentrypositive + S (dst_positive_table_zero_resultright) = S ((S (dst_index_table_zero_resultright)) * dst_positive_scale_table_zero_resultright)) /\ exists ff_q_pvs_table_zero_resultrightentrypositive. dst_positive_code_table_zero_resultright = ff_q_pvs_table_zero_resultrightentrypositive * S ((S (dst_index_table_zero_resultright)) * dst_positive_scale_table_zero_resultright) + (dst_positive_table_zero_resultright))) /\ (((((exists ff_h_pvs_table_zero_resultrightentrynegative. ff_h_pvs_table_zero_resultrightentrynegative + S (dst_negative_table_zero_resultright) = S ((S (dst_index_table_zero_resultright)) * dst_negative_scale_table_zero_resultright)) /\ exists ff_q_pvs_table_zero_resultrightentrynegative. dst_negative_code_table_zero_resultright = ff_q_pvs_table_zero_resultrightentrynegative * S ((S (dst_index_table_zero_resultright)) * dst_negative_scale_table_zero_resultright) + (dst_negative_table_zero_resultright))) /\ (exists ge_balance_positive_table_zero_resultrightentryvalue ge_balance_negative_table_zero_resultrightentryvalue. (((((dst_value_table_zero_resultright) = 2 * (ge_balance_positive_table_zero_resultrightentryvalue) /\ (ge_balance_negative_table_zero_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_zero_resultrightentryvaluedecode. (((dst_value_table_zero_resultright) = 2 * ge_signed_half_table_zero_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_zero_resultrightentryvalue) = S ge_signed_half_table_zero_resultrightentryvaluedecode))) /\ ((dst_positive_table_zero_resultright) + ge_balance_negative_table_zero_resultrightentryvalue = (dst_negative_table_zero_resultright) + ge_balance_positive_table_zero_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_zero_resulttable dst_positive_scale_table_zero_resulttable dst_negative_code_table_zero_resulttable dst_negative_scale_table_zero_resulttable. (((H) = (((((dst_positive_code_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable)) * S ((dst_positive_code_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable)) + ((dst_positive_scale_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable))) + (((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) * S ((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) + ((dst_negative_scale_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)))) * S ((((dst_positive_code_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable)) * S ((dst_positive_code_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable)) + ((dst_positive_scale_table_zero_resulttable) + (dst_positive_scale_table_zero_resulttable))) + (((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) * S ((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) + ((dst_negative_scale_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)))) + ((((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) * S ((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) + ((dst_negative_scale_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable))) + (((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) * S ((dst_negative_code_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)) + ((dst_negative_scale_table_zero_resulttable) + (dst_negative_scale_table_zero_resulttable)))))) /\ (forall dst_index_table_zero_resulttable. (exists pvs_le_gap_table_zero_resulttabledomain. pvs_le_gap_table_zero_resulttabledomain + (dst_index_table_zero_resulttable) = (0)) -> exists dst_positive_table_zero_resulttable dst_negative_table_zero_resulttable dst_value_table_zero_resulttable. ((((exists ff_h_pvs_table_zero_resulttableentrypositive. ff_h_pvs_table_zero_resulttableentrypositive + S (dst_positive_table_zero_resulttable) = S ((S (dst_index_table_zero_resulttable)) * dst_positive_scale_table_zero_resulttable)) /\ exists ff_q_pvs_table_zero_resulttableentrypositive. dst_positive_code_table_zero_resulttable = ff_q_pvs_table_zero_resulttableentrypositive * S ((S (dst_index_table_zero_resulttable)) * dst_positive_scale_table_zero_resulttable) + (dst_positive_table_zero_resulttable))) /\ (((((exists ff_h_pvs_table_zero_resulttableentrynegative. ff_h_pvs_table_zero_resulttableentrynegative + S (dst_negative_table_zero_resulttable) = S ((S (dst_index_table_zero_resulttable)) * dst_negative_scale_table_zero_resulttable)) /\ exists ff_q_pvs_table_zero_resulttableentrynegative. dst_negative_code_table_zero_resulttable = ff_q_pvs_table_zero_resulttableentrynegative * S ((S (dst_index_table_zero_resulttable)) * dst_negative_scale_table_zero_resulttable) + (dst_negative_table_zero_resulttable))) /\ (exists ge_balance_positive_table_zero_resulttableentryvalue ge_balance_negative_table_zero_resulttableentryvalue. (((((dst_value_table_zero_resulttable) = 2 * (ge_balance_positive_table_zero_resulttableentryvalue) /\ (ge_balance_negative_table_zero_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_zero_resulttableentryvaluedecode. (((dst_value_table_zero_resulttable) = 2 * ge_signed_half_table_zero_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_zero_resulttableentryvalue) = S ge_signed_half_table_zero_resulttableentryvaluedecode))) /\ ((dst_positive_table_zero_resulttable) + ge_balance_negative_table_zero_resulttableentryvalue = (dst_negative_table_zero_resulttable) + ge_balance_positive_table_zero_resulttableentryvalue))))))))) /\ (forall dc_input_table_zero_result dc_output_table_zero_result. ~(dc_input_table_zero_result=0) -> (exists pvs_le_gap_table_zero_resultdomain. pvs_le_gap_table_zero_resultdomain + (dc_input_table_zero_result) = (0)) -> (exists dst_positive_code_table_zero_resultlookup dst_positive_scale_table_zero_resultlookup dst_negative_code_table_zero_resultlookup dst_negative_scale_table_zero_resultlookup dst_positive_table_zero_resultlookup dst_negative_table_zero_resultlookup. (((H) = (((((dst_positive_code_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup)) * S ((dst_positive_code_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup)) + ((dst_positive_scale_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup))) + (((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) * S ((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) + ((dst_negative_scale_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)))) * S ((((dst_positive_code_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup)) * S ((dst_positive_code_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup)) + ((dst_positive_scale_table_zero_resultlookup) + (dst_positive_scale_table_zero_resultlookup))) + (((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) * S ((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) + ((dst_negative_scale_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)))) + ((((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) * S ((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) + ((dst_negative_scale_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup))) + (((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) * S ((dst_negative_code_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)) + ((dst_negative_scale_table_zero_resultlookup) + (dst_negative_scale_table_zero_resultlookup)))))) /\ (((((exists ff_h_pvs_table_zero_resultlookuppositive. ff_h_pvs_table_zero_resultlookuppositive + S (dst_positive_table_zero_resultlookup) = S ((S (dc_input_table_zero_result)) * dst_positive_scale_table_zero_resultlookup)) /\ exists ff_q_pvs_table_zero_resultlookuppositive. dst_positive_code_table_zero_resultlookup = ff_q_pvs_table_zero_resultlookuppositive * S ((S (dc_input_table_zero_result)) * dst_positive_scale_table_zero_resultlookup) + (dst_positive_table_zero_resultlookup))) /\ (((((exists ff_h_pvs_table_zero_resultlookupnegative. ff_h_pvs_table_zero_resultlookupnegative + S (dst_negative_table_zero_resultlookup) = S ((S (dc_input_table_zero_result)) * dst_negative_scale_table_zero_resultlookup)) /\ exists ff_q_pvs_table_zero_resultlookupnegative. dst_negative_code_table_zero_resultlookup = ff_q_pvs_table_zero_resultlookupnegative * S ((S (dc_input_table_zero_result)) * dst_negative_scale_table_zero_resultlookup) + (dst_negative_table_zero_resultlookup))) /\ (exists ge_balance_positive_table_zero_resultlookupvalue ge_balance_negative_table_zero_resultlookupvalue. (((((dc_output_table_zero_result) = 2 * (ge_balance_positive_table_zero_resultlookupvalue) /\ (ge_balance_negative_table_zero_resultlookupvalue) = 0) \/ exists ge_signed_half_table_zero_resultlookupvaluedecode. (((dc_output_table_zero_result) = 2 * ge_signed_half_table_zero_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultlookupvalue) = 0) /\ (ge_balance_negative_table_zero_resultlookupvalue) = S ge_signed_half_table_zero_resultlookupvaluedecode))) /\ ((dst_positive_table_zero_resultlookup) + ge_balance_negative_table_zero_resultlookupvalue = (dst_negative_table_zero_resultlookup) + ge_balance_positive_table_zero_resultlookupvalue))))))))) -> (((~((dc_input_table_zero_result)=0)) /\ (exists dc_mask_table_zero_resultvalue. ((((exists dst_positive_code_table_zero_resultvaluemasktable dst_positive_scale_table_zero_resultvaluemasktable dst_negative_code_table_zero_resultvaluemasktable dst_negative_scale_table_zero_resultvaluemasktable. (((dc_mask_table_zero_resultvalue) = (((((dst_positive_code_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable)) * S ((dst_positive_code_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable)) + ((dst_positive_scale_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable))) + (((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) * S ((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) + ((dst_negative_scale_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)))) * S ((((dst_positive_code_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable)) * S ((dst_positive_code_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable)) + ((dst_positive_scale_table_zero_resultvaluemasktable) + (dst_positive_scale_table_zero_resultvaluemasktable))) + (((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) * S ((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) + ((dst_negative_scale_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)))) + ((((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) * S ((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) + ((dst_negative_scale_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable))) + (((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) * S ((dst_negative_code_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)) + ((dst_negative_scale_table_zero_resultvaluemasktable) + (dst_negative_scale_table_zero_resultvaluemasktable)))))) /\ (forall dst_index_table_zero_resultvaluemasktable. (exists pvs_le_gap_table_zero_resultvaluemasktabledomain. pvs_le_gap_table_zero_resultvaluemasktabledomain + (dst_index_table_zero_resultvaluemasktable) = (dc_input_table_zero_result)) -> exists dst_positive_table_zero_resultvaluemasktable dst_negative_table_zero_resultvaluemasktable dst_value_table_zero_resultvaluemasktable. ((((exists ff_h_pvs_table_zero_resultvaluemasktableentrypositive. ff_h_pvs_table_zero_resultvaluemasktableentrypositive + S (dst_positive_table_zero_resultvaluemasktable) = S ((S (dst_index_table_zero_resultvaluemasktable)) * dst_positive_scale_table_zero_resultvaluemasktable)) /\ exists ff_q_pvs_table_zero_resultvaluemasktableentrypositive. dst_positive_code_table_zero_resultvaluemasktable = ff_q_pvs_table_zero_resultvaluemasktableentrypositive * S ((S (dst_index_table_zero_resultvaluemasktable)) * dst_positive_scale_table_zero_resultvaluemasktable) + (dst_positive_table_zero_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemasktableentrynegative. ff_h_pvs_table_zero_resultvaluemasktableentrynegative + S (dst_negative_table_zero_resultvaluemasktable) = S ((S (dst_index_table_zero_resultvaluemasktable)) * dst_negative_scale_table_zero_resultvaluemasktable)) /\ exists ff_q_pvs_table_zero_resultvaluemasktableentrynegative. dst_negative_code_table_zero_resultvaluemasktable = ff_q_pvs_table_zero_resultvaluemasktableentrynegative * S ((S (dst_index_table_zero_resultvaluemasktable)) * dst_negative_scale_table_zero_resultvaluemasktable) + (dst_negative_table_zero_resultvaluemasktable))) /\ (exists ge_balance_positive_table_zero_resultvaluemasktableentryvalue ge_balance_negative_table_zero_resultvaluemasktableentryvalue. (((((dst_value_table_zero_resultvaluemasktable) = 2 * (ge_balance_positive_table_zero_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_zero_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_zero_resultvaluemasktableentryvaluedecode. (((dst_value_table_zero_resultvaluemasktable) = 2 * ge_signed_half_table_zero_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_zero_resultvaluemasktableentryvalue) = S ge_signed_half_table_zero_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_zero_resultvaluemasktable) + ge_balance_negative_table_zero_resultvaluemasktableentryvalue = (dst_negative_table_zero_resultvaluemasktable) + ge_balance_positive_table_zero_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_zero_resultvaluemask dc_value_table_zero_resultvaluemask. (exists pvs_le_gap_table_zero_resultvaluemaskdomain. pvs_le_gap_table_zero_resultvaluemaskdomain + (dc_index_table_zero_resultvaluemask) = (dc_input_table_zero_result)) -> (exists dst_positive_code_table_zero_resultvaluemasklookup dst_positive_scale_table_zero_resultvaluemasklookup dst_negative_code_table_zero_resultvaluemasklookup dst_negative_scale_table_zero_resultvaluemasklookup dst_positive_table_zero_resultvaluemasklookup dst_negative_table_zero_resultvaluemasklookup. (((dc_mask_table_zero_resultvalue) = (((((dst_positive_code_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup)) * S ((dst_positive_code_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup)) + ((dst_positive_scale_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup))) + (((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) * S ((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) + ((dst_negative_scale_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)))) * S ((((dst_positive_code_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup)) * S ((dst_positive_code_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup)) + ((dst_positive_scale_table_zero_resultvaluemasklookup) + (dst_positive_scale_table_zero_resultvaluemasklookup))) + (((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) * S ((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) + ((dst_negative_scale_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)))) + ((((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) * S ((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) + ((dst_negative_scale_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup))) + (((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) * S ((dst_negative_code_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)) + ((dst_negative_scale_table_zero_resultvaluemasklookup) + (dst_negative_scale_table_zero_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemasklookuppositive. ff_h_pvs_table_zero_resultvaluemasklookuppositive + S (dst_positive_table_zero_resultvaluemasklookup) = S ((S (dc_index_table_zero_resultvaluemask)) * dst_positive_scale_table_zero_resultvaluemasklookup)) /\ exists ff_q_pvs_table_zero_resultvaluemasklookuppositive. dst_positive_code_table_zero_resultvaluemasklookup = ff_q_pvs_table_zero_resultvaluemasklookuppositive * S ((S (dc_index_table_zero_resultvaluemask)) * dst_positive_scale_table_zero_resultvaluemasklookup) + (dst_positive_table_zero_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemasklookupnegative. ff_h_pvs_table_zero_resultvaluemasklookupnegative + S (dst_negative_table_zero_resultvaluemasklookup) = S ((S (dc_index_table_zero_resultvaluemask)) * dst_negative_scale_table_zero_resultvaluemasklookup)) /\ exists ff_q_pvs_table_zero_resultvaluemasklookupnegative. dst_negative_code_table_zero_resultvaluemasklookup = ff_q_pvs_table_zero_resultvaluemasklookupnegative * S ((S (dc_index_table_zero_resultvaluemask)) * dst_negative_scale_table_zero_resultvaluemasklookup) + (dst_negative_table_zero_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_zero_resultvaluemasklookupvalue ge_balance_negative_table_zero_resultvaluemasklookupvalue. (((((dc_value_table_zero_resultvaluemask) = 2 * (ge_balance_positive_table_zero_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_zero_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_zero_resultvaluemasklookupvaluedecode. (((dc_value_table_zero_resultvaluemask) = 2 * ge_signed_half_table_zero_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_zero_resultvaluemasklookupvalue) = S ge_signed_half_table_zero_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_zero_resultvaluemasklookup) + ge_balance_negative_table_zero_resultvaluemasklookupvalue = (dst_negative_table_zero_resultvaluemasklookup) + ge_balance_positive_table_zero_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_zero_resultvaluemask)=0)) /\ (exists dc_quotient_table_zero_resultvaluemaskentry dc_left_table_zero_resultvaluemaskentry dc_right_table_zero_resultvaluemaskentry. (((dc_input_table_zero_result)=(dc_index_table_zero_resultvaluemask)*dc_quotient_table_zero_resultvaluemaskentry) /\ (((exists dst_positive_code_table_zero_resultvaluemaskentryleft dst_positive_scale_table_zero_resultvaluemaskentryleft dst_negative_code_table_zero_resultvaluemaskentryleft dst_negative_scale_table_zero_resultvaluemaskentryleft dst_positive_table_zero_resultvaluemaskentryleft dst_negative_table_zero_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_positive_code_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft)) + ((dst_positive_scale_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft))) + (((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) + ((dst_negative_scale_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_positive_code_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft)) + ((dst_positive_scale_table_zero_resultvaluemaskentryleft) + (dst_positive_scale_table_zero_resultvaluemaskentryleft))) + (((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) + ((dst_negative_scale_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) + ((dst_negative_scale_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft))) + (((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) * S ((dst_negative_code_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)) + ((dst_negative_scale_table_zero_resultvaluemaskentryleft) + (dst_negative_scale_table_zero_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemaskentryleftpositive. ff_h_pvs_table_zero_resultvaluemaskentryleftpositive + S (dst_positive_table_zero_resultvaluemaskentryleft) = S ((S (dc_index_table_zero_resultvaluemask)) * dst_positive_scale_table_zero_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_zero_resultvaluemaskentryleftpositive. dst_positive_code_table_zero_resultvaluemaskentryleft = ff_q_pvs_table_zero_resultvaluemaskentryleftpositive * S ((S (dc_index_table_zero_resultvaluemask)) * dst_positive_scale_table_zero_resultvaluemaskentryleft) + (dst_positive_table_zero_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemaskentryleftnegative. ff_h_pvs_table_zero_resultvaluemaskentryleftnegative + S (dst_negative_table_zero_resultvaluemaskentryleft) = S ((S (dc_index_table_zero_resultvaluemask)) * dst_negative_scale_table_zero_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_zero_resultvaluemaskentryleftnegative. dst_negative_code_table_zero_resultvaluemaskentryleft = ff_q_pvs_table_zero_resultvaluemaskentryleftnegative * S ((S (dc_index_table_zero_resultvaluemask)) * dst_negative_scale_table_zero_resultvaluemaskentryleft) + (dst_negative_table_zero_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_zero_resultvaluemaskentryleftvalue ge_balance_negative_table_zero_resultvaluemaskentryleftvalue. (((((dc_left_table_zero_resultvaluemaskentry) = 2 * (ge_balance_positive_table_zero_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_zero_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_zero_resultvaluemaskentryleftvaluedecode. (((dc_left_table_zero_resultvaluemaskentry) = 2 * ge_signed_half_table_zero_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_zero_resultvaluemaskentryleftvalue) = S ge_signed_half_table_zero_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_zero_resultvaluemaskentryleft) + ge_balance_negative_table_zero_resultvaluemaskentryleftvalue = (dst_negative_table_zero_resultvaluemaskentryleft) + ge_balance_positive_table_zero_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_zero_resultvaluemaskentryright dst_positive_scale_table_zero_resultvaluemaskentryright dst_negative_code_table_zero_resultvaluemaskentryright dst_negative_scale_table_zero_resultvaluemaskentryright dst_positive_table_zero_resultvaluemaskentryright dst_negative_table_zero_resultvaluemaskentryright. (((G) = (((((dst_positive_code_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright)) * S ((dst_positive_code_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright)) + ((dst_positive_scale_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright))) + (((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) * S ((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) + ((dst_negative_scale_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright)) * S ((dst_positive_code_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright)) + ((dst_positive_scale_table_zero_resultvaluemaskentryright) + (dst_positive_scale_table_zero_resultvaluemaskentryright))) + (((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) * S ((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) + ((dst_negative_scale_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)))) + ((((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) * S ((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) + ((dst_negative_scale_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright))) + (((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) * S ((dst_negative_code_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)) + ((dst_negative_scale_table_zero_resultvaluemaskentryright) + (dst_negative_scale_table_zero_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemaskentryrightpositive. ff_h_pvs_table_zero_resultvaluemaskentryrightpositive + S (dst_positive_table_zero_resultvaluemaskentryright) = S ((S (dc_quotient_table_zero_resultvaluemaskentry)) * dst_positive_scale_table_zero_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_zero_resultvaluemaskentryrightpositive. dst_positive_code_table_zero_resultvaluemaskentryright = ff_q_pvs_table_zero_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_zero_resultvaluemaskentry)) * dst_positive_scale_table_zero_resultvaluemaskentryright) + (dst_positive_table_zero_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_zero_resultvaluemaskentryrightnegative. ff_h_pvs_table_zero_resultvaluemaskentryrightnegative + S (dst_negative_table_zero_resultvaluemaskentryright) = S ((S (dc_quotient_table_zero_resultvaluemaskentry)) * dst_negative_scale_table_zero_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_zero_resultvaluemaskentryrightnegative. dst_negative_code_table_zero_resultvaluemaskentryright = ff_q_pvs_table_zero_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_zero_resultvaluemaskentry)) * dst_negative_scale_table_zero_resultvaluemaskentryright) + (dst_negative_table_zero_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_zero_resultvaluemaskentryrightvalue ge_balance_negative_table_zero_resultvaluemaskentryrightvalue. (((((dc_right_table_zero_resultvaluemaskentry) = 2 * (ge_balance_positive_table_zero_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_zero_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_zero_resultvaluemaskentryrightvaluedecode. (((dc_right_table_zero_resultvaluemaskentry) = 2 * ge_signed_half_table_zero_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_zero_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_zero_resultvaluemaskentryrightvalue) = S ge_signed_half_table_zero_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_zero_resultvaluemaskentryright) + ge_balance_negative_table_zero_resultvaluemaskentryrightvalue = (dst_negative_table_zero_resultvaluemaskentryright) + ge_balance_positive_table_zero_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_zero_resultvaluemaskentryproduct sto_an_table_zero_resultvaluemaskentryproduct sto_bp_table_zero_resultvaluemaskentryproduct sto_bn_table_zero_resultvaluemaskentryproduct sto_cp_table_zero_resultvaluemaskentryproduct sto_cn_table_zero_resultvaluemaskentryproduct. (((((dc_left_table_zero_resultvaluemaskentry) = 2 * (sto_ap_table_zero_resultvaluemaskentryproduct) /\ (sto_an_table_zero_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_zero_resultvaluemaskentryproductleft. (((dc_left_table_zero_resultvaluemaskentry) = 2 * ge_signed_half_table_zero_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_zero_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_zero_resultvaluemaskentryproduct) = S ge_signed_half_table_zero_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_zero_resultvaluemaskentry) = 2 * (sto_bp_table_zero_resultvaluemaskentryproduct) /\ (sto_bn_table_zero_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_zero_resultvaluemaskentryproductright. (((dc_right_table_zero_resultvaluemaskentry) = 2 * ge_signed_half_table_zero_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_zero_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_zero_resultvaluemaskentryproduct) = S ge_signed_half_table_zero_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_zero_resultvaluemask) = 2 * (sto_cp_table_zero_resultvaluemaskentryproduct) /\ (sto_cn_table_zero_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_zero_resultvaluemaskentryproductoutput. (((dc_value_table_zero_resultvaluemask) = 2 * ge_signed_half_table_zero_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_zero_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_zero_resultvaluemaskentryproduct) = S ge_signed_half_table_zero_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_zero_resultvaluemaskentryproduct * sto_bp_table_zero_resultvaluemaskentryproduct + sto_an_table_zero_resultvaluemaskentryproduct * sto_bn_table_zero_resultvaluemaskentryproduct) + sto_cn_table_zero_resultvaluemaskentryproduct = (sto_ap_table_zero_resultvaluemaskentryproduct * sto_bn_table_zero_resultvaluemaskentryproduct + sto_an_table_zero_resultvaluemaskentryproduct * sto_bp_table_zero_resultvaluemaskentryproduct) + sto_cp_table_zero_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_zero_resultvaluemask)=0 \/ ~(exists pvs_factor_table_zero_resultvaluemaskentrynondivisor. (dc_input_table_zero_result) = (dc_index_table_zero_resultvaluemask) * pvs_factor_table_zero_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_zero_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_zero_resultvaluefold dst_positive_scale_table_zero_resultvaluefold dst_negative_code_table_zero_resultvaluefold dst_negative_scale_table_zero_resultvaluefold dst_positive_sum_table_zero_resultvaluefold dst_negative_sum_table_zero_resultvaluefold. (((dc_mask_table_zero_resultvalue) = (((((dst_positive_code_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold)) * S ((dst_positive_code_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold)) + ((dst_positive_scale_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold))) + (((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) * S ((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) + ((dst_negative_scale_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)))) * S ((((dst_positive_code_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold)) * S ((dst_positive_code_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold)) + ((dst_positive_scale_table_zero_resultvaluefold) + (dst_positive_scale_table_zero_resultvaluefold))) + (((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) * S ((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) + ((dst_negative_scale_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)))) + ((((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) * S ((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) + ((dst_negative_scale_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold))) + (((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) * S ((dst_negative_code_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)) + ((dst_negative_scale_table_zero_resultvaluefold) + (dst_negative_scale_table_zero_resultvaluefold)))))) /\ (((exists fs_u_dst_table_zero_resultvaluefoldpositive fs_v_dst_table_zero_resultvaluefoldpositive. ((((exists fs_h_dst_table_zero_resultvaluefoldpositive_body_start. fs_h_dst_table_zero_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_zero_resultvaluefoldpositive)) /\ exists fs_q_dst_table_zero_resultvaluefoldpositive_body_start. fs_u_dst_table_zero_resultvaluefoldpositive = fs_q_dst_table_zero_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_zero_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldpositive_body_terminal. fs_h_dst_table_zero_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_zero_resultvaluefold) = S ((S (S (dc_input_table_zero_result))) * fs_v_dst_table_zero_resultvaluefoldpositive)) /\ exists fs_q_dst_table_zero_resultvaluefoldpositive_body_terminal. fs_u_dst_table_zero_resultvaluefoldpositive = fs_q_dst_table_zero_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_zero_result))) * fs_v_dst_table_zero_resultvaluefoldpositive) + (dst_positive_sum_table_zero_resultvaluefold))) /\ forall fs_i_dst_table_zero_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_zero_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_zero_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_zero_resultvaluefoldpositive_body_steps = S (dc_input_table_zero_result)) -> exists fs_a_dst_table_zero_resultvaluefoldpositive_body_steps fs_r_dst_table_zero_resultvaluefoldpositive_body_steps fs_s_dst_table_zero_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_zero_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_zero_resultvaluefold)) /\ exists fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_zero_resultvaluefold = fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_zero_resultvaluefold) + (fs_a_dst_table_zero_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_zero_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_zero_resultvaluefoldpositive)) /\ exists fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_zero_resultvaluefoldpositive = fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_zero_resultvaluefoldpositive) + (fs_r_dst_table_zero_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_zero_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_zero_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_zero_resultvaluefoldpositive)) /\ exists fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_zero_resultvaluefoldpositive = fs_q_dst_table_zero_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_zero_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_zero_resultvaluefoldpositive) + (fs_s_dst_table_zero_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_zero_resultvaluefoldpositive_body_steps = fs_r_dst_table_zero_resultvaluefoldpositive_body_steps + fs_a_dst_table_zero_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_zero_resultvaluefoldnegative fs_v_dst_table_zero_resultvaluefoldnegative. ((((exists fs_h_dst_table_zero_resultvaluefoldnegative_body_start. fs_h_dst_table_zero_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_zero_resultvaluefoldnegative)) /\ exists fs_q_dst_table_zero_resultvaluefoldnegative_body_start. fs_u_dst_table_zero_resultvaluefoldnegative = fs_q_dst_table_zero_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_zero_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldnegative_body_terminal. fs_h_dst_table_zero_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_zero_resultvaluefold) = S ((S (S (dc_input_table_zero_result))) * fs_v_dst_table_zero_resultvaluefoldnegative)) /\ exists fs_q_dst_table_zero_resultvaluefoldnegative_body_terminal. fs_u_dst_table_zero_resultvaluefoldnegative = fs_q_dst_table_zero_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_zero_result))) * fs_v_dst_table_zero_resultvaluefoldnegative) + (dst_negative_sum_table_zero_resultvaluefold))) /\ forall fs_i_dst_table_zero_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_zero_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_zero_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_zero_resultvaluefoldnegative_body_steps = S (dc_input_table_zero_result)) -> exists fs_a_dst_table_zero_resultvaluefoldnegative_body_steps fs_r_dst_table_zero_resultvaluefoldnegative_body_steps fs_s_dst_table_zero_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_zero_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_zero_resultvaluefold)) /\ exists fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_zero_resultvaluefold = fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_zero_resultvaluefold) + (fs_a_dst_table_zero_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_zero_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_zero_resultvaluefoldnegative)) /\ exists fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_zero_resultvaluefoldnegative = fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_zero_resultvaluefoldnegative) + (fs_r_dst_table_zero_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_zero_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_zero_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_zero_resultvaluefoldnegative)) /\ exists fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_zero_resultvaluefoldnegative = fs_q_dst_table_zero_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_zero_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_zero_resultvaluefoldnegative) + (fs_s_dst_table_zero_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_zero_resultvaluefoldnegative_body_steps = fs_r_dst_table_zero_resultvaluefoldnegative_body_steps + fs_a_dst_table_zero_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_zero_resultvaluefoldresult ge_balance_negative_table_zero_resultvaluefoldresult. (((((dc_output_table_zero_result) = 2 * (ge_balance_positive_table_zero_resultvaluefoldresult) /\ (ge_balance_negative_table_zero_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_zero_resultvaluefoldresultdecode. (((dc_output_table_zero_result) = 2 * ge_signed_half_table_zero_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_zero_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_zero_resultvaluefoldresult) = S ge_signed_half_table_zero_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_zero_resultvaluefold) + ge_balance_negative_table_zero_resultvaluefoldresult = (dst_negative_sum_table_zero_resultvaluefold) + ge_balance_positive_table_zero_resultvaluefoldresult))))))))))))))))))))