Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F G. (exists dst_positive_code_table_total_left dst_positive_scale_table_total_left dst_negative_code_table_total_left dst_negative_scale_table_total_left. (((F) = (((((dst_positive_code_table_total_left) + (dst_positive_scale_table_total_left)) * S ((dst_positive_code_table_total_left) + (dst_positive_scale_table_total_left)) + ((dst_positive_scale_table_total_left) + (dst_positive_scale_table_total_left))) + (((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) * S ((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) + ((dst_negative_scale_table_total_left) + (dst_negative_scale_table_total_left)))) * S ((((dst_positive_code_table_total_left) + (dst_positive_scale_table_total_left)) * S ((dst_positive_code_table_total_left) + (dst_positive_scale_table_total_left)) + ((dst_positive_scale_table_total_left) + (dst_positive_scale_table_total_left))) + (((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) * S ((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) + ((dst_negative_scale_table_total_left) + (dst_negative_scale_table_total_left)))) + ((((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) * S ((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) + ((dst_negative_scale_table_total_left) + (dst_negative_scale_table_total_left))) + (((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) * S ((dst_negative_code_table_total_left) + (dst_negative_scale_table_total_left)) + ((dst_negative_scale_table_total_left) + (dst_negative_scale_table_total_left)))))) /\ (forall dst_index_table_total_left. (exists pvs_le_gap_table_total_leftdomain. pvs_le_gap_table_total_leftdomain + (dst_index_table_total_left) = (N)) -> exists dst_positive_table_total_left dst_negative_table_total_left dst_value_table_total_left. ((((exists ff_h_pvs_table_total_leftentrypositive. ff_h_pvs_table_total_leftentrypositive + S (dst_positive_table_total_left) = S ((S (dst_index_table_total_left)) * dst_positive_scale_table_total_left)) /\ exists ff_q_pvs_table_total_leftentrypositive. dst_positive_code_table_total_left = ff_q_pvs_table_total_leftentrypositive * S ((S (dst_index_table_total_left)) * dst_positive_scale_table_total_left) + (dst_positive_table_total_left))) /\ (((((exists ff_h_pvs_table_total_leftentrynegative. ff_h_pvs_table_total_leftentrynegative + S (dst_negative_table_total_left) = S ((S (dst_index_table_total_left)) * dst_negative_scale_table_total_left)) /\ exists ff_q_pvs_table_total_leftentrynegative. dst_negative_code_table_total_left = ff_q_pvs_table_total_leftentrynegative * S ((S (dst_index_table_total_left)) * dst_negative_scale_table_total_left) + (dst_negative_table_total_left))) /\ (exists ge_balance_positive_table_total_leftentryvalue ge_balance_negative_table_total_leftentryvalue. (((((dst_value_table_total_left) = 2 * (ge_balance_positive_table_total_leftentryvalue) /\ (ge_balance_negative_table_total_leftentryvalue) = 0) \/ exists ge_signed_half_table_total_leftentryvaluedecode. (((dst_value_table_total_left) = 2 * ge_signed_half_table_total_leftentryvaluedecode + 1 /\ (ge_balance_positive_table_total_leftentryvalue) = 0) /\ (ge_balance_negative_table_total_leftentryvalue) = S ge_signed_half_table_total_leftentryvaluedecode))) /\ ((dst_positive_table_total_left) + ge_balance_negative_table_total_leftentryvalue = (dst_negative_table_total_left) + ge_balance_positive_table_total_leftentryvalue))))))))) -> (exists dst_positive_code_table_total_right dst_positive_scale_table_total_right dst_negative_code_table_total_right dst_negative_scale_table_total_right. (((G) = (((((dst_positive_code_table_total_right) + (dst_positive_scale_table_total_right)) * S ((dst_positive_code_table_total_right) + (dst_positive_scale_table_total_right)) + ((dst_positive_scale_table_total_right) + (dst_positive_scale_table_total_right))) + (((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) * S ((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) + ((dst_negative_scale_table_total_right) + (dst_negative_scale_table_total_right)))) * S ((((dst_positive_code_table_total_right) + (dst_positive_scale_table_total_right)) * S ((dst_positive_code_table_total_right) + (dst_positive_scale_table_total_right)) + ((dst_positive_scale_table_total_right) + (dst_positive_scale_table_total_right))) + (((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) * S ((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) + ((dst_negative_scale_table_total_right) + (dst_negative_scale_table_total_right)))) + ((((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) * S ((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) + ((dst_negative_scale_table_total_right) + (dst_negative_scale_table_total_right))) + (((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) * S ((dst_negative_code_table_total_right) + (dst_negative_scale_table_total_right)) + ((dst_negative_scale_table_total_right) + (dst_negative_scale_table_total_right)))))) /\ (forall dst_index_table_total_right. (exists pvs_le_gap_table_total_rightdomain. pvs_le_gap_table_total_rightdomain + (dst_index_table_total_right) = (N)) -> exists dst_positive_table_total_right dst_negative_table_total_right dst_value_table_total_right. ((((exists ff_h_pvs_table_total_rightentrypositive. ff_h_pvs_table_total_rightentrypositive + S (dst_positive_table_total_right) = S ((S (dst_index_table_total_right)) * dst_positive_scale_table_total_right)) /\ exists ff_q_pvs_table_total_rightentrypositive. dst_positive_code_table_total_right = ff_q_pvs_table_total_rightentrypositive * S ((S (dst_index_table_total_right)) * dst_positive_scale_table_total_right) + (dst_positive_table_total_right))) /\ (((((exists ff_h_pvs_table_total_rightentrynegative. ff_h_pvs_table_total_rightentrynegative + S (dst_negative_table_total_right) = S ((S (dst_index_table_total_right)) * dst_negative_scale_table_total_right)) /\ exists ff_q_pvs_table_total_rightentrynegative. dst_negative_code_table_total_right = ff_q_pvs_table_total_rightentrynegative * S ((S (dst_index_table_total_right)) * dst_negative_scale_table_total_right) + (dst_negative_table_total_right))) /\ (exists ge_balance_positive_table_total_rightentryvalue ge_balance_negative_table_total_rightentryvalue. (((((dst_value_table_total_right) = 2 * (ge_balance_positive_table_total_rightentryvalue) /\ (ge_balance_negative_table_total_rightentryvalue) = 0) \/ exists ge_signed_half_table_total_rightentryvaluedecode. (((dst_value_table_total_right) = 2 * ge_signed_half_table_total_rightentryvaluedecode + 1 /\ (ge_balance_positive_table_total_rightentryvalue) = 0) /\ (ge_balance_negative_table_total_rightentryvalue) = S ge_signed_half_table_total_rightentryvaluedecode))) /\ ((dst_positive_table_total_right) + ge_balance_negative_table_total_rightentryvalue = (dst_negative_table_total_right) + ge_balance_positive_table_total_rightentryvalue))))))))) -> exists H. ((((exists dst_positive_code_table_total_resultleft dst_positive_scale_table_total_resultleft dst_negative_code_table_total_resultleft dst_negative_scale_table_total_resultleft. (((F) = (((((dst_positive_code_table_total_resultleft) + (dst_positive_scale_table_total_resultleft)) * S ((dst_positive_code_table_total_resultleft) + (dst_positive_scale_table_total_resultleft)) + ((dst_positive_scale_table_total_resultleft) + (dst_positive_scale_table_total_resultleft))) + (((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) * S ((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) + ((dst_negative_scale_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)))) * S ((((dst_positive_code_table_total_resultleft) + (dst_positive_scale_table_total_resultleft)) * S ((dst_positive_code_table_total_resultleft) + (dst_positive_scale_table_total_resultleft)) + ((dst_positive_scale_table_total_resultleft) + (dst_positive_scale_table_total_resultleft))) + (((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) * S ((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) + ((dst_negative_scale_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)))) + ((((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) * S ((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) + ((dst_negative_scale_table_total_resultleft) + (dst_negative_scale_table_total_resultleft))) + (((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) * S ((dst_negative_code_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)) + ((dst_negative_scale_table_total_resultleft) + (dst_negative_scale_table_total_resultleft)))))) /\ (forall dst_index_table_total_resultleft. (exists pvs_le_gap_table_total_resultleftdomain. pvs_le_gap_table_total_resultleftdomain + (dst_index_table_total_resultleft) = (N)) -> exists dst_positive_table_total_resultleft dst_negative_table_total_resultleft dst_value_table_total_resultleft. ((((exists ff_h_pvs_table_total_resultleftentrypositive. ff_h_pvs_table_total_resultleftentrypositive + S (dst_positive_table_total_resultleft) = S ((S (dst_index_table_total_resultleft)) * dst_positive_scale_table_total_resultleft)) /\ exists ff_q_pvs_table_total_resultleftentrypositive. dst_positive_code_table_total_resultleft = ff_q_pvs_table_total_resultleftentrypositive * S ((S (dst_index_table_total_resultleft)) * dst_positive_scale_table_total_resultleft) + (dst_positive_table_total_resultleft))) /\ (((((exists ff_h_pvs_table_total_resultleftentrynegative. ff_h_pvs_table_total_resultleftentrynegative + S (dst_negative_table_total_resultleft) = S ((S (dst_index_table_total_resultleft)) * dst_negative_scale_table_total_resultleft)) /\ exists ff_q_pvs_table_total_resultleftentrynegative. dst_negative_code_table_total_resultleft = ff_q_pvs_table_total_resultleftentrynegative * S ((S (dst_index_table_total_resultleft)) * dst_negative_scale_table_total_resultleft) + (dst_negative_table_total_resultleft))) /\ (exists ge_balance_positive_table_total_resultleftentryvalue ge_balance_negative_table_total_resultleftentryvalue. (((((dst_value_table_total_resultleft) = 2 * (ge_balance_positive_table_total_resultleftentryvalue) /\ (ge_balance_negative_table_total_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_total_resultleftentryvaluedecode. (((dst_value_table_total_resultleft) = 2 * ge_signed_half_table_total_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_total_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_total_resultleftentryvalue) = S ge_signed_half_table_total_resultleftentryvaluedecode))) /\ ((dst_positive_table_total_resultleft) + ge_balance_negative_table_total_resultleftentryvalue = (dst_negative_table_total_resultleft) + ge_balance_positive_table_total_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_total_resultright dst_positive_scale_table_total_resultright dst_negative_code_table_total_resultright dst_negative_scale_table_total_resultright. (((G) = (((((dst_positive_code_table_total_resultright) + (dst_positive_scale_table_total_resultright)) * S ((dst_positive_code_table_total_resultright) + (dst_positive_scale_table_total_resultright)) + ((dst_positive_scale_table_total_resultright) + (dst_positive_scale_table_total_resultright))) + (((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) * S ((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) + ((dst_negative_scale_table_total_resultright) + (dst_negative_scale_table_total_resultright)))) * S ((((dst_positive_code_table_total_resultright) + (dst_positive_scale_table_total_resultright)) * S ((dst_positive_code_table_total_resultright) + (dst_positive_scale_table_total_resultright)) + ((dst_positive_scale_table_total_resultright) + (dst_positive_scale_table_total_resultright))) + (((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) * S ((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) + ((dst_negative_scale_table_total_resultright) + (dst_negative_scale_table_total_resultright)))) + ((((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) * S ((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) + ((dst_negative_scale_table_total_resultright) + (dst_negative_scale_table_total_resultright))) + (((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) * S ((dst_negative_code_table_total_resultright) + (dst_negative_scale_table_total_resultright)) + ((dst_negative_scale_table_total_resultright) + (dst_negative_scale_table_total_resultright)))))) /\ (forall dst_index_table_total_resultright. (exists pvs_le_gap_table_total_resultrightdomain. pvs_le_gap_table_total_resultrightdomain + (dst_index_table_total_resultright) = (N)) -> exists dst_positive_table_total_resultright dst_negative_table_total_resultright dst_value_table_total_resultright. ((((exists ff_h_pvs_table_total_resultrightentrypositive. ff_h_pvs_table_total_resultrightentrypositive + S (dst_positive_table_total_resultright) = S ((S (dst_index_table_total_resultright)) * dst_positive_scale_table_total_resultright)) /\ exists ff_q_pvs_table_total_resultrightentrypositive. dst_positive_code_table_total_resultright = ff_q_pvs_table_total_resultrightentrypositive * S ((S (dst_index_table_total_resultright)) * dst_positive_scale_table_total_resultright) + (dst_positive_table_total_resultright))) /\ (((((exists ff_h_pvs_table_total_resultrightentrynegative. ff_h_pvs_table_total_resultrightentrynegative + S (dst_negative_table_total_resultright) = S ((S (dst_index_table_total_resultright)) * dst_negative_scale_table_total_resultright)) /\ exists ff_q_pvs_table_total_resultrightentrynegative. dst_negative_code_table_total_resultright = ff_q_pvs_table_total_resultrightentrynegative * S ((S (dst_index_table_total_resultright)) * dst_negative_scale_table_total_resultright) + (dst_negative_table_total_resultright))) /\ (exists ge_balance_positive_table_total_resultrightentryvalue ge_balance_negative_table_total_resultrightentryvalue. (((((dst_value_table_total_resultright) = 2 * (ge_balance_positive_table_total_resultrightentryvalue) /\ (ge_balance_negative_table_total_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_total_resultrightentryvaluedecode. (((dst_value_table_total_resultright) = 2 * ge_signed_half_table_total_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_total_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_total_resultrightentryvalue) = S ge_signed_half_table_total_resultrightentryvaluedecode))) /\ ((dst_positive_table_total_resultright) + ge_balance_negative_table_total_resultrightentryvalue = (dst_negative_table_total_resultright) + ge_balance_positive_table_total_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_total_resulttable dst_positive_scale_table_total_resulttable dst_negative_code_table_total_resulttable dst_negative_scale_table_total_resulttable. (((H) = (((((dst_positive_code_table_total_resulttable) + (dst_positive_scale_table_total_resulttable)) * S ((dst_positive_code_table_total_resulttable) + (dst_positive_scale_table_total_resulttable)) + ((dst_positive_scale_table_total_resulttable) + (dst_positive_scale_table_total_resulttable))) + (((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) * S ((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) + ((dst_negative_scale_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)))) * S ((((dst_positive_code_table_total_resulttable) + (dst_positive_scale_table_total_resulttable)) * S ((dst_positive_code_table_total_resulttable) + (dst_positive_scale_table_total_resulttable)) + ((dst_positive_scale_table_total_resulttable) + (dst_positive_scale_table_total_resulttable))) + (((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) * S ((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) + ((dst_negative_scale_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)))) + ((((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) * S ((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) + ((dst_negative_scale_table_total_resulttable) + (dst_negative_scale_table_total_resulttable))) + (((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) * S ((dst_negative_code_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)) + ((dst_negative_scale_table_total_resulttable) + (dst_negative_scale_table_total_resulttable)))))) /\ (forall dst_index_table_total_resulttable. (exists pvs_le_gap_table_total_resulttabledomain. pvs_le_gap_table_total_resulttabledomain + (dst_index_table_total_resulttable) = (N)) -> exists dst_positive_table_total_resulttable dst_negative_table_total_resulttable dst_value_table_total_resulttable. ((((exists ff_h_pvs_table_total_resulttableentrypositive. ff_h_pvs_table_total_resulttableentrypositive + S (dst_positive_table_total_resulttable) = S ((S (dst_index_table_total_resulttable)) * dst_positive_scale_table_total_resulttable)) /\ exists ff_q_pvs_table_total_resulttableentrypositive. dst_positive_code_table_total_resulttable = ff_q_pvs_table_total_resulttableentrypositive * S ((S (dst_index_table_total_resulttable)) * dst_positive_scale_table_total_resulttable) + (dst_positive_table_total_resulttable))) /\ (((((exists ff_h_pvs_table_total_resulttableentrynegative. ff_h_pvs_table_total_resulttableentrynegative + S (dst_negative_table_total_resulttable) = S ((S (dst_index_table_total_resulttable)) * dst_negative_scale_table_total_resulttable)) /\ exists ff_q_pvs_table_total_resulttableentrynegative. dst_negative_code_table_total_resulttable = ff_q_pvs_table_total_resulttableentrynegative * S ((S (dst_index_table_total_resulttable)) * dst_negative_scale_table_total_resulttable) + (dst_negative_table_total_resulttable))) /\ (exists ge_balance_positive_table_total_resulttableentryvalue ge_balance_negative_table_total_resulttableentryvalue. (((((dst_value_table_total_resulttable) = 2 * (ge_balance_positive_table_total_resulttableentryvalue) /\ (ge_balance_negative_table_total_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_total_resulttableentryvaluedecode. (((dst_value_table_total_resulttable) = 2 * ge_signed_half_table_total_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_total_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_total_resulttableentryvalue) = S ge_signed_half_table_total_resulttableentryvaluedecode))) /\ ((dst_positive_table_total_resulttable) + ge_balance_negative_table_total_resulttableentryvalue = (dst_negative_table_total_resulttable) + ge_balance_positive_table_total_resulttableentryvalue))))))))) /\ (forall dc_input_table_total_result dc_output_table_total_result. ~(dc_input_table_total_result=0) -> (exists pvs_le_gap_table_total_resultdomain. pvs_le_gap_table_total_resultdomain + (dc_input_table_total_result) = (N)) -> (exists dst_positive_code_table_total_resultlookup dst_positive_scale_table_total_resultlookup dst_negative_code_table_total_resultlookup dst_negative_scale_table_total_resultlookup dst_positive_table_total_resultlookup dst_negative_table_total_resultlookup. (((H) = (((((dst_positive_code_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup)) * S ((dst_positive_code_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup)) + ((dst_positive_scale_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup))) + (((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) * S ((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) + ((dst_negative_scale_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)))) * S ((((dst_positive_code_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup)) * S ((dst_positive_code_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup)) + ((dst_positive_scale_table_total_resultlookup) + (dst_positive_scale_table_total_resultlookup))) + (((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) * S ((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) + ((dst_negative_scale_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)))) + ((((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) * S ((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) + ((dst_negative_scale_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup))) + (((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) * S ((dst_negative_code_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)) + ((dst_negative_scale_table_total_resultlookup) + (dst_negative_scale_table_total_resultlookup)))))) /\ (((((exists ff_h_pvs_table_total_resultlookuppositive. ff_h_pvs_table_total_resultlookuppositive + S (dst_positive_table_total_resultlookup) = S ((S (dc_input_table_total_result)) * dst_positive_scale_table_total_resultlookup)) /\ exists ff_q_pvs_table_total_resultlookuppositive. dst_positive_code_table_total_resultlookup = ff_q_pvs_table_total_resultlookuppositive * S ((S (dc_input_table_total_result)) * dst_positive_scale_table_total_resultlookup) + (dst_positive_table_total_resultlookup))) /\ (((((exists ff_h_pvs_table_total_resultlookupnegative. ff_h_pvs_table_total_resultlookupnegative + S (dst_negative_table_total_resultlookup) = S ((S (dc_input_table_total_result)) * dst_negative_scale_table_total_resultlookup)) /\ exists ff_q_pvs_table_total_resultlookupnegative. dst_negative_code_table_total_resultlookup = ff_q_pvs_table_total_resultlookupnegative * S ((S (dc_input_table_total_result)) * dst_negative_scale_table_total_resultlookup) + (dst_negative_table_total_resultlookup))) /\ (exists ge_balance_positive_table_total_resultlookupvalue ge_balance_negative_table_total_resultlookupvalue. (((((dc_output_table_total_result) = 2 * (ge_balance_positive_table_total_resultlookupvalue) /\ (ge_balance_negative_table_total_resultlookupvalue) = 0) \/ exists ge_signed_half_table_total_resultlookupvaluedecode. (((dc_output_table_total_result) = 2 * ge_signed_half_table_total_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_total_resultlookupvalue) = 0) /\ (ge_balance_negative_table_total_resultlookupvalue) = S ge_signed_half_table_total_resultlookupvaluedecode))) /\ ((dst_positive_table_total_resultlookup) + ge_balance_negative_table_total_resultlookupvalue = (dst_negative_table_total_resultlookup) + ge_balance_positive_table_total_resultlookupvalue))))))))) -> (((~((dc_input_table_total_result)=0)) /\ (exists dc_mask_table_total_resultvalue. ((((exists dst_positive_code_table_total_resultvaluemasktable dst_positive_scale_table_total_resultvaluemasktable dst_negative_code_table_total_resultvaluemasktable dst_negative_scale_table_total_resultvaluemasktable. (((dc_mask_table_total_resultvalue) = (((((dst_positive_code_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable)) * S ((dst_positive_code_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable)) + ((dst_positive_scale_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable))) + (((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) * S ((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) + ((dst_negative_scale_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)))) * S ((((dst_positive_code_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable)) * S ((dst_positive_code_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable)) + ((dst_positive_scale_table_total_resultvaluemasktable) + (dst_positive_scale_table_total_resultvaluemasktable))) + (((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) * S ((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) + ((dst_negative_scale_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)))) + ((((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) * S ((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) + ((dst_negative_scale_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable))) + (((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) * S ((dst_negative_code_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)) + ((dst_negative_scale_table_total_resultvaluemasktable) + (dst_negative_scale_table_total_resultvaluemasktable)))))) /\ (forall dst_index_table_total_resultvaluemasktable. (exists pvs_le_gap_table_total_resultvaluemasktabledomain. pvs_le_gap_table_total_resultvaluemasktabledomain + (dst_index_table_total_resultvaluemasktable) = (dc_input_table_total_result)) -> exists dst_positive_table_total_resultvaluemasktable dst_negative_table_total_resultvaluemasktable dst_value_table_total_resultvaluemasktable. ((((exists ff_h_pvs_table_total_resultvaluemasktableentrypositive. ff_h_pvs_table_total_resultvaluemasktableentrypositive + S (dst_positive_table_total_resultvaluemasktable) = S ((S (dst_index_table_total_resultvaluemasktable)) * dst_positive_scale_table_total_resultvaluemasktable)) /\ exists ff_q_pvs_table_total_resultvaluemasktableentrypositive. dst_positive_code_table_total_resultvaluemasktable = ff_q_pvs_table_total_resultvaluemasktableentrypositive * S ((S (dst_index_table_total_resultvaluemasktable)) * dst_positive_scale_table_total_resultvaluemasktable) + (dst_positive_table_total_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_total_resultvaluemasktableentrynegative. ff_h_pvs_table_total_resultvaluemasktableentrynegative + S (dst_negative_table_total_resultvaluemasktable) = S ((S (dst_index_table_total_resultvaluemasktable)) * dst_negative_scale_table_total_resultvaluemasktable)) /\ exists ff_q_pvs_table_total_resultvaluemasktableentrynegative. dst_negative_code_table_total_resultvaluemasktable = ff_q_pvs_table_total_resultvaluemasktableentrynegative * S ((S (dst_index_table_total_resultvaluemasktable)) * dst_negative_scale_table_total_resultvaluemasktable) + (dst_negative_table_total_resultvaluemasktable))) /\ (exists ge_balance_positive_table_total_resultvaluemasktableentryvalue ge_balance_negative_table_total_resultvaluemasktableentryvalue. (((((dst_value_table_total_resultvaluemasktable) = 2 * (ge_balance_positive_table_total_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_total_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_total_resultvaluemasktableentryvaluedecode. (((dst_value_table_total_resultvaluemasktable) = 2 * ge_signed_half_table_total_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_total_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_total_resultvaluemasktableentryvalue) = S ge_signed_half_table_total_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_total_resultvaluemasktable) + ge_balance_negative_table_total_resultvaluemasktableentryvalue = (dst_negative_table_total_resultvaluemasktable) + ge_balance_positive_table_total_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_total_resultvaluemask dc_value_table_total_resultvaluemask. (exists pvs_le_gap_table_total_resultvaluemaskdomain. pvs_le_gap_table_total_resultvaluemaskdomain + (dc_index_table_total_resultvaluemask) = (dc_input_table_total_result)) -> (exists dst_positive_code_table_total_resultvaluemasklookup dst_positive_scale_table_total_resultvaluemasklookup dst_negative_code_table_total_resultvaluemasklookup dst_negative_scale_table_total_resultvaluemasklookup dst_positive_table_total_resultvaluemasklookup dst_negative_table_total_resultvaluemasklookup. (((dc_mask_table_total_resultvalue) = (((((dst_positive_code_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup)) * S ((dst_positive_code_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup)) + ((dst_positive_scale_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup))) + (((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) * S ((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) + ((dst_negative_scale_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)))) * S ((((dst_positive_code_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup)) * S ((dst_positive_code_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup)) + ((dst_positive_scale_table_total_resultvaluemasklookup) + (dst_positive_scale_table_total_resultvaluemasklookup))) + (((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) * S ((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) + ((dst_negative_scale_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)))) + ((((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) * S ((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) + ((dst_negative_scale_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup))) + (((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) * S ((dst_negative_code_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)) + ((dst_negative_scale_table_total_resultvaluemasklookup) + (dst_negative_scale_table_total_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_total_resultvaluemasklookuppositive. ff_h_pvs_table_total_resultvaluemasklookuppositive + S (dst_positive_table_total_resultvaluemasklookup) = S ((S (dc_index_table_total_resultvaluemask)) * dst_positive_scale_table_total_resultvaluemasklookup)) /\ exists ff_q_pvs_table_total_resultvaluemasklookuppositive. dst_positive_code_table_total_resultvaluemasklookup = ff_q_pvs_table_total_resultvaluemasklookuppositive * S ((S (dc_index_table_total_resultvaluemask)) * dst_positive_scale_table_total_resultvaluemasklookup) + (dst_positive_table_total_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_total_resultvaluemasklookupnegative. ff_h_pvs_table_total_resultvaluemasklookupnegative + S (dst_negative_table_total_resultvaluemasklookup) = S ((S (dc_index_table_total_resultvaluemask)) * dst_negative_scale_table_total_resultvaluemasklookup)) /\ exists ff_q_pvs_table_total_resultvaluemasklookupnegative. dst_negative_code_table_total_resultvaluemasklookup = ff_q_pvs_table_total_resultvaluemasklookupnegative * S ((S (dc_index_table_total_resultvaluemask)) * dst_negative_scale_table_total_resultvaluemasklookup) + (dst_negative_table_total_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_total_resultvaluemasklookupvalue ge_balance_negative_table_total_resultvaluemasklookupvalue. (((((dc_value_table_total_resultvaluemask) = 2 * (ge_balance_positive_table_total_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_total_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_total_resultvaluemasklookupvaluedecode. (((dc_value_table_total_resultvaluemask) = 2 * ge_signed_half_table_total_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_total_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_total_resultvaluemasklookupvalue) = S ge_signed_half_table_total_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_total_resultvaluemasklookup) + ge_balance_negative_table_total_resultvaluemasklookupvalue = (dst_negative_table_total_resultvaluemasklookup) + ge_balance_positive_table_total_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_total_resultvaluemask)=0)) /\ (exists dc_quotient_table_total_resultvaluemaskentry dc_left_table_total_resultvaluemaskentry dc_right_table_total_resultvaluemaskentry. (((dc_input_table_total_result)=(dc_index_table_total_resultvaluemask)*dc_quotient_table_total_resultvaluemaskentry) /\ (((exists dst_positive_code_table_total_resultvaluemaskentryleft dst_positive_scale_table_total_resultvaluemaskentryleft dst_negative_code_table_total_resultvaluemaskentryleft dst_negative_scale_table_total_resultvaluemaskentryleft dst_positive_table_total_resultvaluemaskentryleft dst_negative_table_total_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft)) * S ((dst_positive_code_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft)) + ((dst_positive_scale_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft))) + (((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) * S ((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) + ((dst_negative_scale_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft)) * S ((dst_positive_code_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft)) + ((dst_positive_scale_table_total_resultvaluemaskentryleft) + (dst_positive_scale_table_total_resultvaluemaskentryleft))) + (((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) * S ((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) + ((dst_negative_scale_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) * S ((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) + ((dst_negative_scale_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft))) + (((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) * S ((dst_negative_code_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)) + ((dst_negative_scale_table_total_resultvaluemaskentryleft) + (dst_negative_scale_table_total_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_total_resultvaluemaskentryleftpositive. ff_h_pvs_table_total_resultvaluemaskentryleftpositive + S (dst_positive_table_total_resultvaluemaskentryleft) = S ((S (dc_index_table_total_resultvaluemask)) * dst_positive_scale_table_total_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_total_resultvaluemaskentryleftpositive. dst_positive_code_table_total_resultvaluemaskentryleft = ff_q_pvs_table_total_resultvaluemaskentryleftpositive * S ((S (dc_index_table_total_resultvaluemask)) * dst_positive_scale_table_total_resultvaluemaskentryleft) + (dst_positive_table_total_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_total_resultvaluemaskentryleftnegative. ff_h_pvs_table_total_resultvaluemaskentryleftnegative + S (dst_negative_table_total_resultvaluemaskentryleft) = S ((S (dc_index_table_total_resultvaluemask)) * dst_negative_scale_table_total_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_total_resultvaluemaskentryleftnegative. dst_negative_code_table_total_resultvaluemaskentryleft = ff_q_pvs_table_total_resultvaluemaskentryleftnegative * S ((S (dc_index_table_total_resultvaluemask)) * dst_negative_scale_table_total_resultvaluemaskentryleft) + (dst_negative_table_total_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_total_resultvaluemaskentryleftvalue ge_balance_negative_table_total_resultvaluemaskentryleftvalue. (((((dc_left_table_total_resultvaluemaskentry) = 2 * (ge_balance_positive_table_total_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_total_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_total_resultvaluemaskentryleftvaluedecode. (((dc_left_table_total_resultvaluemaskentry) = 2 * ge_signed_half_table_total_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_total_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_total_resultvaluemaskentryleftvalue) = S ge_signed_half_table_total_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_total_resultvaluemaskentryleft) + ge_balance_negative_table_total_resultvaluemaskentryleftvalue = (dst_negative_table_total_resultvaluemaskentryleft) + ge_balance_positive_table_total_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_total_resultvaluemaskentryright dst_positive_scale_table_total_resultvaluemaskentryright dst_negative_code_table_total_resultvaluemaskentryright dst_negative_scale_table_total_resultvaluemaskentryright dst_positive_table_total_resultvaluemaskentryright dst_negative_table_total_resultvaluemaskentryright. (((G) = (((((dst_positive_code_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright)) * S ((dst_positive_code_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright)) + ((dst_positive_scale_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright))) + (((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) * S ((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) + ((dst_negative_scale_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright)) * S ((dst_positive_code_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright)) + ((dst_positive_scale_table_total_resultvaluemaskentryright) + (dst_positive_scale_table_total_resultvaluemaskentryright))) + (((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) * S ((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) + ((dst_negative_scale_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)))) + ((((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) * S ((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) + ((dst_negative_scale_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright))) + (((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) * S ((dst_negative_code_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)) + ((dst_negative_scale_table_total_resultvaluemaskentryright) + (dst_negative_scale_table_total_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_total_resultvaluemaskentryrightpositive. ff_h_pvs_table_total_resultvaluemaskentryrightpositive + S (dst_positive_table_total_resultvaluemaskentryright) = S ((S (dc_quotient_table_total_resultvaluemaskentry)) * dst_positive_scale_table_total_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_total_resultvaluemaskentryrightpositive. dst_positive_code_table_total_resultvaluemaskentryright = ff_q_pvs_table_total_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_total_resultvaluemaskentry)) * dst_positive_scale_table_total_resultvaluemaskentryright) + (dst_positive_table_total_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_total_resultvaluemaskentryrightnegative. ff_h_pvs_table_total_resultvaluemaskentryrightnegative + S (dst_negative_table_total_resultvaluemaskentryright) = S ((S (dc_quotient_table_total_resultvaluemaskentry)) * dst_negative_scale_table_total_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_total_resultvaluemaskentryrightnegative. dst_negative_code_table_total_resultvaluemaskentryright = ff_q_pvs_table_total_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_total_resultvaluemaskentry)) * dst_negative_scale_table_total_resultvaluemaskentryright) + (dst_negative_table_total_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_total_resultvaluemaskentryrightvalue ge_balance_negative_table_total_resultvaluemaskentryrightvalue. (((((dc_right_table_total_resultvaluemaskentry) = 2 * (ge_balance_positive_table_total_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_total_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_total_resultvaluemaskentryrightvaluedecode. (((dc_right_table_total_resultvaluemaskentry) = 2 * ge_signed_half_table_total_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_total_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_total_resultvaluemaskentryrightvalue) = S ge_signed_half_table_total_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_total_resultvaluemaskentryright) + ge_balance_negative_table_total_resultvaluemaskentryrightvalue = (dst_negative_table_total_resultvaluemaskentryright) + ge_balance_positive_table_total_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_total_resultvaluemaskentryproduct sto_an_table_total_resultvaluemaskentryproduct sto_bp_table_total_resultvaluemaskentryproduct sto_bn_table_total_resultvaluemaskentryproduct sto_cp_table_total_resultvaluemaskentryproduct sto_cn_table_total_resultvaluemaskentryproduct. (((((dc_left_table_total_resultvaluemaskentry) = 2 * (sto_ap_table_total_resultvaluemaskentryproduct) /\ (sto_an_table_total_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_resultvaluemaskentryproductleft. (((dc_left_table_total_resultvaluemaskentry) = 2 * ge_signed_half_table_total_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_total_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_total_resultvaluemaskentryproduct) = S ge_signed_half_table_total_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_total_resultvaluemaskentry) = 2 * (sto_bp_table_total_resultvaluemaskentryproduct) /\ (sto_bn_table_total_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_resultvaluemaskentryproductright. (((dc_right_table_total_resultvaluemaskentry) = 2 * ge_signed_half_table_total_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_total_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_total_resultvaluemaskentryproduct) = S ge_signed_half_table_total_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_total_resultvaluemask) = 2 * (sto_cp_table_total_resultvaluemaskentryproduct) /\ (sto_cn_table_total_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_resultvaluemaskentryproductoutput. (((dc_value_table_total_resultvaluemask) = 2 * ge_signed_half_table_total_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_total_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_total_resultvaluemaskentryproduct) = S ge_signed_half_table_total_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_total_resultvaluemaskentryproduct * sto_bp_table_total_resultvaluemaskentryproduct + sto_an_table_total_resultvaluemaskentryproduct * sto_bn_table_total_resultvaluemaskentryproduct) + sto_cn_table_total_resultvaluemaskentryproduct = (sto_ap_table_total_resultvaluemaskentryproduct * sto_bn_table_total_resultvaluemaskentryproduct + sto_an_table_total_resultvaluemaskentryproduct * sto_bp_table_total_resultvaluemaskentryproduct) + sto_cp_table_total_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_total_resultvaluemask)=0 \/ ~(exists pvs_factor_table_total_resultvaluemaskentrynondivisor. (dc_input_table_total_result) = (dc_index_table_total_resultvaluemask) * pvs_factor_table_total_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_total_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_total_resultvaluefold dst_positive_scale_table_total_resultvaluefold dst_negative_code_table_total_resultvaluefold dst_negative_scale_table_total_resultvaluefold dst_positive_sum_table_total_resultvaluefold dst_negative_sum_table_total_resultvaluefold. (((dc_mask_table_total_resultvalue) = (((((dst_positive_code_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold)) * S ((dst_positive_code_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold)) + ((dst_positive_scale_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold))) + (((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) * S ((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) + ((dst_negative_scale_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)))) * S ((((dst_positive_code_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold)) * S ((dst_positive_code_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold)) + ((dst_positive_scale_table_total_resultvaluefold) + (dst_positive_scale_table_total_resultvaluefold))) + (((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) * S ((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) + ((dst_negative_scale_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)))) + ((((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) * S ((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) + ((dst_negative_scale_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold))) + (((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) * S ((dst_negative_code_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)) + ((dst_negative_scale_table_total_resultvaluefold) + (dst_negative_scale_table_total_resultvaluefold)))))) /\ (((exists fs_u_dst_table_total_resultvaluefoldpositive fs_v_dst_table_total_resultvaluefoldpositive. ((((exists fs_h_dst_table_total_resultvaluefoldpositive_body_start. fs_h_dst_table_total_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_total_resultvaluefoldpositive)) /\ exists fs_q_dst_table_total_resultvaluefoldpositive_body_start. fs_u_dst_table_total_resultvaluefoldpositive = fs_q_dst_table_total_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_total_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldpositive_body_terminal. fs_h_dst_table_total_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_total_resultvaluefold) = S ((S (S (dc_input_table_total_result))) * fs_v_dst_table_total_resultvaluefoldpositive)) /\ exists fs_q_dst_table_total_resultvaluefoldpositive_body_terminal. fs_u_dst_table_total_resultvaluefoldpositive = fs_q_dst_table_total_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_total_result))) * fs_v_dst_table_total_resultvaluefoldpositive) + (dst_positive_sum_table_total_resultvaluefold))) /\ forall fs_i_dst_table_total_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_total_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_total_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_total_resultvaluefoldpositive_body_steps = S (dc_input_table_total_result)) -> exists fs_a_dst_table_total_resultvaluefoldpositive_body_steps fs_r_dst_table_total_resultvaluefoldpositive_body_steps fs_s_dst_table_total_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_total_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_total_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_total_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_total_resultvaluefold)) /\ exists fs_q_dst_table_total_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_total_resultvaluefold = fs_q_dst_table_total_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_total_resultvaluefold) + (fs_a_dst_table_total_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_total_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_total_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_total_resultvaluefoldpositive)) /\ exists fs_q_dst_table_total_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_total_resultvaluefoldpositive = fs_q_dst_table_total_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_total_resultvaluefoldpositive) + (fs_r_dst_table_total_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_total_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_total_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_total_resultvaluefoldpositive)) /\ exists fs_q_dst_table_total_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_total_resultvaluefoldpositive = fs_q_dst_table_total_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_total_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_total_resultvaluefoldpositive) + (fs_s_dst_table_total_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_total_resultvaluefoldpositive_body_steps = fs_r_dst_table_total_resultvaluefoldpositive_body_steps + fs_a_dst_table_total_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_total_resultvaluefoldnegative fs_v_dst_table_total_resultvaluefoldnegative. ((((exists fs_h_dst_table_total_resultvaluefoldnegative_body_start. fs_h_dst_table_total_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_total_resultvaluefoldnegative)) /\ exists fs_q_dst_table_total_resultvaluefoldnegative_body_start. fs_u_dst_table_total_resultvaluefoldnegative = fs_q_dst_table_total_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_total_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldnegative_body_terminal. fs_h_dst_table_total_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_total_resultvaluefold) = S ((S (S (dc_input_table_total_result))) * fs_v_dst_table_total_resultvaluefoldnegative)) /\ exists fs_q_dst_table_total_resultvaluefoldnegative_body_terminal. fs_u_dst_table_total_resultvaluefoldnegative = fs_q_dst_table_total_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_total_result))) * fs_v_dst_table_total_resultvaluefoldnegative) + (dst_negative_sum_table_total_resultvaluefold))) /\ forall fs_i_dst_table_total_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_total_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_total_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_total_resultvaluefoldnegative_body_steps = S (dc_input_table_total_result)) -> exists fs_a_dst_table_total_resultvaluefoldnegative_body_steps fs_r_dst_table_total_resultvaluefoldnegative_body_steps fs_s_dst_table_total_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_total_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_total_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_total_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_total_resultvaluefold)) /\ exists fs_q_dst_table_total_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_total_resultvaluefold = fs_q_dst_table_total_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_total_resultvaluefold) + (fs_a_dst_table_total_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_total_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_total_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_total_resultvaluefoldnegative)) /\ exists fs_q_dst_table_total_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_total_resultvaluefoldnegative = fs_q_dst_table_total_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_total_resultvaluefoldnegative) + (fs_r_dst_table_total_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_total_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_total_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_total_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_total_resultvaluefoldnegative)) /\ exists fs_q_dst_table_total_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_total_resultvaluefoldnegative = fs_q_dst_table_total_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_total_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_total_resultvaluefoldnegative) + (fs_s_dst_table_total_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_total_resultvaluefoldnegative_body_steps = fs_r_dst_table_total_resultvaluefoldnegative_body_steps + fs_a_dst_table_total_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_total_resultvaluefoldresult ge_balance_negative_table_total_resultvaluefoldresult. (((((dc_output_table_total_result) = 2 * (ge_balance_positive_table_total_resultvaluefoldresult) /\ (ge_balance_negative_table_total_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_total_resultvaluefoldresultdecode. (((dc_output_table_total_result) = 2 * ge_signed_half_table_total_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_total_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_total_resultvaluefoldresult) = S ge_signed_half_table_total_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_total_resultvaluefold) + ge_balance_negative_table_total_resultvaluefoldresult = (dst_negative_sum_table_total_resultvaluefold) + ge_balance_positive_table_total_resultvaluefoldresult)))))))))))))))))))) /\ (forall K. (((exists dst_positive_code_table_total_otherleft dst_positive_scale_table_total_otherleft dst_negative_code_table_total_otherleft dst_negative_scale_table_total_otherleft. (((F) = (((((dst_positive_code_table_total_otherleft) + (dst_positive_scale_table_total_otherleft)) * S ((dst_positive_code_table_total_otherleft) + (dst_positive_scale_table_total_otherleft)) + ((dst_positive_scale_table_total_otherleft) + (dst_positive_scale_table_total_otherleft))) + (((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) * S ((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) + ((dst_negative_scale_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)))) * S ((((dst_positive_code_table_total_otherleft) + (dst_positive_scale_table_total_otherleft)) * S ((dst_positive_code_table_total_otherleft) + (dst_positive_scale_table_total_otherleft)) + ((dst_positive_scale_table_total_otherleft) + (dst_positive_scale_table_total_otherleft))) + (((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) * S ((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) + ((dst_negative_scale_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)))) + ((((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) * S ((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) + ((dst_negative_scale_table_total_otherleft) + (dst_negative_scale_table_total_otherleft))) + (((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) * S ((dst_negative_code_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)) + ((dst_negative_scale_table_total_otherleft) + (dst_negative_scale_table_total_otherleft)))))) /\ (forall dst_index_table_total_otherleft. (exists pvs_le_gap_table_total_otherleftdomain. pvs_le_gap_table_total_otherleftdomain + (dst_index_table_total_otherleft) = (N)) -> exists dst_positive_table_total_otherleft dst_negative_table_total_otherleft dst_value_table_total_otherleft. ((((exists ff_h_pvs_table_total_otherleftentrypositive. ff_h_pvs_table_total_otherleftentrypositive + S (dst_positive_table_total_otherleft) = S ((S (dst_index_table_total_otherleft)) * dst_positive_scale_table_total_otherleft)) /\ exists ff_q_pvs_table_total_otherleftentrypositive. dst_positive_code_table_total_otherleft = ff_q_pvs_table_total_otherleftentrypositive * S ((S (dst_index_table_total_otherleft)) * dst_positive_scale_table_total_otherleft) + (dst_positive_table_total_otherleft))) /\ (((((exists ff_h_pvs_table_total_otherleftentrynegative. ff_h_pvs_table_total_otherleftentrynegative + S (dst_negative_table_total_otherleft) = S ((S (dst_index_table_total_otherleft)) * dst_negative_scale_table_total_otherleft)) /\ exists ff_q_pvs_table_total_otherleftentrynegative. dst_negative_code_table_total_otherleft = ff_q_pvs_table_total_otherleftentrynegative * S ((S (dst_index_table_total_otherleft)) * dst_negative_scale_table_total_otherleft) + (dst_negative_table_total_otherleft))) /\ (exists ge_balance_positive_table_total_otherleftentryvalue ge_balance_negative_table_total_otherleftentryvalue. (((((dst_value_table_total_otherleft) = 2 * (ge_balance_positive_table_total_otherleftentryvalue) /\ (ge_balance_negative_table_total_otherleftentryvalue) = 0) \/ exists ge_signed_half_table_total_otherleftentryvaluedecode. (((dst_value_table_total_otherleft) = 2 * ge_signed_half_table_total_otherleftentryvaluedecode + 1 /\ (ge_balance_positive_table_total_otherleftentryvalue) = 0) /\ (ge_balance_negative_table_total_otherleftentryvalue) = S ge_signed_half_table_total_otherleftentryvaluedecode))) /\ ((dst_positive_table_total_otherleft) + ge_balance_negative_table_total_otherleftentryvalue = (dst_negative_table_total_otherleft) + ge_balance_positive_table_total_otherleftentryvalue))))))))) /\ (((exists dst_positive_code_table_total_otherright dst_positive_scale_table_total_otherright dst_negative_code_table_total_otherright dst_negative_scale_table_total_otherright. (((G) = (((((dst_positive_code_table_total_otherright) + (dst_positive_scale_table_total_otherright)) * S ((dst_positive_code_table_total_otherright) + (dst_positive_scale_table_total_otherright)) + ((dst_positive_scale_table_total_otherright) + (dst_positive_scale_table_total_otherright))) + (((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) * S ((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) + ((dst_negative_scale_table_total_otherright) + (dst_negative_scale_table_total_otherright)))) * S ((((dst_positive_code_table_total_otherright) + (dst_positive_scale_table_total_otherright)) * S ((dst_positive_code_table_total_otherright) + (dst_positive_scale_table_total_otherright)) + ((dst_positive_scale_table_total_otherright) + (dst_positive_scale_table_total_otherright))) + (((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) * S ((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) + ((dst_negative_scale_table_total_otherright) + (dst_negative_scale_table_total_otherright)))) + ((((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) * S ((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) + ((dst_negative_scale_table_total_otherright) + (dst_negative_scale_table_total_otherright))) + (((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) * S ((dst_negative_code_table_total_otherright) + (dst_negative_scale_table_total_otherright)) + ((dst_negative_scale_table_total_otherright) + (dst_negative_scale_table_total_otherright)))))) /\ (forall dst_index_table_total_otherright. (exists pvs_le_gap_table_total_otherrightdomain. pvs_le_gap_table_total_otherrightdomain + (dst_index_table_total_otherright) = (N)) -> exists dst_positive_table_total_otherright dst_negative_table_total_otherright dst_value_table_total_otherright. ((((exists ff_h_pvs_table_total_otherrightentrypositive. ff_h_pvs_table_total_otherrightentrypositive + S (dst_positive_table_total_otherright) = S ((S (dst_index_table_total_otherright)) * dst_positive_scale_table_total_otherright)) /\ exists ff_q_pvs_table_total_otherrightentrypositive. dst_positive_code_table_total_otherright = ff_q_pvs_table_total_otherrightentrypositive * S ((S (dst_index_table_total_otherright)) * dst_positive_scale_table_total_otherright) + (dst_positive_table_total_otherright))) /\ (((((exists ff_h_pvs_table_total_otherrightentrynegative. ff_h_pvs_table_total_otherrightentrynegative + S (dst_negative_table_total_otherright) = S ((S (dst_index_table_total_otherright)) * dst_negative_scale_table_total_otherright)) /\ exists ff_q_pvs_table_total_otherrightentrynegative. dst_negative_code_table_total_otherright = ff_q_pvs_table_total_otherrightentrynegative * S ((S (dst_index_table_total_otherright)) * dst_negative_scale_table_total_otherright) + (dst_negative_table_total_otherright))) /\ (exists ge_balance_positive_table_total_otherrightentryvalue ge_balance_negative_table_total_otherrightentryvalue. (((((dst_value_table_total_otherright) = 2 * (ge_balance_positive_table_total_otherrightentryvalue) /\ (ge_balance_negative_table_total_otherrightentryvalue) = 0) \/ exists ge_signed_half_table_total_otherrightentryvaluedecode. (((dst_value_table_total_otherright) = 2 * ge_signed_half_table_total_otherrightentryvaluedecode + 1 /\ (ge_balance_positive_table_total_otherrightentryvalue) = 0) /\ (ge_balance_negative_table_total_otherrightentryvalue) = S ge_signed_half_table_total_otherrightentryvaluedecode))) /\ ((dst_positive_table_total_otherright) + ge_balance_negative_table_total_otherrightentryvalue = (dst_negative_table_total_otherright) + ge_balance_positive_table_total_otherrightentryvalue))))))))) /\ (((exists dst_positive_code_table_total_othertable dst_positive_scale_table_total_othertable dst_negative_code_table_total_othertable dst_negative_scale_table_total_othertable. (((K) = (((((dst_positive_code_table_total_othertable) + (dst_positive_scale_table_total_othertable)) * S ((dst_positive_code_table_total_othertable) + (dst_positive_scale_table_total_othertable)) + ((dst_positive_scale_table_total_othertable) + (dst_positive_scale_table_total_othertable))) + (((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) * S ((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) + ((dst_negative_scale_table_total_othertable) + (dst_negative_scale_table_total_othertable)))) * S ((((dst_positive_code_table_total_othertable) + (dst_positive_scale_table_total_othertable)) * S ((dst_positive_code_table_total_othertable) + (dst_positive_scale_table_total_othertable)) + ((dst_positive_scale_table_total_othertable) + (dst_positive_scale_table_total_othertable))) + (((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) * S ((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) + ((dst_negative_scale_table_total_othertable) + (dst_negative_scale_table_total_othertable)))) + ((((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) * S ((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) + ((dst_negative_scale_table_total_othertable) + (dst_negative_scale_table_total_othertable))) + (((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) * S ((dst_negative_code_table_total_othertable) + (dst_negative_scale_table_total_othertable)) + ((dst_negative_scale_table_total_othertable) + (dst_negative_scale_table_total_othertable)))))) /\ (forall dst_index_table_total_othertable. (exists pvs_le_gap_table_total_othertabledomain. pvs_le_gap_table_total_othertabledomain + (dst_index_table_total_othertable) = (N)) -> exists dst_positive_table_total_othertable dst_negative_table_total_othertable dst_value_table_total_othertable. ((((exists ff_h_pvs_table_total_othertableentrypositive. ff_h_pvs_table_total_othertableentrypositive + S (dst_positive_table_total_othertable) = S ((S (dst_index_table_total_othertable)) * dst_positive_scale_table_total_othertable)) /\ exists ff_q_pvs_table_total_othertableentrypositive. dst_positive_code_table_total_othertable = ff_q_pvs_table_total_othertableentrypositive * S ((S (dst_index_table_total_othertable)) * dst_positive_scale_table_total_othertable) + (dst_positive_table_total_othertable))) /\ (((((exists ff_h_pvs_table_total_othertableentrynegative. ff_h_pvs_table_total_othertableentrynegative + S (dst_negative_table_total_othertable) = S ((S (dst_index_table_total_othertable)) * dst_negative_scale_table_total_othertable)) /\ exists ff_q_pvs_table_total_othertableentrynegative. dst_negative_code_table_total_othertable = ff_q_pvs_table_total_othertableentrynegative * S ((S (dst_index_table_total_othertable)) * dst_negative_scale_table_total_othertable) + (dst_negative_table_total_othertable))) /\ (exists ge_balance_positive_table_total_othertableentryvalue ge_balance_negative_table_total_othertableentryvalue. (((((dst_value_table_total_othertable) = 2 * (ge_balance_positive_table_total_othertableentryvalue) /\ (ge_balance_negative_table_total_othertableentryvalue) = 0) \/ exists ge_signed_half_table_total_othertableentryvaluedecode. (((dst_value_table_total_othertable) = 2 * ge_signed_half_table_total_othertableentryvaluedecode + 1 /\ (ge_balance_positive_table_total_othertableentryvalue) = 0) /\ (ge_balance_negative_table_total_othertableentryvalue) = S ge_signed_half_table_total_othertableentryvaluedecode))) /\ ((dst_positive_table_total_othertable) + ge_balance_negative_table_total_othertableentryvalue = (dst_negative_table_total_othertable) + ge_balance_positive_table_total_othertableentryvalue))))))))) /\ (forall dc_input_table_total_other dc_output_table_total_other. ~(dc_input_table_total_other=0) -> (exists pvs_le_gap_table_total_otherdomain. pvs_le_gap_table_total_otherdomain + (dc_input_table_total_other) = (N)) -> (exists dst_positive_code_table_total_otherlookup dst_positive_scale_table_total_otherlookup dst_negative_code_table_total_otherlookup dst_negative_scale_table_total_otherlookup dst_positive_table_total_otherlookup dst_negative_table_total_otherlookup. (((K) = (((((dst_positive_code_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup)) * S ((dst_positive_code_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup)) + ((dst_positive_scale_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup))) + (((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) * S ((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) + ((dst_negative_scale_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)))) * S ((((dst_positive_code_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup)) * S ((dst_positive_code_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup)) + ((dst_positive_scale_table_total_otherlookup) + (dst_positive_scale_table_total_otherlookup))) + (((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) * S ((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) + ((dst_negative_scale_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)))) + ((((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) * S ((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) + ((dst_negative_scale_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup))) + (((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) * S ((dst_negative_code_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)) + ((dst_negative_scale_table_total_otherlookup) + (dst_negative_scale_table_total_otherlookup)))))) /\ (((((exists ff_h_pvs_table_total_otherlookuppositive. ff_h_pvs_table_total_otherlookuppositive + S (dst_positive_table_total_otherlookup) = S ((S (dc_input_table_total_other)) * dst_positive_scale_table_total_otherlookup)) /\ exists ff_q_pvs_table_total_otherlookuppositive. dst_positive_code_table_total_otherlookup = ff_q_pvs_table_total_otherlookuppositive * S ((S (dc_input_table_total_other)) * dst_positive_scale_table_total_otherlookup) + (dst_positive_table_total_otherlookup))) /\ (((((exists ff_h_pvs_table_total_otherlookupnegative. ff_h_pvs_table_total_otherlookupnegative + S (dst_negative_table_total_otherlookup) = S ((S (dc_input_table_total_other)) * dst_negative_scale_table_total_otherlookup)) /\ exists ff_q_pvs_table_total_otherlookupnegative. dst_negative_code_table_total_otherlookup = ff_q_pvs_table_total_otherlookupnegative * S ((S (dc_input_table_total_other)) * dst_negative_scale_table_total_otherlookup) + (dst_negative_table_total_otherlookup))) /\ (exists ge_balance_positive_table_total_otherlookupvalue ge_balance_negative_table_total_otherlookupvalue. (((((dc_output_table_total_other) = 2 * (ge_balance_positive_table_total_otherlookupvalue) /\ (ge_balance_negative_table_total_otherlookupvalue) = 0) \/ exists ge_signed_half_table_total_otherlookupvaluedecode. (((dc_output_table_total_other) = 2 * ge_signed_half_table_total_otherlookupvaluedecode + 1 /\ (ge_balance_positive_table_total_otherlookupvalue) = 0) /\ (ge_balance_negative_table_total_otherlookupvalue) = S ge_signed_half_table_total_otherlookupvaluedecode))) /\ ((dst_positive_table_total_otherlookup) + ge_balance_negative_table_total_otherlookupvalue = (dst_negative_table_total_otherlookup) + ge_balance_positive_table_total_otherlookupvalue))))))))) -> (((~((dc_input_table_total_other)=0)) /\ (exists dc_mask_table_total_othervalue. ((((exists dst_positive_code_table_total_othervaluemasktable dst_positive_scale_table_total_othervaluemasktable dst_negative_code_table_total_othervaluemasktable dst_negative_scale_table_total_othervaluemasktable. (((dc_mask_table_total_othervalue) = (((((dst_positive_code_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable)) * S ((dst_positive_code_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable)) + ((dst_positive_scale_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable))) + (((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) * S ((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) + ((dst_negative_scale_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)))) * S ((((dst_positive_code_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable)) * S ((dst_positive_code_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable)) + ((dst_positive_scale_table_total_othervaluemasktable) + (dst_positive_scale_table_total_othervaluemasktable))) + (((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) * S ((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) + ((dst_negative_scale_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)))) + ((((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) * S ((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) + ((dst_negative_scale_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable))) + (((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) * S ((dst_negative_code_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)) + ((dst_negative_scale_table_total_othervaluemasktable) + (dst_negative_scale_table_total_othervaluemasktable)))))) /\ (forall dst_index_table_total_othervaluemasktable. (exists pvs_le_gap_table_total_othervaluemasktabledomain. pvs_le_gap_table_total_othervaluemasktabledomain + (dst_index_table_total_othervaluemasktable) = (dc_input_table_total_other)) -> exists dst_positive_table_total_othervaluemasktable dst_negative_table_total_othervaluemasktable dst_value_table_total_othervaluemasktable. ((((exists ff_h_pvs_table_total_othervaluemasktableentrypositive. ff_h_pvs_table_total_othervaluemasktableentrypositive + S (dst_positive_table_total_othervaluemasktable) = S ((S (dst_index_table_total_othervaluemasktable)) * dst_positive_scale_table_total_othervaluemasktable)) /\ exists ff_q_pvs_table_total_othervaluemasktableentrypositive. dst_positive_code_table_total_othervaluemasktable = ff_q_pvs_table_total_othervaluemasktableentrypositive * S ((S (dst_index_table_total_othervaluemasktable)) * dst_positive_scale_table_total_othervaluemasktable) + (dst_positive_table_total_othervaluemasktable))) /\ (((((exists ff_h_pvs_table_total_othervaluemasktableentrynegative. ff_h_pvs_table_total_othervaluemasktableentrynegative + S (dst_negative_table_total_othervaluemasktable) = S ((S (dst_index_table_total_othervaluemasktable)) * dst_negative_scale_table_total_othervaluemasktable)) /\ exists ff_q_pvs_table_total_othervaluemasktableentrynegative. dst_negative_code_table_total_othervaluemasktable = ff_q_pvs_table_total_othervaluemasktableentrynegative * S ((S (dst_index_table_total_othervaluemasktable)) * dst_negative_scale_table_total_othervaluemasktable) + (dst_negative_table_total_othervaluemasktable))) /\ (exists ge_balance_positive_table_total_othervaluemasktableentryvalue ge_balance_negative_table_total_othervaluemasktableentryvalue. (((((dst_value_table_total_othervaluemasktable) = 2 * (ge_balance_positive_table_total_othervaluemasktableentryvalue) /\ (ge_balance_negative_table_total_othervaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_total_othervaluemasktableentryvaluedecode. (((dst_value_table_total_othervaluemasktable) = 2 * ge_signed_half_table_total_othervaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_total_othervaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_total_othervaluemasktableentryvalue) = S ge_signed_half_table_total_othervaluemasktableentryvaluedecode))) /\ ((dst_positive_table_total_othervaluemasktable) + ge_balance_negative_table_total_othervaluemasktableentryvalue = (dst_negative_table_total_othervaluemasktable) + ge_balance_positive_table_total_othervaluemasktableentryvalue))))))))) /\ (forall dc_index_table_total_othervaluemask dc_value_table_total_othervaluemask. (exists pvs_le_gap_table_total_othervaluemaskdomain. pvs_le_gap_table_total_othervaluemaskdomain + (dc_index_table_total_othervaluemask) = (dc_input_table_total_other)) -> (exists dst_positive_code_table_total_othervaluemasklookup dst_positive_scale_table_total_othervaluemasklookup dst_negative_code_table_total_othervaluemasklookup dst_negative_scale_table_total_othervaluemasklookup dst_positive_table_total_othervaluemasklookup dst_negative_table_total_othervaluemasklookup. (((dc_mask_table_total_othervalue) = (((((dst_positive_code_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup)) * S ((dst_positive_code_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup)) + ((dst_positive_scale_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup))) + (((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) * S ((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) + ((dst_negative_scale_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)))) * S ((((dst_positive_code_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup)) * S ((dst_positive_code_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup)) + ((dst_positive_scale_table_total_othervaluemasklookup) + (dst_positive_scale_table_total_othervaluemasklookup))) + (((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) * S ((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) + ((dst_negative_scale_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)))) + ((((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) * S ((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) + ((dst_negative_scale_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup))) + (((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) * S ((dst_negative_code_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)) + ((dst_negative_scale_table_total_othervaluemasklookup) + (dst_negative_scale_table_total_othervaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_total_othervaluemasklookuppositive. ff_h_pvs_table_total_othervaluemasklookuppositive + S (dst_positive_table_total_othervaluemasklookup) = S ((S (dc_index_table_total_othervaluemask)) * dst_positive_scale_table_total_othervaluemasklookup)) /\ exists ff_q_pvs_table_total_othervaluemasklookuppositive. dst_positive_code_table_total_othervaluemasklookup = ff_q_pvs_table_total_othervaluemasklookuppositive * S ((S (dc_index_table_total_othervaluemask)) * dst_positive_scale_table_total_othervaluemasklookup) + (dst_positive_table_total_othervaluemasklookup))) /\ (((((exists ff_h_pvs_table_total_othervaluemasklookupnegative. ff_h_pvs_table_total_othervaluemasklookupnegative + S (dst_negative_table_total_othervaluemasklookup) = S ((S (dc_index_table_total_othervaluemask)) * dst_negative_scale_table_total_othervaluemasklookup)) /\ exists ff_q_pvs_table_total_othervaluemasklookupnegative. dst_negative_code_table_total_othervaluemasklookup = ff_q_pvs_table_total_othervaluemasklookupnegative * S ((S (dc_index_table_total_othervaluemask)) * dst_negative_scale_table_total_othervaluemasklookup) + (dst_negative_table_total_othervaluemasklookup))) /\ (exists ge_balance_positive_table_total_othervaluemasklookupvalue ge_balance_negative_table_total_othervaluemasklookupvalue. (((((dc_value_table_total_othervaluemask) = 2 * (ge_balance_positive_table_total_othervaluemasklookupvalue) /\ (ge_balance_negative_table_total_othervaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_total_othervaluemasklookupvaluedecode. (((dc_value_table_total_othervaluemask) = 2 * ge_signed_half_table_total_othervaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_total_othervaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_total_othervaluemasklookupvalue) = S ge_signed_half_table_total_othervaluemasklookupvaluedecode))) /\ ((dst_positive_table_total_othervaluemasklookup) + ge_balance_negative_table_total_othervaluemasklookupvalue = (dst_negative_table_total_othervaluemasklookup) + ge_balance_positive_table_total_othervaluemasklookupvalue))))))))) -> ((((~((dc_index_table_total_othervaluemask)=0)) /\ (exists dc_quotient_table_total_othervaluemaskentry dc_left_table_total_othervaluemaskentry dc_right_table_total_othervaluemaskentry. (((dc_input_table_total_other)=(dc_index_table_total_othervaluemask)*dc_quotient_table_total_othervaluemaskentry) /\ (((exists dst_positive_code_table_total_othervaluemaskentryleft dst_positive_scale_table_total_othervaluemaskentryleft dst_negative_code_table_total_othervaluemaskentryleft dst_negative_scale_table_total_othervaluemaskentryleft dst_positive_table_total_othervaluemaskentryleft dst_negative_table_total_othervaluemaskentryleft. (((F) = (((((dst_positive_code_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft)) * S ((dst_positive_code_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft)) + ((dst_positive_scale_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft))) + (((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) * S ((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) + ((dst_negative_scale_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)))) * S ((((dst_positive_code_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft)) * S ((dst_positive_code_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft)) + ((dst_positive_scale_table_total_othervaluemaskentryleft) + (dst_positive_scale_table_total_othervaluemaskentryleft))) + (((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) * S ((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) + ((dst_negative_scale_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)))) + ((((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) * S ((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) + ((dst_negative_scale_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft))) + (((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) * S ((dst_negative_code_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)) + ((dst_negative_scale_table_total_othervaluemaskentryleft) + (dst_negative_scale_table_total_othervaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_total_othervaluemaskentryleftpositive. ff_h_pvs_table_total_othervaluemaskentryleftpositive + S (dst_positive_table_total_othervaluemaskentryleft) = S ((S (dc_index_table_total_othervaluemask)) * dst_positive_scale_table_total_othervaluemaskentryleft)) /\ exists ff_q_pvs_table_total_othervaluemaskentryleftpositive. dst_positive_code_table_total_othervaluemaskentryleft = ff_q_pvs_table_total_othervaluemaskentryleftpositive * S ((S (dc_index_table_total_othervaluemask)) * dst_positive_scale_table_total_othervaluemaskentryleft) + (dst_positive_table_total_othervaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_total_othervaluemaskentryleftnegative. ff_h_pvs_table_total_othervaluemaskentryleftnegative + S (dst_negative_table_total_othervaluemaskentryleft) = S ((S (dc_index_table_total_othervaluemask)) * dst_negative_scale_table_total_othervaluemaskentryleft)) /\ exists ff_q_pvs_table_total_othervaluemaskentryleftnegative. dst_negative_code_table_total_othervaluemaskentryleft = ff_q_pvs_table_total_othervaluemaskentryleftnegative * S ((S (dc_index_table_total_othervaluemask)) * dst_negative_scale_table_total_othervaluemaskentryleft) + (dst_negative_table_total_othervaluemaskentryleft))) /\ (exists ge_balance_positive_table_total_othervaluemaskentryleftvalue ge_balance_negative_table_total_othervaluemaskentryleftvalue. (((((dc_left_table_total_othervaluemaskentry) = 2 * (ge_balance_positive_table_total_othervaluemaskentryleftvalue) /\ (ge_balance_negative_table_total_othervaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_total_othervaluemaskentryleftvaluedecode. (((dc_left_table_total_othervaluemaskentry) = 2 * ge_signed_half_table_total_othervaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_total_othervaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_total_othervaluemaskentryleftvalue) = S ge_signed_half_table_total_othervaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_total_othervaluemaskentryleft) + ge_balance_negative_table_total_othervaluemaskentryleftvalue = (dst_negative_table_total_othervaluemaskentryleft) + ge_balance_positive_table_total_othervaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_total_othervaluemaskentryright dst_positive_scale_table_total_othervaluemaskentryright dst_negative_code_table_total_othervaluemaskentryright dst_negative_scale_table_total_othervaluemaskentryright dst_positive_table_total_othervaluemaskentryright dst_negative_table_total_othervaluemaskentryright. (((G) = (((((dst_positive_code_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright)) * S ((dst_positive_code_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright)) + ((dst_positive_scale_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright))) + (((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) * S ((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) + ((dst_negative_scale_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)))) * S ((((dst_positive_code_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright)) * S ((dst_positive_code_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright)) + ((dst_positive_scale_table_total_othervaluemaskentryright) + (dst_positive_scale_table_total_othervaluemaskentryright))) + (((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) * S ((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) + ((dst_negative_scale_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)))) + ((((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) * S ((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) + ((dst_negative_scale_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright))) + (((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) * S ((dst_negative_code_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)) + ((dst_negative_scale_table_total_othervaluemaskentryright) + (dst_negative_scale_table_total_othervaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_total_othervaluemaskentryrightpositive. ff_h_pvs_table_total_othervaluemaskentryrightpositive + S (dst_positive_table_total_othervaluemaskentryright) = S ((S (dc_quotient_table_total_othervaluemaskentry)) * dst_positive_scale_table_total_othervaluemaskentryright)) /\ exists ff_q_pvs_table_total_othervaluemaskentryrightpositive. dst_positive_code_table_total_othervaluemaskentryright = ff_q_pvs_table_total_othervaluemaskentryrightpositive * S ((S (dc_quotient_table_total_othervaluemaskentry)) * dst_positive_scale_table_total_othervaluemaskentryright) + (dst_positive_table_total_othervaluemaskentryright))) /\ (((((exists ff_h_pvs_table_total_othervaluemaskentryrightnegative. ff_h_pvs_table_total_othervaluemaskentryrightnegative + S (dst_negative_table_total_othervaluemaskentryright) = S ((S (dc_quotient_table_total_othervaluemaskentry)) * dst_negative_scale_table_total_othervaluemaskentryright)) /\ exists ff_q_pvs_table_total_othervaluemaskentryrightnegative. dst_negative_code_table_total_othervaluemaskentryright = ff_q_pvs_table_total_othervaluemaskentryrightnegative * S ((S (dc_quotient_table_total_othervaluemaskentry)) * dst_negative_scale_table_total_othervaluemaskentryright) + (dst_negative_table_total_othervaluemaskentryright))) /\ (exists ge_balance_positive_table_total_othervaluemaskentryrightvalue ge_balance_negative_table_total_othervaluemaskentryrightvalue. (((((dc_right_table_total_othervaluemaskentry) = 2 * (ge_balance_positive_table_total_othervaluemaskentryrightvalue) /\ (ge_balance_negative_table_total_othervaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_total_othervaluemaskentryrightvaluedecode. (((dc_right_table_total_othervaluemaskentry) = 2 * ge_signed_half_table_total_othervaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_total_othervaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_total_othervaluemaskentryrightvalue) = S ge_signed_half_table_total_othervaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_total_othervaluemaskentryright) + ge_balance_negative_table_total_othervaluemaskentryrightvalue = (dst_negative_table_total_othervaluemaskentryright) + ge_balance_positive_table_total_othervaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_total_othervaluemaskentryproduct sto_an_table_total_othervaluemaskentryproduct sto_bp_table_total_othervaluemaskentryproduct sto_bn_table_total_othervaluemaskentryproduct sto_cp_table_total_othervaluemaskentryproduct sto_cn_table_total_othervaluemaskentryproduct. (((((dc_left_table_total_othervaluemaskentry) = 2 * (sto_ap_table_total_othervaluemaskentryproduct) /\ (sto_an_table_total_othervaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_othervaluemaskentryproductleft. (((dc_left_table_total_othervaluemaskentry) = 2 * ge_signed_half_table_total_othervaluemaskentryproductleft + 1 /\ (sto_ap_table_total_othervaluemaskentryproduct) = 0) /\ (sto_an_table_total_othervaluemaskentryproduct) = S ge_signed_half_table_total_othervaluemaskentryproductleft))) /\ ((((((dc_right_table_total_othervaluemaskentry) = 2 * (sto_bp_table_total_othervaluemaskentryproduct) /\ (sto_bn_table_total_othervaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_othervaluemaskentryproductright. (((dc_right_table_total_othervaluemaskentry) = 2 * ge_signed_half_table_total_othervaluemaskentryproductright + 1 /\ (sto_bp_table_total_othervaluemaskentryproduct) = 0) /\ (sto_bn_table_total_othervaluemaskentryproduct) = S ge_signed_half_table_total_othervaluemaskentryproductright))) /\ ((((((dc_value_table_total_othervaluemask) = 2 * (sto_cp_table_total_othervaluemaskentryproduct) /\ (sto_cn_table_total_othervaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_total_othervaluemaskentryproductoutput. (((dc_value_table_total_othervaluemask) = 2 * ge_signed_half_table_total_othervaluemaskentryproductoutput + 1 /\ (sto_cp_table_total_othervaluemaskentryproduct) = 0) /\ (sto_cn_table_total_othervaluemaskentryproduct) = S ge_signed_half_table_total_othervaluemaskentryproductoutput))) /\ ((sto_ap_table_total_othervaluemaskentryproduct * sto_bp_table_total_othervaluemaskentryproduct + sto_an_table_total_othervaluemaskentryproduct * sto_bn_table_total_othervaluemaskentryproduct) + sto_cn_table_total_othervaluemaskentryproduct = (sto_ap_table_total_othervaluemaskentryproduct * sto_bn_table_total_othervaluemaskentryproduct + sto_an_table_total_othervaluemaskentryproduct * sto_bp_table_total_othervaluemaskentryproduct) + sto_cp_table_total_othervaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_total_othervaluemask)=0 \/ ~(exists pvs_factor_table_total_othervaluemaskentrynondivisor. (dc_input_table_total_other) = (dc_index_table_total_othervaluemask) * pvs_factor_table_total_othervaluemaskentrynondivisor)) /\ ((dc_value_table_total_othervaluemask)=0))))))) /\ (exists dst_positive_code_table_total_othervaluefold dst_positive_scale_table_total_othervaluefold dst_negative_code_table_total_othervaluefold dst_negative_scale_table_total_othervaluefold dst_positive_sum_table_total_othervaluefold dst_negative_sum_table_total_othervaluefold. (((dc_mask_table_total_othervalue) = (((((dst_positive_code_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold)) * S ((dst_positive_code_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold)) + ((dst_positive_scale_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold))) + (((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) * S ((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) + ((dst_negative_scale_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)))) * S ((((dst_positive_code_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold)) * S ((dst_positive_code_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold)) + ((dst_positive_scale_table_total_othervaluefold) + (dst_positive_scale_table_total_othervaluefold))) + (((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) * S ((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) + ((dst_negative_scale_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)))) + ((((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) * S ((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) + ((dst_negative_scale_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold))) + (((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) * S ((dst_negative_code_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)) + ((dst_negative_scale_table_total_othervaluefold) + (dst_negative_scale_table_total_othervaluefold)))))) /\ (((exists fs_u_dst_table_total_othervaluefoldpositive fs_v_dst_table_total_othervaluefoldpositive. ((((exists fs_h_dst_table_total_othervaluefoldpositive_body_start. fs_h_dst_table_total_othervaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_total_othervaluefoldpositive)) /\ exists fs_q_dst_table_total_othervaluefoldpositive_body_start. fs_u_dst_table_total_othervaluefoldpositive = fs_q_dst_table_total_othervaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_total_othervaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_total_othervaluefoldpositive_body_terminal. fs_h_dst_table_total_othervaluefoldpositive_body_terminal + S (dst_positive_sum_table_total_othervaluefold) = S ((S (S (dc_input_table_total_other))) * fs_v_dst_table_total_othervaluefoldpositive)) /\ exists fs_q_dst_table_total_othervaluefoldpositive_body_terminal. fs_u_dst_table_total_othervaluefoldpositive = fs_q_dst_table_total_othervaluefoldpositive_body_terminal * S ((S (S (dc_input_table_total_other))) * fs_v_dst_table_total_othervaluefoldpositive) + (dst_positive_sum_table_total_othervaluefold))) /\ forall fs_i_dst_table_total_othervaluefoldpositive_body_steps. (exists fs_lt_dst_table_total_othervaluefoldpositive_body_steps_bound. fs_lt_dst_table_total_othervaluefoldpositive_body_steps_bound + S fs_i_dst_table_total_othervaluefoldpositive_body_steps = S (dc_input_table_total_other)) -> exists fs_a_dst_table_total_othervaluefoldpositive_body_steps fs_r_dst_table_total_othervaluefoldpositive_body_steps fs_s_dst_table_total_othervaluefoldpositive_body_steps. ((((exists fs_h_dst_table_total_othervaluefoldpositive_body_steps_summand. fs_h_dst_table_total_othervaluefoldpositive_body_steps_summand + S (fs_a_dst_table_total_othervaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * dst_positive_scale_table_total_othervaluefold)) /\ exists fs_q_dst_table_total_othervaluefoldpositive_body_steps_summand. dst_positive_code_table_total_othervaluefold = fs_q_dst_table_total_othervaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * dst_positive_scale_table_total_othervaluefold) + (fs_a_dst_table_total_othervaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_total_othervaluefoldpositive_body_steps_partial. fs_h_dst_table_total_othervaluefoldpositive_body_steps_partial + S (fs_r_dst_table_total_othervaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * fs_v_dst_table_total_othervaluefoldpositive)) /\ exists fs_q_dst_table_total_othervaluefoldpositive_body_steps_partial. fs_u_dst_table_total_othervaluefoldpositive = fs_q_dst_table_total_othervaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * fs_v_dst_table_total_othervaluefoldpositive) + (fs_r_dst_table_total_othervaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_total_othervaluefoldpositive_body_steps_successor. fs_h_dst_table_total_othervaluefoldpositive_body_steps_successor + S (fs_s_dst_table_total_othervaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * fs_v_dst_table_total_othervaluefoldpositive)) /\ exists fs_q_dst_table_total_othervaluefoldpositive_body_steps_successor. fs_u_dst_table_total_othervaluefoldpositive = fs_q_dst_table_total_othervaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_total_othervaluefoldpositive_body_steps)) * fs_v_dst_table_total_othervaluefoldpositive) + (fs_s_dst_table_total_othervaluefoldpositive_body_steps))) /\ fs_s_dst_table_total_othervaluefoldpositive_body_steps = fs_r_dst_table_total_othervaluefoldpositive_body_steps + fs_a_dst_table_total_othervaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_total_othervaluefoldnegative fs_v_dst_table_total_othervaluefoldnegative. ((((exists fs_h_dst_table_total_othervaluefoldnegative_body_start. fs_h_dst_table_total_othervaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_total_othervaluefoldnegative)) /\ exists fs_q_dst_table_total_othervaluefoldnegative_body_start. fs_u_dst_table_total_othervaluefoldnegative = fs_q_dst_table_total_othervaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_total_othervaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_total_othervaluefoldnegative_body_terminal. fs_h_dst_table_total_othervaluefoldnegative_body_terminal + S (dst_negative_sum_table_total_othervaluefold) = S ((S (S (dc_input_table_total_other))) * fs_v_dst_table_total_othervaluefoldnegative)) /\ exists fs_q_dst_table_total_othervaluefoldnegative_body_terminal. fs_u_dst_table_total_othervaluefoldnegative = fs_q_dst_table_total_othervaluefoldnegative_body_terminal * S ((S (S (dc_input_table_total_other))) * fs_v_dst_table_total_othervaluefoldnegative) + (dst_negative_sum_table_total_othervaluefold))) /\ forall fs_i_dst_table_total_othervaluefoldnegative_body_steps. (exists fs_lt_dst_table_total_othervaluefoldnegative_body_steps_bound. fs_lt_dst_table_total_othervaluefoldnegative_body_steps_bound + S fs_i_dst_table_total_othervaluefoldnegative_body_steps = S (dc_input_table_total_other)) -> exists fs_a_dst_table_total_othervaluefoldnegative_body_steps fs_r_dst_table_total_othervaluefoldnegative_body_steps fs_s_dst_table_total_othervaluefoldnegative_body_steps. ((((exists fs_h_dst_table_total_othervaluefoldnegative_body_steps_summand. fs_h_dst_table_total_othervaluefoldnegative_body_steps_summand + S (fs_a_dst_table_total_othervaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * dst_negative_scale_table_total_othervaluefold)) /\ exists fs_q_dst_table_total_othervaluefoldnegative_body_steps_summand. dst_negative_code_table_total_othervaluefold = fs_q_dst_table_total_othervaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * dst_negative_scale_table_total_othervaluefold) + (fs_a_dst_table_total_othervaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_total_othervaluefoldnegative_body_steps_partial. fs_h_dst_table_total_othervaluefoldnegative_body_steps_partial + S (fs_r_dst_table_total_othervaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * fs_v_dst_table_total_othervaluefoldnegative)) /\ exists fs_q_dst_table_total_othervaluefoldnegative_body_steps_partial. fs_u_dst_table_total_othervaluefoldnegative = fs_q_dst_table_total_othervaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * fs_v_dst_table_total_othervaluefoldnegative) + (fs_r_dst_table_total_othervaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_total_othervaluefoldnegative_body_steps_successor. fs_h_dst_table_total_othervaluefoldnegative_body_steps_successor + S (fs_s_dst_table_total_othervaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * fs_v_dst_table_total_othervaluefoldnegative)) /\ exists fs_q_dst_table_total_othervaluefoldnegative_body_steps_successor. fs_u_dst_table_total_othervaluefoldnegative = fs_q_dst_table_total_othervaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_total_othervaluefoldnegative_body_steps)) * fs_v_dst_table_total_othervaluefoldnegative) + (fs_s_dst_table_total_othervaluefoldnegative_body_steps))) /\ fs_s_dst_table_total_othervaluefoldnegative_body_steps = fs_r_dst_table_total_othervaluefoldnegative_body_steps + fs_a_dst_table_total_othervaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_total_othervaluefoldresult ge_balance_negative_table_total_othervaluefoldresult. (((((dc_output_table_total_other) = 2 * (ge_balance_positive_table_total_othervaluefoldresult) /\ (ge_balance_negative_table_total_othervaluefoldresult) = 0) \/ exists ge_signed_half_table_total_othervaluefoldresultdecode. (((dc_output_table_total_other) = 2 * ge_signed_half_table_total_othervaluefoldresultdecode + 1 /\ (ge_balance_positive_table_total_othervaluefoldresult) = 0) /\ (ge_balance_negative_table_total_othervaluefoldresult) = S ge_signed_half_table_total_othervaluefoldresultdecode))) /\ ((dst_positive_sum_table_total_othervaluefold) + ge_balance_negative_table_total_othervaluefoldresult = (dst_negative_sum_table_total_othervaluefold) + ge_balance_positive_table_total_othervaluefoldresult)))))))))))))))))))) -> (forall dm_index_table_total_equal dm_first_value_table_total_equal dm_second_value_table_total_equal. ~(dm_index_table_total_equal=0) -> (exists pvs_le_gap_table_total_equaldomain. pvs_le_gap_table_total_equaldomain + (dm_index_table_total_equal) = (N)) -> (exists dst_positive_code_table_total_equalfirst dst_positive_scale_table_total_equalfirst dst_negative_code_table_total_equalfirst dst_negative_scale_table_total_equalfirst dst_positive_table_total_equalfirst dst_negative_table_total_equalfirst. (((H) = (((((dst_positive_code_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst)) * S ((dst_positive_code_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst)) + ((dst_positive_scale_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst))) + (((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) * S ((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) + ((dst_negative_scale_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)))) * S ((((dst_positive_code_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst)) * S ((dst_positive_code_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst)) + ((dst_positive_scale_table_total_equalfirst) + (dst_positive_scale_table_total_equalfirst))) + (((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) * S ((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) + ((dst_negative_scale_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)))) + ((((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) * S ((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) + ((dst_negative_scale_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst))) + (((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) * S ((dst_negative_code_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)) + ((dst_negative_scale_table_total_equalfirst) + (dst_negative_scale_table_total_equalfirst)))))) /\ (((((exists ff_h_pvs_table_total_equalfirstpositive. ff_h_pvs_table_total_equalfirstpositive + S (dst_positive_table_total_equalfirst) = S ((S (dm_index_table_total_equal)) * dst_positive_scale_table_total_equalfirst)) /\ exists ff_q_pvs_table_total_equalfirstpositive. dst_positive_code_table_total_equalfirst = ff_q_pvs_table_total_equalfirstpositive * S ((S (dm_index_table_total_equal)) * dst_positive_scale_table_total_equalfirst) + (dst_positive_table_total_equalfirst))) /\ (((((exists ff_h_pvs_table_total_equalfirstnegative. ff_h_pvs_table_total_equalfirstnegative + S (dst_negative_table_total_equalfirst) = S ((S (dm_index_table_total_equal)) * dst_negative_scale_table_total_equalfirst)) /\ exists ff_q_pvs_table_total_equalfirstnegative. dst_negative_code_table_total_equalfirst = ff_q_pvs_table_total_equalfirstnegative * S ((S (dm_index_table_total_equal)) * dst_negative_scale_table_total_equalfirst) + (dst_negative_table_total_equalfirst))) /\ (exists ge_balance_positive_table_total_equalfirstvalue ge_balance_negative_table_total_equalfirstvalue. (((((dm_first_value_table_total_equal) = 2 * (ge_balance_positive_table_total_equalfirstvalue) /\ (ge_balance_negative_table_total_equalfirstvalue) = 0) \/ exists ge_signed_half_table_total_equalfirstvaluedecode. (((dm_first_value_table_total_equal) = 2 * ge_signed_half_table_total_equalfirstvaluedecode + 1 /\ (ge_balance_positive_table_total_equalfirstvalue) = 0) /\ (ge_balance_negative_table_total_equalfirstvalue) = S ge_signed_half_table_total_equalfirstvaluedecode))) /\ ((dst_positive_table_total_equalfirst) + ge_balance_negative_table_total_equalfirstvalue = (dst_negative_table_total_equalfirst) + ge_balance_positive_table_total_equalfirstvalue))))))))) -> (exists dst_positive_code_table_total_equalsecond dst_positive_scale_table_total_equalsecond dst_negative_code_table_total_equalsecond dst_negative_scale_table_total_equalsecond dst_positive_table_total_equalsecond dst_negative_table_total_equalsecond. (((K) = (((((dst_positive_code_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond)) * S ((dst_positive_code_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond)) + ((dst_positive_scale_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond))) + (((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) * S ((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) + ((dst_negative_scale_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)))) * S ((((dst_positive_code_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond)) * S ((dst_positive_code_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond)) + ((dst_positive_scale_table_total_equalsecond) + (dst_positive_scale_table_total_equalsecond))) + (((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) * S ((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) + ((dst_negative_scale_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)))) + ((((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) * S ((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) + ((dst_negative_scale_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond))) + (((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) * S ((dst_negative_code_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)) + ((dst_negative_scale_table_total_equalsecond) + (dst_negative_scale_table_total_equalsecond)))))) /\ (((((exists ff_h_pvs_table_total_equalsecondpositive. ff_h_pvs_table_total_equalsecondpositive + S (dst_positive_table_total_equalsecond) = S ((S (dm_index_table_total_equal)) * dst_positive_scale_table_total_equalsecond)) /\ exists ff_q_pvs_table_total_equalsecondpositive. dst_positive_code_table_total_equalsecond = ff_q_pvs_table_total_equalsecondpositive * S ((S (dm_index_table_total_equal)) * dst_positive_scale_table_total_equalsecond) + (dst_positive_table_total_equalsecond))) /\ (((((exists ff_h_pvs_table_total_equalsecondnegative. ff_h_pvs_table_total_equalsecondnegative + S (dst_negative_table_total_equalsecond) = S ((S (dm_index_table_total_equal)) * dst_negative_scale_table_total_equalsecond)) /\ exists ff_q_pvs_table_total_equalsecondnegative. dst_negative_code_table_total_equalsecond = ff_q_pvs_table_total_equalsecondnegative * S ((S (dm_index_table_total_equal)) * dst_negative_scale_table_total_equalsecond) + (dst_negative_table_total_equalsecond))) /\ (exists ge_balance_positive_table_total_equalsecondvalue ge_balance_negative_table_total_equalsecondvalue. (((((dm_second_value_table_total_equal) = 2 * (ge_balance_positive_table_total_equalsecondvalue) /\ (ge_balance_negative_table_total_equalsecondvalue) = 0) \/ exists ge_signed_half_table_total_equalsecondvaluedecode. (((dm_second_value_table_total_equal) = 2 * ge_signed_half_table_total_equalsecondvaluedecode + 1 /\ (ge_balance_positive_table_total_equalsecondvalue) = 0) /\ (ge_balance_negative_table_total_equalsecondvalue) = S ge_signed_half_table_total_equalsecondvaluedecode))) /\ ((dst_positive_table_total_equalsecond) + ge_balance_negative_table_total_equalsecondvalue = (dst_negative_table_total_equalsecond) + ge_balance_positive_table_total_equalsecondvalue))))))))) -> dm_first_value_table_total_equal=dm_second_value_table_total_equal)))Constructive proof overview
Generated structural guide
Construct the entire finite Dirichlet-convolution table and prove positive-window uniqueness, not equality of arbitrary codes or zeroth values.
The unchanged tactic script uses 2 declared prerequisites and contains 26 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–5
02Establish hL6–12
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution table exists.
03Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
cases h
04Construct an explicit witnessL14–14
Supply the displayed value, then prove that it has the required property.
- L14
exists x
05Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
06Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
exact h_witness
07Fix variables and assumptionsL17–18
08Use earlier factsL19–26
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
specialize dirichlet_convolution_table_extensional (N) - L20
specialize dirichlet_convolution_table_extensional (F) - L21
specialize dirichlet_convolution_table_extensional (G) - L22
specialize dirichlet_convolution_table_extensional (x) - L23
specialize dirichlet_convolution_table_extensional (K) - L24
apply dirichlet_convolution_table_extensional - L25
exact h_witness - L26
exact hK
Original exact command ledger · 26 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hF - 0005
intro hG - 0006
have h : exists H. (((exists dst_positive_code_table_unique_constructleft dst_positive_scale_table_unique_constructleft dst_negative_code_table_unique_constructleft dst_negative_scale_table_unique_constructleft. (((F) = (((((dst_positive_code_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft)) * S ((dst_positive_code_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft)) + ((dst_positive_scale_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft))) + (((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) * S ((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) + ((dst_negative_scale_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)))) * S ((((dst_positive_code_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft)) * S ((dst_positive_code_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft)) + ((dst_positive_scale_table_unique_constructleft) + (dst_positive_scale_table_unique_constructleft))) + (((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) * S ((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) + ((dst_negative_scale_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)))) + ((((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) * S ((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) + ((dst_negative_scale_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft))) + (((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) * S ((dst_negative_code_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)) + ((dst_negative_scale_table_unique_constructleft) + (dst_negative_scale_table_unique_constructleft)))))) /\ (forall dst_index_table_unique_constructleft. (exists pvs_le_gap_table_unique_constructleftdomain. pvs_le_gap_table_unique_constructleftdomain + (dst_index_table_unique_constructleft) = (N)) -> exists dst_positive_table_unique_constructleft dst_negative_table_unique_constructleft dst_value_table_unique_constructleft. ((((exists ff_h_pvs_table_unique_constructleftentrypositive. ff_h_pvs_table_unique_constructleftentrypositive + S (dst_positive_table_unique_constructleft) = S ((S (dst_index_table_unique_constructleft)) * dst_positive_scale_table_unique_constructleft)) /\ exists ff_q_pvs_table_unique_constructleftentrypositive. dst_positive_code_table_unique_constructleft = ff_q_pvs_table_unique_constructleftentrypositive * S ((S (dst_index_table_unique_constructleft)) * dst_positive_scale_table_unique_constructleft) + (dst_positive_table_unique_constructleft))) /\ (((((exists ff_h_pvs_table_unique_constructleftentrynegative. ff_h_pvs_table_unique_constructleftentrynegative + S (dst_negative_table_unique_constructleft) = S ((S (dst_index_table_unique_constructleft)) * dst_negative_scale_table_unique_constructleft)) /\ exists ff_q_pvs_table_unique_constructleftentrynegative. dst_negative_code_table_unique_constructleft = ff_q_pvs_table_unique_constructleftentrynegative * S ((S (dst_index_table_unique_constructleft)) * dst_negative_scale_table_unique_constructleft) + (dst_negative_table_unique_constructleft))) /\ (exists ge_balance_positive_table_unique_constructleftentryvalue ge_balance_negative_table_unique_constructleftentryvalue. (((((dst_value_table_unique_constructleft) = 2 * (ge_balance_positive_table_unique_constructleftentryvalue) /\ (ge_balance_negative_table_unique_constructleftentryvalue) = 0) \/ exists ge_signed_half_table_unique_constructleftentryvaluedecode. (((dst_value_table_unique_constructleft) = 2 * ge_signed_half_table_unique_constructleftentryvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructleftentryvalue) = 0) /\ (ge_balance_negative_table_unique_constructleftentryvalue) = S ge_signed_half_table_unique_constructleftentryvaluedecode))) /\ ((dst_positive_table_unique_constructleft) + ge_balance_negative_table_unique_constructleftentryvalue = (dst_negative_table_unique_constructleft) + ge_balance_positive_table_unique_constructleftentryvalue))))))))) /\ (((exists dst_positive_code_table_unique_constructright dst_positive_scale_table_unique_constructright dst_negative_code_table_unique_constructright dst_negative_scale_table_unique_constructright. (((G) = (((((dst_positive_code_table_unique_constructright) + (dst_positive_scale_table_unique_constructright)) * S ((dst_positive_code_table_unique_constructright) + (dst_positive_scale_table_unique_constructright)) + ((dst_positive_scale_table_unique_constructright) + (dst_positive_scale_table_unique_constructright))) + (((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) * S ((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) + ((dst_negative_scale_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)))) * S ((((dst_positive_code_table_unique_constructright) + (dst_positive_scale_table_unique_constructright)) * S ((dst_positive_code_table_unique_constructright) + (dst_positive_scale_table_unique_constructright)) + ((dst_positive_scale_table_unique_constructright) + (dst_positive_scale_table_unique_constructright))) + (((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) * S ((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) + ((dst_negative_scale_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)))) + ((((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) * S ((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) + ((dst_negative_scale_table_unique_constructright) + (dst_negative_scale_table_unique_constructright))) + (((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) * S ((dst_negative_code_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)) + ((dst_negative_scale_table_unique_constructright) + (dst_negative_scale_table_unique_constructright)))))) /\ (forall dst_index_table_unique_constructright. (exists pvs_le_gap_table_unique_constructrightdomain. pvs_le_gap_table_unique_constructrightdomain + (dst_index_table_unique_constructright) = (N)) -> exists dst_positive_table_unique_constructright dst_negative_table_unique_constructright dst_value_table_unique_constructright. ((((exists ff_h_pvs_table_unique_constructrightentrypositive. ff_h_pvs_table_unique_constructrightentrypositive + S (dst_positive_table_unique_constructright) = S ((S (dst_index_table_unique_constructright)) * dst_positive_scale_table_unique_constructright)) /\ exists ff_q_pvs_table_unique_constructrightentrypositive. dst_positive_code_table_unique_constructright = ff_q_pvs_table_unique_constructrightentrypositive * S ((S (dst_index_table_unique_constructright)) * dst_positive_scale_table_unique_constructright) + (dst_positive_table_unique_constructright))) /\ (((((exists ff_h_pvs_table_unique_constructrightentrynegative. ff_h_pvs_table_unique_constructrightentrynegative + S (dst_negative_table_unique_constructright) = S ((S (dst_index_table_unique_constructright)) * dst_negative_scale_table_unique_constructright)) /\ exists ff_q_pvs_table_unique_constructrightentrynegative. dst_negative_code_table_unique_constructright = ff_q_pvs_table_unique_constructrightentrynegative * S ((S (dst_index_table_unique_constructright)) * dst_negative_scale_table_unique_constructright) + (dst_negative_table_unique_constructright))) /\ (exists ge_balance_positive_table_unique_constructrightentryvalue ge_balance_negative_table_unique_constructrightentryvalue. (((((dst_value_table_unique_constructright) = 2 * (ge_balance_positive_table_unique_constructrightentryvalue) /\ (ge_balance_negative_table_unique_constructrightentryvalue) = 0) \/ exists ge_signed_half_table_unique_constructrightentryvaluedecode. (((dst_value_table_unique_constructright) = 2 * ge_signed_half_table_unique_constructrightentryvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructrightentryvalue) = 0) /\ (ge_balance_negative_table_unique_constructrightentryvalue) = S ge_signed_half_table_unique_constructrightentryvaluedecode))) /\ ((dst_positive_table_unique_constructright) + ge_balance_negative_table_unique_constructrightentryvalue = (dst_negative_table_unique_constructright) + ge_balance_positive_table_unique_constructrightentryvalue))))))))) /\ (((exists dst_positive_code_table_unique_constructtable dst_positive_scale_table_unique_constructtable dst_negative_code_table_unique_constructtable dst_negative_scale_table_unique_constructtable. (((H) = (((((dst_positive_code_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable)) * S ((dst_positive_code_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable)) + ((dst_positive_scale_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable))) + (((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) * S ((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) + ((dst_negative_scale_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)))) * S ((((dst_positive_code_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable)) * S ((dst_positive_code_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable)) + ((dst_positive_scale_table_unique_constructtable) + (dst_positive_scale_table_unique_constructtable))) + (((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) * S ((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) + ((dst_negative_scale_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)))) + ((((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) * S ((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) + ((dst_negative_scale_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable))) + (((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) * S ((dst_negative_code_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)) + ((dst_negative_scale_table_unique_constructtable) + (dst_negative_scale_table_unique_constructtable)))))) /\ (forall dst_index_table_unique_constructtable. (exists pvs_le_gap_table_unique_constructtabledomain. pvs_le_gap_table_unique_constructtabledomain + (dst_index_table_unique_constructtable) = (N)) -> exists dst_positive_table_unique_constructtable dst_negative_table_unique_constructtable dst_value_table_unique_constructtable. ((((exists ff_h_pvs_table_unique_constructtableentrypositive. ff_h_pvs_table_unique_constructtableentrypositive + S (dst_positive_table_unique_constructtable) = S ((S (dst_index_table_unique_constructtable)) * dst_positive_scale_table_unique_constructtable)) /\ exists ff_q_pvs_table_unique_constructtableentrypositive. dst_positive_code_table_unique_constructtable = ff_q_pvs_table_unique_constructtableentrypositive * S ((S (dst_index_table_unique_constructtable)) * dst_positive_scale_table_unique_constructtable) + (dst_positive_table_unique_constructtable))) /\ (((((exists ff_h_pvs_table_unique_constructtableentrynegative. ff_h_pvs_table_unique_constructtableentrynegative + S (dst_negative_table_unique_constructtable) = S ((S (dst_index_table_unique_constructtable)) * dst_negative_scale_table_unique_constructtable)) /\ exists ff_q_pvs_table_unique_constructtableentrynegative. dst_negative_code_table_unique_constructtable = ff_q_pvs_table_unique_constructtableentrynegative * S ((S (dst_index_table_unique_constructtable)) * dst_negative_scale_table_unique_constructtable) + (dst_negative_table_unique_constructtable))) /\ (exists ge_balance_positive_table_unique_constructtableentryvalue ge_balance_negative_table_unique_constructtableentryvalue. (((((dst_value_table_unique_constructtable) = 2 * (ge_balance_positive_table_unique_constructtableentryvalue) /\ (ge_balance_negative_table_unique_constructtableentryvalue) = 0) \/ exists ge_signed_half_table_unique_constructtableentryvaluedecode. (((dst_value_table_unique_constructtable) = 2 * ge_signed_half_table_unique_constructtableentryvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructtableentryvalue) = 0) /\ (ge_balance_negative_table_unique_constructtableentryvalue) = S ge_signed_half_table_unique_constructtableentryvaluedecode))) /\ ((dst_positive_table_unique_constructtable) + ge_balance_negative_table_unique_constructtableentryvalue = (dst_negative_table_unique_constructtable) + ge_balance_positive_table_unique_constructtableentryvalue))))))))) /\ (forall dc_input_table_unique_construct dc_output_table_unique_construct. ~(dc_input_table_unique_construct=0) -> (exists pvs_le_gap_table_unique_constructdomain. pvs_le_gap_table_unique_constructdomain + (dc_input_table_unique_construct) = (N)) -> (exists dst_positive_code_table_unique_constructlookup dst_positive_scale_table_unique_constructlookup dst_negative_code_table_unique_constructlookup dst_negative_scale_table_unique_constructlookup dst_positive_table_unique_constructlookup dst_negative_table_unique_constructlookup. (((H) = (((((dst_positive_code_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup)) * S ((dst_positive_code_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup)) + ((dst_positive_scale_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup))) + (((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) * S ((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) + ((dst_negative_scale_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)))) * S ((((dst_positive_code_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup)) * S ((dst_positive_code_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup)) + ((dst_positive_scale_table_unique_constructlookup) + (dst_positive_scale_table_unique_constructlookup))) + (((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) * S ((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) + ((dst_negative_scale_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)))) + ((((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) * S ((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) + ((dst_negative_scale_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup))) + (((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) * S ((dst_negative_code_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)) + ((dst_negative_scale_table_unique_constructlookup) + (dst_negative_scale_table_unique_constructlookup)))))) /\ (((((exists ff_h_pvs_table_unique_constructlookuppositive. ff_h_pvs_table_unique_constructlookuppositive + S (dst_positive_table_unique_constructlookup) = S ((S (dc_input_table_unique_construct)) * dst_positive_scale_table_unique_constructlookup)) /\ exists ff_q_pvs_table_unique_constructlookuppositive. dst_positive_code_table_unique_constructlookup = ff_q_pvs_table_unique_constructlookuppositive * S ((S (dc_input_table_unique_construct)) * dst_positive_scale_table_unique_constructlookup) + (dst_positive_table_unique_constructlookup))) /\ (((((exists ff_h_pvs_table_unique_constructlookupnegative. ff_h_pvs_table_unique_constructlookupnegative + S (dst_negative_table_unique_constructlookup) = S ((S (dc_input_table_unique_construct)) * dst_negative_scale_table_unique_constructlookup)) /\ exists ff_q_pvs_table_unique_constructlookupnegative. dst_negative_code_table_unique_constructlookup = ff_q_pvs_table_unique_constructlookupnegative * S ((S (dc_input_table_unique_construct)) * dst_negative_scale_table_unique_constructlookup) + (dst_negative_table_unique_constructlookup))) /\ (exists ge_balance_positive_table_unique_constructlookupvalue ge_balance_negative_table_unique_constructlookupvalue. (((((dc_output_table_unique_construct) = 2 * (ge_balance_positive_table_unique_constructlookupvalue) /\ (ge_balance_negative_table_unique_constructlookupvalue) = 0) \/ exists ge_signed_half_table_unique_constructlookupvaluedecode. (((dc_output_table_unique_construct) = 2 * ge_signed_half_table_unique_constructlookupvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructlookupvalue) = 0) /\ (ge_balance_negative_table_unique_constructlookupvalue) = S ge_signed_half_table_unique_constructlookupvaluedecode))) /\ ((dst_positive_table_unique_constructlookup) + ge_balance_negative_table_unique_constructlookupvalue = (dst_negative_table_unique_constructlookup) + ge_balance_positive_table_unique_constructlookupvalue))))))))) -> (((~((dc_input_table_unique_construct)=0)) /\ (exists dc_mask_table_unique_constructvalue. ((((exists dst_positive_code_table_unique_constructvaluemasktable dst_positive_scale_table_unique_constructvaluemasktable dst_negative_code_table_unique_constructvaluemasktable dst_negative_scale_table_unique_constructvaluemasktable. (((dc_mask_table_unique_constructvalue) = (((((dst_positive_code_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable)) * S ((dst_positive_code_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable)) + ((dst_positive_scale_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable))) + (((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) * S ((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) + ((dst_negative_scale_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)))) * S ((((dst_positive_code_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable)) * S ((dst_positive_code_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable)) + ((dst_positive_scale_table_unique_constructvaluemasktable) + (dst_positive_scale_table_unique_constructvaluemasktable))) + (((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) * S ((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) + ((dst_negative_scale_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)))) + ((((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) * S ((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) + ((dst_negative_scale_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable))) + (((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) * S ((dst_negative_code_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)) + ((dst_negative_scale_table_unique_constructvaluemasktable) + (dst_negative_scale_table_unique_constructvaluemasktable)))))) /\ (forall dst_index_table_unique_constructvaluemasktable. (exists pvs_le_gap_table_unique_constructvaluemasktabledomain. pvs_le_gap_table_unique_constructvaluemasktabledomain + (dst_index_table_unique_constructvaluemasktable) = (dc_input_table_unique_construct)) -> exists dst_positive_table_unique_constructvaluemasktable dst_negative_table_unique_constructvaluemasktable dst_value_table_unique_constructvaluemasktable. ((((exists ff_h_pvs_table_unique_constructvaluemasktableentrypositive. ff_h_pvs_table_unique_constructvaluemasktableentrypositive + S (dst_positive_table_unique_constructvaluemasktable) = S ((S (dst_index_table_unique_constructvaluemasktable)) * dst_positive_scale_table_unique_constructvaluemasktable)) /\ exists ff_q_pvs_table_unique_constructvaluemasktableentrypositive. dst_positive_code_table_unique_constructvaluemasktable = ff_q_pvs_table_unique_constructvaluemasktableentrypositive * S ((S (dst_index_table_unique_constructvaluemasktable)) * dst_positive_scale_table_unique_constructvaluemasktable) + (dst_positive_table_unique_constructvaluemasktable))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemasktableentrynegative. ff_h_pvs_table_unique_constructvaluemasktableentrynegative + S (dst_negative_table_unique_constructvaluemasktable) = S ((S (dst_index_table_unique_constructvaluemasktable)) * dst_negative_scale_table_unique_constructvaluemasktable)) /\ exists ff_q_pvs_table_unique_constructvaluemasktableentrynegative. dst_negative_code_table_unique_constructvaluemasktable = ff_q_pvs_table_unique_constructvaluemasktableentrynegative * S ((S (dst_index_table_unique_constructvaluemasktable)) * dst_negative_scale_table_unique_constructvaluemasktable) + (dst_negative_table_unique_constructvaluemasktable))) /\ (exists ge_balance_positive_table_unique_constructvaluemasktableentryvalue ge_balance_negative_table_unique_constructvaluemasktableentryvalue. (((((dst_value_table_unique_constructvaluemasktable) = 2 * (ge_balance_positive_table_unique_constructvaluemasktableentryvalue) /\ (ge_balance_negative_table_unique_constructvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_unique_constructvaluemasktableentryvaluedecode. (((dst_value_table_unique_constructvaluemasktable) = 2 * ge_signed_half_table_unique_constructvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_unique_constructvaluemasktableentryvalue) = S ge_signed_half_table_unique_constructvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_unique_constructvaluemasktable) + ge_balance_negative_table_unique_constructvaluemasktableentryvalue = (dst_negative_table_unique_constructvaluemasktable) + ge_balance_positive_table_unique_constructvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_unique_constructvaluemask dc_value_table_unique_constructvaluemask. (exists pvs_le_gap_table_unique_constructvaluemaskdomain. pvs_le_gap_table_unique_constructvaluemaskdomain + (dc_index_table_unique_constructvaluemask) = (dc_input_table_unique_construct)) -> (exists dst_positive_code_table_unique_constructvaluemasklookup dst_positive_scale_table_unique_constructvaluemasklookup dst_negative_code_table_unique_constructvaluemasklookup dst_negative_scale_table_unique_constructvaluemasklookup dst_positive_table_unique_constructvaluemasklookup dst_negative_table_unique_constructvaluemasklookup. (((dc_mask_table_unique_constructvalue) = (((((dst_positive_code_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup)) * S ((dst_positive_code_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup)) + ((dst_positive_scale_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup))) + (((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) * S ((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) + ((dst_negative_scale_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)))) * S ((((dst_positive_code_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup)) * S ((dst_positive_code_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup)) + ((dst_positive_scale_table_unique_constructvaluemasklookup) + (dst_positive_scale_table_unique_constructvaluemasklookup))) + (((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) * S ((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) + ((dst_negative_scale_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)))) + ((((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) * S ((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) + ((dst_negative_scale_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup))) + (((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) * S ((dst_negative_code_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)) + ((dst_negative_scale_table_unique_constructvaluemasklookup) + (dst_negative_scale_table_unique_constructvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemasklookuppositive. ff_h_pvs_table_unique_constructvaluemasklookuppositive + S (dst_positive_table_unique_constructvaluemasklookup) = S ((S (dc_index_table_unique_constructvaluemask)) * dst_positive_scale_table_unique_constructvaluemasklookup)) /\ exists ff_q_pvs_table_unique_constructvaluemasklookuppositive. dst_positive_code_table_unique_constructvaluemasklookup = ff_q_pvs_table_unique_constructvaluemasklookuppositive * S ((S (dc_index_table_unique_constructvaluemask)) * dst_positive_scale_table_unique_constructvaluemasklookup) + (dst_positive_table_unique_constructvaluemasklookup))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemasklookupnegative. ff_h_pvs_table_unique_constructvaluemasklookupnegative + S (dst_negative_table_unique_constructvaluemasklookup) = S ((S (dc_index_table_unique_constructvaluemask)) * dst_negative_scale_table_unique_constructvaluemasklookup)) /\ exists ff_q_pvs_table_unique_constructvaluemasklookupnegative. dst_negative_code_table_unique_constructvaluemasklookup = ff_q_pvs_table_unique_constructvaluemasklookupnegative * S ((S (dc_index_table_unique_constructvaluemask)) * dst_negative_scale_table_unique_constructvaluemasklookup) + (dst_negative_table_unique_constructvaluemasklookup))) /\ (exists ge_balance_positive_table_unique_constructvaluemasklookupvalue ge_balance_negative_table_unique_constructvaluemasklookupvalue. (((((dc_value_table_unique_constructvaluemask) = 2 * (ge_balance_positive_table_unique_constructvaluemasklookupvalue) /\ (ge_balance_negative_table_unique_constructvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_unique_constructvaluemasklookupvaluedecode. (((dc_value_table_unique_constructvaluemask) = 2 * ge_signed_half_table_unique_constructvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_unique_constructvaluemasklookupvalue) = S ge_signed_half_table_unique_constructvaluemasklookupvaluedecode))) /\ ((dst_positive_table_unique_constructvaluemasklookup) + ge_balance_negative_table_unique_constructvaluemasklookupvalue = (dst_negative_table_unique_constructvaluemasklookup) + ge_balance_positive_table_unique_constructvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_unique_constructvaluemask)=0)) /\ (exists dc_quotient_table_unique_constructvaluemaskentry dc_left_table_unique_constructvaluemaskentry dc_right_table_unique_constructvaluemaskentry. (((dc_input_table_unique_construct)=(dc_index_table_unique_constructvaluemask)*dc_quotient_table_unique_constructvaluemaskentry) /\ (((exists dst_positive_code_table_unique_constructvaluemaskentryleft dst_positive_scale_table_unique_constructvaluemaskentryleft dst_negative_code_table_unique_constructvaluemaskentryleft dst_negative_scale_table_unique_constructvaluemaskentryleft dst_positive_table_unique_constructvaluemaskentryleft dst_negative_table_unique_constructvaluemaskentryleft. (((F) = (((((dst_positive_code_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_positive_code_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft)) + ((dst_positive_scale_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft))) + (((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) + ((dst_negative_scale_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)))) * S ((((dst_positive_code_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_positive_code_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft)) + ((dst_positive_scale_table_unique_constructvaluemaskentryleft) + (dst_positive_scale_table_unique_constructvaluemaskentryleft))) + (((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) + ((dst_negative_scale_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)))) + ((((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) + ((dst_negative_scale_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft))) + (((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) * S ((dst_negative_code_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)) + ((dst_negative_scale_table_unique_constructvaluemaskentryleft) + (dst_negative_scale_table_unique_constructvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemaskentryleftpositive. ff_h_pvs_table_unique_constructvaluemaskentryleftpositive + S (dst_positive_table_unique_constructvaluemaskentryleft) = S ((S (dc_index_table_unique_constructvaluemask)) * dst_positive_scale_table_unique_constructvaluemaskentryleft)) /\ exists ff_q_pvs_table_unique_constructvaluemaskentryleftpositive. dst_positive_code_table_unique_constructvaluemaskentryleft = ff_q_pvs_table_unique_constructvaluemaskentryleftpositive * S ((S (dc_index_table_unique_constructvaluemask)) * dst_positive_scale_table_unique_constructvaluemaskentryleft) + (dst_positive_table_unique_constructvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemaskentryleftnegative. ff_h_pvs_table_unique_constructvaluemaskentryleftnegative + S (dst_negative_table_unique_constructvaluemaskentryleft) = S ((S (dc_index_table_unique_constructvaluemask)) * dst_negative_scale_table_unique_constructvaluemaskentryleft)) /\ exists ff_q_pvs_table_unique_constructvaluemaskentryleftnegative. dst_negative_code_table_unique_constructvaluemaskentryleft = ff_q_pvs_table_unique_constructvaluemaskentryleftnegative * S ((S (dc_index_table_unique_constructvaluemask)) * dst_negative_scale_table_unique_constructvaluemaskentryleft) + (dst_negative_table_unique_constructvaluemaskentryleft))) /\ (exists ge_balance_positive_table_unique_constructvaluemaskentryleftvalue ge_balance_negative_table_unique_constructvaluemaskentryleftvalue. (((((dc_left_table_unique_constructvaluemaskentry) = 2 * (ge_balance_positive_table_unique_constructvaluemaskentryleftvalue) /\ (ge_balance_negative_table_unique_constructvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_unique_constructvaluemaskentryleftvaluedecode. (((dc_left_table_unique_constructvaluemaskentry) = 2 * ge_signed_half_table_unique_constructvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_unique_constructvaluemaskentryleftvalue) = S ge_signed_half_table_unique_constructvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_unique_constructvaluemaskentryleft) + ge_balance_negative_table_unique_constructvaluemaskentryleftvalue = (dst_negative_table_unique_constructvaluemaskentryleft) + ge_balance_positive_table_unique_constructvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_unique_constructvaluemaskentryright dst_positive_scale_table_unique_constructvaluemaskentryright dst_negative_code_table_unique_constructvaluemaskentryright dst_negative_scale_table_unique_constructvaluemaskentryright dst_positive_table_unique_constructvaluemaskentryright dst_negative_table_unique_constructvaluemaskentryright. (((G) = (((((dst_positive_code_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright)) * S ((dst_positive_code_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright)) + ((dst_positive_scale_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright))) + (((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) * S ((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) + ((dst_negative_scale_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)))) * S ((((dst_positive_code_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright)) * S ((dst_positive_code_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright)) + ((dst_positive_scale_table_unique_constructvaluemaskentryright) + (dst_positive_scale_table_unique_constructvaluemaskentryright))) + (((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) * S ((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) + ((dst_negative_scale_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)))) + ((((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) * S ((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) + ((dst_negative_scale_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright))) + (((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) * S ((dst_negative_code_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)) + ((dst_negative_scale_table_unique_constructvaluemaskentryright) + (dst_negative_scale_table_unique_constructvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemaskentryrightpositive. ff_h_pvs_table_unique_constructvaluemaskentryrightpositive + S (dst_positive_table_unique_constructvaluemaskentryright) = S ((S (dc_quotient_table_unique_constructvaluemaskentry)) * dst_positive_scale_table_unique_constructvaluemaskentryright)) /\ exists ff_q_pvs_table_unique_constructvaluemaskentryrightpositive. dst_positive_code_table_unique_constructvaluemaskentryright = ff_q_pvs_table_unique_constructvaluemaskentryrightpositive * S ((S (dc_quotient_table_unique_constructvaluemaskentry)) * dst_positive_scale_table_unique_constructvaluemaskentryright) + (dst_positive_table_unique_constructvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_unique_constructvaluemaskentryrightnegative. ff_h_pvs_table_unique_constructvaluemaskentryrightnegative + S (dst_negative_table_unique_constructvaluemaskentryright) = S ((S (dc_quotient_table_unique_constructvaluemaskentry)) * dst_negative_scale_table_unique_constructvaluemaskentryright)) /\ exists ff_q_pvs_table_unique_constructvaluemaskentryrightnegative. dst_negative_code_table_unique_constructvaluemaskentryright = ff_q_pvs_table_unique_constructvaluemaskentryrightnegative * S ((S (dc_quotient_table_unique_constructvaluemaskentry)) * dst_negative_scale_table_unique_constructvaluemaskentryright) + (dst_negative_table_unique_constructvaluemaskentryright))) /\ (exists ge_balance_positive_table_unique_constructvaluemaskentryrightvalue ge_balance_negative_table_unique_constructvaluemaskentryrightvalue. (((((dc_right_table_unique_constructvaluemaskentry) = 2 * (ge_balance_positive_table_unique_constructvaluemaskentryrightvalue) /\ (ge_balance_negative_table_unique_constructvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_unique_constructvaluemaskentryrightvaluedecode. (((dc_right_table_unique_constructvaluemaskentry) = 2 * ge_signed_half_table_unique_constructvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_unique_constructvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_unique_constructvaluemaskentryrightvalue) = S ge_signed_half_table_unique_constructvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_unique_constructvaluemaskentryright) + ge_balance_negative_table_unique_constructvaluemaskentryrightvalue = (dst_negative_table_unique_constructvaluemaskentryright) + ge_balance_positive_table_unique_constructvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_unique_constructvaluemaskentryproduct sto_an_table_unique_constructvaluemaskentryproduct sto_bp_table_unique_constructvaluemaskentryproduct sto_bn_table_unique_constructvaluemaskentryproduct sto_cp_table_unique_constructvaluemaskentryproduct sto_cn_table_unique_constructvaluemaskentryproduct. (((((dc_left_table_unique_constructvaluemaskentry) = 2 * (sto_ap_table_unique_constructvaluemaskentryproduct) /\ (sto_an_table_unique_constructvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_unique_constructvaluemaskentryproductleft. (((dc_left_table_unique_constructvaluemaskentry) = 2 * ge_signed_half_table_unique_constructvaluemaskentryproductleft + 1 /\ (sto_ap_table_unique_constructvaluemaskentryproduct) = 0) /\ (sto_an_table_unique_constructvaluemaskentryproduct) = S ge_signed_half_table_unique_constructvaluemaskentryproductleft))) /\ ((((((dc_right_table_unique_constructvaluemaskentry) = 2 * (sto_bp_table_unique_constructvaluemaskentryproduct) /\ (sto_bn_table_unique_constructvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_unique_constructvaluemaskentryproductright. (((dc_right_table_unique_constructvaluemaskentry) = 2 * ge_signed_half_table_unique_constructvaluemaskentryproductright + 1 /\ (sto_bp_table_unique_constructvaluemaskentryproduct) = 0) /\ (sto_bn_table_unique_constructvaluemaskentryproduct) = S ge_signed_half_table_unique_constructvaluemaskentryproductright))) /\ ((((((dc_value_table_unique_constructvaluemask) = 2 * (sto_cp_table_unique_constructvaluemaskentryproduct) /\ (sto_cn_table_unique_constructvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_unique_constructvaluemaskentryproductoutput. (((dc_value_table_unique_constructvaluemask) = 2 * ge_signed_half_table_unique_constructvaluemaskentryproductoutput + 1 /\ (sto_cp_table_unique_constructvaluemaskentryproduct) = 0) /\ (sto_cn_table_unique_constructvaluemaskentryproduct) = S ge_signed_half_table_unique_constructvaluemaskentryproductoutput))) /\ ((sto_ap_table_unique_constructvaluemaskentryproduct * sto_bp_table_unique_constructvaluemaskentryproduct + sto_an_table_unique_constructvaluemaskentryproduct * sto_bn_table_unique_constructvaluemaskentryproduct) + sto_cn_table_unique_constructvaluemaskentryproduct = (sto_ap_table_unique_constructvaluemaskentryproduct * sto_bn_table_unique_constructvaluemaskentryproduct + sto_an_table_unique_constructvaluemaskentryproduct * sto_bp_table_unique_constructvaluemaskentryproduct) + sto_cp_table_unique_constructvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_unique_constructvaluemask)=0 \/ ~(exists pvs_factor_table_unique_constructvaluemaskentrynondivisor. (dc_input_table_unique_construct) = (dc_index_table_unique_constructvaluemask) * pvs_factor_table_unique_constructvaluemaskentrynondivisor)) /\ ((dc_value_table_unique_constructvaluemask)=0))))))) /\ (exists dst_positive_code_table_unique_constructvaluefold dst_positive_scale_table_unique_constructvaluefold dst_negative_code_table_unique_constructvaluefold dst_negative_scale_table_unique_constructvaluefold dst_positive_sum_table_unique_constructvaluefold dst_negative_sum_table_unique_constructvaluefold. (((dc_mask_table_unique_constructvalue) = (((((dst_positive_code_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold)) * S ((dst_positive_code_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold)) + ((dst_positive_scale_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold))) + (((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) * S ((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) + ((dst_negative_scale_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)))) * S ((((dst_positive_code_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold)) * S ((dst_positive_code_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold)) + ((dst_positive_scale_table_unique_constructvaluefold) + (dst_positive_scale_table_unique_constructvaluefold))) + (((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) * S ((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) + ((dst_negative_scale_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)))) + ((((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) * S ((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) + ((dst_negative_scale_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold))) + (((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) * S ((dst_negative_code_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)) + ((dst_negative_scale_table_unique_constructvaluefold) + (dst_negative_scale_table_unique_constructvaluefold)))))) /\ (((exists fs_u_dst_table_unique_constructvaluefoldpositive fs_v_dst_table_unique_constructvaluefoldpositive. ((((exists fs_h_dst_table_unique_constructvaluefoldpositive_body_start. fs_h_dst_table_unique_constructvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_unique_constructvaluefoldpositive)) /\ exists fs_q_dst_table_unique_constructvaluefoldpositive_body_start. fs_u_dst_table_unique_constructvaluefoldpositive = fs_q_dst_table_unique_constructvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_unique_constructvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldpositive_body_terminal. fs_h_dst_table_unique_constructvaluefoldpositive_body_terminal + S (dst_positive_sum_table_unique_constructvaluefold) = S ((S (S (dc_input_table_unique_construct))) * fs_v_dst_table_unique_constructvaluefoldpositive)) /\ exists fs_q_dst_table_unique_constructvaluefoldpositive_body_terminal. fs_u_dst_table_unique_constructvaluefoldpositive = fs_q_dst_table_unique_constructvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_unique_construct))) * fs_v_dst_table_unique_constructvaluefoldpositive) + (dst_positive_sum_table_unique_constructvaluefold))) /\ forall fs_i_dst_table_unique_constructvaluefoldpositive_body_steps. (exists fs_lt_dst_table_unique_constructvaluefoldpositive_body_steps_bound. fs_lt_dst_table_unique_constructvaluefoldpositive_body_steps_bound + S fs_i_dst_table_unique_constructvaluefoldpositive_body_steps = S (dc_input_table_unique_construct)) -> exists fs_a_dst_table_unique_constructvaluefoldpositive_body_steps fs_r_dst_table_unique_constructvaluefoldpositive_body_steps fs_s_dst_table_unique_constructvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_summand. fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_unique_constructvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * dst_positive_scale_table_unique_constructvaluefold)) /\ exists fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_summand. dst_positive_code_table_unique_constructvaluefold = fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * dst_positive_scale_table_unique_constructvaluefold) + (fs_a_dst_table_unique_constructvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_partial. fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_unique_constructvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * fs_v_dst_table_unique_constructvaluefoldpositive)) /\ exists fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_partial. fs_u_dst_table_unique_constructvaluefoldpositive = fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * fs_v_dst_table_unique_constructvaluefoldpositive) + (fs_r_dst_table_unique_constructvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_successor. fs_h_dst_table_unique_constructvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_unique_constructvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * fs_v_dst_table_unique_constructvaluefoldpositive)) /\ exists fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_successor. fs_u_dst_table_unique_constructvaluefoldpositive = fs_q_dst_table_unique_constructvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_unique_constructvaluefoldpositive_body_steps)) * fs_v_dst_table_unique_constructvaluefoldpositive) + (fs_s_dst_table_unique_constructvaluefoldpositive_body_steps))) /\ fs_s_dst_table_unique_constructvaluefoldpositive_body_steps = fs_r_dst_table_unique_constructvaluefoldpositive_body_steps + fs_a_dst_table_unique_constructvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_unique_constructvaluefoldnegative fs_v_dst_table_unique_constructvaluefoldnegative. ((((exists fs_h_dst_table_unique_constructvaluefoldnegative_body_start. fs_h_dst_table_unique_constructvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_unique_constructvaluefoldnegative)) /\ exists fs_q_dst_table_unique_constructvaluefoldnegative_body_start. fs_u_dst_table_unique_constructvaluefoldnegative = fs_q_dst_table_unique_constructvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_unique_constructvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldnegative_body_terminal. fs_h_dst_table_unique_constructvaluefoldnegative_body_terminal + S (dst_negative_sum_table_unique_constructvaluefold) = S ((S (S (dc_input_table_unique_construct))) * fs_v_dst_table_unique_constructvaluefoldnegative)) /\ exists fs_q_dst_table_unique_constructvaluefoldnegative_body_terminal. fs_u_dst_table_unique_constructvaluefoldnegative = fs_q_dst_table_unique_constructvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_unique_construct))) * fs_v_dst_table_unique_constructvaluefoldnegative) + (dst_negative_sum_table_unique_constructvaluefold))) /\ forall fs_i_dst_table_unique_constructvaluefoldnegative_body_steps. (exists fs_lt_dst_table_unique_constructvaluefoldnegative_body_steps_bound. fs_lt_dst_table_unique_constructvaluefoldnegative_body_steps_bound + S fs_i_dst_table_unique_constructvaluefoldnegative_body_steps = S (dc_input_table_unique_construct)) -> exists fs_a_dst_table_unique_constructvaluefoldnegative_body_steps fs_r_dst_table_unique_constructvaluefoldnegative_body_steps fs_s_dst_table_unique_constructvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_summand. fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_unique_constructvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * dst_negative_scale_table_unique_constructvaluefold)) /\ exists fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_summand. dst_negative_code_table_unique_constructvaluefold = fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * dst_negative_scale_table_unique_constructvaluefold) + (fs_a_dst_table_unique_constructvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_partial. fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_unique_constructvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * fs_v_dst_table_unique_constructvaluefoldnegative)) /\ exists fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_partial. fs_u_dst_table_unique_constructvaluefoldnegative = fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * fs_v_dst_table_unique_constructvaluefoldnegative) + (fs_r_dst_table_unique_constructvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_successor. fs_h_dst_table_unique_constructvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_unique_constructvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * fs_v_dst_table_unique_constructvaluefoldnegative)) /\ exists fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_successor. fs_u_dst_table_unique_constructvaluefoldnegative = fs_q_dst_table_unique_constructvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_unique_constructvaluefoldnegative_body_steps)) * fs_v_dst_table_unique_constructvaluefoldnegative) + (fs_s_dst_table_unique_constructvaluefoldnegative_body_steps))) /\ fs_s_dst_table_unique_constructvaluefoldnegative_body_steps = fs_r_dst_table_unique_constructvaluefoldnegative_body_steps + fs_a_dst_table_unique_constructvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_unique_constructvaluefoldresult ge_balance_negative_table_unique_constructvaluefoldresult. (((((dc_output_table_unique_construct) = 2 * (ge_balance_positive_table_unique_constructvaluefoldresult) /\ (ge_balance_negative_table_unique_constructvaluefoldresult) = 0) \/ exists ge_signed_half_table_unique_constructvaluefoldresultdecode. (((dc_output_table_unique_construct) = 2 * ge_signed_half_table_unique_constructvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_unique_constructvaluefoldresult) = 0) /\ (ge_balance_negative_table_unique_constructvaluefoldresult) = S ge_signed_half_table_unique_constructvaluefoldresultdecode))) /\ ((dst_positive_sum_table_unique_constructvaluefold) + ge_balance_negative_table_unique_constructvaluefoldresult = (dst_negative_sum_table_unique_constructvaluefold) + ge_balance_positive_table_unique_constructvaluefoldresult)))))))))))))))))))) - 0007
specialize dirichlet_convolution_table_exists (N) - 0008
specialize dirichlet_convolution_table_exists (F) - 0009
specialize dirichlet_convolution_table_exists (G) - 0010
apply dirichlet_convolution_table_exists - 0011
exact hF - 0012
exact hG - 0013
cases h - 0014
exists x - 0015
split - 0016
exact h_witness - 0017
intro K - 0018
intro hK - 0019
specialize dirichlet_convolution_table_extensional (N) - 0020
specialize dirichlet_convolution_table_extensional (F) - 0021
specialize dirichlet_convolution_table_extensional (G) - 0022
specialize dirichlet_convolution_table_extensional (x) - 0023
specialize dirichlet_convolution_table_extensional (K) - 0024
apply dirichlet_convolution_table_extensional - 0025
exact h_witness - 0026
exact hK