Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ H. ∀ z. DirichletTable(N,F,G,H) → DirichletSum(F,G,S N,z) → ∃ x. DirichletTable(S N,F,G,x) ∧ ArithTableEqual(H,x,S N)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
arithmetic_signed_table_append · checked external prerequisitesigned_table_domain_resize · checked external prerequisitele_eq_or_lt · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisite
Original expanded first-order statement
forall N F G H z. (((exists dst_positive_code_table_append_previousleft dst_positive_scale_table_append_previousleft dst_negative_code_table_append_previousleft dst_negative_scale_table_append_previousleft. (((F) = (((((dst_positive_code_table_append_previousleft) + (dst_positive_scale_table_append_previousleft)) * S ((dst_positive_code_table_append_previousleft) + (dst_positive_scale_table_append_previousleft)) + ((dst_positive_scale_table_append_previousleft) + (dst_positive_scale_table_append_previousleft))) + (((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) * S ((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) + ((dst_negative_scale_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)))) * S ((((dst_positive_code_table_append_previousleft) + (dst_positive_scale_table_append_previousleft)) * S ((dst_positive_code_table_append_previousleft) + (dst_positive_scale_table_append_previousleft)) + ((dst_positive_scale_table_append_previousleft) + (dst_positive_scale_table_append_previousleft))) + (((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) * S ((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) + ((dst_negative_scale_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)))) + ((((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) * S ((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) + ((dst_negative_scale_table_append_previousleft) + (dst_negative_scale_table_append_previousleft))) + (((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) * S ((dst_negative_code_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)) + ((dst_negative_scale_table_append_previousleft) + (dst_negative_scale_table_append_previousleft)))))) /\ (forall dst_index_table_append_previousleft. (exists pvs_le_gap_table_append_previousleftdomain. pvs_le_gap_table_append_previousleftdomain + (dst_index_table_append_previousleft) = (N)) -> exists dst_positive_table_append_previousleft dst_negative_table_append_previousleft dst_value_table_append_previousleft. ((((exists ff_h_pvs_table_append_previousleftentrypositive. ff_h_pvs_table_append_previousleftentrypositive + S (dst_positive_table_append_previousleft) = S ((S (dst_index_table_append_previousleft)) * dst_positive_scale_table_append_previousleft)) /\ exists ff_q_pvs_table_append_previousleftentrypositive. dst_positive_code_table_append_previousleft = ff_q_pvs_table_append_previousleftentrypositive * S ((S (dst_index_table_append_previousleft)) * dst_positive_scale_table_append_previousleft) + (dst_positive_table_append_previousleft))) /\ (((((exists ff_h_pvs_table_append_previousleftentrynegative. ff_h_pvs_table_append_previousleftentrynegative + S (dst_negative_table_append_previousleft) = S ((S (dst_index_table_append_previousleft)) * dst_negative_scale_table_append_previousleft)) /\ exists ff_q_pvs_table_append_previousleftentrynegative. dst_negative_code_table_append_previousleft = ff_q_pvs_table_append_previousleftentrynegative * S ((S (dst_index_table_append_previousleft)) * dst_negative_scale_table_append_previousleft) + (dst_negative_table_append_previousleft))) /\ (exists ge_balance_positive_table_append_previousleftentryvalue ge_balance_negative_table_append_previousleftentryvalue. (((((dst_value_table_append_previousleft) = 2 * (ge_balance_positive_table_append_previousleftentryvalue) /\ (ge_balance_negative_table_append_previousleftentryvalue) = 0) \/ exists ge_signed_half_table_append_previousleftentryvaluedecode. (((dst_value_table_append_previousleft) = 2 * ge_signed_half_table_append_previousleftentryvaluedecode + 1 /\ (ge_balance_positive_table_append_previousleftentryvalue) = 0) /\ (ge_balance_negative_table_append_previousleftentryvalue) = S ge_signed_half_table_append_previousleftentryvaluedecode))) /\ ((dst_positive_table_append_previousleft) + ge_balance_negative_table_append_previousleftentryvalue = (dst_negative_table_append_previousleft) + ge_balance_positive_table_append_previousleftentryvalue))))))))) /\ (((exists dst_positive_code_table_append_previousright dst_positive_scale_table_append_previousright dst_negative_code_table_append_previousright dst_negative_scale_table_append_previousright. (((G) = (((((dst_positive_code_table_append_previousright) + (dst_positive_scale_table_append_previousright)) * S ((dst_positive_code_table_append_previousright) + (dst_positive_scale_table_append_previousright)) + ((dst_positive_scale_table_append_previousright) + (dst_positive_scale_table_append_previousright))) + (((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) * S ((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) + ((dst_negative_scale_table_append_previousright) + (dst_negative_scale_table_append_previousright)))) * S ((((dst_positive_code_table_append_previousright) + (dst_positive_scale_table_append_previousright)) * S ((dst_positive_code_table_append_previousright) + (dst_positive_scale_table_append_previousright)) + ((dst_positive_scale_table_append_previousright) + (dst_positive_scale_table_append_previousright))) + (((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) * S ((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) + ((dst_negative_scale_table_append_previousright) + (dst_negative_scale_table_append_previousright)))) + ((((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) * S ((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) + ((dst_negative_scale_table_append_previousright) + (dst_negative_scale_table_append_previousright))) + (((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) * S ((dst_negative_code_table_append_previousright) + (dst_negative_scale_table_append_previousright)) + ((dst_negative_scale_table_append_previousright) + (dst_negative_scale_table_append_previousright)))))) /\ (forall dst_index_table_append_previousright. (exists pvs_le_gap_table_append_previousrightdomain. pvs_le_gap_table_append_previousrightdomain + (dst_index_table_append_previousright) = (N)) -> exists dst_positive_table_append_previousright dst_negative_table_append_previousright dst_value_table_append_previousright. ((((exists ff_h_pvs_table_append_previousrightentrypositive. ff_h_pvs_table_append_previousrightentrypositive + S (dst_positive_table_append_previousright) = S ((S (dst_index_table_append_previousright)) * dst_positive_scale_table_append_previousright)) /\ exists ff_q_pvs_table_append_previousrightentrypositive. dst_positive_code_table_append_previousright = ff_q_pvs_table_append_previousrightentrypositive * S ((S (dst_index_table_append_previousright)) * dst_positive_scale_table_append_previousright) + (dst_positive_table_append_previousright))) /\ (((((exists ff_h_pvs_table_append_previousrightentrynegative. ff_h_pvs_table_append_previousrightentrynegative + S (dst_negative_table_append_previousright) = S ((S (dst_index_table_append_previousright)) * dst_negative_scale_table_append_previousright)) /\ exists ff_q_pvs_table_append_previousrightentrynegative. dst_negative_code_table_append_previousright = ff_q_pvs_table_append_previousrightentrynegative * S ((S (dst_index_table_append_previousright)) * dst_negative_scale_table_append_previousright) + (dst_negative_table_append_previousright))) /\ (exists ge_balance_positive_table_append_previousrightentryvalue ge_balance_negative_table_append_previousrightentryvalue. (((((dst_value_table_append_previousright) = 2 * (ge_balance_positive_table_append_previousrightentryvalue) /\ (ge_balance_negative_table_append_previousrightentryvalue) = 0) \/ exists ge_signed_half_table_append_previousrightentryvaluedecode. (((dst_value_table_append_previousright) = 2 * ge_signed_half_table_append_previousrightentryvaluedecode + 1 /\ (ge_balance_positive_table_append_previousrightentryvalue) = 0) /\ (ge_balance_negative_table_append_previousrightentryvalue) = S ge_signed_half_table_append_previousrightentryvaluedecode))) /\ ((dst_positive_table_append_previousright) + ge_balance_negative_table_append_previousrightentryvalue = (dst_negative_table_append_previousright) + ge_balance_positive_table_append_previousrightentryvalue))))))))) /\ (((exists dst_positive_code_table_append_previoustable dst_positive_scale_table_append_previoustable dst_negative_code_table_append_previoustable dst_negative_scale_table_append_previoustable. (((H) = (((((dst_positive_code_table_append_previoustable) + (dst_positive_scale_table_append_previoustable)) * S ((dst_positive_code_table_append_previoustable) + (dst_positive_scale_table_append_previoustable)) + ((dst_positive_scale_table_append_previoustable) + (dst_positive_scale_table_append_previoustable))) + (((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) * S ((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) + ((dst_negative_scale_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)))) * S ((((dst_positive_code_table_append_previoustable) + (dst_positive_scale_table_append_previoustable)) * S ((dst_positive_code_table_append_previoustable) + (dst_positive_scale_table_append_previoustable)) + ((dst_positive_scale_table_append_previoustable) + (dst_positive_scale_table_append_previoustable))) + (((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) * S ((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) + ((dst_negative_scale_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)))) + ((((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) * S ((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) + ((dst_negative_scale_table_append_previoustable) + (dst_negative_scale_table_append_previoustable))) + (((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) * S ((dst_negative_code_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)) + ((dst_negative_scale_table_append_previoustable) + (dst_negative_scale_table_append_previoustable)))))) /\ (forall dst_index_table_append_previoustable. (exists pvs_le_gap_table_append_previoustabledomain. pvs_le_gap_table_append_previoustabledomain + (dst_index_table_append_previoustable) = (N)) -> exists dst_positive_table_append_previoustable dst_negative_table_append_previoustable dst_value_table_append_previoustable. ((((exists ff_h_pvs_table_append_previoustableentrypositive. ff_h_pvs_table_append_previoustableentrypositive + S (dst_positive_table_append_previoustable) = S ((S (dst_index_table_append_previoustable)) * dst_positive_scale_table_append_previoustable)) /\ exists ff_q_pvs_table_append_previoustableentrypositive. dst_positive_code_table_append_previoustable = ff_q_pvs_table_append_previoustableentrypositive * S ((S (dst_index_table_append_previoustable)) * dst_positive_scale_table_append_previoustable) + (dst_positive_table_append_previoustable))) /\ (((((exists ff_h_pvs_table_append_previoustableentrynegative. ff_h_pvs_table_append_previoustableentrynegative + S (dst_negative_table_append_previoustable) = S ((S (dst_index_table_append_previoustable)) * dst_negative_scale_table_append_previoustable)) /\ exists ff_q_pvs_table_append_previoustableentrynegative. dst_negative_code_table_append_previoustable = ff_q_pvs_table_append_previoustableentrynegative * S ((S (dst_index_table_append_previoustable)) * dst_negative_scale_table_append_previoustable) + (dst_negative_table_append_previoustable))) /\ (exists ge_balance_positive_table_append_previoustableentryvalue ge_balance_negative_table_append_previoustableentryvalue. (((((dst_value_table_append_previoustable) = 2 * (ge_balance_positive_table_append_previoustableentryvalue) /\ (ge_balance_negative_table_append_previoustableentryvalue) = 0) \/ exists ge_signed_half_table_append_previoustableentryvaluedecode. (((dst_value_table_append_previoustable) = 2 * ge_signed_half_table_append_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_table_append_previoustableentryvalue) = 0) /\ (ge_balance_negative_table_append_previoustableentryvalue) = S ge_signed_half_table_append_previoustableentryvaluedecode))) /\ ((dst_positive_table_append_previoustable) + ge_balance_negative_table_append_previoustableentryvalue = (dst_negative_table_append_previoustable) + ge_balance_positive_table_append_previoustableentryvalue))))))))) /\ (forall dc_input_table_append_previous dc_output_table_append_previous. ~(dc_input_table_append_previous=0) -> (exists pvs_le_gap_table_append_previousdomain. pvs_le_gap_table_append_previousdomain + (dc_input_table_append_previous) = (N)) -> (exists dst_positive_code_table_append_previouslookup dst_positive_scale_table_append_previouslookup dst_negative_code_table_append_previouslookup dst_negative_scale_table_append_previouslookup dst_positive_table_append_previouslookup dst_negative_table_append_previouslookup. (((H) = (((((dst_positive_code_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup)) * S ((dst_positive_code_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup)) + ((dst_positive_scale_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup))) + (((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) * S ((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) + ((dst_negative_scale_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)))) * S ((((dst_positive_code_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup)) * S ((dst_positive_code_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup)) + ((dst_positive_scale_table_append_previouslookup) + (dst_positive_scale_table_append_previouslookup))) + (((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) * S ((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) + ((dst_negative_scale_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)))) + ((((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) * S ((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) + ((dst_negative_scale_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup))) + (((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) * S ((dst_negative_code_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)) + ((dst_negative_scale_table_append_previouslookup) + (dst_negative_scale_table_append_previouslookup)))))) /\ (((((exists ff_h_pvs_table_append_previouslookuppositive. ff_h_pvs_table_append_previouslookuppositive + S (dst_positive_table_append_previouslookup) = S ((S (dc_input_table_append_previous)) * dst_positive_scale_table_append_previouslookup)) /\ exists ff_q_pvs_table_append_previouslookuppositive. dst_positive_code_table_append_previouslookup = ff_q_pvs_table_append_previouslookuppositive * S ((S (dc_input_table_append_previous)) * dst_positive_scale_table_append_previouslookup) + (dst_positive_table_append_previouslookup))) /\ (((((exists ff_h_pvs_table_append_previouslookupnegative. ff_h_pvs_table_append_previouslookupnegative + S (dst_negative_table_append_previouslookup) = S ((S (dc_input_table_append_previous)) * dst_negative_scale_table_append_previouslookup)) /\ exists ff_q_pvs_table_append_previouslookupnegative. dst_negative_code_table_append_previouslookup = ff_q_pvs_table_append_previouslookupnegative * S ((S (dc_input_table_append_previous)) * dst_negative_scale_table_append_previouslookup) + (dst_negative_table_append_previouslookup))) /\ (exists ge_balance_positive_table_append_previouslookupvalue ge_balance_negative_table_append_previouslookupvalue. (((((dc_output_table_append_previous) = 2 * (ge_balance_positive_table_append_previouslookupvalue) /\ (ge_balance_negative_table_append_previouslookupvalue) = 0) \/ exists ge_signed_half_table_append_previouslookupvaluedecode. (((dc_output_table_append_previous) = 2 * ge_signed_half_table_append_previouslookupvaluedecode + 1 /\ (ge_balance_positive_table_append_previouslookupvalue) = 0) /\ (ge_balance_negative_table_append_previouslookupvalue) = S ge_signed_half_table_append_previouslookupvaluedecode))) /\ ((dst_positive_table_append_previouslookup) + ge_balance_negative_table_append_previouslookupvalue = (dst_negative_table_append_previouslookup) + ge_balance_positive_table_append_previouslookupvalue))))))))) -> (((~((dc_input_table_append_previous)=0)) /\ (exists dc_mask_table_append_previousvalue. ((((exists dst_positive_code_table_append_previousvaluemasktable dst_positive_scale_table_append_previousvaluemasktable dst_negative_code_table_append_previousvaluemasktable dst_negative_scale_table_append_previousvaluemasktable. (((dc_mask_table_append_previousvalue) = (((((dst_positive_code_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable)) * S ((dst_positive_code_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable)) + ((dst_positive_scale_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable))) + (((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) * S ((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) + ((dst_negative_scale_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)))) * S ((((dst_positive_code_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable)) * S ((dst_positive_code_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable)) + ((dst_positive_scale_table_append_previousvaluemasktable) + (dst_positive_scale_table_append_previousvaluemasktable))) + (((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) * S ((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) + ((dst_negative_scale_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)))) + ((((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) * S ((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) + ((dst_negative_scale_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable))) + (((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) * S ((dst_negative_code_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)) + ((dst_negative_scale_table_append_previousvaluemasktable) + (dst_negative_scale_table_append_previousvaluemasktable)))))) /\ (forall dst_index_table_append_previousvaluemasktable. (exists pvs_le_gap_table_append_previousvaluemasktabledomain. pvs_le_gap_table_append_previousvaluemasktabledomain + (dst_index_table_append_previousvaluemasktable) = (dc_input_table_append_previous)) -> exists dst_positive_table_append_previousvaluemasktable dst_negative_table_append_previousvaluemasktable dst_value_table_append_previousvaluemasktable. ((((exists ff_h_pvs_table_append_previousvaluemasktableentrypositive. ff_h_pvs_table_append_previousvaluemasktableentrypositive + S (dst_positive_table_append_previousvaluemasktable) = S ((S (dst_index_table_append_previousvaluemasktable)) * dst_positive_scale_table_append_previousvaluemasktable)) /\ exists ff_q_pvs_table_append_previousvaluemasktableentrypositive. dst_positive_code_table_append_previousvaluemasktable = ff_q_pvs_table_append_previousvaluemasktableentrypositive * S ((S (dst_index_table_append_previousvaluemasktable)) * dst_positive_scale_table_append_previousvaluemasktable) + (dst_positive_table_append_previousvaluemasktable))) /\ (((((exists ff_h_pvs_table_append_previousvaluemasktableentrynegative. ff_h_pvs_table_append_previousvaluemasktableentrynegative + S (dst_negative_table_append_previousvaluemasktable) = S ((S (dst_index_table_append_previousvaluemasktable)) * dst_negative_scale_table_append_previousvaluemasktable)) /\ exists ff_q_pvs_table_append_previousvaluemasktableentrynegative. dst_negative_code_table_append_previousvaluemasktable = ff_q_pvs_table_append_previousvaluemasktableentrynegative * S ((S (dst_index_table_append_previousvaluemasktable)) * dst_negative_scale_table_append_previousvaluemasktable) + (dst_negative_table_append_previousvaluemasktable))) /\ (exists ge_balance_positive_table_append_previousvaluemasktableentryvalue ge_balance_negative_table_append_previousvaluemasktableentryvalue. (((((dst_value_table_append_previousvaluemasktable) = 2 * (ge_balance_positive_table_append_previousvaluemasktableentryvalue) /\ (ge_balance_negative_table_append_previousvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_append_previousvaluemasktableentryvaluedecode. (((dst_value_table_append_previousvaluemasktable) = 2 * ge_signed_half_table_append_previousvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_append_previousvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_append_previousvaluemasktableentryvalue) = S ge_signed_half_table_append_previousvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_append_previousvaluemasktable) + ge_balance_negative_table_append_previousvaluemasktableentryvalue = (dst_negative_table_append_previousvaluemasktable) + ge_balance_positive_table_append_previousvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_append_previousvaluemask dc_value_table_append_previousvaluemask. (exists pvs_le_gap_table_append_previousvaluemaskdomain. pvs_le_gap_table_append_previousvaluemaskdomain + (dc_index_table_append_previousvaluemask) = (dc_input_table_append_previous)) -> (exists dst_positive_code_table_append_previousvaluemasklookup dst_positive_scale_table_append_previousvaluemasklookup dst_negative_code_table_append_previousvaluemasklookup dst_negative_scale_table_append_previousvaluemasklookup dst_positive_table_append_previousvaluemasklookup dst_negative_table_append_previousvaluemasklookup. (((dc_mask_table_append_previousvalue) = (((((dst_positive_code_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup)) * S ((dst_positive_code_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup)) + ((dst_positive_scale_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup))) + (((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) * S ((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) + ((dst_negative_scale_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)))) * S ((((dst_positive_code_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup)) * S ((dst_positive_code_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup)) + ((dst_positive_scale_table_append_previousvaluemasklookup) + (dst_positive_scale_table_append_previousvaluemasklookup))) + (((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) * S ((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) + ((dst_negative_scale_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)))) + ((((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) * S ((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) + ((dst_negative_scale_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup))) + (((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) * S ((dst_negative_code_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)) + ((dst_negative_scale_table_append_previousvaluemasklookup) + (dst_negative_scale_table_append_previousvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_append_previousvaluemasklookuppositive. ff_h_pvs_table_append_previousvaluemasklookuppositive + S (dst_positive_table_append_previousvaluemasklookup) = S ((S (dc_index_table_append_previousvaluemask)) * dst_positive_scale_table_append_previousvaluemasklookup)) /\ exists ff_q_pvs_table_append_previousvaluemasklookuppositive. dst_positive_code_table_append_previousvaluemasklookup = ff_q_pvs_table_append_previousvaluemasklookuppositive * S ((S (dc_index_table_append_previousvaluemask)) * dst_positive_scale_table_append_previousvaluemasklookup) + (dst_positive_table_append_previousvaluemasklookup))) /\ (((((exists ff_h_pvs_table_append_previousvaluemasklookupnegative. ff_h_pvs_table_append_previousvaluemasklookupnegative + S (dst_negative_table_append_previousvaluemasklookup) = S ((S (dc_index_table_append_previousvaluemask)) * dst_negative_scale_table_append_previousvaluemasklookup)) /\ exists ff_q_pvs_table_append_previousvaluemasklookupnegative. dst_negative_code_table_append_previousvaluemasklookup = ff_q_pvs_table_append_previousvaluemasklookupnegative * S ((S (dc_index_table_append_previousvaluemask)) * dst_negative_scale_table_append_previousvaluemasklookup) + (dst_negative_table_append_previousvaluemasklookup))) /\ (exists ge_balance_positive_table_append_previousvaluemasklookupvalue ge_balance_negative_table_append_previousvaluemasklookupvalue. (((((dc_value_table_append_previousvaluemask) = 2 * (ge_balance_positive_table_append_previousvaluemasklookupvalue) /\ (ge_balance_negative_table_append_previousvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_append_previousvaluemasklookupvaluedecode. (((dc_value_table_append_previousvaluemask) = 2 * ge_signed_half_table_append_previousvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_append_previousvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_append_previousvaluemasklookupvalue) = S ge_signed_half_table_append_previousvaluemasklookupvaluedecode))) /\ ((dst_positive_table_append_previousvaluemasklookup) + ge_balance_negative_table_append_previousvaluemasklookupvalue = (dst_negative_table_append_previousvaluemasklookup) + ge_balance_positive_table_append_previousvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_append_previousvaluemask)=0)) /\ (exists dc_quotient_table_append_previousvaluemaskentry dc_left_table_append_previousvaluemaskentry dc_right_table_append_previousvaluemaskentry. (((dc_input_table_append_previous)=(dc_index_table_append_previousvaluemask)*dc_quotient_table_append_previousvaluemaskentry) /\ (((exists dst_positive_code_table_append_previousvaluemaskentryleft dst_positive_scale_table_append_previousvaluemaskentryleft dst_negative_code_table_append_previousvaluemaskentryleft dst_negative_scale_table_append_previousvaluemaskentryleft dst_positive_table_append_previousvaluemaskentryleft dst_negative_table_append_previousvaluemaskentryleft. (((F) = (((((dst_positive_code_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft)) * S ((dst_positive_code_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft)) + ((dst_positive_scale_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft))) + (((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) * S ((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) + ((dst_negative_scale_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)))) * S ((((dst_positive_code_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft)) * S ((dst_positive_code_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft)) + ((dst_positive_scale_table_append_previousvaluemaskentryleft) + (dst_positive_scale_table_append_previousvaluemaskentryleft))) + (((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) * S ((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) + ((dst_negative_scale_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)))) + ((((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) * S ((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) + ((dst_negative_scale_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft))) + (((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) * S ((dst_negative_code_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)) + ((dst_negative_scale_table_append_previousvaluemaskentryleft) + (dst_negative_scale_table_append_previousvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_append_previousvaluemaskentryleftpositive. ff_h_pvs_table_append_previousvaluemaskentryleftpositive + S (dst_positive_table_append_previousvaluemaskentryleft) = S ((S (dc_index_table_append_previousvaluemask)) * dst_positive_scale_table_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_table_append_previousvaluemaskentryleftpositive. dst_positive_code_table_append_previousvaluemaskentryleft = ff_q_pvs_table_append_previousvaluemaskentryleftpositive * S ((S (dc_index_table_append_previousvaluemask)) * dst_positive_scale_table_append_previousvaluemaskentryleft) + (dst_positive_table_append_previousvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_append_previousvaluemaskentryleftnegative. ff_h_pvs_table_append_previousvaluemaskentryleftnegative + S (dst_negative_table_append_previousvaluemaskentryleft) = S ((S (dc_index_table_append_previousvaluemask)) * dst_negative_scale_table_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_table_append_previousvaluemaskentryleftnegative. dst_negative_code_table_append_previousvaluemaskentryleft = ff_q_pvs_table_append_previousvaluemaskentryleftnegative * S ((S (dc_index_table_append_previousvaluemask)) * dst_negative_scale_table_append_previousvaluemaskentryleft) + (dst_negative_table_append_previousvaluemaskentryleft))) /\ (exists ge_balance_positive_table_append_previousvaluemaskentryleftvalue ge_balance_negative_table_append_previousvaluemaskentryleftvalue. (((((dc_left_table_append_previousvaluemaskentry) = 2 * (ge_balance_positive_table_append_previousvaluemaskentryleftvalue) /\ (ge_balance_negative_table_append_previousvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_append_previousvaluemaskentryleftvaluedecode. (((dc_left_table_append_previousvaluemaskentry) = 2 * ge_signed_half_table_append_previousvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_append_previousvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_append_previousvaluemaskentryleftvalue) = S ge_signed_half_table_append_previousvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_append_previousvaluemaskentryleft) + ge_balance_negative_table_append_previousvaluemaskentryleftvalue = (dst_negative_table_append_previousvaluemaskentryleft) + ge_balance_positive_table_append_previousvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_append_previousvaluemaskentryright dst_positive_scale_table_append_previousvaluemaskentryright dst_negative_code_table_append_previousvaluemaskentryright dst_negative_scale_table_append_previousvaluemaskentryright dst_positive_table_append_previousvaluemaskentryright dst_negative_table_append_previousvaluemaskentryright. (((G) = (((((dst_positive_code_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright)) * S ((dst_positive_code_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright)) + ((dst_positive_scale_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright))) + (((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) * S ((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) + ((dst_negative_scale_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)))) * S ((((dst_positive_code_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright)) * S ((dst_positive_code_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright)) + ((dst_positive_scale_table_append_previousvaluemaskentryright) + (dst_positive_scale_table_append_previousvaluemaskentryright))) + (((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) * S ((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) + ((dst_negative_scale_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)))) + ((((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) * S ((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) + ((dst_negative_scale_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright))) + (((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) * S ((dst_negative_code_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)) + ((dst_negative_scale_table_append_previousvaluemaskentryright) + (dst_negative_scale_table_append_previousvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_append_previousvaluemaskentryrightpositive. ff_h_pvs_table_append_previousvaluemaskentryrightpositive + S (dst_positive_table_append_previousvaluemaskentryright) = S ((S (dc_quotient_table_append_previousvaluemaskentry)) * dst_positive_scale_table_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_table_append_previousvaluemaskentryrightpositive. dst_positive_code_table_append_previousvaluemaskentryright = ff_q_pvs_table_append_previousvaluemaskentryrightpositive * S ((S (dc_quotient_table_append_previousvaluemaskentry)) * dst_positive_scale_table_append_previousvaluemaskentryright) + (dst_positive_table_append_previousvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_append_previousvaluemaskentryrightnegative. ff_h_pvs_table_append_previousvaluemaskentryrightnegative + S (dst_negative_table_append_previousvaluemaskentryright) = S ((S (dc_quotient_table_append_previousvaluemaskentry)) * dst_negative_scale_table_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_table_append_previousvaluemaskentryrightnegative. dst_negative_code_table_append_previousvaluemaskentryright = ff_q_pvs_table_append_previousvaluemaskentryrightnegative * S ((S (dc_quotient_table_append_previousvaluemaskentry)) * dst_negative_scale_table_append_previousvaluemaskentryright) + (dst_negative_table_append_previousvaluemaskentryright))) /\ (exists ge_balance_positive_table_append_previousvaluemaskentryrightvalue ge_balance_negative_table_append_previousvaluemaskentryrightvalue. (((((dc_right_table_append_previousvaluemaskentry) = 2 * (ge_balance_positive_table_append_previousvaluemaskentryrightvalue) /\ (ge_balance_negative_table_append_previousvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_append_previousvaluemaskentryrightvaluedecode. (((dc_right_table_append_previousvaluemaskentry) = 2 * ge_signed_half_table_append_previousvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_append_previousvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_append_previousvaluemaskentryrightvalue) = S ge_signed_half_table_append_previousvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_append_previousvaluemaskentryright) + ge_balance_negative_table_append_previousvaluemaskentryrightvalue = (dst_negative_table_append_previousvaluemaskentryright) + ge_balance_positive_table_append_previousvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_append_previousvaluemaskentryproduct sto_an_table_append_previousvaluemaskentryproduct sto_bp_table_append_previousvaluemaskentryproduct sto_bn_table_append_previousvaluemaskentryproduct sto_cp_table_append_previousvaluemaskentryproduct sto_cn_table_append_previousvaluemaskentryproduct. (((((dc_left_table_append_previousvaluemaskentry) = 2 * (sto_ap_table_append_previousvaluemaskentryproduct) /\ (sto_an_table_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_previousvaluemaskentryproductleft. (((dc_left_table_append_previousvaluemaskentry) = 2 * ge_signed_half_table_append_previousvaluemaskentryproductleft + 1 /\ (sto_ap_table_append_previousvaluemaskentryproduct) = 0) /\ (sto_an_table_append_previousvaluemaskentryproduct) = S ge_signed_half_table_append_previousvaluemaskentryproductleft))) /\ ((((((dc_right_table_append_previousvaluemaskentry) = 2 * (sto_bp_table_append_previousvaluemaskentryproduct) /\ (sto_bn_table_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_previousvaluemaskentryproductright. (((dc_right_table_append_previousvaluemaskentry) = 2 * ge_signed_half_table_append_previousvaluemaskentryproductright + 1 /\ (sto_bp_table_append_previousvaluemaskentryproduct) = 0) /\ (sto_bn_table_append_previousvaluemaskentryproduct) = S ge_signed_half_table_append_previousvaluemaskentryproductright))) /\ ((((((dc_value_table_append_previousvaluemask) = 2 * (sto_cp_table_append_previousvaluemaskentryproduct) /\ (sto_cn_table_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_previousvaluemaskentryproductoutput. (((dc_value_table_append_previousvaluemask) = 2 * ge_signed_half_table_append_previousvaluemaskentryproductoutput + 1 /\ (sto_cp_table_append_previousvaluemaskentryproduct) = 0) /\ (sto_cn_table_append_previousvaluemaskentryproduct) = S ge_signed_half_table_append_previousvaluemaskentryproductoutput))) /\ ((sto_ap_table_append_previousvaluemaskentryproduct * sto_bp_table_append_previousvaluemaskentryproduct + sto_an_table_append_previousvaluemaskentryproduct * sto_bn_table_append_previousvaluemaskentryproduct) + sto_cn_table_append_previousvaluemaskentryproduct = (sto_ap_table_append_previousvaluemaskentryproduct * sto_bn_table_append_previousvaluemaskentryproduct + sto_an_table_append_previousvaluemaskentryproduct * sto_bp_table_append_previousvaluemaskentryproduct) + sto_cp_table_append_previousvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_append_previousvaluemask)=0 \/ ~(exists pvs_factor_table_append_previousvaluemaskentrynondivisor. (dc_input_table_append_previous) = (dc_index_table_append_previousvaluemask) * pvs_factor_table_append_previousvaluemaskentrynondivisor)) /\ ((dc_value_table_append_previousvaluemask)=0))))))) /\ (exists dst_positive_code_table_append_previousvaluefold dst_positive_scale_table_append_previousvaluefold dst_negative_code_table_append_previousvaluefold dst_negative_scale_table_append_previousvaluefold dst_positive_sum_table_append_previousvaluefold dst_negative_sum_table_append_previousvaluefold. (((dc_mask_table_append_previousvalue) = (((((dst_positive_code_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold)) * S ((dst_positive_code_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold)) + ((dst_positive_scale_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold))) + (((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) * S ((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) + ((dst_negative_scale_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)))) * S ((((dst_positive_code_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold)) * S ((dst_positive_code_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold)) + ((dst_positive_scale_table_append_previousvaluefold) + (dst_positive_scale_table_append_previousvaluefold))) + (((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) * S ((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) + ((dst_negative_scale_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)))) + ((((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) * S ((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) + ((dst_negative_scale_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold))) + (((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) * S ((dst_negative_code_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)) + ((dst_negative_scale_table_append_previousvaluefold) + (dst_negative_scale_table_append_previousvaluefold)))))) /\ (((exists fs_u_dst_table_append_previousvaluefoldpositive fs_v_dst_table_append_previousvaluefoldpositive. ((((exists fs_h_dst_table_append_previousvaluefoldpositive_body_start. fs_h_dst_table_append_previousvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_previousvaluefoldpositive)) /\ exists fs_q_dst_table_append_previousvaluefoldpositive_body_start. fs_u_dst_table_append_previousvaluefoldpositive = fs_q_dst_table_append_previousvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_append_previousvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldpositive_body_terminal. fs_h_dst_table_append_previousvaluefoldpositive_body_terminal + S (dst_positive_sum_table_append_previousvaluefold) = S ((S (S (dc_input_table_append_previous))) * fs_v_dst_table_append_previousvaluefoldpositive)) /\ exists fs_q_dst_table_append_previousvaluefoldpositive_body_terminal. fs_u_dst_table_append_previousvaluefoldpositive = fs_q_dst_table_append_previousvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_append_previous))) * fs_v_dst_table_append_previousvaluefoldpositive) + (dst_positive_sum_table_append_previousvaluefold))) /\ forall fs_i_dst_table_append_previousvaluefoldpositive_body_steps. (exists fs_lt_dst_table_append_previousvaluefoldpositive_body_steps_bound. fs_lt_dst_table_append_previousvaluefoldpositive_body_steps_bound + S fs_i_dst_table_append_previousvaluefoldpositive_body_steps = S (dc_input_table_append_previous)) -> exists fs_a_dst_table_append_previousvaluefoldpositive_body_steps fs_r_dst_table_append_previousvaluefoldpositive_body_steps fs_s_dst_table_append_previousvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_append_previousvaluefoldpositive_body_steps_summand. fs_h_dst_table_append_previousvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_table_append_previousvaluefold)) /\ exists fs_q_dst_table_append_previousvaluefoldpositive_body_steps_summand. dst_positive_code_table_append_previousvaluefold = fs_q_dst_table_append_previousvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_table_append_previousvaluefold) + (fs_a_dst_table_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldpositive_body_steps_partial. fs_h_dst_table_append_previousvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_table_append_previousvaluefoldpositive)) /\ exists fs_q_dst_table_append_previousvaluefoldpositive_body_steps_partial. fs_u_dst_table_append_previousvaluefoldpositive = fs_q_dst_table_append_previousvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_table_append_previousvaluefoldpositive) + (fs_r_dst_table_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldpositive_body_steps_successor. fs_h_dst_table_append_previousvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_append_previousvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_table_append_previousvaluefoldpositive)) /\ exists fs_q_dst_table_append_previousvaluefoldpositive_body_steps_successor. fs_u_dst_table_append_previousvaluefoldpositive = fs_q_dst_table_append_previousvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_table_append_previousvaluefoldpositive) + (fs_s_dst_table_append_previousvaluefoldpositive_body_steps))) /\ fs_s_dst_table_append_previousvaluefoldpositive_body_steps = fs_r_dst_table_append_previousvaluefoldpositive_body_steps + fs_a_dst_table_append_previousvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_append_previousvaluefoldnegative fs_v_dst_table_append_previousvaluefoldnegative. ((((exists fs_h_dst_table_append_previousvaluefoldnegative_body_start. fs_h_dst_table_append_previousvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_previousvaluefoldnegative)) /\ exists fs_q_dst_table_append_previousvaluefoldnegative_body_start. fs_u_dst_table_append_previousvaluefoldnegative = fs_q_dst_table_append_previousvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_append_previousvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldnegative_body_terminal. fs_h_dst_table_append_previousvaluefoldnegative_body_terminal + S (dst_negative_sum_table_append_previousvaluefold) = S ((S (S (dc_input_table_append_previous))) * fs_v_dst_table_append_previousvaluefoldnegative)) /\ exists fs_q_dst_table_append_previousvaluefoldnegative_body_terminal. fs_u_dst_table_append_previousvaluefoldnegative = fs_q_dst_table_append_previousvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_append_previous))) * fs_v_dst_table_append_previousvaluefoldnegative) + (dst_negative_sum_table_append_previousvaluefold))) /\ forall fs_i_dst_table_append_previousvaluefoldnegative_body_steps. (exists fs_lt_dst_table_append_previousvaluefoldnegative_body_steps_bound. fs_lt_dst_table_append_previousvaluefoldnegative_body_steps_bound + S fs_i_dst_table_append_previousvaluefoldnegative_body_steps = S (dc_input_table_append_previous)) -> exists fs_a_dst_table_append_previousvaluefoldnegative_body_steps fs_r_dst_table_append_previousvaluefoldnegative_body_steps fs_s_dst_table_append_previousvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_append_previousvaluefoldnegative_body_steps_summand. fs_h_dst_table_append_previousvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_table_append_previousvaluefold)) /\ exists fs_q_dst_table_append_previousvaluefoldnegative_body_steps_summand. dst_negative_code_table_append_previousvaluefold = fs_q_dst_table_append_previousvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_table_append_previousvaluefold) + (fs_a_dst_table_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldnegative_body_steps_partial. fs_h_dst_table_append_previousvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_table_append_previousvaluefoldnegative)) /\ exists fs_q_dst_table_append_previousvaluefoldnegative_body_steps_partial. fs_u_dst_table_append_previousvaluefoldnegative = fs_q_dst_table_append_previousvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_table_append_previousvaluefoldnegative) + (fs_r_dst_table_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_previousvaluefoldnegative_body_steps_successor. fs_h_dst_table_append_previousvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_append_previousvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_table_append_previousvaluefoldnegative)) /\ exists fs_q_dst_table_append_previousvaluefoldnegative_body_steps_successor. fs_u_dst_table_append_previousvaluefoldnegative = fs_q_dst_table_append_previousvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_table_append_previousvaluefoldnegative) + (fs_s_dst_table_append_previousvaluefoldnegative_body_steps))) /\ fs_s_dst_table_append_previousvaluefoldnegative_body_steps = fs_r_dst_table_append_previousvaluefoldnegative_body_steps + fs_a_dst_table_append_previousvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_append_previousvaluefoldresult ge_balance_negative_table_append_previousvaluefoldresult. (((((dc_output_table_append_previous) = 2 * (ge_balance_positive_table_append_previousvaluefoldresult) /\ (ge_balance_negative_table_append_previousvaluefoldresult) = 0) \/ exists ge_signed_half_table_append_previousvaluefoldresultdecode. (((dc_output_table_append_previous) = 2 * ge_signed_half_table_append_previousvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_append_previousvaluefoldresult) = 0) /\ (ge_balance_negative_table_append_previousvaluefoldresult) = S ge_signed_half_table_append_previousvaluefoldresultdecode))) /\ ((dst_positive_sum_table_append_previousvaluefold) + ge_balance_negative_table_append_previousvaluefoldresult = (dst_negative_sum_table_append_previousvaluefold) + ge_balance_positive_table_append_previousvaluefoldresult)))))))))))))))))))) -> (((~((S N)=0)) /\ (exists dc_mask_table_append_value. ((((exists dst_positive_code_table_append_valuemasktable dst_positive_scale_table_append_valuemasktable dst_negative_code_table_append_valuemasktable dst_negative_scale_table_append_valuemasktable. (((dc_mask_table_append_value) = (((((dst_positive_code_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable)) * S ((dst_positive_code_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable)) + ((dst_positive_scale_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable))) + (((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) * S ((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) + ((dst_negative_scale_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)))) * S ((((dst_positive_code_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable)) * S ((dst_positive_code_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable)) + ((dst_positive_scale_table_append_valuemasktable) + (dst_positive_scale_table_append_valuemasktable))) + (((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) * S ((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) + ((dst_negative_scale_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)))) + ((((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) * S ((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) + ((dst_negative_scale_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable))) + (((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) * S ((dst_negative_code_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)) + ((dst_negative_scale_table_append_valuemasktable) + (dst_negative_scale_table_append_valuemasktable)))))) /\ (forall dst_index_table_append_valuemasktable. (exists pvs_le_gap_table_append_valuemasktabledomain. pvs_le_gap_table_append_valuemasktabledomain + (dst_index_table_append_valuemasktable) = (S N)) -> exists dst_positive_table_append_valuemasktable dst_negative_table_append_valuemasktable dst_value_table_append_valuemasktable. ((((exists ff_h_pvs_table_append_valuemasktableentrypositive. ff_h_pvs_table_append_valuemasktableentrypositive + S (dst_positive_table_append_valuemasktable) = S ((S (dst_index_table_append_valuemasktable)) * dst_positive_scale_table_append_valuemasktable)) /\ exists ff_q_pvs_table_append_valuemasktableentrypositive. dst_positive_code_table_append_valuemasktable = ff_q_pvs_table_append_valuemasktableentrypositive * S ((S (dst_index_table_append_valuemasktable)) * dst_positive_scale_table_append_valuemasktable) + (dst_positive_table_append_valuemasktable))) /\ (((((exists ff_h_pvs_table_append_valuemasktableentrynegative. ff_h_pvs_table_append_valuemasktableentrynegative + S (dst_negative_table_append_valuemasktable) = S ((S (dst_index_table_append_valuemasktable)) * dst_negative_scale_table_append_valuemasktable)) /\ exists ff_q_pvs_table_append_valuemasktableentrynegative. dst_negative_code_table_append_valuemasktable = ff_q_pvs_table_append_valuemasktableentrynegative * S ((S (dst_index_table_append_valuemasktable)) * dst_negative_scale_table_append_valuemasktable) + (dst_negative_table_append_valuemasktable))) /\ (exists ge_balance_positive_table_append_valuemasktableentryvalue ge_balance_negative_table_append_valuemasktableentryvalue. (((((dst_value_table_append_valuemasktable) = 2 * (ge_balance_positive_table_append_valuemasktableentryvalue) /\ (ge_balance_negative_table_append_valuemasktableentryvalue) = 0) \/ exists ge_signed_half_table_append_valuemasktableentryvaluedecode. (((dst_value_table_append_valuemasktable) = 2 * ge_signed_half_table_append_valuemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_append_valuemasktableentryvalue) = 0) /\ (ge_balance_negative_table_append_valuemasktableentryvalue) = S ge_signed_half_table_append_valuemasktableentryvaluedecode))) /\ ((dst_positive_table_append_valuemasktable) + ge_balance_negative_table_append_valuemasktableentryvalue = (dst_negative_table_append_valuemasktable) + ge_balance_positive_table_append_valuemasktableentryvalue))))))))) /\ (forall dc_index_table_append_valuemask dc_value_table_append_valuemask. (exists pvs_le_gap_table_append_valuemaskdomain. pvs_le_gap_table_append_valuemaskdomain + (dc_index_table_append_valuemask) = (S N)) -> (exists dst_positive_code_table_append_valuemasklookup dst_positive_scale_table_append_valuemasklookup dst_negative_code_table_append_valuemasklookup dst_negative_scale_table_append_valuemasklookup dst_positive_table_append_valuemasklookup dst_negative_table_append_valuemasklookup. (((dc_mask_table_append_value) = (((((dst_positive_code_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup)) * S ((dst_positive_code_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup)) + ((dst_positive_scale_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup))) + (((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) * S ((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) + ((dst_negative_scale_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)))) * S ((((dst_positive_code_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup)) * S ((dst_positive_code_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup)) + ((dst_positive_scale_table_append_valuemasklookup) + (dst_positive_scale_table_append_valuemasklookup))) + (((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) * S ((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) + ((dst_negative_scale_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)))) + ((((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) * S ((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) + ((dst_negative_scale_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup))) + (((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) * S ((dst_negative_code_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)) + ((dst_negative_scale_table_append_valuemasklookup) + (dst_negative_scale_table_append_valuemasklookup)))))) /\ (((((exists ff_h_pvs_table_append_valuemasklookuppositive. ff_h_pvs_table_append_valuemasklookuppositive + S (dst_positive_table_append_valuemasklookup) = S ((S (dc_index_table_append_valuemask)) * dst_positive_scale_table_append_valuemasklookup)) /\ exists ff_q_pvs_table_append_valuemasklookuppositive. dst_positive_code_table_append_valuemasklookup = ff_q_pvs_table_append_valuemasklookuppositive * S ((S (dc_index_table_append_valuemask)) * dst_positive_scale_table_append_valuemasklookup) + (dst_positive_table_append_valuemasklookup))) /\ (((((exists ff_h_pvs_table_append_valuemasklookupnegative. ff_h_pvs_table_append_valuemasklookupnegative + S (dst_negative_table_append_valuemasklookup) = S ((S (dc_index_table_append_valuemask)) * dst_negative_scale_table_append_valuemasklookup)) /\ exists ff_q_pvs_table_append_valuemasklookupnegative. dst_negative_code_table_append_valuemasklookup = ff_q_pvs_table_append_valuemasklookupnegative * S ((S (dc_index_table_append_valuemask)) * dst_negative_scale_table_append_valuemasklookup) + (dst_negative_table_append_valuemasklookup))) /\ (exists ge_balance_positive_table_append_valuemasklookupvalue ge_balance_negative_table_append_valuemasklookupvalue. (((((dc_value_table_append_valuemask) = 2 * (ge_balance_positive_table_append_valuemasklookupvalue) /\ (ge_balance_negative_table_append_valuemasklookupvalue) = 0) \/ exists ge_signed_half_table_append_valuemasklookupvaluedecode. (((dc_value_table_append_valuemask) = 2 * ge_signed_half_table_append_valuemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_append_valuemasklookupvalue) = 0) /\ (ge_balance_negative_table_append_valuemasklookupvalue) = S ge_signed_half_table_append_valuemasklookupvaluedecode))) /\ ((dst_positive_table_append_valuemasklookup) + ge_balance_negative_table_append_valuemasklookupvalue = (dst_negative_table_append_valuemasklookup) + ge_balance_positive_table_append_valuemasklookupvalue))))))))) -> ((((~((dc_index_table_append_valuemask)=0)) /\ (exists dc_quotient_table_append_valuemaskentry dc_left_table_append_valuemaskentry dc_right_table_append_valuemaskentry. (((S N)=(dc_index_table_append_valuemask)*dc_quotient_table_append_valuemaskentry) /\ (((exists dst_positive_code_table_append_valuemaskentryleft dst_positive_scale_table_append_valuemaskentryleft dst_negative_code_table_append_valuemaskentryleft dst_negative_scale_table_append_valuemaskentryleft dst_positive_table_append_valuemaskentryleft dst_negative_table_append_valuemaskentryleft. (((F) = (((((dst_positive_code_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft)) * S ((dst_positive_code_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft)) + ((dst_positive_scale_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft))) + (((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) * S ((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) + ((dst_negative_scale_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)))) * S ((((dst_positive_code_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft)) * S ((dst_positive_code_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft)) + ((dst_positive_scale_table_append_valuemaskentryleft) + (dst_positive_scale_table_append_valuemaskentryleft))) + (((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) * S ((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) + ((dst_negative_scale_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)))) + ((((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) * S ((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) + ((dst_negative_scale_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft))) + (((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) * S ((dst_negative_code_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)) + ((dst_negative_scale_table_append_valuemaskentryleft) + (dst_negative_scale_table_append_valuemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_append_valuemaskentryleftpositive. ff_h_pvs_table_append_valuemaskentryleftpositive + S (dst_positive_table_append_valuemaskentryleft) = S ((S (dc_index_table_append_valuemask)) * dst_positive_scale_table_append_valuemaskentryleft)) /\ exists ff_q_pvs_table_append_valuemaskentryleftpositive. dst_positive_code_table_append_valuemaskentryleft = ff_q_pvs_table_append_valuemaskentryleftpositive * S ((S (dc_index_table_append_valuemask)) * dst_positive_scale_table_append_valuemaskentryleft) + (dst_positive_table_append_valuemaskentryleft))) /\ (((((exists ff_h_pvs_table_append_valuemaskentryleftnegative. ff_h_pvs_table_append_valuemaskentryleftnegative + S (dst_negative_table_append_valuemaskentryleft) = S ((S (dc_index_table_append_valuemask)) * dst_negative_scale_table_append_valuemaskentryleft)) /\ exists ff_q_pvs_table_append_valuemaskentryleftnegative. dst_negative_code_table_append_valuemaskentryleft = ff_q_pvs_table_append_valuemaskentryleftnegative * S ((S (dc_index_table_append_valuemask)) * dst_negative_scale_table_append_valuemaskentryleft) + (dst_negative_table_append_valuemaskentryleft))) /\ (exists ge_balance_positive_table_append_valuemaskentryleftvalue ge_balance_negative_table_append_valuemaskentryleftvalue. (((((dc_left_table_append_valuemaskentry) = 2 * (ge_balance_positive_table_append_valuemaskentryleftvalue) /\ (ge_balance_negative_table_append_valuemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_append_valuemaskentryleftvaluedecode. (((dc_left_table_append_valuemaskentry) = 2 * ge_signed_half_table_append_valuemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_append_valuemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_append_valuemaskentryleftvalue) = S ge_signed_half_table_append_valuemaskentryleftvaluedecode))) /\ ((dst_positive_table_append_valuemaskentryleft) + ge_balance_negative_table_append_valuemaskentryleftvalue = (dst_negative_table_append_valuemaskentryleft) + ge_balance_positive_table_append_valuemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_append_valuemaskentryright dst_positive_scale_table_append_valuemaskentryright dst_negative_code_table_append_valuemaskentryright dst_negative_scale_table_append_valuemaskentryright dst_positive_table_append_valuemaskentryright dst_negative_table_append_valuemaskentryright. (((G) = (((((dst_positive_code_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright)) * S ((dst_positive_code_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright)) + ((dst_positive_scale_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright))) + (((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) * S ((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) + ((dst_negative_scale_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)))) * S ((((dst_positive_code_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright)) * S ((dst_positive_code_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright)) + ((dst_positive_scale_table_append_valuemaskentryright) + (dst_positive_scale_table_append_valuemaskentryright))) + (((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) * S ((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) + ((dst_negative_scale_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)))) + ((((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) * S ((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) + ((dst_negative_scale_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright))) + (((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) * S ((dst_negative_code_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)) + ((dst_negative_scale_table_append_valuemaskentryright) + (dst_negative_scale_table_append_valuemaskentryright)))))) /\ (((((exists ff_h_pvs_table_append_valuemaskentryrightpositive. ff_h_pvs_table_append_valuemaskentryrightpositive + S (dst_positive_table_append_valuemaskentryright) = S ((S (dc_quotient_table_append_valuemaskentry)) * dst_positive_scale_table_append_valuemaskentryright)) /\ exists ff_q_pvs_table_append_valuemaskentryrightpositive. dst_positive_code_table_append_valuemaskentryright = ff_q_pvs_table_append_valuemaskentryrightpositive * S ((S (dc_quotient_table_append_valuemaskentry)) * dst_positive_scale_table_append_valuemaskentryright) + (dst_positive_table_append_valuemaskentryright))) /\ (((((exists ff_h_pvs_table_append_valuemaskentryrightnegative. ff_h_pvs_table_append_valuemaskentryrightnegative + S (dst_negative_table_append_valuemaskentryright) = S ((S (dc_quotient_table_append_valuemaskentry)) * dst_negative_scale_table_append_valuemaskentryright)) /\ exists ff_q_pvs_table_append_valuemaskentryrightnegative. dst_negative_code_table_append_valuemaskentryright = ff_q_pvs_table_append_valuemaskentryrightnegative * S ((S (dc_quotient_table_append_valuemaskentry)) * dst_negative_scale_table_append_valuemaskentryright) + (dst_negative_table_append_valuemaskentryright))) /\ (exists ge_balance_positive_table_append_valuemaskentryrightvalue ge_balance_negative_table_append_valuemaskentryrightvalue. (((((dc_right_table_append_valuemaskentry) = 2 * (ge_balance_positive_table_append_valuemaskentryrightvalue) /\ (ge_balance_negative_table_append_valuemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_append_valuemaskentryrightvaluedecode. (((dc_right_table_append_valuemaskentry) = 2 * ge_signed_half_table_append_valuemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_append_valuemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_append_valuemaskentryrightvalue) = S ge_signed_half_table_append_valuemaskentryrightvaluedecode))) /\ ((dst_positive_table_append_valuemaskentryright) + ge_balance_negative_table_append_valuemaskentryrightvalue = (dst_negative_table_append_valuemaskentryright) + ge_balance_positive_table_append_valuemaskentryrightvalue))))))))) /\ (exists sto_ap_table_append_valuemaskentryproduct sto_an_table_append_valuemaskentryproduct sto_bp_table_append_valuemaskentryproduct sto_bn_table_append_valuemaskentryproduct sto_cp_table_append_valuemaskentryproduct sto_cn_table_append_valuemaskentryproduct. (((((dc_left_table_append_valuemaskentry) = 2 * (sto_ap_table_append_valuemaskentryproduct) /\ (sto_an_table_append_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_valuemaskentryproductleft. (((dc_left_table_append_valuemaskentry) = 2 * ge_signed_half_table_append_valuemaskentryproductleft + 1 /\ (sto_ap_table_append_valuemaskentryproduct) = 0) /\ (sto_an_table_append_valuemaskentryproduct) = S ge_signed_half_table_append_valuemaskentryproductleft))) /\ ((((((dc_right_table_append_valuemaskentry) = 2 * (sto_bp_table_append_valuemaskentryproduct) /\ (sto_bn_table_append_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_valuemaskentryproductright. (((dc_right_table_append_valuemaskentry) = 2 * ge_signed_half_table_append_valuemaskentryproductright + 1 /\ (sto_bp_table_append_valuemaskentryproduct) = 0) /\ (sto_bn_table_append_valuemaskentryproduct) = S ge_signed_half_table_append_valuemaskentryproductright))) /\ ((((((dc_value_table_append_valuemask) = 2 * (sto_cp_table_append_valuemaskentryproduct) /\ (sto_cn_table_append_valuemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_valuemaskentryproductoutput. (((dc_value_table_append_valuemask) = 2 * ge_signed_half_table_append_valuemaskentryproductoutput + 1 /\ (sto_cp_table_append_valuemaskentryproduct) = 0) /\ (sto_cn_table_append_valuemaskentryproduct) = S ge_signed_half_table_append_valuemaskentryproductoutput))) /\ ((sto_ap_table_append_valuemaskentryproduct * sto_bp_table_append_valuemaskentryproduct + sto_an_table_append_valuemaskentryproduct * sto_bn_table_append_valuemaskentryproduct) + sto_cn_table_append_valuemaskentryproduct = (sto_ap_table_append_valuemaskentryproduct * sto_bn_table_append_valuemaskentryproduct + sto_an_table_append_valuemaskentryproduct * sto_bp_table_append_valuemaskentryproduct) + sto_cp_table_append_valuemaskentryproduct))))))))))))))) \/ ((((dc_index_table_append_valuemask)=0 \/ ~(exists pvs_factor_table_append_valuemaskentrynondivisor. (S N) = (dc_index_table_append_valuemask) * pvs_factor_table_append_valuemaskentrynondivisor)) /\ ((dc_value_table_append_valuemask)=0))))))) /\ (exists dst_positive_code_table_append_valuefold dst_positive_scale_table_append_valuefold dst_negative_code_table_append_valuefold dst_negative_scale_table_append_valuefold dst_positive_sum_table_append_valuefold dst_negative_sum_table_append_valuefold. (((dc_mask_table_append_value) = (((((dst_positive_code_table_append_valuefold) + (dst_positive_scale_table_append_valuefold)) * S ((dst_positive_code_table_append_valuefold) + (dst_positive_scale_table_append_valuefold)) + ((dst_positive_scale_table_append_valuefold) + (dst_positive_scale_table_append_valuefold))) + (((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) * S ((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) + ((dst_negative_scale_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)))) * S ((((dst_positive_code_table_append_valuefold) + (dst_positive_scale_table_append_valuefold)) * S ((dst_positive_code_table_append_valuefold) + (dst_positive_scale_table_append_valuefold)) + ((dst_positive_scale_table_append_valuefold) + (dst_positive_scale_table_append_valuefold))) + (((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) * S ((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) + ((dst_negative_scale_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)))) + ((((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) * S ((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) + ((dst_negative_scale_table_append_valuefold) + (dst_negative_scale_table_append_valuefold))) + (((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) * S ((dst_negative_code_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)) + ((dst_negative_scale_table_append_valuefold) + (dst_negative_scale_table_append_valuefold)))))) /\ (((exists fs_u_dst_table_append_valuefoldpositive fs_v_dst_table_append_valuefoldpositive. ((((exists fs_h_dst_table_append_valuefoldpositive_body_start. fs_h_dst_table_append_valuefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_valuefoldpositive)) /\ exists fs_q_dst_table_append_valuefoldpositive_body_start. fs_u_dst_table_append_valuefoldpositive = fs_q_dst_table_append_valuefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_append_valuefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_append_valuefoldpositive_body_terminal. fs_h_dst_table_append_valuefoldpositive_body_terminal + S (dst_positive_sum_table_append_valuefold) = S ((S (S (S N))) * fs_v_dst_table_append_valuefoldpositive)) /\ exists fs_q_dst_table_append_valuefoldpositive_body_terminal. fs_u_dst_table_append_valuefoldpositive = fs_q_dst_table_append_valuefoldpositive_body_terminal * S ((S (S (S N))) * fs_v_dst_table_append_valuefoldpositive) + (dst_positive_sum_table_append_valuefold))) /\ forall fs_i_dst_table_append_valuefoldpositive_body_steps. (exists fs_lt_dst_table_append_valuefoldpositive_body_steps_bound. fs_lt_dst_table_append_valuefoldpositive_body_steps_bound + S fs_i_dst_table_append_valuefoldpositive_body_steps = S (S N)) -> exists fs_a_dst_table_append_valuefoldpositive_body_steps fs_r_dst_table_append_valuefoldpositive_body_steps fs_s_dst_table_append_valuefoldpositive_body_steps. ((((exists fs_h_dst_table_append_valuefoldpositive_body_steps_summand. fs_h_dst_table_append_valuefoldpositive_body_steps_summand + S (fs_a_dst_table_append_valuefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_valuefoldpositive_body_steps)) * dst_positive_scale_table_append_valuefold)) /\ exists fs_q_dst_table_append_valuefoldpositive_body_steps_summand. dst_positive_code_table_append_valuefold = fs_q_dst_table_append_valuefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_append_valuefoldpositive_body_steps)) * dst_positive_scale_table_append_valuefold) + (fs_a_dst_table_append_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_valuefoldpositive_body_steps_partial. fs_h_dst_table_append_valuefoldpositive_body_steps_partial + S (fs_r_dst_table_append_valuefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_valuefoldpositive_body_steps)) * fs_v_dst_table_append_valuefoldpositive)) /\ exists fs_q_dst_table_append_valuefoldpositive_body_steps_partial. fs_u_dst_table_append_valuefoldpositive = fs_q_dst_table_append_valuefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_append_valuefoldpositive_body_steps)) * fs_v_dst_table_append_valuefoldpositive) + (fs_r_dst_table_append_valuefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_valuefoldpositive_body_steps_successor. fs_h_dst_table_append_valuefoldpositive_body_steps_successor + S (fs_s_dst_table_append_valuefoldpositive_body_steps) = S ((S (S fs_i_dst_table_append_valuefoldpositive_body_steps)) * fs_v_dst_table_append_valuefoldpositive)) /\ exists fs_q_dst_table_append_valuefoldpositive_body_steps_successor. fs_u_dst_table_append_valuefoldpositive = fs_q_dst_table_append_valuefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_append_valuefoldpositive_body_steps)) * fs_v_dst_table_append_valuefoldpositive) + (fs_s_dst_table_append_valuefoldpositive_body_steps))) /\ fs_s_dst_table_append_valuefoldpositive_body_steps = fs_r_dst_table_append_valuefoldpositive_body_steps + fs_a_dst_table_append_valuefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_append_valuefoldnegative fs_v_dst_table_append_valuefoldnegative. ((((exists fs_h_dst_table_append_valuefoldnegative_body_start. fs_h_dst_table_append_valuefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_valuefoldnegative)) /\ exists fs_q_dst_table_append_valuefoldnegative_body_start. fs_u_dst_table_append_valuefoldnegative = fs_q_dst_table_append_valuefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_append_valuefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_append_valuefoldnegative_body_terminal. fs_h_dst_table_append_valuefoldnegative_body_terminal + S (dst_negative_sum_table_append_valuefold) = S ((S (S (S N))) * fs_v_dst_table_append_valuefoldnegative)) /\ exists fs_q_dst_table_append_valuefoldnegative_body_terminal. fs_u_dst_table_append_valuefoldnegative = fs_q_dst_table_append_valuefoldnegative_body_terminal * S ((S (S (S N))) * fs_v_dst_table_append_valuefoldnegative) + (dst_negative_sum_table_append_valuefold))) /\ forall fs_i_dst_table_append_valuefoldnegative_body_steps. (exists fs_lt_dst_table_append_valuefoldnegative_body_steps_bound. fs_lt_dst_table_append_valuefoldnegative_body_steps_bound + S fs_i_dst_table_append_valuefoldnegative_body_steps = S (S N)) -> exists fs_a_dst_table_append_valuefoldnegative_body_steps fs_r_dst_table_append_valuefoldnegative_body_steps fs_s_dst_table_append_valuefoldnegative_body_steps. ((((exists fs_h_dst_table_append_valuefoldnegative_body_steps_summand. fs_h_dst_table_append_valuefoldnegative_body_steps_summand + S (fs_a_dst_table_append_valuefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_valuefoldnegative_body_steps)) * dst_negative_scale_table_append_valuefold)) /\ exists fs_q_dst_table_append_valuefoldnegative_body_steps_summand. dst_negative_code_table_append_valuefold = fs_q_dst_table_append_valuefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_append_valuefoldnegative_body_steps)) * dst_negative_scale_table_append_valuefold) + (fs_a_dst_table_append_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_valuefoldnegative_body_steps_partial. fs_h_dst_table_append_valuefoldnegative_body_steps_partial + S (fs_r_dst_table_append_valuefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_valuefoldnegative_body_steps)) * fs_v_dst_table_append_valuefoldnegative)) /\ exists fs_q_dst_table_append_valuefoldnegative_body_steps_partial. fs_u_dst_table_append_valuefoldnegative = fs_q_dst_table_append_valuefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_append_valuefoldnegative_body_steps)) * fs_v_dst_table_append_valuefoldnegative) + (fs_r_dst_table_append_valuefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_valuefoldnegative_body_steps_successor. fs_h_dst_table_append_valuefoldnegative_body_steps_successor + S (fs_s_dst_table_append_valuefoldnegative_body_steps) = S ((S (S fs_i_dst_table_append_valuefoldnegative_body_steps)) * fs_v_dst_table_append_valuefoldnegative)) /\ exists fs_q_dst_table_append_valuefoldnegative_body_steps_successor. fs_u_dst_table_append_valuefoldnegative = fs_q_dst_table_append_valuefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_append_valuefoldnegative_body_steps)) * fs_v_dst_table_append_valuefoldnegative) + (fs_s_dst_table_append_valuefoldnegative_body_steps))) /\ fs_s_dst_table_append_valuefoldnegative_body_steps = fs_r_dst_table_append_valuefoldnegative_body_steps + fs_a_dst_table_append_valuefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_append_valuefoldresult ge_balance_negative_table_append_valuefoldresult. (((((z) = 2 * (ge_balance_positive_table_append_valuefoldresult) /\ (ge_balance_negative_table_append_valuefoldresult) = 0) \/ exists ge_signed_half_table_append_valuefoldresultdecode. (((z) = 2 * ge_signed_half_table_append_valuefoldresultdecode + 1 /\ (ge_balance_positive_table_append_valuefoldresult) = 0) /\ (ge_balance_negative_table_append_valuefoldresult) = S ge_signed_half_table_append_valuefoldresultdecode))) /\ ((dst_positive_sum_table_append_valuefold) + ge_balance_negative_table_append_valuefoldresult = (dst_negative_sum_table_append_valuefold) + ge_balance_positive_table_append_valuefoldresult))))))))))))) -> exists K. (((exists dst_positive_code_table_append_resultleft dst_positive_scale_table_append_resultleft dst_negative_code_table_append_resultleft dst_negative_scale_table_append_resultleft. (((F) = (((((dst_positive_code_table_append_resultleft) + (dst_positive_scale_table_append_resultleft)) * S ((dst_positive_code_table_append_resultleft) + (dst_positive_scale_table_append_resultleft)) + ((dst_positive_scale_table_append_resultleft) + (dst_positive_scale_table_append_resultleft))) + (((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) * S ((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) + ((dst_negative_scale_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)))) * S ((((dst_positive_code_table_append_resultleft) + (dst_positive_scale_table_append_resultleft)) * S ((dst_positive_code_table_append_resultleft) + (dst_positive_scale_table_append_resultleft)) + ((dst_positive_scale_table_append_resultleft) + (dst_positive_scale_table_append_resultleft))) + (((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) * S ((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) + ((dst_negative_scale_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)))) + ((((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) * S ((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) + ((dst_negative_scale_table_append_resultleft) + (dst_negative_scale_table_append_resultleft))) + (((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) * S ((dst_negative_code_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)) + ((dst_negative_scale_table_append_resultleft) + (dst_negative_scale_table_append_resultleft)))))) /\ (forall dst_index_table_append_resultleft. (exists pvs_le_gap_table_append_resultleftdomain. pvs_le_gap_table_append_resultleftdomain + (dst_index_table_append_resultleft) = (S N)) -> exists dst_positive_table_append_resultleft dst_negative_table_append_resultleft dst_value_table_append_resultleft. ((((exists ff_h_pvs_table_append_resultleftentrypositive. ff_h_pvs_table_append_resultleftentrypositive + S (dst_positive_table_append_resultleft) = S ((S (dst_index_table_append_resultleft)) * dst_positive_scale_table_append_resultleft)) /\ exists ff_q_pvs_table_append_resultleftentrypositive. dst_positive_code_table_append_resultleft = ff_q_pvs_table_append_resultleftentrypositive * S ((S (dst_index_table_append_resultleft)) * dst_positive_scale_table_append_resultleft) + (dst_positive_table_append_resultleft))) /\ (((((exists ff_h_pvs_table_append_resultleftentrynegative. ff_h_pvs_table_append_resultleftentrynegative + S (dst_negative_table_append_resultleft) = S ((S (dst_index_table_append_resultleft)) * dst_negative_scale_table_append_resultleft)) /\ exists ff_q_pvs_table_append_resultleftentrynegative. dst_negative_code_table_append_resultleft = ff_q_pvs_table_append_resultleftentrynegative * S ((S (dst_index_table_append_resultleft)) * dst_negative_scale_table_append_resultleft) + (dst_negative_table_append_resultleft))) /\ (exists ge_balance_positive_table_append_resultleftentryvalue ge_balance_negative_table_append_resultleftentryvalue. (((((dst_value_table_append_resultleft) = 2 * (ge_balance_positive_table_append_resultleftentryvalue) /\ (ge_balance_negative_table_append_resultleftentryvalue) = 0) \/ exists ge_signed_half_table_append_resultleftentryvaluedecode. (((dst_value_table_append_resultleft) = 2 * ge_signed_half_table_append_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_table_append_resultleftentryvalue) = 0) /\ (ge_balance_negative_table_append_resultleftentryvalue) = S ge_signed_half_table_append_resultleftentryvaluedecode))) /\ ((dst_positive_table_append_resultleft) + ge_balance_negative_table_append_resultleftentryvalue = (dst_negative_table_append_resultleft) + ge_balance_positive_table_append_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_table_append_resultright dst_positive_scale_table_append_resultright dst_negative_code_table_append_resultright dst_negative_scale_table_append_resultright. (((G) = (((((dst_positive_code_table_append_resultright) + (dst_positive_scale_table_append_resultright)) * S ((dst_positive_code_table_append_resultright) + (dst_positive_scale_table_append_resultright)) + ((dst_positive_scale_table_append_resultright) + (dst_positive_scale_table_append_resultright))) + (((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) * S ((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) + ((dst_negative_scale_table_append_resultright) + (dst_negative_scale_table_append_resultright)))) * S ((((dst_positive_code_table_append_resultright) + (dst_positive_scale_table_append_resultright)) * S ((dst_positive_code_table_append_resultright) + (dst_positive_scale_table_append_resultright)) + ((dst_positive_scale_table_append_resultright) + (dst_positive_scale_table_append_resultright))) + (((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) * S ((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) + ((dst_negative_scale_table_append_resultright) + (dst_negative_scale_table_append_resultright)))) + ((((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) * S ((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) + ((dst_negative_scale_table_append_resultright) + (dst_negative_scale_table_append_resultright))) + (((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) * S ((dst_negative_code_table_append_resultright) + (dst_negative_scale_table_append_resultright)) + ((dst_negative_scale_table_append_resultright) + (dst_negative_scale_table_append_resultright)))))) /\ (forall dst_index_table_append_resultright. (exists pvs_le_gap_table_append_resultrightdomain. pvs_le_gap_table_append_resultrightdomain + (dst_index_table_append_resultright) = (S N)) -> exists dst_positive_table_append_resultright dst_negative_table_append_resultright dst_value_table_append_resultright. ((((exists ff_h_pvs_table_append_resultrightentrypositive. ff_h_pvs_table_append_resultrightentrypositive + S (dst_positive_table_append_resultright) = S ((S (dst_index_table_append_resultright)) * dst_positive_scale_table_append_resultright)) /\ exists ff_q_pvs_table_append_resultrightentrypositive. dst_positive_code_table_append_resultright = ff_q_pvs_table_append_resultrightentrypositive * S ((S (dst_index_table_append_resultright)) * dst_positive_scale_table_append_resultright) + (dst_positive_table_append_resultright))) /\ (((((exists ff_h_pvs_table_append_resultrightentrynegative. ff_h_pvs_table_append_resultrightentrynegative + S (dst_negative_table_append_resultright) = S ((S (dst_index_table_append_resultright)) * dst_negative_scale_table_append_resultright)) /\ exists ff_q_pvs_table_append_resultrightentrynegative. dst_negative_code_table_append_resultright = ff_q_pvs_table_append_resultrightentrynegative * S ((S (dst_index_table_append_resultright)) * dst_negative_scale_table_append_resultright) + (dst_negative_table_append_resultright))) /\ (exists ge_balance_positive_table_append_resultrightentryvalue ge_balance_negative_table_append_resultrightentryvalue. (((((dst_value_table_append_resultright) = 2 * (ge_balance_positive_table_append_resultrightentryvalue) /\ (ge_balance_negative_table_append_resultrightentryvalue) = 0) \/ exists ge_signed_half_table_append_resultrightentryvaluedecode. (((dst_value_table_append_resultright) = 2 * ge_signed_half_table_append_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_table_append_resultrightentryvalue) = 0) /\ (ge_balance_negative_table_append_resultrightentryvalue) = S ge_signed_half_table_append_resultrightentryvaluedecode))) /\ ((dst_positive_table_append_resultright) + ge_balance_negative_table_append_resultrightentryvalue = (dst_negative_table_append_resultright) + ge_balance_positive_table_append_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_table_append_resulttable dst_positive_scale_table_append_resulttable dst_negative_code_table_append_resulttable dst_negative_scale_table_append_resulttable. (((K) = (((((dst_positive_code_table_append_resulttable) + (dst_positive_scale_table_append_resulttable)) * S ((dst_positive_code_table_append_resulttable) + (dst_positive_scale_table_append_resulttable)) + ((dst_positive_scale_table_append_resulttable) + (dst_positive_scale_table_append_resulttable))) + (((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) * S ((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) + ((dst_negative_scale_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)))) * S ((((dst_positive_code_table_append_resulttable) + (dst_positive_scale_table_append_resulttable)) * S ((dst_positive_code_table_append_resulttable) + (dst_positive_scale_table_append_resulttable)) + ((dst_positive_scale_table_append_resulttable) + (dst_positive_scale_table_append_resulttable))) + (((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) * S ((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) + ((dst_negative_scale_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)))) + ((((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) * S ((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) + ((dst_negative_scale_table_append_resulttable) + (dst_negative_scale_table_append_resulttable))) + (((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) * S ((dst_negative_code_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)) + ((dst_negative_scale_table_append_resulttable) + (dst_negative_scale_table_append_resulttable)))))) /\ (forall dst_index_table_append_resulttable. (exists pvs_le_gap_table_append_resulttabledomain. pvs_le_gap_table_append_resulttabledomain + (dst_index_table_append_resulttable) = (S N)) -> exists dst_positive_table_append_resulttable dst_negative_table_append_resulttable dst_value_table_append_resulttable. ((((exists ff_h_pvs_table_append_resulttableentrypositive. ff_h_pvs_table_append_resulttableentrypositive + S (dst_positive_table_append_resulttable) = S ((S (dst_index_table_append_resulttable)) * dst_positive_scale_table_append_resulttable)) /\ exists ff_q_pvs_table_append_resulttableentrypositive. dst_positive_code_table_append_resulttable = ff_q_pvs_table_append_resulttableentrypositive * S ((S (dst_index_table_append_resulttable)) * dst_positive_scale_table_append_resulttable) + (dst_positive_table_append_resulttable))) /\ (((((exists ff_h_pvs_table_append_resulttableentrynegative. ff_h_pvs_table_append_resulttableentrynegative + S (dst_negative_table_append_resulttable) = S ((S (dst_index_table_append_resulttable)) * dst_negative_scale_table_append_resulttable)) /\ exists ff_q_pvs_table_append_resulttableentrynegative. dst_negative_code_table_append_resulttable = ff_q_pvs_table_append_resulttableentrynegative * S ((S (dst_index_table_append_resulttable)) * dst_negative_scale_table_append_resulttable) + (dst_negative_table_append_resulttable))) /\ (exists ge_balance_positive_table_append_resulttableentryvalue ge_balance_negative_table_append_resulttableentryvalue. (((((dst_value_table_append_resulttable) = 2 * (ge_balance_positive_table_append_resulttableentryvalue) /\ (ge_balance_negative_table_append_resulttableentryvalue) = 0) \/ exists ge_signed_half_table_append_resulttableentryvaluedecode. (((dst_value_table_append_resulttable) = 2 * ge_signed_half_table_append_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_table_append_resulttableentryvalue) = 0) /\ (ge_balance_negative_table_append_resulttableentryvalue) = S ge_signed_half_table_append_resulttableentryvaluedecode))) /\ ((dst_positive_table_append_resulttable) + ge_balance_negative_table_append_resulttableentryvalue = (dst_negative_table_append_resulttable) + ge_balance_positive_table_append_resulttableentryvalue))))))))) /\ (forall dc_input_table_append_result dc_output_table_append_result. ~(dc_input_table_append_result=0) -> (exists pvs_le_gap_table_append_resultdomain. pvs_le_gap_table_append_resultdomain + (dc_input_table_append_result) = (S N)) -> (exists dst_positive_code_table_append_resultlookup dst_positive_scale_table_append_resultlookup dst_negative_code_table_append_resultlookup dst_negative_scale_table_append_resultlookup dst_positive_table_append_resultlookup dst_negative_table_append_resultlookup. (((K) = (((((dst_positive_code_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup)) * S ((dst_positive_code_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup)) + ((dst_positive_scale_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup))) + (((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) * S ((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) + ((dst_negative_scale_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)))) * S ((((dst_positive_code_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup)) * S ((dst_positive_code_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup)) + ((dst_positive_scale_table_append_resultlookup) + (dst_positive_scale_table_append_resultlookup))) + (((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) * S ((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) + ((dst_negative_scale_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)))) + ((((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) * S ((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) + ((dst_negative_scale_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup))) + (((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) * S ((dst_negative_code_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)) + ((dst_negative_scale_table_append_resultlookup) + (dst_negative_scale_table_append_resultlookup)))))) /\ (((((exists ff_h_pvs_table_append_resultlookuppositive. ff_h_pvs_table_append_resultlookuppositive + S (dst_positive_table_append_resultlookup) = S ((S (dc_input_table_append_result)) * dst_positive_scale_table_append_resultlookup)) /\ exists ff_q_pvs_table_append_resultlookuppositive. dst_positive_code_table_append_resultlookup = ff_q_pvs_table_append_resultlookuppositive * S ((S (dc_input_table_append_result)) * dst_positive_scale_table_append_resultlookup) + (dst_positive_table_append_resultlookup))) /\ (((((exists ff_h_pvs_table_append_resultlookupnegative. ff_h_pvs_table_append_resultlookupnegative + S (dst_negative_table_append_resultlookup) = S ((S (dc_input_table_append_result)) * dst_negative_scale_table_append_resultlookup)) /\ exists ff_q_pvs_table_append_resultlookupnegative. dst_negative_code_table_append_resultlookup = ff_q_pvs_table_append_resultlookupnegative * S ((S (dc_input_table_append_result)) * dst_negative_scale_table_append_resultlookup) + (dst_negative_table_append_resultlookup))) /\ (exists ge_balance_positive_table_append_resultlookupvalue ge_balance_negative_table_append_resultlookupvalue. (((((dc_output_table_append_result) = 2 * (ge_balance_positive_table_append_resultlookupvalue) /\ (ge_balance_negative_table_append_resultlookupvalue) = 0) \/ exists ge_signed_half_table_append_resultlookupvaluedecode. (((dc_output_table_append_result) = 2 * ge_signed_half_table_append_resultlookupvaluedecode + 1 /\ (ge_balance_positive_table_append_resultlookupvalue) = 0) /\ (ge_balance_negative_table_append_resultlookupvalue) = S ge_signed_half_table_append_resultlookupvaluedecode))) /\ ((dst_positive_table_append_resultlookup) + ge_balance_negative_table_append_resultlookupvalue = (dst_negative_table_append_resultlookup) + ge_balance_positive_table_append_resultlookupvalue))))))))) -> (((~((dc_input_table_append_result)=0)) /\ (exists dc_mask_table_append_resultvalue. ((((exists dst_positive_code_table_append_resultvaluemasktable dst_positive_scale_table_append_resultvaluemasktable dst_negative_code_table_append_resultvaluemasktable dst_negative_scale_table_append_resultvaluemasktable. (((dc_mask_table_append_resultvalue) = (((((dst_positive_code_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable)) * S ((dst_positive_code_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable)) + ((dst_positive_scale_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable))) + (((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) * S ((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) + ((dst_negative_scale_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)))) * S ((((dst_positive_code_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable)) * S ((dst_positive_code_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable)) + ((dst_positive_scale_table_append_resultvaluemasktable) + (dst_positive_scale_table_append_resultvaluemasktable))) + (((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) * S ((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) + ((dst_negative_scale_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)))) + ((((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) * S ((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) + ((dst_negative_scale_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable))) + (((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) * S ((dst_negative_code_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)) + ((dst_negative_scale_table_append_resultvaluemasktable) + (dst_negative_scale_table_append_resultvaluemasktable)))))) /\ (forall dst_index_table_append_resultvaluemasktable. (exists pvs_le_gap_table_append_resultvaluemasktabledomain. pvs_le_gap_table_append_resultvaluemasktabledomain + (dst_index_table_append_resultvaluemasktable) = (dc_input_table_append_result)) -> exists dst_positive_table_append_resultvaluemasktable dst_negative_table_append_resultvaluemasktable dst_value_table_append_resultvaluemasktable. ((((exists ff_h_pvs_table_append_resultvaluemasktableentrypositive. ff_h_pvs_table_append_resultvaluemasktableentrypositive + S (dst_positive_table_append_resultvaluemasktable) = S ((S (dst_index_table_append_resultvaluemasktable)) * dst_positive_scale_table_append_resultvaluemasktable)) /\ exists ff_q_pvs_table_append_resultvaluemasktableentrypositive. dst_positive_code_table_append_resultvaluemasktable = ff_q_pvs_table_append_resultvaluemasktableentrypositive * S ((S (dst_index_table_append_resultvaluemasktable)) * dst_positive_scale_table_append_resultvaluemasktable) + (dst_positive_table_append_resultvaluemasktable))) /\ (((((exists ff_h_pvs_table_append_resultvaluemasktableentrynegative. ff_h_pvs_table_append_resultvaluemasktableentrynegative + S (dst_negative_table_append_resultvaluemasktable) = S ((S (dst_index_table_append_resultvaluemasktable)) * dst_negative_scale_table_append_resultvaluemasktable)) /\ exists ff_q_pvs_table_append_resultvaluemasktableentrynegative. dst_negative_code_table_append_resultvaluemasktable = ff_q_pvs_table_append_resultvaluemasktableentrynegative * S ((S (dst_index_table_append_resultvaluemasktable)) * dst_negative_scale_table_append_resultvaluemasktable) + (dst_negative_table_append_resultvaluemasktable))) /\ (exists ge_balance_positive_table_append_resultvaluemasktableentryvalue ge_balance_negative_table_append_resultvaluemasktableentryvalue. (((((dst_value_table_append_resultvaluemasktable) = 2 * (ge_balance_positive_table_append_resultvaluemasktableentryvalue) /\ (ge_balance_negative_table_append_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_table_append_resultvaluemasktableentryvaluedecode. (((dst_value_table_append_resultvaluemasktable) = 2 * ge_signed_half_table_append_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_table_append_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_table_append_resultvaluemasktableentryvalue) = S ge_signed_half_table_append_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_table_append_resultvaluemasktable) + ge_balance_negative_table_append_resultvaluemasktableentryvalue = (dst_negative_table_append_resultvaluemasktable) + ge_balance_positive_table_append_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_table_append_resultvaluemask dc_value_table_append_resultvaluemask. (exists pvs_le_gap_table_append_resultvaluemaskdomain. pvs_le_gap_table_append_resultvaluemaskdomain + (dc_index_table_append_resultvaluemask) = (dc_input_table_append_result)) -> (exists dst_positive_code_table_append_resultvaluemasklookup dst_positive_scale_table_append_resultvaluemasklookup dst_negative_code_table_append_resultvaluemasklookup dst_negative_scale_table_append_resultvaluemasklookup dst_positive_table_append_resultvaluemasklookup dst_negative_table_append_resultvaluemasklookup. (((dc_mask_table_append_resultvalue) = (((((dst_positive_code_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup)) * S ((dst_positive_code_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup)) + ((dst_positive_scale_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup))) + (((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) * S ((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) + ((dst_negative_scale_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)))) * S ((((dst_positive_code_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup)) * S ((dst_positive_code_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup)) + ((dst_positive_scale_table_append_resultvaluemasklookup) + (dst_positive_scale_table_append_resultvaluemasklookup))) + (((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) * S ((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) + ((dst_negative_scale_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)))) + ((((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) * S ((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) + ((dst_negative_scale_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup))) + (((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) * S ((dst_negative_code_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)) + ((dst_negative_scale_table_append_resultvaluemasklookup) + (dst_negative_scale_table_append_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_table_append_resultvaluemasklookuppositive. ff_h_pvs_table_append_resultvaluemasklookuppositive + S (dst_positive_table_append_resultvaluemasklookup) = S ((S (dc_index_table_append_resultvaluemask)) * dst_positive_scale_table_append_resultvaluemasklookup)) /\ exists ff_q_pvs_table_append_resultvaluemasklookuppositive. dst_positive_code_table_append_resultvaluemasklookup = ff_q_pvs_table_append_resultvaluemasklookuppositive * S ((S (dc_index_table_append_resultvaluemask)) * dst_positive_scale_table_append_resultvaluemasklookup) + (dst_positive_table_append_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_table_append_resultvaluemasklookupnegative. ff_h_pvs_table_append_resultvaluemasklookupnegative + S (dst_negative_table_append_resultvaluemasklookup) = S ((S (dc_index_table_append_resultvaluemask)) * dst_negative_scale_table_append_resultvaluemasklookup)) /\ exists ff_q_pvs_table_append_resultvaluemasklookupnegative. dst_negative_code_table_append_resultvaluemasklookup = ff_q_pvs_table_append_resultvaluemasklookupnegative * S ((S (dc_index_table_append_resultvaluemask)) * dst_negative_scale_table_append_resultvaluemasklookup) + (dst_negative_table_append_resultvaluemasklookup))) /\ (exists ge_balance_positive_table_append_resultvaluemasklookupvalue ge_balance_negative_table_append_resultvaluemasklookupvalue. (((((dc_value_table_append_resultvaluemask) = 2 * (ge_balance_positive_table_append_resultvaluemasklookupvalue) /\ (ge_balance_negative_table_append_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_table_append_resultvaluemasklookupvaluedecode. (((dc_value_table_append_resultvaluemask) = 2 * ge_signed_half_table_append_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_table_append_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_table_append_resultvaluemasklookupvalue) = S ge_signed_half_table_append_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_table_append_resultvaluemasklookup) + ge_balance_negative_table_append_resultvaluemasklookupvalue = (dst_negative_table_append_resultvaluemasklookup) + ge_balance_positive_table_append_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_table_append_resultvaluemask)=0)) /\ (exists dc_quotient_table_append_resultvaluemaskentry dc_left_table_append_resultvaluemaskentry dc_right_table_append_resultvaluemaskentry. (((dc_input_table_append_result)=(dc_index_table_append_resultvaluemask)*dc_quotient_table_append_resultvaluemaskentry) /\ (((exists dst_positive_code_table_append_resultvaluemaskentryleft dst_positive_scale_table_append_resultvaluemaskentryleft dst_negative_code_table_append_resultvaluemaskentryleft dst_negative_scale_table_append_resultvaluemaskentryleft dst_positive_table_append_resultvaluemaskentryleft dst_negative_table_append_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft)) * S ((dst_positive_code_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft)) + ((dst_positive_scale_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft))) + (((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) * S ((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) + ((dst_negative_scale_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)))) * S ((((dst_positive_code_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft)) * S ((dst_positive_code_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft)) + ((dst_positive_scale_table_append_resultvaluemaskentryleft) + (dst_positive_scale_table_append_resultvaluemaskentryleft))) + (((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) * S ((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) + ((dst_negative_scale_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)))) + ((((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) * S ((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) + ((dst_negative_scale_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft))) + (((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) * S ((dst_negative_code_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)) + ((dst_negative_scale_table_append_resultvaluemaskentryleft) + (dst_negative_scale_table_append_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_table_append_resultvaluemaskentryleftpositive. ff_h_pvs_table_append_resultvaluemaskentryleftpositive + S (dst_positive_table_append_resultvaluemaskentryleft) = S ((S (dc_index_table_append_resultvaluemask)) * dst_positive_scale_table_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_append_resultvaluemaskentryleftpositive. dst_positive_code_table_append_resultvaluemaskentryleft = ff_q_pvs_table_append_resultvaluemaskentryleftpositive * S ((S (dc_index_table_append_resultvaluemask)) * dst_positive_scale_table_append_resultvaluemaskentryleft) + (dst_positive_table_append_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_table_append_resultvaluemaskentryleftnegative. ff_h_pvs_table_append_resultvaluemaskentryleftnegative + S (dst_negative_table_append_resultvaluemaskentryleft) = S ((S (dc_index_table_append_resultvaluemask)) * dst_negative_scale_table_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_table_append_resultvaluemaskentryleftnegative. dst_negative_code_table_append_resultvaluemaskentryleft = ff_q_pvs_table_append_resultvaluemaskentryleftnegative * S ((S (dc_index_table_append_resultvaluemask)) * dst_negative_scale_table_append_resultvaluemaskentryleft) + (dst_negative_table_append_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_table_append_resultvaluemaskentryleftvalue ge_balance_negative_table_append_resultvaluemaskentryleftvalue. (((((dc_left_table_append_resultvaluemaskentry) = 2 * (ge_balance_positive_table_append_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_table_append_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_table_append_resultvaluemaskentryleftvaluedecode. (((dc_left_table_append_resultvaluemaskentry) = 2 * ge_signed_half_table_append_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_table_append_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_table_append_resultvaluemaskentryleftvalue) = S ge_signed_half_table_append_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_table_append_resultvaluemaskentryleft) + ge_balance_negative_table_append_resultvaluemaskentryleftvalue = (dst_negative_table_append_resultvaluemaskentryleft) + ge_balance_positive_table_append_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_table_append_resultvaluemaskentryright dst_positive_scale_table_append_resultvaluemaskentryright dst_negative_code_table_append_resultvaluemaskentryright dst_negative_scale_table_append_resultvaluemaskentryright dst_positive_table_append_resultvaluemaskentryright dst_negative_table_append_resultvaluemaskentryright. (((G) = (((((dst_positive_code_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright)) * S ((dst_positive_code_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright)) + ((dst_positive_scale_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright))) + (((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) * S ((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) + ((dst_negative_scale_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)))) * S ((((dst_positive_code_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright)) * S ((dst_positive_code_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright)) + ((dst_positive_scale_table_append_resultvaluemaskentryright) + (dst_positive_scale_table_append_resultvaluemaskentryright))) + (((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) * S ((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) + ((dst_negative_scale_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)))) + ((((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) * S ((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) + ((dst_negative_scale_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright))) + (((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) * S ((dst_negative_code_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)) + ((dst_negative_scale_table_append_resultvaluemaskentryright) + (dst_negative_scale_table_append_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_table_append_resultvaluemaskentryrightpositive. ff_h_pvs_table_append_resultvaluemaskentryrightpositive + S (dst_positive_table_append_resultvaluemaskentryright) = S ((S (dc_quotient_table_append_resultvaluemaskentry)) * dst_positive_scale_table_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_append_resultvaluemaskentryrightpositive. dst_positive_code_table_append_resultvaluemaskentryright = ff_q_pvs_table_append_resultvaluemaskentryrightpositive * S ((S (dc_quotient_table_append_resultvaluemaskentry)) * dst_positive_scale_table_append_resultvaluemaskentryright) + (dst_positive_table_append_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_table_append_resultvaluemaskentryrightnegative. ff_h_pvs_table_append_resultvaluemaskentryrightnegative + S (dst_negative_table_append_resultvaluemaskentryright) = S ((S (dc_quotient_table_append_resultvaluemaskentry)) * dst_negative_scale_table_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_table_append_resultvaluemaskentryrightnegative. dst_negative_code_table_append_resultvaluemaskentryright = ff_q_pvs_table_append_resultvaluemaskentryrightnegative * S ((S (dc_quotient_table_append_resultvaluemaskentry)) * dst_negative_scale_table_append_resultvaluemaskentryright) + (dst_negative_table_append_resultvaluemaskentryright))) /\ (exists ge_balance_positive_table_append_resultvaluemaskentryrightvalue ge_balance_negative_table_append_resultvaluemaskentryrightvalue. (((((dc_right_table_append_resultvaluemaskentry) = 2 * (ge_balance_positive_table_append_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_table_append_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_table_append_resultvaluemaskentryrightvaluedecode. (((dc_right_table_append_resultvaluemaskentry) = 2 * ge_signed_half_table_append_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_table_append_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_table_append_resultvaluemaskentryrightvalue) = S ge_signed_half_table_append_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_table_append_resultvaluemaskentryright) + ge_balance_negative_table_append_resultvaluemaskentryrightvalue = (dst_negative_table_append_resultvaluemaskentryright) + ge_balance_positive_table_append_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_table_append_resultvaluemaskentryproduct sto_an_table_append_resultvaluemaskentryproduct sto_bp_table_append_resultvaluemaskentryproduct sto_bn_table_append_resultvaluemaskentryproduct sto_cp_table_append_resultvaluemaskentryproduct sto_cn_table_append_resultvaluemaskentryproduct. (((((dc_left_table_append_resultvaluemaskentry) = 2 * (sto_ap_table_append_resultvaluemaskentryproduct) /\ (sto_an_table_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_resultvaluemaskentryproductleft. (((dc_left_table_append_resultvaluemaskentry) = 2 * ge_signed_half_table_append_resultvaluemaskentryproductleft + 1 /\ (sto_ap_table_append_resultvaluemaskentryproduct) = 0) /\ (sto_an_table_append_resultvaluemaskentryproduct) = S ge_signed_half_table_append_resultvaluemaskentryproductleft))) /\ ((((((dc_right_table_append_resultvaluemaskentry) = 2 * (sto_bp_table_append_resultvaluemaskentryproduct) /\ (sto_bn_table_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_resultvaluemaskentryproductright. (((dc_right_table_append_resultvaluemaskentry) = 2 * ge_signed_half_table_append_resultvaluemaskentryproductright + 1 /\ (sto_bp_table_append_resultvaluemaskentryproduct) = 0) /\ (sto_bn_table_append_resultvaluemaskentryproduct) = S ge_signed_half_table_append_resultvaluemaskentryproductright))) /\ ((((((dc_value_table_append_resultvaluemask) = 2 * (sto_cp_table_append_resultvaluemaskentryproduct) /\ (sto_cn_table_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_table_append_resultvaluemaskentryproductoutput. (((dc_value_table_append_resultvaluemask) = 2 * ge_signed_half_table_append_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_table_append_resultvaluemaskentryproduct) = 0) /\ (sto_cn_table_append_resultvaluemaskentryproduct) = S ge_signed_half_table_append_resultvaluemaskentryproductoutput))) /\ ((sto_ap_table_append_resultvaluemaskentryproduct * sto_bp_table_append_resultvaluemaskentryproduct + sto_an_table_append_resultvaluemaskentryproduct * sto_bn_table_append_resultvaluemaskentryproduct) + sto_cn_table_append_resultvaluemaskentryproduct = (sto_ap_table_append_resultvaluemaskentryproduct * sto_bn_table_append_resultvaluemaskentryproduct + sto_an_table_append_resultvaluemaskentryproduct * sto_bp_table_append_resultvaluemaskentryproduct) + sto_cp_table_append_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_table_append_resultvaluemask)=0 \/ ~(exists pvs_factor_table_append_resultvaluemaskentrynondivisor. (dc_input_table_append_result) = (dc_index_table_append_resultvaluemask) * pvs_factor_table_append_resultvaluemaskentrynondivisor)) /\ ((dc_value_table_append_resultvaluemask)=0))))))) /\ (exists dst_positive_code_table_append_resultvaluefold dst_positive_scale_table_append_resultvaluefold dst_negative_code_table_append_resultvaluefold dst_negative_scale_table_append_resultvaluefold dst_positive_sum_table_append_resultvaluefold dst_negative_sum_table_append_resultvaluefold. (((dc_mask_table_append_resultvalue) = (((((dst_positive_code_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold)) * S ((dst_positive_code_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold)) + ((dst_positive_scale_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold))) + (((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) * S ((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) + ((dst_negative_scale_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)))) * S ((((dst_positive_code_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold)) * S ((dst_positive_code_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold)) + ((dst_positive_scale_table_append_resultvaluefold) + (dst_positive_scale_table_append_resultvaluefold))) + (((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) * S ((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) + ((dst_negative_scale_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)))) + ((((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) * S ((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) + ((dst_negative_scale_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold))) + (((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) * S ((dst_negative_code_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)) + ((dst_negative_scale_table_append_resultvaluefold) + (dst_negative_scale_table_append_resultvaluefold)))))) /\ (((exists fs_u_dst_table_append_resultvaluefoldpositive fs_v_dst_table_append_resultvaluefoldpositive. ((((exists fs_h_dst_table_append_resultvaluefoldpositive_body_start. fs_h_dst_table_append_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_resultvaluefoldpositive)) /\ exists fs_q_dst_table_append_resultvaluefoldpositive_body_start. fs_u_dst_table_append_resultvaluefoldpositive = fs_q_dst_table_append_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_table_append_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldpositive_body_terminal. fs_h_dst_table_append_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_table_append_resultvaluefold) = S ((S (S (dc_input_table_append_result))) * fs_v_dst_table_append_resultvaluefoldpositive)) /\ exists fs_q_dst_table_append_resultvaluefoldpositive_body_terminal. fs_u_dst_table_append_resultvaluefoldpositive = fs_q_dst_table_append_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_table_append_result))) * fs_v_dst_table_append_resultvaluefoldpositive) + (dst_positive_sum_table_append_resultvaluefold))) /\ forall fs_i_dst_table_append_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_table_append_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_table_append_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_table_append_resultvaluefoldpositive_body_steps = S (dc_input_table_append_result)) -> exists fs_a_dst_table_append_resultvaluefoldpositive_body_steps fs_r_dst_table_append_resultvaluefoldpositive_body_steps fs_s_dst_table_append_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_table_append_resultvaluefoldpositive_body_steps_summand. fs_h_dst_table_append_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_table_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_append_resultvaluefold)) /\ exists fs_q_dst_table_append_resultvaluefoldpositive_body_steps_summand. dst_positive_code_table_append_resultvaluefold = fs_q_dst_table_append_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_table_append_resultvaluefold) + (fs_a_dst_table_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldpositive_body_steps_partial. fs_h_dst_table_append_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_table_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_append_resultvaluefoldpositive)) /\ exists fs_q_dst_table_append_resultvaluefoldpositive_body_steps_partial. fs_u_dst_table_append_resultvaluefoldpositive = fs_q_dst_table_append_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_append_resultvaluefoldpositive) + (fs_r_dst_table_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldpositive_body_steps_successor. fs_h_dst_table_append_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_table_append_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_append_resultvaluefoldpositive)) /\ exists fs_q_dst_table_append_resultvaluefoldpositive_body_steps_successor. fs_u_dst_table_append_resultvaluefoldpositive = fs_q_dst_table_append_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_table_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_table_append_resultvaluefoldpositive) + (fs_s_dst_table_append_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_table_append_resultvaluefoldpositive_body_steps = fs_r_dst_table_append_resultvaluefoldpositive_body_steps + fs_a_dst_table_append_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_table_append_resultvaluefoldnegative fs_v_dst_table_append_resultvaluefoldnegative. ((((exists fs_h_dst_table_append_resultvaluefoldnegative_body_start. fs_h_dst_table_append_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_table_append_resultvaluefoldnegative)) /\ exists fs_q_dst_table_append_resultvaluefoldnegative_body_start. fs_u_dst_table_append_resultvaluefoldnegative = fs_q_dst_table_append_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_table_append_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldnegative_body_terminal. fs_h_dst_table_append_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_table_append_resultvaluefold) = S ((S (S (dc_input_table_append_result))) * fs_v_dst_table_append_resultvaluefoldnegative)) /\ exists fs_q_dst_table_append_resultvaluefoldnegative_body_terminal. fs_u_dst_table_append_resultvaluefoldnegative = fs_q_dst_table_append_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_table_append_result))) * fs_v_dst_table_append_resultvaluefoldnegative) + (dst_negative_sum_table_append_resultvaluefold))) /\ forall fs_i_dst_table_append_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_table_append_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_table_append_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_table_append_resultvaluefoldnegative_body_steps = S (dc_input_table_append_result)) -> exists fs_a_dst_table_append_resultvaluefoldnegative_body_steps fs_r_dst_table_append_resultvaluefoldnegative_body_steps fs_s_dst_table_append_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_table_append_resultvaluefoldnegative_body_steps_summand. fs_h_dst_table_append_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_table_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_append_resultvaluefold)) /\ exists fs_q_dst_table_append_resultvaluefoldnegative_body_steps_summand. dst_negative_code_table_append_resultvaluefold = fs_q_dst_table_append_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_table_append_resultvaluefold) + (fs_a_dst_table_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldnegative_body_steps_partial. fs_h_dst_table_append_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_table_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_append_resultvaluefoldnegative)) /\ exists fs_q_dst_table_append_resultvaluefoldnegative_body_steps_partial. fs_u_dst_table_append_resultvaluefoldnegative = fs_q_dst_table_append_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_append_resultvaluefoldnegative) + (fs_r_dst_table_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_table_append_resultvaluefoldnegative_body_steps_successor. fs_h_dst_table_append_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_table_append_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_append_resultvaluefoldnegative)) /\ exists fs_q_dst_table_append_resultvaluefoldnegative_body_steps_successor. fs_u_dst_table_append_resultvaluefoldnegative = fs_q_dst_table_append_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_table_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_table_append_resultvaluefoldnegative) + (fs_s_dst_table_append_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_table_append_resultvaluefoldnegative_body_steps = fs_r_dst_table_append_resultvaluefoldnegative_body_steps + fs_a_dst_table_append_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_table_append_resultvaluefoldresult ge_balance_negative_table_append_resultvaluefoldresult. (((((dc_output_table_append_result) = 2 * (ge_balance_positive_table_append_resultvaluefoldresult) /\ (ge_balance_negative_table_append_resultvaluefoldresult) = 0) \/ exists ge_signed_half_table_append_resultvaluefoldresultdecode. (((dc_output_table_append_result) = 2 * ge_signed_half_table_append_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_table_append_resultvaluefoldresult) = 0) /\ (ge_balance_negative_table_append_resultvaluefoldresult) = S ge_signed_half_table_append_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_table_append_resultvaluefold) + ge_balance_negative_table_append_resultvaluefoldresult = (dst_negative_sum_table_append_resultvaluefold) + ge_balance_positive_table_append_resultvaluefoldresult)))))))))))))))))))) /\ (forall dst_index_table_append_preserved dst_first_table_append_preserved dst_second_table_append_preserved. (exists pvs_gap_table_append_preservedbound. pvs_gap_table_append_preservedbound + S (dst_index_table_append_preserved) = (S N)) -> (exists dst_positive_code_table_append_preservedfirst dst_positive_scale_table_append_preservedfirst dst_negative_code_table_append_preservedfirst dst_negative_scale_table_append_preservedfirst dst_positive_table_append_preservedfirst dst_negative_table_append_preservedfirst. (((H) = (((((dst_positive_code_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst)) * S ((dst_positive_code_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst)) + ((dst_positive_scale_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst))) + (((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) * S ((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) + ((dst_negative_scale_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)))) * S ((((dst_positive_code_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst)) * S ((dst_positive_code_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst)) + ((dst_positive_scale_table_append_preservedfirst) + (dst_positive_scale_table_append_preservedfirst))) + (((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) * S ((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) + ((dst_negative_scale_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)))) + ((((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) * S ((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) + ((dst_negative_scale_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst))) + (((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) * S ((dst_negative_code_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)) + ((dst_negative_scale_table_append_preservedfirst) + (dst_negative_scale_table_append_preservedfirst)))))) /\ (((((exists ff_h_pvs_table_append_preservedfirstpositive. ff_h_pvs_table_append_preservedfirstpositive + S (dst_positive_table_append_preservedfirst) = S ((S (dst_index_table_append_preserved)) * dst_positive_scale_table_append_preservedfirst)) /\ exists ff_q_pvs_table_append_preservedfirstpositive. dst_positive_code_table_append_preservedfirst = ff_q_pvs_table_append_preservedfirstpositive * S ((S (dst_index_table_append_preserved)) * dst_positive_scale_table_append_preservedfirst) + (dst_positive_table_append_preservedfirst))) /\ (((((exists ff_h_pvs_table_append_preservedfirstnegative. ff_h_pvs_table_append_preservedfirstnegative + S (dst_negative_table_append_preservedfirst) = S ((S (dst_index_table_append_preserved)) * dst_negative_scale_table_append_preservedfirst)) /\ exists ff_q_pvs_table_append_preservedfirstnegative. dst_negative_code_table_append_preservedfirst = ff_q_pvs_table_append_preservedfirstnegative * S ((S (dst_index_table_append_preserved)) * dst_negative_scale_table_append_preservedfirst) + (dst_negative_table_append_preservedfirst))) /\ (exists ge_balance_positive_table_append_preservedfirstvalue ge_balance_negative_table_append_preservedfirstvalue. (((((dst_first_table_append_preserved) = 2 * (ge_balance_positive_table_append_preservedfirstvalue) /\ (ge_balance_negative_table_append_preservedfirstvalue) = 0) \/ exists ge_signed_half_table_append_preservedfirstvaluedecode. (((dst_first_table_append_preserved) = 2 * ge_signed_half_table_append_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_table_append_preservedfirstvalue) = 0) /\ (ge_balance_negative_table_append_preservedfirstvalue) = S ge_signed_half_table_append_preservedfirstvaluedecode))) /\ ((dst_positive_table_append_preservedfirst) + ge_balance_negative_table_append_preservedfirstvalue = (dst_negative_table_append_preservedfirst) + ge_balance_positive_table_append_preservedfirstvalue))))))))) -> (exists dst_positive_code_table_append_preservedsecond dst_positive_scale_table_append_preservedsecond dst_negative_code_table_append_preservedsecond dst_negative_scale_table_append_preservedsecond dst_positive_table_append_preservedsecond dst_negative_table_append_preservedsecond. (((K) = (((((dst_positive_code_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond)) * S ((dst_positive_code_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond)) + ((dst_positive_scale_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond))) + (((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) * S ((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) + ((dst_negative_scale_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)))) * S ((((dst_positive_code_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond)) * S ((dst_positive_code_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond)) + ((dst_positive_scale_table_append_preservedsecond) + (dst_positive_scale_table_append_preservedsecond))) + (((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) * S ((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) + ((dst_negative_scale_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)))) + ((((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) * S ((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) + ((dst_negative_scale_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond))) + (((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) * S ((dst_negative_code_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)) + ((dst_negative_scale_table_append_preservedsecond) + (dst_negative_scale_table_append_preservedsecond)))))) /\ (((((exists ff_h_pvs_table_append_preservedsecondpositive. ff_h_pvs_table_append_preservedsecondpositive + S (dst_positive_table_append_preservedsecond) = S ((S (dst_index_table_append_preserved)) * dst_positive_scale_table_append_preservedsecond)) /\ exists ff_q_pvs_table_append_preservedsecondpositive. dst_positive_code_table_append_preservedsecond = ff_q_pvs_table_append_preservedsecondpositive * S ((S (dst_index_table_append_preserved)) * dst_positive_scale_table_append_preservedsecond) + (dst_positive_table_append_preservedsecond))) /\ (((((exists ff_h_pvs_table_append_preservedsecondnegative. ff_h_pvs_table_append_preservedsecondnegative + S (dst_negative_table_append_preservedsecond) = S ((S (dst_index_table_append_preserved)) * dst_negative_scale_table_append_preservedsecond)) /\ exists ff_q_pvs_table_append_preservedsecondnegative. dst_negative_code_table_append_preservedsecond = ff_q_pvs_table_append_preservedsecondnegative * S ((S (dst_index_table_append_preserved)) * dst_negative_scale_table_append_preservedsecond) + (dst_negative_table_append_preservedsecond))) /\ (exists ge_balance_positive_table_append_preservedsecondvalue ge_balance_negative_table_append_preservedsecondvalue. (((((dst_second_table_append_preserved) = 2 * (ge_balance_positive_table_append_preservedsecondvalue) /\ (ge_balance_negative_table_append_preservedsecondvalue) = 0) \/ exists ge_signed_half_table_append_preservedsecondvaluedecode. (((dst_second_table_append_preserved) = 2 * ge_signed_half_table_append_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_table_append_preservedsecondvalue) = 0) /\ (ge_balance_negative_table_append_preservedsecondvalue) = S ge_signed_half_table_append_preservedsecondvaluedecode))) /\ ((dst_positive_table_append_preservedsecond) + ge_balance_negative_table_append_preservedsecondvalue = (dst_negative_table_append_preservedsecond) + ge_balance_positive_table_append_preservedsecondvalue))))))))) -> dst_first_table_append_preserved = dst_second_table_append_preserved)Complete tactic proof in conservative notation
All 102 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
102 script commands · 24 reading checkpoints · 6 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.
01Fix variables and assumptionsL1–7
02Separate the logical casesL8–10
03Establish hextL11–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table append.
- L11
have hext : ∃ K. ArithTable(S N,K) ∧ (ArithTableEqual(H,K,S N) ∧ ArithAt(K,S N,z))Definitions: ArithTable(S N,K)ArithTableEqual(H,K,S N)ArithAt(K,S N,z)Original native command in the exact edition - L12
specialize arithmetic_signed_table_append (N) - L13
specialize arithmetic_signed_table_append (H) - L14
specialize arithmetic_signed_table_append (z) - L15
apply arithmetic_signed_table_append - L16
exact hc_right_right_left
04Separate the logical casesL17–19
05Construct an explicit witnessL20–20
Supply the displayed value, then prove that it has the required property.
- L20
exists x
06Separate the logical casesL21–22
07Use earlier factsL23–27
08Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
split
09Use earlier factsL29–33
10Separate the logical casesL34–34
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L34
split
11Use earlier factsL35–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
exact hext_witness_left
12Fix variables and assumptionsL36–40
13Establish hcaseL41–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
14Separate the logical casesL46–46
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L46
cases hcase
15Calculate and transport equalitiesL47–50
16Establish heqL51–60
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.
- L51
have heq : z=u - L52
specialize divisor_signed_table_at_functional (x) - L53
specialize divisor_signed_table_at_functional (S N) - L54
specialize divisor_signed_table_at_functional (z) - L55
specialize divisor_signed_table_at_functional (u) - L56
apply divisor_signed_table_at_functional - L57
exact hext_witness_right_right - L58
exact hu - L59
rewrite heq at hz - L60
rewrite heq at hz
17Calculate and transport equalitiesL61–70
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
18Calculate and transport equalitiesL71–71
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L71
rewrite hcase_left
19Use earlier factsL72–72
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L72
exact hz
20Establish hlowL73–77
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.
21Establish hvL78–84
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L78
have hv : ∃ v. ArithAt(H,n,v)Definitions: ArithAt(H,n,v)Original native command in the exact edition - L79
specialize divisor_signed_table_lookup (N) - L80
specialize divisor_signed_table_lookup (H) - L81
specialize divisor_signed_table_lookup (n) - L82
apply divisor_signed_table_lookup - L83
exact hc_right_right_left - L84
exact hlow
22Separate the logical casesL85–85
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L85
cases hv
23Establish heqL86–95
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hext witness right left.
Original defined command ledger · 102 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro H - 0005
intro z - 0006
intro hc - 0007
intro hz - 0008
cases hc - 0009
cases hc_right - 0010
cases hc_right_right - 0011
have hext : ∃ K. ArithTable(S N,K) ∧ (ArithTableEqual(H,K,S N) ∧ ArithAt(K,S N,z)) - 0012
specialize arithmetic_signed_table_append (N) - 0013
specialize arithmetic_signed_table_append (H) - 0014
specialize arithmetic_signed_table_append (z) - 0015
apply arithmetic_signed_table_append - 0016
exact hc_right_right_left - 0017
cases hext - 0018
cases hext_witness - 0019
cases hext_witness_right - 0020
exists x - 0021
split - 0022
split - 0023
specialize signed_table_domain_resize (N) - 0024
specialize signed_table_domain_resize (S N) - 0025
specialize signed_table_domain_resize (F) - 0026
apply signed_table_domain_resize - 0027
exact hc_left - 0028
split - 0029
specialize signed_table_domain_resize (N) - 0030
specialize signed_table_domain_resize (S N) - 0031
specialize signed_table_domain_resize (G) - 0032
apply signed_table_domain_resize - 0033
exact hc_right_left - 0034
split - 0035
exact hext_witness_left - 0036
intro n - 0037
intro u - 0038
intro hn - 0039
intro hbound - 0040
intro hu - 0041
have hcase : n = S N ∨ Lt(n,S N) - 0042
specialize le_eq_or_lt (n) - 0043
specialize le_eq_or_lt (S N) - 0044
apply le_eq_or_lt - 0045
exact hbound - 0046
cases hcase - 0047
rewrite hcase_left at hu - 0048
rewrite hcase_left at hu - 0049
rewrite hcase_left at hu - 0050
rewrite hcase_left at hu - 0051
have heq : z=u - 0052
specialize divisor_signed_table_at_functional (x) - 0053
specialize divisor_signed_table_at_functional (S N) - 0054
specialize divisor_signed_table_at_functional (z) - 0055
specialize divisor_signed_table_at_functional (u) - 0056
apply divisor_signed_table_at_functional - 0057
exact hext_witness_right_right - 0058
exact hu - 0059
rewrite heq at hz - 0060
rewrite heq at hz - 0061
rewrite hcase_left - 0062
rewrite hcase_left - 0063
rewrite hcase_left - 0064
rewrite hcase_left - 0065
rewrite hcase_left - 0066
rewrite hcase_left - 0067
rewrite hcase_left - 0068
rewrite hcase_left - 0069
rewrite hcase_left - 0070
rewrite hcase_left - 0071
rewrite hcase_left - 0072
exact hz - 0073
have hlow : Le(n,N) - 0074
specialize le_of_succ_le_succ (n) - 0075
specialize le_of_succ_le_succ (N) - 0076
apply le_of_succ_le_succ - 0077
exact hcase_right - 0078
have hv : ∃ v. ArithAt(H,n,v) - 0079
specialize divisor_signed_table_lookup (N) - 0080
specialize divisor_signed_table_lookup (H) - 0081
specialize divisor_signed_table_lookup (n) - 0082
apply divisor_signed_table_lookup - 0083
exact hc_right_right_left - 0084
exact hlow - 0085
cases hv - 0086
have heq : x1=u - 0087
specialize hext_witness_right_left (n) - 0088
specialize hext_witness_right_left (x1) - 0089
specialize hext_witness_right_left (u) - 0090
apply hext_witness_right_left - 0091
exact hcase_right - 0092
exact hv_witness - 0093
exact hu - 0094
rewrite heq at hv_witness - 0095
rewrite heq at hv_witness - 0096
specialize hc_right_right_right (n) - 0097
specialize hc_right_right_right (u) - 0098
apply hc_right_right_right - 0099
exact hn - 0100
exact hlow - 0101
exact hv_witness - 0102
exact hext_witness_right_left