Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ArithTable(N,F) → ArithTable(N,G) → ∃ x. DirichletTable(N,F,G,x) ∧ (∀ y. DirichletTable(N,F,G,y) → ArithPositiveEqual(x,y,N))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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)))Complete tactic proof in conservative notation
All 26 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
26 script commands · 8 reading checkpoints · 1 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
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.
- L6
have h : ∃ H. DirichletTable(N,F,G,H)Definitions: DirichletTable(N,F,G,H)Original native command in the exact edition - L7
specialize dirichlet_convolution_table_exists (N) - L8
specialize dirichlet_convolution_table_exists (F) - L9
specialize dirichlet_convolution_table_exists (G) - L10
apply dirichlet_convolution_table_exists - L11
exact hF - L12
exact hG
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 defined command ledger · 26 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hF - 0005
intro hG - 0006
have h : ∃ H. DirichletTable(N,F,G,H) - 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