DF001D

dirichlet_convolution_fubini_interchange

Actual first/last-factor grid construction and finite Fubini prove F*(H*G)=H*(F*G) at every positive in-domain index; neither a pair permutation nor a rearrangement oracle is supplied.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

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. ∀ U. ∀ V. ∀ n. ∀ a. ∀ b. DirichletTable(N,H,G,U) → DirichletTable(N,F,G,V) → ¬n = 0 → Le(n,N) → DirichletSum(F,U,n,a) → DirichletSum(H,V,n,b) → a = b

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedPrefixSum(F,l,z) · 2ArithRowSums(F,R,o,s,t,m,n) · 2DirichletSum(F,G,n,z) · 2DirichletTable(N,F,G,H) · 2DirichletGrid(F,G,H,n,T) · 1Le(a,b) · 1

Actual proof prerequisites

dirichlet_grid_fubini_existssigned_table_domain_resize · checked external prerequisitedirichlet_convolution_sum_functional · checked external prerequisitedirichlet_grid_row_sums_convolution_prefixdirichlet_grid_column_sums_convolution_prefix
Original expanded first-order statement 
forall N F G H U V n a b. (((exists dst_positive_code_interchange_HGleft dst_positive_scale_interchange_HGleft dst_negative_code_interchange_HGleft dst_negative_scale_interchange_HGleft. (((H) = (((((dst_positive_code_interchange_HGleft) + (dst_positive_scale_interchange_HGleft)) * S ((dst_positive_code_interchange_HGleft) + (dst_positive_scale_interchange_HGleft)) + ((dst_positive_scale_interchange_HGleft) + (dst_positive_scale_interchange_HGleft))) + (((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) * S ((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) + ((dst_negative_scale_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)))) * S ((((dst_positive_code_interchange_HGleft) + (dst_positive_scale_interchange_HGleft)) * S ((dst_positive_code_interchange_HGleft) + (dst_positive_scale_interchange_HGleft)) + ((dst_positive_scale_interchange_HGleft) + (dst_positive_scale_interchange_HGleft))) + (((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) * S ((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) + ((dst_negative_scale_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)))) + ((((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) * S ((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) + ((dst_negative_scale_interchange_HGleft) + (dst_negative_scale_interchange_HGleft))) + (((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) * S ((dst_negative_code_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)) + ((dst_negative_scale_interchange_HGleft) + (dst_negative_scale_interchange_HGleft)))))) /\ (forall dst_index_interchange_HGleft. (exists pvs_le_gap_interchange_HGleftdomain. pvs_le_gap_interchange_HGleftdomain + (dst_index_interchange_HGleft) = (N)) -> exists dst_positive_interchange_HGleft dst_negative_interchange_HGleft dst_value_interchange_HGleft. ((((exists ff_h_pvs_interchange_HGleftentrypositive. ff_h_pvs_interchange_HGleftentrypositive + S (dst_positive_interchange_HGleft) = S ((S (dst_index_interchange_HGleft)) * dst_positive_scale_interchange_HGleft)) /\ exists ff_q_pvs_interchange_HGleftentrypositive. dst_positive_code_interchange_HGleft = ff_q_pvs_interchange_HGleftentrypositive * S ((S (dst_index_interchange_HGleft)) * dst_positive_scale_interchange_HGleft) + (dst_positive_interchange_HGleft))) /\ (((((exists ff_h_pvs_interchange_HGleftentrynegative. ff_h_pvs_interchange_HGleftentrynegative + S (dst_negative_interchange_HGleft) = S ((S (dst_index_interchange_HGleft)) * dst_negative_scale_interchange_HGleft)) /\ exists ff_q_pvs_interchange_HGleftentrynegative. dst_negative_code_interchange_HGleft = ff_q_pvs_interchange_HGleftentrynegative * S ((S (dst_index_interchange_HGleft)) * dst_negative_scale_interchange_HGleft) + (dst_negative_interchange_HGleft))) /\ (exists ge_balance_positive_interchange_HGleftentryvalue ge_balance_negative_interchange_HGleftentryvalue. (((((dst_value_interchange_HGleft) = 2 * (ge_balance_positive_interchange_HGleftentryvalue) /\ (ge_balance_negative_interchange_HGleftentryvalue) = 0) \/ exists ge_signed_half_interchange_HGleftentryvaluedecode. (((dst_value_interchange_HGleft) = 2 * ge_signed_half_interchange_HGleftentryvaluedecode + 1 /\ (ge_balance_positive_interchange_HGleftentryvalue) = 0) /\ (ge_balance_negative_interchange_HGleftentryvalue) = S ge_signed_half_interchange_HGleftentryvaluedecode))) /\ ((dst_positive_interchange_HGleft) + ge_balance_negative_interchange_HGleftentryvalue = (dst_negative_interchange_HGleft) + ge_balance_positive_interchange_HGleftentryvalue))))))))) /\ (((exists dst_positive_code_interchange_HGright dst_positive_scale_interchange_HGright dst_negative_code_interchange_HGright dst_negative_scale_interchange_HGright. (((G) = (((((dst_positive_code_interchange_HGright) + (dst_positive_scale_interchange_HGright)) * S ((dst_positive_code_interchange_HGright) + (dst_positive_scale_interchange_HGright)) + ((dst_positive_scale_interchange_HGright) + (dst_positive_scale_interchange_HGright))) + (((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) * S ((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) + ((dst_negative_scale_interchange_HGright) + (dst_negative_scale_interchange_HGright)))) * S ((((dst_positive_code_interchange_HGright) + (dst_positive_scale_interchange_HGright)) * S ((dst_positive_code_interchange_HGright) + (dst_positive_scale_interchange_HGright)) + ((dst_positive_scale_interchange_HGright) + (dst_positive_scale_interchange_HGright))) + (((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) * S ((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) + ((dst_negative_scale_interchange_HGright) + (dst_negative_scale_interchange_HGright)))) + ((((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) * S ((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) + ((dst_negative_scale_interchange_HGright) + (dst_negative_scale_interchange_HGright))) + (((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) * S ((dst_negative_code_interchange_HGright) + (dst_negative_scale_interchange_HGright)) + ((dst_negative_scale_interchange_HGright) + (dst_negative_scale_interchange_HGright)))))) /\ (forall dst_index_interchange_HGright. (exists pvs_le_gap_interchange_HGrightdomain. pvs_le_gap_interchange_HGrightdomain + (dst_index_interchange_HGright) = (N)) -> exists dst_positive_interchange_HGright dst_negative_interchange_HGright dst_value_interchange_HGright. ((((exists ff_h_pvs_interchange_HGrightentrypositive. ff_h_pvs_interchange_HGrightentrypositive + S (dst_positive_interchange_HGright) = S ((S (dst_index_interchange_HGright)) * dst_positive_scale_interchange_HGright)) /\ exists ff_q_pvs_interchange_HGrightentrypositive. dst_positive_code_interchange_HGright = ff_q_pvs_interchange_HGrightentrypositive * S ((S (dst_index_interchange_HGright)) * dst_positive_scale_interchange_HGright) + (dst_positive_interchange_HGright))) /\ (((((exists ff_h_pvs_interchange_HGrightentrynegative. ff_h_pvs_interchange_HGrightentrynegative + S (dst_negative_interchange_HGright) = S ((S (dst_index_interchange_HGright)) * dst_negative_scale_interchange_HGright)) /\ exists ff_q_pvs_interchange_HGrightentrynegative. dst_negative_code_interchange_HGright = ff_q_pvs_interchange_HGrightentrynegative * S ((S (dst_index_interchange_HGright)) * dst_negative_scale_interchange_HGright) + (dst_negative_interchange_HGright))) /\ (exists ge_balance_positive_interchange_HGrightentryvalue ge_balance_negative_interchange_HGrightentryvalue. (((((dst_value_interchange_HGright) = 2 * (ge_balance_positive_interchange_HGrightentryvalue) /\ (ge_balance_negative_interchange_HGrightentryvalue) = 0) \/ exists ge_signed_half_interchange_HGrightentryvaluedecode. (((dst_value_interchange_HGright) = 2 * ge_signed_half_interchange_HGrightentryvaluedecode + 1 /\ (ge_balance_positive_interchange_HGrightentryvalue) = 0) /\ (ge_balance_negative_interchange_HGrightentryvalue) = S ge_signed_half_interchange_HGrightentryvaluedecode))) /\ ((dst_positive_interchange_HGright) + ge_balance_negative_interchange_HGrightentryvalue = (dst_negative_interchange_HGright) + ge_balance_positive_interchange_HGrightentryvalue))))))))) /\ (((exists dst_positive_code_interchange_HGtable dst_positive_scale_interchange_HGtable dst_negative_code_interchange_HGtable dst_negative_scale_interchange_HGtable. (((U) = (((((dst_positive_code_interchange_HGtable) + (dst_positive_scale_interchange_HGtable)) * S ((dst_positive_code_interchange_HGtable) + (dst_positive_scale_interchange_HGtable)) + ((dst_positive_scale_interchange_HGtable) + (dst_positive_scale_interchange_HGtable))) + (((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) * S ((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) + ((dst_negative_scale_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)))) * S ((((dst_positive_code_interchange_HGtable) + (dst_positive_scale_interchange_HGtable)) * S ((dst_positive_code_interchange_HGtable) + (dst_positive_scale_interchange_HGtable)) + ((dst_positive_scale_interchange_HGtable) + (dst_positive_scale_interchange_HGtable))) + (((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) * S ((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) + ((dst_negative_scale_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)))) + ((((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) * S ((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) + ((dst_negative_scale_interchange_HGtable) + (dst_negative_scale_interchange_HGtable))) + (((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) * S ((dst_negative_code_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)) + ((dst_negative_scale_interchange_HGtable) + (dst_negative_scale_interchange_HGtable)))))) /\ (forall dst_index_interchange_HGtable. (exists pvs_le_gap_interchange_HGtabledomain. pvs_le_gap_interchange_HGtabledomain + (dst_index_interchange_HGtable) = (N)) -> exists dst_positive_interchange_HGtable dst_negative_interchange_HGtable dst_value_interchange_HGtable. ((((exists ff_h_pvs_interchange_HGtableentrypositive. ff_h_pvs_interchange_HGtableentrypositive + S (dst_positive_interchange_HGtable) = S ((S (dst_index_interchange_HGtable)) * dst_positive_scale_interchange_HGtable)) /\ exists ff_q_pvs_interchange_HGtableentrypositive. dst_positive_code_interchange_HGtable = ff_q_pvs_interchange_HGtableentrypositive * S ((S (dst_index_interchange_HGtable)) * dst_positive_scale_interchange_HGtable) + (dst_positive_interchange_HGtable))) /\ (((((exists ff_h_pvs_interchange_HGtableentrynegative. ff_h_pvs_interchange_HGtableentrynegative + S (dst_negative_interchange_HGtable) = S ((S (dst_index_interchange_HGtable)) * dst_negative_scale_interchange_HGtable)) /\ exists ff_q_pvs_interchange_HGtableentrynegative. dst_negative_code_interchange_HGtable = ff_q_pvs_interchange_HGtableentrynegative * S ((S (dst_index_interchange_HGtable)) * dst_negative_scale_interchange_HGtable) + (dst_negative_interchange_HGtable))) /\ (exists ge_balance_positive_interchange_HGtableentryvalue ge_balance_negative_interchange_HGtableentryvalue. (((((dst_value_interchange_HGtable) = 2 * (ge_balance_positive_interchange_HGtableentryvalue) /\ (ge_balance_negative_interchange_HGtableentryvalue) = 0) \/ exists ge_signed_half_interchange_HGtableentryvaluedecode. (((dst_value_interchange_HGtable) = 2 * ge_signed_half_interchange_HGtableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_HGtableentryvalue) = 0) /\ (ge_balance_negative_interchange_HGtableentryvalue) = S ge_signed_half_interchange_HGtableentryvaluedecode))) /\ ((dst_positive_interchange_HGtable) + ge_balance_negative_interchange_HGtableentryvalue = (dst_negative_interchange_HGtable) + ge_balance_positive_interchange_HGtableentryvalue))))))))) /\ (forall dc_input_interchange_HG dc_output_interchange_HG. ~(dc_input_interchange_HG=0) -> (exists pvs_le_gap_interchange_HGdomain. pvs_le_gap_interchange_HGdomain + (dc_input_interchange_HG) = (N)) -> (exists dst_positive_code_interchange_HGlookup dst_positive_scale_interchange_HGlookup dst_negative_code_interchange_HGlookup dst_negative_scale_interchange_HGlookup dst_positive_interchange_HGlookup dst_negative_interchange_HGlookup. (((U) = (((((dst_positive_code_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup)) * S ((dst_positive_code_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup)) + ((dst_positive_scale_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup))) + (((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) * S ((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) + ((dst_negative_scale_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)))) * S ((((dst_positive_code_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup)) * S ((dst_positive_code_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup)) + ((dst_positive_scale_interchange_HGlookup) + (dst_positive_scale_interchange_HGlookup))) + (((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) * S ((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) + ((dst_negative_scale_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)))) + ((((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) * S ((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) + ((dst_negative_scale_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup))) + (((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) * S ((dst_negative_code_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)) + ((dst_negative_scale_interchange_HGlookup) + (dst_negative_scale_interchange_HGlookup)))))) /\ (((((exists ff_h_pvs_interchange_HGlookuppositive. ff_h_pvs_interchange_HGlookuppositive + S (dst_positive_interchange_HGlookup) = S ((S (dc_input_interchange_HG)) * dst_positive_scale_interchange_HGlookup)) /\ exists ff_q_pvs_interchange_HGlookuppositive. dst_positive_code_interchange_HGlookup = ff_q_pvs_interchange_HGlookuppositive * S ((S (dc_input_interchange_HG)) * dst_positive_scale_interchange_HGlookup) + (dst_positive_interchange_HGlookup))) /\ (((((exists ff_h_pvs_interchange_HGlookupnegative. ff_h_pvs_interchange_HGlookupnegative + S (dst_negative_interchange_HGlookup) = S ((S (dc_input_interchange_HG)) * dst_negative_scale_interchange_HGlookup)) /\ exists ff_q_pvs_interchange_HGlookupnegative. dst_negative_code_interchange_HGlookup = ff_q_pvs_interchange_HGlookupnegative * S ((S (dc_input_interchange_HG)) * dst_negative_scale_interchange_HGlookup) + (dst_negative_interchange_HGlookup))) /\ (exists ge_balance_positive_interchange_HGlookupvalue ge_balance_negative_interchange_HGlookupvalue. (((((dc_output_interchange_HG) = 2 * (ge_balance_positive_interchange_HGlookupvalue) /\ (ge_balance_negative_interchange_HGlookupvalue) = 0) \/ exists ge_signed_half_interchange_HGlookupvaluedecode. (((dc_output_interchange_HG) = 2 * ge_signed_half_interchange_HGlookupvaluedecode + 1 /\ (ge_balance_positive_interchange_HGlookupvalue) = 0) /\ (ge_balance_negative_interchange_HGlookupvalue) = S ge_signed_half_interchange_HGlookupvaluedecode))) /\ ((dst_positive_interchange_HGlookup) + ge_balance_negative_interchange_HGlookupvalue = (dst_negative_interchange_HGlookup) + ge_balance_positive_interchange_HGlookupvalue))))))))) -> (((~((dc_input_interchange_HG)=0)) /\ (exists dc_mask_interchange_HGvalue. ((((exists dst_positive_code_interchange_HGvaluemasktable dst_positive_scale_interchange_HGvaluemasktable dst_negative_code_interchange_HGvaluemasktable dst_negative_scale_interchange_HGvaluemasktable. (((dc_mask_interchange_HGvalue) = (((((dst_positive_code_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable)) * S ((dst_positive_code_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable)) + ((dst_positive_scale_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable))) + (((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) * S ((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) + ((dst_negative_scale_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)))) * S ((((dst_positive_code_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable)) * S ((dst_positive_code_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable)) + ((dst_positive_scale_interchange_HGvaluemasktable) + (dst_positive_scale_interchange_HGvaluemasktable))) + (((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) * S ((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) + ((dst_negative_scale_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)))) + ((((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) * S ((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) + ((dst_negative_scale_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable))) + (((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) * S ((dst_negative_code_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)) + ((dst_negative_scale_interchange_HGvaluemasktable) + (dst_negative_scale_interchange_HGvaluemasktable)))))) /\ (forall dst_index_interchange_HGvaluemasktable. (exists pvs_le_gap_interchange_HGvaluemasktabledomain. pvs_le_gap_interchange_HGvaluemasktabledomain + (dst_index_interchange_HGvaluemasktable) = (dc_input_interchange_HG)) -> exists dst_positive_interchange_HGvaluemasktable dst_negative_interchange_HGvaluemasktable dst_value_interchange_HGvaluemasktable. ((((exists ff_h_pvs_interchange_HGvaluemasktableentrypositive. ff_h_pvs_interchange_HGvaluemasktableentrypositive + S (dst_positive_interchange_HGvaluemasktable) = S ((S (dst_index_interchange_HGvaluemasktable)) * dst_positive_scale_interchange_HGvaluemasktable)) /\ exists ff_q_pvs_interchange_HGvaluemasktableentrypositive. dst_positive_code_interchange_HGvaluemasktable = ff_q_pvs_interchange_HGvaluemasktableentrypositive * S ((S (dst_index_interchange_HGvaluemasktable)) * dst_positive_scale_interchange_HGvaluemasktable) + (dst_positive_interchange_HGvaluemasktable))) /\ (((((exists ff_h_pvs_interchange_HGvaluemasktableentrynegative. ff_h_pvs_interchange_HGvaluemasktableentrynegative + S (dst_negative_interchange_HGvaluemasktable) = S ((S (dst_index_interchange_HGvaluemasktable)) * dst_negative_scale_interchange_HGvaluemasktable)) /\ exists ff_q_pvs_interchange_HGvaluemasktableentrynegative. dst_negative_code_interchange_HGvaluemasktable = ff_q_pvs_interchange_HGvaluemasktableentrynegative * S ((S (dst_index_interchange_HGvaluemasktable)) * dst_negative_scale_interchange_HGvaluemasktable) + (dst_negative_interchange_HGvaluemasktable))) /\ (exists ge_balance_positive_interchange_HGvaluemasktableentryvalue ge_balance_negative_interchange_HGvaluemasktableentryvalue. (((((dst_value_interchange_HGvaluemasktable) = 2 * (ge_balance_positive_interchange_HGvaluemasktableentryvalue) /\ (ge_balance_negative_interchange_HGvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_interchange_HGvaluemasktableentryvaluedecode. (((dst_value_interchange_HGvaluemasktable) = 2 * ge_signed_half_interchange_HGvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_HGvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_interchange_HGvaluemasktableentryvalue) = S ge_signed_half_interchange_HGvaluemasktableentryvaluedecode))) /\ ((dst_positive_interchange_HGvaluemasktable) + ge_balance_negative_interchange_HGvaluemasktableentryvalue = (dst_negative_interchange_HGvaluemasktable) + ge_balance_positive_interchange_HGvaluemasktableentryvalue))))))))) /\ (forall dc_index_interchange_HGvaluemask dc_value_interchange_HGvaluemask. (exists pvs_le_gap_interchange_HGvaluemaskdomain. pvs_le_gap_interchange_HGvaluemaskdomain + (dc_index_interchange_HGvaluemask) = (dc_input_interchange_HG)) -> (exists dst_positive_code_interchange_HGvaluemasklookup dst_positive_scale_interchange_HGvaluemasklookup dst_negative_code_interchange_HGvaluemasklookup dst_negative_scale_interchange_HGvaluemasklookup dst_positive_interchange_HGvaluemasklookup dst_negative_interchange_HGvaluemasklookup. (((dc_mask_interchange_HGvalue) = (((((dst_positive_code_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup)) * S ((dst_positive_code_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup)) + ((dst_positive_scale_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup))) + (((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) * S ((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) + ((dst_negative_scale_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)))) * S ((((dst_positive_code_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup)) * S ((dst_positive_code_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup)) + ((dst_positive_scale_interchange_HGvaluemasklookup) + (dst_positive_scale_interchange_HGvaluemasklookup))) + (((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) * S ((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) + ((dst_negative_scale_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)))) + ((((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) * S ((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) + ((dst_negative_scale_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup))) + (((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) * S ((dst_negative_code_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)) + ((dst_negative_scale_interchange_HGvaluemasklookup) + (dst_negative_scale_interchange_HGvaluemasklookup)))))) /\ (((((exists ff_h_pvs_interchange_HGvaluemasklookuppositive. ff_h_pvs_interchange_HGvaluemasklookuppositive + S (dst_positive_interchange_HGvaluemasklookup) = S ((S (dc_index_interchange_HGvaluemask)) * dst_positive_scale_interchange_HGvaluemasklookup)) /\ exists ff_q_pvs_interchange_HGvaluemasklookuppositive. dst_positive_code_interchange_HGvaluemasklookup = ff_q_pvs_interchange_HGvaluemasklookuppositive * S ((S (dc_index_interchange_HGvaluemask)) * dst_positive_scale_interchange_HGvaluemasklookup) + (dst_positive_interchange_HGvaluemasklookup))) /\ (((((exists ff_h_pvs_interchange_HGvaluemasklookupnegative. ff_h_pvs_interchange_HGvaluemasklookupnegative + S (dst_negative_interchange_HGvaluemasklookup) = S ((S (dc_index_interchange_HGvaluemask)) * dst_negative_scale_interchange_HGvaluemasklookup)) /\ exists ff_q_pvs_interchange_HGvaluemasklookupnegative. dst_negative_code_interchange_HGvaluemasklookup = ff_q_pvs_interchange_HGvaluemasklookupnegative * S ((S (dc_index_interchange_HGvaluemask)) * dst_negative_scale_interchange_HGvaluemasklookup) + (dst_negative_interchange_HGvaluemasklookup))) /\ (exists ge_balance_positive_interchange_HGvaluemasklookupvalue ge_balance_negative_interchange_HGvaluemasklookupvalue. (((((dc_value_interchange_HGvaluemask) = 2 * (ge_balance_positive_interchange_HGvaluemasklookupvalue) /\ (ge_balance_negative_interchange_HGvaluemasklookupvalue) = 0) \/ exists ge_signed_half_interchange_HGvaluemasklookupvaluedecode. (((dc_value_interchange_HGvaluemask) = 2 * ge_signed_half_interchange_HGvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_interchange_HGvaluemasklookupvalue) = 0) /\ (ge_balance_negative_interchange_HGvaluemasklookupvalue) = S ge_signed_half_interchange_HGvaluemasklookupvaluedecode))) /\ ((dst_positive_interchange_HGvaluemasklookup) + ge_balance_negative_interchange_HGvaluemasklookupvalue = (dst_negative_interchange_HGvaluemasklookup) + ge_balance_positive_interchange_HGvaluemasklookupvalue))))))))) -> ((((~((dc_index_interchange_HGvaluemask)=0)) /\ (exists dc_quotient_interchange_HGvaluemaskentry dc_left_interchange_HGvaluemaskentry dc_right_interchange_HGvaluemaskentry. (((dc_input_interchange_HG)=(dc_index_interchange_HGvaluemask)*dc_quotient_interchange_HGvaluemaskentry) /\ (((exists dst_positive_code_interchange_HGvaluemaskentryleft dst_positive_scale_interchange_HGvaluemaskentryleft dst_negative_code_interchange_HGvaluemaskentryleft dst_negative_scale_interchange_HGvaluemaskentryleft dst_positive_interchange_HGvaluemaskentryleft dst_negative_interchange_HGvaluemaskentryleft. (((H) = (((((dst_positive_code_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft)) * S ((dst_positive_code_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft)) + ((dst_positive_scale_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft))) + (((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) * S ((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) + ((dst_negative_scale_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)))) * S ((((dst_positive_code_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft)) * S ((dst_positive_code_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft)) + ((dst_positive_scale_interchange_HGvaluemaskentryleft) + (dst_positive_scale_interchange_HGvaluemaskentryleft))) + (((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) * S ((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) + ((dst_negative_scale_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)))) + ((((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) * S ((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) + ((dst_negative_scale_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft))) + (((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) * S ((dst_negative_code_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)) + ((dst_negative_scale_interchange_HGvaluemaskentryleft) + (dst_negative_scale_interchange_HGvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_interchange_HGvaluemaskentryleftpositive. ff_h_pvs_interchange_HGvaluemaskentryleftpositive + S (dst_positive_interchange_HGvaluemaskentryleft) = S ((S (dc_index_interchange_HGvaluemask)) * dst_positive_scale_interchange_HGvaluemaskentryleft)) /\ exists ff_q_pvs_interchange_HGvaluemaskentryleftpositive. dst_positive_code_interchange_HGvaluemaskentryleft = ff_q_pvs_interchange_HGvaluemaskentryleftpositive * S ((S (dc_index_interchange_HGvaluemask)) * dst_positive_scale_interchange_HGvaluemaskentryleft) + (dst_positive_interchange_HGvaluemaskentryleft))) /\ (((((exists ff_h_pvs_interchange_HGvaluemaskentryleftnegative. ff_h_pvs_interchange_HGvaluemaskentryleftnegative + S (dst_negative_interchange_HGvaluemaskentryleft) = S ((S (dc_index_interchange_HGvaluemask)) * dst_negative_scale_interchange_HGvaluemaskentryleft)) /\ exists ff_q_pvs_interchange_HGvaluemaskentryleftnegative. dst_negative_code_interchange_HGvaluemaskentryleft = ff_q_pvs_interchange_HGvaluemaskentryleftnegative * S ((S (dc_index_interchange_HGvaluemask)) * dst_negative_scale_interchange_HGvaluemaskentryleft) + (dst_negative_interchange_HGvaluemaskentryleft))) /\ (exists ge_balance_positive_interchange_HGvaluemaskentryleftvalue ge_balance_negative_interchange_HGvaluemaskentryleftvalue. (((((dc_left_interchange_HGvaluemaskentry) = 2 * (ge_balance_positive_interchange_HGvaluemaskentryleftvalue) /\ (ge_balance_negative_interchange_HGvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_interchange_HGvaluemaskentryleftvaluedecode. (((dc_left_interchange_HGvaluemaskentry) = 2 * ge_signed_half_interchange_HGvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_interchange_HGvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_interchange_HGvaluemaskentryleftvalue) = S ge_signed_half_interchange_HGvaluemaskentryleftvaluedecode))) /\ ((dst_positive_interchange_HGvaluemaskentryleft) + ge_balance_negative_interchange_HGvaluemaskentryleftvalue = (dst_negative_interchange_HGvaluemaskentryleft) + ge_balance_positive_interchange_HGvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_interchange_HGvaluemaskentryright dst_positive_scale_interchange_HGvaluemaskentryright dst_negative_code_interchange_HGvaluemaskentryright dst_negative_scale_interchange_HGvaluemaskentryright dst_positive_interchange_HGvaluemaskentryright dst_negative_interchange_HGvaluemaskentryright. (((G) = (((((dst_positive_code_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright)) * S ((dst_positive_code_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright)) + ((dst_positive_scale_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright))) + (((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) * S ((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) + ((dst_negative_scale_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)))) * S ((((dst_positive_code_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright)) * S ((dst_positive_code_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright)) + ((dst_positive_scale_interchange_HGvaluemaskentryright) + (dst_positive_scale_interchange_HGvaluemaskentryright))) + (((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) * S ((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) + ((dst_negative_scale_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)))) + ((((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) * S ((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) + ((dst_negative_scale_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright))) + (((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) * S ((dst_negative_code_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)) + ((dst_negative_scale_interchange_HGvaluemaskentryright) + (dst_negative_scale_interchange_HGvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_interchange_HGvaluemaskentryrightpositive. ff_h_pvs_interchange_HGvaluemaskentryrightpositive + S (dst_positive_interchange_HGvaluemaskentryright) = S ((S (dc_quotient_interchange_HGvaluemaskentry)) * dst_positive_scale_interchange_HGvaluemaskentryright)) /\ exists ff_q_pvs_interchange_HGvaluemaskentryrightpositive. dst_positive_code_interchange_HGvaluemaskentryright = ff_q_pvs_interchange_HGvaluemaskentryrightpositive * S ((S (dc_quotient_interchange_HGvaluemaskentry)) * dst_positive_scale_interchange_HGvaluemaskentryright) + (dst_positive_interchange_HGvaluemaskentryright))) /\ (((((exists ff_h_pvs_interchange_HGvaluemaskentryrightnegative. ff_h_pvs_interchange_HGvaluemaskentryrightnegative + S (dst_negative_interchange_HGvaluemaskentryright) = S ((S (dc_quotient_interchange_HGvaluemaskentry)) * dst_negative_scale_interchange_HGvaluemaskentryright)) /\ exists ff_q_pvs_interchange_HGvaluemaskentryrightnegative. dst_negative_code_interchange_HGvaluemaskentryright = ff_q_pvs_interchange_HGvaluemaskentryrightnegative * S ((S (dc_quotient_interchange_HGvaluemaskentry)) * dst_negative_scale_interchange_HGvaluemaskentryright) + (dst_negative_interchange_HGvaluemaskentryright))) /\ (exists ge_balance_positive_interchange_HGvaluemaskentryrightvalue ge_balance_negative_interchange_HGvaluemaskentryrightvalue. (((((dc_right_interchange_HGvaluemaskentry) = 2 * (ge_balance_positive_interchange_HGvaluemaskentryrightvalue) /\ (ge_balance_negative_interchange_HGvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_interchange_HGvaluemaskentryrightvaluedecode. (((dc_right_interchange_HGvaluemaskentry) = 2 * ge_signed_half_interchange_HGvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_interchange_HGvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_interchange_HGvaluemaskentryrightvalue) = S ge_signed_half_interchange_HGvaluemaskentryrightvaluedecode))) /\ ((dst_positive_interchange_HGvaluemaskentryright) + ge_balance_negative_interchange_HGvaluemaskentryrightvalue = (dst_negative_interchange_HGvaluemaskentryright) + ge_balance_positive_interchange_HGvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_interchange_HGvaluemaskentryproduct sto_an_interchange_HGvaluemaskentryproduct sto_bp_interchange_HGvaluemaskentryproduct sto_bn_interchange_HGvaluemaskentryproduct sto_cp_interchange_HGvaluemaskentryproduct sto_cn_interchange_HGvaluemaskentryproduct. (((((dc_left_interchange_HGvaluemaskentry) = 2 * (sto_ap_interchange_HGvaluemaskentryproduct) /\ (sto_an_interchange_HGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_HGvaluemaskentryproductleft. (((dc_left_interchange_HGvaluemaskentry) = 2 * ge_signed_half_interchange_HGvaluemaskentryproductleft + 1 /\ (sto_ap_interchange_HGvaluemaskentryproduct) = 0) /\ (sto_an_interchange_HGvaluemaskentryproduct) = S ge_signed_half_interchange_HGvaluemaskentryproductleft))) /\ ((((((dc_right_interchange_HGvaluemaskentry) = 2 * (sto_bp_interchange_HGvaluemaskentryproduct) /\ (sto_bn_interchange_HGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_HGvaluemaskentryproductright. (((dc_right_interchange_HGvaluemaskentry) = 2 * ge_signed_half_interchange_HGvaluemaskentryproductright + 1 /\ (sto_bp_interchange_HGvaluemaskentryproduct) = 0) /\ (sto_bn_interchange_HGvaluemaskentryproduct) = S ge_signed_half_interchange_HGvaluemaskentryproductright))) /\ ((((((dc_value_interchange_HGvaluemask) = 2 * (sto_cp_interchange_HGvaluemaskentryproduct) /\ (sto_cn_interchange_HGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_HGvaluemaskentryproductoutput. (((dc_value_interchange_HGvaluemask) = 2 * ge_signed_half_interchange_HGvaluemaskentryproductoutput + 1 /\ (sto_cp_interchange_HGvaluemaskentryproduct) = 0) /\ (sto_cn_interchange_HGvaluemaskentryproduct) = S ge_signed_half_interchange_HGvaluemaskentryproductoutput))) /\ ((sto_ap_interchange_HGvaluemaskentryproduct * sto_bp_interchange_HGvaluemaskentryproduct + sto_an_interchange_HGvaluemaskentryproduct * sto_bn_interchange_HGvaluemaskentryproduct) + sto_cn_interchange_HGvaluemaskentryproduct = (sto_ap_interchange_HGvaluemaskentryproduct * sto_bn_interchange_HGvaluemaskentryproduct + sto_an_interchange_HGvaluemaskentryproduct * sto_bp_interchange_HGvaluemaskentryproduct) + sto_cp_interchange_HGvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_interchange_HGvaluemask)=0 \/ ~(exists pvs_factor_interchange_HGvaluemaskentrynondivisor. (dc_input_interchange_HG) = (dc_index_interchange_HGvaluemask) * pvs_factor_interchange_HGvaluemaskentrynondivisor)) /\ ((dc_value_interchange_HGvaluemask)=0))))))) /\ (exists dst_positive_code_interchange_HGvaluefold dst_positive_scale_interchange_HGvaluefold dst_negative_code_interchange_HGvaluefold dst_negative_scale_interchange_HGvaluefold dst_positive_sum_interchange_HGvaluefold dst_negative_sum_interchange_HGvaluefold. (((dc_mask_interchange_HGvalue) = (((((dst_positive_code_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold)) * S ((dst_positive_code_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold)) + ((dst_positive_scale_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold))) + (((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) * S ((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) + ((dst_negative_scale_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)))) * S ((((dst_positive_code_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold)) * S ((dst_positive_code_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold)) + ((dst_positive_scale_interchange_HGvaluefold) + (dst_positive_scale_interchange_HGvaluefold))) + (((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) * S ((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) + ((dst_negative_scale_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)))) + ((((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) * S ((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) + ((dst_negative_scale_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold))) + (((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) * S ((dst_negative_code_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)) + ((dst_negative_scale_interchange_HGvaluefold) + (dst_negative_scale_interchange_HGvaluefold)))))) /\ (((exists fs_u_dst_interchange_HGvaluefoldpositive fs_v_dst_interchange_HGvaluefoldpositive. ((((exists fs_h_dst_interchange_HGvaluefoldpositive_body_start. fs_h_dst_interchange_HGvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_HGvaluefoldpositive)) /\ exists fs_q_dst_interchange_HGvaluefoldpositive_body_start. fs_u_dst_interchange_HGvaluefoldpositive = fs_q_dst_interchange_HGvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_interchange_HGvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldpositive_body_terminal. fs_h_dst_interchange_HGvaluefoldpositive_body_terminal + S (dst_positive_sum_interchange_HGvaluefold) = S ((S (S (dc_input_interchange_HG))) * fs_v_dst_interchange_HGvaluefoldpositive)) /\ exists fs_q_dst_interchange_HGvaluefoldpositive_body_terminal. fs_u_dst_interchange_HGvaluefoldpositive = fs_q_dst_interchange_HGvaluefoldpositive_body_terminal * S ((S (S (dc_input_interchange_HG))) * fs_v_dst_interchange_HGvaluefoldpositive) + (dst_positive_sum_interchange_HGvaluefold))) /\ forall fs_i_dst_interchange_HGvaluefoldpositive_body_steps. (exists fs_lt_dst_interchange_HGvaluefoldpositive_body_steps_bound. fs_lt_dst_interchange_HGvaluefoldpositive_body_steps_bound + S fs_i_dst_interchange_HGvaluefoldpositive_body_steps = S (dc_input_interchange_HG)) -> exists fs_a_dst_interchange_HGvaluefoldpositive_body_steps fs_r_dst_interchange_HGvaluefoldpositive_body_steps fs_s_dst_interchange_HGvaluefoldpositive_body_steps. ((((exists fs_h_dst_interchange_HGvaluefoldpositive_body_steps_summand. fs_h_dst_interchange_HGvaluefoldpositive_body_steps_summand + S (fs_a_dst_interchange_HGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * dst_positive_scale_interchange_HGvaluefold)) /\ exists fs_q_dst_interchange_HGvaluefoldpositive_body_steps_summand. dst_positive_code_interchange_HGvaluefold = fs_q_dst_interchange_HGvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * dst_positive_scale_interchange_HGvaluefold) + (fs_a_dst_interchange_HGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldpositive_body_steps_partial. fs_h_dst_interchange_HGvaluefoldpositive_body_steps_partial + S (fs_r_dst_interchange_HGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_HGvaluefoldpositive)) /\ exists fs_q_dst_interchange_HGvaluefoldpositive_body_steps_partial. fs_u_dst_interchange_HGvaluefoldpositive = fs_q_dst_interchange_HGvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_HGvaluefoldpositive) + (fs_r_dst_interchange_HGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldpositive_body_steps_successor. fs_h_dst_interchange_HGvaluefoldpositive_body_steps_successor + S (fs_s_dst_interchange_HGvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_HGvaluefoldpositive)) /\ exists fs_q_dst_interchange_HGvaluefoldpositive_body_steps_successor. fs_u_dst_interchange_HGvaluefoldpositive = fs_q_dst_interchange_HGvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_interchange_HGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_HGvaluefoldpositive) + (fs_s_dst_interchange_HGvaluefoldpositive_body_steps))) /\ fs_s_dst_interchange_HGvaluefoldpositive_body_steps = fs_r_dst_interchange_HGvaluefoldpositive_body_steps + fs_a_dst_interchange_HGvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_interchange_HGvaluefoldnegative fs_v_dst_interchange_HGvaluefoldnegative. ((((exists fs_h_dst_interchange_HGvaluefoldnegative_body_start. fs_h_dst_interchange_HGvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_HGvaluefoldnegative)) /\ exists fs_q_dst_interchange_HGvaluefoldnegative_body_start. fs_u_dst_interchange_HGvaluefoldnegative = fs_q_dst_interchange_HGvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_interchange_HGvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldnegative_body_terminal. fs_h_dst_interchange_HGvaluefoldnegative_body_terminal + S (dst_negative_sum_interchange_HGvaluefold) = S ((S (S (dc_input_interchange_HG))) * fs_v_dst_interchange_HGvaluefoldnegative)) /\ exists fs_q_dst_interchange_HGvaluefoldnegative_body_terminal. fs_u_dst_interchange_HGvaluefoldnegative = fs_q_dst_interchange_HGvaluefoldnegative_body_terminal * S ((S (S (dc_input_interchange_HG))) * fs_v_dst_interchange_HGvaluefoldnegative) + (dst_negative_sum_interchange_HGvaluefold))) /\ forall fs_i_dst_interchange_HGvaluefoldnegative_body_steps. (exists fs_lt_dst_interchange_HGvaluefoldnegative_body_steps_bound. fs_lt_dst_interchange_HGvaluefoldnegative_body_steps_bound + S fs_i_dst_interchange_HGvaluefoldnegative_body_steps = S (dc_input_interchange_HG)) -> exists fs_a_dst_interchange_HGvaluefoldnegative_body_steps fs_r_dst_interchange_HGvaluefoldnegative_body_steps fs_s_dst_interchange_HGvaluefoldnegative_body_steps. ((((exists fs_h_dst_interchange_HGvaluefoldnegative_body_steps_summand. fs_h_dst_interchange_HGvaluefoldnegative_body_steps_summand + S (fs_a_dst_interchange_HGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * dst_negative_scale_interchange_HGvaluefold)) /\ exists fs_q_dst_interchange_HGvaluefoldnegative_body_steps_summand. dst_negative_code_interchange_HGvaluefold = fs_q_dst_interchange_HGvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * dst_negative_scale_interchange_HGvaluefold) + (fs_a_dst_interchange_HGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldnegative_body_steps_partial. fs_h_dst_interchange_HGvaluefoldnegative_body_steps_partial + S (fs_r_dst_interchange_HGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_HGvaluefoldnegative)) /\ exists fs_q_dst_interchange_HGvaluefoldnegative_body_steps_partial. fs_u_dst_interchange_HGvaluefoldnegative = fs_q_dst_interchange_HGvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_HGvaluefoldnegative) + (fs_r_dst_interchange_HGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_HGvaluefoldnegative_body_steps_successor. fs_h_dst_interchange_HGvaluefoldnegative_body_steps_successor + S (fs_s_dst_interchange_HGvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_HGvaluefoldnegative)) /\ exists fs_q_dst_interchange_HGvaluefoldnegative_body_steps_successor. fs_u_dst_interchange_HGvaluefoldnegative = fs_q_dst_interchange_HGvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_interchange_HGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_HGvaluefoldnegative) + (fs_s_dst_interchange_HGvaluefoldnegative_body_steps))) /\ fs_s_dst_interchange_HGvaluefoldnegative_body_steps = fs_r_dst_interchange_HGvaluefoldnegative_body_steps + fs_a_dst_interchange_HGvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_interchange_HGvaluefoldresult ge_balance_negative_interchange_HGvaluefoldresult. (((((dc_output_interchange_HG) = 2 * (ge_balance_positive_interchange_HGvaluefoldresult) /\ (ge_balance_negative_interchange_HGvaluefoldresult) = 0) \/ exists ge_signed_half_interchange_HGvaluefoldresultdecode. (((dc_output_interchange_HG) = 2 * ge_signed_half_interchange_HGvaluefoldresultdecode + 1 /\ (ge_balance_positive_interchange_HGvaluefoldresult) = 0) /\ (ge_balance_negative_interchange_HGvaluefoldresult) = S ge_signed_half_interchange_HGvaluefoldresultdecode))) /\ ((dst_positive_sum_interchange_HGvaluefold) + ge_balance_negative_interchange_HGvaluefoldresult = (dst_negative_sum_interchange_HGvaluefold) + ge_balance_positive_interchange_HGvaluefoldresult)))))))))))))))))))) -> (((exists dst_positive_code_interchange_FGleft dst_positive_scale_interchange_FGleft dst_negative_code_interchange_FGleft dst_negative_scale_interchange_FGleft. (((F) = (((((dst_positive_code_interchange_FGleft) + (dst_positive_scale_interchange_FGleft)) * S ((dst_positive_code_interchange_FGleft) + (dst_positive_scale_interchange_FGleft)) + ((dst_positive_scale_interchange_FGleft) + (dst_positive_scale_interchange_FGleft))) + (((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) * S ((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) + ((dst_negative_scale_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)))) * S ((((dst_positive_code_interchange_FGleft) + (dst_positive_scale_interchange_FGleft)) * S ((dst_positive_code_interchange_FGleft) + (dst_positive_scale_interchange_FGleft)) + ((dst_positive_scale_interchange_FGleft) + (dst_positive_scale_interchange_FGleft))) + (((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) * S ((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) + ((dst_negative_scale_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)))) + ((((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) * S ((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) + ((dst_negative_scale_interchange_FGleft) + (dst_negative_scale_interchange_FGleft))) + (((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) * S ((dst_negative_code_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)) + ((dst_negative_scale_interchange_FGleft) + (dst_negative_scale_interchange_FGleft)))))) /\ (forall dst_index_interchange_FGleft. (exists pvs_le_gap_interchange_FGleftdomain. pvs_le_gap_interchange_FGleftdomain + (dst_index_interchange_FGleft) = (N)) -> exists dst_positive_interchange_FGleft dst_negative_interchange_FGleft dst_value_interchange_FGleft. ((((exists ff_h_pvs_interchange_FGleftentrypositive. ff_h_pvs_interchange_FGleftentrypositive + S (dst_positive_interchange_FGleft) = S ((S (dst_index_interchange_FGleft)) * dst_positive_scale_interchange_FGleft)) /\ exists ff_q_pvs_interchange_FGleftentrypositive. dst_positive_code_interchange_FGleft = ff_q_pvs_interchange_FGleftentrypositive * S ((S (dst_index_interchange_FGleft)) * dst_positive_scale_interchange_FGleft) + (dst_positive_interchange_FGleft))) /\ (((((exists ff_h_pvs_interchange_FGleftentrynegative. ff_h_pvs_interchange_FGleftentrynegative + S (dst_negative_interchange_FGleft) = S ((S (dst_index_interchange_FGleft)) * dst_negative_scale_interchange_FGleft)) /\ exists ff_q_pvs_interchange_FGleftentrynegative. dst_negative_code_interchange_FGleft = ff_q_pvs_interchange_FGleftentrynegative * S ((S (dst_index_interchange_FGleft)) * dst_negative_scale_interchange_FGleft) + (dst_negative_interchange_FGleft))) /\ (exists ge_balance_positive_interchange_FGleftentryvalue ge_balance_negative_interchange_FGleftentryvalue. (((((dst_value_interchange_FGleft) = 2 * (ge_balance_positive_interchange_FGleftentryvalue) /\ (ge_balance_negative_interchange_FGleftentryvalue) = 0) \/ exists ge_signed_half_interchange_FGleftentryvaluedecode. (((dst_value_interchange_FGleft) = 2 * ge_signed_half_interchange_FGleftentryvaluedecode + 1 /\ (ge_balance_positive_interchange_FGleftentryvalue) = 0) /\ (ge_balance_negative_interchange_FGleftentryvalue) = S ge_signed_half_interchange_FGleftentryvaluedecode))) /\ ((dst_positive_interchange_FGleft) + ge_balance_negative_interchange_FGleftentryvalue = (dst_negative_interchange_FGleft) + ge_balance_positive_interchange_FGleftentryvalue))))))))) /\ (((exists dst_positive_code_interchange_FGright dst_positive_scale_interchange_FGright dst_negative_code_interchange_FGright dst_negative_scale_interchange_FGright. (((G) = (((((dst_positive_code_interchange_FGright) + (dst_positive_scale_interchange_FGright)) * S ((dst_positive_code_interchange_FGright) + (dst_positive_scale_interchange_FGright)) + ((dst_positive_scale_interchange_FGright) + (dst_positive_scale_interchange_FGright))) + (((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) * S ((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) + ((dst_negative_scale_interchange_FGright) + (dst_negative_scale_interchange_FGright)))) * S ((((dst_positive_code_interchange_FGright) + (dst_positive_scale_interchange_FGright)) * S ((dst_positive_code_interchange_FGright) + (dst_positive_scale_interchange_FGright)) + ((dst_positive_scale_interchange_FGright) + (dst_positive_scale_interchange_FGright))) + (((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) * S ((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) + ((dst_negative_scale_interchange_FGright) + (dst_negative_scale_interchange_FGright)))) + ((((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) * S ((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) + ((dst_negative_scale_interchange_FGright) + (dst_negative_scale_interchange_FGright))) + (((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) * S ((dst_negative_code_interchange_FGright) + (dst_negative_scale_interchange_FGright)) + ((dst_negative_scale_interchange_FGright) + (dst_negative_scale_interchange_FGright)))))) /\ (forall dst_index_interchange_FGright. (exists pvs_le_gap_interchange_FGrightdomain. pvs_le_gap_interchange_FGrightdomain + (dst_index_interchange_FGright) = (N)) -> exists dst_positive_interchange_FGright dst_negative_interchange_FGright dst_value_interchange_FGright. ((((exists ff_h_pvs_interchange_FGrightentrypositive. ff_h_pvs_interchange_FGrightentrypositive + S (dst_positive_interchange_FGright) = S ((S (dst_index_interchange_FGright)) * dst_positive_scale_interchange_FGright)) /\ exists ff_q_pvs_interchange_FGrightentrypositive. dst_positive_code_interchange_FGright = ff_q_pvs_interchange_FGrightentrypositive * S ((S (dst_index_interchange_FGright)) * dst_positive_scale_interchange_FGright) + (dst_positive_interchange_FGright))) /\ (((((exists ff_h_pvs_interchange_FGrightentrynegative. ff_h_pvs_interchange_FGrightentrynegative + S (dst_negative_interchange_FGright) = S ((S (dst_index_interchange_FGright)) * dst_negative_scale_interchange_FGright)) /\ exists ff_q_pvs_interchange_FGrightentrynegative. dst_negative_code_interchange_FGright = ff_q_pvs_interchange_FGrightentrynegative * S ((S (dst_index_interchange_FGright)) * dst_negative_scale_interchange_FGright) + (dst_negative_interchange_FGright))) /\ (exists ge_balance_positive_interchange_FGrightentryvalue ge_balance_negative_interchange_FGrightentryvalue. (((((dst_value_interchange_FGright) = 2 * (ge_balance_positive_interchange_FGrightentryvalue) /\ (ge_balance_negative_interchange_FGrightentryvalue) = 0) \/ exists ge_signed_half_interchange_FGrightentryvaluedecode. (((dst_value_interchange_FGright) = 2 * ge_signed_half_interchange_FGrightentryvaluedecode + 1 /\ (ge_balance_positive_interchange_FGrightentryvalue) = 0) /\ (ge_balance_negative_interchange_FGrightentryvalue) = S ge_signed_half_interchange_FGrightentryvaluedecode))) /\ ((dst_positive_interchange_FGright) + ge_balance_negative_interchange_FGrightentryvalue = (dst_negative_interchange_FGright) + ge_balance_positive_interchange_FGrightentryvalue))))))))) /\ (((exists dst_positive_code_interchange_FGtable dst_positive_scale_interchange_FGtable dst_negative_code_interchange_FGtable dst_negative_scale_interchange_FGtable. (((V) = (((((dst_positive_code_interchange_FGtable) + (dst_positive_scale_interchange_FGtable)) * S ((dst_positive_code_interchange_FGtable) + (dst_positive_scale_interchange_FGtable)) + ((dst_positive_scale_interchange_FGtable) + (dst_positive_scale_interchange_FGtable))) + (((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) * S ((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) + ((dst_negative_scale_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)))) * S ((((dst_positive_code_interchange_FGtable) + (dst_positive_scale_interchange_FGtable)) * S ((dst_positive_code_interchange_FGtable) + (dst_positive_scale_interchange_FGtable)) + ((dst_positive_scale_interchange_FGtable) + (dst_positive_scale_interchange_FGtable))) + (((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) * S ((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) + ((dst_negative_scale_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)))) + ((((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) * S ((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) + ((dst_negative_scale_interchange_FGtable) + (dst_negative_scale_interchange_FGtable))) + (((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) * S ((dst_negative_code_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)) + ((dst_negative_scale_interchange_FGtable) + (dst_negative_scale_interchange_FGtable)))))) /\ (forall dst_index_interchange_FGtable. (exists pvs_le_gap_interchange_FGtabledomain. pvs_le_gap_interchange_FGtabledomain + (dst_index_interchange_FGtable) = (N)) -> exists dst_positive_interchange_FGtable dst_negative_interchange_FGtable dst_value_interchange_FGtable. ((((exists ff_h_pvs_interchange_FGtableentrypositive. ff_h_pvs_interchange_FGtableentrypositive + S (dst_positive_interchange_FGtable) = S ((S (dst_index_interchange_FGtable)) * dst_positive_scale_interchange_FGtable)) /\ exists ff_q_pvs_interchange_FGtableentrypositive. dst_positive_code_interchange_FGtable = ff_q_pvs_interchange_FGtableentrypositive * S ((S (dst_index_interchange_FGtable)) * dst_positive_scale_interchange_FGtable) + (dst_positive_interchange_FGtable))) /\ (((((exists ff_h_pvs_interchange_FGtableentrynegative. ff_h_pvs_interchange_FGtableentrynegative + S (dst_negative_interchange_FGtable) = S ((S (dst_index_interchange_FGtable)) * dst_negative_scale_interchange_FGtable)) /\ exists ff_q_pvs_interchange_FGtableentrynegative. dst_negative_code_interchange_FGtable = ff_q_pvs_interchange_FGtableentrynegative * S ((S (dst_index_interchange_FGtable)) * dst_negative_scale_interchange_FGtable) + (dst_negative_interchange_FGtable))) /\ (exists ge_balance_positive_interchange_FGtableentryvalue ge_balance_negative_interchange_FGtableentryvalue. (((((dst_value_interchange_FGtable) = 2 * (ge_balance_positive_interchange_FGtableentryvalue) /\ (ge_balance_negative_interchange_FGtableentryvalue) = 0) \/ exists ge_signed_half_interchange_FGtableentryvaluedecode. (((dst_value_interchange_FGtable) = 2 * ge_signed_half_interchange_FGtableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_FGtableentryvalue) = 0) /\ (ge_balance_negative_interchange_FGtableentryvalue) = S ge_signed_half_interchange_FGtableentryvaluedecode))) /\ ((dst_positive_interchange_FGtable) + ge_balance_negative_interchange_FGtableentryvalue = (dst_negative_interchange_FGtable) + ge_balance_positive_interchange_FGtableentryvalue))))))))) /\ (forall dc_input_interchange_FG dc_output_interchange_FG. ~(dc_input_interchange_FG=0) -> (exists pvs_le_gap_interchange_FGdomain. pvs_le_gap_interchange_FGdomain + (dc_input_interchange_FG) = (N)) -> (exists dst_positive_code_interchange_FGlookup dst_positive_scale_interchange_FGlookup dst_negative_code_interchange_FGlookup dst_negative_scale_interchange_FGlookup dst_positive_interchange_FGlookup dst_negative_interchange_FGlookup. (((V) = (((((dst_positive_code_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup)) * S ((dst_positive_code_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup)) + ((dst_positive_scale_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup))) + (((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) * S ((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) + ((dst_negative_scale_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)))) * S ((((dst_positive_code_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup)) * S ((dst_positive_code_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup)) + ((dst_positive_scale_interchange_FGlookup) + (dst_positive_scale_interchange_FGlookup))) + (((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) * S ((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) + ((dst_negative_scale_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)))) + ((((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) * S ((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) + ((dst_negative_scale_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup))) + (((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) * S ((dst_negative_code_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)) + ((dst_negative_scale_interchange_FGlookup) + (dst_negative_scale_interchange_FGlookup)))))) /\ (((((exists ff_h_pvs_interchange_FGlookuppositive. ff_h_pvs_interchange_FGlookuppositive + S (dst_positive_interchange_FGlookup) = S ((S (dc_input_interchange_FG)) * dst_positive_scale_interchange_FGlookup)) /\ exists ff_q_pvs_interchange_FGlookuppositive. dst_positive_code_interchange_FGlookup = ff_q_pvs_interchange_FGlookuppositive * S ((S (dc_input_interchange_FG)) * dst_positive_scale_interchange_FGlookup) + (dst_positive_interchange_FGlookup))) /\ (((((exists ff_h_pvs_interchange_FGlookupnegative. ff_h_pvs_interchange_FGlookupnegative + S (dst_negative_interchange_FGlookup) = S ((S (dc_input_interchange_FG)) * dst_negative_scale_interchange_FGlookup)) /\ exists ff_q_pvs_interchange_FGlookupnegative. dst_negative_code_interchange_FGlookup = ff_q_pvs_interchange_FGlookupnegative * S ((S (dc_input_interchange_FG)) * dst_negative_scale_interchange_FGlookup) + (dst_negative_interchange_FGlookup))) /\ (exists ge_balance_positive_interchange_FGlookupvalue ge_balance_negative_interchange_FGlookupvalue. (((((dc_output_interchange_FG) = 2 * (ge_balance_positive_interchange_FGlookupvalue) /\ (ge_balance_negative_interchange_FGlookupvalue) = 0) \/ exists ge_signed_half_interchange_FGlookupvaluedecode. (((dc_output_interchange_FG) = 2 * ge_signed_half_interchange_FGlookupvaluedecode + 1 /\ (ge_balance_positive_interchange_FGlookupvalue) = 0) /\ (ge_balance_negative_interchange_FGlookupvalue) = S ge_signed_half_interchange_FGlookupvaluedecode))) /\ ((dst_positive_interchange_FGlookup) + ge_balance_negative_interchange_FGlookupvalue = (dst_negative_interchange_FGlookup) + ge_balance_positive_interchange_FGlookupvalue))))))))) -> (((~((dc_input_interchange_FG)=0)) /\ (exists dc_mask_interchange_FGvalue. ((((exists dst_positive_code_interchange_FGvaluemasktable dst_positive_scale_interchange_FGvaluemasktable dst_negative_code_interchange_FGvaluemasktable dst_negative_scale_interchange_FGvaluemasktable. (((dc_mask_interchange_FGvalue) = (((((dst_positive_code_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable)) * S ((dst_positive_code_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable)) + ((dst_positive_scale_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable))) + (((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) * S ((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) + ((dst_negative_scale_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)))) * S ((((dst_positive_code_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable)) * S ((dst_positive_code_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable)) + ((dst_positive_scale_interchange_FGvaluemasktable) + (dst_positive_scale_interchange_FGvaluemasktable))) + (((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) * S ((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) + ((dst_negative_scale_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)))) + ((((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) * S ((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) + ((dst_negative_scale_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable))) + (((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) * S ((dst_negative_code_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)) + ((dst_negative_scale_interchange_FGvaluemasktable) + (dst_negative_scale_interchange_FGvaluemasktable)))))) /\ (forall dst_index_interchange_FGvaluemasktable. (exists pvs_le_gap_interchange_FGvaluemasktabledomain. pvs_le_gap_interchange_FGvaluemasktabledomain + (dst_index_interchange_FGvaluemasktable) = (dc_input_interchange_FG)) -> exists dst_positive_interchange_FGvaluemasktable dst_negative_interchange_FGvaluemasktable dst_value_interchange_FGvaluemasktable. ((((exists ff_h_pvs_interchange_FGvaluemasktableentrypositive. ff_h_pvs_interchange_FGvaluemasktableentrypositive + S (dst_positive_interchange_FGvaluemasktable) = S ((S (dst_index_interchange_FGvaluemasktable)) * dst_positive_scale_interchange_FGvaluemasktable)) /\ exists ff_q_pvs_interchange_FGvaluemasktableentrypositive. dst_positive_code_interchange_FGvaluemasktable = ff_q_pvs_interchange_FGvaluemasktableentrypositive * S ((S (dst_index_interchange_FGvaluemasktable)) * dst_positive_scale_interchange_FGvaluemasktable) + (dst_positive_interchange_FGvaluemasktable))) /\ (((((exists ff_h_pvs_interchange_FGvaluemasktableentrynegative. ff_h_pvs_interchange_FGvaluemasktableentrynegative + S (dst_negative_interchange_FGvaluemasktable) = S ((S (dst_index_interchange_FGvaluemasktable)) * dst_negative_scale_interchange_FGvaluemasktable)) /\ exists ff_q_pvs_interchange_FGvaluemasktableentrynegative. dst_negative_code_interchange_FGvaluemasktable = ff_q_pvs_interchange_FGvaluemasktableentrynegative * S ((S (dst_index_interchange_FGvaluemasktable)) * dst_negative_scale_interchange_FGvaluemasktable) + (dst_negative_interchange_FGvaluemasktable))) /\ (exists ge_balance_positive_interchange_FGvaluemasktableentryvalue ge_balance_negative_interchange_FGvaluemasktableentryvalue. (((((dst_value_interchange_FGvaluemasktable) = 2 * (ge_balance_positive_interchange_FGvaluemasktableentryvalue) /\ (ge_balance_negative_interchange_FGvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_interchange_FGvaluemasktableentryvaluedecode. (((dst_value_interchange_FGvaluemasktable) = 2 * ge_signed_half_interchange_FGvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_FGvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_interchange_FGvaluemasktableentryvalue) = S ge_signed_half_interchange_FGvaluemasktableentryvaluedecode))) /\ ((dst_positive_interchange_FGvaluemasktable) + ge_balance_negative_interchange_FGvaluemasktableentryvalue = (dst_negative_interchange_FGvaluemasktable) + ge_balance_positive_interchange_FGvaluemasktableentryvalue))))))))) /\ (forall dc_index_interchange_FGvaluemask dc_value_interchange_FGvaluemask. (exists pvs_le_gap_interchange_FGvaluemaskdomain. pvs_le_gap_interchange_FGvaluemaskdomain + (dc_index_interchange_FGvaluemask) = (dc_input_interchange_FG)) -> (exists dst_positive_code_interchange_FGvaluemasklookup dst_positive_scale_interchange_FGvaluemasklookup dst_negative_code_interchange_FGvaluemasklookup dst_negative_scale_interchange_FGvaluemasklookup dst_positive_interchange_FGvaluemasklookup dst_negative_interchange_FGvaluemasklookup. (((dc_mask_interchange_FGvalue) = (((((dst_positive_code_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup)) * S ((dst_positive_code_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup)) + ((dst_positive_scale_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup))) + (((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) * S ((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) + ((dst_negative_scale_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)))) * S ((((dst_positive_code_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup)) * S ((dst_positive_code_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup)) + ((dst_positive_scale_interchange_FGvaluemasklookup) + (dst_positive_scale_interchange_FGvaluemasklookup))) + (((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) * S ((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) + ((dst_negative_scale_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)))) + ((((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) * S ((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) + ((dst_negative_scale_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup))) + (((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) * S ((dst_negative_code_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)) + ((dst_negative_scale_interchange_FGvaluemasklookup) + (dst_negative_scale_interchange_FGvaluemasklookup)))))) /\ (((((exists ff_h_pvs_interchange_FGvaluemasklookuppositive. ff_h_pvs_interchange_FGvaluemasklookuppositive + S (dst_positive_interchange_FGvaluemasklookup) = S ((S (dc_index_interchange_FGvaluemask)) * dst_positive_scale_interchange_FGvaluemasklookup)) /\ exists ff_q_pvs_interchange_FGvaluemasklookuppositive. dst_positive_code_interchange_FGvaluemasklookup = ff_q_pvs_interchange_FGvaluemasklookuppositive * S ((S (dc_index_interchange_FGvaluemask)) * dst_positive_scale_interchange_FGvaluemasklookup) + (dst_positive_interchange_FGvaluemasklookup))) /\ (((((exists ff_h_pvs_interchange_FGvaluemasklookupnegative. ff_h_pvs_interchange_FGvaluemasklookupnegative + S (dst_negative_interchange_FGvaluemasklookup) = S ((S (dc_index_interchange_FGvaluemask)) * dst_negative_scale_interchange_FGvaluemasklookup)) /\ exists ff_q_pvs_interchange_FGvaluemasklookupnegative. dst_negative_code_interchange_FGvaluemasklookup = ff_q_pvs_interchange_FGvaluemasklookupnegative * S ((S (dc_index_interchange_FGvaluemask)) * dst_negative_scale_interchange_FGvaluemasklookup) + (dst_negative_interchange_FGvaluemasklookup))) /\ (exists ge_balance_positive_interchange_FGvaluemasklookupvalue ge_balance_negative_interchange_FGvaluemasklookupvalue. (((((dc_value_interchange_FGvaluemask) = 2 * (ge_balance_positive_interchange_FGvaluemasklookupvalue) /\ (ge_balance_negative_interchange_FGvaluemasklookupvalue) = 0) \/ exists ge_signed_half_interchange_FGvaluemasklookupvaluedecode. (((dc_value_interchange_FGvaluemask) = 2 * ge_signed_half_interchange_FGvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_interchange_FGvaluemasklookupvalue) = 0) /\ (ge_balance_negative_interchange_FGvaluemasklookupvalue) = S ge_signed_half_interchange_FGvaluemasklookupvaluedecode))) /\ ((dst_positive_interchange_FGvaluemasklookup) + ge_balance_negative_interchange_FGvaluemasklookupvalue = (dst_negative_interchange_FGvaluemasklookup) + ge_balance_positive_interchange_FGvaluemasklookupvalue))))))))) -> ((((~((dc_index_interchange_FGvaluemask)=0)) /\ (exists dc_quotient_interchange_FGvaluemaskentry dc_left_interchange_FGvaluemaskentry dc_right_interchange_FGvaluemaskentry. (((dc_input_interchange_FG)=(dc_index_interchange_FGvaluemask)*dc_quotient_interchange_FGvaluemaskentry) /\ (((exists dst_positive_code_interchange_FGvaluemaskentryleft dst_positive_scale_interchange_FGvaluemaskentryleft dst_negative_code_interchange_FGvaluemaskentryleft dst_negative_scale_interchange_FGvaluemaskentryleft dst_positive_interchange_FGvaluemaskentryleft dst_negative_interchange_FGvaluemaskentryleft. (((F) = (((((dst_positive_code_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft)) * S ((dst_positive_code_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft)) + ((dst_positive_scale_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft))) + (((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) * S ((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) + ((dst_negative_scale_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)))) * S ((((dst_positive_code_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft)) * S ((dst_positive_code_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft)) + ((dst_positive_scale_interchange_FGvaluemaskentryleft) + (dst_positive_scale_interchange_FGvaluemaskentryleft))) + (((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) * S ((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) + ((dst_negative_scale_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)))) + ((((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) * S ((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) + ((dst_negative_scale_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft))) + (((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) * S ((dst_negative_code_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)) + ((dst_negative_scale_interchange_FGvaluemaskentryleft) + (dst_negative_scale_interchange_FGvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_interchange_FGvaluemaskentryleftpositive. ff_h_pvs_interchange_FGvaluemaskentryleftpositive + S (dst_positive_interchange_FGvaluemaskentryleft) = S ((S (dc_index_interchange_FGvaluemask)) * dst_positive_scale_interchange_FGvaluemaskentryleft)) /\ exists ff_q_pvs_interchange_FGvaluemaskentryleftpositive. dst_positive_code_interchange_FGvaluemaskentryleft = ff_q_pvs_interchange_FGvaluemaskentryleftpositive * S ((S (dc_index_interchange_FGvaluemask)) * dst_positive_scale_interchange_FGvaluemaskentryleft) + (dst_positive_interchange_FGvaluemaskentryleft))) /\ (((((exists ff_h_pvs_interchange_FGvaluemaskentryleftnegative. ff_h_pvs_interchange_FGvaluemaskentryleftnegative + S (dst_negative_interchange_FGvaluemaskentryleft) = S ((S (dc_index_interchange_FGvaluemask)) * dst_negative_scale_interchange_FGvaluemaskentryleft)) /\ exists ff_q_pvs_interchange_FGvaluemaskentryleftnegative. dst_negative_code_interchange_FGvaluemaskentryleft = ff_q_pvs_interchange_FGvaluemaskentryleftnegative * S ((S (dc_index_interchange_FGvaluemask)) * dst_negative_scale_interchange_FGvaluemaskentryleft) + (dst_negative_interchange_FGvaluemaskentryleft))) /\ (exists ge_balance_positive_interchange_FGvaluemaskentryleftvalue ge_balance_negative_interchange_FGvaluemaskentryleftvalue. (((((dc_left_interchange_FGvaluemaskentry) = 2 * (ge_balance_positive_interchange_FGvaluemaskentryleftvalue) /\ (ge_balance_negative_interchange_FGvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_interchange_FGvaluemaskentryleftvaluedecode. (((dc_left_interchange_FGvaluemaskentry) = 2 * ge_signed_half_interchange_FGvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_interchange_FGvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_interchange_FGvaluemaskentryleftvalue) = S ge_signed_half_interchange_FGvaluemaskentryleftvaluedecode))) /\ ((dst_positive_interchange_FGvaluemaskentryleft) + ge_balance_negative_interchange_FGvaluemaskentryleftvalue = (dst_negative_interchange_FGvaluemaskentryleft) + ge_balance_positive_interchange_FGvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_interchange_FGvaluemaskentryright dst_positive_scale_interchange_FGvaluemaskentryright dst_negative_code_interchange_FGvaluemaskentryright dst_negative_scale_interchange_FGvaluemaskentryright dst_positive_interchange_FGvaluemaskentryright dst_negative_interchange_FGvaluemaskentryright. (((G) = (((((dst_positive_code_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright)) * S ((dst_positive_code_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright)) + ((dst_positive_scale_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright))) + (((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) * S ((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) + ((dst_negative_scale_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)))) * S ((((dst_positive_code_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright)) * S ((dst_positive_code_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright)) + ((dst_positive_scale_interchange_FGvaluemaskentryright) + (dst_positive_scale_interchange_FGvaluemaskentryright))) + (((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) * S ((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) + ((dst_negative_scale_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)))) + ((((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) * S ((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) + ((dst_negative_scale_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright))) + (((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) * S ((dst_negative_code_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)) + ((dst_negative_scale_interchange_FGvaluemaskentryright) + (dst_negative_scale_interchange_FGvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_interchange_FGvaluemaskentryrightpositive. ff_h_pvs_interchange_FGvaluemaskentryrightpositive + S (dst_positive_interchange_FGvaluemaskentryright) = S ((S (dc_quotient_interchange_FGvaluemaskentry)) * dst_positive_scale_interchange_FGvaluemaskentryright)) /\ exists ff_q_pvs_interchange_FGvaluemaskentryrightpositive. dst_positive_code_interchange_FGvaluemaskentryright = ff_q_pvs_interchange_FGvaluemaskentryrightpositive * S ((S (dc_quotient_interchange_FGvaluemaskentry)) * dst_positive_scale_interchange_FGvaluemaskentryright) + (dst_positive_interchange_FGvaluemaskentryright))) /\ (((((exists ff_h_pvs_interchange_FGvaluemaskentryrightnegative. ff_h_pvs_interchange_FGvaluemaskentryrightnegative + S (dst_negative_interchange_FGvaluemaskentryright) = S ((S (dc_quotient_interchange_FGvaluemaskentry)) * dst_negative_scale_interchange_FGvaluemaskentryright)) /\ exists ff_q_pvs_interchange_FGvaluemaskentryrightnegative. dst_negative_code_interchange_FGvaluemaskentryright = ff_q_pvs_interchange_FGvaluemaskentryrightnegative * S ((S (dc_quotient_interchange_FGvaluemaskentry)) * dst_negative_scale_interchange_FGvaluemaskentryright) + (dst_negative_interchange_FGvaluemaskentryright))) /\ (exists ge_balance_positive_interchange_FGvaluemaskentryrightvalue ge_balance_negative_interchange_FGvaluemaskentryrightvalue. (((((dc_right_interchange_FGvaluemaskentry) = 2 * (ge_balance_positive_interchange_FGvaluemaskentryrightvalue) /\ (ge_balance_negative_interchange_FGvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_interchange_FGvaluemaskentryrightvaluedecode. (((dc_right_interchange_FGvaluemaskentry) = 2 * ge_signed_half_interchange_FGvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_interchange_FGvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_interchange_FGvaluemaskentryrightvalue) = S ge_signed_half_interchange_FGvaluemaskentryrightvaluedecode))) /\ ((dst_positive_interchange_FGvaluemaskentryright) + ge_balance_negative_interchange_FGvaluemaskentryrightvalue = (dst_negative_interchange_FGvaluemaskentryright) + ge_balance_positive_interchange_FGvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_interchange_FGvaluemaskentryproduct sto_an_interchange_FGvaluemaskentryproduct sto_bp_interchange_FGvaluemaskentryproduct sto_bn_interchange_FGvaluemaskentryproduct sto_cp_interchange_FGvaluemaskentryproduct sto_cn_interchange_FGvaluemaskentryproduct. (((((dc_left_interchange_FGvaluemaskentry) = 2 * (sto_ap_interchange_FGvaluemaskentryproduct) /\ (sto_an_interchange_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_FGvaluemaskentryproductleft. (((dc_left_interchange_FGvaluemaskentry) = 2 * ge_signed_half_interchange_FGvaluemaskentryproductleft + 1 /\ (sto_ap_interchange_FGvaluemaskentryproduct) = 0) /\ (sto_an_interchange_FGvaluemaskentryproduct) = S ge_signed_half_interchange_FGvaluemaskentryproductleft))) /\ ((((((dc_right_interchange_FGvaluemaskentry) = 2 * (sto_bp_interchange_FGvaluemaskentryproduct) /\ (sto_bn_interchange_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_FGvaluemaskentryproductright. (((dc_right_interchange_FGvaluemaskentry) = 2 * ge_signed_half_interchange_FGvaluemaskentryproductright + 1 /\ (sto_bp_interchange_FGvaluemaskentryproduct) = 0) /\ (sto_bn_interchange_FGvaluemaskentryproduct) = S ge_signed_half_interchange_FGvaluemaskentryproductright))) /\ ((((((dc_value_interchange_FGvaluemask) = 2 * (sto_cp_interchange_FGvaluemaskentryproduct) /\ (sto_cn_interchange_FGvaluemaskentryproduct) = 0) \/ exists ge_signed_half_interchange_FGvaluemaskentryproductoutput. (((dc_value_interchange_FGvaluemask) = 2 * ge_signed_half_interchange_FGvaluemaskentryproductoutput + 1 /\ (sto_cp_interchange_FGvaluemaskentryproduct) = 0) /\ (sto_cn_interchange_FGvaluemaskentryproduct) = S ge_signed_half_interchange_FGvaluemaskentryproductoutput))) /\ ((sto_ap_interchange_FGvaluemaskentryproduct * sto_bp_interchange_FGvaluemaskentryproduct + sto_an_interchange_FGvaluemaskentryproduct * sto_bn_interchange_FGvaluemaskentryproduct) + sto_cn_interchange_FGvaluemaskentryproduct = (sto_ap_interchange_FGvaluemaskentryproduct * sto_bn_interchange_FGvaluemaskentryproduct + sto_an_interchange_FGvaluemaskentryproduct * sto_bp_interchange_FGvaluemaskentryproduct) + sto_cp_interchange_FGvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_interchange_FGvaluemask)=0 \/ ~(exists pvs_factor_interchange_FGvaluemaskentrynondivisor. (dc_input_interchange_FG) = (dc_index_interchange_FGvaluemask) * pvs_factor_interchange_FGvaluemaskentrynondivisor)) /\ ((dc_value_interchange_FGvaluemask)=0))))))) /\ (exists dst_positive_code_interchange_FGvaluefold dst_positive_scale_interchange_FGvaluefold dst_negative_code_interchange_FGvaluefold dst_negative_scale_interchange_FGvaluefold dst_positive_sum_interchange_FGvaluefold dst_negative_sum_interchange_FGvaluefold. (((dc_mask_interchange_FGvalue) = (((((dst_positive_code_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold)) * S ((dst_positive_code_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold)) + ((dst_positive_scale_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold))) + (((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) * S ((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) + ((dst_negative_scale_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)))) * S ((((dst_positive_code_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold)) * S ((dst_positive_code_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold)) + ((dst_positive_scale_interchange_FGvaluefold) + (dst_positive_scale_interchange_FGvaluefold))) + (((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) * S ((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) + ((dst_negative_scale_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)))) + ((((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) * S ((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) + ((dst_negative_scale_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold))) + (((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) * S ((dst_negative_code_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)) + ((dst_negative_scale_interchange_FGvaluefold) + (dst_negative_scale_interchange_FGvaluefold)))))) /\ (((exists fs_u_dst_interchange_FGvaluefoldpositive fs_v_dst_interchange_FGvaluefoldpositive. ((((exists fs_h_dst_interchange_FGvaluefoldpositive_body_start. fs_h_dst_interchange_FGvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_FGvaluefoldpositive)) /\ exists fs_q_dst_interchange_FGvaluefoldpositive_body_start. fs_u_dst_interchange_FGvaluefoldpositive = fs_q_dst_interchange_FGvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_interchange_FGvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldpositive_body_terminal. fs_h_dst_interchange_FGvaluefoldpositive_body_terminal + S (dst_positive_sum_interchange_FGvaluefold) = S ((S (S (dc_input_interchange_FG))) * fs_v_dst_interchange_FGvaluefoldpositive)) /\ exists fs_q_dst_interchange_FGvaluefoldpositive_body_terminal. fs_u_dst_interchange_FGvaluefoldpositive = fs_q_dst_interchange_FGvaluefoldpositive_body_terminal * S ((S (S (dc_input_interchange_FG))) * fs_v_dst_interchange_FGvaluefoldpositive) + (dst_positive_sum_interchange_FGvaluefold))) /\ forall fs_i_dst_interchange_FGvaluefoldpositive_body_steps. (exists fs_lt_dst_interchange_FGvaluefoldpositive_body_steps_bound. fs_lt_dst_interchange_FGvaluefoldpositive_body_steps_bound + S fs_i_dst_interchange_FGvaluefoldpositive_body_steps = S (dc_input_interchange_FG)) -> exists fs_a_dst_interchange_FGvaluefoldpositive_body_steps fs_r_dst_interchange_FGvaluefoldpositive_body_steps fs_s_dst_interchange_FGvaluefoldpositive_body_steps. ((((exists fs_h_dst_interchange_FGvaluefoldpositive_body_steps_summand. fs_h_dst_interchange_FGvaluefoldpositive_body_steps_summand + S (fs_a_dst_interchange_FGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * dst_positive_scale_interchange_FGvaluefold)) /\ exists fs_q_dst_interchange_FGvaluefoldpositive_body_steps_summand. dst_positive_code_interchange_FGvaluefold = fs_q_dst_interchange_FGvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * dst_positive_scale_interchange_FGvaluefold) + (fs_a_dst_interchange_FGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldpositive_body_steps_partial. fs_h_dst_interchange_FGvaluefoldpositive_body_steps_partial + S (fs_r_dst_interchange_FGvaluefoldpositive_body_steps) = S ((S (fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_FGvaluefoldpositive)) /\ exists fs_q_dst_interchange_FGvaluefoldpositive_body_steps_partial. fs_u_dst_interchange_FGvaluefoldpositive = fs_q_dst_interchange_FGvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_FGvaluefoldpositive) + (fs_r_dst_interchange_FGvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldpositive_body_steps_successor. fs_h_dst_interchange_FGvaluefoldpositive_body_steps_successor + S (fs_s_dst_interchange_FGvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_FGvaluefoldpositive)) /\ exists fs_q_dst_interchange_FGvaluefoldpositive_body_steps_successor. fs_u_dst_interchange_FGvaluefoldpositive = fs_q_dst_interchange_FGvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_interchange_FGvaluefoldpositive_body_steps)) * fs_v_dst_interchange_FGvaluefoldpositive) + (fs_s_dst_interchange_FGvaluefoldpositive_body_steps))) /\ fs_s_dst_interchange_FGvaluefoldpositive_body_steps = fs_r_dst_interchange_FGvaluefoldpositive_body_steps + fs_a_dst_interchange_FGvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_interchange_FGvaluefoldnegative fs_v_dst_interchange_FGvaluefoldnegative. ((((exists fs_h_dst_interchange_FGvaluefoldnegative_body_start. fs_h_dst_interchange_FGvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_FGvaluefoldnegative)) /\ exists fs_q_dst_interchange_FGvaluefoldnegative_body_start. fs_u_dst_interchange_FGvaluefoldnegative = fs_q_dst_interchange_FGvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_interchange_FGvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldnegative_body_terminal. fs_h_dst_interchange_FGvaluefoldnegative_body_terminal + S (dst_negative_sum_interchange_FGvaluefold) = S ((S (S (dc_input_interchange_FG))) * fs_v_dst_interchange_FGvaluefoldnegative)) /\ exists fs_q_dst_interchange_FGvaluefoldnegative_body_terminal. fs_u_dst_interchange_FGvaluefoldnegative = fs_q_dst_interchange_FGvaluefoldnegative_body_terminal * S ((S (S (dc_input_interchange_FG))) * fs_v_dst_interchange_FGvaluefoldnegative) + (dst_negative_sum_interchange_FGvaluefold))) /\ forall fs_i_dst_interchange_FGvaluefoldnegative_body_steps. (exists fs_lt_dst_interchange_FGvaluefoldnegative_body_steps_bound. fs_lt_dst_interchange_FGvaluefoldnegative_body_steps_bound + S fs_i_dst_interchange_FGvaluefoldnegative_body_steps = S (dc_input_interchange_FG)) -> exists fs_a_dst_interchange_FGvaluefoldnegative_body_steps fs_r_dst_interchange_FGvaluefoldnegative_body_steps fs_s_dst_interchange_FGvaluefoldnegative_body_steps. ((((exists fs_h_dst_interchange_FGvaluefoldnegative_body_steps_summand. fs_h_dst_interchange_FGvaluefoldnegative_body_steps_summand + S (fs_a_dst_interchange_FGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * dst_negative_scale_interchange_FGvaluefold)) /\ exists fs_q_dst_interchange_FGvaluefoldnegative_body_steps_summand. dst_negative_code_interchange_FGvaluefold = fs_q_dst_interchange_FGvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * dst_negative_scale_interchange_FGvaluefold) + (fs_a_dst_interchange_FGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldnegative_body_steps_partial. fs_h_dst_interchange_FGvaluefoldnegative_body_steps_partial + S (fs_r_dst_interchange_FGvaluefoldnegative_body_steps) = S ((S (fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_FGvaluefoldnegative)) /\ exists fs_q_dst_interchange_FGvaluefoldnegative_body_steps_partial. fs_u_dst_interchange_FGvaluefoldnegative = fs_q_dst_interchange_FGvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_FGvaluefoldnegative) + (fs_r_dst_interchange_FGvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_FGvaluefoldnegative_body_steps_successor. fs_h_dst_interchange_FGvaluefoldnegative_body_steps_successor + S (fs_s_dst_interchange_FGvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_FGvaluefoldnegative)) /\ exists fs_q_dst_interchange_FGvaluefoldnegative_body_steps_successor. fs_u_dst_interchange_FGvaluefoldnegative = fs_q_dst_interchange_FGvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_interchange_FGvaluefoldnegative_body_steps)) * fs_v_dst_interchange_FGvaluefoldnegative) + (fs_s_dst_interchange_FGvaluefoldnegative_body_steps))) /\ fs_s_dst_interchange_FGvaluefoldnegative_body_steps = fs_r_dst_interchange_FGvaluefoldnegative_body_steps + fs_a_dst_interchange_FGvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_interchange_FGvaluefoldresult ge_balance_negative_interchange_FGvaluefoldresult. (((((dc_output_interchange_FG) = 2 * (ge_balance_positive_interchange_FGvaluefoldresult) /\ (ge_balance_negative_interchange_FGvaluefoldresult) = 0) \/ exists ge_signed_half_interchange_FGvaluefoldresultdecode. (((dc_output_interchange_FG) = 2 * ge_signed_half_interchange_FGvaluefoldresultdecode + 1 /\ (ge_balance_positive_interchange_FGvaluefoldresult) = 0) /\ (ge_balance_negative_interchange_FGvaluefoldresult) = S ge_signed_half_interchange_FGvaluefoldresultdecode))) /\ ((dst_positive_sum_interchange_FGvaluefold) + ge_balance_negative_interchange_FGvaluefoldresult = (dst_negative_sum_interchange_FGvaluefold) + ge_balance_positive_interchange_FGvaluefoldresult)))))))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_interchange_domain. pvs_le_gap_interchange_domain + (n) = (N)) -> (((~((n)=0)) /\ (exists dc_mask_interchange_first. ((((exists dst_positive_code_interchange_firstmasktable dst_positive_scale_interchange_firstmasktable dst_negative_code_interchange_firstmasktable dst_negative_scale_interchange_firstmasktable. (((dc_mask_interchange_first) = (((((dst_positive_code_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable)) * S ((dst_positive_code_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable)) + ((dst_positive_scale_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable))) + (((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) * S ((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) + ((dst_negative_scale_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)))) * S ((((dst_positive_code_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable)) * S ((dst_positive_code_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable)) + ((dst_positive_scale_interchange_firstmasktable) + (dst_positive_scale_interchange_firstmasktable))) + (((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) * S ((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) + ((dst_negative_scale_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)))) + ((((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) * S ((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) + ((dst_negative_scale_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable))) + (((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) * S ((dst_negative_code_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)) + ((dst_negative_scale_interchange_firstmasktable) + (dst_negative_scale_interchange_firstmasktable)))))) /\ (forall dst_index_interchange_firstmasktable. (exists pvs_le_gap_interchange_firstmasktabledomain. pvs_le_gap_interchange_firstmasktabledomain + (dst_index_interchange_firstmasktable) = (n)) -> exists dst_positive_interchange_firstmasktable dst_negative_interchange_firstmasktable dst_value_interchange_firstmasktable. ((((exists ff_h_pvs_interchange_firstmasktableentrypositive. ff_h_pvs_interchange_firstmasktableentrypositive + S (dst_positive_interchange_firstmasktable) = S ((S (dst_index_interchange_firstmasktable)) * dst_positive_scale_interchange_firstmasktable)) /\ exists ff_q_pvs_interchange_firstmasktableentrypositive. dst_positive_code_interchange_firstmasktable = ff_q_pvs_interchange_firstmasktableentrypositive * S ((S (dst_index_interchange_firstmasktable)) * dst_positive_scale_interchange_firstmasktable) + (dst_positive_interchange_firstmasktable))) /\ (((((exists ff_h_pvs_interchange_firstmasktableentrynegative. ff_h_pvs_interchange_firstmasktableentrynegative + S (dst_negative_interchange_firstmasktable) = S ((S (dst_index_interchange_firstmasktable)) * dst_negative_scale_interchange_firstmasktable)) /\ exists ff_q_pvs_interchange_firstmasktableentrynegative. dst_negative_code_interchange_firstmasktable = ff_q_pvs_interchange_firstmasktableentrynegative * S ((S (dst_index_interchange_firstmasktable)) * dst_negative_scale_interchange_firstmasktable) + (dst_negative_interchange_firstmasktable))) /\ (exists ge_balance_positive_interchange_firstmasktableentryvalue ge_balance_negative_interchange_firstmasktableentryvalue. (((((dst_value_interchange_firstmasktable) = 2 * (ge_balance_positive_interchange_firstmasktableentryvalue) /\ (ge_balance_negative_interchange_firstmasktableentryvalue) = 0) \/ exists ge_signed_half_interchange_firstmasktableentryvaluedecode. (((dst_value_interchange_firstmasktable) = 2 * ge_signed_half_interchange_firstmasktableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_firstmasktableentryvalue) = 0) /\ (ge_balance_negative_interchange_firstmasktableentryvalue) = S ge_signed_half_interchange_firstmasktableentryvaluedecode))) /\ ((dst_positive_interchange_firstmasktable) + ge_balance_negative_interchange_firstmasktableentryvalue = (dst_negative_interchange_firstmasktable) + ge_balance_positive_interchange_firstmasktableentryvalue))))))))) /\ (forall dc_index_interchange_firstmask dc_value_interchange_firstmask. (exists pvs_le_gap_interchange_firstmaskdomain. pvs_le_gap_interchange_firstmaskdomain + (dc_index_interchange_firstmask) = (n)) -> (exists dst_positive_code_interchange_firstmasklookup dst_positive_scale_interchange_firstmasklookup dst_negative_code_interchange_firstmasklookup dst_negative_scale_interchange_firstmasklookup dst_positive_interchange_firstmasklookup dst_negative_interchange_firstmasklookup. (((dc_mask_interchange_first) = (((((dst_positive_code_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup)) * S ((dst_positive_code_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup)) + ((dst_positive_scale_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup))) + (((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) * S ((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) + ((dst_negative_scale_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)))) * S ((((dst_positive_code_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup)) * S ((dst_positive_code_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup)) + ((dst_positive_scale_interchange_firstmasklookup) + (dst_positive_scale_interchange_firstmasklookup))) + (((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) * S ((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) + ((dst_negative_scale_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)))) + ((((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) * S ((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) + ((dst_negative_scale_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup))) + (((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) * S ((dst_negative_code_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)) + ((dst_negative_scale_interchange_firstmasklookup) + (dst_negative_scale_interchange_firstmasklookup)))))) /\ (((((exists ff_h_pvs_interchange_firstmasklookuppositive. ff_h_pvs_interchange_firstmasklookuppositive + S (dst_positive_interchange_firstmasklookup) = S ((S (dc_index_interchange_firstmask)) * dst_positive_scale_interchange_firstmasklookup)) /\ exists ff_q_pvs_interchange_firstmasklookuppositive. dst_positive_code_interchange_firstmasklookup = ff_q_pvs_interchange_firstmasklookuppositive * S ((S (dc_index_interchange_firstmask)) * dst_positive_scale_interchange_firstmasklookup) + (dst_positive_interchange_firstmasklookup))) /\ (((((exists ff_h_pvs_interchange_firstmasklookupnegative. ff_h_pvs_interchange_firstmasklookupnegative + S (dst_negative_interchange_firstmasklookup) = S ((S (dc_index_interchange_firstmask)) * dst_negative_scale_interchange_firstmasklookup)) /\ exists ff_q_pvs_interchange_firstmasklookupnegative. dst_negative_code_interchange_firstmasklookup = ff_q_pvs_interchange_firstmasklookupnegative * S ((S (dc_index_interchange_firstmask)) * dst_negative_scale_interchange_firstmasklookup) + (dst_negative_interchange_firstmasklookup))) /\ (exists ge_balance_positive_interchange_firstmasklookupvalue ge_balance_negative_interchange_firstmasklookupvalue. (((((dc_value_interchange_firstmask) = 2 * (ge_balance_positive_interchange_firstmasklookupvalue) /\ (ge_balance_negative_interchange_firstmasklookupvalue) = 0) \/ exists ge_signed_half_interchange_firstmasklookupvaluedecode. (((dc_value_interchange_firstmask) = 2 * ge_signed_half_interchange_firstmasklookupvaluedecode + 1 /\ (ge_balance_positive_interchange_firstmasklookupvalue) = 0) /\ (ge_balance_negative_interchange_firstmasklookupvalue) = S ge_signed_half_interchange_firstmasklookupvaluedecode))) /\ ((dst_positive_interchange_firstmasklookup) + ge_balance_negative_interchange_firstmasklookupvalue = (dst_negative_interchange_firstmasklookup) + ge_balance_positive_interchange_firstmasklookupvalue))))))))) -> ((((~((dc_index_interchange_firstmask)=0)) /\ (exists dc_quotient_interchange_firstmaskentry dc_left_interchange_firstmaskentry dc_right_interchange_firstmaskentry. (((n)=(dc_index_interchange_firstmask)*dc_quotient_interchange_firstmaskentry) /\ (((exists dst_positive_code_interchange_firstmaskentryleft dst_positive_scale_interchange_firstmaskentryleft dst_negative_code_interchange_firstmaskentryleft dst_negative_scale_interchange_firstmaskentryleft dst_positive_interchange_firstmaskentryleft dst_negative_interchange_firstmaskentryleft. (((F) = (((((dst_positive_code_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft)) * S ((dst_positive_code_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft)) + ((dst_positive_scale_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft))) + (((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) * S ((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) + ((dst_negative_scale_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)))) * S ((((dst_positive_code_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft)) * S ((dst_positive_code_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft)) + ((dst_positive_scale_interchange_firstmaskentryleft) + (dst_positive_scale_interchange_firstmaskentryleft))) + (((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) * S ((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) + ((dst_negative_scale_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)))) + ((((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) * S ((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) + ((dst_negative_scale_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft))) + (((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) * S ((dst_negative_code_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)) + ((dst_negative_scale_interchange_firstmaskentryleft) + (dst_negative_scale_interchange_firstmaskentryleft)))))) /\ (((((exists ff_h_pvs_interchange_firstmaskentryleftpositive. ff_h_pvs_interchange_firstmaskentryleftpositive + S (dst_positive_interchange_firstmaskentryleft) = S ((S (dc_index_interchange_firstmask)) * dst_positive_scale_interchange_firstmaskentryleft)) /\ exists ff_q_pvs_interchange_firstmaskentryleftpositive. dst_positive_code_interchange_firstmaskentryleft = ff_q_pvs_interchange_firstmaskentryleftpositive * S ((S (dc_index_interchange_firstmask)) * dst_positive_scale_interchange_firstmaskentryleft) + (dst_positive_interchange_firstmaskentryleft))) /\ (((((exists ff_h_pvs_interchange_firstmaskentryleftnegative. ff_h_pvs_interchange_firstmaskentryleftnegative + S (dst_negative_interchange_firstmaskentryleft) = S ((S (dc_index_interchange_firstmask)) * dst_negative_scale_interchange_firstmaskentryleft)) /\ exists ff_q_pvs_interchange_firstmaskentryleftnegative. dst_negative_code_interchange_firstmaskentryleft = ff_q_pvs_interchange_firstmaskentryleftnegative * S ((S (dc_index_interchange_firstmask)) * dst_negative_scale_interchange_firstmaskentryleft) + (dst_negative_interchange_firstmaskentryleft))) /\ (exists ge_balance_positive_interchange_firstmaskentryleftvalue ge_balance_negative_interchange_firstmaskentryleftvalue. (((((dc_left_interchange_firstmaskentry) = 2 * (ge_balance_positive_interchange_firstmaskentryleftvalue) /\ (ge_balance_negative_interchange_firstmaskentryleftvalue) = 0) \/ exists ge_signed_half_interchange_firstmaskentryleftvaluedecode. (((dc_left_interchange_firstmaskentry) = 2 * ge_signed_half_interchange_firstmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_interchange_firstmaskentryleftvalue) = 0) /\ (ge_balance_negative_interchange_firstmaskentryleftvalue) = S ge_signed_half_interchange_firstmaskentryleftvaluedecode))) /\ ((dst_positive_interchange_firstmaskentryleft) + ge_balance_negative_interchange_firstmaskentryleftvalue = (dst_negative_interchange_firstmaskentryleft) + ge_balance_positive_interchange_firstmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_interchange_firstmaskentryright dst_positive_scale_interchange_firstmaskentryright dst_negative_code_interchange_firstmaskentryright dst_negative_scale_interchange_firstmaskentryright dst_positive_interchange_firstmaskentryright dst_negative_interchange_firstmaskentryright. (((U) = (((((dst_positive_code_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright)) * S ((dst_positive_code_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright)) + ((dst_positive_scale_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright))) + (((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) * S ((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) + ((dst_negative_scale_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)))) * S ((((dst_positive_code_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright)) * S ((dst_positive_code_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright)) + ((dst_positive_scale_interchange_firstmaskentryright) + (dst_positive_scale_interchange_firstmaskentryright))) + (((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) * S ((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) + ((dst_negative_scale_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)))) + ((((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) * S ((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) + ((dst_negative_scale_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright))) + (((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) * S ((dst_negative_code_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)) + ((dst_negative_scale_interchange_firstmaskentryright) + (dst_negative_scale_interchange_firstmaskentryright)))))) /\ (((((exists ff_h_pvs_interchange_firstmaskentryrightpositive. ff_h_pvs_interchange_firstmaskentryrightpositive + S (dst_positive_interchange_firstmaskentryright) = S ((S (dc_quotient_interchange_firstmaskentry)) * dst_positive_scale_interchange_firstmaskentryright)) /\ exists ff_q_pvs_interchange_firstmaskentryrightpositive. dst_positive_code_interchange_firstmaskentryright = ff_q_pvs_interchange_firstmaskentryrightpositive * S ((S (dc_quotient_interchange_firstmaskentry)) * dst_positive_scale_interchange_firstmaskentryright) + (dst_positive_interchange_firstmaskentryright))) /\ (((((exists ff_h_pvs_interchange_firstmaskentryrightnegative. ff_h_pvs_interchange_firstmaskentryrightnegative + S (dst_negative_interchange_firstmaskentryright) = S ((S (dc_quotient_interchange_firstmaskentry)) * dst_negative_scale_interchange_firstmaskentryright)) /\ exists ff_q_pvs_interchange_firstmaskentryrightnegative. dst_negative_code_interchange_firstmaskentryright = ff_q_pvs_interchange_firstmaskentryrightnegative * S ((S (dc_quotient_interchange_firstmaskentry)) * dst_negative_scale_interchange_firstmaskentryright) + (dst_negative_interchange_firstmaskentryright))) /\ (exists ge_balance_positive_interchange_firstmaskentryrightvalue ge_balance_negative_interchange_firstmaskentryrightvalue. (((((dc_right_interchange_firstmaskentry) = 2 * (ge_balance_positive_interchange_firstmaskentryrightvalue) /\ (ge_balance_negative_interchange_firstmaskentryrightvalue) = 0) \/ exists ge_signed_half_interchange_firstmaskentryrightvaluedecode. (((dc_right_interchange_firstmaskentry) = 2 * ge_signed_half_interchange_firstmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_interchange_firstmaskentryrightvalue) = 0) /\ (ge_balance_negative_interchange_firstmaskentryrightvalue) = S ge_signed_half_interchange_firstmaskentryrightvaluedecode))) /\ ((dst_positive_interchange_firstmaskentryright) + ge_balance_negative_interchange_firstmaskentryrightvalue = (dst_negative_interchange_firstmaskentryright) + ge_balance_positive_interchange_firstmaskentryrightvalue))))))))) /\ (exists sto_ap_interchange_firstmaskentryproduct sto_an_interchange_firstmaskentryproduct sto_bp_interchange_firstmaskentryproduct sto_bn_interchange_firstmaskentryproduct sto_cp_interchange_firstmaskentryproduct sto_cn_interchange_firstmaskentryproduct. (((((dc_left_interchange_firstmaskentry) = 2 * (sto_ap_interchange_firstmaskentryproduct) /\ (sto_an_interchange_firstmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_firstmaskentryproductleft. (((dc_left_interchange_firstmaskentry) = 2 * ge_signed_half_interchange_firstmaskentryproductleft + 1 /\ (sto_ap_interchange_firstmaskentryproduct) = 0) /\ (sto_an_interchange_firstmaskentryproduct) = S ge_signed_half_interchange_firstmaskentryproductleft))) /\ ((((((dc_right_interchange_firstmaskentry) = 2 * (sto_bp_interchange_firstmaskentryproduct) /\ (sto_bn_interchange_firstmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_firstmaskentryproductright. (((dc_right_interchange_firstmaskentry) = 2 * ge_signed_half_interchange_firstmaskentryproductright + 1 /\ (sto_bp_interchange_firstmaskentryproduct) = 0) /\ (sto_bn_interchange_firstmaskentryproduct) = S ge_signed_half_interchange_firstmaskentryproductright))) /\ ((((((dc_value_interchange_firstmask) = 2 * (sto_cp_interchange_firstmaskentryproduct) /\ (sto_cn_interchange_firstmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_firstmaskentryproductoutput. (((dc_value_interchange_firstmask) = 2 * ge_signed_half_interchange_firstmaskentryproductoutput + 1 /\ (sto_cp_interchange_firstmaskentryproduct) = 0) /\ (sto_cn_interchange_firstmaskentryproduct) = S ge_signed_half_interchange_firstmaskentryproductoutput))) /\ ((sto_ap_interchange_firstmaskentryproduct * sto_bp_interchange_firstmaskentryproduct + sto_an_interchange_firstmaskentryproduct * sto_bn_interchange_firstmaskentryproduct) + sto_cn_interchange_firstmaskentryproduct = (sto_ap_interchange_firstmaskentryproduct * sto_bn_interchange_firstmaskentryproduct + sto_an_interchange_firstmaskentryproduct * sto_bp_interchange_firstmaskentryproduct) + sto_cp_interchange_firstmaskentryproduct))))))))))))))) \/ ((((dc_index_interchange_firstmask)=0 \/ ~(exists pvs_factor_interchange_firstmaskentrynondivisor. (n) = (dc_index_interchange_firstmask) * pvs_factor_interchange_firstmaskentrynondivisor)) /\ ((dc_value_interchange_firstmask)=0))))))) /\ (exists dst_positive_code_interchange_firstfold dst_positive_scale_interchange_firstfold dst_negative_code_interchange_firstfold dst_negative_scale_interchange_firstfold dst_positive_sum_interchange_firstfold dst_negative_sum_interchange_firstfold. (((dc_mask_interchange_first) = (((((dst_positive_code_interchange_firstfold) + (dst_positive_scale_interchange_firstfold)) * S ((dst_positive_code_interchange_firstfold) + (dst_positive_scale_interchange_firstfold)) + ((dst_positive_scale_interchange_firstfold) + (dst_positive_scale_interchange_firstfold))) + (((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) * S ((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) + ((dst_negative_scale_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)))) * S ((((dst_positive_code_interchange_firstfold) + (dst_positive_scale_interchange_firstfold)) * S ((dst_positive_code_interchange_firstfold) + (dst_positive_scale_interchange_firstfold)) + ((dst_positive_scale_interchange_firstfold) + (dst_positive_scale_interchange_firstfold))) + (((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) * S ((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) + ((dst_negative_scale_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)))) + ((((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) * S ((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) + ((dst_negative_scale_interchange_firstfold) + (dst_negative_scale_interchange_firstfold))) + (((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) * S ((dst_negative_code_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)) + ((dst_negative_scale_interchange_firstfold) + (dst_negative_scale_interchange_firstfold)))))) /\ (((exists fs_u_dst_interchange_firstfoldpositive fs_v_dst_interchange_firstfoldpositive. ((((exists fs_h_dst_interchange_firstfoldpositive_body_start. fs_h_dst_interchange_firstfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_firstfoldpositive)) /\ exists fs_q_dst_interchange_firstfoldpositive_body_start. fs_u_dst_interchange_firstfoldpositive = fs_q_dst_interchange_firstfoldpositive_body_start * S ((S (0)) * fs_v_dst_interchange_firstfoldpositive) + (0))) /\ ((((exists fs_h_dst_interchange_firstfoldpositive_body_terminal. fs_h_dst_interchange_firstfoldpositive_body_terminal + S (dst_positive_sum_interchange_firstfold) = S ((S (S (n))) * fs_v_dst_interchange_firstfoldpositive)) /\ exists fs_q_dst_interchange_firstfoldpositive_body_terminal. fs_u_dst_interchange_firstfoldpositive = fs_q_dst_interchange_firstfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_interchange_firstfoldpositive) + (dst_positive_sum_interchange_firstfold))) /\ forall fs_i_dst_interchange_firstfoldpositive_body_steps. (exists fs_lt_dst_interchange_firstfoldpositive_body_steps_bound. fs_lt_dst_interchange_firstfoldpositive_body_steps_bound + S fs_i_dst_interchange_firstfoldpositive_body_steps = S (n)) -> exists fs_a_dst_interchange_firstfoldpositive_body_steps fs_r_dst_interchange_firstfoldpositive_body_steps fs_s_dst_interchange_firstfoldpositive_body_steps. ((((exists fs_h_dst_interchange_firstfoldpositive_body_steps_summand. fs_h_dst_interchange_firstfoldpositive_body_steps_summand + S (fs_a_dst_interchange_firstfoldpositive_body_steps) = S ((S (fs_i_dst_interchange_firstfoldpositive_body_steps)) * dst_positive_scale_interchange_firstfold)) /\ exists fs_q_dst_interchange_firstfoldpositive_body_steps_summand. dst_positive_code_interchange_firstfold = fs_q_dst_interchange_firstfoldpositive_body_steps_summand * S ((S (fs_i_dst_interchange_firstfoldpositive_body_steps)) * dst_positive_scale_interchange_firstfold) + (fs_a_dst_interchange_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_firstfoldpositive_body_steps_partial. fs_h_dst_interchange_firstfoldpositive_body_steps_partial + S (fs_r_dst_interchange_firstfoldpositive_body_steps) = S ((S (fs_i_dst_interchange_firstfoldpositive_body_steps)) * fs_v_dst_interchange_firstfoldpositive)) /\ exists fs_q_dst_interchange_firstfoldpositive_body_steps_partial. fs_u_dst_interchange_firstfoldpositive = fs_q_dst_interchange_firstfoldpositive_body_steps_partial * S ((S (fs_i_dst_interchange_firstfoldpositive_body_steps)) * fs_v_dst_interchange_firstfoldpositive) + (fs_r_dst_interchange_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_firstfoldpositive_body_steps_successor. fs_h_dst_interchange_firstfoldpositive_body_steps_successor + S (fs_s_dst_interchange_firstfoldpositive_body_steps) = S ((S (S fs_i_dst_interchange_firstfoldpositive_body_steps)) * fs_v_dst_interchange_firstfoldpositive)) /\ exists fs_q_dst_interchange_firstfoldpositive_body_steps_successor. fs_u_dst_interchange_firstfoldpositive = fs_q_dst_interchange_firstfoldpositive_body_steps_successor * S ((S (S fs_i_dst_interchange_firstfoldpositive_body_steps)) * fs_v_dst_interchange_firstfoldpositive) + (fs_s_dst_interchange_firstfoldpositive_body_steps))) /\ fs_s_dst_interchange_firstfoldpositive_body_steps = fs_r_dst_interchange_firstfoldpositive_body_steps + fs_a_dst_interchange_firstfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_interchange_firstfoldnegative fs_v_dst_interchange_firstfoldnegative. ((((exists fs_h_dst_interchange_firstfoldnegative_body_start. fs_h_dst_interchange_firstfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_firstfoldnegative)) /\ exists fs_q_dst_interchange_firstfoldnegative_body_start. fs_u_dst_interchange_firstfoldnegative = fs_q_dst_interchange_firstfoldnegative_body_start * S ((S (0)) * fs_v_dst_interchange_firstfoldnegative) + (0))) /\ ((((exists fs_h_dst_interchange_firstfoldnegative_body_terminal. fs_h_dst_interchange_firstfoldnegative_body_terminal + S (dst_negative_sum_interchange_firstfold) = S ((S (S (n))) * fs_v_dst_interchange_firstfoldnegative)) /\ exists fs_q_dst_interchange_firstfoldnegative_body_terminal. fs_u_dst_interchange_firstfoldnegative = fs_q_dst_interchange_firstfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_interchange_firstfoldnegative) + (dst_negative_sum_interchange_firstfold))) /\ forall fs_i_dst_interchange_firstfoldnegative_body_steps. (exists fs_lt_dst_interchange_firstfoldnegative_body_steps_bound. fs_lt_dst_interchange_firstfoldnegative_body_steps_bound + S fs_i_dst_interchange_firstfoldnegative_body_steps = S (n)) -> exists fs_a_dst_interchange_firstfoldnegative_body_steps fs_r_dst_interchange_firstfoldnegative_body_steps fs_s_dst_interchange_firstfoldnegative_body_steps. ((((exists fs_h_dst_interchange_firstfoldnegative_body_steps_summand. fs_h_dst_interchange_firstfoldnegative_body_steps_summand + S (fs_a_dst_interchange_firstfoldnegative_body_steps) = S ((S (fs_i_dst_interchange_firstfoldnegative_body_steps)) * dst_negative_scale_interchange_firstfold)) /\ exists fs_q_dst_interchange_firstfoldnegative_body_steps_summand. dst_negative_code_interchange_firstfold = fs_q_dst_interchange_firstfoldnegative_body_steps_summand * S ((S (fs_i_dst_interchange_firstfoldnegative_body_steps)) * dst_negative_scale_interchange_firstfold) + (fs_a_dst_interchange_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_firstfoldnegative_body_steps_partial. fs_h_dst_interchange_firstfoldnegative_body_steps_partial + S (fs_r_dst_interchange_firstfoldnegative_body_steps) = S ((S (fs_i_dst_interchange_firstfoldnegative_body_steps)) * fs_v_dst_interchange_firstfoldnegative)) /\ exists fs_q_dst_interchange_firstfoldnegative_body_steps_partial. fs_u_dst_interchange_firstfoldnegative = fs_q_dst_interchange_firstfoldnegative_body_steps_partial * S ((S (fs_i_dst_interchange_firstfoldnegative_body_steps)) * fs_v_dst_interchange_firstfoldnegative) + (fs_r_dst_interchange_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_firstfoldnegative_body_steps_successor. fs_h_dst_interchange_firstfoldnegative_body_steps_successor + S (fs_s_dst_interchange_firstfoldnegative_body_steps) = S ((S (S fs_i_dst_interchange_firstfoldnegative_body_steps)) * fs_v_dst_interchange_firstfoldnegative)) /\ exists fs_q_dst_interchange_firstfoldnegative_body_steps_successor. fs_u_dst_interchange_firstfoldnegative = fs_q_dst_interchange_firstfoldnegative_body_steps_successor * S ((S (S fs_i_dst_interchange_firstfoldnegative_body_steps)) * fs_v_dst_interchange_firstfoldnegative) + (fs_s_dst_interchange_firstfoldnegative_body_steps))) /\ fs_s_dst_interchange_firstfoldnegative_body_steps = fs_r_dst_interchange_firstfoldnegative_body_steps + fs_a_dst_interchange_firstfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_interchange_firstfoldresult ge_balance_negative_interchange_firstfoldresult. (((((a) = 2 * (ge_balance_positive_interchange_firstfoldresult) /\ (ge_balance_negative_interchange_firstfoldresult) = 0) \/ exists ge_signed_half_interchange_firstfoldresultdecode. (((a) = 2 * ge_signed_half_interchange_firstfoldresultdecode + 1 /\ (ge_balance_positive_interchange_firstfoldresult) = 0) /\ (ge_balance_negative_interchange_firstfoldresult) = S ge_signed_half_interchange_firstfoldresultdecode))) /\ ((dst_positive_sum_interchange_firstfold) + ge_balance_negative_interchange_firstfoldresult = (dst_negative_sum_interchange_firstfold) + ge_balance_positive_interchange_firstfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_interchange_second. ((((exists dst_positive_code_interchange_secondmasktable dst_positive_scale_interchange_secondmasktable dst_negative_code_interchange_secondmasktable dst_negative_scale_interchange_secondmasktable. (((dc_mask_interchange_second) = (((((dst_positive_code_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable)) * S ((dst_positive_code_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable)) + ((dst_positive_scale_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable))) + (((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) * S ((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) + ((dst_negative_scale_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)))) * S ((((dst_positive_code_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable)) * S ((dst_positive_code_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable)) + ((dst_positive_scale_interchange_secondmasktable) + (dst_positive_scale_interchange_secondmasktable))) + (((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) * S ((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) + ((dst_negative_scale_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)))) + ((((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) * S ((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) + ((dst_negative_scale_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable))) + (((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) * S ((dst_negative_code_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)) + ((dst_negative_scale_interchange_secondmasktable) + (dst_negative_scale_interchange_secondmasktable)))))) /\ (forall dst_index_interchange_secondmasktable. (exists pvs_le_gap_interchange_secondmasktabledomain. pvs_le_gap_interchange_secondmasktabledomain + (dst_index_interchange_secondmasktable) = (n)) -> exists dst_positive_interchange_secondmasktable dst_negative_interchange_secondmasktable dst_value_interchange_secondmasktable. ((((exists ff_h_pvs_interchange_secondmasktableentrypositive. ff_h_pvs_interchange_secondmasktableentrypositive + S (dst_positive_interchange_secondmasktable) = S ((S (dst_index_interchange_secondmasktable)) * dst_positive_scale_interchange_secondmasktable)) /\ exists ff_q_pvs_interchange_secondmasktableentrypositive. dst_positive_code_interchange_secondmasktable = ff_q_pvs_interchange_secondmasktableentrypositive * S ((S (dst_index_interchange_secondmasktable)) * dst_positive_scale_interchange_secondmasktable) + (dst_positive_interchange_secondmasktable))) /\ (((((exists ff_h_pvs_interchange_secondmasktableentrynegative. ff_h_pvs_interchange_secondmasktableentrynegative + S (dst_negative_interchange_secondmasktable) = S ((S (dst_index_interchange_secondmasktable)) * dst_negative_scale_interchange_secondmasktable)) /\ exists ff_q_pvs_interchange_secondmasktableentrynegative. dst_negative_code_interchange_secondmasktable = ff_q_pvs_interchange_secondmasktableentrynegative * S ((S (dst_index_interchange_secondmasktable)) * dst_negative_scale_interchange_secondmasktable) + (dst_negative_interchange_secondmasktable))) /\ (exists ge_balance_positive_interchange_secondmasktableentryvalue ge_balance_negative_interchange_secondmasktableentryvalue. (((((dst_value_interchange_secondmasktable) = 2 * (ge_balance_positive_interchange_secondmasktableentryvalue) /\ (ge_balance_negative_interchange_secondmasktableentryvalue) = 0) \/ exists ge_signed_half_interchange_secondmasktableentryvaluedecode. (((dst_value_interchange_secondmasktable) = 2 * ge_signed_half_interchange_secondmasktableentryvaluedecode + 1 /\ (ge_balance_positive_interchange_secondmasktableentryvalue) = 0) /\ (ge_balance_negative_interchange_secondmasktableentryvalue) = S ge_signed_half_interchange_secondmasktableentryvaluedecode))) /\ ((dst_positive_interchange_secondmasktable) + ge_balance_negative_interchange_secondmasktableentryvalue = (dst_negative_interchange_secondmasktable) + ge_balance_positive_interchange_secondmasktableentryvalue))))))))) /\ (forall dc_index_interchange_secondmask dc_value_interchange_secondmask. (exists pvs_le_gap_interchange_secondmaskdomain. pvs_le_gap_interchange_secondmaskdomain + (dc_index_interchange_secondmask) = (n)) -> (exists dst_positive_code_interchange_secondmasklookup dst_positive_scale_interchange_secondmasklookup dst_negative_code_interchange_secondmasklookup dst_negative_scale_interchange_secondmasklookup dst_positive_interchange_secondmasklookup dst_negative_interchange_secondmasklookup. (((dc_mask_interchange_second) = (((((dst_positive_code_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup)) * S ((dst_positive_code_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup)) + ((dst_positive_scale_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup))) + (((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) * S ((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) + ((dst_negative_scale_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)))) * S ((((dst_positive_code_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup)) * S ((dst_positive_code_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup)) + ((dst_positive_scale_interchange_secondmasklookup) + (dst_positive_scale_interchange_secondmasklookup))) + (((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) * S ((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) + ((dst_negative_scale_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)))) + ((((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) * S ((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) + ((dst_negative_scale_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup))) + (((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) * S ((dst_negative_code_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)) + ((dst_negative_scale_interchange_secondmasklookup) + (dst_negative_scale_interchange_secondmasklookup)))))) /\ (((((exists ff_h_pvs_interchange_secondmasklookuppositive. ff_h_pvs_interchange_secondmasklookuppositive + S (dst_positive_interchange_secondmasklookup) = S ((S (dc_index_interchange_secondmask)) * dst_positive_scale_interchange_secondmasklookup)) /\ exists ff_q_pvs_interchange_secondmasklookuppositive. dst_positive_code_interchange_secondmasklookup = ff_q_pvs_interchange_secondmasklookuppositive * S ((S (dc_index_interchange_secondmask)) * dst_positive_scale_interchange_secondmasklookup) + (dst_positive_interchange_secondmasklookup))) /\ (((((exists ff_h_pvs_interchange_secondmasklookupnegative. ff_h_pvs_interchange_secondmasklookupnegative + S (dst_negative_interchange_secondmasklookup) = S ((S (dc_index_interchange_secondmask)) * dst_negative_scale_interchange_secondmasklookup)) /\ exists ff_q_pvs_interchange_secondmasklookupnegative. dst_negative_code_interchange_secondmasklookup = ff_q_pvs_interchange_secondmasklookupnegative * S ((S (dc_index_interchange_secondmask)) * dst_negative_scale_interchange_secondmasklookup) + (dst_negative_interchange_secondmasklookup))) /\ (exists ge_balance_positive_interchange_secondmasklookupvalue ge_balance_negative_interchange_secondmasklookupvalue. (((((dc_value_interchange_secondmask) = 2 * (ge_balance_positive_interchange_secondmasklookupvalue) /\ (ge_balance_negative_interchange_secondmasklookupvalue) = 0) \/ exists ge_signed_half_interchange_secondmasklookupvaluedecode. (((dc_value_interchange_secondmask) = 2 * ge_signed_half_interchange_secondmasklookupvaluedecode + 1 /\ (ge_balance_positive_interchange_secondmasklookupvalue) = 0) /\ (ge_balance_negative_interchange_secondmasklookupvalue) = S ge_signed_half_interchange_secondmasklookupvaluedecode))) /\ ((dst_positive_interchange_secondmasklookup) + ge_balance_negative_interchange_secondmasklookupvalue = (dst_negative_interchange_secondmasklookup) + ge_balance_positive_interchange_secondmasklookupvalue))))))))) -> ((((~((dc_index_interchange_secondmask)=0)) /\ (exists dc_quotient_interchange_secondmaskentry dc_left_interchange_secondmaskentry dc_right_interchange_secondmaskentry. (((n)=(dc_index_interchange_secondmask)*dc_quotient_interchange_secondmaskentry) /\ (((exists dst_positive_code_interchange_secondmaskentryleft dst_positive_scale_interchange_secondmaskentryleft dst_negative_code_interchange_secondmaskentryleft dst_negative_scale_interchange_secondmaskentryleft dst_positive_interchange_secondmaskentryleft dst_negative_interchange_secondmaskentryleft. (((H) = (((((dst_positive_code_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft)) * S ((dst_positive_code_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft)) + ((dst_positive_scale_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft))) + (((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) * S ((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) + ((dst_negative_scale_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)))) * S ((((dst_positive_code_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft)) * S ((dst_positive_code_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft)) + ((dst_positive_scale_interchange_secondmaskentryleft) + (dst_positive_scale_interchange_secondmaskentryleft))) + (((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) * S ((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) + ((dst_negative_scale_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)))) + ((((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) * S ((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) + ((dst_negative_scale_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft))) + (((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) * S ((dst_negative_code_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)) + ((dst_negative_scale_interchange_secondmaskentryleft) + (dst_negative_scale_interchange_secondmaskentryleft)))))) /\ (((((exists ff_h_pvs_interchange_secondmaskentryleftpositive. ff_h_pvs_interchange_secondmaskentryleftpositive + S (dst_positive_interchange_secondmaskentryleft) = S ((S (dc_index_interchange_secondmask)) * dst_positive_scale_interchange_secondmaskentryleft)) /\ exists ff_q_pvs_interchange_secondmaskentryleftpositive. dst_positive_code_interchange_secondmaskentryleft = ff_q_pvs_interchange_secondmaskentryleftpositive * S ((S (dc_index_interchange_secondmask)) * dst_positive_scale_interchange_secondmaskentryleft) + (dst_positive_interchange_secondmaskentryleft))) /\ (((((exists ff_h_pvs_interchange_secondmaskentryleftnegative. ff_h_pvs_interchange_secondmaskentryleftnegative + S (dst_negative_interchange_secondmaskentryleft) = S ((S (dc_index_interchange_secondmask)) * dst_negative_scale_interchange_secondmaskentryleft)) /\ exists ff_q_pvs_interchange_secondmaskentryleftnegative. dst_negative_code_interchange_secondmaskentryleft = ff_q_pvs_interchange_secondmaskentryleftnegative * S ((S (dc_index_interchange_secondmask)) * dst_negative_scale_interchange_secondmaskentryleft) + (dst_negative_interchange_secondmaskentryleft))) /\ (exists ge_balance_positive_interchange_secondmaskentryleftvalue ge_balance_negative_interchange_secondmaskentryleftvalue. (((((dc_left_interchange_secondmaskentry) = 2 * (ge_balance_positive_interchange_secondmaskentryleftvalue) /\ (ge_balance_negative_interchange_secondmaskentryleftvalue) = 0) \/ exists ge_signed_half_interchange_secondmaskentryleftvaluedecode. (((dc_left_interchange_secondmaskentry) = 2 * ge_signed_half_interchange_secondmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_interchange_secondmaskentryleftvalue) = 0) /\ (ge_balance_negative_interchange_secondmaskentryleftvalue) = S ge_signed_half_interchange_secondmaskentryleftvaluedecode))) /\ ((dst_positive_interchange_secondmaskentryleft) + ge_balance_negative_interchange_secondmaskentryleftvalue = (dst_negative_interchange_secondmaskentryleft) + ge_balance_positive_interchange_secondmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_interchange_secondmaskentryright dst_positive_scale_interchange_secondmaskentryright dst_negative_code_interchange_secondmaskentryright dst_negative_scale_interchange_secondmaskentryright dst_positive_interchange_secondmaskentryright dst_negative_interchange_secondmaskentryright. (((V) = (((((dst_positive_code_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright)) * S ((dst_positive_code_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright)) + ((dst_positive_scale_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright))) + (((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) * S ((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) + ((dst_negative_scale_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)))) * S ((((dst_positive_code_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright)) * S ((dst_positive_code_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright)) + ((dst_positive_scale_interchange_secondmaskentryright) + (dst_positive_scale_interchange_secondmaskentryright))) + (((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) * S ((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) + ((dst_negative_scale_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)))) + ((((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) * S ((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) + ((dst_negative_scale_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright))) + (((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) * S ((dst_negative_code_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)) + ((dst_negative_scale_interchange_secondmaskentryright) + (dst_negative_scale_interchange_secondmaskentryright)))))) /\ (((((exists ff_h_pvs_interchange_secondmaskentryrightpositive. ff_h_pvs_interchange_secondmaskentryrightpositive + S (dst_positive_interchange_secondmaskentryright) = S ((S (dc_quotient_interchange_secondmaskentry)) * dst_positive_scale_interchange_secondmaskentryright)) /\ exists ff_q_pvs_interchange_secondmaskentryrightpositive. dst_positive_code_interchange_secondmaskentryright = ff_q_pvs_interchange_secondmaskentryrightpositive * S ((S (dc_quotient_interchange_secondmaskentry)) * dst_positive_scale_interchange_secondmaskentryright) + (dst_positive_interchange_secondmaskentryright))) /\ (((((exists ff_h_pvs_interchange_secondmaskentryrightnegative. ff_h_pvs_interchange_secondmaskentryrightnegative + S (dst_negative_interchange_secondmaskentryright) = S ((S (dc_quotient_interchange_secondmaskentry)) * dst_negative_scale_interchange_secondmaskentryright)) /\ exists ff_q_pvs_interchange_secondmaskentryrightnegative. dst_negative_code_interchange_secondmaskentryright = ff_q_pvs_interchange_secondmaskentryrightnegative * S ((S (dc_quotient_interchange_secondmaskentry)) * dst_negative_scale_interchange_secondmaskentryright) + (dst_negative_interchange_secondmaskentryright))) /\ (exists ge_balance_positive_interchange_secondmaskentryrightvalue ge_balance_negative_interchange_secondmaskentryrightvalue. (((((dc_right_interchange_secondmaskentry) = 2 * (ge_balance_positive_interchange_secondmaskentryrightvalue) /\ (ge_balance_negative_interchange_secondmaskentryrightvalue) = 0) \/ exists ge_signed_half_interchange_secondmaskentryrightvaluedecode. (((dc_right_interchange_secondmaskentry) = 2 * ge_signed_half_interchange_secondmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_interchange_secondmaskentryrightvalue) = 0) /\ (ge_balance_negative_interchange_secondmaskentryrightvalue) = S ge_signed_half_interchange_secondmaskentryrightvaluedecode))) /\ ((dst_positive_interchange_secondmaskentryright) + ge_balance_negative_interchange_secondmaskentryrightvalue = (dst_negative_interchange_secondmaskentryright) + ge_balance_positive_interchange_secondmaskentryrightvalue))))))))) /\ (exists sto_ap_interchange_secondmaskentryproduct sto_an_interchange_secondmaskentryproduct sto_bp_interchange_secondmaskentryproduct sto_bn_interchange_secondmaskentryproduct sto_cp_interchange_secondmaskentryproduct sto_cn_interchange_secondmaskentryproduct. (((((dc_left_interchange_secondmaskentry) = 2 * (sto_ap_interchange_secondmaskentryproduct) /\ (sto_an_interchange_secondmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_secondmaskentryproductleft. (((dc_left_interchange_secondmaskentry) = 2 * ge_signed_half_interchange_secondmaskentryproductleft + 1 /\ (sto_ap_interchange_secondmaskentryproduct) = 0) /\ (sto_an_interchange_secondmaskentryproduct) = S ge_signed_half_interchange_secondmaskentryproductleft))) /\ ((((((dc_right_interchange_secondmaskentry) = 2 * (sto_bp_interchange_secondmaskentryproduct) /\ (sto_bn_interchange_secondmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_secondmaskentryproductright. (((dc_right_interchange_secondmaskentry) = 2 * ge_signed_half_interchange_secondmaskentryproductright + 1 /\ (sto_bp_interchange_secondmaskentryproduct) = 0) /\ (sto_bn_interchange_secondmaskentryproduct) = S ge_signed_half_interchange_secondmaskentryproductright))) /\ ((((((dc_value_interchange_secondmask) = 2 * (sto_cp_interchange_secondmaskentryproduct) /\ (sto_cn_interchange_secondmaskentryproduct) = 0) \/ exists ge_signed_half_interchange_secondmaskentryproductoutput. (((dc_value_interchange_secondmask) = 2 * ge_signed_half_interchange_secondmaskentryproductoutput + 1 /\ (sto_cp_interchange_secondmaskentryproduct) = 0) /\ (sto_cn_interchange_secondmaskentryproduct) = S ge_signed_half_interchange_secondmaskentryproductoutput))) /\ ((sto_ap_interchange_secondmaskentryproduct * sto_bp_interchange_secondmaskentryproduct + sto_an_interchange_secondmaskentryproduct * sto_bn_interchange_secondmaskentryproduct) + sto_cn_interchange_secondmaskentryproduct = (sto_ap_interchange_secondmaskentryproduct * sto_bn_interchange_secondmaskentryproduct + sto_an_interchange_secondmaskentryproduct * sto_bp_interchange_secondmaskentryproduct) + sto_cp_interchange_secondmaskentryproduct))))))))))))))) \/ ((((dc_index_interchange_secondmask)=0 \/ ~(exists pvs_factor_interchange_secondmaskentrynondivisor. (n) = (dc_index_interchange_secondmask) * pvs_factor_interchange_secondmaskentrynondivisor)) /\ ((dc_value_interchange_secondmask)=0))))))) /\ (exists dst_positive_code_interchange_secondfold dst_positive_scale_interchange_secondfold dst_negative_code_interchange_secondfold dst_negative_scale_interchange_secondfold dst_positive_sum_interchange_secondfold dst_negative_sum_interchange_secondfold. (((dc_mask_interchange_second) = (((((dst_positive_code_interchange_secondfold) + (dst_positive_scale_interchange_secondfold)) * S ((dst_positive_code_interchange_secondfold) + (dst_positive_scale_interchange_secondfold)) + ((dst_positive_scale_interchange_secondfold) + (dst_positive_scale_interchange_secondfold))) + (((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) * S ((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) + ((dst_negative_scale_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)))) * S ((((dst_positive_code_interchange_secondfold) + (dst_positive_scale_interchange_secondfold)) * S ((dst_positive_code_interchange_secondfold) + (dst_positive_scale_interchange_secondfold)) + ((dst_positive_scale_interchange_secondfold) + (dst_positive_scale_interchange_secondfold))) + (((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) * S ((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) + ((dst_negative_scale_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)))) + ((((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) * S ((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) + ((dst_negative_scale_interchange_secondfold) + (dst_negative_scale_interchange_secondfold))) + (((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) * S ((dst_negative_code_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)) + ((dst_negative_scale_interchange_secondfold) + (dst_negative_scale_interchange_secondfold)))))) /\ (((exists fs_u_dst_interchange_secondfoldpositive fs_v_dst_interchange_secondfoldpositive. ((((exists fs_h_dst_interchange_secondfoldpositive_body_start. fs_h_dst_interchange_secondfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_secondfoldpositive)) /\ exists fs_q_dst_interchange_secondfoldpositive_body_start. fs_u_dst_interchange_secondfoldpositive = fs_q_dst_interchange_secondfoldpositive_body_start * S ((S (0)) * fs_v_dst_interchange_secondfoldpositive) + (0))) /\ ((((exists fs_h_dst_interchange_secondfoldpositive_body_terminal. fs_h_dst_interchange_secondfoldpositive_body_terminal + S (dst_positive_sum_interchange_secondfold) = S ((S (S (n))) * fs_v_dst_interchange_secondfoldpositive)) /\ exists fs_q_dst_interchange_secondfoldpositive_body_terminal. fs_u_dst_interchange_secondfoldpositive = fs_q_dst_interchange_secondfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_interchange_secondfoldpositive) + (dst_positive_sum_interchange_secondfold))) /\ forall fs_i_dst_interchange_secondfoldpositive_body_steps. (exists fs_lt_dst_interchange_secondfoldpositive_body_steps_bound. fs_lt_dst_interchange_secondfoldpositive_body_steps_bound + S fs_i_dst_interchange_secondfoldpositive_body_steps = S (n)) -> exists fs_a_dst_interchange_secondfoldpositive_body_steps fs_r_dst_interchange_secondfoldpositive_body_steps fs_s_dst_interchange_secondfoldpositive_body_steps. ((((exists fs_h_dst_interchange_secondfoldpositive_body_steps_summand. fs_h_dst_interchange_secondfoldpositive_body_steps_summand + S (fs_a_dst_interchange_secondfoldpositive_body_steps) = S ((S (fs_i_dst_interchange_secondfoldpositive_body_steps)) * dst_positive_scale_interchange_secondfold)) /\ exists fs_q_dst_interchange_secondfoldpositive_body_steps_summand. dst_positive_code_interchange_secondfold = fs_q_dst_interchange_secondfoldpositive_body_steps_summand * S ((S (fs_i_dst_interchange_secondfoldpositive_body_steps)) * dst_positive_scale_interchange_secondfold) + (fs_a_dst_interchange_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_secondfoldpositive_body_steps_partial. fs_h_dst_interchange_secondfoldpositive_body_steps_partial + S (fs_r_dst_interchange_secondfoldpositive_body_steps) = S ((S (fs_i_dst_interchange_secondfoldpositive_body_steps)) * fs_v_dst_interchange_secondfoldpositive)) /\ exists fs_q_dst_interchange_secondfoldpositive_body_steps_partial. fs_u_dst_interchange_secondfoldpositive = fs_q_dst_interchange_secondfoldpositive_body_steps_partial * S ((S (fs_i_dst_interchange_secondfoldpositive_body_steps)) * fs_v_dst_interchange_secondfoldpositive) + (fs_r_dst_interchange_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_interchange_secondfoldpositive_body_steps_successor. fs_h_dst_interchange_secondfoldpositive_body_steps_successor + S (fs_s_dst_interchange_secondfoldpositive_body_steps) = S ((S (S fs_i_dst_interchange_secondfoldpositive_body_steps)) * fs_v_dst_interchange_secondfoldpositive)) /\ exists fs_q_dst_interchange_secondfoldpositive_body_steps_successor. fs_u_dst_interchange_secondfoldpositive = fs_q_dst_interchange_secondfoldpositive_body_steps_successor * S ((S (S fs_i_dst_interchange_secondfoldpositive_body_steps)) * fs_v_dst_interchange_secondfoldpositive) + (fs_s_dst_interchange_secondfoldpositive_body_steps))) /\ fs_s_dst_interchange_secondfoldpositive_body_steps = fs_r_dst_interchange_secondfoldpositive_body_steps + fs_a_dst_interchange_secondfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_interchange_secondfoldnegative fs_v_dst_interchange_secondfoldnegative. ((((exists fs_h_dst_interchange_secondfoldnegative_body_start. fs_h_dst_interchange_secondfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_interchange_secondfoldnegative)) /\ exists fs_q_dst_interchange_secondfoldnegative_body_start. fs_u_dst_interchange_secondfoldnegative = fs_q_dst_interchange_secondfoldnegative_body_start * S ((S (0)) * fs_v_dst_interchange_secondfoldnegative) + (0))) /\ ((((exists fs_h_dst_interchange_secondfoldnegative_body_terminal. fs_h_dst_interchange_secondfoldnegative_body_terminal + S (dst_negative_sum_interchange_secondfold) = S ((S (S (n))) * fs_v_dst_interchange_secondfoldnegative)) /\ exists fs_q_dst_interchange_secondfoldnegative_body_terminal. fs_u_dst_interchange_secondfoldnegative = fs_q_dst_interchange_secondfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_interchange_secondfoldnegative) + (dst_negative_sum_interchange_secondfold))) /\ forall fs_i_dst_interchange_secondfoldnegative_body_steps. (exists fs_lt_dst_interchange_secondfoldnegative_body_steps_bound. fs_lt_dst_interchange_secondfoldnegative_body_steps_bound + S fs_i_dst_interchange_secondfoldnegative_body_steps = S (n)) -> exists fs_a_dst_interchange_secondfoldnegative_body_steps fs_r_dst_interchange_secondfoldnegative_body_steps fs_s_dst_interchange_secondfoldnegative_body_steps. ((((exists fs_h_dst_interchange_secondfoldnegative_body_steps_summand. fs_h_dst_interchange_secondfoldnegative_body_steps_summand + S (fs_a_dst_interchange_secondfoldnegative_body_steps) = S ((S (fs_i_dst_interchange_secondfoldnegative_body_steps)) * dst_negative_scale_interchange_secondfold)) /\ exists fs_q_dst_interchange_secondfoldnegative_body_steps_summand. dst_negative_code_interchange_secondfold = fs_q_dst_interchange_secondfoldnegative_body_steps_summand * S ((S (fs_i_dst_interchange_secondfoldnegative_body_steps)) * dst_negative_scale_interchange_secondfold) + (fs_a_dst_interchange_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_secondfoldnegative_body_steps_partial. fs_h_dst_interchange_secondfoldnegative_body_steps_partial + S (fs_r_dst_interchange_secondfoldnegative_body_steps) = S ((S (fs_i_dst_interchange_secondfoldnegative_body_steps)) * fs_v_dst_interchange_secondfoldnegative)) /\ exists fs_q_dst_interchange_secondfoldnegative_body_steps_partial. fs_u_dst_interchange_secondfoldnegative = fs_q_dst_interchange_secondfoldnegative_body_steps_partial * S ((S (fs_i_dst_interchange_secondfoldnegative_body_steps)) * fs_v_dst_interchange_secondfoldnegative) + (fs_r_dst_interchange_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_interchange_secondfoldnegative_body_steps_successor. fs_h_dst_interchange_secondfoldnegative_body_steps_successor + S (fs_s_dst_interchange_secondfoldnegative_body_steps) = S ((S (S fs_i_dst_interchange_secondfoldnegative_body_steps)) * fs_v_dst_interchange_secondfoldnegative)) /\ exists fs_q_dst_interchange_secondfoldnegative_body_steps_successor. fs_u_dst_interchange_secondfoldnegative = fs_q_dst_interchange_secondfoldnegative_body_steps_successor * S ((S (S fs_i_dst_interchange_secondfoldnegative_body_steps)) * fs_v_dst_interchange_secondfoldnegative) + (fs_s_dst_interchange_secondfoldnegative_body_steps))) /\ fs_s_dst_interchange_secondfoldnegative_body_steps = fs_r_dst_interchange_secondfoldnegative_body_steps + fs_a_dst_interchange_secondfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_interchange_secondfoldresult ge_balance_negative_interchange_secondfoldresult. (((((b) = 2 * (ge_balance_positive_interchange_secondfoldresult) /\ (ge_balance_negative_interchange_secondfoldresult) = 0) \/ exists ge_signed_half_interchange_secondfoldresultdecode. (((b) = 2 * ge_signed_half_interchange_secondfoldresultdecode + 1 /\ (ge_balance_positive_interchange_secondfoldresult) = 0) /\ (ge_balance_negative_interchange_secondfoldresult) = S ge_signed_half_interchange_secondfoldresultdecode))) /\ ((dst_positive_sum_interchange_secondfold) + ge_balance_negative_interchange_secondfoldresult = (dst_negative_sum_interchange_secondfold) + ge_balance_positive_interchange_secondfoldresult))))))))))))) -> a=b

Complete tactic proof in conservative notation

All 114 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

114 script commands · 27 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
dirichlet grid fubini existsdirichlet grid row sums convolution prefixdirichlet grid column sums convolution prefix
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro H
  5. L5
    intro U
  6. L6
    intro V
  7. L7
    intro n
  8. L8
    intro a
  9. L9
    intro b
  10. L10
    intro hU
02Fix variables and assumptionsL11–15

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hV
  2. L12
    intro hn
  3. L13
    intro hN
  4. L14
    intro ha
  5. L15
    intro hb
03Establish hfL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet grid fubini exists.

  1. L16
    have hf : ∃ T. ∃ R. ∃ C. ∃ z. DirichletGrid(F,G,H,n,T) ∧ (ArithRowSums(T,R,0,S n,1,S n,S n) ∧ (ArithRowSums(T,C,0,1,S n,S n,S n) ∧ (SignedPrefixSum(R,S n,z) ∧ SignedPrefixSum(C,S n,z))))Definitions: DirichletGrid(F,G,H,n,T)ArithRowSums(T,R,0,S n,1,S n,S n)ArithRowSums(T,C,0,1,S n,S n,S n)SignedPrefixSum(R,S n,z)SignedPrefixSum(C,S n,z)Original native command in the exact edition
  2. L17
    specialize dirichlet_grid_fubini_exists (F)
  3. L18
    specialize dirichlet_grid_fubini_exists (G)
  4. L19
    specialize dirichlet_grid_fubini_exists (H)
  5. L20
    specialize dirichlet_grid_fubini_exists (n)
  6. L21
    apply dirichlet_grid_fubini_exists
  7. L22
    specialize signed_table_domain_resize (N)
  8. L23
    specialize signed_table_domain_resize (0)
  9. L24
    specialize signed_table_domain_resize (F)
  10. L25
    apply signed_table_domain_resize
04Separate the logical casesL26–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L26
    cases hV
  2. L27
    cases hV_right
  3. L28
    cases hV_right_right
05Use earlier factsL29–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L29
    exact hV_left
  2. L30
    specialize signed_table_domain_resize (N)
  3. L31
    specialize signed_table_domain_resize (0)
  4. L32
    specialize signed_table_domain_resize (G)
  5. L33
    apply signed_table_domain_resize
06Separate the logical casesL34–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L34
    cases hU
  2. L35
    cases hU_right
  3. L36
    cases hU_right_right
07Use earlier factsL37–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L37
    exact hU_right_left
  2. L38
    specialize signed_table_domain_resize (N)
  3. L39
    specialize signed_table_domain_resize (0)
  4. L40
    specialize signed_table_domain_resize (H)
  5. L41
    apply signed_table_domain_resize
08Separate the logical casesL42–44

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L42
    cases hU
  2. L43
    cases hU_right
  3. L44
    cases hU_right_right
09Use earlier factsL45–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    exact hU_left
10Separate the logical casesL46–53

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L46
    cases hf
  2. L47
    cases hf_witness
  3. L48
    cases hf_witness_witness
  4. L49
    cases hf_witness_witness_witness
  5. L50
    cases hf_witness_witness_witness_witness
  6. L51
    cases hf_witness_witness_witness_witness_right
  7. L52
    cases hf_witness_witness_witness_witness_right_right
  8. L53
    cases hf_witness_witness_witness_witness_right_right_right
11Calculate and transport equalitiesL54–54

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L54
    trans x3
12Use earlier factsL55–61

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L55
    specialize dirichlet_convolution_sum_functional (F)
  2. L56
    specialize dirichlet_convolution_sum_functional (U)
  3. L57
    specialize dirichlet_convolution_sum_functional (n)
  4. L58
    specialize dirichlet_convolution_sum_functional (a)
  5. L59
    specialize dirichlet_convolution_sum_functional (x3)
  6. L60
    apply dirichlet_convolution_sum_functional
  7. L61
    exact ha
13Separate the logical casesL62–62

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L62
    split
14Use earlier factsL63–63

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L63
    exact hn
15Construct an explicit witnessL64–64

Supply the displayed value, then prove that it has the required property.

  1. L64
    exists x1
16Separate the logical casesL65–65

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L65
    split
17Use earlier factsL66–74

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L66
    specialize dirichlet_grid_row_sums_convolution_prefix (N)
  2. L67
    specialize dirichlet_grid_row_sums_convolution_prefix (F)
  3. L68
    specialize dirichlet_grid_row_sums_convolution_prefix (G)
  4. L69
    specialize dirichlet_grid_row_sums_convolution_prefix (H)
  5. L70
    specialize dirichlet_grid_row_sums_convolution_prefix (U)
  6. L71
    specialize dirichlet_grid_row_sums_convolution_prefix (n)
  7. L72
    specialize dirichlet_grid_row_sums_convolution_prefix (x)
  8. L73
    specialize dirichlet_grid_row_sums_convolution_prefix (x1)
  9. L74
    apply dirichlet_grid_row_sums_convolution_prefix
18Separate the logical casesL75–77

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L75
    cases hV
  2. L76
    cases hV_right
  3. L77
    cases hV_right_right
19Use earlier factsL78–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L78
    exact hV_left
  2. L79
    exact hU
  3. L80
    exact hn
  4. L81
    exact hN
  5. L82
    exact hf_witness_witness_witness_witness_left
  6. L83
    exact hf_witness_witness_witness_witness_right_left
  7. L84
    exact hf_witness_witness_witness_witness_right_right_right_left
  8. L85
    specialize dirichlet_convolution_sum_functional (H)
  9. L86
    specialize dirichlet_convolution_sum_functional (V)
  10. L87
    specialize dirichlet_convolution_sum_functional (n)
20Use earlier factsL88–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L88
    specialize dirichlet_convolution_sum_functional (x3)
  2. L89
    specialize dirichlet_convolution_sum_functional (b)
  3. L90
    apply dirichlet_convolution_sum_functional
21Separate the logical casesL91–91

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L91
    split
22Use earlier factsL92–92

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L92
    exact hn
23Construct an explicit witnessL93–93

Supply the displayed value, then prove that it has the required property.

  1. L93
    exists x2
24Separate the logical casesL94–94

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L94
    split
25Use earlier factsL95–103

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L95
    specialize dirichlet_grid_column_sums_convolution_prefix (N)
  2. L96
    specialize dirichlet_grid_column_sums_convolution_prefix (F)
  3. L97
    specialize dirichlet_grid_column_sums_convolution_prefix (G)
  4. L98
    specialize dirichlet_grid_column_sums_convolution_prefix (H)
  5. L99
    specialize dirichlet_grid_column_sums_convolution_prefix (V)
  6. L100
    specialize dirichlet_grid_column_sums_convolution_prefix (n)
  7. L101
    specialize dirichlet_grid_column_sums_convolution_prefix (x)
  8. L102
    specialize dirichlet_grid_column_sums_convolution_prefix (x2)
  9. L103
    apply dirichlet_grid_column_sums_convolution_prefix
26Separate the logical casesL104–106

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L104
    cases hU
  2. L105
    cases hU_right
  3. L106
    cases hU_right_right
27Use earlier factsL107–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L107
    exact hU_left
  2. L108
    exact hV
  3. L109
    exact hn
  4. L110
    exact hN
  5. L111
    exact hf_witness_witness_witness_witness_left
  6. L112
    exact hf_witness_witness_witness_witness_right_right_left
  7. L113
    exact hf_witness_witness_witness_witness_right_right_right_right
  8. L114
    exact hb

Library-wide reading audit

Original defined command ledger · 114 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro G
  4. 0004intro H
  5. 0005intro U
  6. 0006intro V
  7. 0007intro n
  8. 0008intro a
  9. 0009intro b
  10. 0010intro hU
  11. 0011intro hV
  12. 0012intro hn
  13. 0013intro hN
  14. 0014intro ha
  15. 0015intro hb
  16. 0016have hf : ∃ T. ∃ R. ∃ C. ∃ z. DirichletGrid(F,G,H,n,T) ∧ (ArithRowSums(T,R,0,S n,1,S n,S n) ∧ (ArithRowSums(T,C,0,1,S n,S n,S n) ∧ (SignedPrefixSum(R,S n,z) ∧ SignedPrefixSum(C,S n,z))))
  17. 0017specialize dirichlet_grid_fubini_exists (F)
  18. 0018specialize dirichlet_grid_fubini_exists (G)
  19. 0019specialize dirichlet_grid_fubini_exists (H)
  20. 0020specialize dirichlet_grid_fubini_exists (n)
  21. 0021apply dirichlet_grid_fubini_exists
  22. 0022specialize signed_table_domain_resize (N)
  23. 0023specialize signed_table_domain_resize (0)
  24. 0024specialize signed_table_domain_resize (F)
  25. 0025apply signed_table_domain_resize
  26. 0026cases hV
  27. 0027cases hV_right
  28. 0028cases hV_right_right
  29. 0029exact hV_left
  30. 0030specialize signed_table_domain_resize (N)
  31. 0031specialize signed_table_domain_resize (0)
  32. 0032specialize signed_table_domain_resize (G)
  33. 0033apply signed_table_domain_resize
  34. 0034cases hU
  35. 0035cases hU_right
  36. 0036cases hU_right_right
  37. 0037exact hU_right_left
  38. 0038specialize signed_table_domain_resize (N)
  39. 0039specialize signed_table_domain_resize (0)
  40. 0040specialize signed_table_domain_resize (H)
  41. 0041apply signed_table_domain_resize
  42. 0042cases hU
  43. 0043cases hU_right
  44. 0044cases hU_right_right
  45. 0045exact hU_left
  46. 0046cases hf
  47. 0047cases hf_witness
  48. 0048cases hf_witness_witness
  49. 0049cases hf_witness_witness_witness
  50. 0050cases hf_witness_witness_witness_witness
  51. 0051cases hf_witness_witness_witness_witness_right
  52. 0052cases hf_witness_witness_witness_witness_right_right
  53. 0053cases hf_witness_witness_witness_witness_right_right_right
  54. 0054trans x3
  55. 0055specialize dirichlet_convolution_sum_functional (F)
  56. 0056specialize dirichlet_convolution_sum_functional (U)
  57. 0057specialize dirichlet_convolution_sum_functional (n)
  58. 0058specialize dirichlet_convolution_sum_functional (a)
  59. 0059specialize dirichlet_convolution_sum_functional (x3)
  60. 0060apply dirichlet_convolution_sum_functional
  61. 0061exact ha
  62. 0062split
  63. 0063exact hn
  64. 0064exists x1
  65. 0065split
  66. 0066specialize dirichlet_grid_row_sums_convolution_prefix (N)
  67. 0067specialize dirichlet_grid_row_sums_convolution_prefix (F)
  68. 0068specialize dirichlet_grid_row_sums_convolution_prefix (G)
  69. 0069specialize dirichlet_grid_row_sums_convolution_prefix (H)
  70. 0070specialize dirichlet_grid_row_sums_convolution_prefix (U)
  71. 0071specialize dirichlet_grid_row_sums_convolution_prefix (n)
  72. 0072specialize dirichlet_grid_row_sums_convolution_prefix (x)
  73. 0073specialize dirichlet_grid_row_sums_convolution_prefix (x1)
  74. 0074apply dirichlet_grid_row_sums_convolution_prefix
  75. 0075cases hV
  76. 0076cases hV_right
  77. 0077cases hV_right_right
  78. 0078exact hV_left
  79. 0079exact hU
  80. 0080exact hn
  81. 0081exact hN
  82. 0082exact hf_witness_witness_witness_witness_left
  83. 0083exact hf_witness_witness_witness_witness_right_left
  84. 0084exact hf_witness_witness_witness_witness_right_right_right_left
  85. 0085specialize dirichlet_convolution_sum_functional (H)
  86. 0086specialize dirichlet_convolution_sum_functional (V)
  87. 0087specialize dirichlet_convolution_sum_functional (n)
  88. 0088specialize dirichlet_convolution_sum_functional (x3)
  89. 0089specialize dirichlet_convolution_sum_functional (b)
  90. 0090apply dirichlet_convolution_sum_functional
  91. 0091split
  92. 0092exact hn
  93. 0093exists x2
  94. 0094split
  95. 0095specialize dirichlet_grid_column_sums_convolution_prefix (N)
  96. 0096specialize dirichlet_grid_column_sums_convolution_prefix (F)
  97. 0097specialize dirichlet_grid_column_sums_convolution_prefix (G)
  98. 0098specialize dirichlet_grid_column_sums_convolution_prefix (H)
  99. 0099specialize dirichlet_grid_column_sums_convolution_prefix (V)
  100. 0100specialize dirichlet_grid_column_sums_convolution_prefix (n)
  101. 0101specialize dirichlet_grid_column_sums_convolution_prefix (x)
  102. 0102specialize dirichlet_grid_column_sums_convolution_prefix (x2)
  103. 0103apply dirichlet_grid_column_sums_convolution_prefix
  104. 0104cases hU
  105. 0105cases hU_right
  106. 0106cases hU_right_right
  107. 0107exact hU_left
  108. 0108exact hV
  109. 0109exact hn
  110. 0110exact hN
  111. 0111exact hf_witness_witness_witness_witness_left
  112. 0112exact hf_witness_witness_witness_witness_right_right_left
  113. 0113exact hf_witness_witness_witness_witness_right_right_right_right
  114. 0114exact hb