dirichlet_convolution_table_exists

Exact expanded first-order arithmetic statement

forall N F G. (exists dst_positive_code_table_exists_left dst_positive_scale_table_exists_left dst_negative_code_table_exists_left dst_negative_scale_table_exists_left. (((F) = (((((dst_positive_code_table_exists_left) + (dst_positive_scale_table_exists_left)) * S ((dst_positive_code_table_exists_left) + (dst_positive_scale_table_exists_left)) + ((dst_positive_scale_table_exists_left) + (dst_positive_scale_table_exists_left))) + (((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) * S ((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) + ((dst_negative_scale_table_exists_left) + (dst_negative_scale_table_exists_left)))) * S ((((dst_positive_code_table_exists_left) + (dst_positive_scale_table_exists_left)) * S ((dst_positive_code_table_exists_left) + (dst_positive_scale_table_exists_left)) + ((dst_positive_scale_table_exists_left) + (dst_positive_scale_table_exists_left))) + (((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) * S ((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) + ((dst_negative_scale_table_exists_left) + (dst_negative_scale_table_exists_left)))) + ((((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) * S ((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) + ((dst_negative_scale_table_exists_left) + (dst_negative_scale_table_exists_left))) + (((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) * S ((dst_negative_code_table_exists_left) + (dst_negative_scale_table_exists_left)) + ((dst_negative_scale_table_exists_left) + (dst_negative_scale_table_exists_left)))))) /\ (forall dst_index_table_exists_left. (exists pvs_le_gap_table_exists_leftdomain. pvs_le_gap_table_exists_leftdomain + (dst_index_table_exists_left) = (N)) -> exists dst_positive_table_exists_left dst_negative_table_exists_left dst_value_table_exists_left. ((((exists ff_h_pvs_table_exists_leftentrypositive. ff_h_pvs_table_exists_leftentrypositive + S (dst_positive_table_exists_left) = S ((S (dst_index_table_exists_left)) * dst_positive_scale_table_exists_left)) /\ exists ff_q_pvs_table_exists_leftentrypositive. dst_positive_code_table_exists_left = ff_q_pvs_table_exists_leftentrypositive * S ((S (dst_index_table_exists_left)) * dst_positive_scale_table_exists_left) + (dst_positive_table_exists_left))) /\ (((((exists ff_h_pvs_table_exists_leftentrynegative. ff_h_pvs_table_exists_leftentrynegative + S (dst_negative_table_exists_left) = S ((S (dst_index_table_exists_left)) * dst_negative_scale_table_exists_left)) /\ exists ff_q_pvs_table_exists_leftentrynegative. dst_negative_code_table_exists_left = ff_q_pvs_table_exists_leftentrynegative * S ((S (dst_index_table_exists_left)) * dst_negative_scale_table_exists_left) + (dst_negative_table_exists_left))) /\ (exists ge_balance_positive_table_exists_leftentryvalue ge_balance_negative_table_exists_leftentryvalue. (((((dst_value_table_exists_left) = 2 * (ge_balance_positive_table_exists_leftentryvalue) /\ (ge_balance_negative_table_exists_leftentryvalue) = 0) \/ exists ge_signed_half_table_exists_leftentryvaluedecode. (((dst_value_table_exists_left) = 2 * ge_signed_half_table_exists_leftentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_leftentryvalue) = 0) /\ (ge_balance_negative_table_exists_leftentryvalue) = S ge_signed_half_table_exists_leftentryvaluedecode))) /\ ((dst_positive_table_exists_left) + ge_balance_negative_table_exists_leftentryvalue = (dst_negative_table_exists_left) + ge_balance_positive_table_exists_leftentryvalue))))))))) -> (exists dst_positive_code_table_exists_right dst_positive_scale_table_exists_right dst_negative_code_table_exists_right dst_negative_scale_table_exists_right. (((G) = (((((dst_positive_code_table_exists_right) + (dst_positive_scale_table_exists_right)) * S ((dst_positive_code_table_exists_right) + (dst_positive_scale_table_exists_right)) + ((dst_positive_scale_table_exists_right) + (dst_positive_scale_table_exists_right))) + (((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) * S ((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) + ((dst_negative_scale_table_exists_right) + (dst_negative_scale_table_exists_right)))) * S ((((dst_positive_code_table_exists_right) + (dst_positive_scale_table_exists_right)) * S ((dst_positive_code_table_exists_right) + (dst_positive_scale_table_exists_right)) + ((dst_positive_scale_table_exists_right) + (dst_positive_scale_table_exists_right))) + (((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) * S ((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) + ((dst_negative_scale_table_exists_right) + (dst_negative_scale_table_exists_right)))) + ((((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) * S ((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) + ((dst_negative_scale_table_exists_right) + (dst_negative_scale_table_exists_right))) + (((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) * S ((dst_negative_code_table_exists_right) + (dst_negative_scale_table_exists_right)) + ((dst_negative_scale_table_exists_right) + (dst_negative_scale_table_exists_right)))))) /\ (forall dst_index_table_exists_right. (exists pvs_le_gap_table_exists_rightdomain. pvs_le_gap_table_exists_rightdomain + (dst_index_table_exists_right) = (N)) -> exists dst_positive_table_exists_right dst_negative_table_exists_right dst_value_table_exists_right. ((((exists ff_h_pvs_table_exists_rightentrypositive. ff_h_pvs_table_exists_rightentrypositive + S (dst_positive_table_exists_right) = S ((S (dst_index_table_exists_right)) * dst_positive_scale_table_exists_right)) /\ exists ff_q_pvs_table_exists_rightentrypositive. dst_positive_code_table_exists_right = ff_q_pvs_table_exists_rightentrypositive * S ((S (dst_index_table_exists_right)) * dst_positive_scale_table_exists_right) + (dst_positive_table_exists_right))) /\ (((((exists ff_h_pvs_table_exists_rightentrynegative. ff_h_pvs_table_exists_rightentrynegative + S (dst_negative_table_exists_right) = S ((S (dst_index_table_exists_right)) * dst_negative_scale_table_exists_right)) /\ exists ff_q_pvs_table_exists_rightentrynegative. dst_negative_code_table_exists_right = ff_q_pvs_table_exists_rightentrynegative * S ((S (dst_index_table_exists_right)) * dst_negative_scale_table_exists_right) + (dst_negative_table_exists_right))) /\ (exists ge_balance_positive_table_exists_rightentryvalue ge_balance_negative_table_exists_rightentryvalue. (((((dst_value_table_exists_right) = 2 * (ge_balance_positive_table_exists_rightentryvalue) /\ (ge_balance_negative_table_exists_rightentryvalue) = 0) \/ exists ge_signed_half_table_exists_rightentryvaluedecode. (((dst_value_table_exists_right) = 2 * ge_signed_half_table_exists_rightentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_rightentryvalue) = 0) /\ (ge_balance_negative_table_exists_rightentryvalue) = S ge_signed_half_table_exists_rightentryvaluedecode))) /\ ((dst_positive_table_exists_right) + ge_balance_negative_table_exists_rightentryvalue = (dst_negative_table_exists_right) + ge_balance_positive_table_exists_rightentryvalue))))))))) -> exists H. (((exists dst_positive_code_table_exists_resultleft dst_positive_scale_table_exists_resultleft dst_negative_code_table_exists_resultleft dst_negative_scale_table_exists_resultleft. (((F) = (((((dst_positive_code_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft)) * S ((dst_positive_code_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft)) + ((dst_positive_scale_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft))) + (((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) * S ((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) + ((dst_negative_scale_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)))) * S ((((dst_positive_code_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft)) * S ((dst_positive_code_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft)) + ((dst_positive_scale_table_exists_resultleft) + (dst_positive_scale_table_exists_resultleft))) + (((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) * S ((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) + ((dst_negative_scale_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)))) + ((((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) * S ((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) + ((dst_negative_scale_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft))) + (((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) * S ((dst_negative_code_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)) + ((dst_negative_scale_table_exists_resultleft) + (dst_negative_scale_table_exists_resultleft)))))) /\ (forall dst_index_table_exists_resultleft. (exists pvs_le_gap_table_exists_resultleftdomain. pvs_le_gap_table_exists_resultleftdomain + (dst_index_table_exists_resultleft) = (N)) -> exists dst_positive_table_exists_resultleft dst_negative_table_exists_resultleft dst_value_table_exists_resultleft. ((((exists ff_h_pvs_table_exists_resultleftentrypositive. ff_h_pvs_table_exists_resultleftentrypositive + S (dst_positive_table_exists_resultleft) = S ((S (dst_index_table_exists_resultleft)) * dst_positive_scale_table_exists_resultleft)) /\ exists ff_q_pvs_table_exists_resultleftentrypositive. dst_positive_code_table_exists_resultleft = ff_q_pvs_table_exists_resultleftentrypositive * S ((S (dst_index_table_exists_resultleft)) * dst_positive_scale_table_exists_resultleft) + (dst_positive_table_exists_resultleft))) /\ (((((exists ff_h_pvs_table_exists_resultleftentrynegative. ff_h_pvs_table_exists_resultleftentrynegative + S (dst_negative_table_exists_resultleft) = S ((S (dst_index_table_exists_resultleft)) * dst_negative_scale_table_exists_resultleft)) /\ exists ff_q_pvs_table_exists_resultleftentrynegative. dst_negative_code_table_exists_resultleft = ff_q_pvs_table_exists_resultleftentrynegative * S ((S (dst_index_table_exists_resultleft)) * dst_negative_scale_table_exists_resultleft) + (dst_negative_table_exists_resultleft))) /\ (exists ge_balance_positive_table_exists_resultleftentryvalue ge_balance_negative_table_exists_resultleftentryvalue. (((((dst_value_table_exists_resultleft) = 2 * (ge_balance_positive_table_exists_resultleftentryvalue) /\ (ge_balance_negative_table_exists_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_exists_resultleftentryvaluedecode. (((dst_value_table_exists_resultleft) = 2 * ge_signed_half_table_exists_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_exists_resultleftentryvalue) = S ge_signed_half_table_exists_resultleftentryvaluedecode))) /\ ((dst_positive_table_exists_resultleft) + ge_balance_negative_table_exists_resultleftentryvalue = (dst_negative_table_exists_resultleft) + ge_balance_positive_table_exists_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_exists_resultright dst_positive_scale_table_exists_resultright dst_negative_code_table_exists_resultright dst_negative_scale_table_exists_resultright. (((G) = (((((dst_positive_code_table_exists_resultright) + (dst_positive_scale_table_exists_resultright)) * S ((dst_positive_code_table_exists_resultright) + (dst_positive_scale_table_exists_resultright)) + ((dst_positive_scale_table_exists_resultright) + (dst_positive_scale_table_exists_resultright))) + (((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) * S ((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) + ((dst_negative_scale_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)))) * S ((((dst_positive_code_table_exists_resultright) + (dst_positive_scale_table_exists_resultright)) * S ((dst_positive_code_table_exists_resultright) + (dst_positive_scale_table_exists_resultright)) + ((dst_positive_scale_table_exists_resultright) + (dst_positive_scale_table_exists_resultright))) + (((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) * S ((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) + ((dst_negative_scale_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)))) + ((((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) * S ((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) + ((dst_negative_scale_table_exists_resultright) + (dst_negative_scale_table_exists_resultright))) + (((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) * S ((dst_negative_code_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)) + ((dst_negative_scale_table_exists_resultright) + (dst_negative_scale_table_exists_resultright)))))) /\ (forall dst_index_table_exists_resultright. (exists pvs_le_gap_table_exists_resultrightdomain. pvs_le_gap_table_exists_resultrightdomain + (dst_index_table_exists_resultright) = (N)) -> exists dst_positive_table_exists_resultright dst_negative_table_exists_resultright dst_value_table_exists_resultright. ((((exists ff_h_pvs_table_exists_resultrightentrypositive. ff_h_pvs_table_exists_resultrightentrypositive + S (dst_positive_table_exists_resultright) = S ((S (dst_index_table_exists_resultright)) * dst_positive_scale_table_exists_resultright)) /\ exists ff_q_pvs_table_exists_resultrightentrypositive. dst_positive_code_table_exists_resultright = ff_q_pvs_table_exists_resultrightentrypositive * S ((S (dst_index_table_exists_resultright)) * dst_positive_scale_table_exists_resultright) + (dst_positive_table_exists_resultright))) /\ (((((exists ff_h_pvs_table_exists_resultrightentrynegative. ff_h_pvs_table_exists_resultrightentrynegative + S (dst_negative_table_exists_resultright) = S ((S (dst_index_table_exists_resultright)) * dst_negative_scale_table_exists_resultright)) /\ exists ff_q_pvs_table_exists_resultrightentrynegative. dst_negative_code_table_exists_resultright = ff_q_pvs_table_exists_resultrightentrynegative * S ((S (dst_index_table_exists_resultright)) * dst_negative_scale_table_exists_resultright) + (dst_negative_table_exists_resultright))) /\ (exists ge_balance_positive_table_exists_resultrightentryvalue ge_balance_negative_table_exists_resultrightentryvalue. (((((dst_value_table_exists_resultright) = 2 * (ge_balance_positive_table_exists_resultrightentryvalue) /\ (ge_balance_negative_table_exists_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_exists_resultrightentryvaluedecode. (((dst_value_table_exists_resultright) = 2 * ge_signed_half_table_exists_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_exists_resultrightentryvalue) = S ge_signed_half_table_exists_resultrightentryvaluedecode))) /\ ((dst_positive_table_exists_resultright) + ge_balance_negative_table_exists_resultrightentryvalue = (dst_negative_table_exists_resultright) + ge_balance_positive_table_exists_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_exists_resulttable dst_positive_scale_table_exists_resulttable dst_negative_code_table_exists_resulttable dst_negative_scale_table_exists_resulttable. (((H) = (((((dst_positive_code_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable)) * S ((dst_positive_code_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable)) + ((dst_positive_scale_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable))) + (((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) * S ((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) + ((dst_negative_scale_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)))) * S ((((dst_positive_code_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable)) * S ((dst_positive_code_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable)) + ((dst_positive_scale_table_exists_resulttable) + (dst_positive_scale_table_exists_resulttable))) + (((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) * S ((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) + ((dst_negative_scale_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)))) + ((((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) * S ((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) + ((dst_negative_scale_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable))) + (((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) * S ((dst_negative_code_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)) + ((dst_negative_scale_table_exists_resulttable) + (dst_negative_scale_table_exists_resulttable)))))) /\ (forall dst_index_table_exists_resulttable. (exists pvs_le_gap_table_exists_resulttabledomain. pvs_le_gap_table_exists_resulttabledomain + (dst_index_table_exists_resulttable) = (N)) -> exists dst_positive_table_exists_resulttable dst_negative_table_exists_resulttable dst_value_table_exists_resulttable. ((((exists ff_h_pvs_table_exists_resulttableentrypositive. ff_h_pvs_table_exists_resulttableentrypositive + S (dst_positive_table_exists_resulttable) = S ((S (dst_index_table_exists_resulttable)) * dst_positive_scale_table_exists_resulttable)) /\ exists ff_q_pvs_table_exists_resulttableentrypositive. dst_positive_code_table_exists_resulttable = ff_q_pvs_table_exists_resulttableentrypositive * S ((S (dst_index_table_exists_resulttable)) * dst_positive_scale_table_exists_resulttable) + (dst_positive_table_exists_resulttable))) /\ (((((exists ff_h_pvs_table_exists_resulttableentrynegative. ff_h_pvs_table_exists_resulttableentrynegative + S (dst_negative_table_exists_resulttable) = S ((S (dst_index_table_exists_resulttable)) * dst_negative_scale_table_exists_resulttable)) /\ exists ff_q_pvs_table_exists_resulttableentrynegative. dst_negative_code_table_exists_resulttable = ff_q_pvs_table_exists_resulttableentrynegative * S ((S (dst_index_table_exists_resulttable)) * dst_negative_scale_table_exists_resulttable) + (dst_negative_table_exists_resulttable))) /\ (exists ge_balance_positive_table_exists_resulttableentryvalue ge_balance_negative_table_exists_resulttableentryvalue. (((((dst_value_table_exists_resulttable) = 2 * (ge_balance_positive_table_exists_resulttableentryvalue) /\ (ge_balance_negative_table_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_exists_resulttableentryvaluedecode. (((dst_value_table_exists_resulttable) = 2 * ge_signed_half_table_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_exists_resulttableentryvalue) = S ge_signed_half_table_exists_resulttableentryvaluedecode))) /\ ((dst_positive_table_exists_resulttable) + ge_balance_negative_table_exists_resulttableentryvalue = (dst_negative_table_exists_resulttable) + ge_balance_positive_table_exists_resulttableentryvalue))))))))) /\ (forall dc_input_table_exists_result dc_output_table_exists_result. ~(dc_input_table_exists_result=0) -> (exists pvs_le_gap_table_exists_resultdomain. pvs_le_gap_table_exists_resultdomain + (dc_input_table_exists_result) = (N)) -> (exists dst_positive_code_table_exists_resultlookup dst_positive_scale_table_exists_resultlookup dst_negative_code_table_exists_resultlookup dst_negative_scale_table_exists_resultlookup dst_positive_table_exists_resultlookup dst_negative_table_exists_resultlookup. (((H) = (((((dst_positive_code_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup)) * S ((dst_positive_code_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup)) + ((dst_positive_scale_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup))) + (((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) * S ((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) + ((dst_negative_scale_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)))) * S ((((dst_positive_code_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup)) * S ((dst_positive_code_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup)) + ((dst_positive_scale_table_exists_resultlookup) + (dst_positive_scale_table_exists_resultlookup))) + (((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) * S ((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) + ((dst_negative_scale_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)))) + ((((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) * S ((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) + ((dst_negative_scale_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup))) + (((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) * S ((dst_negative_code_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)) + ((dst_negative_scale_table_exists_resultlookup) + (dst_negative_scale_table_exists_resultlookup)))))) /\ (((((exists ff_h_pvs_table_exists_resultlookuppositive. ff_h_pvs_table_exists_resultlookuppositive + S (dst_positive_table_exists_resultlookup) = S ((S (dc_input_table_exists_result)) * dst_positive_scale_table_exists_resultlookup)) /\ exists ff_q_pvs_table_exists_resultlookuppositive. dst_positive_code_table_exists_resultlookup = ff_q_pvs_table_exists_resultlookuppositive * S ((S (dc_input_table_exists_result)) * dst_positive_scale_table_exists_resultlookup) + (dst_positive_table_exists_resultlookup))) /\ (((((exists ff_h_pvs_table_exists_resultlookupnegative. ff_h_pvs_table_exists_resultlookupnegative + S (dst_negative_table_exists_resultlookup) = S ((S (dc_input_table_exists_result)) * dst_negative_scale_table_exists_resultlookup)) /\ exists ff_q_pvs_table_exists_resultlookupnegative. dst_negative_code_table_exists_resultlookup = ff_q_pvs_table_exists_resultlookupnegative * S ((S (dc_input_table_exists_result)) * dst_negative_scale_table_exists_resultlookup) + (dst_negative_table_exists_resultlookup))) /\ (exists ge_balance_positive_table_exists_resultlookupvalue ge_balance_negative_table_exists_resultlookupvalue. (((((dc_output_table_exists_result) = 2 * (ge_balance_positive_table_exists_resultlookupvalue) /\ (ge_balance_negative_table_exists_resultlookupvalue) = 0) \/ exists ge_signed_half_table_exists_resultlookupvaluedecode. (((dc_output_table_exists_result) = 2 * ge_signed_half_table_exists_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultlookupvalue) = 0) /\ (ge_balance_negative_table_exists_resultlookupvalue) = S ge_signed_half_table_exists_resultlookupvaluedecode))) /\ ((dst_positive_table_exists_resultlookup) + ge_balance_negative_table_exists_resultlookupvalue = (dst_negative_table_exists_resultlookup) + ge_balance_positive_table_exists_resultlookupvalue))))))))) -> (((~((dc_input_table_exists_result)=0)) /\ (exists dc_mask_table_exists_resultvalue. ((((exists dst_positive_code_table_exists_resultvaluemasktable dst_positive_scale_table_exists_resultvaluemasktable dst_negative_code_table_exists_resultvaluemasktable dst_negative_scale_table_exists_resultvaluemasktable. (((dc_mask_table_exists_resultvalue) = (((((dst_positive_code_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable)) * S ((dst_positive_code_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable)) + ((dst_positive_scale_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable))) + (((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) * S ((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) + ((dst_negative_scale_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)))) * S ((((dst_positive_code_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable)) * S ((dst_positive_code_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable)) + ((dst_positive_scale_table_exists_resultvaluemasktable) + (dst_positive_scale_table_exists_resultvaluemasktable))) + (((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) * S ((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) + ((dst_negative_scale_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)))) + ((((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) * S ((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) + ((dst_negative_scale_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable))) + (((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) * S ((dst_negative_code_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)) + ((dst_negative_scale_table_exists_resultvaluemasktable) + (dst_negative_scale_table_exists_resultvaluemasktable)))))) /\ (forall dst_index_table_exists_resultvaluemasktable. (exists pvs_le_gap_table_exists_resultvaluemasktabledomain. pvs_le_gap_table_exists_resultvaluemasktabledomain + (dst_index_table_exists_resultvaluemasktable) = (dc_input_table_exists_result)) -> exists dst_positive_table_exists_resultvaluemasktable dst_negative_table_exists_resultvaluemasktable dst_value_table_exists_resultvaluemasktable. ((((exists ff_h_pvs_table_exists_resultvaluemasktableentrypositive. ff_h_pvs_table_exists_resultvaluemasktableentrypositive + S (dst_positive_table_exists_resultvaluemasktable) = S ((S (dst_index_table_exists_resultvaluemasktable)) * dst_positive_scale_table_exists_resultvaluemasktable)) /\ exists ff_q_pvs_table_exists_resultvaluemasktableentrypositive. dst_positive_code_table_exists_resultvaluemasktable = ff_q_pvs_table_exists_resultvaluemasktableentrypositive * S ((S (dst_index_table_exists_resultvaluemasktable)) * dst_positive_scale_table_exists_resultvaluemasktable) + (dst_positive_table_exists_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemasktableentrynegative. ff_h_pvs_table_exists_resultvaluemasktableentrynegative + S (dst_negative_table_exists_resultvaluemasktable) = S ((S (dst_index_table_exists_resultvaluemasktable)) * dst_negative_scale_table_exists_resultvaluemasktable)) /\ exists ff_q_pvs_table_exists_resultvaluemasktableentrynegative. dst_negative_code_table_exists_resultvaluemasktable = ff_q_pvs_table_exists_resultvaluemasktableentrynegative * S ((S (dst_index_table_exists_resultvaluemasktable)) * dst_negative_scale_table_exists_resultvaluemasktable) + (dst_negative_table_exists_resultvaluemasktable))) /\ (exists ge_balance_positive_table_exists_resultvaluemasktableentryvalue ge_balance_negative_table_exists_resultvaluemasktableentryvalue. (((((dst_value_table_exists_resultvaluemasktable) = 2 * (ge_balance_positive_table_exists_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_exists_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_exists_resultvaluemasktableentryvaluedecode. (((dst_value_table_exists_resultvaluemasktable) = 2 * ge_signed_half_table_exists_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_exists_resultvaluemasktableentryvalue) = S ge_signed_half_table_exists_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_exists_resultvaluemasktable) + ge_balance_negative_table_exists_resultvaluemasktableentryvalue = (dst_negative_table_exists_resultvaluemasktable) + ge_balance_positive_table_exists_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_exists_resultvaluemask dc_value_table_exists_resultvaluemask. (exists pvs_le_gap_table_exists_resultvaluemaskdomain. pvs_le_gap_table_exists_resultvaluemaskdomain + (dc_index_table_exists_resultvaluemask) = (dc_input_table_exists_result)) -> (exists dst_positive_code_table_exists_resultvaluemasklookup dst_positive_scale_table_exists_resultvaluemasklookup dst_negative_code_table_exists_resultvaluemasklookup dst_negative_scale_table_exists_resultvaluemasklookup dst_positive_table_exists_resultvaluemasklookup dst_negative_table_exists_resultvaluemasklookup. (((dc_mask_table_exists_resultvalue) = (((((dst_positive_code_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup)) * S ((dst_positive_code_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup)) + ((dst_positive_scale_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup))) + (((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) * S ((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) + ((dst_negative_scale_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)))) * S ((((dst_positive_code_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup)) * S ((dst_positive_code_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup)) + ((dst_positive_scale_table_exists_resultvaluemasklookup) + (dst_positive_scale_table_exists_resultvaluemasklookup))) + (((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) * S ((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) + ((dst_negative_scale_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)))) + ((((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) * S ((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) + ((dst_negative_scale_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup))) + (((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) * S ((dst_negative_code_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)) + ((dst_negative_scale_table_exists_resultvaluemasklookup) + (dst_negative_scale_table_exists_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemasklookuppositive. ff_h_pvs_table_exists_resultvaluemasklookuppositive + S (dst_positive_table_exists_resultvaluemasklookup) = S ((S (dc_index_table_exists_resultvaluemask)) * dst_positive_scale_table_exists_resultvaluemasklookup)) /\ exists ff_q_pvs_table_exists_resultvaluemasklookuppositive. dst_positive_code_table_exists_resultvaluemasklookup = ff_q_pvs_table_exists_resultvaluemasklookuppositive * S ((S (dc_index_table_exists_resultvaluemask)) * dst_positive_scale_table_exists_resultvaluemasklookup) + (dst_positive_table_exists_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemasklookupnegative. ff_h_pvs_table_exists_resultvaluemasklookupnegative + S (dst_negative_table_exists_resultvaluemasklookup) = S ((S (dc_index_table_exists_resultvaluemask)) * dst_negative_scale_table_exists_resultvaluemasklookup)) /\ exists ff_q_pvs_table_exists_resultvaluemasklookupnegative. dst_negative_code_table_exists_resultvaluemasklookup = ff_q_pvs_table_exists_resultvaluemasklookupnegative * S ((S (dc_index_table_exists_resultvaluemask)) * dst_negative_scale_table_exists_resultvaluemasklookup) + (dst_negative_table_exists_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_exists_resultvaluemasklookupvalue ge_balance_negative_table_exists_resultvaluemasklookupvalue. (((((dc_value_table_exists_resultvaluemask) = 2 * (ge_balance_positive_table_exists_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_exists_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_exists_resultvaluemasklookupvaluedecode. (((dc_value_table_exists_resultvaluemask) = 2 * ge_signed_half_table_exists_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_exists_resultvaluemasklookupvalue) = S ge_signed_half_table_exists_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_exists_resultvaluemasklookup) + ge_balance_negative_table_exists_resultvaluemasklookupvalue = (dst_negative_table_exists_resultvaluemasklookup) + ge_balance_positive_table_exists_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_exists_resultvaluemask)=0)) /\ (exists dc_quotient_table_exists_resultvaluemaskentry dc_left_table_exists_resultvaluemaskentry dc_right_table_exists_resultvaluemaskentry. (((dc_input_table_exists_result)=(dc_index_table_exists_resultvaluemask)*dc_quotient_table_exists_resultvaluemaskentry) /\ (((exists dst_positive_code_table_exists_resultvaluemaskentryleft dst_positive_scale_table_exists_resultvaluemaskentryleft dst_negative_code_table_exists_resultvaluemaskentryleft dst_negative_scale_table_exists_resultvaluemaskentryleft dst_positive_table_exists_resultvaluemaskentryleft dst_negative_table_exists_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_positive_code_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft)) + ((dst_positive_scale_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft))) + (((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) + ((dst_negative_scale_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_positive_code_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft)) + ((dst_positive_scale_table_exists_resultvaluemaskentryleft) + (dst_positive_scale_table_exists_resultvaluemaskentryleft))) + (((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) + ((dst_negative_scale_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) + ((dst_negative_scale_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft))) + (((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) * S ((dst_negative_code_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)) + ((dst_negative_scale_table_exists_resultvaluemaskentryleft) + (dst_negative_scale_table_exists_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemaskentryleftpositive. ff_h_pvs_table_exists_resultvaluemaskentryleftpositive + S (dst_positive_table_exists_resultvaluemaskentryleft) = S ((S (dc_index_table_exists_resultvaluemask)) * dst_positive_scale_table_exists_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_exists_resultvaluemaskentryleftpositive. dst_positive_code_table_exists_resultvaluemaskentryleft = ff_q_pvs_table_exists_resultvaluemaskentryleftpositive * S ((S (dc_index_table_exists_resultvaluemask)) * dst_positive_scale_table_exists_resultvaluemaskentryleft) + (dst_positive_table_exists_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemaskentryleftnegative. ff_h_pvs_table_exists_resultvaluemaskentryleftnegative + S (dst_negative_table_exists_resultvaluemaskentryleft) = S ((S (dc_index_table_exists_resultvaluemask)) * dst_negative_scale_table_exists_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_exists_resultvaluemaskentryleftnegative. dst_negative_code_table_exists_resultvaluemaskentryleft = ff_q_pvs_table_exists_resultvaluemaskentryleftnegative * S ((S (dc_index_table_exists_resultvaluemask)) * dst_negative_scale_table_exists_resultvaluemaskentryleft) + (dst_negative_table_exists_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_exists_resultvaluemaskentryleftvalue ge_balance_negative_table_exists_resultvaluemaskentryleftvalue. (((((dc_left_table_exists_resultvaluemaskentry) = 2 * (ge_balance_positive_table_exists_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_exists_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_exists_resultvaluemaskentryleftvaluedecode. (((dc_left_table_exists_resultvaluemaskentry) = 2 * ge_signed_half_table_exists_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_exists_resultvaluemaskentryleftvalue) = S ge_signed_half_table_exists_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_exists_resultvaluemaskentryleft) + ge_balance_negative_table_exists_resultvaluemaskentryleftvalue = (dst_negative_table_exists_resultvaluemaskentryleft) + ge_balance_positive_table_exists_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_exists_resultvaluemaskentryright dst_positive_scale_table_exists_resultvaluemaskentryright dst_negative_code_table_exists_resultvaluemaskentryright dst_negative_scale_table_exists_resultvaluemaskentryright dst_positive_table_exists_resultvaluemaskentryright dst_negative_table_exists_resultvaluemaskentryright. (((G) = (((((dst_positive_code_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright)) * S ((dst_positive_code_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright)) + ((dst_positive_scale_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright))) + (((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) * S ((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) + ((dst_negative_scale_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright)) * S ((dst_positive_code_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright)) + ((dst_positive_scale_table_exists_resultvaluemaskentryright) + (dst_positive_scale_table_exists_resultvaluemaskentryright))) + (((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) * S ((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) + ((dst_negative_scale_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)))) + ((((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) * S ((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) + ((dst_negative_scale_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright))) + (((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) * S ((dst_negative_code_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)) + ((dst_negative_scale_table_exists_resultvaluemaskentryright) + (dst_negative_scale_table_exists_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemaskentryrightpositive. ff_h_pvs_table_exists_resultvaluemaskentryrightpositive + S (dst_positive_table_exists_resultvaluemaskentryright) = S ((S (dc_quotient_table_exists_resultvaluemaskentry)) * dst_positive_scale_table_exists_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_exists_resultvaluemaskentryrightpositive. dst_positive_code_table_exists_resultvaluemaskentryright = ff_q_pvs_table_exists_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_exists_resultvaluemaskentry)) * dst_positive_scale_table_exists_resultvaluemaskentryright) + (dst_positive_table_exists_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_exists_resultvaluemaskentryrightnegative. ff_h_pvs_table_exists_resultvaluemaskentryrightnegative + S (dst_negative_table_exists_resultvaluemaskentryright) = S ((S (dc_quotient_table_exists_resultvaluemaskentry)) * dst_negative_scale_table_exists_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_exists_resultvaluemaskentryrightnegative. dst_negative_code_table_exists_resultvaluemaskentryright = ff_q_pvs_table_exists_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_exists_resultvaluemaskentry)) * dst_negative_scale_table_exists_resultvaluemaskentryright) + (dst_negative_table_exists_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_exists_resultvaluemaskentryrightvalue ge_balance_negative_table_exists_resultvaluemaskentryrightvalue. (((((dc_right_table_exists_resultvaluemaskentry) = 2 * (ge_balance_positive_table_exists_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_exists_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_exists_resultvaluemaskentryrightvaluedecode. (((dc_right_table_exists_resultvaluemaskentry) = 2 * ge_signed_half_table_exists_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_exists_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_exists_resultvaluemaskentryrightvalue) = S ge_signed_half_table_exists_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_exists_resultvaluemaskentryright) + ge_balance_negative_table_exists_resultvaluemaskentryrightvalue = (dst_negative_table_exists_resultvaluemaskentryright) + ge_balance_positive_table_exists_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_exists_resultvaluemaskentryproduct sto_an_table_exists_resultvaluemaskentryproduct sto_bp_table_exists_resultvaluemaskentryproduct sto_bn_table_exists_resultvaluemaskentryproduct sto_cp_table_exists_resultvaluemaskentryproduct sto_cn_table_exists_resultvaluemaskentryproduct. (((((dc_left_table_exists_resultvaluemaskentry) = 2 * (sto_ap_table_exists_resultvaluemaskentryproduct) /\ (sto_an_table_exists_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_exists_resultvaluemaskentryproductleft. (((dc_left_table_exists_resultvaluemaskentry) = 2 * ge_signed_half_table_exists_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_exists_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_exists_resultvaluemaskentryproduct) = S ge_signed_half_table_exists_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_exists_resultvaluemaskentry) = 2 * (sto_bp_table_exists_resultvaluemaskentryproduct) /\ (sto_bn_table_exists_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_exists_resultvaluemaskentryproductright. (((dc_right_table_exists_resultvaluemaskentry) = 2 * ge_signed_half_table_exists_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_exists_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_exists_resultvaluemaskentryproduct) = S ge_signed_half_table_exists_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_exists_resultvaluemask) = 2 * (sto_cp_table_exists_resultvaluemaskentryproduct) /\ (sto_cn_table_exists_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_exists_resultvaluemaskentryproductoutput. (((dc_value_table_exists_resultvaluemask) = 2 * ge_signed_half_table_exists_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_exists_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_exists_resultvaluemaskentryproduct) = S ge_signed_half_table_exists_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_exists_resultvaluemaskentryproduct * sto_bp_table_exists_resultvaluemaskentryproduct + sto_an_table_exists_resultvaluemaskentryproduct * sto_bn_table_exists_resultvaluemaskentryproduct) + sto_cn_table_exists_resultvaluemaskentryproduct = (sto_ap_table_exists_resultvaluemaskentryproduct * sto_bn_table_exists_resultvaluemaskentryproduct + sto_an_table_exists_resultvaluemaskentryproduct * sto_bp_table_exists_resultvaluemaskentryproduct) + sto_cp_table_exists_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_exists_resultvaluemask)=0 \/ ~(exists pvs_factor_table_exists_resultvaluemaskentrynondivisor. (dc_input_table_exists_result) = (dc_index_table_exists_resultvaluemask) * pvs_factor_table_exists_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_exists_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_exists_resultvaluefold dst_positive_scale_table_exists_resultvaluefold dst_negative_code_table_exists_resultvaluefold dst_negative_scale_table_exists_resultvaluefold dst_positive_sum_table_exists_resultvaluefold dst_negative_sum_table_exists_resultvaluefold. (((dc_mask_table_exists_resultvalue) = (((((dst_positive_code_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold)) * S ((dst_positive_code_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold)) + ((dst_positive_scale_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold))) + (((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) * S ((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) + ((dst_negative_scale_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)))) * S ((((dst_positive_code_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold)) * S ((dst_positive_code_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold)) + ((dst_positive_scale_table_exists_resultvaluefold) + (dst_positive_scale_table_exists_resultvaluefold))) + (((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) * S ((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) + ((dst_negative_scale_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)))) + ((((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) * S ((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) + ((dst_negative_scale_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold))) + (((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) * S ((dst_negative_code_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)) + ((dst_negative_scale_table_exists_resultvaluefold) + (dst_negative_scale_table_exists_resultvaluefold)))))) /\ (((exists fs_u_dst_table_exists_resultvaluefoldpositive fs_v_dst_table_exists_resultvaluefoldpositive. ((((exists fs_h_dst_table_exists_resultvaluefoldpositive_body_start. fs_h_dst_table_exists_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_exists_resultvaluefoldpositive)) /\ exists fs_q_dst_table_exists_resultvaluefoldpositive_body_start. fs_u_dst_table_exists_resultvaluefoldpositive = fs_q_dst_table_exists_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_exists_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldpositive_body_terminal. fs_h_dst_table_exists_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_exists_resultvaluefold) = S ((S (S (dc_input_table_exists_result))) * fs_v_dst_table_exists_resultvaluefoldpositive)) /\ exists fs_q_dst_table_exists_resultvaluefoldpositive_body_terminal. fs_u_dst_table_exists_resultvaluefoldpositive = fs_q_dst_table_exists_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_exists_result))) * fs_v_dst_table_exists_resultvaluefoldpositive) + (dst_positive_sum_table_exists_resultvaluefold))) /\ forall fs_i_dst_table_exists_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_exists_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_exists_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_exists_resultvaluefoldpositive_body_steps = S (dc_input_table_exists_result)) -> exists fs_a_dst_table_exists_resultvaluefoldpositive_body_steps fs_r_dst_table_exists_resultvaluefoldpositive_body_steps fs_s_dst_table_exists_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_exists_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_exists_resultvaluefold)) /\ exists fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_exists_resultvaluefold = fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_exists_resultvaluefold) + (fs_a_dst_table_exists_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_exists_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_exists_resultvaluefoldpositive)) /\ exists fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_exists_resultvaluefoldpositive = fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_exists_resultvaluefoldpositive) + (fs_r_dst_table_exists_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_exists_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_exists_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_exists_resultvaluefoldpositive)) /\ exists fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_exists_resultvaluefoldpositive = fs_q_dst_table_exists_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_exists_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_exists_resultvaluefoldpositive) + (fs_s_dst_table_exists_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_exists_resultvaluefoldpositive_body_steps = fs_r_dst_table_exists_resultvaluefoldpositive_body_steps + fs_a_dst_table_exists_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_exists_resultvaluefoldnegative fs_v_dst_table_exists_resultvaluefoldnegative. ((((exists fs_h_dst_table_exists_resultvaluefoldnegative_body_start. fs_h_dst_table_exists_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_exists_resultvaluefoldnegative)) /\ exists fs_q_dst_table_exists_resultvaluefoldnegative_body_start. fs_u_dst_table_exists_resultvaluefoldnegative = fs_q_dst_table_exists_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_exists_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldnegative_body_terminal. fs_h_dst_table_exists_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_exists_resultvaluefold) = S ((S (S (dc_input_table_exists_result))) * fs_v_dst_table_exists_resultvaluefoldnegative)) /\ exists fs_q_dst_table_exists_resultvaluefoldnegative_body_terminal. fs_u_dst_table_exists_resultvaluefoldnegative = fs_q_dst_table_exists_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_exists_result))) * fs_v_dst_table_exists_resultvaluefoldnegative) + (dst_negative_sum_table_exists_resultvaluefold))) /\ forall fs_i_dst_table_exists_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_exists_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_exists_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_exists_resultvaluefoldnegative_body_steps = S (dc_input_table_exists_result)) -> exists fs_a_dst_table_exists_resultvaluefoldnegative_body_steps fs_r_dst_table_exists_resultvaluefoldnegative_body_steps fs_s_dst_table_exists_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_exists_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_exists_resultvaluefold)) /\ exists fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_exists_resultvaluefold = fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_exists_resultvaluefold) + (fs_a_dst_table_exists_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_exists_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_exists_resultvaluefoldnegative)) /\ exists fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_exists_resultvaluefoldnegative = fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_exists_resultvaluefoldnegative) + (fs_r_dst_table_exists_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_exists_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_exists_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_exists_resultvaluefoldnegative)) /\ exists fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_exists_resultvaluefoldnegative = fs_q_dst_table_exists_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_exists_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_exists_resultvaluefoldnegative) + (fs_s_dst_table_exists_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_exists_resultvaluefoldnegative_body_steps = fs_r_dst_table_exists_resultvaluefoldnegative_body_steps + fs_a_dst_table_exists_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_exists_resultvaluefoldresult ge_balance_negative_table_exists_resultvaluefoldresult. (((((dc_output_table_exists_result) = 2 * (ge_balance_positive_table_exists_resultvaluefoldresult) /\ (ge_balance_negative_table_exists_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_exists_resultvaluefoldresultdecode. (((dc_output_table_exists_result) = 2 * ge_signed_half_table_exists_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_exists_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_exists_resultvaluefoldresult) = S ge_signed_half_table_exists_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_exists_resultvaluefold) + ge_balance_negative_table_exists_resultvaluefoldresult = (dst_negative_sum_table_exists_resultvaluefold) + ge_balance_positive_table_exists_resultvaluefoldresult))))))))))))))))))))