Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Full G009 remains broader.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ H. ∀ A. ∀ B. ∀ n. ∀ u. ∀ v. DirichletTable(N,F,G,A) → DirichletTable(N,G,H,B) → ¬n = 0 → Le(n,N) → DirichletSum(A,H,n,u) → DirichletSum(F,B,n,v) → u = vEvery linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F G H A B n u v. (((exists dst_positive_code_assoc_FGleft dst_positive_scale_assoc_FGleft dst_negative_code_assoc_FGleft dst_negative_scale_assoc_FGleft. (((F) = (((((dst_positive_code_assoc_FGleft) + (dst_positive_scale_assoc_FGleft)) * S ((dst_positive_code_assoc_FGleft) + (dst_positive_scale_assoc_FGleft)) + ((dst_positive_scale_assoc_FGleft) + (dst_positive_scale_assoc_FGleft))) + (((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) * S ((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) + ((dst_negative_scale_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)))) * S ((((dst_positive_code_assoc_FGleft) + (dst_positive_scale_assoc_FGleft)) * S ((dst_positive_code_assoc_FGleft) + (dst_positive_scale_assoc_FGleft)) + ((dst_positive_scale_assoc_FGleft) + (dst_positive_scale_assoc_FGleft))) + (((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) * S ((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) + ((dst_negative_scale_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)))) + ((((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) * S ((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) + ((dst_negative_scale_assoc_FGleft) + (dst_negative_scale_assoc_FGleft))) + (((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) * S ((dst_negative_code_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)) + ((dst_negative_scale_assoc_FGleft) + (dst_negative_scale_assoc_FGleft)))))) /\ (forall dst_index_assoc_FGleft. (exists pvs_le_gap_assoc_FGleftdomain. pvs_le_gap_assoc_FGleftdomain + (dst_index_assoc_FGleft) = (N)) -> exists dst_positive_assoc_FGleft dst_negative_assoc_FGleft dst_value_assoc_FGleft. ((((exists ff_h_pvs_assoc_FGleftentrypositive. ff_h_pvs_assoc_FGleftentrypositive + S (dst_positive_assoc_FGleft) = S ((S (dst_index_assoc_FGleft)) * dst_positive_scale_assoc_FGleft)) /\ exists ff_q_pvs_assoc_FGleftentrypositive. dst_positive_code_assoc_FGleft = ff_q_pvs_assoc_FGleftentrypositive * S ((S (dst_index_assoc_FGleft)) * dst_positive_scale_assoc_FGleft) + (dst_positive_assoc_FGleft))) /\ (((((exists ff_h_pvs_assoc_FGleftentrynegative. ff_h_pvs_assoc_FGleftentrynegative + S (dst_negative_assoc_FGleft) = S ((S (dst_index_assoc_FGleft)) * dst_negative_scale_assoc_FGleft)) /\ exists ff_q_pvs_assoc_FGleftentrynegative. dst_negative_code_assoc_FGleft = ff_q_pvs_assoc_FGleftentrynegative * S ((S (dst_index_assoc_FGleft)) * dst_negative_scale_assoc_FGleft) + (dst_negative_assoc_FGleft))) /\ (exists ge_balance_positive_assoc_FGleftentryvalue ge_balance_negative_assoc_FGleftentryvalue. (((((dst_value_assoc_FGleft) = 2 * (ge_balance_positive_assoc_FGleftentryvalue) /\ (ge_balance_negative_assoc_FGleftentryvalue) = 0) \/ exists ge_signed_half_assoc_FGleftentryvaluedecode. (((dst_value_assoc_FGleft) = 2 * ge_signed_half_assoc_FGleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_FGleftentryvalue) = 0) /\ (ge_balance_negative_assoc_FGleftentryvalue) = S ge_signed_half_assoc_FGleftentryvaluedecode))) /\ ((dst_positive_assoc_FGleft) + ge_balance_negative_assoc_FGleftentryvalue = (dst_negative_assoc_FGleft) + ge_balance_positive_assoc_FGleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_FGright dst_positive_scale_assoc_FGright dst_negative_code_assoc_FGright dst_negative_scale_assoc_FGright. (((G) = (((((dst_positive_code_assoc_FGright) + (dst_positive_scale_assoc_FGright)) * S ((dst_positive_code_assoc_FGright) + (dst_positive_scale_assoc_FGright)) + ((dst_positive_scale_assoc_FGright) + (dst_positive_scale_assoc_FGright))) + (((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) * S ((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) + ((dst_negative_scale_assoc_FGright) + (dst_negative_scale_assoc_FGright)))) * S ((((dst_positive_code_assoc_FGright) + (dst_positive_scale_assoc_FGright)) * S ((dst_positive_code_assoc_FGright) + (dst_positive_scale_assoc_FGright)) + ((dst_positive_scale_assoc_FGright) + (dst_positive_scale_assoc_FGright))) + (((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) * S ((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) + ((dst_negative_scale_assoc_FGright) + (dst_negative_scale_assoc_FGright)))) + ((((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) * S ((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) + ((dst_negative_scale_assoc_FGright) + (dst_negative_scale_assoc_FGright))) + (((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) * S ((dst_negative_code_assoc_FGright) + (dst_negative_scale_assoc_FGright)) + ((dst_negative_scale_assoc_FGright) + (dst_negative_scale_assoc_FGright)))))) /\ (forall dst_index_assoc_FGright. (exists pvs_le_gap_assoc_FGrightdomain. pvs_le_gap_assoc_FGrightdomain + (dst_index_assoc_FGright) = (N)) -> exists dst_positive_assoc_FGright dst_negative_assoc_FGright dst_value_assoc_FGright. ((((exists ff_h_pvs_assoc_FGrightentrypositive. ff_h_pvs_assoc_FGrightentrypositive + S (dst_positive_assoc_FGright) = S ((S (dst_index_assoc_FGright)) * dst_positive_scale_assoc_FGright)) /\ exists ff_q_pvs_assoc_FGrightentrypositive. dst_positive_code_assoc_FGright = ff_q_pvs_assoc_FGrightentrypositive * S ((S (dst_index_assoc_FGright)) * dst_positive_scale_assoc_FGright) + (dst_positive_assoc_FGright))) /\ (((((exists ff_h_pvs_assoc_FGrightentrynegative. ff_h_pvs_assoc_FGrightentrynegative + S (dst_negative_assoc_FGright) = S ((S (dst_index_assoc_FGright)) * dst_negative_scale_assoc_FGright)) /\ exists ff_q_pvs_assoc_FGrightentrynegative. dst_negative_code_assoc_FGright = ff_q_pvs_assoc_FGrightentrynegative * S ((S (dst_index_assoc_FGright)) * dst_negative_scale_assoc_FGright) + (dst_negative_assoc_FGright))) /\ (exists ge_balance_positive_assoc_FGrightentryvalue ge_balance_negative_assoc_FGrightentryvalue. (((((dst_value_assoc_FGright) = 2 * (ge_balance_positive_assoc_FGrightentryvalue) /\ (ge_balance_negative_assoc_FGrightentryvalue) = 0) \/ exists ge_signed_half_assoc_FGrightentryvaluedecode. (((dst_value_assoc_FGright) = 2 * ge_signed_half_assoc_FGrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_FGrightentryvalue) = 0) /\ (ge_balance_negative_assoc_FGrightentryvalue) = S ge_signed_half_assoc_FGrightentryvaluedecode))) /\ ((dst_positive_assoc_FGright) + ge_balance_negative_assoc_FGrightentryvalue = (dst_negative_assoc_FGright) + ge_balance_positive_assoc_FGrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_FGtable dst_positive_scale_assoc_FGtable dst_negative_code_assoc_FGtable dst_negative_scale_assoc_FGtable. (((A) = (((((dst_positive_code_assoc_FGtable) + (dst_positive_scale_assoc_FGtable)) * S ((dst_positive_code_assoc_FGtable) + (dst_positive_scale_assoc_FGtable)) + ((dst_positive_scale_assoc_FGtable) + (dst_positive_scale_assoc_FGtable))) + (((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) * S ((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) + ((dst_negative_scale_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)))) * S ((((dst_positive_code_assoc_FGtable) + (dst_positive_scale_assoc_FGtable)) * S ((dst_positive_code_assoc_FGtable) + (dst_positive_scale_assoc_FGtable)) + ((dst_positive_scale_assoc_FGtable) + (dst_positive_scale_assoc_FGtable))) + (((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) * S ((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) + ((dst_negative_scale_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)))) + ((((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) * S ((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) + ((dst_negative_scale_assoc_FGtable) + (dst_negative_scale_assoc_FGtable))) + (((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) * S ((dst_negative_code_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)) + ((dst_negative_scale_assoc_FGtable) + (dst_negative_scale_assoc_FGtable)))))) /\ (forall dst_index_assoc_FGtable. (exists pvs_le_gap_assoc_FGtabledomain. pvs_le_gap_assoc_FGtabledomain + (dst_index_assoc_FGtable) = (N)) -> exists dst_positive_assoc_FGtable dst_negative_assoc_FGtable dst_value_assoc_FGtable. ((((exists ff_h_pvs_assoc_FGtableentrypositive. ff_h_pvs_assoc_FGtableentrypositive + S (dst_positive_assoc_FGtable) = S ((S (dst_index_assoc_FGtable)) * dst_positive_scale_assoc_FGtable)) /\ exists ff_q_pvs_assoc_FGtableentrypositive. dst_positive_code_assoc_FGtable = ff_q_pvs_assoc_FGtableentrypositive * S ((S (dst_index_assoc_FGtable)) * dst_positive_scale_assoc_FGtable) + (dst_positive_assoc_FGtable))) /\ (((((exists ff_h_pvs_assoc_FGtableentrynegative. ff_h_pvs_assoc_FGtableentrynegative + S (dst_negative_assoc_FGtable) = S ((S (dst_index_assoc_FGtable)) * dst_negative_scale_assoc_FGtable)) /\ exists ff_q_pvs_assoc_FGtableentrynegative. dst_negative_code_assoc_FGtable = ff_q_pvs_assoc_FGtableentrynegative * S ((S (dst_index_assoc_FGtable)) * dst_negative_scale_assoc_FGtable) + (dst_negative_assoc_FGtable))) /\ (exists ge_balance_positive_assoc_FGtableentryvalue ge_balance_negative_assoc_FGtableentryvalue. (((((dst_value_assoc_FGtable) = 2 * (ge_balance_positive_assoc_FGtableentryvalue) /\ (ge_balance_negative_assoc_FGtableentryvalue) = 0) \/ exists ge_signed_half_assoc_FGtableentryvaluedecode. (((dst_value_assoc_FGtable) = 2 * ge_signed_half_assoc_FGtableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_FGtableentryvalue) = 0) /\ (ge_balance_negative_assoc_FGtableentryvalue) = S ge_signed_half_assoc_FGtableentryvaluedecode))) /\ ((dst_positive_assoc_FGtable) + ge_balance_negative_assoc_FGtableentryvalue = (dst_negative_assoc_FGtable) + ge_balance_positive_assoc_FGtableentryvalue))))))))) /\ (forall dc_input_assoc_FG dc_output_assoc_FG. ~(dc_input_assoc_FG=0) -> (exists pvs_le_gap_assoc_FGdomain. pvs_le_gap_assoc_FGdomain + (dc_input_assoc_FG) = (N)) -> (exists dst_positive_code_assoc_FGlookup dst_positive_scale_assoc_FGlookup dst_negative_code_assoc_FGlookup dst_negative_scale_assoc_FGlookup dst_positive_assoc_FGlookup dst_negative_assoc_FGlookup. (((A) = (((((dst_positive_code_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup)) * S ((dst_positive_code_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup)) + ((dst_positive_scale_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup))) + (((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) * S ((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) + ((dst_negative_scale_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)))) * S ((((dst_positive_code_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup)) * S ((dst_positive_code_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup)) + ((dst_positive_scale_assoc_FGlookup) + (dst_positive_scale_assoc_FGlookup))) + (((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) * S ((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) + ((dst_negative_scale_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)))) + ((((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) * S ((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) + ((dst_negative_scale_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup))) + (((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) * S ((dst_negative_code_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)) + ((dst_negative_scale_assoc_FGlookup) + (dst_negative_scale_assoc_FGlookup)))))) /\ (((((exists ff_h_pvs_assoc_FGlookuppositive. ff_h_pvs_assoc_FGlookuppositive + S (dst_positive_assoc_FGlookup) = S ((S (dc_input_assoc_FG)) * dst_positive_scale_assoc_FGlookup)) /\ exists ff_q_pvs_assoc_FGlookuppositive. dst_positive_code_assoc_FGlookup = ff_q_pvs_assoc_FGlookuppositive * S ((S (dc_input_assoc_FG)) * dst_positive_scale_assoc_FGlookup) + (dst_positive_assoc_FGlookup))) /\ (((((exists ff_h_pvs_assoc_FGlookupnegative. ff_h_pvs_assoc_FGlookupnegative + S (dst_negative_assoc_FGlookup) = S ((S (dc_input_assoc_FG)) * dst_negative_scale_assoc_FGlookup)) /\ exists ff_q_pvs_assoc_FGlookupnegative. dst_negative_code_assoc_FGlookup = ff_q_pvs_assoc_FGlookupnegative * S ((S (dc_input_assoc_FG)) * dst_negative_scale_assoc_FGlookup) + (dst_negative_assoc_FGlookup))) /\ (exists ge_balance_positive_assoc_FGlookupvalue ge_balance_negative_assoc_FGlookupvalue. (((((dc_output_assoc_FG) = 2 * (ge_balance_positive_assoc_FGlookupvalue) /\ (ge_balance_negative_assoc_FGlookupvalue) = 0) \/ exists ge_signed_half_assoc_FGlookupvaluedecode. (((dc_output_assoc_FG) = 2 * ge_signed_half_assoc_FGlookupvaluedecode + 1 /\ (ge_balance_positive_assoc_FGlookupvalue) = 0) /\ (ge_balance_negative_assoc_FGlookupvalue) = S ge_signed_half_assoc_FGlookupvaluedecode))) /\ ((dst_positive_assoc_FGlookup) + ge_balance_negative_assoc_FGlookupvalue = (dst_negative_assoc_FGlookup) + ge_balance_positive_assoc_FGlookupvalue))))))))) -> (((~((dc_input_assoc_FG)=0)) /\ (exists dc_mask_assoc_FGvalue. ((((exists dst_positive_code_assoc_FGvaluemasktable dst_positive_scale_assoc_FGvaluemasktable dst_negative_code_assoc_FGvaluemasktable dst_negative_scale_assoc_FGvaluemasktable. (((dc_mask_assoc_FGvalue) = (((((dst_positive_code_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable)) * S ((dst_positive_code_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable)) + ((dst_positive_scale_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable))) + (((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) * S ((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) + ((dst_negative_scale_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)))) * S ((((dst_positive_code_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable)) * S ((dst_positive_code_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable)) + ((dst_positive_scale_assoc_FGvaluemasktable) + (dst_positive_scale_assoc_FGvaluemasktable))) + (((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) * S ((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) + ((dst_negative_scale_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)))) + ((((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) * S ((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) + ((dst_negative_scale_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable))) + (((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) * S ((dst_negative_code_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)) + ((dst_negative_scale_assoc_FGvaluemasktable) + (dst_negative_scale_assoc_FGvaluemasktable)))))) /\ (forall dst_index_assoc_FGvaluemasktable. (exists pvs_le_gap_assoc_FGvaluemasktabledomain. pvs_le_gap_assoc_FGvaluemasktabledomain + (dst_index_assoc_FGvaluemasktable) = (dc_input_assoc_FG)) -> exists dst_positive_assoc_FGvaluemasktable dst_negative_assoc_FGvaluemasktable dst_value_assoc_FGvaluemasktable. ((((exists ff_h_pvs_assoc_FGvaluemasktableentrypositive. ff_h_pvs_assoc_FGvaluemasktableentrypositive + S (dst_positive_assoc_FGvaluemasktable) = S ((S (dst_index_assoc_FGvaluemasktable)) * dst_positive_scale_assoc_FGvaluemasktable)) /\ exists ff_q_pvs_assoc_FGvaluemasktableentrypositive. dst_positive_code_assoc_FGvaluemasktable = ff_q_pvs_assoc_FGvaluemasktableentrypositive * S ((S (dst_index_assoc_FGvaluemasktable)) * dst_positive_scale_assoc_FGvaluemasktable) + (dst_positive_assoc_FGvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_FGvaluemasktableentrynegative. ff_h_pvs_assoc_FGvaluemasktableentrynegative + S (dst_negative_assoc_FGvaluemasktable) = S ((S (dst_index_assoc_FGvaluemasktable)) * dst_negative_scale_assoc_FGvaluemasktable)) /\ exists ff_q_pvs_assoc_FGvaluemasktableentrynegative. dst_negative_code_assoc_FGvaluemasktable = ff_q_pvs_assoc_FGvaluemasktableentrynegative * S ((S (dst_index_assoc_FGvaluemasktable)) * dst_negative_scale_assoc_FGvaluemasktable) + (dst_negative_assoc_FGvaluemasktable))) /\ (exists ge_balance_positive_assoc_FGvaluemasktableentryvalue ge_balance_negative_assoc_FGvaluemasktableentryvalue. (((((dst_value_assoc_FGvaluemasktable) = 2 * (ge_balance_positive_assoc_FGvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_FGvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_FGvaluemasktableentryvaluedecode. (((dst_value_assoc_FGvaluemasktable) = 2 * ge_signed_half_assoc_FGvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_FGvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_FGvaluemasktableentryvalue) = S ge_signed_half_assoc_FGvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_FGvaluemasktable) + ge_balance_negative_assoc_FGvaluemasktableentryvalue = (dst_negative_assoc_FGvaluemasktable) + ge_balance_positive_assoc_FGvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_FGvaluemask dc_value_assoc_FGvaluemask. (exists pvs_le_gap_assoc_FGvaluemaskdomain. pvs_le_gap_assoc_FGvaluemaskdomain + (dc_index_assoc_FGvaluemask) = (dc_input_assoc_FG)) -> (exists dst_positive_code_assoc_FGvaluemasklookup dst_positive_scale_assoc_FGvaluemasklookup dst_negative_code_assoc_FGvaluemasklookup dst_negative_scale_assoc_FGvaluemasklookup dst_positive_assoc_FGvaluemasklookup dst_negative_assoc_FGvaluemasklookup. (((dc_mask_assoc_FGvalue) = (((((dst_positive_code_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup)) * S ((dst_positive_code_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup)) + ((dst_positive_scale_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup))) + (((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) * S ((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) + ((dst_negative_scale_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)))) * S ((((dst_positive_code_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup)) * S ((dst_positive_code_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup)) + ((dst_positive_scale_assoc_FGvaluemasklookup) + (dst_positive_scale_assoc_FGvaluemasklookup))) + (((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) * S ((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) + ((dst_negative_scale_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)))) + ((((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) * S ((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) + ((dst_negative_scale_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup))) + (((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) * S ((dst_negative_code_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)) + ((dst_negative_scale_assoc_FGvaluemasklookup) + (dst_negative_scale_assoc_FGvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_FGvaluemasklookuppositive. ff_h_pvs_assoc_FGvaluemasklookuppositive + S (dst_positive_assoc_FGvaluemasklookup) = S ((S (dc_index_assoc_FGvaluemask)) * dst_positive_scale_assoc_FGvaluemasklookup)) /\ exists ff_q_pvs_assoc_FGvaluemasklookuppositive. dst_positive_code_assoc_FGvaluemasklookup = ff_q_pvs_assoc_FGvaluemasklookuppositive * S ((S (dc_index_assoc_FGvaluemask)) * dst_positive_scale_assoc_FGvaluemasklookup) + (dst_positive_assoc_FGvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_FGvaluemasklookupnegative. ff_h_pvs_assoc_FGvaluemasklookupnegative + S (dst_negative_assoc_FGvaluemasklookup) = S ((S (dc_index_assoc_FGvaluemask)) * dst_negative_scale_assoc_FGvaluemasklookup)) /\ exists ff_q_pvs_assoc_FGvaluemasklookupnegative. dst_negative_code_assoc_FGvaluemasklookup = ff_q_pvs_assoc_FGvaluemasklookupnegative * S ((S (dc_index_assoc_FGvaluemask)) * dst_negative_scale_assoc_FGvaluemasklookup) + (dst_negative_assoc_FGvaluemasklookup))) /\ (exists ge_balance_positive_assoc_FGvaluemasklookupvalue ge_balance_negative_assoc_FGvaluemasklookupvalue. (((((dc_value_assoc_FGvaluemask) = 2 * (ge_balance_positive_assoc_FGvaluemasklookupvalue) /\ (ge_balance_negative_assoc_FGvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_FGvaluemasklookupvaluedecode. (((dc_value_assoc_FGvaluemask) = 2 * ge_signed_half_assoc_FGvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_FGvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_FGvaluemasklookupvalue) = S ge_signed_half_assoc_FGvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_FGvaluemasklookup) + ge_balance_negative_assoc_FGvaluemasklookupvalue = (dst_negative_assoc_FGvaluemasklookup) + ge_balance_positive_assoc_FGvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_FGvaluemask)=0)) /\ (exists dc_quotient_assoc_FGvaluemaskentry dc_left_assoc_FGvaluemaskentry dc_right_assoc_FGvaluemaskentry. (((dc_input_assoc_FG)=(dc_index_assoc_FGvaluemask)*dc_quotient_assoc_FGvaluemaskentry) /\ (((exists dst_positive_code_assoc_FGvaluemaskentryleft dst_positive_scale_assoc_FGvaluemaskentryleft dst_negative_code_assoc_FGvaluemaskentryleft dst_negative_scale_assoc_FGvaluemaskentryleft dst_positive_assoc_FGvaluemaskentryleft dst_negative_assoc_FGvaluemaskentryleft. (((F) = (((((dst_positive_code_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft)) * S ((dst_positive_code_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft)) + ((dst_positive_scale_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft))) + (((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) * S ((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) + ((dst_negative_scale_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft)) * S ((dst_positive_code_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft)) + ((dst_positive_scale_assoc_FGvaluemaskentryleft) + (dst_positive_scale_assoc_FGvaluemaskentryleft))) + (((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) * S ((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) + ((dst_negative_scale_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)))) + ((((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) * S ((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) + ((dst_negative_scale_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft))) + (((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) * S ((dst_negative_code_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)) + ((dst_negative_scale_assoc_FGvaluemaskentryleft) + (dst_negative_scale_assoc_FGvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_FGvaluemaskentryleftpositive. ff_h_pvs_assoc_FGvaluemaskentryleftpositive + S (dst_positive_assoc_FGvaluemaskentryleft) = S ((S (dc_index_assoc_FGvaluemask)) * dst_positive_scale_assoc_FGvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_FGvaluemaskentryleftpositive. dst_positive_code_assoc_FGvaluemaskentryleft = ff_q_pvs_assoc_FGvaluemaskentryleftpositive * S ((S (dc_index_assoc_FGvaluemask)) * dst_positive_scale_assoc_FGvaluemaskentryleft) + (dst_positive_assoc_FGvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_FGvaluemaskentryleftnegative. ff_h_pvs_assoc_FGvaluemaskentryleftnegative + S (dst_negative_assoc_FGvaluemaskentryleft) = S ((S (dc_index_assoc_FGvaluemask)) * dst_negative_scale_assoc_FGvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_FGvaluemaskentryleftnegative. dst_negative_code_assoc_FGvaluemaskentryleft = ff_q_pvs_assoc_FGvaluemaskentryleftnegative * S ((S (dc_index_assoc_FGvaluemask)) * dst_negative_scale_assoc_FGvaluemaskentryleft) + (dst_negative_assoc_FGvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_FGvaluemaskentryleftvalue ge_balance_negative_assoc_FGvaluemaskentryleftvalue. (((((dc_left_assoc_FGvaluemaskentry) = 2 * (ge_balance_positive_assoc_FGvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_FGvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_FGvaluemaskentryleftvaluedecode. (((dc_left_assoc_FGvaluemaskentry) = 2 * ge_signed_half_assoc_FGvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_FGvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_FGvaluemaskentryleftvalue) = S ge_signed_half_assoc_FGvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_FGvaluemaskentryleft) + ge_balance_negative_assoc_FGvaluemaskentryleftvalue = (dst_negative_assoc_FGvaluemaskentryleft) + ge_balance_positive_assoc_FGvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_FGvaluemaskentryright dst_positive_scale_assoc_FGvaluemaskentryright dst_negative_code_assoc_FGvaluemaskentryright dst_negative_scale_assoc_FGvaluemaskentryright dst_positive_assoc_FGvaluemaskentryright dst_negative_assoc_FGvaluemaskentryright. (((G) = (((((dst_positive_code_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright)) * S ((dst_positive_code_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright)) + ((dst_positive_scale_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright))) + (((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) * S ((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) + ((dst_negative_scale_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)))) * S ((((dst_positive_code_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright)) * S ((dst_positive_code_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright)) + ((dst_positive_scale_assoc_FGvaluemaskentryright) + (dst_positive_scale_assoc_FGvaluemaskentryright))) + (((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) * S ((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) + ((dst_negative_scale_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)))) + ((((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) * S ((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) + ((dst_negative_scale_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright))) + (((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) * S ((dst_negative_code_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)) + ((dst_negative_scale_assoc_FGvaluemaskentryright) + (dst_negative_scale_assoc_FGvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_FGvaluemaskentryrightpositive. ff_h_pvs_assoc_FGvaluemaskentryrightpositive + S (dst_positive_assoc_FGvaluemaskentryright) = S ((S (dc_quotient_assoc_FGvaluemaskentry)) * dst_positive_scale_assoc_FGvaluemaskentryright)) /\ exists ff_q_pvs_assoc_FGvaluemaskentryrightpositive. dst_positive_code_assoc_FGvaluemaskentryright = ff_q_pvs_assoc_FGvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_FGvaluemaskentry)) * dst_positive_scale_assoc_FGvaluemaskentryright) + (dst_positive_assoc_FGvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_FGvaluemaskentryrightnegative. ff_h_pvs_assoc_FGvaluemaskentryrightnegative + S (dst_negative_assoc_FGvaluemaskentryright) = S ((S (dc_quotient_assoc_FGvaluemaskentry)) * dst_negative_scale_assoc_FGvaluemaskentryright)) /\ exists ff_q_pvs_assoc_FGvaluemaskentryrightnegative. dst_negative_code_assoc_FGvaluemaskentryright = ff_q_pvs_assoc_FGvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_FGvaluemaskentry)) * dst_negative_scale_assoc_FGvaluemaskentryright) + (dst_negative_assoc_FGvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_FGvaluemaskentryrightvalue ge_balance_negative_assoc_FGvaluemaskentryrightvalue. (((((dc_right_assoc_FGvaluemaskentry) = 2 * (ge_balance_positive_assoc_FGvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_FGvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_FGvaluemaskentryrightvaluedecode. (((dc_right_assoc_FGvaluemaskentry) = 2 * ge_signed_half_assoc_FGvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_FGvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_FGvaluemaskentryrightvalue) = S ge_signed_half_assoc_FGvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_FGvaluemaskentryright) + ge_balance_negative_assoc_FGvaluemaskentryrightvalue = (dst_negative_assoc_FGvaluemaskentryright) + ge_balance_positive_assoc_FGvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_FGvaluemaskentryproduct sto_an_assoc_FGvaluemaskentryproduct sto_bp_assoc_FGvaluemaskentryproduct sto_bn_assoc_FGvaluemaskentryproduct sto_cp_assoc_FGvaluemaskentryproduct sto_cn_assoc_FGvaluemaskentryproduct. (((((dc_left_assoc_FGvaluemaskentry) = 2 * (sto_ap_assoc_FGvaluemaskentryproduct) /\ (sto_an_assoc_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_FGvaluemaskentryproductleft. (((dc_left_assoc_FGvaluemaskentry) = 2 * ge_signed_half_assoc_FGvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_FGvaluemaskentryproduct) = 0) /\ (sto_an_assoc_FGvaluemaskentryproduct) = S ge_signed_half_assoc_FGvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_FGvaluemaskentry) = 2 * (sto_bp_assoc_FGvaluemaskentryproduct) /\ (sto_bn_assoc_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_FGvaluemaskentryproductright. (((dc_right_assoc_FGvaluemaskentry) = 2 * ge_signed_half_assoc_FGvaluemaskentryproductright + 1 /\ (sto_bp_assoc_FGvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_FGvaluemaskentryproduct) = S ge_signed_half_assoc_FGvaluemaskentryproductright))) /\ ((((((dc_value_assoc_FGvaluemask) = 2 * (sto_cp_assoc_FGvaluemaskentryproduct) /\ (sto_cn_assoc_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_FGvaluemaskentryproductoutput. (((dc_value_assoc_FGvaluemask) = 2 * ge_signed_half_assoc_FGvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_FGvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_FGvaluemaskentryproduct) = S ge_signed_half_assoc_FGvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_FGvaluemaskentryproduct * sto_bp_assoc_FGvaluemaskentryproduct + sto_an_assoc_FGvaluemaskentryproduct * sto_bn_assoc_FGvaluemaskentryproduct) + sto_cn_assoc_FGvaluemaskentryproduct = (sto_ap_assoc_FGvaluemaskentryproduct * sto_bn_assoc_FGvaluemaskentryproduct + sto_an_assoc_FGvaluemaskentryproduct * sto_bp_assoc_FGvaluemaskentryproduct) + sto_cp_assoc_FGvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_FGvaluemask)=0 \/ ~(exists pvs_factor_assoc_FGvaluemaskentrynondivisor. (dc_input_assoc_FG) = (dc_index_assoc_FGvaluemask) * pvs_factor_assoc_FGvaluemaskentrynondivisor)) /\ ((dc_value_assoc_FGvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_FGvaluefold dst_positive_scale_assoc_FGvaluefold dst_negative_code_assoc_FGvaluefold dst_negative_scale_assoc_FGvaluefold dst_positive_sum_assoc_FGvaluefold dst_negative_sum_assoc_FGvaluefold. (((dc_mask_assoc_FGvalue) = (((((dst_positive_code_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold)) * S ((dst_positive_code_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold)) + ((dst_positive_scale_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold))) + (((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) * S ((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) + ((dst_negative_scale_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)))) * S ((((dst_positive_code_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold)) * S ((dst_positive_code_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold)) + ((dst_positive_scale_assoc_FGvaluefold) + (dst_positive_scale_assoc_FGvaluefold))) + (((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) * S ((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) + ((dst_negative_scale_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)))) + ((((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) * S ((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) + ((dst_negative_scale_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold))) + (((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) * S ((dst_negative_code_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)) + ((dst_negative_scale_assoc_FGvaluefold) + (dst_negative_scale_assoc_FGvaluefold)))))) /\ (((exists fs_u_dst_assoc_FGvaluefoldpositive fs_v_dst_assoc_FGvaluefoldpositive. ((((exists fs_h_dst_assoc_FGvaluefoldpositive_body_start. fs_h_dst_assoc_FGvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_FGvaluefoldpositive)) /\ exists fs_q_dst_assoc_FGvaluefoldpositive_body_start. fs_u_dst_assoc_FGvaluefoldpositive = fs_q_dst_assoc_FGvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_FGvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldpositive_body_terminal. fs_h_dst_assoc_FGvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_FGvaluefold) = S ((S (S (dc_input_assoc_FG))) * fs_v_dst_assoc_FGvaluefoldpositive)) /\ exists fs_q_dst_assoc_FGvaluefoldpositive_body_terminal. fs_u_dst_assoc_FGvaluefoldpositive = fs_q_dst_assoc_FGvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_FG))) * fs_v_dst_assoc_FGvaluefoldpositive) + (dst_positive_sum_assoc_FGvaluefold))) /\ forall fs_i_dst_assoc_FGvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_FGvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_FGvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_FGvaluefoldpositive_body_steps = S (dc_input_assoc_FG)) -> exists fs_a_dst_assoc_FGvaluefoldpositive_body_steps fs_r_dst_assoc_FGvaluefoldpositive_body_steps fs_s_dst_assoc_FGvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_FGvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_FGvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_FGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_FGvaluefold)) /\ exists fs_q_dst_assoc_FGvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_FGvaluefold = fs_q_dst_assoc_FGvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_FGvaluefold) + (fs_a_dst_assoc_FGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_FGvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_FGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * fs_v_dst_assoc_FGvaluefoldpositive)) /\ exists fs_q_dst_assoc_FGvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_FGvaluefoldpositive = fs_q_dst_assoc_FGvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * fs_v_dst_assoc_FGvaluefoldpositive) + (fs_r_dst_assoc_FGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_FGvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_FGvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * fs_v_dst_assoc_FGvaluefoldpositive)) /\ exists fs_q_dst_assoc_FGvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_FGvaluefoldpositive = fs_q_dst_assoc_FGvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_FGvaluefoldpositive_body_steps)) * fs_v_dst_assoc_FGvaluefoldpositive) + (fs_s_dst_assoc_FGvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_FGvaluefoldpositive_body_steps = fs_r_dst_assoc_FGvaluefoldpositive_body_steps + fs_a_dst_assoc_FGvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_FGvaluefoldnegative fs_v_dst_assoc_FGvaluefoldnegative. ((((exists fs_h_dst_assoc_FGvaluefoldnegative_body_start. fs_h_dst_assoc_FGvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_FGvaluefoldnegative)) /\ exists fs_q_dst_assoc_FGvaluefoldnegative_body_start. fs_u_dst_assoc_FGvaluefoldnegative = fs_q_dst_assoc_FGvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_FGvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldnegative_body_terminal. fs_h_dst_assoc_FGvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_FGvaluefold) = S ((S (S (dc_input_assoc_FG))) * fs_v_dst_assoc_FGvaluefoldnegative)) /\ exists fs_q_dst_assoc_FGvaluefoldnegative_body_terminal. fs_u_dst_assoc_FGvaluefoldnegative = fs_q_dst_assoc_FGvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_FG))) * fs_v_dst_assoc_FGvaluefoldnegative) + (dst_negative_sum_assoc_FGvaluefold))) /\ forall fs_i_dst_assoc_FGvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_FGvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_FGvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_FGvaluefoldnegative_body_steps = S (dc_input_assoc_FG)) -> exists fs_a_dst_assoc_FGvaluefoldnegative_body_steps fs_r_dst_assoc_FGvaluefoldnegative_body_steps fs_s_dst_assoc_FGvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_FGvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_FGvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_FGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_FGvaluefold)) /\ exists fs_q_dst_assoc_FGvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_FGvaluefold = fs_q_dst_assoc_FGvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_FGvaluefold) + (fs_a_dst_assoc_FGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_FGvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_FGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * fs_v_dst_assoc_FGvaluefoldnegative)) /\ exists fs_q_dst_assoc_FGvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_FGvaluefoldnegative = fs_q_dst_assoc_FGvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * fs_v_dst_assoc_FGvaluefoldnegative) + (fs_r_dst_assoc_FGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_FGvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_FGvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_FGvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * fs_v_dst_assoc_FGvaluefoldnegative)) /\ exists fs_q_dst_assoc_FGvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_FGvaluefoldnegative = fs_q_dst_assoc_FGvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_FGvaluefoldnegative_body_steps)) * fs_v_dst_assoc_FGvaluefoldnegative) + (fs_s_dst_assoc_FGvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_FGvaluefoldnegative_body_steps = fs_r_dst_assoc_FGvaluefoldnegative_body_steps + fs_a_dst_assoc_FGvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_FGvaluefoldresult ge_balance_negative_assoc_FGvaluefoldresult. (((((dc_output_assoc_FG) = 2 * (ge_balance_positive_assoc_FGvaluefoldresult) /\ (ge_balance_negative_assoc_FGvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_FGvaluefoldresultdecode. (((dc_output_assoc_FG) = 2 * ge_signed_half_assoc_FGvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_FGvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_FGvaluefoldresult) = S ge_signed_half_assoc_FGvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_FGvaluefold) + ge_balance_negative_assoc_FGvaluefoldresult = (dst_negative_sum_assoc_FGvaluefold) + ge_balance_positive_assoc_FGvaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_assoc_GHleft dst_positive_scale_assoc_GHleft dst_negative_code_assoc_GHleft dst_negative_scale_assoc_GHleft. (((G) = (((((dst_positive_code_assoc_GHleft) + (dst_positive_scale_assoc_GHleft)) * S ((dst_positive_code_assoc_GHleft) + (dst_positive_scale_assoc_GHleft)) + ((dst_positive_scale_assoc_GHleft) + (dst_positive_scale_assoc_GHleft))) + (((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) * S ((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) + ((dst_negative_scale_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)))) * S ((((dst_positive_code_assoc_GHleft) + (dst_positive_scale_assoc_GHleft)) * S ((dst_positive_code_assoc_GHleft) + (dst_positive_scale_assoc_GHleft)) + ((dst_positive_scale_assoc_GHleft) + (dst_positive_scale_assoc_GHleft))) + (((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) * S ((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) + ((dst_negative_scale_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)))) + ((((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) * S ((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) + ((dst_negative_scale_assoc_GHleft) + (dst_negative_scale_assoc_GHleft))) + (((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) * S ((dst_negative_code_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)) + ((dst_negative_scale_assoc_GHleft) + (dst_negative_scale_assoc_GHleft)))))) /\ (forall dst_index_assoc_GHleft. (exists pvs_le_gap_assoc_GHleftdomain. pvs_le_gap_assoc_GHleftdomain + (dst_index_assoc_GHleft) = (N)) -> exists dst_positive_assoc_GHleft dst_negative_assoc_GHleft dst_value_assoc_GHleft. ((((exists ff_h_pvs_assoc_GHleftentrypositive. ff_h_pvs_assoc_GHleftentrypositive + S (dst_positive_assoc_GHleft) = S ((S (dst_index_assoc_GHleft)) * dst_positive_scale_assoc_GHleft)) /\ exists ff_q_pvs_assoc_GHleftentrypositive. dst_positive_code_assoc_GHleft = ff_q_pvs_assoc_GHleftentrypositive * S ((S (dst_index_assoc_GHleft)) * dst_positive_scale_assoc_GHleft) + (dst_positive_assoc_GHleft))) /\ (((((exists ff_h_pvs_assoc_GHleftentrynegative. ff_h_pvs_assoc_GHleftentrynegative + S (dst_negative_assoc_GHleft) = S ((S (dst_index_assoc_GHleft)) * dst_negative_scale_assoc_GHleft)) /\ exists ff_q_pvs_assoc_GHleftentrynegative. dst_negative_code_assoc_GHleft = ff_q_pvs_assoc_GHleftentrynegative * S ((S (dst_index_assoc_GHleft)) * dst_negative_scale_assoc_GHleft) + (dst_negative_assoc_GHleft))) /\ (exists ge_balance_positive_assoc_GHleftentryvalue ge_balance_negative_assoc_GHleftentryvalue. (((((dst_value_assoc_GHleft) = 2 * (ge_balance_positive_assoc_GHleftentryvalue) /\ (ge_balance_negative_assoc_GHleftentryvalue) = 0) \/ exists ge_signed_half_assoc_GHleftentryvaluedecode. (((dst_value_assoc_GHleft) = 2 * ge_signed_half_assoc_GHleftentryvaluedecode + 1 /\ (ge_balance_positive_assoc_GHleftentryvalue) = 0) /\ (ge_balance_negative_assoc_GHleftentryvalue) = S ge_signed_half_assoc_GHleftentryvaluedecode))) /\ ((dst_positive_assoc_GHleft) + ge_balance_negative_assoc_GHleftentryvalue = (dst_negative_assoc_GHleft) + ge_balance_positive_assoc_GHleftentryvalue))))))))) /\ (((exists dst_positive_code_assoc_GHright dst_positive_scale_assoc_GHright dst_negative_code_assoc_GHright dst_negative_scale_assoc_GHright. (((H) = (((((dst_positive_code_assoc_GHright) + (dst_positive_scale_assoc_GHright)) * S ((dst_positive_code_assoc_GHright) + (dst_positive_scale_assoc_GHright)) + ((dst_positive_scale_assoc_GHright) + (dst_positive_scale_assoc_GHright))) + (((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) * S ((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) + ((dst_negative_scale_assoc_GHright) + (dst_negative_scale_assoc_GHright)))) * S ((((dst_positive_code_assoc_GHright) + (dst_positive_scale_assoc_GHright)) * S ((dst_positive_code_assoc_GHright) + (dst_positive_scale_assoc_GHright)) + ((dst_positive_scale_assoc_GHright) + (dst_positive_scale_assoc_GHright))) + (((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) * S ((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) + ((dst_negative_scale_assoc_GHright) + (dst_negative_scale_assoc_GHright)))) + ((((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) * S ((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) + ((dst_negative_scale_assoc_GHright) + (dst_negative_scale_assoc_GHright))) + (((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) * S ((dst_negative_code_assoc_GHright) + (dst_negative_scale_assoc_GHright)) + ((dst_negative_scale_assoc_GHright) + (dst_negative_scale_assoc_GHright)))))) /\ (forall dst_index_assoc_GHright. (exists pvs_le_gap_assoc_GHrightdomain. pvs_le_gap_assoc_GHrightdomain + (dst_index_assoc_GHright) = (N)) -> exists dst_positive_assoc_GHright dst_negative_assoc_GHright dst_value_assoc_GHright. ((((exists ff_h_pvs_assoc_GHrightentrypositive. ff_h_pvs_assoc_GHrightentrypositive + S (dst_positive_assoc_GHright) = S ((S (dst_index_assoc_GHright)) * dst_positive_scale_assoc_GHright)) /\ exists ff_q_pvs_assoc_GHrightentrypositive. dst_positive_code_assoc_GHright = ff_q_pvs_assoc_GHrightentrypositive * S ((S (dst_index_assoc_GHright)) * dst_positive_scale_assoc_GHright) + (dst_positive_assoc_GHright))) /\ (((((exists ff_h_pvs_assoc_GHrightentrynegative. ff_h_pvs_assoc_GHrightentrynegative + S (dst_negative_assoc_GHright) = S ((S (dst_index_assoc_GHright)) * dst_negative_scale_assoc_GHright)) /\ exists ff_q_pvs_assoc_GHrightentrynegative. dst_negative_code_assoc_GHright = ff_q_pvs_assoc_GHrightentrynegative * S ((S (dst_index_assoc_GHright)) * dst_negative_scale_assoc_GHright) + (dst_negative_assoc_GHright))) /\ (exists ge_balance_positive_assoc_GHrightentryvalue ge_balance_negative_assoc_GHrightentryvalue. (((((dst_value_assoc_GHright) = 2 * (ge_balance_positive_assoc_GHrightentryvalue) /\ (ge_balance_negative_assoc_GHrightentryvalue) = 0) \/ exists ge_signed_half_assoc_GHrightentryvaluedecode. (((dst_value_assoc_GHright) = 2 * ge_signed_half_assoc_GHrightentryvaluedecode + 1 /\ (ge_balance_positive_assoc_GHrightentryvalue) = 0) /\ (ge_balance_negative_assoc_GHrightentryvalue) = S ge_signed_half_assoc_GHrightentryvaluedecode))) /\ ((dst_positive_assoc_GHright) + ge_balance_negative_assoc_GHrightentryvalue = (dst_negative_assoc_GHright) + ge_balance_positive_assoc_GHrightentryvalue))))))))) /\ (((exists dst_positive_code_assoc_GHtable dst_positive_scale_assoc_GHtable dst_negative_code_assoc_GHtable dst_negative_scale_assoc_GHtable. (((B) = (((((dst_positive_code_assoc_GHtable) + (dst_positive_scale_assoc_GHtable)) * S ((dst_positive_code_assoc_GHtable) + (dst_positive_scale_assoc_GHtable)) + ((dst_positive_scale_assoc_GHtable) + (dst_positive_scale_assoc_GHtable))) + (((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) * S ((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) + ((dst_negative_scale_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)))) * S ((((dst_positive_code_assoc_GHtable) + (dst_positive_scale_assoc_GHtable)) * S ((dst_positive_code_assoc_GHtable) + (dst_positive_scale_assoc_GHtable)) + ((dst_positive_scale_assoc_GHtable) + (dst_positive_scale_assoc_GHtable))) + (((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) * S ((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) + ((dst_negative_scale_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)))) + ((((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) * S ((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) + ((dst_negative_scale_assoc_GHtable) + (dst_negative_scale_assoc_GHtable))) + (((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) * S ((dst_negative_code_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)) + ((dst_negative_scale_assoc_GHtable) + (dst_negative_scale_assoc_GHtable)))))) /\ (forall dst_index_assoc_GHtable. (exists pvs_le_gap_assoc_GHtabledomain. pvs_le_gap_assoc_GHtabledomain + (dst_index_assoc_GHtable) = (N)) -> exists dst_positive_assoc_GHtable dst_negative_assoc_GHtable dst_value_assoc_GHtable. ((((exists ff_h_pvs_assoc_GHtableentrypositive. ff_h_pvs_assoc_GHtableentrypositive + S (dst_positive_assoc_GHtable) = S ((S (dst_index_assoc_GHtable)) * dst_positive_scale_assoc_GHtable)) /\ exists ff_q_pvs_assoc_GHtableentrypositive. dst_positive_code_assoc_GHtable = ff_q_pvs_assoc_GHtableentrypositive * S ((S (dst_index_assoc_GHtable)) * dst_positive_scale_assoc_GHtable) + (dst_positive_assoc_GHtable))) /\ (((((exists ff_h_pvs_assoc_GHtableentrynegative. ff_h_pvs_assoc_GHtableentrynegative + S (dst_negative_assoc_GHtable) = S ((S (dst_index_assoc_GHtable)) * dst_negative_scale_assoc_GHtable)) /\ exists ff_q_pvs_assoc_GHtableentrynegative. dst_negative_code_assoc_GHtable = ff_q_pvs_assoc_GHtableentrynegative * S ((S (dst_index_assoc_GHtable)) * dst_negative_scale_assoc_GHtable) + (dst_negative_assoc_GHtable))) /\ (exists ge_balance_positive_assoc_GHtableentryvalue ge_balance_negative_assoc_GHtableentryvalue. (((((dst_value_assoc_GHtable) = 2 * (ge_balance_positive_assoc_GHtableentryvalue) /\ (ge_balance_negative_assoc_GHtableentryvalue) = 0) \/ exists ge_signed_half_assoc_GHtableentryvaluedecode. (((dst_value_assoc_GHtable) = 2 * ge_signed_half_assoc_GHtableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_GHtableentryvalue) = 0) /\ (ge_balance_negative_assoc_GHtableentryvalue) = S ge_signed_half_assoc_GHtableentryvaluedecode))) /\ ((dst_positive_assoc_GHtable) + ge_balance_negative_assoc_GHtableentryvalue = (dst_negative_assoc_GHtable) + ge_balance_positive_assoc_GHtableentryvalue))))))))) /\ (forall dc_input_assoc_GH dc_output_assoc_GH. ~(dc_input_assoc_GH=0) -> (exists pvs_le_gap_assoc_GHdomain. pvs_le_gap_assoc_GHdomain + (dc_input_assoc_GH) = (N)) -> (exists dst_positive_code_assoc_GHlookup dst_positive_scale_assoc_GHlookup dst_negative_code_assoc_GHlookup dst_negative_scale_assoc_GHlookup dst_positive_assoc_GHlookup dst_negative_assoc_GHlookup. (((B) = (((((dst_positive_code_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup)) * S ((dst_positive_code_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup)) + ((dst_positive_scale_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup))) + (((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) * S ((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) + ((dst_negative_scale_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)))) * S ((((dst_positive_code_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup)) * S ((dst_positive_code_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup)) + ((dst_positive_scale_assoc_GHlookup) + (dst_positive_scale_assoc_GHlookup))) + (((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) * S ((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) + ((dst_negative_scale_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)))) + ((((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) * S ((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) + ((dst_negative_scale_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup))) + (((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) * S ((dst_negative_code_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)) + ((dst_negative_scale_assoc_GHlookup) + (dst_negative_scale_assoc_GHlookup)))))) /\ (((((exists ff_h_pvs_assoc_GHlookuppositive. ff_h_pvs_assoc_GHlookuppositive + S (dst_positive_assoc_GHlookup) = S ((S (dc_input_assoc_GH)) * dst_positive_scale_assoc_GHlookup)) /\ exists ff_q_pvs_assoc_GHlookuppositive. dst_positive_code_assoc_GHlookup = ff_q_pvs_assoc_GHlookuppositive * S ((S (dc_input_assoc_GH)) * dst_positive_scale_assoc_GHlookup) + (dst_positive_assoc_GHlookup))) /\ (((((exists ff_h_pvs_assoc_GHlookupnegative. ff_h_pvs_assoc_GHlookupnegative + S (dst_negative_assoc_GHlookup) = S ((S (dc_input_assoc_GH)) * dst_negative_scale_assoc_GHlookup)) /\ exists ff_q_pvs_assoc_GHlookupnegative. dst_negative_code_assoc_GHlookup = ff_q_pvs_assoc_GHlookupnegative * S ((S (dc_input_assoc_GH)) * dst_negative_scale_assoc_GHlookup) + (dst_negative_assoc_GHlookup))) /\ (exists ge_balance_positive_assoc_GHlookupvalue ge_balance_negative_assoc_GHlookupvalue. (((((dc_output_assoc_GH) = 2 * (ge_balance_positive_assoc_GHlookupvalue) /\ (ge_balance_negative_assoc_GHlookupvalue) = 0) \/ exists ge_signed_half_assoc_GHlookupvaluedecode. (((dc_output_assoc_GH) = 2 * ge_signed_half_assoc_GHlookupvaluedecode + 1 /\ (ge_balance_positive_assoc_GHlookupvalue) = 0) /\ (ge_balance_negative_assoc_GHlookupvalue) = S ge_signed_half_assoc_GHlookupvaluedecode))) /\ ((dst_positive_assoc_GHlookup) + ge_balance_negative_assoc_GHlookupvalue = (dst_negative_assoc_GHlookup) + ge_balance_positive_assoc_GHlookupvalue))))))))) -> (((~((dc_input_assoc_GH)=0)) /\ (exists dc_mask_assoc_GHvalue. ((((exists dst_positive_code_assoc_GHvaluemasktable dst_positive_scale_assoc_GHvaluemasktable dst_negative_code_assoc_GHvaluemasktable dst_negative_scale_assoc_GHvaluemasktable. (((dc_mask_assoc_GHvalue) = (((((dst_positive_code_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable)) * S ((dst_positive_code_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable)) + ((dst_positive_scale_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable))) + (((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) * S ((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) + ((dst_negative_scale_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)))) * S ((((dst_positive_code_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable)) * S ((dst_positive_code_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable)) + ((dst_positive_scale_assoc_GHvaluemasktable) + (dst_positive_scale_assoc_GHvaluemasktable))) + (((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) * S ((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) + ((dst_negative_scale_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)))) + ((((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) * S ((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) + ((dst_negative_scale_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable))) + (((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) * S ((dst_negative_code_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)) + ((dst_negative_scale_assoc_GHvaluemasktable) + (dst_negative_scale_assoc_GHvaluemasktable)))))) /\ (forall dst_index_assoc_GHvaluemasktable. (exists pvs_le_gap_assoc_GHvaluemasktabledomain. pvs_le_gap_assoc_GHvaluemasktabledomain + (dst_index_assoc_GHvaluemasktable) = (dc_input_assoc_GH)) -> exists dst_positive_assoc_GHvaluemasktable dst_negative_assoc_GHvaluemasktable dst_value_assoc_GHvaluemasktable. ((((exists ff_h_pvs_assoc_GHvaluemasktableentrypositive. ff_h_pvs_assoc_GHvaluemasktableentrypositive + S (dst_positive_assoc_GHvaluemasktable) = S ((S (dst_index_assoc_GHvaluemasktable)) * dst_positive_scale_assoc_GHvaluemasktable)) /\ exists ff_q_pvs_assoc_GHvaluemasktableentrypositive. dst_positive_code_assoc_GHvaluemasktable = ff_q_pvs_assoc_GHvaluemasktableentrypositive * S ((S (dst_index_assoc_GHvaluemasktable)) * dst_positive_scale_assoc_GHvaluemasktable) + (dst_positive_assoc_GHvaluemasktable))) /\ (((((exists ff_h_pvs_assoc_GHvaluemasktableentrynegative. ff_h_pvs_assoc_GHvaluemasktableentrynegative + S (dst_negative_assoc_GHvaluemasktable) = S ((S (dst_index_assoc_GHvaluemasktable)) * dst_negative_scale_assoc_GHvaluemasktable)) /\ exists ff_q_pvs_assoc_GHvaluemasktableentrynegative. dst_negative_code_assoc_GHvaluemasktable = ff_q_pvs_assoc_GHvaluemasktableentrynegative * S ((S (dst_index_assoc_GHvaluemasktable)) * dst_negative_scale_assoc_GHvaluemasktable) + (dst_negative_assoc_GHvaluemasktable))) /\ (exists ge_balance_positive_assoc_GHvaluemasktableentryvalue ge_balance_negative_assoc_GHvaluemasktableentryvalue. (((((dst_value_assoc_GHvaluemasktable) = 2 * (ge_balance_positive_assoc_GHvaluemasktableentryvalue) /\ (ge_balance_negative_assoc_GHvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_GHvaluemasktableentryvaluedecode. (((dst_value_assoc_GHvaluemasktable) = 2 * ge_signed_half_assoc_GHvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_GHvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_GHvaluemasktableentryvalue) = S ge_signed_half_assoc_GHvaluemasktableentryvaluedecode))) /\ ((dst_positive_assoc_GHvaluemasktable) + ge_balance_negative_assoc_GHvaluemasktableentryvalue = (dst_negative_assoc_GHvaluemasktable) + ge_balance_positive_assoc_GHvaluemasktableentryvalue))))))))) /\ (forall dc_index_assoc_GHvaluemask dc_value_assoc_GHvaluemask. (exists pvs_le_gap_assoc_GHvaluemaskdomain. pvs_le_gap_assoc_GHvaluemaskdomain + (dc_index_assoc_GHvaluemask) = (dc_input_assoc_GH)) -> (exists dst_positive_code_assoc_GHvaluemasklookup dst_positive_scale_assoc_GHvaluemasklookup dst_negative_code_assoc_GHvaluemasklookup dst_negative_scale_assoc_GHvaluemasklookup dst_positive_assoc_GHvaluemasklookup dst_negative_assoc_GHvaluemasklookup. (((dc_mask_assoc_GHvalue) = (((((dst_positive_code_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup)) * S ((dst_positive_code_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup)) + ((dst_positive_scale_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup))) + (((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) * S ((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) + ((dst_negative_scale_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)))) * S ((((dst_positive_code_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup)) * S ((dst_positive_code_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup)) + ((dst_positive_scale_assoc_GHvaluemasklookup) + (dst_positive_scale_assoc_GHvaluemasklookup))) + (((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) * S ((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) + ((dst_negative_scale_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)))) + ((((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) * S ((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) + ((dst_negative_scale_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup))) + (((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) * S ((dst_negative_code_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)) + ((dst_negative_scale_assoc_GHvaluemasklookup) + (dst_negative_scale_assoc_GHvaluemasklookup)))))) /\ (((((exists ff_h_pvs_assoc_GHvaluemasklookuppositive. ff_h_pvs_assoc_GHvaluemasklookuppositive + S (dst_positive_assoc_GHvaluemasklookup) = S ((S (dc_index_assoc_GHvaluemask)) * dst_positive_scale_assoc_GHvaluemasklookup)) /\ exists ff_q_pvs_assoc_GHvaluemasklookuppositive. dst_positive_code_assoc_GHvaluemasklookup = ff_q_pvs_assoc_GHvaluemasklookuppositive * S ((S (dc_index_assoc_GHvaluemask)) * dst_positive_scale_assoc_GHvaluemasklookup) + (dst_positive_assoc_GHvaluemasklookup))) /\ (((((exists ff_h_pvs_assoc_GHvaluemasklookupnegative. ff_h_pvs_assoc_GHvaluemasklookupnegative + S (dst_negative_assoc_GHvaluemasklookup) = S ((S (dc_index_assoc_GHvaluemask)) * dst_negative_scale_assoc_GHvaluemasklookup)) /\ exists ff_q_pvs_assoc_GHvaluemasklookupnegative. dst_negative_code_assoc_GHvaluemasklookup = ff_q_pvs_assoc_GHvaluemasklookupnegative * S ((S (dc_index_assoc_GHvaluemask)) * dst_negative_scale_assoc_GHvaluemasklookup) + (dst_negative_assoc_GHvaluemasklookup))) /\ (exists ge_balance_positive_assoc_GHvaluemasklookupvalue ge_balance_negative_assoc_GHvaluemasklookupvalue. (((((dc_value_assoc_GHvaluemask) = 2 * (ge_balance_positive_assoc_GHvaluemasklookupvalue) /\ (ge_balance_negative_assoc_GHvaluemasklookupvalue) = 0) \/ exists ge_signed_half_assoc_GHvaluemasklookupvaluedecode. (((dc_value_assoc_GHvaluemask) = 2 * ge_signed_half_assoc_GHvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_GHvaluemasklookupvalue) = 0) /\ (ge_balance_negative_assoc_GHvaluemasklookupvalue) = S ge_signed_half_assoc_GHvaluemasklookupvaluedecode))) /\ ((dst_positive_assoc_GHvaluemasklookup) + ge_balance_negative_assoc_GHvaluemasklookupvalue = (dst_negative_assoc_GHvaluemasklookup) + ge_balance_positive_assoc_GHvaluemasklookupvalue))))))))) -> ((((~((dc_index_assoc_GHvaluemask)=0)) /\ (exists dc_quotient_assoc_GHvaluemaskentry dc_left_assoc_GHvaluemaskentry dc_right_assoc_GHvaluemaskentry. (((dc_input_assoc_GH)=(dc_index_assoc_GHvaluemask)*dc_quotient_assoc_GHvaluemaskentry) /\ (((exists dst_positive_code_assoc_GHvaluemaskentryleft dst_positive_scale_assoc_GHvaluemaskentryleft dst_negative_code_assoc_GHvaluemaskentryleft dst_negative_scale_assoc_GHvaluemaskentryleft dst_positive_assoc_GHvaluemaskentryleft dst_negative_assoc_GHvaluemaskentryleft. (((G) = (((((dst_positive_code_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft)) * S ((dst_positive_code_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft)) + ((dst_positive_scale_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft))) + (((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) * S ((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) + ((dst_negative_scale_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)))) * S ((((dst_positive_code_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft)) * S ((dst_positive_code_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft)) + ((dst_positive_scale_assoc_GHvaluemaskentryleft) + (dst_positive_scale_assoc_GHvaluemaskentryleft))) + (((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) * S ((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) + ((dst_negative_scale_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)))) + ((((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) * S ((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) + ((dst_negative_scale_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft))) + (((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) * S ((dst_negative_code_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)) + ((dst_negative_scale_assoc_GHvaluemaskentryleft) + (dst_negative_scale_assoc_GHvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_GHvaluemaskentryleftpositive. ff_h_pvs_assoc_GHvaluemaskentryleftpositive + S (dst_positive_assoc_GHvaluemaskentryleft) = S ((S (dc_index_assoc_GHvaluemask)) * dst_positive_scale_assoc_GHvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_GHvaluemaskentryleftpositive. dst_positive_code_assoc_GHvaluemaskentryleft = ff_q_pvs_assoc_GHvaluemaskentryleftpositive * S ((S (dc_index_assoc_GHvaluemask)) * dst_positive_scale_assoc_GHvaluemaskentryleft) + (dst_positive_assoc_GHvaluemaskentryleft))) /\ (((((exists ff_h_pvs_assoc_GHvaluemaskentryleftnegative. ff_h_pvs_assoc_GHvaluemaskentryleftnegative + S (dst_negative_assoc_GHvaluemaskentryleft) = S ((S (dc_index_assoc_GHvaluemask)) * dst_negative_scale_assoc_GHvaluemaskentryleft)) /\ exists ff_q_pvs_assoc_GHvaluemaskentryleftnegative. dst_negative_code_assoc_GHvaluemaskentryleft = ff_q_pvs_assoc_GHvaluemaskentryleftnegative * S ((S (dc_index_assoc_GHvaluemask)) * dst_negative_scale_assoc_GHvaluemaskentryleft) + (dst_negative_assoc_GHvaluemaskentryleft))) /\ (exists ge_balance_positive_assoc_GHvaluemaskentryleftvalue ge_balance_negative_assoc_GHvaluemaskentryleftvalue. (((((dc_left_assoc_GHvaluemaskentry) = 2 * (ge_balance_positive_assoc_GHvaluemaskentryleftvalue) /\ (ge_balance_negative_assoc_GHvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_GHvaluemaskentryleftvaluedecode. (((dc_left_assoc_GHvaluemaskentry) = 2 * ge_signed_half_assoc_GHvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_GHvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_GHvaluemaskentryleftvalue) = S ge_signed_half_assoc_GHvaluemaskentryleftvaluedecode))) /\ ((dst_positive_assoc_GHvaluemaskentryleft) + ge_balance_negative_assoc_GHvaluemaskentryleftvalue = (dst_negative_assoc_GHvaluemaskentryleft) + ge_balance_positive_assoc_GHvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_GHvaluemaskentryright dst_positive_scale_assoc_GHvaluemaskentryright dst_negative_code_assoc_GHvaluemaskentryright dst_negative_scale_assoc_GHvaluemaskentryright dst_positive_assoc_GHvaluemaskentryright dst_negative_assoc_GHvaluemaskentryright. (((H) = (((((dst_positive_code_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright)) * S ((dst_positive_code_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright)) + ((dst_positive_scale_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright))) + (((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) * S ((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) + ((dst_negative_scale_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)))) * S ((((dst_positive_code_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright)) * S ((dst_positive_code_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright)) + ((dst_positive_scale_assoc_GHvaluemaskentryright) + (dst_positive_scale_assoc_GHvaluemaskentryright))) + (((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) * S ((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) + ((dst_negative_scale_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)))) + ((((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) * S ((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) + ((dst_negative_scale_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright))) + (((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) * S ((dst_negative_code_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)) + ((dst_negative_scale_assoc_GHvaluemaskentryright) + (dst_negative_scale_assoc_GHvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_GHvaluemaskentryrightpositive. ff_h_pvs_assoc_GHvaluemaskentryrightpositive + S (dst_positive_assoc_GHvaluemaskentryright) = S ((S (dc_quotient_assoc_GHvaluemaskentry)) * dst_positive_scale_assoc_GHvaluemaskentryright)) /\ exists ff_q_pvs_assoc_GHvaluemaskentryrightpositive. dst_positive_code_assoc_GHvaluemaskentryright = ff_q_pvs_assoc_GHvaluemaskentryrightpositive * S ((S (dc_quotient_assoc_GHvaluemaskentry)) * dst_positive_scale_assoc_GHvaluemaskentryright) + (dst_positive_assoc_GHvaluemaskentryright))) /\ (((((exists ff_h_pvs_assoc_GHvaluemaskentryrightnegative. ff_h_pvs_assoc_GHvaluemaskentryrightnegative + S (dst_negative_assoc_GHvaluemaskentryright) = S ((S (dc_quotient_assoc_GHvaluemaskentry)) * dst_negative_scale_assoc_GHvaluemaskentryright)) /\ exists ff_q_pvs_assoc_GHvaluemaskentryrightnegative. dst_negative_code_assoc_GHvaluemaskentryright = ff_q_pvs_assoc_GHvaluemaskentryrightnegative * S ((S (dc_quotient_assoc_GHvaluemaskentry)) * dst_negative_scale_assoc_GHvaluemaskentryright) + (dst_negative_assoc_GHvaluemaskentryright))) /\ (exists ge_balance_positive_assoc_GHvaluemaskentryrightvalue ge_balance_negative_assoc_GHvaluemaskentryrightvalue. (((((dc_right_assoc_GHvaluemaskentry) = 2 * (ge_balance_positive_assoc_GHvaluemaskentryrightvalue) /\ (ge_balance_negative_assoc_GHvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_GHvaluemaskentryrightvaluedecode. (((dc_right_assoc_GHvaluemaskentry) = 2 * ge_signed_half_assoc_GHvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_GHvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_GHvaluemaskentryrightvalue) = S ge_signed_half_assoc_GHvaluemaskentryrightvaluedecode))) /\ ((dst_positive_assoc_GHvaluemaskentryright) + ge_balance_negative_assoc_GHvaluemaskentryrightvalue = (dst_negative_assoc_GHvaluemaskentryright) + ge_balance_positive_assoc_GHvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_GHvaluemaskentryproduct sto_an_assoc_GHvaluemaskentryproduct sto_bp_assoc_GHvaluemaskentryproduct sto_bn_assoc_GHvaluemaskentryproduct sto_cp_assoc_GHvaluemaskentryproduct sto_cn_assoc_GHvaluemaskentryproduct. (((((dc_left_assoc_GHvaluemaskentry) = 2 * (sto_ap_assoc_GHvaluemaskentryproduct) /\ (sto_an_assoc_GHvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_GHvaluemaskentryproductleft. (((dc_left_assoc_GHvaluemaskentry) = 2 * ge_signed_half_assoc_GHvaluemaskentryproductleft + 1 /\ (sto_ap_assoc_GHvaluemaskentryproduct) = 0) /\ (sto_an_assoc_GHvaluemaskentryproduct) = S ge_signed_half_assoc_GHvaluemaskentryproductleft))) /\ ((((((dc_right_assoc_GHvaluemaskentry) = 2 * (sto_bp_assoc_GHvaluemaskentryproduct) /\ (sto_bn_assoc_GHvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_GHvaluemaskentryproductright. (((dc_right_assoc_GHvaluemaskentry) = 2 * ge_signed_half_assoc_GHvaluemaskentryproductright + 1 /\ (sto_bp_assoc_GHvaluemaskentryproduct) = 0) /\ (sto_bn_assoc_GHvaluemaskentryproduct) = S ge_signed_half_assoc_GHvaluemaskentryproductright))) /\ ((((((dc_value_assoc_GHvaluemask) = 2 * (sto_cp_assoc_GHvaluemaskentryproduct) /\ (sto_cn_assoc_GHvaluemaskentryproduct) = 0) \/ exists ge_signed_half_assoc_GHvaluemaskentryproductoutput. (((dc_value_assoc_GHvaluemask) = 2 * ge_signed_half_assoc_GHvaluemaskentryproductoutput + 1 /\ (sto_cp_assoc_GHvaluemaskentryproduct) = 0) /\ (sto_cn_assoc_GHvaluemaskentryproduct) = S ge_signed_half_assoc_GHvaluemaskentryproductoutput))) /\ ((sto_ap_assoc_GHvaluemaskentryproduct * sto_bp_assoc_GHvaluemaskentryproduct + sto_an_assoc_GHvaluemaskentryproduct * sto_bn_assoc_GHvaluemaskentryproduct) + sto_cn_assoc_GHvaluemaskentryproduct = (sto_ap_assoc_GHvaluemaskentryproduct * sto_bn_assoc_GHvaluemaskentryproduct + sto_an_assoc_GHvaluemaskentryproduct * sto_bp_assoc_GHvaluemaskentryproduct) + sto_cp_assoc_GHvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_GHvaluemask)=0 \/ ~(exists pvs_factor_assoc_GHvaluemaskentrynondivisor. (dc_input_assoc_GH) = (dc_index_assoc_GHvaluemask) * pvs_factor_assoc_GHvaluemaskentrynondivisor)) /\ ((dc_value_assoc_GHvaluemask)=0))))))) /\ (exists dst_positive_code_assoc_GHvaluefold dst_positive_scale_assoc_GHvaluefold dst_negative_code_assoc_GHvaluefold dst_negative_scale_assoc_GHvaluefold dst_positive_sum_assoc_GHvaluefold dst_negative_sum_assoc_GHvaluefold. (((dc_mask_assoc_GHvalue) = (((((dst_positive_code_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold)) * S ((dst_positive_code_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold)) + ((dst_positive_scale_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold))) + (((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) * S ((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) + ((dst_negative_scale_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)))) * S ((((dst_positive_code_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold)) * S ((dst_positive_code_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold)) + ((dst_positive_scale_assoc_GHvaluefold) + (dst_positive_scale_assoc_GHvaluefold))) + (((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) * S ((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) + ((dst_negative_scale_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)))) + ((((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) * S ((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) + ((dst_negative_scale_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold))) + (((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) * S ((dst_negative_code_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)) + ((dst_negative_scale_assoc_GHvaluefold) + (dst_negative_scale_assoc_GHvaluefold)))))) /\ (((exists fs_u_dst_assoc_GHvaluefoldpositive fs_v_dst_assoc_GHvaluefoldpositive. ((((exists fs_h_dst_assoc_GHvaluefoldpositive_body_start. fs_h_dst_assoc_GHvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_GHvaluefoldpositive)) /\ exists fs_q_dst_assoc_GHvaluefoldpositive_body_start. fs_u_dst_assoc_GHvaluefoldpositive = fs_q_dst_assoc_GHvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_GHvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldpositive_body_terminal. fs_h_dst_assoc_GHvaluefoldpositive_body_terminal + S (dst_positive_sum_assoc_GHvaluefold) = S ((S (S (dc_input_assoc_GH))) * fs_v_dst_assoc_GHvaluefoldpositive)) /\ exists fs_q_dst_assoc_GHvaluefoldpositive_body_terminal. fs_u_dst_assoc_GHvaluefoldpositive = fs_q_dst_assoc_GHvaluefoldpositive_body_terminal * S ((S (S (dc_input_assoc_GH))) * fs_v_dst_assoc_GHvaluefoldpositive) + (dst_positive_sum_assoc_GHvaluefold))) /\ forall fs_i_dst_assoc_GHvaluefoldpositive_body_steps. (exists fs_lt_dst_assoc_GHvaluefoldpositive_body_steps_bound. fs_lt_dst_assoc_GHvaluefoldpositive_body_steps_bound + S fs_i_dst_assoc_GHvaluefoldpositive_body_steps = S (dc_input_assoc_GH)) -> exists fs_a_dst_assoc_GHvaluefoldpositive_body_steps fs_r_dst_assoc_GHvaluefoldpositive_body_steps fs_s_dst_assoc_GHvaluefoldpositive_body_steps. ((((exists fs_h_dst_assoc_GHvaluefoldpositive_body_steps_summand. fs_h_dst_assoc_GHvaluefoldpositive_body_steps_summand + S (fs_a_dst_assoc_GHvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_GHvaluefold)) /\ exists fs_q_dst_assoc_GHvaluefoldpositive_body_steps_summand. dst_positive_code_assoc_GHvaluefold = fs_q_dst_assoc_GHvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * dst_positive_scale_assoc_GHvaluefold) + (fs_a_dst_assoc_GHvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldpositive_body_steps_partial. fs_h_dst_assoc_GHvaluefoldpositive_body_steps_partial + S (fs_r_dst_assoc_GHvaluefoldpositive_body_steps) = S ((S (fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * fs_v_dst_assoc_GHvaluefoldpositive)) /\ exists fs_q_dst_assoc_GHvaluefoldpositive_body_steps_partial. fs_u_dst_assoc_GHvaluefoldpositive = fs_q_dst_assoc_GHvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * fs_v_dst_assoc_GHvaluefoldpositive) + (fs_r_dst_assoc_GHvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldpositive_body_steps_successor. fs_h_dst_assoc_GHvaluefoldpositive_body_steps_successor + S (fs_s_dst_assoc_GHvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * fs_v_dst_assoc_GHvaluefoldpositive)) /\ exists fs_q_dst_assoc_GHvaluefoldpositive_body_steps_successor. fs_u_dst_assoc_GHvaluefoldpositive = fs_q_dst_assoc_GHvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_GHvaluefoldpositive_body_steps)) * fs_v_dst_assoc_GHvaluefoldpositive) + (fs_s_dst_assoc_GHvaluefoldpositive_body_steps))) /\ fs_s_dst_assoc_GHvaluefoldpositive_body_steps = fs_r_dst_assoc_GHvaluefoldpositive_body_steps + fs_a_dst_assoc_GHvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_GHvaluefoldnegative fs_v_dst_assoc_GHvaluefoldnegative. ((((exists fs_h_dst_assoc_GHvaluefoldnegative_body_start. fs_h_dst_assoc_GHvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_GHvaluefoldnegative)) /\ exists fs_q_dst_assoc_GHvaluefoldnegative_body_start. fs_u_dst_assoc_GHvaluefoldnegative = fs_q_dst_assoc_GHvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_GHvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldnegative_body_terminal. fs_h_dst_assoc_GHvaluefoldnegative_body_terminal + S (dst_negative_sum_assoc_GHvaluefold) = S ((S (S (dc_input_assoc_GH))) * fs_v_dst_assoc_GHvaluefoldnegative)) /\ exists fs_q_dst_assoc_GHvaluefoldnegative_body_terminal. fs_u_dst_assoc_GHvaluefoldnegative = fs_q_dst_assoc_GHvaluefoldnegative_body_terminal * S ((S (S (dc_input_assoc_GH))) * fs_v_dst_assoc_GHvaluefoldnegative) + (dst_negative_sum_assoc_GHvaluefold))) /\ forall fs_i_dst_assoc_GHvaluefoldnegative_body_steps. (exists fs_lt_dst_assoc_GHvaluefoldnegative_body_steps_bound. fs_lt_dst_assoc_GHvaluefoldnegative_body_steps_bound + S fs_i_dst_assoc_GHvaluefoldnegative_body_steps = S (dc_input_assoc_GH)) -> exists fs_a_dst_assoc_GHvaluefoldnegative_body_steps fs_r_dst_assoc_GHvaluefoldnegative_body_steps fs_s_dst_assoc_GHvaluefoldnegative_body_steps. ((((exists fs_h_dst_assoc_GHvaluefoldnegative_body_steps_summand. fs_h_dst_assoc_GHvaluefoldnegative_body_steps_summand + S (fs_a_dst_assoc_GHvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_GHvaluefold)) /\ exists fs_q_dst_assoc_GHvaluefoldnegative_body_steps_summand. dst_negative_code_assoc_GHvaluefold = fs_q_dst_assoc_GHvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * dst_negative_scale_assoc_GHvaluefold) + (fs_a_dst_assoc_GHvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldnegative_body_steps_partial. fs_h_dst_assoc_GHvaluefoldnegative_body_steps_partial + S (fs_r_dst_assoc_GHvaluefoldnegative_body_steps) = S ((S (fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * fs_v_dst_assoc_GHvaluefoldnegative)) /\ exists fs_q_dst_assoc_GHvaluefoldnegative_body_steps_partial. fs_u_dst_assoc_GHvaluefoldnegative = fs_q_dst_assoc_GHvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * fs_v_dst_assoc_GHvaluefoldnegative) + (fs_r_dst_assoc_GHvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_GHvaluefoldnegative_body_steps_successor. fs_h_dst_assoc_GHvaluefoldnegative_body_steps_successor + S (fs_s_dst_assoc_GHvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * fs_v_dst_assoc_GHvaluefoldnegative)) /\ exists fs_q_dst_assoc_GHvaluefoldnegative_body_steps_successor. fs_u_dst_assoc_GHvaluefoldnegative = fs_q_dst_assoc_GHvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_GHvaluefoldnegative_body_steps)) * fs_v_dst_assoc_GHvaluefoldnegative) + (fs_s_dst_assoc_GHvaluefoldnegative_body_steps))) /\ fs_s_dst_assoc_GHvaluefoldnegative_body_steps = fs_r_dst_assoc_GHvaluefoldnegative_body_steps + fs_a_dst_assoc_GHvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_GHvaluefoldresult ge_balance_negative_assoc_GHvaluefoldresult. (((((dc_output_assoc_GH) = 2 * (ge_balance_positive_assoc_GHvaluefoldresult) /\ (ge_balance_negative_assoc_GHvaluefoldresult) = 0) \/ exists ge_signed_half_assoc_GHvaluefoldresultdecode. (((dc_output_assoc_GH) = 2 * ge_signed_half_assoc_GHvaluefoldresultdecode + 1 /\ (ge_balance_positive_assoc_GHvaluefoldresult) = 0) /\ (ge_balance_negative_assoc_GHvaluefoldresult) = S ge_signed_half_assoc_GHvaluefoldresultdecode))) /\ ((dst_positive_sum_assoc_GHvaluefold) + ge_balance_negative_assoc_GHvaluefoldresult = (dst_negative_sum_assoc_GHvaluefold) + ge_balance_positive_assoc_GHvaluefoldresult)))))))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_assoc_domain. pvs_le_gap_assoc_domain + (n) = (N)) -> (((~((n)=0)) /\ (exists dc_mask_assoc_left. ((((exists dst_positive_code_assoc_leftmasktable dst_positive_scale_assoc_leftmasktable dst_negative_code_assoc_leftmasktable dst_negative_scale_assoc_leftmasktable. (((dc_mask_assoc_left) = (((((dst_positive_code_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable)) * S ((dst_positive_code_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable)) + ((dst_positive_scale_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable))) + (((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) * S ((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) + ((dst_negative_scale_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)))) * S ((((dst_positive_code_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable)) * S ((dst_positive_code_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable)) + ((dst_positive_scale_assoc_leftmasktable) + (dst_positive_scale_assoc_leftmasktable))) + (((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) * S ((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) + ((dst_negative_scale_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)))) + ((((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) * S ((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) + ((dst_negative_scale_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable))) + (((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) * S ((dst_negative_code_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)) + ((dst_negative_scale_assoc_leftmasktable) + (dst_negative_scale_assoc_leftmasktable)))))) /\ (forall dst_index_assoc_leftmasktable. (exists pvs_le_gap_assoc_leftmasktabledomain. pvs_le_gap_assoc_leftmasktabledomain + (dst_index_assoc_leftmasktable) = (n)) -> exists dst_positive_assoc_leftmasktable dst_negative_assoc_leftmasktable dst_value_assoc_leftmasktable. ((((exists ff_h_pvs_assoc_leftmasktableentrypositive. ff_h_pvs_assoc_leftmasktableentrypositive + S (dst_positive_assoc_leftmasktable) = S ((S (dst_index_assoc_leftmasktable)) * dst_positive_scale_assoc_leftmasktable)) /\ exists ff_q_pvs_assoc_leftmasktableentrypositive. dst_positive_code_assoc_leftmasktable = ff_q_pvs_assoc_leftmasktableentrypositive * S ((S (dst_index_assoc_leftmasktable)) * dst_positive_scale_assoc_leftmasktable) + (dst_positive_assoc_leftmasktable))) /\ (((((exists ff_h_pvs_assoc_leftmasktableentrynegative. ff_h_pvs_assoc_leftmasktableentrynegative + S (dst_negative_assoc_leftmasktable) = S ((S (dst_index_assoc_leftmasktable)) * dst_negative_scale_assoc_leftmasktable)) /\ exists ff_q_pvs_assoc_leftmasktableentrynegative. dst_negative_code_assoc_leftmasktable = ff_q_pvs_assoc_leftmasktableentrynegative * S ((S (dst_index_assoc_leftmasktable)) * dst_negative_scale_assoc_leftmasktable) + (dst_negative_assoc_leftmasktable))) /\ (exists ge_balance_positive_assoc_leftmasktableentryvalue ge_balance_negative_assoc_leftmasktableentryvalue. (((((dst_value_assoc_leftmasktable) = 2 * (ge_balance_positive_assoc_leftmasktableentryvalue) /\ (ge_balance_negative_assoc_leftmasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_leftmasktableentryvaluedecode. (((dst_value_assoc_leftmasktable) = 2 * ge_signed_half_assoc_leftmasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_leftmasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_leftmasktableentryvalue) = S ge_signed_half_assoc_leftmasktableentryvaluedecode))) /\ ((dst_positive_assoc_leftmasktable) + ge_balance_negative_assoc_leftmasktableentryvalue = (dst_negative_assoc_leftmasktable) + ge_balance_positive_assoc_leftmasktableentryvalue))))))))) /\ (forall dc_index_assoc_leftmask dc_value_assoc_leftmask. (exists pvs_le_gap_assoc_leftmaskdomain. pvs_le_gap_assoc_leftmaskdomain + (dc_index_assoc_leftmask) = (n)) -> (exists dst_positive_code_assoc_leftmasklookup dst_positive_scale_assoc_leftmasklookup dst_negative_code_assoc_leftmasklookup dst_negative_scale_assoc_leftmasklookup dst_positive_assoc_leftmasklookup dst_negative_assoc_leftmasklookup. (((dc_mask_assoc_left) = (((((dst_positive_code_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup)) * S ((dst_positive_code_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup)) + ((dst_positive_scale_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup))) + (((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) * S ((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) + ((dst_negative_scale_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)))) * S ((((dst_positive_code_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup)) * S ((dst_positive_code_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup)) + ((dst_positive_scale_assoc_leftmasklookup) + (dst_positive_scale_assoc_leftmasklookup))) + (((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) * S ((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) + ((dst_negative_scale_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)))) + ((((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) * S ((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) + ((dst_negative_scale_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup))) + (((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) * S ((dst_negative_code_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)) + ((dst_negative_scale_assoc_leftmasklookup) + (dst_negative_scale_assoc_leftmasklookup)))))) /\ (((((exists ff_h_pvs_assoc_leftmasklookuppositive. ff_h_pvs_assoc_leftmasklookuppositive + S (dst_positive_assoc_leftmasklookup) = S ((S (dc_index_assoc_leftmask)) * dst_positive_scale_assoc_leftmasklookup)) /\ exists ff_q_pvs_assoc_leftmasklookuppositive. dst_positive_code_assoc_leftmasklookup = ff_q_pvs_assoc_leftmasklookuppositive * S ((S (dc_index_assoc_leftmask)) * dst_positive_scale_assoc_leftmasklookup) + (dst_positive_assoc_leftmasklookup))) /\ (((((exists ff_h_pvs_assoc_leftmasklookupnegative. ff_h_pvs_assoc_leftmasklookupnegative + S (dst_negative_assoc_leftmasklookup) = S ((S (dc_index_assoc_leftmask)) * dst_negative_scale_assoc_leftmasklookup)) /\ exists ff_q_pvs_assoc_leftmasklookupnegative. dst_negative_code_assoc_leftmasklookup = ff_q_pvs_assoc_leftmasklookupnegative * S ((S (dc_index_assoc_leftmask)) * dst_negative_scale_assoc_leftmasklookup) + (dst_negative_assoc_leftmasklookup))) /\ (exists ge_balance_positive_assoc_leftmasklookupvalue ge_balance_negative_assoc_leftmasklookupvalue. (((((dc_value_assoc_leftmask) = 2 * (ge_balance_positive_assoc_leftmasklookupvalue) /\ (ge_balance_negative_assoc_leftmasklookupvalue) = 0) \/ exists ge_signed_half_assoc_leftmasklookupvaluedecode. (((dc_value_assoc_leftmask) = 2 * ge_signed_half_assoc_leftmasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_leftmasklookupvalue) = 0) /\ (ge_balance_negative_assoc_leftmasklookupvalue) = S ge_signed_half_assoc_leftmasklookupvaluedecode))) /\ ((dst_positive_assoc_leftmasklookup) + ge_balance_negative_assoc_leftmasklookupvalue = (dst_negative_assoc_leftmasklookup) + ge_balance_positive_assoc_leftmasklookupvalue))))))))) -> ((((~((dc_index_assoc_leftmask)=0)) /\ (exists dc_quotient_assoc_leftmaskentry dc_left_assoc_leftmaskentry dc_right_assoc_leftmaskentry. (((n)=(dc_index_assoc_leftmask)*dc_quotient_assoc_leftmaskentry) /\ (((exists dst_positive_code_assoc_leftmaskentryleft dst_positive_scale_assoc_leftmaskentryleft dst_negative_code_assoc_leftmaskentryleft dst_negative_scale_assoc_leftmaskentryleft dst_positive_assoc_leftmaskentryleft dst_negative_assoc_leftmaskentryleft. (((A) = (((((dst_positive_code_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft)) * S ((dst_positive_code_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft)) + ((dst_positive_scale_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft))) + (((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) * S ((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) + ((dst_negative_scale_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)))) * S ((((dst_positive_code_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft)) * S ((dst_positive_code_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft)) + ((dst_positive_scale_assoc_leftmaskentryleft) + (dst_positive_scale_assoc_leftmaskentryleft))) + (((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) * S ((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) + ((dst_negative_scale_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)))) + ((((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) * S ((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) + ((dst_negative_scale_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft))) + (((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) * S ((dst_negative_code_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)) + ((dst_negative_scale_assoc_leftmaskentryleft) + (dst_negative_scale_assoc_leftmaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_leftmaskentryleftpositive. ff_h_pvs_assoc_leftmaskentryleftpositive + S (dst_positive_assoc_leftmaskentryleft) = S ((S (dc_index_assoc_leftmask)) * dst_positive_scale_assoc_leftmaskentryleft)) /\ exists ff_q_pvs_assoc_leftmaskentryleftpositive. dst_positive_code_assoc_leftmaskentryleft = ff_q_pvs_assoc_leftmaskentryleftpositive * S ((S (dc_index_assoc_leftmask)) * dst_positive_scale_assoc_leftmaskentryleft) + (dst_positive_assoc_leftmaskentryleft))) /\ (((((exists ff_h_pvs_assoc_leftmaskentryleftnegative. ff_h_pvs_assoc_leftmaskentryleftnegative + S (dst_negative_assoc_leftmaskentryleft) = S ((S (dc_index_assoc_leftmask)) * dst_negative_scale_assoc_leftmaskentryleft)) /\ exists ff_q_pvs_assoc_leftmaskentryleftnegative. dst_negative_code_assoc_leftmaskentryleft = ff_q_pvs_assoc_leftmaskentryleftnegative * S ((S (dc_index_assoc_leftmask)) * dst_negative_scale_assoc_leftmaskentryleft) + (dst_negative_assoc_leftmaskentryleft))) /\ (exists ge_balance_positive_assoc_leftmaskentryleftvalue ge_balance_negative_assoc_leftmaskentryleftvalue. (((((dc_left_assoc_leftmaskentry) = 2 * (ge_balance_positive_assoc_leftmaskentryleftvalue) /\ (ge_balance_negative_assoc_leftmaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_leftmaskentryleftvaluedecode. (((dc_left_assoc_leftmaskentry) = 2 * ge_signed_half_assoc_leftmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_leftmaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_leftmaskentryleftvalue) = S ge_signed_half_assoc_leftmaskentryleftvaluedecode))) /\ ((dst_positive_assoc_leftmaskentryleft) + ge_balance_negative_assoc_leftmaskentryleftvalue = (dst_negative_assoc_leftmaskentryleft) + ge_balance_positive_assoc_leftmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_leftmaskentryright dst_positive_scale_assoc_leftmaskentryright dst_negative_code_assoc_leftmaskentryright dst_negative_scale_assoc_leftmaskentryright dst_positive_assoc_leftmaskentryright dst_negative_assoc_leftmaskentryright. (((H) = (((((dst_positive_code_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright)) * S ((dst_positive_code_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright)) + ((dst_positive_scale_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright))) + (((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) * S ((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) + ((dst_negative_scale_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)))) * S ((((dst_positive_code_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright)) * S ((dst_positive_code_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright)) + ((dst_positive_scale_assoc_leftmaskentryright) + (dst_positive_scale_assoc_leftmaskentryright))) + (((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) * S ((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) + ((dst_negative_scale_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)))) + ((((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) * S ((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) + ((dst_negative_scale_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright))) + (((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) * S ((dst_negative_code_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)) + ((dst_negative_scale_assoc_leftmaskentryright) + (dst_negative_scale_assoc_leftmaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_leftmaskentryrightpositive. ff_h_pvs_assoc_leftmaskentryrightpositive + S (dst_positive_assoc_leftmaskentryright) = S ((S (dc_quotient_assoc_leftmaskentry)) * dst_positive_scale_assoc_leftmaskentryright)) /\ exists ff_q_pvs_assoc_leftmaskentryrightpositive. dst_positive_code_assoc_leftmaskentryright = ff_q_pvs_assoc_leftmaskentryrightpositive * S ((S (dc_quotient_assoc_leftmaskentry)) * dst_positive_scale_assoc_leftmaskentryright) + (dst_positive_assoc_leftmaskentryright))) /\ (((((exists ff_h_pvs_assoc_leftmaskentryrightnegative. ff_h_pvs_assoc_leftmaskentryrightnegative + S (dst_negative_assoc_leftmaskentryright) = S ((S (dc_quotient_assoc_leftmaskentry)) * dst_negative_scale_assoc_leftmaskentryright)) /\ exists ff_q_pvs_assoc_leftmaskentryrightnegative. dst_negative_code_assoc_leftmaskentryright = ff_q_pvs_assoc_leftmaskentryrightnegative * S ((S (dc_quotient_assoc_leftmaskentry)) * dst_negative_scale_assoc_leftmaskentryright) + (dst_negative_assoc_leftmaskentryright))) /\ (exists ge_balance_positive_assoc_leftmaskentryrightvalue ge_balance_negative_assoc_leftmaskentryrightvalue. (((((dc_right_assoc_leftmaskentry) = 2 * (ge_balance_positive_assoc_leftmaskentryrightvalue) /\ (ge_balance_negative_assoc_leftmaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_leftmaskentryrightvaluedecode. (((dc_right_assoc_leftmaskentry) = 2 * ge_signed_half_assoc_leftmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_leftmaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_leftmaskentryrightvalue) = S ge_signed_half_assoc_leftmaskentryrightvaluedecode))) /\ ((dst_positive_assoc_leftmaskentryright) + ge_balance_negative_assoc_leftmaskentryrightvalue = (dst_negative_assoc_leftmaskentryright) + ge_balance_positive_assoc_leftmaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_leftmaskentryproduct sto_an_assoc_leftmaskentryproduct sto_bp_assoc_leftmaskentryproduct sto_bn_assoc_leftmaskentryproduct sto_cp_assoc_leftmaskentryproduct sto_cn_assoc_leftmaskentryproduct. (((((dc_left_assoc_leftmaskentry) = 2 * (sto_ap_assoc_leftmaskentryproduct) /\ (sto_an_assoc_leftmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_leftmaskentryproductleft. (((dc_left_assoc_leftmaskentry) = 2 * ge_signed_half_assoc_leftmaskentryproductleft + 1 /\ (sto_ap_assoc_leftmaskentryproduct) = 0) /\ (sto_an_assoc_leftmaskentryproduct) = S ge_signed_half_assoc_leftmaskentryproductleft))) /\ ((((((dc_right_assoc_leftmaskentry) = 2 * (sto_bp_assoc_leftmaskentryproduct) /\ (sto_bn_assoc_leftmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_leftmaskentryproductright. (((dc_right_assoc_leftmaskentry) = 2 * ge_signed_half_assoc_leftmaskentryproductright + 1 /\ (sto_bp_assoc_leftmaskentryproduct) = 0) /\ (sto_bn_assoc_leftmaskentryproduct) = S ge_signed_half_assoc_leftmaskentryproductright))) /\ ((((((dc_value_assoc_leftmask) = 2 * (sto_cp_assoc_leftmaskentryproduct) /\ (sto_cn_assoc_leftmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_leftmaskentryproductoutput. (((dc_value_assoc_leftmask) = 2 * ge_signed_half_assoc_leftmaskentryproductoutput + 1 /\ (sto_cp_assoc_leftmaskentryproduct) = 0) /\ (sto_cn_assoc_leftmaskentryproduct) = S ge_signed_half_assoc_leftmaskentryproductoutput))) /\ ((sto_ap_assoc_leftmaskentryproduct * sto_bp_assoc_leftmaskentryproduct + sto_an_assoc_leftmaskentryproduct * sto_bn_assoc_leftmaskentryproduct) + sto_cn_assoc_leftmaskentryproduct = (sto_ap_assoc_leftmaskentryproduct * sto_bn_assoc_leftmaskentryproduct + sto_an_assoc_leftmaskentryproduct * sto_bp_assoc_leftmaskentryproduct) + sto_cp_assoc_leftmaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_leftmask)=0 \/ ~(exists pvs_factor_assoc_leftmaskentrynondivisor. (n) = (dc_index_assoc_leftmask) * pvs_factor_assoc_leftmaskentrynondivisor)) /\ ((dc_value_assoc_leftmask)=0))))))) /\ (exists dst_positive_code_assoc_leftfold dst_positive_scale_assoc_leftfold dst_negative_code_assoc_leftfold dst_negative_scale_assoc_leftfold dst_positive_sum_assoc_leftfold dst_negative_sum_assoc_leftfold. (((dc_mask_assoc_left) = (((((dst_positive_code_assoc_leftfold) + (dst_positive_scale_assoc_leftfold)) * S ((dst_positive_code_assoc_leftfold) + (dst_positive_scale_assoc_leftfold)) + ((dst_positive_scale_assoc_leftfold) + (dst_positive_scale_assoc_leftfold))) + (((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) * S ((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) + ((dst_negative_scale_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)))) * S ((((dst_positive_code_assoc_leftfold) + (dst_positive_scale_assoc_leftfold)) * S ((dst_positive_code_assoc_leftfold) + (dst_positive_scale_assoc_leftfold)) + ((dst_positive_scale_assoc_leftfold) + (dst_positive_scale_assoc_leftfold))) + (((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) * S ((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) + ((dst_negative_scale_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)))) + ((((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) * S ((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) + ((dst_negative_scale_assoc_leftfold) + (dst_negative_scale_assoc_leftfold))) + (((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) * S ((dst_negative_code_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)) + ((dst_negative_scale_assoc_leftfold) + (dst_negative_scale_assoc_leftfold)))))) /\ (((exists fs_u_dst_assoc_leftfoldpositive fs_v_dst_assoc_leftfoldpositive. ((((exists fs_h_dst_assoc_leftfoldpositive_body_start. fs_h_dst_assoc_leftfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_leftfoldpositive)) /\ exists fs_q_dst_assoc_leftfoldpositive_body_start. fs_u_dst_assoc_leftfoldpositive = fs_q_dst_assoc_leftfoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_leftfoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_leftfoldpositive_body_terminal. fs_h_dst_assoc_leftfoldpositive_body_terminal + S (dst_positive_sum_assoc_leftfold) = S ((S (S (n))) * fs_v_dst_assoc_leftfoldpositive)) /\ exists fs_q_dst_assoc_leftfoldpositive_body_terminal. fs_u_dst_assoc_leftfoldpositive = fs_q_dst_assoc_leftfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_assoc_leftfoldpositive) + (dst_positive_sum_assoc_leftfold))) /\ forall fs_i_dst_assoc_leftfoldpositive_body_steps. (exists fs_lt_dst_assoc_leftfoldpositive_body_steps_bound. fs_lt_dst_assoc_leftfoldpositive_body_steps_bound + S fs_i_dst_assoc_leftfoldpositive_body_steps = S (n)) -> exists fs_a_dst_assoc_leftfoldpositive_body_steps fs_r_dst_assoc_leftfoldpositive_body_steps fs_s_dst_assoc_leftfoldpositive_body_steps. ((((exists fs_h_dst_assoc_leftfoldpositive_body_steps_summand. fs_h_dst_assoc_leftfoldpositive_body_steps_summand + S (fs_a_dst_assoc_leftfoldpositive_body_steps) = S ((S (fs_i_dst_assoc_leftfoldpositive_body_steps)) * dst_positive_scale_assoc_leftfold)) /\ exists fs_q_dst_assoc_leftfoldpositive_body_steps_summand. dst_positive_code_assoc_leftfold = fs_q_dst_assoc_leftfoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_leftfoldpositive_body_steps)) * dst_positive_scale_assoc_leftfold) + (fs_a_dst_assoc_leftfoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_leftfoldpositive_body_steps_partial. fs_h_dst_assoc_leftfoldpositive_body_steps_partial + S (fs_r_dst_assoc_leftfoldpositive_body_steps) = S ((S (fs_i_dst_assoc_leftfoldpositive_body_steps)) * fs_v_dst_assoc_leftfoldpositive)) /\ exists fs_q_dst_assoc_leftfoldpositive_body_steps_partial. fs_u_dst_assoc_leftfoldpositive = fs_q_dst_assoc_leftfoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_leftfoldpositive_body_steps)) * fs_v_dst_assoc_leftfoldpositive) + (fs_r_dst_assoc_leftfoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_leftfoldpositive_body_steps_successor. fs_h_dst_assoc_leftfoldpositive_body_steps_successor + S (fs_s_dst_assoc_leftfoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_leftfoldpositive_body_steps)) * fs_v_dst_assoc_leftfoldpositive)) /\ exists fs_q_dst_assoc_leftfoldpositive_body_steps_successor. fs_u_dst_assoc_leftfoldpositive = fs_q_dst_assoc_leftfoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_leftfoldpositive_body_steps)) * fs_v_dst_assoc_leftfoldpositive) + (fs_s_dst_assoc_leftfoldpositive_body_steps))) /\ fs_s_dst_assoc_leftfoldpositive_body_steps = fs_r_dst_assoc_leftfoldpositive_body_steps + fs_a_dst_assoc_leftfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_leftfoldnegative fs_v_dst_assoc_leftfoldnegative. ((((exists fs_h_dst_assoc_leftfoldnegative_body_start. fs_h_dst_assoc_leftfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_leftfoldnegative)) /\ exists fs_q_dst_assoc_leftfoldnegative_body_start. fs_u_dst_assoc_leftfoldnegative = fs_q_dst_assoc_leftfoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_leftfoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_leftfoldnegative_body_terminal. fs_h_dst_assoc_leftfoldnegative_body_terminal + S (dst_negative_sum_assoc_leftfold) = S ((S (S (n))) * fs_v_dst_assoc_leftfoldnegative)) /\ exists fs_q_dst_assoc_leftfoldnegative_body_terminal. fs_u_dst_assoc_leftfoldnegative = fs_q_dst_assoc_leftfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_assoc_leftfoldnegative) + (dst_negative_sum_assoc_leftfold))) /\ forall fs_i_dst_assoc_leftfoldnegative_body_steps. (exists fs_lt_dst_assoc_leftfoldnegative_body_steps_bound. fs_lt_dst_assoc_leftfoldnegative_body_steps_bound + S fs_i_dst_assoc_leftfoldnegative_body_steps = S (n)) -> exists fs_a_dst_assoc_leftfoldnegative_body_steps fs_r_dst_assoc_leftfoldnegative_body_steps fs_s_dst_assoc_leftfoldnegative_body_steps. ((((exists fs_h_dst_assoc_leftfoldnegative_body_steps_summand. fs_h_dst_assoc_leftfoldnegative_body_steps_summand + S (fs_a_dst_assoc_leftfoldnegative_body_steps) = S ((S (fs_i_dst_assoc_leftfoldnegative_body_steps)) * dst_negative_scale_assoc_leftfold)) /\ exists fs_q_dst_assoc_leftfoldnegative_body_steps_summand. dst_negative_code_assoc_leftfold = fs_q_dst_assoc_leftfoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_leftfoldnegative_body_steps)) * dst_negative_scale_assoc_leftfold) + (fs_a_dst_assoc_leftfoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_leftfoldnegative_body_steps_partial. fs_h_dst_assoc_leftfoldnegative_body_steps_partial + S (fs_r_dst_assoc_leftfoldnegative_body_steps) = S ((S (fs_i_dst_assoc_leftfoldnegative_body_steps)) * fs_v_dst_assoc_leftfoldnegative)) /\ exists fs_q_dst_assoc_leftfoldnegative_body_steps_partial. fs_u_dst_assoc_leftfoldnegative = fs_q_dst_assoc_leftfoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_leftfoldnegative_body_steps)) * fs_v_dst_assoc_leftfoldnegative) + (fs_r_dst_assoc_leftfoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_leftfoldnegative_body_steps_successor. fs_h_dst_assoc_leftfoldnegative_body_steps_successor + S (fs_s_dst_assoc_leftfoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_leftfoldnegative_body_steps)) * fs_v_dst_assoc_leftfoldnegative)) /\ exists fs_q_dst_assoc_leftfoldnegative_body_steps_successor. fs_u_dst_assoc_leftfoldnegative = fs_q_dst_assoc_leftfoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_leftfoldnegative_body_steps)) * fs_v_dst_assoc_leftfoldnegative) + (fs_s_dst_assoc_leftfoldnegative_body_steps))) /\ fs_s_dst_assoc_leftfoldnegative_body_steps = fs_r_dst_assoc_leftfoldnegative_body_steps + fs_a_dst_assoc_leftfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_leftfoldresult ge_balance_negative_assoc_leftfoldresult. (((((u) = 2 * (ge_balance_positive_assoc_leftfoldresult) /\ (ge_balance_negative_assoc_leftfoldresult) = 0) \/ exists ge_signed_half_assoc_leftfoldresultdecode. (((u) = 2 * ge_signed_half_assoc_leftfoldresultdecode + 1 /\ (ge_balance_positive_assoc_leftfoldresult) = 0) /\ (ge_balance_negative_assoc_leftfoldresult) = S ge_signed_half_assoc_leftfoldresultdecode))) /\ ((dst_positive_sum_assoc_leftfold) + ge_balance_negative_assoc_leftfoldresult = (dst_negative_sum_assoc_leftfold) + ge_balance_positive_assoc_leftfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_assoc_right. ((((exists dst_positive_code_assoc_rightmasktable dst_positive_scale_assoc_rightmasktable dst_negative_code_assoc_rightmasktable dst_negative_scale_assoc_rightmasktable. (((dc_mask_assoc_right) = (((((dst_positive_code_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable)) * S ((dst_positive_code_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable)) + ((dst_positive_scale_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable))) + (((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) * S ((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) + ((dst_negative_scale_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)))) * S ((((dst_positive_code_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable)) * S ((dst_positive_code_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable)) + ((dst_positive_scale_assoc_rightmasktable) + (dst_positive_scale_assoc_rightmasktable))) + (((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) * S ((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) + ((dst_negative_scale_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)))) + ((((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) * S ((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) + ((dst_negative_scale_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable))) + (((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) * S ((dst_negative_code_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)) + ((dst_negative_scale_assoc_rightmasktable) + (dst_negative_scale_assoc_rightmasktable)))))) /\ (forall dst_index_assoc_rightmasktable. (exists pvs_le_gap_assoc_rightmasktabledomain. pvs_le_gap_assoc_rightmasktabledomain + (dst_index_assoc_rightmasktable) = (n)) -> exists dst_positive_assoc_rightmasktable dst_negative_assoc_rightmasktable dst_value_assoc_rightmasktable. ((((exists ff_h_pvs_assoc_rightmasktableentrypositive. ff_h_pvs_assoc_rightmasktableentrypositive + S (dst_positive_assoc_rightmasktable) = S ((S (dst_index_assoc_rightmasktable)) * dst_positive_scale_assoc_rightmasktable)) /\ exists ff_q_pvs_assoc_rightmasktableentrypositive. dst_positive_code_assoc_rightmasktable = ff_q_pvs_assoc_rightmasktableentrypositive * S ((S (dst_index_assoc_rightmasktable)) * dst_positive_scale_assoc_rightmasktable) + (dst_positive_assoc_rightmasktable))) /\ (((((exists ff_h_pvs_assoc_rightmasktableentrynegative. ff_h_pvs_assoc_rightmasktableentrynegative + S (dst_negative_assoc_rightmasktable) = S ((S (dst_index_assoc_rightmasktable)) * dst_negative_scale_assoc_rightmasktable)) /\ exists ff_q_pvs_assoc_rightmasktableentrynegative. dst_negative_code_assoc_rightmasktable = ff_q_pvs_assoc_rightmasktableentrynegative * S ((S (dst_index_assoc_rightmasktable)) * dst_negative_scale_assoc_rightmasktable) + (dst_negative_assoc_rightmasktable))) /\ (exists ge_balance_positive_assoc_rightmasktableentryvalue ge_balance_negative_assoc_rightmasktableentryvalue. (((((dst_value_assoc_rightmasktable) = 2 * (ge_balance_positive_assoc_rightmasktableentryvalue) /\ (ge_balance_negative_assoc_rightmasktableentryvalue) = 0) \/ exists ge_signed_half_assoc_rightmasktableentryvaluedecode. (((dst_value_assoc_rightmasktable) = 2 * ge_signed_half_assoc_rightmasktableentryvaluedecode + 1 /\ (ge_balance_positive_assoc_rightmasktableentryvalue) = 0) /\ (ge_balance_negative_assoc_rightmasktableentryvalue) = S ge_signed_half_assoc_rightmasktableentryvaluedecode))) /\ ((dst_positive_assoc_rightmasktable) + ge_balance_negative_assoc_rightmasktableentryvalue = (dst_negative_assoc_rightmasktable) + ge_balance_positive_assoc_rightmasktableentryvalue))))))))) /\ (forall dc_index_assoc_rightmask dc_value_assoc_rightmask. (exists pvs_le_gap_assoc_rightmaskdomain. pvs_le_gap_assoc_rightmaskdomain + (dc_index_assoc_rightmask) = (n)) -> (exists dst_positive_code_assoc_rightmasklookup dst_positive_scale_assoc_rightmasklookup dst_negative_code_assoc_rightmasklookup dst_negative_scale_assoc_rightmasklookup dst_positive_assoc_rightmasklookup dst_negative_assoc_rightmasklookup. (((dc_mask_assoc_right) = (((((dst_positive_code_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup)) * S ((dst_positive_code_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup)) + ((dst_positive_scale_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup))) + (((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) * S ((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) + ((dst_negative_scale_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)))) * S ((((dst_positive_code_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup)) * S ((dst_positive_code_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup)) + ((dst_positive_scale_assoc_rightmasklookup) + (dst_positive_scale_assoc_rightmasklookup))) + (((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) * S ((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) + ((dst_negative_scale_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)))) + ((((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) * S ((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) + ((dst_negative_scale_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup))) + (((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) * S ((dst_negative_code_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)) + ((dst_negative_scale_assoc_rightmasklookup) + (dst_negative_scale_assoc_rightmasklookup)))))) /\ (((((exists ff_h_pvs_assoc_rightmasklookuppositive. ff_h_pvs_assoc_rightmasklookuppositive + S (dst_positive_assoc_rightmasklookup) = S ((S (dc_index_assoc_rightmask)) * dst_positive_scale_assoc_rightmasklookup)) /\ exists ff_q_pvs_assoc_rightmasklookuppositive. dst_positive_code_assoc_rightmasklookup = ff_q_pvs_assoc_rightmasklookuppositive * S ((S (dc_index_assoc_rightmask)) * dst_positive_scale_assoc_rightmasklookup) + (dst_positive_assoc_rightmasklookup))) /\ (((((exists ff_h_pvs_assoc_rightmasklookupnegative. ff_h_pvs_assoc_rightmasklookupnegative + S (dst_negative_assoc_rightmasklookup) = S ((S (dc_index_assoc_rightmask)) * dst_negative_scale_assoc_rightmasklookup)) /\ exists ff_q_pvs_assoc_rightmasklookupnegative. dst_negative_code_assoc_rightmasklookup = ff_q_pvs_assoc_rightmasklookupnegative * S ((S (dc_index_assoc_rightmask)) * dst_negative_scale_assoc_rightmasklookup) + (dst_negative_assoc_rightmasklookup))) /\ (exists ge_balance_positive_assoc_rightmasklookupvalue ge_balance_negative_assoc_rightmasklookupvalue. (((((dc_value_assoc_rightmask) = 2 * (ge_balance_positive_assoc_rightmasklookupvalue) /\ (ge_balance_negative_assoc_rightmasklookupvalue) = 0) \/ exists ge_signed_half_assoc_rightmasklookupvaluedecode. (((dc_value_assoc_rightmask) = 2 * ge_signed_half_assoc_rightmasklookupvaluedecode + 1 /\ (ge_balance_positive_assoc_rightmasklookupvalue) = 0) /\ (ge_balance_negative_assoc_rightmasklookupvalue) = S ge_signed_half_assoc_rightmasklookupvaluedecode))) /\ ((dst_positive_assoc_rightmasklookup) + ge_balance_negative_assoc_rightmasklookupvalue = (dst_negative_assoc_rightmasklookup) + ge_balance_positive_assoc_rightmasklookupvalue))))))))) -> ((((~((dc_index_assoc_rightmask)=0)) /\ (exists dc_quotient_assoc_rightmaskentry dc_left_assoc_rightmaskentry dc_right_assoc_rightmaskentry. (((n)=(dc_index_assoc_rightmask)*dc_quotient_assoc_rightmaskentry) /\ (((exists dst_positive_code_assoc_rightmaskentryleft dst_positive_scale_assoc_rightmaskentryleft dst_negative_code_assoc_rightmaskentryleft dst_negative_scale_assoc_rightmaskentryleft dst_positive_assoc_rightmaskentryleft dst_negative_assoc_rightmaskentryleft. (((F) = (((((dst_positive_code_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft)) * S ((dst_positive_code_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft)) + ((dst_positive_scale_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft))) + (((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) * S ((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) + ((dst_negative_scale_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)))) * S ((((dst_positive_code_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft)) * S ((dst_positive_code_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft)) + ((dst_positive_scale_assoc_rightmaskentryleft) + (dst_positive_scale_assoc_rightmaskentryleft))) + (((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) * S ((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) + ((dst_negative_scale_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)))) + ((((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) * S ((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) + ((dst_negative_scale_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft))) + (((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) * S ((dst_negative_code_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)) + ((dst_negative_scale_assoc_rightmaskentryleft) + (dst_negative_scale_assoc_rightmaskentryleft)))))) /\ (((((exists ff_h_pvs_assoc_rightmaskentryleftpositive. ff_h_pvs_assoc_rightmaskentryleftpositive + S (dst_positive_assoc_rightmaskentryleft) = S ((S (dc_index_assoc_rightmask)) * dst_positive_scale_assoc_rightmaskentryleft)) /\ exists ff_q_pvs_assoc_rightmaskentryleftpositive. dst_positive_code_assoc_rightmaskentryleft = ff_q_pvs_assoc_rightmaskentryleftpositive * S ((S (dc_index_assoc_rightmask)) * dst_positive_scale_assoc_rightmaskentryleft) + (dst_positive_assoc_rightmaskentryleft))) /\ (((((exists ff_h_pvs_assoc_rightmaskentryleftnegative. ff_h_pvs_assoc_rightmaskentryleftnegative + S (dst_negative_assoc_rightmaskentryleft) = S ((S (dc_index_assoc_rightmask)) * dst_negative_scale_assoc_rightmaskentryleft)) /\ exists ff_q_pvs_assoc_rightmaskentryleftnegative. dst_negative_code_assoc_rightmaskentryleft = ff_q_pvs_assoc_rightmaskentryleftnegative * S ((S (dc_index_assoc_rightmask)) * dst_negative_scale_assoc_rightmaskentryleft) + (dst_negative_assoc_rightmaskentryleft))) /\ (exists ge_balance_positive_assoc_rightmaskentryleftvalue ge_balance_negative_assoc_rightmaskentryleftvalue. (((((dc_left_assoc_rightmaskentry) = 2 * (ge_balance_positive_assoc_rightmaskentryleftvalue) /\ (ge_balance_negative_assoc_rightmaskentryleftvalue) = 0) \/ exists ge_signed_half_assoc_rightmaskentryleftvaluedecode. (((dc_left_assoc_rightmaskentry) = 2 * ge_signed_half_assoc_rightmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_assoc_rightmaskentryleftvalue) = 0) /\ (ge_balance_negative_assoc_rightmaskentryleftvalue) = S ge_signed_half_assoc_rightmaskentryleftvaluedecode))) /\ ((dst_positive_assoc_rightmaskentryleft) + ge_balance_negative_assoc_rightmaskentryleftvalue = (dst_negative_assoc_rightmaskentryleft) + ge_balance_positive_assoc_rightmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_assoc_rightmaskentryright dst_positive_scale_assoc_rightmaskentryright dst_negative_code_assoc_rightmaskentryright dst_negative_scale_assoc_rightmaskentryright dst_positive_assoc_rightmaskentryright dst_negative_assoc_rightmaskentryright. (((B) = (((((dst_positive_code_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright)) * S ((dst_positive_code_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright)) + ((dst_positive_scale_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright))) + (((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) * S ((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) + ((dst_negative_scale_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)))) * S ((((dst_positive_code_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright)) * S ((dst_positive_code_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright)) + ((dst_positive_scale_assoc_rightmaskentryright) + (dst_positive_scale_assoc_rightmaskentryright))) + (((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) * S ((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) + ((dst_negative_scale_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)))) + ((((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) * S ((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) + ((dst_negative_scale_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright))) + (((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) * S ((dst_negative_code_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)) + ((dst_negative_scale_assoc_rightmaskentryright) + (dst_negative_scale_assoc_rightmaskentryright)))))) /\ (((((exists ff_h_pvs_assoc_rightmaskentryrightpositive. ff_h_pvs_assoc_rightmaskentryrightpositive + S (dst_positive_assoc_rightmaskentryright) = S ((S (dc_quotient_assoc_rightmaskentry)) * dst_positive_scale_assoc_rightmaskentryright)) /\ exists ff_q_pvs_assoc_rightmaskentryrightpositive. dst_positive_code_assoc_rightmaskentryright = ff_q_pvs_assoc_rightmaskentryrightpositive * S ((S (dc_quotient_assoc_rightmaskentry)) * dst_positive_scale_assoc_rightmaskentryright) + (dst_positive_assoc_rightmaskentryright))) /\ (((((exists ff_h_pvs_assoc_rightmaskentryrightnegative. ff_h_pvs_assoc_rightmaskentryrightnegative + S (dst_negative_assoc_rightmaskentryright) = S ((S (dc_quotient_assoc_rightmaskentry)) * dst_negative_scale_assoc_rightmaskentryright)) /\ exists ff_q_pvs_assoc_rightmaskentryrightnegative. dst_negative_code_assoc_rightmaskentryright = ff_q_pvs_assoc_rightmaskentryrightnegative * S ((S (dc_quotient_assoc_rightmaskentry)) * dst_negative_scale_assoc_rightmaskentryright) + (dst_negative_assoc_rightmaskentryright))) /\ (exists ge_balance_positive_assoc_rightmaskentryrightvalue ge_balance_negative_assoc_rightmaskentryrightvalue. (((((dc_right_assoc_rightmaskentry) = 2 * (ge_balance_positive_assoc_rightmaskentryrightvalue) /\ (ge_balance_negative_assoc_rightmaskentryrightvalue) = 0) \/ exists ge_signed_half_assoc_rightmaskentryrightvaluedecode. (((dc_right_assoc_rightmaskentry) = 2 * ge_signed_half_assoc_rightmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_assoc_rightmaskentryrightvalue) = 0) /\ (ge_balance_negative_assoc_rightmaskentryrightvalue) = S ge_signed_half_assoc_rightmaskentryrightvaluedecode))) /\ ((dst_positive_assoc_rightmaskentryright) + ge_balance_negative_assoc_rightmaskentryrightvalue = (dst_negative_assoc_rightmaskentryright) + ge_balance_positive_assoc_rightmaskentryrightvalue))))))))) /\ (exists sto_ap_assoc_rightmaskentryproduct sto_an_assoc_rightmaskentryproduct sto_bp_assoc_rightmaskentryproduct sto_bn_assoc_rightmaskentryproduct sto_cp_assoc_rightmaskentryproduct sto_cn_assoc_rightmaskentryproduct. (((((dc_left_assoc_rightmaskentry) = 2 * (sto_ap_assoc_rightmaskentryproduct) /\ (sto_an_assoc_rightmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_rightmaskentryproductleft. (((dc_left_assoc_rightmaskentry) = 2 * ge_signed_half_assoc_rightmaskentryproductleft + 1 /\ (sto_ap_assoc_rightmaskentryproduct) = 0) /\ (sto_an_assoc_rightmaskentryproduct) = S ge_signed_half_assoc_rightmaskentryproductleft))) /\ ((((((dc_right_assoc_rightmaskentry) = 2 * (sto_bp_assoc_rightmaskentryproduct) /\ (sto_bn_assoc_rightmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_rightmaskentryproductright. (((dc_right_assoc_rightmaskentry) = 2 * ge_signed_half_assoc_rightmaskentryproductright + 1 /\ (sto_bp_assoc_rightmaskentryproduct) = 0) /\ (sto_bn_assoc_rightmaskentryproduct) = S ge_signed_half_assoc_rightmaskentryproductright))) /\ ((((((dc_value_assoc_rightmask) = 2 * (sto_cp_assoc_rightmaskentryproduct) /\ (sto_cn_assoc_rightmaskentryproduct) = 0) \/ exists ge_signed_half_assoc_rightmaskentryproductoutput. (((dc_value_assoc_rightmask) = 2 * ge_signed_half_assoc_rightmaskentryproductoutput + 1 /\ (sto_cp_assoc_rightmaskentryproduct) = 0) /\ (sto_cn_assoc_rightmaskentryproduct) = S ge_signed_half_assoc_rightmaskentryproductoutput))) /\ ((sto_ap_assoc_rightmaskentryproduct * sto_bp_assoc_rightmaskentryproduct + sto_an_assoc_rightmaskentryproduct * sto_bn_assoc_rightmaskentryproduct) + sto_cn_assoc_rightmaskentryproduct = (sto_ap_assoc_rightmaskentryproduct * sto_bn_assoc_rightmaskentryproduct + sto_an_assoc_rightmaskentryproduct * sto_bp_assoc_rightmaskentryproduct) + sto_cp_assoc_rightmaskentryproduct))))))))))))))) \/ ((((dc_index_assoc_rightmask)=0 \/ ~(exists pvs_factor_assoc_rightmaskentrynondivisor. (n) = (dc_index_assoc_rightmask) * pvs_factor_assoc_rightmaskentrynondivisor)) /\ ((dc_value_assoc_rightmask)=0))))))) /\ (exists dst_positive_code_assoc_rightfold dst_positive_scale_assoc_rightfold dst_negative_code_assoc_rightfold dst_negative_scale_assoc_rightfold dst_positive_sum_assoc_rightfold dst_negative_sum_assoc_rightfold. (((dc_mask_assoc_right) = (((((dst_positive_code_assoc_rightfold) + (dst_positive_scale_assoc_rightfold)) * S ((dst_positive_code_assoc_rightfold) + (dst_positive_scale_assoc_rightfold)) + ((dst_positive_scale_assoc_rightfold) + (dst_positive_scale_assoc_rightfold))) + (((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) * S ((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) + ((dst_negative_scale_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)))) * S ((((dst_positive_code_assoc_rightfold) + (dst_positive_scale_assoc_rightfold)) * S ((dst_positive_code_assoc_rightfold) + (dst_positive_scale_assoc_rightfold)) + ((dst_positive_scale_assoc_rightfold) + (dst_positive_scale_assoc_rightfold))) + (((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) * S ((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) + ((dst_negative_scale_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)))) + ((((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) * S ((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) + ((dst_negative_scale_assoc_rightfold) + (dst_negative_scale_assoc_rightfold))) + (((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) * S ((dst_negative_code_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)) + ((dst_negative_scale_assoc_rightfold) + (dst_negative_scale_assoc_rightfold)))))) /\ (((exists fs_u_dst_assoc_rightfoldpositive fs_v_dst_assoc_rightfoldpositive. ((((exists fs_h_dst_assoc_rightfoldpositive_body_start. fs_h_dst_assoc_rightfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_rightfoldpositive)) /\ exists fs_q_dst_assoc_rightfoldpositive_body_start. fs_u_dst_assoc_rightfoldpositive = fs_q_dst_assoc_rightfoldpositive_body_start * S ((S (0)) * fs_v_dst_assoc_rightfoldpositive) + (0))) /\ ((((exists fs_h_dst_assoc_rightfoldpositive_body_terminal. fs_h_dst_assoc_rightfoldpositive_body_terminal + S (dst_positive_sum_assoc_rightfold) = S ((S (S (n))) * fs_v_dst_assoc_rightfoldpositive)) /\ exists fs_q_dst_assoc_rightfoldpositive_body_terminal. fs_u_dst_assoc_rightfoldpositive = fs_q_dst_assoc_rightfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_assoc_rightfoldpositive) + (dst_positive_sum_assoc_rightfold))) /\ forall fs_i_dst_assoc_rightfoldpositive_body_steps. (exists fs_lt_dst_assoc_rightfoldpositive_body_steps_bound. fs_lt_dst_assoc_rightfoldpositive_body_steps_bound + S fs_i_dst_assoc_rightfoldpositive_body_steps = S (n)) -> exists fs_a_dst_assoc_rightfoldpositive_body_steps fs_r_dst_assoc_rightfoldpositive_body_steps fs_s_dst_assoc_rightfoldpositive_body_steps. ((((exists fs_h_dst_assoc_rightfoldpositive_body_steps_summand. fs_h_dst_assoc_rightfoldpositive_body_steps_summand + S (fs_a_dst_assoc_rightfoldpositive_body_steps) = S ((S (fs_i_dst_assoc_rightfoldpositive_body_steps)) * dst_positive_scale_assoc_rightfold)) /\ exists fs_q_dst_assoc_rightfoldpositive_body_steps_summand. dst_positive_code_assoc_rightfold = fs_q_dst_assoc_rightfoldpositive_body_steps_summand * S ((S (fs_i_dst_assoc_rightfoldpositive_body_steps)) * dst_positive_scale_assoc_rightfold) + (fs_a_dst_assoc_rightfoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_rightfoldpositive_body_steps_partial. fs_h_dst_assoc_rightfoldpositive_body_steps_partial + S (fs_r_dst_assoc_rightfoldpositive_body_steps) = S ((S (fs_i_dst_assoc_rightfoldpositive_body_steps)) * fs_v_dst_assoc_rightfoldpositive)) /\ exists fs_q_dst_assoc_rightfoldpositive_body_steps_partial. fs_u_dst_assoc_rightfoldpositive = fs_q_dst_assoc_rightfoldpositive_body_steps_partial * S ((S (fs_i_dst_assoc_rightfoldpositive_body_steps)) * fs_v_dst_assoc_rightfoldpositive) + (fs_r_dst_assoc_rightfoldpositive_body_steps))) /\ ((((exists fs_h_dst_assoc_rightfoldpositive_body_steps_successor. fs_h_dst_assoc_rightfoldpositive_body_steps_successor + S (fs_s_dst_assoc_rightfoldpositive_body_steps) = S ((S (S fs_i_dst_assoc_rightfoldpositive_body_steps)) * fs_v_dst_assoc_rightfoldpositive)) /\ exists fs_q_dst_assoc_rightfoldpositive_body_steps_successor. fs_u_dst_assoc_rightfoldpositive = fs_q_dst_assoc_rightfoldpositive_body_steps_successor * S ((S (S fs_i_dst_assoc_rightfoldpositive_body_steps)) * fs_v_dst_assoc_rightfoldpositive) + (fs_s_dst_assoc_rightfoldpositive_body_steps))) /\ fs_s_dst_assoc_rightfoldpositive_body_steps = fs_r_dst_assoc_rightfoldpositive_body_steps + fs_a_dst_assoc_rightfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_assoc_rightfoldnegative fs_v_dst_assoc_rightfoldnegative. ((((exists fs_h_dst_assoc_rightfoldnegative_body_start. fs_h_dst_assoc_rightfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_assoc_rightfoldnegative)) /\ exists fs_q_dst_assoc_rightfoldnegative_body_start. fs_u_dst_assoc_rightfoldnegative = fs_q_dst_assoc_rightfoldnegative_body_start * S ((S (0)) * fs_v_dst_assoc_rightfoldnegative) + (0))) /\ ((((exists fs_h_dst_assoc_rightfoldnegative_body_terminal. fs_h_dst_assoc_rightfoldnegative_body_terminal + S (dst_negative_sum_assoc_rightfold) = S ((S (S (n))) * fs_v_dst_assoc_rightfoldnegative)) /\ exists fs_q_dst_assoc_rightfoldnegative_body_terminal. fs_u_dst_assoc_rightfoldnegative = fs_q_dst_assoc_rightfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_assoc_rightfoldnegative) + (dst_negative_sum_assoc_rightfold))) /\ forall fs_i_dst_assoc_rightfoldnegative_body_steps. (exists fs_lt_dst_assoc_rightfoldnegative_body_steps_bound. fs_lt_dst_assoc_rightfoldnegative_body_steps_bound + S fs_i_dst_assoc_rightfoldnegative_body_steps = S (n)) -> exists fs_a_dst_assoc_rightfoldnegative_body_steps fs_r_dst_assoc_rightfoldnegative_body_steps fs_s_dst_assoc_rightfoldnegative_body_steps. ((((exists fs_h_dst_assoc_rightfoldnegative_body_steps_summand. fs_h_dst_assoc_rightfoldnegative_body_steps_summand + S (fs_a_dst_assoc_rightfoldnegative_body_steps) = S ((S (fs_i_dst_assoc_rightfoldnegative_body_steps)) * dst_negative_scale_assoc_rightfold)) /\ exists fs_q_dst_assoc_rightfoldnegative_body_steps_summand. dst_negative_code_assoc_rightfold = fs_q_dst_assoc_rightfoldnegative_body_steps_summand * S ((S (fs_i_dst_assoc_rightfoldnegative_body_steps)) * dst_negative_scale_assoc_rightfold) + (fs_a_dst_assoc_rightfoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_rightfoldnegative_body_steps_partial. fs_h_dst_assoc_rightfoldnegative_body_steps_partial + S (fs_r_dst_assoc_rightfoldnegative_body_steps) = S ((S (fs_i_dst_assoc_rightfoldnegative_body_steps)) * fs_v_dst_assoc_rightfoldnegative)) /\ exists fs_q_dst_assoc_rightfoldnegative_body_steps_partial. fs_u_dst_assoc_rightfoldnegative = fs_q_dst_assoc_rightfoldnegative_body_steps_partial * S ((S (fs_i_dst_assoc_rightfoldnegative_body_steps)) * fs_v_dst_assoc_rightfoldnegative) + (fs_r_dst_assoc_rightfoldnegative_body_steps))) /\ ((((exists fs_h_dst_assoc_rightfoldnegative_body_steps_successor. fs_h_dst_assoc_rightfoldnegative_body_steps_successor + S (fs_s_dst_assoc_rightfoldnegative_body_steps) = S ((S (S fs_i_dst_assoc_rightfoldnegative_body_steps)) * fs_v_dst_assoc_rightfoldnegative)) /\ exists fs_q_dst_assoc_rightfoldnegative_body_steps_successor. fs_u_dst_assoc_rightfoldnegative = fs_q_dst_assoc_rightfoldnegative_body_steps_successor * S ((S (S fs_i_dst_assoc_rightfoldnegative_body_steps)) * fs_v_dst_assoc_rightfoldnegative) + (fs_s_dst_assoc_rightfoldnegative_body_steps))) /\ fs_s_dst_assoc_rightfoldnegative_body_steps = fs_r_dst_assoc_rightfoldnegative_body_steps + fs_a_dst_assoc_rightfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_assoc_rightfoldresult ge_balance_negative_assoc_rightfoldresult. (((((v) = 2 * (ge_balance_positive_assoc_rightfoldresult) /\ (ge_balance_negative_assoc_rightfoldresult) = 0) \/ exists ge_signed_half_assoc_rightfoldresultdecode. (((v) = 2 * ge_signed_half_assoc_rightfoldresultdecode + 1 /\ (ge_balance_positive_assoc_rightfoldresult) = 0) /\ (ge_balance_negative_assoc_rightfoldresult) = S ge_signed_half_assoc_rightfoldresultdecode))) /\ ((dst_positive_sum_assoc_rightfold) + ge_balance_negative_assoc_rightfoldresult = (dst_negative_sum_assoc_rightfold) + ge_balance_positive_assoc_rightfoldresult))))))))))))) -> u=vComplete tactic proof in conservative notation
All 51 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
51 script commands · 9 reading checkpoints · 0 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 (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–15
03Use earlier factsL16–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
specialize dirichlet_convolution_fubini_interchange (N) - L17
specialize dirichlet_convolution_fubini_interchange (H) - L18
specialize dirichlet_convolution_fubini_interchange (G) - L19
specialize dirichlet_convolution_fubini_interchange (F) - L20
specialize dirichlet_convolution_fubini_interchange (A) - L21
specialize dirichlet_convolution_fubini_interchange (B) - L22
specialize dirichlet_convolution_fubini_interchange (n) - L23
specialize dirichlet_convolution_fubini_interchange (u) - L24
specialize dirichlet_convolution_fubini_interchange (v) - L25
apply dirichlet_convolution_fubini_interchange
04Use earlier factsL26–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
exact hA - L27
specialize dirichlet_convolution_table_commutative (N) - L28
specialize dirichlet_convolution_table_commutative (G) - L29
specialize dirichlet_convolution_table_commutative (H) - L30
specialize dirichlet_convolution_table_commutative (B) - L31
apply dirichlet_convolution_table_commutative - L32
exact hB - L33
exact hn - L34
exact hN - L35
specialize dirichlet_convolution_sum_swap (N)
05Use earlier factsL36–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Separate the logical casesL41–43
07Use earlier factsL44–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
exact hA_right_right_left
08Separate the logical casesL45–47
Original defined command ledger · 51 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro A - 0006
intro B - 0007
intro n - 0008
intro u - 0009
intro v - 0010
intro hA - 0011
intro hB - 0012
intro hn - 0013
intro hN - 0014
intro hu - 0015
intro hv - 0016
specialize dirichlet_convolution_fubini_interchange (N) - 0017
specialize dirichlet_convolution_fubini_interchange (H) - 0018
specialize dirichlet_convolution_fubini_interchange (G) - 0019
specialize dirichlet_convolution_fubini_interchange (F) - 0020
specialize dirichlet_convolution_fubini_interchange (A) - 0021
specialize dirichlet_convolution_fubini_interchange (B) - 0022
specialize dirichlet_convolution_fubini_interchange (n) - 0023
specialize dirichlet_convolution_fubini_interchange (u) - 0024
specialize dirichlet_convolution_fubini_interchange (v) - 0025
apply dirichlet_convolution_fubini_interchange - 0026
exact hA - 0027
specialize dirichlet_convolution_table_commutative (N) - 0028
specialize dirichlet_convolution_table_commutative (G) - 0029
specialize dirichlet_convolution_table_commutative (H) - 0030
specialize dirichlet_convolution_table_commutative (B) - 0031
apply dirichlet_convolution_table_commutative - 0032
exact hB - 0033
exact hn - 0034
exact hN - 0035
specialize dirichlet_convolution_sum_swap (N) - 0036
specialize dirichlet_convolution_sum_swap (A) - 0037
specialize dirichlet_convolution_sum_swap (H) - 0038
specialize dirichlet_convolution_sum_swap (n) - 0039
specialize dirichlet_convolution_sum_swap (u) - 0040
apply dirichlet_convolution_sum_swap - 0041
cases hA - 0042
cases hA_right - 0043
cases hA_right_right - 0044
exact hA_right_right_left - 0045
cases hB - 0046
cases hB_right - 0047
cases hB_right_right - 0048
exact hB_right_left - 0049
exact hN - 0050
exact hu - 0051
exact hv