Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ T. ∀ G. ∀ u. ArithTable(S N,F) → ArithTable(S N,T) → ArithAt(F,1,u) → SignedUnit(u) → DirichletTable(N,G,F,T) → ∃ x. DirichletTable(S N,x,F,T) ∧ ArithTableEqual(G,x,S N)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
dirichlet_convolution_strict_prefix_exists · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisitele_refl · checked external prerequisitedirichlet_signed_unit_affine_solve · checked external prerequisitearithmetic_signed_table_append · checked external prerequisitedirichlet_convolution_first_input_append_step · checked external prerequisitele_eq_or_lt · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitedirichlet_convolution_first_input_append_preserves · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement
forall N F T G u. (exists dst_positive_code_solve_append_F dst_positive_scale_solve_append_F dst_negative_code_solve_append_F dst_negative_scale_solve_append_F. (((F) = (((((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) * S ((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) + ((dst_positive_scale_solve_append_F) + (dst_positive_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))) * S ((((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) * S ((dst_positive_code_solve_append_F) + (dst_positive_scale_solve_append_F)) + ((dst_positive_scale_solve_append_F) + (dst_positive_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))) + ((((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F))) + (((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) * S ((dst_negative_code_solve_append_F) + (dst_negative_scale_solve_append_F)) + ((dst_negative_scale_solve_append_F) + (dst_negative_scale_solve_append_F)))))) /\ (forall dst_index_solve_append_F. (exists pvs_le_gap_solve_append_Fdomain. pvs_le_gap_solve_append_Fdomain + (dst_index_solve_append_F) = (S N)) -> exists dst_positive_solve_append_F dst_negative_solve_append_F dst_value_solve_append_F. ((((exists ff_h_pvs_solve_append_Fentrypositive. ff_h_pvs_solve_append_Fentrypositive + S (dst_positive_solve_append_F) = S ((S (dst_index_solve_append_F)) * dst_positive_scale_solve_append_F)) /\ exists ff_q_pvs_solve_append_Fentrypositive. dst_positive_code_solve_append_F = ff_q_pvs_solve_append_Fentrypositive * S ((S (dst_index_solve_append_F)) * dst_positive_scale_solve_append_F) + (dst_positive_solve_append_F))) /\ (((((exists ff_h_pvs_solve_append_Fentrynegative. ff_h_pvs_solve_append_Fentrynegative + S (dst_negative_solve_append_F) = S ((S (dst_index_solve_append_F)) * dst_negative_scale_solve_append_F)) /\ exists ff_q_pvs_solve_append_Fentrynegative. dst_negative_code_solve_append_F = ff_q_pvs_solve_append_Fentrynegative * S ((S (dst_index_solve_append_F)) * dst_negative_scale_solve_append_F) + (dst_negative_solve_append_F))) /\ (exists ge_balance_positive_solve_append_Fentryvalue ge_balance_negative_solve_append_Fentryvalue. (((((dst_value_solve_append_F) = 2 * (ge_balance_positive_solve_append_Fentryvalue) /\ (ge_balance_negative_solve_append_Fentryvalue) = 0) \/ exists ge_signed_half_solve_append_Fentryvaluedecode. (((dst_value_solve_append_F) = 2 * ge_signed_half_solve_append_Fentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_Fentryvalue) = 0) /\ (ge_balance_negative_solve_append_Fentryvalue) = S ge_signed_half_solve_append_Fentryvaluedecode))) /\ ((dst_positive_solve_append_F) + ge_balance_negative_solve_append_Fentryvalue = (dst_negative_solve_append_F) + ge_balance_positive_solve_append_Fentryvalue))))))))) -> (exists dst_positive_code_solve_append_T dst_positive_scale_solve_append_T dst_negative_code_solve_append_T dst_negative_scale_solve_append_T. (((T) = (((((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) * S ((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) + ((dst_positive_scale_solve_append_T) + (dst_positive_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))) * S ((((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) * S ((dst_positive_code_solve_append_T) + (dst_positive_scale_solve_append_T)) + ((dst_positive_scale_solve_append_T) + (dst_positive_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))) + ((((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T))) + (((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) * S ((dst_negative_code_solve_append_T) + (dst_negative_scale_solve_append_T)) + ((dst_negative_scale_solve_append_T) + (dst_negative_scale_solve_append_T)))))) /\ (forall dst_index_solve_append_T. (exists pvs_le_gap_solve_append_Tdomain. pvs_le_gap_solve_append_Tdomain + (dst_index_solve_append_T) = (S N)) -> exists dst_positive_solve_append_T dst_negative_solve_append_T dst_value_solve_append_T. ((((exists ff_h_pvs_solve_append_Tentrypositive. ff_h_pvs_solve_append_Tentrypositive + S (dst_positive_solve_append_T) = S ((S (dst_index_solve_append_T)) * dst_positive_scale_solve_append_T)) /\ exists ff_q_pvs_solve_append_Tentrypositive. dst_positive_code_solve_append_T = ff_q_pvs_solve_append_Tentrypositive * S ((S (dst_index_solve_append_T)) * dst_positive_scale_solve_append_T) + (dst_positive_solve_append_T))) /\ (((((exists ff_h_pvs_solve_append_Tentrynegative. ff_h_pvs_solve_append_Tentrynegative + S (dst_negative_solve_append_T) = S ((S (dst_index_solve_append_T)) * dst_negative_scale_solve_append_T)) /\ exists ff_q_pvs_solve_append_Tentrynegative. dst_negative_code_solve_append_T = ff_q_pvs_solve_append_Tentrynegative * S ((S (dst_index_solve_append_T)) * dst_negative_scale_solve_append_T) + (dst_negative_solve_append_T))) /\ (exists ge_balance_positive_solve_append_Tentryvalue ge_balance_negative_solve_append_Tentryvalue. (((((dst_value_solve_append_T) = 2 * (ge_balance_positive_solve_append_Tentryvalue) /\ (ge_balance_negative_solve_append_Tentryvalue) = 0) \/ exists ge_signed_half_solve_append_Tentryvaluedecode. (((dst_value_solve_append_T) = 2 * ge_signed_half_solve_append_Tentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_Tentryvalue) = 0) /\ (ge_balance_negative_solve_append_Tentryvalue) = S ge_signed_half_solve_append_Tentryvaluedecode))) /\ ((dst_positive_solve_append_T) + ge_balance_negative_solve_append_Tentryvalue = (dst_negative_solve_append_T) + ge_balance_positive_solve_append_Tentryvalue))))))))) -> (exists dst_positive_code_solve_append_coefficient dst_positive_scale_solve_append_coefficient dst_negative_code_solve_append_coefficient dst_negative_scale_solve_append_coefficient dst_positive_solve_append_coefficient dst_negative_solve_append_coefficient. (((F) = (((((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) * S ((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) + ((dst_positive_scale_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))) * S ((((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) * S ((dst_positive_code_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient)) + ((dst_positive_scale_solve_append_coefficient) + (dst_positive_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))) + ((((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient))) + (((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) * S ((dst_negative_code_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)) + ((dst_negative_scale_solve_append_coefficient) + (dst_negative_scale_solve_append_coefficient)))))) /\ (((((exists ff_h_pvs_solve_append_coefficientpositive. ff_h_pvs_solve_append_coefficientpositive + S (dst_positive_solve_append_coefficient) = S ((S (1)) * dst_positive_scale_solve_append_coefficient)) /\ exists ff_q_pvs_solve_append_coefficientpositive. dst_positive_code_solve_append_coefficient = ff_q_pvs_solve_append_coefficientpositive * S ((S (1)) * dst_positive_scale_solve_append_coefficient) + (dst_positive_solve_append_coefficient))) /\ (((((exists ff_h_pvs_solve_append_coefficientnegative. ff_h_pvs_solve_append_coefficientnegative + S (dst_negative_solve_append_coefficient) = S ((S (1)) * dst_negative_scale_solve_append_coefficient)) /\ exists ff_q_pvs_solve_append_coefficientnegative. dst_negative_code_solve_append_coefficient = ff_q_pvs_solve_append_coefficientnegative * S ((S (1)) * dst_negative_scale_solve_append_coefficient) + (dst_negative_solve_append_coefficient))) /\ (exists ge_balance_positive_solve_append_coefficientvalue ge_balance_negative_solve_append_coefficientvalue. (((((u) = 2 * (ge_balance_positive_solve_append_coefficientvalue) /\ (ge_balance_negative_solve_append_coefficientvalue) = 0) \/ exists ge_signed_half_solve_append_coefficientvaluedecode. (((u) = 2 * ge_signed_half_solve_append_coefficientvaluedecode + 1 /\ (ge_balance_positive_solve_append_coefficientvalue) = 0) /\ (ge_balance_negative_solve_append_coefficientvalue) = S ge_signed_half_solve_append_coefficientvaluedecode))) /\ ((dst_positive_solve_append_coefficient) + ge_balance_negative_solve_append_coefficientvalue = (dst_negative_solve_append_coefficient) + ge_balance_positive_solve_append_coefficientvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> (((exists dst_positive_code_solve_append_previousleft dst_positive_scale_solve_append_previousleft dst_negative_code_solve_append_previousleft dst_negative_scale_solve_append_previousleft. (((G) = (((((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) * S ((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) + ((dst_positive_scale_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))) * S ((((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) * S ((dst_positive_code_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft)) + ((dst_positive_scale_solve_append_previousleft) + (dst_positive_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))) + ((((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft))) + (((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) * S ((dst_negative_code_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)) + ((dst_negative_scale_solve_append_previousleft) + (dst_negative_scale_solve_append_previousleft)))))) /\ (forall dst_index_solve_append_previousleft. (exists pvs_le_gap_solve_append_previousleftdomain. pvs_le_gap_solve_append_previousleftdomain + (dst_index_solve_append_previousleft) = (N)) -> exists dst_positive_solve_append_previousleft dst_negative_solve_append_previousleft dst_value_solve_append_previousleft. ((((exists ff_h_pvs_solve_append_previousleftentrypositive. ff_h_pvs_solve_append_previousleftentrypositive + S (dst_positive_solve_append_previousleft) = S ((S (dst_index_solve_append_previousleft)) * dst_positive_scale_solve_append_previousleft)) /\ exists ff_q_pvs_solve_append_previousleftentrypositive. dst_positive_code_solve_append_previousleft = ff_q_pvs_solve_append_previousleftentrypositive * S ((S (dst_index_solve_append_previousleft)) * dst_positive_scale_solve_append_previousleft) + (dst_positive_solve_append_previousleft))) /\ (((((exists ff_h_pvs_solve_append_previousleftentrynegative. ff_h_pvs_solve_append_previousleftentrynegative + S (dst_negative_solve_append_previousleft) = S ((S (dst_index_solve_append_previousleft)) * dst_negative_scale_solve_append_previousleft)) /\ exists ff_q_pvs_solve_append_previousleftentrynegative. dst_negative_code_solve_append_previousleft = ff_q_pvs_solve_append_previousleftentrynegative * S ((S (dst_index_solve_append_previousleft)) * dst_negative_scale_solve_append_previousleft) + (dst_negative_solve_append_previousleft))) /\ (exists ge_balance_positive_solve_append_previousleftentryvalue ge_balance_negative_solve_append_previousleftentryvalue. (((((dst_value_solve_append_previousleft) = 2 * (ge_balance_positive_solve_append_previousleftentryvalue) /\ (ge_balance_negative_solve_append_previousleftentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousleftentryvaluedecode. (((dst_value_solve_append_previousleft) = 2 * ge_signed_half_solve_append_previousleftentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousleftentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousleftentryvalue) = S ge_signed_half_solve_append_previousleftentryvaluedecode))) /\ ((dst_positive_solve_append_previousleft) + ge_balance_negative_solve_append_previousleftentryvalue = (dst_negative_solve_append_previousleft) + ge_balance_positive_solve_append_previousleftentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_previousright dst_positive_scale_solve_append_previousright dst_negative_code_solve_append_previousright dst_negative_scale_solve_append_previousright. (((F) = (((((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) * S ((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) + ((dst_positive_scale_solve_append_previousright) + (dst_positive_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))) * S ((((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) * S ((dst_positive_code_solve_append_previousright) + (dst_positive_scale_solve_append_previousright)) + ((dst_positive_scale_solve_append_previousright) + (dst_positive_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))) + ((((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright))) + (((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) * S ((dst_negative_code_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)) + ((dst_negative_scale_solve_append_previousright) + (dst_negative_scale_solve_append_previousright)))))) /\ (forall dst_index_solve_append_previousright. (exists pvs_le_gap_solve_append_previousrightdomain. pvs_le_gap_solve_append_previousrightdomain + (dst_index_solve_append_previousright) = (N)) -> exists dst_positive_solve_append_previousright dst_negative_solve_append_previousright dst_value_solve_append_previousright. ((((exists ff_h_pvs_solve_append_previousrightentrypositive. ff_h_pvs_solve_append_previousrightentrypositive + S (dst_positive_solve_append_previousright) = S ((S (dst_index_solve_append_previousright)) * dst_positive_scale_solve_append_previousright)) /\ exists ff_q_pvs_solve_append_previousrightentrypositive. dst_positive_code_solve_append_previousright = ff_q_pvs_solve_append_previousrightentrypositive * S ((S (dst_index_solve_append_previousright)) * dst_positive_scale_solve_append_previousright) + (dst_positive_solve_append_previousright))) /\ (((((exists ff_h_pvs_solve_append_previousrightentrynegative. ff_h_pvs_solve_append_previousrightentrynegative + S (dst_negative_solve_append_previousright) = S ((S (dst_index_solve_append_previousright)) * dst_negative_scale_solve_append_previousright)) /\ exists ff_q_pvs_solve_append_previousrightentrynegative. dst_negative_code_solve_append_previousright = ff_q_pvs_solve_append_previousrightentrynegative * S ((S (dst_index_solve_append_previousright)) * dst_negative_scale_solve_append_previousright) + (dst_negative_solve_append_previousright))) /\ (exists ge_balance_positive_solve_append_previousrightentryvalue ge_balance_negative_solve_append_previousrightentryvalue. (((((dst_value_solve_append_previousright) = 2 * (ge_balance_positive_solve_append_previousrightentryvalue) /\ (ge_balance_negative_solve_append_previousrightentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousrightentryvaluedecode. (((dst_value_solve_append_previousright) = 2 * ge_signed_half_solve_append_previousrightentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousrightentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousrightentryvalue) = S ge_signed_half_solve_append_previousrightentryvaluedecode))) /\ ((dst_positive_solve_append_previousright) + ge_balance_negative_solve_append_previousrightentryvalue = (dst_negative_solve_append_previousright) + ge_balance_positive_solve_append_previousrightentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_previoustable dst_positive_scale_solve_append_previoustable dst_negative_code_solve_append_previoustable dst_negative_scale_solve_append_previoustable. (((T) = (((((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) * S ((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) + ((dst_positive_scale_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))) * S ((((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) * S ((dst_positive_code_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable)) + ((dst_positive_scale_solve_append_previoustable) + (dst_positive_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))) + ((((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable))) + (((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) * S ((dst_negative_code_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)) + ((dst_negative_scale_solve_append_previoustable) + (dst_negative_scale_solve_append_previoustable)))))) /\ (forall dst_index_solve_append_previoustable. (exists pvs_le_gap_solve_append_previoustabledomain. pvs_le_gap_solve_append_previoustabledomain + (dst_index_solve_append_previoustable) = (N)) -> exists dst_positive_solve_append_previoustable dst_negative_solve_append_previoustable dst_value_solve_append_previoustable. ((((exists ff_h_pvs_solve_append_previoustableentrypositive. ff_h_pvs_solve_append_previoustableentrypositive + S (dst_positive_solve_append_previoustable) = S ((S (dst_index_solve_append_previoustable)) * dst_positive_scale_solve_append_previoustable)) /\ exists ff_q_pvs_solve_append_previoustableentrypositive. dst_positive_code_solve_append_previoustable = ff_q_pvs_solve_append_previoustableentrypositive * S ((S (dst_index_solve_append_previoustable)) * dst_positive_scale_solve_append_previoustable) + (dst_positive_solve_append_previoustable))) /\ (((((exists ff_h_pvs_solve_append_previoustableentrynegative. ff_h_pvs_solve_append_previoustableentrynegative + S (dst_negative_solve_append_previoustable) = S ((S (dst_index_solve_append_previoustable)) * dst_negative_scale_solve_append_previoustable)) /\ exists ff_q_pvs_solve_append_previoustableentrynegative. dst_negative_code_solve_append_previoustable = ff_q_pvs_solve_append_previoustableentrynegative * S ((S (dst_index_solve_append_previoustable)) * dst_negative_scale_solve_append_previoustable) + (dst_negative_solve_append_previoustable))) /\ (exists ge_balance_positive_solve_append_previoustableentryvalue ge_balance_negative_solve_append_previoustableentryvalue. (((((dst_value_solve_append_previoustable) = 2 * (ge_balance_positive_solve_append_previoustableentryvalue) /\ (ge_balance_negative_solve_append_previoustableentryvalue) = 0) \/ exists ge_signed_half_solve_append_previoustableentryvaluedecode. (((dst_value_solve_append_previoustable) = 2 * ge_signed_half_solve_append_previoustableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previoustableentryvalue) = 0) /\ (ge_balance_negative_solve_append_previoustableentryvalue) = S ge_signed_half_solve_append_previoustableentryvaluedecode))) /\ ((dst_positive_solve_append_previoustable) + ge_balance_negative_solve_append_previoustableentryvalue = (dst_negative_solve_append_previoustable) + ge_balance_positive_solve_append_previoustableentryvalue))))))))) /\ (forall dc_input_solve_append_previous dc_output_solve_append_previous. ~(dc_input_solve_append_previous=0) -> (exists pvs_le_gap_solve_append_previousdomain. pvs_le_gap_solve_append_previousdomain + (dc_input_solve_append_previous) = (N)) -> (exists dst_positive_code_solve_append_previouslookup dst_positive_scale_solve_append_previouslookup dst_negative_code_solve_append_previouslookup dst_negative_scale_solve_append_previouslookup dst_positive_solve_append_previouslookup dst_negative_solve_append_previouslookup. (((T) = (((((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) * S ((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) + ((dst_positive_scale_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))) * S ((((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) * S ((dst_positive_code_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup)) + ((dst_positive_scale_solve_append_previouslookup) + (dst_positive_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))) + ((((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup))) + (((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) * S ((dst_negative_code_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)) + ((dst_negative_scale_solve_append_previouslookup) + (dst_negative_scale_solve_append_previouslookup)))))) /\ (((((exists ff_h_pvs_solve_append_previouslookuppositive. ff_h_pvs_solve_append_previouslookuppositive + S (dst_positive_solve_append_previouslookup) = S ((S (dc_input_solve_append_previous)) * dst_positive_scale_solve_append_previouslookup)) /\ exists ff_q_pvs_solve_append_previouslookuppositive. dst_positive_code_solve_append_previouslookup = ff_q_pvs_solve_append_previouslookuppositive * S ((S (dc_input_solve_append_previous)) * dst_positive_scale_solve_append_previouslookup) + (dst_positive_solve_append_previouslookup))) /\ (((((exists ff_h_pvs_solve_append_previouslookupnegative. ff_h_pvs_solve_append_previouslookupnegative + S (dst_negative_solve_append_previouslookup) = S ((S (dc_input_solve_append_previous)) * dst_negative_scale_solve_append_previouslookup)) /\ exists ff_q_pvs_solve_append_previouslookupnegative. dst_negative_code_solve_append_previouslookup = ff_q_pvs_solve_append_previouslookupnegative * S ((S (dc_input_solve_append_previous)) * dst_negative_scale_solve_append_previouslookup) + (dst_negative_solve_append_previouslookup))) /\ (exists ge_balance_positive_solve_append_previouslookupvalue ge_balance_negative_solve_append_previouslookupvalue. (((((dc_output_solve_append_previous) = 2 * (ge_balance_positive_solve_append_previouslookupvalue) /\ (ge_balance_negative_solve_append_previouslookupvalue) = 0) \/ exists ge_signed_half_solve_append_previouslookupvaluedecode. (((dc_output_solve_append_previous) = 2 * ge_signed_half_solve_append_previouslookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_previouslookupvalue) = 0) /\ (ge_balance_negative_solve_append_previouslookupvalue) = S ge_signed_half_solve_append_previouslookupvaluedecode))) /\ ((dst_positive_solve_append_previouslookup) + ge_balance_negative_solve_append_previouslookupvalue = (dst_negative_solve_append_previouslookup) + ge_balance_positive_solve_append_previouslookupvalue))))))))) -> (((~((dc_input_solve_append_previous)=0)) /\ (exists dc_mask_solve_append_previousvalue. ((((exists dst_positive_code_solve_append_previousvaluemasktable dst_positive_scale_solve_append_previousvaluemasktable dst_negative_code_solve_append_previousvaluemasktable dst_negative_scale_solve_append_previousvaluemasktable. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) * S ((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) + ((dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))) * S ((((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) * S ((dst_positive_code_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable)) + ((dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))) + ((((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable))) + (((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) * S ((dst_negative_code_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)) + ((dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_scale_solve_append_previousvaluemasktable)))))) /\ (forall dst_index_solve_append_previousvaluemasktable. (exists pvs_le_gap_solve_append_previousvaluemasktabledomain. pvs_le_gap_solve_append_previousvaluemasktabledomain + (dst_index_solve_append_previousvaluemasktable) = (dc_input_solve_append_previous)) -> exists dst_positive_solve_append_previousvaluemasktable dst_negative_solve_append_previousvaluemasktable dst_value_solve_append_previousvaluemasktable. ((((exists ff_h_pvs_solve_append_previousvaluemasktableentrypositive. ff_h_pvs_solve_append_previousvaluemasktableentrypositive + S (dst_positive_solve_append_previousvaluemasktable) = S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_positive_scale_solve_append_previousvaluemasktable)) /\ exists ff_q_pvs_solve_append_previousvaluemasktableentrypositive. dst_positive_code_solve_append_previousvaluemasktable = ff_q_pvs_solve_append_previousvaluemasktableentrypositive * S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_positive_scale_solve_append_previousvaluemasktable) + (dst_positive_solve_append_previousvaluemasktable))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasktableentrynegative. ff_h_pvs_solve_append_previousvaluemasktableentrynegative + S (dst_negative_solve_append_previousvaluemasktable) = S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_negative_scale_solve_append_previousvaluemasktable)) /\ exists ff_q_pvs_solve_append_previousvaluemasktableentrynegative. dst_negative_code_solve_append_previousvaluemasktable = ff_q_pvs_solve_append_previousvaluemasktableentrynegative * S ((S (dst_index_solve_append_previousvaluemasktable)) * dst_negative_scale_solve_append_previousvaluemasktable) + (dst_negative_solve_append_previousvaluemasktable))) /\ (exists ge_balance_positive_solve_append_previousvaluemasktableentryvalue ge_balance_negative_solve_append_previousvaluemasktableentryvalue. (((((dst_value_solve_append_previousvaluemasktable) = 2 * (ge_balance_positive_solve_append_previousvaluemasktableentryvalue) /\ (ge_balance_negative_solve_append_previousvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode. (((dst_value_solve_append_previousvaluemasktable) = 2 * ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemasktableentryvalue) = S ge_signed_half_solve_append_previousvaluemasktableentryvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemasktable) + ge_balance_negative_solve_append_previousvaluemasktableentryvalue = (dst_negative_solve_append_previousvaluemasktable) + ge_balance_positive_solve_append_previousvaluemasktableentryvalue))))))))) /\ (forall dc_index_solve_append_previousvaluemask dc_value_solve_append_previousvaluemask. (exists pvs_le_gap_solve_append_previousvaluemaskdomain. pvs_le_gap_solve_append_previousvaluemaskdomain + (dc_index_solve_append_previousvaluemask) = (dc_input_solve_append_previous)) -> (exists dst_positive_code_solve_append_previousvaluemasklookup dst_positive_scale_solve_append_previousvaluemasklookup dst_negative_code_solve_append_previousvaluemasklookup dst_negative_scale_solve_append_previousvaluemasklookup dst_positive_solve_append_previousvaluemasklookup dst_negative_solve_append_previousvaluemasklookup. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) * S ((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) + ((dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))) * S ((((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) * S ((dst_positive_code_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup)) + ((dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))) + ((((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup))) + (((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) * S ((dst_negative_code_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)) + ((dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_scale_solve_append_previousvaluemasklookup)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasklookuppositive. ff_h_pvs_solve_append_previousvaluemasklookuppositive + S (dst_positive_solve_append_previousvaluemasklookup) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemasklookup)) /\ exists ff_q_pvs_solve_append_previousvaluemasklookuppositive. dst_positive_code_solve_append_previousvaluemasklookup = ff_q_pvs_solve_append_previousvaluemasklookuppositive * S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemasklookup) + (dst_positive_solve_append_previousvaluemasklookup))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemasklookupnegative. ff_h_pvs_solve_append_previousvaluemasklookupnegative + S (dst_negative_solve_append_previousvaluemasklookup) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemasklookup)) /\ exists ff_q_pvs_solve_append_previousvaluemasklookupnegative. dst_negative_code_solve_append_previousvaluemasklookup = ff_q_pvs_solve_append_previousvaluemasklookupnegative * S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemasklookup) + (dst_negative_solve_append_previousvaluemasklookup))) /\ (exists ge_balance_positive_solve_append_previousvaluemasklookupvalue ge_balance_negative_solve_append_previousvaluemasklookupvalue. (((((dc_value_solve_append_previousvaluemask) = 2 * (ge_balance_positive_solve_append_previousvaluemasklookupvalue) /\ (ge_balance_negative_solve_append_previousvaluemasklookupvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemasklookupvaluedecode. (((dc_value_solve_append_previousvaluemask) = 2 * ge_signed_half_solve_append_previousvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemasklookupvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemasklookupvalue) = S ge_signed_half_solve_append_previousvaluemasklookupvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemasklookup) + ge_balance_negative_solve_append_previousvaluemasklookupvalue = (dst_negative_solve_append_previousvaluemasklookup) + ge_balance_positive_solve_append_previousvaluemasklookupvalue))))))))) -> ((((~((dc_index_solve_append_previousvaluemask)=0)) /\ (exists dc_quotient_solve_append_previousvaluemaskentry dc_left_solve_append_previousvaluemaskentry dc_right_solve_append_previousvaluemaskentry. (((dc_input_solve_append_previous)=(dc_index_solve_append_previousvaluemask)*dc_quotient_solve_append_previousvaluemaskentry) /\ (((exists dst_positive_code_solve_append_previousvaluemaskentryleft dst_positive_scale_solve_append_previousvaluemaskentryleft dst_negative_code_solve_append_previousvaluemaskentryleft dst_negative_scale_solve_append_previousvaluemaskentryleft dst_positive_solve_append_previousvaluemaskentryleft dst_negative_solve_append_previousvaluemaskentryleft. (((G) = (((((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) + ((dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))) * S ((((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_positive_code_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft)) + ((dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))) + ((((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft))) + (((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) * S ((dst_negative_code_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)) + ((dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_scale_solve_append_previousvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryleftpositive. ff_h_pvs_solve_append_previousvaluemaskentryleftpositive + S (dst_positive_solve_append_previousvaluemaskentryleft) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryleftpositive. dst_positive_code_solve_append_previousvaluemaskentryleft = ff_q_pvs_solve_append_previousvaluemaskentryleftpositive * S ((S (dc_index_solve_append_previousvaluemask)) * dst_positive_scale_solve_append_previousvaluemaskentryleft) + (dst_positive_solve_append_previousvaluemaskentryleft))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryleftnegative. ff_h_pvs_solve_append_previousvaluemaskentryleftnegative + S (dst_negative_solve_append_previousvaluemaskentryleft) = S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryleftnegative. dst_negative_code_solve_append_previousvaluemaskentryleft = ff_q_pvs_solve_append_previousvaluemaskentryleftnegative * S ((S (dc_index_solve_append_previousvaluemask)) * dst_negative_scale_solve_append_previousvaluemaskentryleft) + (dst_negative_solve_append_previousvaluemaskentryleft))) /\ (exists ge_balance_positive_solve_append_previousvaluemaskentryleftvalue ge_balance_negative_solve_append_previousvaluemaskentryleftvalue. (((((dc_left_solve_append_previousvaluemaskentry) = 2 * (ge_balance_positive_solve_append_previousvaluemaskentryleftvalue) /\ (ge_balance_negative_solve_append_previousvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode. (((dc_left_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemaskentryleftvalue) = S ge_signed_half_solve_append_previousvaluemaskentryleftvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemaskentryleft) + ge_balance_negative_solve_append_previousvaluemaskentryleftvalue = (dst_negative_solve_append_previousvaluemaskentryleft) + ge_balance_positive_solve_append_previousvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_solve_append_previousvaluemaskentryright dst_positive_scale_solve_append_previousvaluemaskentryright dst_negative_code_solve_append_previousvaluemaskentryright dst_negative_scale_solve_append_previousvaluemaskentryright dst_positive_solve_append_previousvaluemaskentryright dst_negative_solve_append_previousvaluemaskentryright. (((F) = (((((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) * S ((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) + ((dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))) * S ((((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) * S ((dst_positive_code_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright)) + ((dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))) + ((((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright))) + (((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) * S ((dst_negative_code_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)) + ((dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_scale_solve_append_previousvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryrightpositive. ff_h_pvs_solve_append_previousvaluemaskentryrightpositive + S (dst_positive_solve_append_previousvaluemaskentryright) = S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_positive_scale_solve_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryrightpositive. dst_positive_code_solve_append_previousvaluemaskentryright = ff_q_pvs_solve_append_previousvaluemaskentryrightpositive * S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_positive_scale_solve_append_previousvaluemaskentryright) + (dst_positive_solve_append_previousvaluemaskentryright))) /\ (((((exists ff_h_pvs_solve_append_previousvaluemaskentryrightnegative. ff_h_pvs_solve_append_previousvaluemaskentryrightnegative + S (dst_negative_solve_append_previousvaluemaskentryright) = S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_negative_scale_solve_append_previousvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_previousvaluemaskentryrightnegative. dst_negative_code_solve_append_previousvaluemaskentryright = ff_q_pvs_solve_append_previousvaluemaskentryrightnegative * S ((S (dc_quotient_solve_append_previousvaluemaskentry)) * dst_negative_scale_solve_append_previousvaluemaskentryright) + (dst_negative_solve_append_previousvaluemaskentryright))) /\ (exists ge_balance_positive_solve_append_previousvaluemaskentryrightvalue ge_balance_negative_solve_append_previousvaluemaskentryrightvalue. (((((dc_right_solve_append_previousvaluemaskentry) = 2 * (ge_balance_positive_solve_append_previousvaluemaskentryrightvalue) /\ (ge_balance_negative_solve_append_previousvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode. (((dc_right_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_solve_append_previousvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_solve_append_previousvaluemaskentryrightvalue) = S ge_signed_half_solve_append_previousvaluemaskentryrightvaluedecode))) /\ ((dst_positive_solve_append_previousvaluemaskentryright) + ge_balance_negative_solve_append_previousvaluemaskentryrightvalue = (dst_negative_solve_append_previousvaluemaskentryright) + ge_balance_positive_solve_append_previousvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_solve_append_previousvaluemaskentryproduct sto_an_solve_append_previousvaluemaskentryproduct sto_bp_solve_append_previousvaluemaskentryproduct sto_bn_solve_append_previousvaluemaskentryproduct sto_cp_solve_append_previousvaluemaskentryproduct sto_cn_solve_append_previousvaluemaskentryproduct. (((((dc_left_solve_append_previousvaluemaskentry) = 2 * (sto_ap_solve_append_previousvaluemaskentryproduct) /\ (sto_an_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductleft. (((dc_left_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductleft + 1 /\ (sto_ap_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_an_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductleft))) /\ ((((((dc_right_solve_append_previousvaluemaskentry) = 2 * (sto_bp_solve_append_previousvaluemaskentryproduct) /\ (sto_bn_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductright. (((dc_right_solve_append_previousvaluemaskentry) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductright + 1 /\ (sto_bp_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_bn_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductright))) /\ ((((((dc_value_solve_append_previousvaluemask) = 2 * (sto_cp_solve_append_previousvaluemaskentryproduct) /\ (sto_cn_solve_append_previousvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_previousvaluemaskentryproductoutput. (((dc_value_solve_append_previousvaluemask) = 2 * ge_signed_half_solve_append_previousvaluemaskentryproductoutput + 1 /\ (sto_cp_solve_append_previousvaluemaskentryproduct) = 0) /\ (sto_cn_solve_append_previousvaluemaskentryproduct) = S ge_signed_half_solve_append_previousvaluemaskentryproductoutput))) /\ ((sto_ap_solve_append_previousvaluemaskentryproduct * sto_bp_solve_append_previousvaluemaskentryproduct + sto_an_solve_append_previousvaluemaskentryproduct * sto_bn_solve_append_previousvaluemaskentryproduct) + sto_cn_solve_append_previousvaluemaskentryproduct = (sto_ap_solve_append_previousvaluemaskentryproduct * sto_bn_solve_append_previousvaluemaskentryproduct + sto_an_solve_append_previousvaluemaskentryproduct * sto_bp_solve_append_previousvaluemaskentryproduct) + sto_cp_solve_append_previousvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_solve_append_previousvaluemask)=0 \/ ~(exists pvs_factor_solve_append_previousvaluemaskentrynondivisor. (dc_input_solve_append_previous) = (dc_index_solve_append_previousvaluemask) * pvs_factor_solve_append_previousvaluemaskentrynondivisor)) /\ ((dc_value_solve_append_previousvaluemask)=0))))))) /\ (exists dst_positive_code_solve_append_previousvaluefold dst_positive_scale_solve_append_previousvaluefold dst_negative_code_solve_append_previousvaluefold dst_negative_scale_solve_append_previousvaluefold dst_positive_sum_solve_append_previousvaluefold dst_negative_sum_solve_append_previousvaluefold. (((dc_mask_solve_append_previousvalue) = (((((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) * S ((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) + ((dst_positive_scale_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))) * S ((((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) * S ((dst_positive_code_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold)) + ((dst_positive_scale_solve_append_previousvaluefold) + (dst_positive_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))) + ((((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold))) + (((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) * S ((dst_negative_code_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)) + ((dst_negative_scale_solve_append_previousvaluefold) + (dst_negative_scale_solve_append_previousvaluefold)))))) /\ (((exists fs_u_dst_solve_append_previousvaluefoldpositive fs_v_dst_solve_append_previousvaluefoldpositive. ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_start. fs_h_dst_solve_append_previousvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_start. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_terminal. fs_h_dst_solve_append_previousvaluefoldpositive_body_terminal + S (dst_positive_sum_solve_append_previousvaluefold) = S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_terminal. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_terminal * S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldpositive) + (dst_positive_sum_solve_append_previousvaluefold))) /\ forall fs_i_dst_solve_append_previousvaluefoldpositive_body_steps. (exists fs_lt_dst_solve_append_previousvaluefoldpositive_body_steps_bound. fs_lt_dst_solve_append_previousvaluefoldpositive_body_steps_bound + S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps = S (dc_input_solve_append_previous)) -> exists fs_a_dst_solve_append_previousvaluefoldpositive_body_steps fs_r_dst_solve_append_previousvaluefoldpositive_body_steps fs_s_dst_solve_append_previousvaluefoldpositive_body_steps. ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_summand. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_summand + S (fs_a_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_previousvaluefold)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_summand. dst_positive_code_solve_append_previousvaluefold = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_previousvaluefold) + (fs_a_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_partial. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_partial + S (fs_r_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_partial. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (fs_r_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_successor. fs_h_dst_solve_append_previousvaluefoldpositive_body_steps_successor + S (fs_s_dst_solve_append_previousvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive)) /\ exists fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_successor. fs_u_dst_solve_append_previousvaluefoldpositive = fs_q_dst_solve_append_previousvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_solve_append_previousvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_previousvaluefoldpositive) + (fs_s_dst_solve_append_previousvaluefoldpositive_body_steps))) /\ fs_s_dst_solve_append_previousvaluefoldpositive_body_steps = fs_r_dst_solve_append_previousvaluefoldpositive_body_steps + fs_a_dst_solve_append_previousvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_solve_append_previousvaluefoldnegative fs_v_dst_solve_append_previousvaluefoldnegative. ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_start. fs_h_dst_solve_append_previousvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_start. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_terminal. fs_h_dst_solve_append_previousvaluefoldnegative_body_terminal + S (dst_negative_sum_solve_append_previousvaluefold) = S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_terminal. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_terminal * S ((S (S (dc_input_solve_append_previous))) * fs_v_dst_solve_append_previousvaluefoldnegative) + (dst_negative_sum_solve_append_previousvaluefold))) /\ forall fs_i_dst_solve_append_previousvaluefoldnegative_body_steps. (exists fs_lt_dst_solve_append_previousvaluefoldnegative_body_steps_bound. fs_lt_dst_solve_append_previousvaluefoldnegative_body_steps_bound + S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps = S (dc_input_solve_append_previous)) -> exists fs_a_dst_solve_append_previousvaluefoldnegative_body_steps fs_r_dst_solve_append_previousvaluefoldnegative_body_steps fs_s_dst_solve_append_previousvaluefoldnegative_body_steps. ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_summand. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_summand + S (fs_a_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_previousvaluefold)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_summand. dst_negative_code_solve_append_previousvaluefold = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_previousvaluefold) + (fs_a_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_partial. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_partial + S (fs_r_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_partial. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (fs_r_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_successor. fs_h_dst_solve_append_previousvaluefoldnegative_body_steps_successor + S (fs_s_dst_solve_append_previousvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative)) /\ exists fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_successor. fs_u_dst_solve_append_previousvaluefoldnegative = fs_q_dst_solve_append_previousvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_solve_append_previousvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_previousvaluefoldnegative) + (fs_s_dst_solve_append_previousvaluefoldnegative_body_steps))) /\ fs_s_dst_solve_append_previousvaluefoldnegative_body_steps = fs_r_dst_solve_append_previousvaluefoldnegative_body_steps + fs_a_dst_solve_append_previousvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_solve_append_previousvaluefoldresult ge_balance_negative_solve_append_previousvaluefoldresult. (((((dc_output_solve_append_previous) = 2 * (ge_balance_positive_solve_append_previousvaluefoldresult) /\ (ge_balance_negative_solve_append_previousvaluefoldresult) = 0) \/ exists ge_signed_half_solve_append_previousvaluefoldresultdecode. (((dc_output_solve_append_previous) = 2 * ge_signed_half_solve_append_previousvaluefoldresultdecode + 1 /\ (ge_balance_positive_solve_append_previousvaluefoldresult) = 0) /\ (ge_balance_negative_solve_append_previousvaluefoldresult) = S ge_signed_half_solve_append_previousvaluefoldresultdecode))) /\ ((dst_positive_sum_solve_append_previousvaluefold) + ge_balance_negative_solve_append_previousvaluefoldresult = (dst_negative_sum_solve_append_previousvaluefold) + ge_balance_positive_solve_append_previousvaluefoldresult)))))))))))))))))))) -> exists H. ((((exists dst_positive_code_solve_append_resultleft dst_positive_scale_solve_append_resultleft dst_negative_code_solve_append_resultleft dst_negative_scale_solve_append_resultleft. (((H) = (((((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) * S ((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) + ((dst_positive_scale_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))) * S ((((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) * S ((dst_positive_code_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft)) + ((dst_positive_scale_solve_append_resultleft) + (dst_positive_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))) + ((((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft))) + (((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) * S ((dst_negative_code_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)) + ((dst_negative_scale_solve_append_resultleft) + (dst_negative_scale_solve_append_resultleft)))))) /\ (forall dst_index_solve_append_resultleft. (exists pvs_le_gap_solve_append_resultleftdomain. pvs_le_gap_solve_append_resultleftdomain + (dst_index_solve_append_resultleft) = (S N)) -> exists dst_positive_solve_append_resultleft dst_negative_solve_append_resultleft dst_value_solve_append_resultleft. ((((exists ff_h_pvs_solve_append_resultleftentrypositive. ff_h_pvs_solve_append_resultleftentrypositive + S (dst_positive_solve_append_resultleft) = S ((S (dst_index_solve_append_resultleft)) * dst_positive_scale_solve_append_resultleft)) /\ exists ff_q_pvs_solve_append_resultleftentrypositive. dst_positive_code_solve_append_resultleft = ff_q_pvs_solve_append_resultleftentrypositive * S ((S (dst_index_solve_append_resultleft)) * dst_positive_scale_solve_append_resultleft) + (dst_positive_solve_append_resultleft))) /\ (((((exists ff_h_pvs_solve_append_resultleftentrynegative. ff_h_pvs_solve_append_resultleftentrynegative + S (dst_negative_solve_append_resultleft) = S ((S (dst_index_solve_append_resultleft)) * dst_negative_scale_solve_append_resultleft)) /\ exists ff_q_pvs_solve_append_resultleftentrynegative. dst_negative_code_solve_append_resultleft = ff_q_pvs_solve_append_resultleftentrynegative * S ((S (dst_index_solve_append_resultleft)) * dst_negative_scale_solve_append_resultleft) + (dst_negative_solve_append_resultleft))) /\ (exists ge_balance_positive_solve_append_resultleftentryvalue ge_balance_negative_solve_append_resultleftentryvalue. (((((dst_value_solve_append_resultleft) = 2 * (ge_balance_positive_solve_append_resultleftentryvalue) /\ (ge_balance_negative_solve_append_resultleftentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultleftentryvaluedecode. (((dst_value_solve_append_resultleft) = 2 * ge_signed_half_solve_append_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultleftentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultleftentryvalue) = S ge_signed_half_solve_append_resultleftentryvaluedecode))) /\ ((dst_positive_solve_append_resultleft) + ge_balance_negative_solve_append_resultleftentryvalue = (dst_negative_solve_append_resultleft) + ge_balance_positive_solve_append_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_resultright dst_positive_scale_solve_append_resultright dst_negative_code_solve_append_resultright dst_negative_scale_solve_append_resultright. (((F) = (((((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) * S ((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) + ((dst_positive_scale_solve_append_resultright) + (dst_positive_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))) * S ((((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) * S ((dst_positive_code_solve_append_resultright) + (dst_positive_scale_solve_append_resultright)) + ((dst_positive_scale_solve_append_resultright) + (dst_positive_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))) + ((((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright))) + (((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) * S ((dst_negative_code_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)) + ((dst_negative_scale_solve_append_resultright) + (dst_negative_scale_solve_append_resultright)))))) /\ (forall dst_index_solve_append_resultright. (exists pvs_le_gap_solve_append_resultrightdomain. pvs_le_gap_solve_append_resultrightdomain + (dst_index_solve_append_resultright) = (S N)) -> exists dst_positive_solve_append_resultright dst_negative_solve_append_resultright dst_value_solve_append_resultright. ((((exists ff_h_pvs_solve_append_resultrightentrypositive. ff_h_pvs_solve_append_resultrightentrypositive + S (dst_positive_solve_append_resultright) = S ((S (dst_index_solve_append_resultright)) * dst_positive_scale_solve_append_resultright)) /\ exists ff_q_pvs_solve_append_resultrightentrypositive. dst_positive_code_solve_append_resultright = ff_q_pvs_solve_append_resultrightentrypositive * S ((S (dst_index_solve_append_resultright)) * dst_positive_scale_solve_append_resultright) + (dst_positive_solve_append_resultright))) /\ (((((exists ff_h_pvs_solve_append_resultrightentrynegative. ff_h_pvs_solve_append_resultrightentrynegative + S (dst_negative_solve_append_resultright) = S ((S (dst_index_solve_append_resultright)) * dst_negative_scale_solve_append_resultright)) /\ exists ff_q_pvs_solve_append_resultrightentrynegative. dst_negative_code_solve_append_resultright = ff_q_pvs_solve_append_resultrightentrynegative * S ((S (dst_index_solve_append_resultright)) * dst_negative_scale_solve_append_resultright) + (dst_negative_solve_append_resultright))) /\ (exists ge_balance_positive_solve_append_resultrightentryvalue ge_balance_negative_solve_append_resultrightentryvalue. (((((dst_value_solve_append_resultright) = 2 * (ge_balance_positive_solve_append_resultrightentryvalue) /\ (ge_balance_negative_solve_append_resultrightentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultrightentryvaluedecode. (((dst_value_solve_append_resultright) = 2 * ge_signed_half_solve_append_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultrightentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultrightentryvalue) = S ge_signed_half_solve_append_resultrightentryvaluedecode))) /\ ((dst_positive_solve_append_resultright) + ge_balance_negative_solve_append_resultrightentryvalue = (dst_negative_solve_append_resultright) + ge_balance_positive_solve_append_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_solve_append_resulttable dst_positive_scale_solve_append_resulttable dst_negative_code_solve_append_resulttable dst_negative_scale_solve_append_resulttable. (((T) = (((((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) * S ((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) + ((dst_positive_scale_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))) * S ((((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) * S ((dst_positive_code_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable)) + ((dst_positive_scale_solve_append_resulttable) + (dst_positive_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))) + ((((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable))) + (((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) * S ((dst_negative_code_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)) + ((dst_negative_scale_solve_append_resulttable) + (dst_negative_scale_solve_append_resulttable)))))) /\ (forall dst_index_solve_append_resulttable. (exists pvs_le_gap_solve_append_resulttabledomain. pvs_le_gap_solve_append_resulttabledomain + (dst_index_solve_append_resulttable) = (S N)) -> exists dst_positive_solve_append_resulttable dst_negative_solve_append_resulttable dst_value_solve_append_resulttable. ((((exists ff_h_pvs_solve_append_resulttableentrypositive. ff_h_pvs_solve_append_resulttableentrypositive + S (dst_positive_solve_append_resulttable) = S ((S (dst_index_solve_append_resulttable)) * dst_positive_scale_solve_append_resulttable)) /\ exists ff_q_pvs_solve_append_resulttableentrypositive. dst_positive_code_solve_append_resulttable = ff_q_pvs_solve_append_resulttableentrypositive * S ((S (dst_index_solve_append_resulttable)) * dst_positive_scale_solve_append_resulttable) + (dst_positive_solve_append_resulttable))) /\ (((((exists ff_h_pvs_solve_append_resulttableentrynegative. ff_h_pvs_solve_append_resulttableentrynegative + S (dst_negative_solve_append_resulttable) = S ((S (dst_index_solve_append_resulttable)) * dst_negative_scale_solve_append_resulttable)) /\ exists ff_q_pvs_solve_append_resulttableentrynegative. dst_negative_code_solve_append_resulttable = ff_q_pvs_solve_append_resulttableentrynegative * S ((S (dst_index_solve_append_resulttable)) * dst_negative_scale_solve_append_resulttable) + (dst_negative_solve_append_resulttable))) /\ (exists ge_balance_positive_solve_append_resulttableentryvalue ge_balance_negative_solve_append_resulttableentryvalue. (((((dst_value_solve_append_resulttable) = 2 * (ge_balance_positive_solve_append_resulttableentryvalue) /\ (ge_balance_negative_solve_append_resulttableentryvalue) = 0) \/ exists ge_signed_half_solve_append_resulttableentryvaluedecode. (((dst_value_solve_append_resulttable) = 2 * ge_signed_half_solve_append_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resulttableentryvalue) = 0) /\ (ge_balance_negative_solve_append_resulttableentryvalue) = S ge_signed_half_solve_append_resulttableentryvaluedecode))) /\ ((dst_positive_solve_append_resulttable) + ge_balance_negative_solve_append_resulttableentryvalue = (dst_negative_solve_append_resulttable) + ge_balance_positive_solve_append_resulttableentryvalue))))))))) /\ (forall dc_input_solve_append_result dc_output_solve_append_result. ~(dc_input_solve_append_result=0) -> (exists pvs_le_gap_solve_append_resultdomain. pvs_le_gap_solve_append_resultdomain + (dc_input_solve_append_result) = (S N)) -> (exists dst_positive_code_solve_append_resultlookup dst_positive_scale_solve_append_resultlookup dst_negative_code_solve_append_resultlookup dst_negative_scale_solve_append_resultlookup dst_positive_solve_append_resultlookup dst_negative_solve_append_resultlookup. (((T) = (((((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) * S ((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) + ((dst_positive_scale_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))) * S ((((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) * S ((dst_positive_code_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup)) + ((dst_positive_scale_solve_append_resultlookup) + (dst_positive_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))) + ((((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup))) + (((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) * S ((dst_negative_code_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)) + ((dst_negative_scale_solve_append_resultlookup) + (dst_negative_scale_solve_append_resultlookup)))))) /\ (((((exists ff_h_pvs_solve_append_resultlookuppositive. ff_h_pvs_solve_append_resultlookuppositive + S (dst_positive_solve_append_resultlookup) = S ((S (dc_input_solve_append_result)) * dst_positive_scale_solve_append_resultlookup)) /\ exists ff_q_pvs_solve_append_resultlookuppositive. dst_positive_code_solve_append_resultlookup = ff_q_pvs_solve_append_resultlookuppositive * S ((S (dc_input_solve_append_result)) * dst_positive_scale_solve_append_resultlookup) + (dst_positive_solve_append_resultlookup))) /\ (((((exists ff_h_pvs_solve_append_resultlookupnegative. ff_h_pvs_solve_append_resultlookupnegative + S (dst_negative_solve_append_resultlookup) = S ((S (dc_input_solve_append_result)) * dst_negative_scale_solve_append_resultlookup)) /\ exists ff_q_pvs_solve_append_resultlookupnegative. dst_negative_code_solve_append_resultlookup = ff_q_pvs_solve_append_resultlookupnegative * S ((S (dc_input_solve_append_result)) * dst_negative_scale_solve_append_resultlookup) + (dst_negative_solve_append_resultlookup))) /\ (exists ge_balance_positive_solve_append_resultlookupvalue ge_balance_negative_solve_append_resultlookupvalue. (((((dc_output_solve_append_result) = 2 * (ge_balance_positive_solve_append_resultlookupvalue) /\ (ge_balance_negative_solve_append_resultlookupvalue) = 0) \/ exists ge_signed_half_solve_append_resultlookupvaluedecode. (((dc_output_solve_append_result) = 2 * ge_signed_half_solve_append_resultlookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultlookupvalue) = 0) /\ (ge_balance_negative_solve_append_resultlookupvalue) = S ge_signed_half_solve_append_resultlookupvaluedecode))) /\ ((dst_positive_solve_append_resultlookup) + ge_balance_negative_solve_append_resultlookupvalue = (dst_negative_solve_append_resultlookup) + ge_balance_positive_solve_append_resultlookupvalue))))))))) -> (((~((dc_input_solve_append_result)=0)) /\ (exists dc_mask_solve_append_resultvalue. ((((exists dst_positive_code_solve_append_resultvaluemasktable dst_positive_scale_solve_append_resultvaluemasktable dst_negative_code_solve_append_resultvaluemasktable dst_negative_scale_solve_append_resultvaluemasktable. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) * S ((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) + ((dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))) * S ((((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) * S ((dst_positive_code_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable)) + ((dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))) + ((((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable))) + (((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) * S ((dst_negative_code_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)) + ((dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_scale_solve_append_resultvaluemasktable)))))) /\ (forall dst_index_solve_append_resultvaluemasktable. (exists pvs_le_gap_solve_append_resultvaluemasktabledomain. pvs_le_gap_solve_append_resultvaluemasktabledomain + (dst_index_solve_append_resultvaluemasktable) = (dc_input_solve_append_result)) -> exists dst_positive_solve_append_resultvaluemasktable dst_negative_solve_append_resultvaluemasktable dst_value_solve_append_resultvaluemasktable. ((((exists ff_h_pvs_solve_append_resultvaluemasktableentrypositive. ff_h_pvs_solve_append_resultvaluemasktableentrypositive + S (dst_positive_solve_append_resultvaluemasktable) = S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_positive_scale_solve_append_resultvaluemasktable)) /\ exists ff_q_pvs_solve_append_resultvaluemasktableentrypositive. dst_positive_code_solve_append_resultvaluemasktable = ff_q_pvs_solve_append_resultvaluemasktableentrypositive * S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_positive_scale_solve_append_resultvaluemasktable) + (dst_positive_solve_append_resultvaluemasktable))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasktableentrynegative. ff_h_pvs_solve_append_resultvaluemasktableentrynegative + S (dst_negative_solve_append_resultvaluemasktable) = S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_negative_scale_solve_append_resultvaluemasktable)) /\ exists ff_q_pvs_solve_append_resultvaluemasktableentrynegative. dst_negative_code_solve_append_resultvaluemasktable = ff_q_pvs_solve_append_resultvaluemasktableentrynegative * S ((S (dst_index_solve_append_resultvaluemasktable)) * dst_negative_scale_solve_append_resultvaluemasktable) + (dst_negative_solve_append_resultvaluemasktable))) /\ (exists ge_balance_positive_solve_append_resultvaluemasktableentryvalue ge_balance_negative_solve_append_resultvaluemasktableentryvalue. (((((dst_value_solve_append_resultvaluemasktable) = 2 * (ge_balance_positive_solve_append_resultvaluemasktableentryvalue) /\ (ge_balance_negative_solve_append_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode. (((dst_value_solve_append_resultvaluemasktable) = 2 * ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemasktableentryvalue) = S ge_signed_half_solve_append_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemasktable) + ge_balance_negative_solve_append_resultvaluemasktableentryvalue = (dst_negative_solve_append_resultvaluemasktable) + ge_balance_positive_solve_append_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_solve_append_resultvaluemask dc_value_solve_append_resultvaluemask. (exists pvs_le_gap_solve_append_resultvaluemaskdomain. pvs_le_gap_solve_append_resultvaluemaskdomain + (dc_index_solve_append_resultvaluemask) = (dc_input_solve_append_result)) -> (exists dst_positive_code_solve_append_resultvaluemasklookup dst_positive_scale_solve_append_resultvaluemasklookup dst_negative_code_solve_append_resultvaluemasklookup dst_negative_scale_solve_append_resultvaluemasklookup dst_positive_solve_append_resultvaluemasklookup dst_negative_solve_append_resultvaluemasklookup. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) * S ((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) + ((dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))) * S ((((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) * S ((dst_positive_code_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup)) + ((dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))) + ((((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup))) + (((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) * S ((dst_negative_code_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)) + ((dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_scale_solve_append_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasklookuppositive. ff_h_pvs_solve_append_resultvaluemasklookuppositive + S (dst_positive_solve_append_resultvaluemasklookup) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_append_resultvaluemasklookuppositive. dst_positive_code_solve_append_resultvaluemasklookup = ff_q_pvs_solve_append_resultvaluemasklookuppositive * S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemasklookup) + (dst_positive_solve_append_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemasklookupnegative. ff_h_pvs_solve_append_resultvaluemasklookupnegative + S (dst_negative_solve_append_resultvaluemasklookup) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemasklookup)) /\ exists ff_q_pvs_solve_append_resultvaluemasklookupnegative. dst_negative_code_solve_append_resultvaluemasklookup = ff_q_pvs_solve_append_resultvaluemasklookupnegative * S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemasklookup) + (dst_negative_solve_append_resultvaluemasklookup))) /\ (exists ge_balance_positive_solve_append_resultvaluemasklookupvalue ge_balance_negative_solve_append_resultvaluemasklookupvalue. (((((dc_value_solve_append_resultvaluemask) = 2 * (ge_balance_positive_solve_append_resultvaluemasklookupvalue) /\ (ge_balance_negative_solve_append_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemasklookupvaluedecode. (((dc_value_solve_append_resultvaluemask) = 2 * ge_signed_half_solve_append_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemasklookupvalue) = S ge_signed_half_solve_append_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemasklookup) + ge_balance_negative_solve_append_resultvaluemasklookupvalue = (dst_negative_solve_append_resultvaluemasklookup) + ge_balance_positive_solve_append_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_solve_append_resultvaluemask)=0)) /\ (exists dc_quotient_solve_append_resultvaluemaskentry dc_left_solve_append_resultvaluemaskentry dc_right_solve_append_resultvaluemaskentry. (((dc_input_solve_append_result)=(dc_index_solve_append_resultvaluemask)*dc_quotient_solve_append_resultvaluemaskentry) /\ (((exists dst_positive_code_solve_append_resultvaluemaskentryleft dst_positive_scale_solve_append_resultvaluemaskentryleft dst_negative_code_solve_append_resultvaluemaskentryleft dst_negative_scale_solve_append_resultvaluemaskentryleft dst_positive_solve_append_resultvaluemaskentryleft dst_negative_solve_append_resultvaluemaskentryleft. (((H) = (((((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))) * S ((((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_positive_code_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft)) + ((dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))) + ((((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft))) + (((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) * S ((dst_negative_code_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)) + ((dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_scale_solve_append_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryleftpositive. ff_h_pvs_solve_append_resultvaluemaskentryleftpositive + S (dst_positive_solve_append_resultvaluemaskentryleft) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryleftpositive. dst_positive_code_solve_append_resultvaluemaskentryleft = ff_q_pvs_solve_append_resultvaluemaskentryleftpositive * S ((S (dc_index_solve_append_resultvaluemask)) * dst_positive_scale_solve_append_resultvaluemaskentryleft) + (dst_positive_solve_append_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryleftnegative. ff_h_pvs_solve_append_resultvaluemaskentryleftnegative + S (dst_negative_solve_append_resultvaluemaskentryleft) = S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemaskentryleft)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryleftnegative. dst_negative_code_solve_append_resultvaluemaskentryleft = ff_q_pvs_solve_append_resultvaluemaskentryleftnegative * S ((S (dc_index_solve_append_resultvaluemask)) * dst_negative_scale_solve_append_resultvaluemaskentryleft) + (dst_negative_solve_append_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_solve_append_resultvaluemaskentryleftvalue ge_balance_negative_solve_append_resultvaluemaskentryleftvalue. (((((dc_left_solve_append_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_append_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_solve_append_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode. (((dc_left_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemaskentryleftvalue) = S ge_signed_half_solve_append_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemaskentryleft) + ge_balance_negative_solve_append_resultvaluemaskentryleftvalue = (dst_negative_solve_append_resultvaluemaskentryleft) + ge_balance_positive_solve_append_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_solve_append_resultvaluemaskentryright dst_positive_scale_solve_append_resultvaluemaskentryright dst_negative_code_solve_append_resultvaluemaskentryright dst_negative_scale_solve_append_resultvaluemaskentryright dst_positive_solve_append_resultvaluemaskentryright dst_negative_solve_append_resultvaluemaskentryright. (((F) = (((((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) * S ((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) + ((dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))) * S ((((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) * S ((dst_positive_code_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright)) + ((dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))) + ((((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright))) + (((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) * S ((dst_negative_code_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)) + ((dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_scale_solve_append_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryrightpositive. ff_h_pvs_solve_append_resultvaluemaskentryrightpositive + S (dst_positive_solve_append_resultvaluemaskentryright) = S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_positive_scale_solve_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryrightpositive. dst_positive_code_solve_append_resultvaluemaskentryright = ff_q_pvs_solve_append_resultvaluemaskentryrightpositive * S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_positive_scale_solve_append_resultvaluemaskentryright) + (dst_positive_solve_append_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_solve_append_resultvaluemaskentryrightnegative. ff_h_pvs_solve_append_resultvaluemaskentryrightnegative + S (dst_negative_solve_append_resultvaluemaskentryright) = S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_negative_scale_solve_append_resultvaluemaskentryright)) /\ exists ff_q_pvs_solve_append_resultvaluemaskentryrightnegative. dst_negative_code_solve_append_resultvaluemaskentryright = ff_q_pvs_solve_append_resultvaluemaskentryrightnegative * S ((S (dc_quotient_solve_append_resultvaluemaskentry)) * dst_negative_scale_solve_append_resultvaluemaskentryright) + (dst_negative_solve_append_resultvaluemaskentryright))) /\ (exists ge_balance_positive_solve_append_resultvaluemaskentryrightvalue ge_balance_negative_solve_append_resultvaluemaskentryrightvalue. (((((dc_right_solve_append_resultvaluemaskentry) = 2 * (ge_balance_positive_solve_append_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_solve_append_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode. (((dc_right_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_solve_append_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_solve_append_resultvaluemaskentryrightvalue) = S ge_signed_half_solve_append_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_solve_append_resultvaluemaskentryright) + ge_balance_negative_solve_append_resultvaluemaskentryrightvalue = (dst_negative_solve_append_resultvaluemaskentryright) + ge_balance_positive_solve_append_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_solve_append_resultvaluemaskentryproduct sto_an_solve_append_resultvaluemaskentryproduct sto_bp_solve_append_resultvaluemaskentryproduct sto_bn_solve_append_resultvaluemaskentryproduct sto_cp_solve_append_resultvaluemaskentryproduct sto_cn_solve_append_resultvaluemaskentryproduct. (((((dc_left_solve_append_resultvaluemaskentry) = 2 * (sto_ap_solve_append_resultvaluemaskentryproduct) /\ (sto_an_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductleft. (((dc_left_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductleft + 1 /\ (sto_ap_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_an_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductleft))) /\ ((((((dc_right_solve_append_resultvaluemaskentry) = 2 * (sto_bp_solve_append_resultvaluemaskentryproduct) /\ (sto_bn_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductright. (((dc_right_solve_append_resultvaluemaskentry) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductright + 1 /\ (sto_bp_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_bn_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductright))) /\ ((((((dc_value_solve_append_resultvaluemask) = 2 * (sto_cp_solve_append_resultvaluemaskentryproduct) /\ (sto_cn_solve_append_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_solve_append_resultvaluemaskentryproductoutput. (((dc_value_solve_append_resultvaluemask) = 2 * ge_signed_half_solve_append_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_solve_append_resultvaluemaskentryproduct) = 0) /\ (sto_cn_solve_append_resultvaluemaskentryproduct) = S ge_signed_half_solve_append_resultvaluemaskentryproductoutput))) /\ ((sto_ap_solve_append_resultvaluemaskentryproduct * sto_bp_solve_append_resultvaluemaskentryproduct + sto_an_solve_append_resultvaluemaskentryproduct * sto_bn_solve_append_resultvaluemaskentryproduct) + sto_cn_solve_append_resultvaluemaskentryproduct = (sto_ap_solve_append_resultvaluemaskentryproduct * sto_bn_solve_append_resultvaluemaskentryproduct + sto_an_solve_append_resultvaluemaskentryproduct * sto_bp_solve_append_resultvaluemaskentryproduct) + sto_cp_solve_append_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_solve_append_resultvaluemask)=0 \/ ~(exists pvs_factor_solve_append_resultvaluemaskentrynondivisor. (dc_input_solve_append_result) = (dc_index_solve_append_resultvaluemask) * pvs_factor_solve_append_resultvaluemaskentrynondivisor)) /\ ((dc_value_solve_append_resultvaluemask)=0))))))) /\ (exists dst_positive_code_solve_append_resultvaluefold dst_positive_scale_solve_append_resultvaluefold dst_negative_code_solve_append_resultvaluefold dst_negative_scale_solve_append_resultvaluefold dst_positive_sum_solve_append_resultvaluefold dst_negative_sum_solve_append_resultvaluefold. (((dc_mask_solve_append_resultvalue) = (((((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) * S ((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) + ((dst_positive_scale_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))) * S ((((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) * S ((dst_positive_code_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold)) + ((dst_positive_scale_solve_append_resultvaluefold) + (dst_positive_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))) + ((((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold))) + (((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) * S ((dst_negative_code_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)) + ((dst_negative_scale_solve_append_resultvaluefold) + (dst_negative_scale_solve_append_resultvaluefold)))))) /\ (((exists fs_u_dst_solve_append_resultvaluefoldpositive fs_v_dst_solve_append_resultvaluefoldpositive. ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_start. fs_h_dst_solve_append_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_start. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_terminal. fs_h_dst_solve_append_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_solve_append_resultvaluefold) = S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_terminal. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldpositive) + (dst_positive_sum_solve_append_resultvaluefold))) /\ forall fs_i_dst_solve_append_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_solve_append_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_solve_append_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps = S (dc_input_solve_append_result)) -> exists fs_a_dst_solve_append_resultvaluefoldpositive_body_steps fs_r_dst_solve_append_resultvaluefoldpositive_body_steps fs_s_dst_solve_append_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_summand. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_resultvaluefold)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_summand. dst_positive_code_solve_append_resultvaluefold = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * dst_positive_scale_solve_append_resultvaluefold) + (fs_a_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_partial. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_partial. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (fs_r_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_successor. fs_h_dst_solve_append_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_solve_append_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive)) /\ exists fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_successor. fs_u_dst_solve_append_resultvaluefoldpositive = fs_q_dst_solve_append_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_solve_append_resultvaluefoldpositive_body_steps)) * fs_v_dst_solve_append_resultvaluefoldpositive) + (fs_s_dst_solve_append_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_solve_append_resultvaluefoldpositive_body_steps = fs_r_dst_solve_append_resultvaluefoldpositive_body_steps + fs_a_dst_solve_append_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_solve_append_resultvaluefoldnegative fs_v_dst_solve_append_resultvaluefoldnegative. ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_start. fs_h_dst_solve_append_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_start. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_terminal. fs_h_dst_solve_append_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_solve_append_resultvaluefold) = S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_terminal. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_solve_append_result))) * fs_v_dst_solve_append_resultvaluefoldnegative) + (dst_negative_sum_solve_append_resultvaluefold))) /\ forall fs_i_dst_solve_append_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_solve_append_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_solve_append_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps = S (dc_input_solve_append_result)) -> exists fs_a_dst_solve_append_resultvaluefoldnegative_body_steps fs_r_dst_solve_append_resultvaluefoldnegative_body_steps fs_s_dst_solve_append_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_summand. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_resultvaluefold)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_summand. dst_negative_code_solve_append_resultvaluefold = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * dst_negative_scale_solve_append_resultvaluefold) + (fs_a_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_partial. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_partial. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (fs_r_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_successor. fs_h_dst_solve_append_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_solve_append_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative)) /\ exists fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_successor. fs_u_dst_solve_append_resultvaluefoldnegative = fs_q_dst_solve_append_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_solve_append_resultvaluefoldnegative_body_steps)) * fs_v_dst_solve_append_resultvaluefoldnegative) + (fs_s_dst_solve_append_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_solve_append_resultvaluefoldnegative_body_steps = fs_r_dst_solve_append_resultvaluefoldnegative_body_steps + fs_a_dst_solve_append_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_solve_append_resultvaluefoldresult ge_balance_negative_solve_append_resultvaluefoldresult. (((((dc_output_solve_append_result) = 2 * (ge_balance_positive_solve_append_resultvaluefoldresult) /\ (ge_balance_negative_solve_append_resultvaluefoldresult) = 0) \/ exists ge_signed_half_solve_append_resultvaluefoldresultdecode. (((dc_output_solve_append_result) = 2 * ge_signed_half_solve_append_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_solve_append_resultvaluefoldresult) = 0) /\ (ge_balance_negative_solve_append_resultvaluefoldresult) = S ge_signed_half_solve_append_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_solve_append_resultvaluefold) + ge_balance_negative_solve_append_resultvaluefoldresult = (dst_negative_sum_solve_append_resultvaluefold) + ge_balance_positive_solve_append_resultvaluefoldresult)))))))))))))))))))) /\ (forall dst_index_solve_append_preserved dst_first_solve_append_preserved dst_second_solve_append_preserved. (exists pvs_gap_solve_append_preservedbound. pvs_gap_solve_append_preservedbound + S (dst_index_solve_append_preserved) = (S N)) -> (exists dst_positive_code_solve_append_preservedfirst dst_positive_scale_solve_append_preservedfirst dst_negative_code_solve_append_preservedfirst dst_negative_scale_solve_append_preservedfirst dst_positive_solve_append_preservedfirst dst_negative_solve_append_preservedfirst. (((G) = (((((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) * S ((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) + ((dst_positive_scale_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))) * S ((((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) * S ((dst_positive_code_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst)) + ((dst_positive_scale_solve_append_preservedfirst) + (dst_positive_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))) + ((((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst))) + (((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) * S ((dst_negative_code_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)) + ((dst_negative_scale_solve_append_preservedfirst) + (dst_negative_scale_solve_append_preservedfirst)))))) /\ (((((exists ff_h_pvs_solve_append_preservedfirstpositive. ff_h_pvs_solve_append_preservedfirstpositive + S (dst_positive_solve_append_preservedfirst) = S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedfirst)) /\ exists ff_q_pvs_solve_append_preservedfirstpositive. dst_positive_code_solve_append_preservedfirst = ff_q_pvs_solve_append_preservedfirstpositive * S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedfirst) + (dst_positive_solve_append_preservedfirst))) /\ (((((exists ff_h_pvs_solve_append_preservedfirstnegative. ff_h_pvs_solve_append_preservedfirstnegative + S (dst_negative_solve_append_preservedfirst) = S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedfirst)) /\ exists ff_q_pvs_solve_append_preservedfirstnegative. dst_negative_code_solve_append_preservedfirst = ff_q_pvs_solve_append_preservedfirstnegative * S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedfirst) + (dst_negative_solve_append_preservedfirst))) /\ (exists ge_balance_positive_solve_append_preservedfirstvalue ge_balance_negative_solve_append_preservedfirstvalue. (((((dst_first_solve_append_preserved) = 2 * (ge_balance_positive_solve_append_preservedfirstvalue) /\ (ge_balance_negative_solve_append_preservedfirstvalue) = 0) \/ exists ge_signed_half_solve_append_preservedfirstvaluedecode. (((dst_first_solve_append_preserved) = 2 * ge_signed_half_solve_append_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_solve_append_preservedfirstvalue) = 0) /\ (ge_balance_negative_solve_append_preservedfirstvalue) = S ge_signed_half_solve_append_preservedfirstvaluedecode))) /\ ((dst_positive_solve_append_preservedfirst) + ge_balance_negative_solve_append_preservedfirstvalue = (dst_negative_solve_append_preservedfirst) + ge_balance_positive_solve_append_preservedfirstvalue))))))))) -> (exists dst_positive_code_solve_append_preservedsecond dst_positive_scale_solve_append_preservedsecond dst_negative_code_solve_append_preservedsecond dst_negative_scale_solve_append_preservedsecond dst_positive_solve_append_preservedsecond dst_negative_solve_append_preservedsecond. (((H) = (((((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) * S ((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) + ((dst_positive_scale_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))) * S ((((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) * S ((dst_positive_code_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond)) + ((dst_positive_scale_solve_append_preservedsecond) + (dst_positive_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))) + ((((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond))) + (((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) * S ((dst_negative_code_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)) + ((dst_negative_scale_solve_append_preservedsecond) + (dst_negative_scale_solve_append_preservedsecond)))))) /\ (((((exists ff_h_pvs_solve_append_preservedsecondpositive. ff_h_pvs_solve_append_preservedsecondpositive + S (dst_positive_solve_append_preservedsecond) = S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedsecond)) /\ exists ff_q_pvs_solve_append_preservedsecondpositive. dst_positive_code_solve_append_preservedsecond = ff_q_pvs_solve_append_preservedsecondpositive * S ((S (dst_index_solve_append_preserved)) * dst_positive_scale_solve_append_preservedsecond) + (dst_positive_solve_append_preservedsecond))) /\ (((((exists ff_h_pvs_solve_append_preservedsecondnegative. ff_h_pvs_solve_append_preservedsecondnegative + S (dst_negative_solve_append_preservedsecond) = S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedsecond)) /\ exists ff_q_pvs_solve_append_preservedsecondnegative. dst_negative_code_solve_append_preservedsecond = ff_q_pvs_solve_append_preservedsecondnegative * S ((S (dst_index_solve_append_preserved)) * dst_negative_scale_solve_append_preservedsecond) + (dst_negative_solve_append_preservedsecond))) /\ (exists ge_balance_positive_solve_append_preservedsecondvalue ge_balance_negative_solve_append_preservedsecondvalue. (((((dst_second_solve_append_preserved) = 2 * (ge_balance_positive_solve_append_preservedsecondvalue) /\ (ge_balance_negative_solve_append_preservedsecondvalue) = 0) \/ exists ge_signed_half_solve_append_preservedsecondvaluedecode. (((dst_second_solve_append_preserved) = 2 * ge_signed_half_solve_append_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_solve_append_preservedsecondvalue) = 0) /\ (ge_balance_negative_solve_append_preservedsecondvalue) = S ge_signed_half_solve_append_preservedsecondvaluedecode))) /\ ((dst_positive_solve_append_preservedsecond) + ge_balance_negative_solve_append_preservedsecondvalue = (dst_negative_solve_append_preservedsecond) + ge_balance_positive_solve_append_preservedsecondvalue))))))))) -> dst_first_solve_append_preserved = dst_second_solve_append_preserved))Complete tactic proof in conservative notation
All 134 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
134 script commands · 29 reading checkpoints · 7 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–10
02Separate the logical casesL11–13
03Establish hpL14–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution strict prefix exists.
- L14
have hp : ∃ M. ∃ r. DirichletPrefix(G,F,S N,N,M) ∧ SignedPrefixSum(M,S N,r)Definitions: DirichletPrefix(G,F,S N,N,M)SignedPrefixSum(M,S N,r)Original native command in the exact edition - L15
specialize dirichlet_convolution_strict_prefix_exists (S N) - L16
specialize dirichlet_convolution_strict_prefix_exists (N) - L17
specialize dirichlet_convolution_strict_prefix_exists (F) - L18
specialize dirichlet_convolution_strict_prefix_exists (G) - L19
apply dirichlet_convolution_strict_prefix_exists - L20
exact hF - L21
exact hc_left
04Separate the logical casesL22–24
05Establish heL25–32
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L25
have he : ∃ e. ArithAt(T,S N,e)Definitions: ArithAt(T,S N,e)Original native command in the exact edition - L26
specialize divisor_signed_table_lookup (S N) - L27
specialize divisor_signed_table_lookup (T) - L28
specialize divisor_signed_table_lookup (S N) - L29
apply divisor_signed_table_lookup - L30
exact hT - L31
specialize le_refl (S N) - L32
apply le_refl
06Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
cases he
07Establish hsL34–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet signed unit affine solve.
- L34
have hs : ∃ a. ∃ b. SignedMul(a,u,b) ∧ SignedAdd(x1,b,x2)Definitions: SignedMul(a,u,b)SignedAdd(x1,b,x2)Original native command in the exact edition - L35
specialize dirichlet_signed_unit_affine_solve (x1) - L36
specialize dirichlet_signed_unit_affine_solve (u) - L37
specialize dirichlet_signed_unit_affine_solve (x2) - L38
apply dirichlet_signed_unit_affine_solve - L39
exact hunit
08Separate the logical casesL40–42
09Establish hxL43–48
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table append.
- L43
have hx : ∃ H. ArithExtend(G,H,S N,x3)Definitions: ArithExtend(G,H,S N,x3)Original native command in the exact edition - L44
specialize arithmetic_signed_table_append (N) - L45
specialize arithmetic_signed_table_append (G) - L46
specialize arithmetic_signed_table_append (x3) - L47
apply arithmetic_signed_table_append - L48
exact hc_left
10Separate the logical casesL49–51
11Establish hlastL52–61
Establish this local claim before using it. It is not an additional assumption.
- L52
have hlast : DirichletSum(x5,F,S N,x2)Definitions: DirichletSum(x5,F,S N,x2)Original native command in the exact edition - L53
specialize dirichlet_convolution_first_input_append_step (N) - L54
specialize dirichlet_convolution_first_input_append_step (G) - L55
specialize dirichlet_convolution_first_input_append_step (F) - L56
specialize dirichlet_convolution_first_input_append_step (x) - L57
specialize dirichlet_convolution_first_input_append_step (x1) - L58
specialize dirichlet_convolution_first_input_append_step (x5) - L59
specialize dirichlet_convolution_first_input_append_step (x3) - L60
specialize dirichlet_convolution_first_input_append_step (u) - L61
specialize dirichlet_convolution_first_input_append_step (x4)
12Use earlier factsL62–69
Instantiate or apply named facts and discharge the corresponding proof obligations.
13Construct an explicit witnessL70–70
Supply the displayed value, then prove that it has the required property.
- L70
exists x5
14Separate the logical casesL71–72
15Use earlier factsL73–73
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L73
exact hx_witness_left
16Separate the logical casesL74–74
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L74
split
17Use earlier factsL75–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L75
exact hF
18Separate the logical casesL76–76
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L76
split
19Use earlier factsL77–77
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L77
exact hT
20Fix variables and assumptionsL78–82
21Establish hcaseL83–87
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
22Separate the logical casesL88–88
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L88
cases hcase
23Calculate and transport equalitiesL89–92
24Establish heqL93–102
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.
- L93
have heq : x2=z - L94
specialize divisor_signed_table_at_functional (T) - L95
specialize divisor_signed_table_at_functional (S N) - L96
specialize divisor_signed_table_at_functional (x2) - L97
specialize divisor_signed_table_at_functional (z) - L98
apply divisor_signed_table_at_functional - L99
exact he_witness - L100
exact hz - L101
rewrite heq at hlast - L102
rewrite heq at hlast
25Calculate and transport equalitiesL103–112
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
26Calculate and transport equalitiesL113–113
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L113
rewrite hcase_left
27Use earlier factsL114–123
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L114
exact hlast - L115
specialize dirichlet_convolution_first_input_append_preserves (G) - L116
specialize dirichlet_convolution_first_input_append_preserves (F) - L117
specialize dirichlet_convolution_first_input_append_preserves (x5) - L118
specialize dirichlet_convolution_first_input_append_preserves (S N) - L119
specialize dirichlet_convolution_first_input_append_preserves (x3) - L120
specialize dirichlet_convolution_first_input_append_preserves (n) - L121
specialize dirichlet_convolution_first_input_append_preserves (z) - L122
apply dirichlet_convolution_first_input_append_preserves - L123
exact hx_witness
28Use earlier factsL124–133
Instantiate or apply named facts and discharge the corresponding proof obligations.
29Use earlier factsL134–134
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L134
exact hx_witness_right_left
Original defined command ledger · 134 lines
- 0001
intro N - 0002
intro F - 0003
intro T - 0004
intro G - 0005
intro u - 0006
intro hF - 0007
intro hT - 0008
intro hu - 0009
intro hunit - 0010
intro hc - 0011
cases hc - 0012
cases hc_right - 0013
cases hc_right_right - 0014
have hp : ∃ M. ∃ r. DirichletPrefix(G,F,S N,N,M) ∧ SignedPrefixSum(M,S N,r) - 0015
specialize dirichlet_convolution_strict_prefix_exists (S N) - 0016
specialize dirichlet_convolution_strict_prefix_exists (N) - 0017
specialize dirichlet_convolution_strict_prefix_exists (F) - 0018
specialize dirichlet_convolution_strict_prefix_exists (G) - 0019
apply dirichlet_convolution_strict_prefix_exists - 0020
exact hF - 0021
exact hc_left - 0022
cases hp - 0023
cases hp_witness - 0024
cases hp_witness_witness - 0025
have he : ∃ e. ArithAt(T,S N,e) - 0026
specialize divisor_signed_table_lookup (S N) - 0027
specialize divisor_signed_table_lookup (T) - 0028
specialize divisor_signed_table_lookup (S N) - 0029
apply divisor_signed_table_lookup - 0030
exact hT - 0031
specialize le_refl (S N) - 0032
apply le_refl - 0033
cases he - 0034
have hs : ∃ a. ∃ b. SignedMul(a,u,b) ∧ SignedAdd(x1,b,x2) - 0035
specialize dirichlet_signed_unit_affine_solve (x1) - 0036
specialize dirichlet_signed_unit_affine_solve (u) - 0037
specialize dirichlet_signed_unit_affine_solve (x2) - 0038
apply dirichlet_signed_unit_affine_solve - 0039
exact hunit - 0040
cases hs - 0041
cases hs_witness - 0042
cases hs_witness_witness - 0043
have hx : ∃ H. ArithExtend(G,H,S N,x3) - 0044
specialize arithmetic_signed_table_append (N) - 0045
specialize arithmetic_signed_table_append (G) - 0046
specialize arithmetic_signed_table_append (x3) - 0047
apply arithmetic_signed_table_append - 0048
exact hc_left - 0049
cases hx - 0050
cases hx_witness - 0051
cases hx_witness_right - 0052
have hlast : DirichletSum(x5,F,S N,x2) - 0053
specialize dirichlet_convolution_first_input_append_step (N) - 0054
specialize dirichlet_convolution_first_input_append_step (G) - 0055
specialize dirichlet_convolution_first_input_append_step (F) - 0056
specialize dirichlet_convolution_first_input_append_step (x) - 0057
specialize dirichlet_convolution_first_input_append_step (x1) - 0058
specialize dirichlet_convolution_first_input_append_step (x5) - 0059
specialize dirichlet_convolution_first_input_append_step (x3) - 0060
specialize dirichlet_convolution_first_input_append_step (u) - 0061
specialize dirichlet_convolution_first_input_append_step (x4) - 0062
specialize dirichlet_convolution_first_input_append_step (x2) - 0063
apply dirichlet_convolution_first_input_append_step - 0064
exact hp_witness_witness_left - 0065
exact hp_witness_witness_right - 0066
exact hx_witness - 0067
exact hu - 0068
exact hs_witness_witness_left - 0069
exact hs_witness_witness_right - 0070
exists x5 - 0071
split - 0072
split - 0073
exact hx_witness_left - 0074
split - 0075
exact hF - 0076
split - 0077
exact hT - 0078
intro n - 0079
intro z - 0080
intro hn - 0081
intro hb - 0082
intro hz - 0083
have hcase : n = S N ∨ Lt(n,S N) - 0084
specialize le_eq_or_lt (n) - 0085
specialize le_eq_or_lt (S N) - 0086
apply le_eq_or_lt - 0087
exact hb - 0088
cases hcase - 0089
rewrite hcase_left at hz - 0090
rewrite hcase_left at hz - 0091
rewrite hcase_left at hz - 0092
rewrite hcase_left at hz - 0093
have heq : x2=z - 0094
specialize divisor_signed_table_at_functional (T) - 0095
specialize divisor_signed_table_at_functional (S N) - 0096
specialize divisor_signed_table_at_functional (x2) - 0097
specialize divisor_signed_table_at_functional (z) - 0098
apply divisor_signed_table_at_functional - 0099
exact he_witness - 0100
exact hz - 0101
rewrite heq at hlast - 0102
rewrite heq at hlast - 0103
rewrite hcase_left - 0104
rewrite hcase_left - 0105
rewrite hcase_left - 0106
rewrite hcase_left - 0107
rewrite hcase_left - 0108
rewrite hcase_left - 0109
rewrite hcase_left - 0110
rewrite hcase_left - 0111
rewrite hcase_left - 0112
rewrite hcase_left - 0113
rewrite hcase_left - 0114
exact hlast - 0115
specialize dirichlet_convolution_first_input_append_preserves (G) - 0116
specialize dirichlet_convolution_first_input_append_preserves (F) - 0117
specialize dirichlet_convolution_first_input_append_preserves (x5) - 0118
specialize dirichlet_convolution_first_input_append_preserves (S N) - 0119
specialize dirichlet_convolution_first_input_append_preserves (x3) - 0120
specialize dirichlet_convolution_first_input_append_preserves (n) - 0121
specialize dirichlet_convolution_first_input_append_preserves (z) - 0122
apply dirichlet_convolution_first_input_append_preserves - 0123
exact hx_witness - 0124
exact hcase_right - 0125
specialize hc_right_right_right (n) - 0126
specialize hc_right_right_right (z) - 0127
apply hc_right_right_right - 0128
exact hn - 0129
specialize le_of_succ_le_succ (n) - 0130
specialize le_of_succ_le_succ (N) - 0131
apply le_of_succ_le_succ - 0132
exact hcase_right - 0133
exact hz - 0134
exact hx_witness_right_left