DC0009

dirichlet_convolution_prefix_append

Append one actual product-or-zero entry by paired beta recoding, preserving every earlier canonical signed value.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. Full G009 multiplicative-function closure is now admitted in the separate Alpha-v32 multiplicative-convolution family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ n. ∀ l. ∀ M. ∀ z. DirichletPrefix(F,G,n,l,M) → DirichletEntry(F,G,n,S l,z) → ∃ x. DirichletPrefix(F,G,n,S l,x) ∧ ArithTableEqual(M,x,S l)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 2ArithTableEqual(F,G,l) · 2DirichletEntry(F,G,n,d,z) · 1DirichletPrefix(F,G,n,l,M) · 2Le(a,b) · 1Lt(a,b) · 1

Actual proof prerequisites

arithmetic_signed_table_append · checked external prerequisitele_eq_or_lt · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisite
Original expanded first-order statement 
forall F G n l M z. (((exists dst_positive_code_append_sourcetable dst_positive_scale_append_sourcetable dst_negative_code_append_sourcetable dst_negative_scale_append_sourcetable. (((M) = (((((dst_positive_code_append_sourcetable) + (dst_positive_scale_append_sourcetable)) * S ((dst_positive_code_append_sourcetable) + (dst_positive_scale_append_sourcetable)) + ((dst_positive_scale_append_sourcetable) + (dst_positive_scale_append_sourcetable))) + (((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) * S ((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) + ((dst_negative_scale_append_sourcetable) + (dst_negative_scale_append_sourcetable)))) * S ((((dst_positive_code_append_sourcetable) + (dst_positive_scale_append_sourcetable)) * S ((dst_positive_code_append_sourcetable) + (dst_positive_scale_append_sourcetable)) + ((dst_positive_scale_append_sourcetable) + (dst_positive_scale_append_sourcetable))) + (((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) * S ((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) + ((dst_negative_scale_append_sourcetable) + (dst_negative_scale_append_sourcetable)))) + ((((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) * S ((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) + ((dst_negative_scale_append_sourcetable) + (dst_negative_scale_append_sourcetable))) + (((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) * S ((dst_negative_code_append_sourcetable) + (dst_negative_scale_append_sourcetable)) + ((dst_negative_scale_append_sourcetable) + (dst_negative_scale_append_sourcetable)))))) /\ (forall dst_index_append_sourcetable. (exists pvs_le_gap_append_sourcetabledomain. pvs_le_gap_append_sourcetabledomain + (dst_index_append_sourcetable) = (l)) -> exists dst_positive_append_sourcetable dst_negative_append_sourcetable dst_value_append_sourcetable. ((((exists ff_h_pvs_append_sourcetableentrypositive. ff_h_pvs_append_sourcetableentrypositive + S (dst_positive_append_sourcetable) = S ((S (dst_index_append_sourcetable)) * dst_positive_scale_append_sourcetable)) /\ exists ff_q_pvs_append_sourcetableentrypositive. dst_positive_code_append_sourcetable = ff_q_pvs_append_sourcetableentrypositive * S ((S (dst_index_append_sourcetable)) * dst_positive_scale_append_sourcetable) + (dst_positive_append_sourcetable))) /\ (((((exists ff_h_pvs_append_sourcetableentrynegative. ff_h_pvs_append_sourcetableentrynegative + S (dst_negative_append_sourcetable) = S ((S (dst_index_append_sourcetable)) * dst_negative_scale_append_sourcetable)) /\ exists ff_q_pvs_append_sourcetableentrynegative. dst_negative_code_append_sourcetable = ff_q_pvs_append_sourcetableentrynegative * S ((S (dst_index_append_sourcetable)) * dst_negative_scale_append_sourcetable) + (dst_negative_append_sourcetable))) /\ (exists ge_balance_positive_append_sourcetableentryvalue ge_balance_negative_append_sourcetableentryvalue. (((((dst_value_append_sourcetable) = 2 * (ge_balance_positive_append_sourcetableentryvalue) /\ (ge_balance_negative_append_sourcetableentryvalue) = 0) \/ exists ge_signed_half_append_sourcetableentryvaluedecode. (((dst_value_append_sourcetable) = 2 * ge_signed_half_append_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_append_sourcetableentryvalue) = 0) /\ (ge_balance_negative_append_sourcetableentryvalue) = S ge_signed_half_append_sourcetableentryvaluedecode))) /\ ((dst_positive_append_sourcetable) + ge_balance_negative_append_sourcetableentryvalue = (dst_negative_append_sourcetable) + ge_balance_positive_append_sourcetableentryvalue))))))))) /\ (forall dc_index_append_source dc_value_append_source. (exists pvs_le_gap_append_sourcedomain. pvs_le_gap_append_sourcedomain + (dc_index_append_source) = (l)) -> (exists dst_positive_code_append_sourcelookup dst_positive_scale_append_sourcelookup dst_negative_code_append_sourcelookup dst_negative_scale_append_sourcelookup dst_positive_append_sourcelookup dst_negative_append_sourcelookup. (((M) = (((((dst_positive_code_append_sourcelookup) + (dst_positive_scale_append_sourcelookup)) * S ((dst_positive_code_append_sourcelookup) + (dst_positive_scale_append_sourcelookup)) + ((dst_positive_scale_append_sourcelookup) + (dst_positive_scale_append_sourcelookup))) + (((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) * S ((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) + ((dst_negative_scale_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)))) * S ((((dst_positive_code_append_sourcelookup) + (dst_positive_scale_append_sourcelookup)) * S ((dst_positive_code_append_sourcelookup) + (dst_positive_scale_append_sourcelookup)) + ((dst_positive_scale_append_sourcelookup) + (dst_positive_scale_append_sourcelookup))) + (((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) * S ((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) + ((dst_negative_scale_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)))) + ((((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) * S ((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) + ((dst_negative_scale_append_sourcelookup) + (dst_negative_scale_append_sourcelookup))) + (((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) * S ((dst_negative_code_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)) + ((dst_negative_scale_append_sourcelookup) + (dst_negative_scale_append_sourcelookup)))))) /\ (((((exists ff_h_pvs_append_sourcelookuppositive. ff_h_pvs_append_sourcelookuppositive + S (dst_positive_append_sourcelookup) = S ((S (dc_index_append_source)) * dst_positive_scale_append_sourcelookup)) /\ exists ff_q_pvs_append_sourcelookuppositive. dst_positive_code_append_sourcelookup = ff_q_pvs_append_sourcelookuppositive * S ((S (dc_index_append_source)) * dst_positive_scale_append_sourcelookup) + (dst_positive_append_sourcelookup))) /\ (((((exists ff_h_pvs_append_sourcelookupnegative. ff_h_pvs_append_sourcelookupnegative + S (dst_negative_append_sourcelookup) = S ((S (dc_index_append_source)) * dst_negative_scale_append_sourcelookup)) /\ exists ff_q_pvs_append_sourcelookupnegative. dst_negative_code_append_sourcelookup = ff_q_pvs_append_sourcelookupnegative * S ((S (dc_index_append_source)) * dst_negative_scale_append_sourcelookup) + (dst_negative_append_sourcelookup))) /\ (exists ge_balance_positive_append_sourcelookupvalue ge_balance_negative_append_sourcelookupvalue. (((((dc_value_append_source) = 2 * (ge_balance_positive_append_sourcelookupvalue) /\ (ge_balance_negative_append_sourcelookupvalue) = 0) \/ exists ge_signed_half_append_sourcelookupvaluedecode. (((dc_value_append_source) = 2 * ge_signed_half_append_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_append_sourcelookupvalue) = 0) /\ (ge_balance_negative_append_sourcelookupvalue) = S ge_signed_half_append_sourcelookupvaluedecode))) /\ ((dst_positive_append_sourcelookup) + ge_balance_negative_append_sourcelookupvalue = (dst_negative_append_sourcelookup) + ge_balance_positive_append_sourcelookupvalue))))))))) -> ((((~((dc_index_append_source)=0)) /\ (exists dc_quotient_append_sourceentry dc_left_append_sourceentry dc_right_append_sourceentry. (((n)=(dc_index_append_source)*dc_quotient_append_sourceentry) /\ (((exists dst_positive_code_append_sourceentryleft dst_positive_scale_append_sourceentryleft dst_negative_code_append_sourceentryleft dst_negative_scale_append_sourceentryleft dst_positive_append_sourceentryleft dst_negative_append_sourceentryleft. (((F) = (((((dst_positive_code_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft)) * S ((dst_positive_code_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft)) + ((dst_positive_scale_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft))) + (((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) * S ((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) + ((dst_negative_scale_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)))) * S ((((dst_positive_code_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft)) * S ((dst_positive_code_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft)) + ((dst_positive_scale_append_sourceentryleft) + (dst_positive_scale_append_sourceentryleft))) + (((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) * S ((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) + ((dst_negative_scale_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)))) + ((((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) * S ((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) + ((dst_negative_scale_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft))) + (((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) * S ((dst_negative_code_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)) + ((dst_negative_scale_append_sourceentryleft) + (dst_negative_scale_append_sourceentryleft)))))) /\ (((((exists ff_h_pvs_append_sourceentryleftpositive. ff_h_pvs_append_sourceentryleftpositive + S (dst_positive_append_sourceentryleft) = S ((S (dc_index_append_source)) * dst_positive_scale_append_sourceentryleft)) /\ exists ff_q_pvs_append_sourceentryleftpositive. dst_positive_code_append_sourceentryleft = ff_q_pvs_append_sourceentryleftpositive * S ((S (dc_index_append_source)) * dst_positive_scale_append_sourceentryleft) + (dst_positive_append_sourceentryleft))) /\ (((((exists ff_h_pvs_append_sourceentryleftnegative. ff_h_pvs_append_sourceentryleftnegative + S (dst_negative_append_sourceentryleft) = S ((S (dc_index_append_source)) * dst_negative_scale_append_sourceentryleft)) /\ exists ff_q_pvs_append_sourceentryleftnegative. dst_negative_code_append_sourceentryleft = ff_q_pvs_append_sourceentryleftnegative * S ((S (dc_index_append_source)) * dst_negative_scale_append_sourceentryleft) + (dst_negative_append_sourceentryleft))) /\ (exists ge_balance_positive_append_sourceentryleftvalue ge_balance_negative_append_sourceentryleftvalue. (((((dc_left_append_sourceentry) = 2 * (ge_balance_positive_append_sourceentryleftvalue) /\ (ge_balance_negative_append_sourceentryleftvalue) = 0) \/ exists ge_signed_half_append_sourceentryleftvaluedecode. (((dc_left_append_sourceentry) = 2 * ge_signed_half_append_sourceentryleftvaluedecode + 1 /\ (ge_balance_positive_append_sourceentryleftvalue) = 0) /\ (ge_balance_negative_append_sourceentryleftvalue) = S ge_signed_half_append_sourceentryleftvaluedecode))) /\ ((dst_positive_append_sourceentryleft) + ge_balance_negative_append_sourceentryleftvalue = (dst_negative_append_sourceentryleft) + ge_balance_positive_append_sourceentryleftvalue))))))))) /\ (((exists dst_positive_code_append_sourceentryright dst_positive_scale_append_sourceentryright dst_negative_code_append_sourceentryright dst_negative_scale_append_sourceentryright dst_positive_append_sourceentryright dst_negative_append_sourceentryright. (((G) = (((((dst_positive_code_append_sourceentryright) + (dst_positive_scale_append_sourceentryright)) * S ((dst_positive_code_append_sourceentryright) + (dst_positive_scale_append_sourceentryright)) + ((dst_positive_scale_append_sourceentryright) + (dst_positive_scale_append_sourceentryright))) + (((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) * S ((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) + ((dst_negative_scale_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)))) * S ((((dst_positive_code_append_sourceentryright) + (dst_positive_scale_append_sourceentryright)) * S ((dst_positive_code_append_sourceentryright) + (dst_positive_scale_append_sourceentryright)) + ((dst_positive_scale_append_sourceentryright) + (dst_positive_scale_append_sourceentryright))) + (((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) * S ((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) + ((dst_negative_scale_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)))) + ((((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) * S ((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) + ((dst_negative_scale_append_sourceentryright) + (dst_negative_scale_append_sourceentryright))) + (((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) * S ((dst_negative_code_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)) + ((dst_negative_scale_append_sourceentryright) + (dst_negative_scale_append_sourceentryright)))))) /\ (((((exists ff_h_pvs_append_sourceentryrightpositive. ff_h_pvs_append_sourceentryrightpositive + S (dst_positive_append_sourceentryright) = S ((S (dc_quotient_append_sourceentry)) * dst_positive_scale_append_sourceentryright)) /\ exists ff_q_pvs_append_sourceentryrightpositive. dst_positive_code_append_sourceentryright = ff_q_pvs_append_sourceentryrightpositive * S ((S (dc_quotient_append_sourceentry)) * dst_positive_scale_append_sourceentryright) + (dst_positive_append_sourceentryright))) /\ (((((exists ff_h_pvs_append_sourceentryrightnegative. ff_h_pvs_append_sourceentryrightnegative + S (dst_negative_append_sourceentryright) = S ((S (dc_quotient_append_sourceentry)) * dst_negative_scale_append_sourceentryright)) /\ exists ff_q_pvs_append_sourceentryrightnegative. dst_negative_code_append_sourceentryright = ff_q_pvs_append_sourceentryrightnegative * S ((S (dc_quotient_append_sourceentry)) * dst_negative_scale_append_sourceentryright) + (dst_negative_append_sourceentryright))) /\ (exists ge_balance_positive_append_sourceentryrightvalue ge_balance_negative_append_sourceentryrightvalue. (((((dc_right_append_sourceentry) = 2 * (ge_balance_positive_append_sourceentryrightvalue) /\ (ge_balance_negative_append_sourceentryrightvalue) = 0) \/ exists ge_signed_half_append_sourceentryrightvaluedecode. (((dc_right_append_sourceentry) = 2 * ge_signed_half_append_sourceentryrightvaluedecode + 1 /\ (ge_balance_positive_append_sourceentryrightvalue) = 0) /\ (ge_balance_negative_append_sourceentryrightvalue) = S ge_signed_half_append_sourceentryrightvaluedecode))) /\ ((dst_positive_append_sourceentryright) + ge_balance_negative_append_sourceentryrightvalue = (dst_negative_append_sourceentryright) + ge_balance_positive_append_sourceentryrightvalue))))))))) /\ (exists sto_ap_append_sourceentryproduct sto_an_append_sourceentryproduct sto_bp_append_sourceentryproduct sto_bn_append_sourceentryproduct sto_cp_append_sourceentryproduct sto_cn_append_sourceentryproduct. (((((dc_left_append_sourceentry) = 2 * (sto_ap_append_sourceentryproduct) /\ (sto_an_append_sourceentryproduct) = 0) \/ exists ge_signed_half_append_sourceentryproductleft. (((dc_left_append_sourceentry) = 2 * ge_signed_half_append_sourceentryproductleft + 1 /\ (sto_ap_append_sourceentryproduct) = 0) /\ (sto_an_append_sourceentryproduct) = S ge_signed_half_append_sourceentryproductleft))) /\ ((((((dc_right_append_sourceentry) = 2 * (sto_bp_append_sourceentryproduct) /\ (sto_bn_append_sourceentryproduct) = 0) \/ exists ge_signed_half_append_sourceentryproductright. (((dc_right_append_sourceentry) = 2 * ge_signed_half_append_sourceentryproductright + 1 /\ (sto_bp_append_sourceentryproduct) = 0) /\ (sto_bn_append_sourceentryproduct) = S ge_signed_half_append_sourceentryproductright))) /\ ((((((dc_value_append_source) = 2 * (sto_cp_append_sourceentryproduct) /\ (sto_cn_append_sourceentryproduct) = 0) \/ exists ge_signed_half_append_sourceentryproductoutput. (((dc_value_append_source) = 2 * ge_signed_half_append_sourceentryproductoutput + 1 /\ (sto_cp_append_sourceentryproduct) = 0) /\ (sto_cn_append_sourceentryproduct) = S ge_signed_half_append_sourceentryproductoutput))) /\ ((sto_ap_append_sourceentryproduct * sto_bp_append_sourceentryproduct + sto_an_append_sourceentryproduct * sto_bn_append_sourceentryproduct) + sto_cn_append_sourceentryproduct = (sto_ap_append_sourceentryproduct * sto_bn_append_sourceentryproduct + sto_an_append_sourceentryproduct * sto_bp_append_sourceentryproduct) + sto_cp_append_sourceentryproduct))))))))))))))) \/ ((((dc_index_append_source)=0 \/ ~(exists pvs_factor_append_sourceentrynondivisor. (n) = (dc_index_append_source) * pvs_factor_append_sourceentrynondivisor)) /\ ((dc_value_append_source)=0))))))) -> ((((~((S l)=0)) /\ (exists dc_quotient_append_last dc_left_append_last dc_right_append_last. (((n)=(S l)*dc_quotient_append_last) /\ (((exists dst_positive_code_append_lastleft dst_positive_scale_append_lastleft dst_negative_code_append_lastleft dst_negative_scale_append_lastleft dst_positive_append_lastleft dst_negative_append_lastleft. (((F) = (((((dst_positive_code_append_lastleft) + (dst_positive_scale_append_lastleft)) * S ((dst_positive_code_append_lastleft) + (dst_positive_scale_append_lastleft)) + ((dst_positive_scale_append_lastleft) + (dst_positive_scale_append_lastleft))) + (((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) * S ((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) + ((dst_negative_scale_append_lastleft) + (dst_negative_scale_append_lastleft)))) * S ((((dst_positive_code_append_lastleft) + (dst_positive_scale_append_lastleft)) * S ((dst_positive_code_append_lastleft) + (dst_positive_scale_append_lastleft)) + ((dst_positive_scale_append_lastleft) + (dst_positive_scale_append_lastleft))) + (((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) * S ((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) + ((dst_negative_scale_append_lastleft) + (dst_negative_scale_append_lastleft)))) + ((((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) * S ((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) + ((dst_negative_scale_append_lastleft) + (dst_negative_scale_append_lastleft))) + (((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) * S ((dst_negative_code_append_lastleft) + (dst_negative_scale_append_lastleft)) + ((dst_negative_scale_append_lastleft) + (dst_negative_scale_append_lastleft)))))) /\ (((((exists ff_h_pvs_append_lastleftpositive. ff_h_pvs_append_lastleftpositive + S (dst_positive_append_lastleft) = S ((S (S l)) * dst_positive_scale_append_lastleft)) /\ exists ff_q_pvs_append_lastleftpositive. dst_positive_code_append_lastleft = ff_q_pvs_append_lastleftpositive * S ((S (S l)) * dst_positive_scale_append_lastleft) + (dst_positive_append_lastleft))) /\ (((((exists ff_h_pvs_append_lastleftnegative. ff_h_pvs_append_lastleftnegative + S (dst_negative_append_lastleft) = S ((S (S l)) * dst_negative_scale_append_lastleft)) /\ exists ff_q_pvs_append_lastleftnegative. dst_negative_code_append_lastleft = ff_q_pvs_append_lastleftnegative * S ((S (S l)) * dst_negative_scale_append_lastleft) + (dst_negative_append_lastleft))) /\ (exists ge_balance_positive_append_lastleftvalue ge_balance_negative_append_lastleftvalue. (((((dc_left_append_last) = 2 * (ge_balance_positive_append_lastleftvalue) /\ (ge_balance_negative_append_lastleftvalue) = 0) \/ exists ge_signed_half_append_lastleftvaluedecode. (((dc_left_append_last) = 2 * ge_signed_half_append_lastleftvaluedecode + 1 /\ (ge_balance_positive_append_lastleftvalue) = 0) /\ (ge_balance_negative_append_lastleftvalue) = S ge_signed_half_append_lastleftvaluedecode))) /\ ((dst_positive_append_lastleft) + ge_balance_negative_append_lastleftvalue = (dst_negative_append_lastleft) + ge_balance_positive_append_lastleftvalue))))))))) /\ (((exists dst_positive_code_append_lastright dst_positive_scale_append_lastright dst_negative_code_append_lastright dst_negative_scale_append_lastright dst_positive_append_lastright dst_negative_append_lastright. (((G) = (((((dst_positive_code_append_lastright) + (dst_positive_scale_append_lastright)) * S ((dst_positive_code_append_lastright) + (dst_positive_scale_append_lastright)) + ((dst_positive_scale_append_lastright) + (dst_positive_scale_append_lastright))) + (((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) * S ((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) + ((dst_negative_scale_append_lastright) + (dst_negative_scale_append_lastright)))) * S ((((dst_positive_code_append_lastright) + (dst_positive_scale_append_lastright)) * S ((dst_positive_code_append_lastright) + (dst_positive_scale_append_lastright)) + ((dst_positive_scale_append_lastright) + (dst_positive_scale_append_lastright))) + (((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) * S ((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) + ((dst_negative_scale_append_lastright) + (dst_negative_scale_append_lastright)))) + ((((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) * S ((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) + ((dst_negative_scale_append_lastright) + (dst_negative_scale_append_lastright))) + (((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) * S ((dst_negative_code_append_lastright) + (dst_negative_scale_append_lastright)) + ((dst_negative_scale_append_lastright) + (dst_negative_scale_append_lastright)))))) /\ (((((exists ff_h_pvs_append_lastrightpositive. ff_h_pvs_append_lastrightpositive + S (dst_positive_append_lastright) = S ((S (dc_quotient_append_last)) * dst_positive_scale_append_lastright)) /\ exists ff_q_pvs_append_lastrightpositive. dst_positive_code_append_lastright = ff_q_pvs_append_lastrightpositive * S ((S (dc_quotient_append_last)) * dst_positive_scale_append_lastright) + (dst_positive_append_lastright))) /\ (((((exists ff_h_pvs_append_lastrightnegative. ff_h_pvs_append_lastrightnegative + S (dst_negative_append_lastright) = S ((S (dc_quotient_append_last)) * dst_negative_scale_append_lastright)) /\ exists ff_q_pvs_append_lastrightnegative. dst_negative_code_append_lastright = ff_q_pvs_append_lastrightnegative * S ((S (dc_quotient_append_last)) * dst_negative_scale_append_lastright) + (dst_negative_append_lastright))) /\ (exists ge_balance_positive_append_lastrightvalue ge_balance_negative_append_lastrightvalue. (((((dc_right_append_last) = 2 * (ge_balance_positive_append_lastrightvalue) /\ (ge_balance_negative_append_lastrightvalue) = 0) \/ exists ge_signed_half_append_lastrightvaluedecode. (((dc_right_append_last) = 2 * ge_signed_half_append_lastrightvaluedecode + 1 /\ (ge_balance_positive_append_lastrightvalue) = 0) /\ (ge_balance_negative_append_lastrightvalue) = S ge_signed_half_append_lastrightvaluedecode))) /\ ((dst_positive_append_lastright) + ge_balance_negative_append_lastrightvalue = (dst_negative_append_lastright) + ge_balance_positive_append_lastrightvalue))))))))) /\ (exists sto_ap_append_lastproduct sto_an_append_lastproduct sto_bp_append_lastproduct sto_bn_append_lastproduct sto_cp_append_lastproduct sto_cn_append_lastproduct. (((((dc_left_append_last) = 2 * (sto_ap_append_lastproduct) /\ (sto_an_append_lastproduct) = 0) \/ exists ge_signed_half_append_lastproductleft. (((dc_left_append_last) = 2 * ge_signed_half_append_lastproductleft + 1 /\ (sto_ap_append_lastproduct) = 0) /\ (sto_an_append_lastproduct) = S ge_signed_half_append_lastproductleft))) /\ ((((((dc_right_append_last) = 2 * (sto_bp_append_lastproduct) /\ (sto_bn_append_lastproduct) = 0) \/ exists ge_signed_half_append_lastproductright. (((dc_right_append_last) = 2 * ge_signed_half_append_lastproductright + 1 /\ (sto_bp_append_lastproduct) = 0) /\ (sto_bn_append_lastproduct) = S ge_signed_half_append_lastproductright))) /\ ((((((z) = 2 * (sto_cp_append_lastproduct) /\ (sto_cn_append_lastproduct) = 0) \/ exists ge_signed_half_append_lastproductoutput. (((z) = 2 * ge_signed_half_append_lastproductoutput + 1 /\ (sto_cp_append_lastproduct) = 0) /\ (sto_cn_append_lastproduct) = S ge_signed_half_append_lastproductoutput))) /\ ((sto_ap_append_lastproduct * sto_bp_append_lastproduct + sto_an_append_lastproduct * sto_bn_append_lastproduct) + sto_cn_append_lastproduct = (sto_ap_append_lastproduct * sto_bn_append_lastproduct + sto_an_append_lastproduct * sto_bp_append_lastproduct) + sto_cp_append_lastproduct))))))))))))))) \/ ((((S l)=0 \/ ~(exists pvs_factor_append_lastnondivisor. (n) = (S l) * pvs_factor_append_lastnondivisor)) /\ ((z)=0)))) -> exists H. (((exists dst_positive_code_append_resulttable dst_positive_scale_append_resulttable dst_negative_code_append_resulttable dst_negative_scale_append_resulttable. (((H) = (((((dst_positive_code_append_resulttable) + (dst_positive_scale_append_resulttable)) * S ((dst_positive_code_append_resulttable) + (dst_positive_scale_append_resulttable)) + ((dst_positive_scale_append_resulttable) + (dst_positive_scale_append_resulttable))) + (((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) * S ((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) + ((dst_negative_scale_append_resulttable) + (dst_negative_scale_append_resulttable)))) * S ((((dst_positive_code_append_resulttable) + (dst_positive_scale_append_resulttable)) * S ((dst_positive_code_append_resulttable) + (dst_positive_scale_append_resulttable)) + ((dst_positive_scale_append_resulttable) + (dst_positive_scale_append_resulttable))) + (((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) * S ((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) + ((dst_negative_scale_append_resulttable) + (dst_negative_scale_append_resulttable)))) + ((((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) * S ((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) + ((dst_negative_scale_append_resulttable) + (dst_negative_scale_append_resulttable))) + (((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) * S ((dst_negative_code_append_resulttable) + (dst_negative_scale_append_resulttable)) + ((dst_negative_scale_append_resulttable) + (dst_negative_scale_append_resulttable)))))) /\ (forall dst_index_append_resulttable. (exists pvs_le_gap_append_resulttabledomain. pvs_le_gap_append_resulttabledomain + (dst_index_append_resulttable) = (S l)) -> exists dst_positive_append_resulttable dst_negative_append_resulttable dst_value_append_resulttable. ((((exists ff_h_pvs_append_resulttableentrypositive. ff_h_pvs_append_resulttableentrypositive + S (dst_positive_append_resulttable) = S ((S (dst_index_append_resulttable)) * dst_positive_scale_append_resulttable)) /\ exists ff_q_pvs_append_resulttableentrypositive. dst_positive_code_append_resulttable = ff_q_pvs_append_resulttableentrypositive * S ((S (dst_index_append_resulttable)) * dst_positive_scale_append_resulttable) + (dst_positive_append_resulttable))) /\ (((((exists ff_h_pvs_append_resulttableentrynegative. ff_h_pvs_append_resulttableentrynegative + S (dst_negative_append_resulttable) = S ((S (dst_index_append_resulttable)) * dst_negative_scale_append_resulttable)) /\ exists ff_q_pvs_append_resulttableentrynegative. dst_negative_code_append_resulttable = ff_q_pvs_append_resulttableentrynegative * S ((S (dst_index_append_resulttable)) * dst_negative_scale_append_resulttable) + (dst_negative_append_resulttable))) /\ (exists ge_balance_positive_append_resulttableentryvalue ge_balance_negative_append_resulttableentryvalue. (((((dst_value_append_resulttable) = 2 * (ge_balance_positive_append_resulttableentryvalue) /\ (ge_balance_negative_append_resulttableentryvalue) = 0) \/ exists ge_signed_half_append_resulttableentryvaluedecode. (((dst_value_append_resulttable) = 2 * ge_signed_half_append_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_append_resulttableentryvalue) = 0) /\ (ge_balance_negative_append_resulttableentryvalue) = S ge_signed_half_append_resulttableentryvaluedecode))) /\ ((dst_positive_append_resulttable) + ge_balance_negative_append_resulttableentryvalue = (dst_negative_append_resulttable) + ge_balance_positive_append_resulttableentryvalue))))))))) /\ (forall dc_index_append_result dc_value_append_result. (exists pvs_le_gap_append_resultdomain. pvs_le_gap_append_resultdomain + (dc_index_append_result) = (S l)) -> (exists dst_positive_code_append_resultlookup dst_positive_scale_append_resultlookup dst_negative_code_append_resultlookup dst_negative_scale_append_resultlookup dst_positive_append_resultlookup dst_negative_append_resultlookup. (((H) = (((((dst_positive_code_append_resultlookup) + (dst_positive_scale_append_resultlookup)) * S ((dst_positive_code_append_resultlookup) + (dst_positive_scale_append_resultlookup)) + ((dst_positive_scale_append_resultlookup) + (dst_positive_scale_append_resultlookup))) + (((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) * S ((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) + ((dst_negative_scale_append_resultlookup) + (dst_negative_scale_append_resultlookup)))) * S ((((dst_positive_code_append_resultlookup) + (dst_positive_scale_append_resultlookup)) * S ((dst_positive_code_append_resultlookup) + (dst_positive_scale_append_resultlookup)) + ((dst_positive_scale_append_resultlookup) + (dst_positive_scale_append_resultlookup))) + (((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) * S ((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) + ((dst_negative_scale_append_resultlookup) + (dst_negative_scale_append_resultlookup)))) + ((((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) * S ((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) + ((dst_negative_scale_append_resultlookup) + (dst_negative_scale_append_resultlookup))) + (((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) * S ((dst_negative_code_append_resultlookup) + (dst_negative_scale_append_resultlookup)) + ((dst_negative_scale_append_resultlookup) + (dst_negative_scale_append_resultlookup)))))) /\ (((((exists ff_h_pvs_append_resultlookuppositive. ff_h_pvs_append_resultlookuppositive + S (dst_positive_append_resultlookup) = S ((S (dc_index_append_result)) * dst_positive_scale_append_resultlookup)) /\ exists ff_q_pvs_append_resultlookuppositive. dst_positive_code_append_resultlookup = ff_q_pvs_append_resultlookuppositive * S ((S (dc_index_append_result)) * dst_positive_scale_append_resultlookup) + (dst_positive_append_resultlookup))) /\ (((((exists ff_h_pvs_append_resultlookupnegative. ff_h_pvs_append_resultlookupnegative + S (dst_negative_append_resultlookup) = S ((S (dc_index_append_result)) * dst_negative_scale_append_resultlookup)) /\ exists ff_q_pvs_append_resultlookupnegative. dst_negative_code_append_resultlookup = ff_q_pvs_append_resultlookupnegative * S ((S (dc_index_append_result)) * dst_negative_scale_append_resultlookup) + (dst_negative_append_resultlookup))) /\ (exists ge_balance_positive_append_resultlookupvalue ge_balance_negative_append_resultlookupvalue. (((((dc_value_append_result) = 2 * (ge_balance_positive_append_resultlookupvalue) /\ (ge_balance_negative_append_resultlookupvalue) = 0) \/ exists ge_signed_half_append_resultlookupvaluedecode. (((dc_value_append_result) = 2 * ge_signed_half_append_resultlookupvaluedecode + 1 /\ (ge_balance_positive_append_resultlookupvalue) = 0) /\ (ge_balance_negative_append_resultlookupvalue) = S ge_signed_half_append_resultlookupvaluedecode))) /\ ((dst_positive_append_resultlookup) + ge_balance_negative_append_resultlookupvalue = (dst_negative_append_resultlookup) + ge_balance_positive_append_resultlookupvalue))))))))) -> ((((~((dc_index_append_result)=0)) /\ (exists dc_quotient_append_resultentry dc_left_append_resultentry dc_right_append_resultentry. (((n)=(dc_index_append_result)*dc_quotient_append_resultentry) /\ (((exists dst_positive_code_append_resultentryleft dst_positive_scale_append_resultentryleft dst_negative_code_append_resultentryleft dst_negative_scale_append_resultentryleft dst_positive_append_resultentryleft dst_negative_append_resultentryleft. (((F) = (((((dst_positive_code_append_resultentryleft) + (dst_positive_scale_append_resultentryleft)) * S ((dst_positive_code_append_resultentryleft) + (dst_positive_scale_append_resultentryleft)) + ((dst_positive_scale_append_resultentryleft) + (dst_positive_scale_append_resultentryleft))) + (((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) * S ((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) + ((dst_negative_scale_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)))) * S ((((dst_positive_code_append_resultentryleft) + (dst_positive_scale_append_resultentryleft)) * S ((dst_positive_code_append_resultentryleft) + (dst_positive_scale_append_resultentryleft)) + ((dst_positive_scale_append_resultentryleft) + (dst_positive_scale_append_resultentryleft))) + (((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) * S ((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) + ((dst_negative_scale_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)))) + ((((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) * S ((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) + ((dst_negative_scale_append_resultentryleft) + (dst_negative_scale_append_resultentryleft))) + (((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) * S ((dst_negative_code_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)) + ((dst_negative_scale_append_resultentryleft) + (dst_negative_scale_append_resultentryleft)))))) /\ (((((exists ff_h_pvs_append_resultentryleftpositive. ff_h_pvs_append_resultentryleftpositive + S (dst_positive_append_resultentryleft) = S ((S (dc_index_append_result)) * dst_positive_scale_append_resultentryleft)) /\ exists ff_q_pvs_append_resultentryleftpositive. dst_positive_code_append_resultentryleft = ff_q_pvs_append_resultentryleftpositive * S ((S (dc_index_append_result)) * dst_positive_scale_append_resultentryleft) + (dst_positive_append_resultentryleft))) /\ (((((exists ff_h_pvs_append_resultentryleftnegative. ff_h_pvs_append_resultentryleftnegative + S (dst_negative_append_resultentryleft) = S ((S (dc_index_append_result)) * dst_negative_scale_append_resultentryleft)) /\ exists ff_q_pvs_append_resultentryleftnegative. dst_negative_code_append_resultentryleft = ff_q_pvs_append_resultentryleftnegative * S ((S (dc_index_append_result)) * dst_negative_scale_append_resultentryleft) + (dst_negative_append_resultentryleft))) /\ (exists ge_balance_positive_append_resultentryleftvalue ge_balance_negative_append_resultentryleftvalue. (((((dc_left_append_resultentry) = 2 * (ge_balance_positive_append_resultentryleftvalue) /\ (ge_balance_negative_append_resultentryleftvalue) = 0) \/ exists ge_signed_half_append_resultentryleftvaluedecode. (((dc_left_append_resultentry) = 2 * ge_signed_half_append_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_append_resultentryleftvalue) = 0) /\ (ge_balance_negative_append_resultentryleftvalue) = S ge_signed_half_append_resultentryleftvaluedecode))) /\ ((dst_positive_append_resultentryleft) + ge_balance_negative_append_resultentryleftvalue = (dst_negative_append_resultentryleft) + ge_balance_positive_append_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_append_resultentryright dst_positive_scale_append_resultentryright dst_negative_code_append_resultentryright dst_negative_scale_append_resultentryright dst_positive_append_resultentryright dst_negative_append_resultentryright. (((G) = (((((dst_positive_code_append_resultentryright) + (dst_positive_scale_append_resultentryright)) * S ((dst_positive_code_append_resultentryright) + (dst_positive_scale_append_resultentryright)) + ((dst_positive_scale_append_resultentryright) + (dst_positive_scale_append_resultentryright))) + (((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) * S ((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) + ((dst_negative_scale_append_resultentryright) + (dst_negative_scale_append_resultentryright)))) * S ((((dst_positive_code_append_resultentryright) + (dst_positive_scale_append_resultentryright)) * S ((dst_positive_code_append_resultentryright) + (dst_positive_scale_append_resultentryright)) + ((dst_positive_scale_append_resultentryright) + (dst_positive_scale_append_resultentryright))) + (((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) * S ((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) + ((dst_negative_scale_append_resultentryright) + (dst_negative_scale_append_resultentryright)))) + ((((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) * S ((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) + ((dst_negative_scale_append_resultentryright) + (dst_negative_scale_append_resultentryright))) + (((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) * S ((dst_negative_code_append_resultentryright) + (dst_negative_scale_append_resultentryright)) + ((dst_negative_scale_append_resultentryright) + (dst_negative_scale_append_resultentryright)))))) /\ (((((exists ff_h_pvs_append_resultentryrightpositive. ff_h_pvs_append_resultentryrightpositive + S (dst_positive_append_resultentryright) = S ((S (dc_quotient_append_resultentry)) * dst_positive_scale_append_resultentryright)) /\ exists ff_q_pvs_append_resultentryrightpositive. dst_positive_code_append_resultentryright = ff_q_pvs_append_resultentryrightpositive * S ((S (dc_quotient_append_resultentry)) * dst_positive_scale_append_resultentryright) + (dst_positive_append_resultentryright))) /\ (((((exists ff_h_pvs_append_resultentryrightnegative. ff_h_pvs_append_resultentryrightnegative + S (dst_negative_append_resultentryright) = S ((S (dc_quotient_append_resultentry)) * dst_negative_scale_append_resultentryright)) /\ exists ff_q_pvs_append_resultentryrightnegative. dst_negative_code_append_resultentryright = ff_q_pvs_append_resultentryrightnegative * S ((S (dc_quotient_append_resultentry)) * dst_negative_scale_append_resultentryright) + (dst_negative_append_resultentryright))) /\ (exists ge_balance_positive_append_resultentryrightvalue ge_balance_negative_append_resultentryrightvalue. (((((dc_right_append_resultentry) = 2 * (ge_balance_positive_append_resultentryrightvalue) /\ (ge_balance_negative_append_resultentryrightvalue) = 0) \/ exists ge_signed_half_append_resultentryrightvaluedecode. (((dc_right_append_resultentry) = 2 * ge_signed_half_append_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_append_resultentryrightvalue) = 0) /\ (ge_balance_negative_append_resultentryrightvalue) = S ge_signed_half_append_resultentryrightvaluedecode))) /\ ((dst_positive_append_resultentryright) + ge_balance_negative_append_resultentryrightvalue = (dst_negative_append_resultentryright) + ge_balance_positive_append_resultentryrightvalue))))))))) /\ (exists sto_ap_append_resultentryproduct sto_an_append_resultentryproduct sto_bp_append_resultentryproduct sto_bn_append_resultentryproduct sto_cp_append_resultentryproduct sto_cn_append_resultentryproduct. (((((dc_left_append_resultentry) = 2 * (sto_ap_append_resultentryproduct) /\ (sto_an_append_resultentryproduct) = 0) \/ exists ge_signed_half_append_resultentryproductleft. (((dc_left_append_resultentry) = 2 * ge_signed_half_append_resultentryproductleft + 1 /\ (sto_ap_append_resultentryproduct) = 0) /\ (sto_an_append_resultentryproduct) = S ge_signed_half_append_resultentryproductleft))) /\ ((((((dc_right_append_resultentry) = 2 * (sto_bp_append_resultentryproduct) /\ (sto_bn_append_resultentryproduct) = 0) \/ exists ge_signed_half_append_resultentryproductright. (((dc_right_append_resultentry) = 2 * ge_signed_half_append_resultentryproductright + 1 /\ (sto_bp_append_resultentryproduct) = 0) /\ (sto_bn_append_resultentryproduct) = S ge_signed_half_append_resultentryproductright))) /\ ((((((dc_value_append_result) = 2 * (sto_cp_append_resultentryproduct) /\ (sto_cn_append_resultentryproduct) = 0) \/ exists ge_signed_half_append_resultentryproductoutput. (((dc_value_append_result) = 2 * ge_signed_half_append_resultentryproductoutput + 1 /\ (sto_cp_append_resultentryproduct) = 0) /\ (sto_cn_append_resultentryproduct) = S ge_signed_half_append_resultentryproductoutput))) /\ ((sto_ap_append_resultentryproduct * sto_bp_append_resultentryproduct + sto_an_append_resultentryproduct * sto_bn_append_resultentryproduct) + sto_cn_append_resultentryproduct = (sto_ap_append_resultentryproduct * sto_bn_append_resultentryproduct + sto_an_append_resultentryproduct * sto_bp_append_resultentryproduct) + sto_cp_append_resultentryproduct))))))))))))))) \/ ((((dc_index_append_result)=0 \/ ~(exists pvs_factor_append_resultentrynondivisor. (n) = (dc_index_append_result) * pvs_factor_append_resultentrynondivisor)) /\ ((dc_value_append_result)=0))))))) /\ (forall dst_index_append_equal dst_first_append_equal dst_second_append_equal. (exists pvs_gap_append_equalbound. pvs_gap_append_equalbound + S (dst_index_append_equal) = (S l)) -> (exists dst_positive_code_append_equalfirst dst_positive_scale_append_equalfirst dst_negative_code_append_equalfirst dst_negative_scale_append_equalfirst dst_positive_append_equalfirst dst_negative_append_equalfirst. (((M) = (((((dst_positive_code_append_equalfirst) + (dst_positive_scale_append_equalfirst)) * S ((dst_positive_code_append_equalfirst) + (dst_positive_scale_append_equalfirst)) + ((dst_positive_scale_append_equalfirst) + (dst_positive_scale_append_equalfirst))) + (((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) * S ((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) + ((dst_negative_scale_append_equalfirst) + (dst_negative_scale_append_equalfirst)))) * S ((((dst_positive_code_append_equalfirst) + (dst_positive_scale_append_equalfirst)) * S ((dst_positive_code_append_equalfirst) + (dst_positive_scale_append_equalfirst)) + ((dst_positive_scale_append_equalfirst) + (dst_positive_scale_append_equalfirst))) + (((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) * S ((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) + ((dst_negative_scale_append_equalfirst) + (dst_negative_scale_append_equalfirst)))) + ((((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) * S ((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) + ((dst_negative_scale_append_equalfirst) + (dst_negative_scale_append_equalfirst))) + (((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) * S ((dst_negative_code_append_equalfirst) + (dst_negative_scale_append_equalfirst)) + ((dst_negative_scale_append_equalfirst) + (dst_negative_scale_append_equalfirst)))))) /\ (((((exists ff_h_pvs_append_equalfirstpositive. ff_h_pvs_append_equalfirstpositive + S (dst_positive_append_equalfirst) = S ((S (dst_index_append_equal)) * dst_positive_scale_append_equalfirst)) /\ exists ff_q_pvs_append_equalfirstpositive. dst_positive_code_append_equalfirst = ff_q_pvs_append_equalfirstpositive * S ((S (dst_index_append_equal)) * dst_positive_scale_append_equalfirst) + (dst_positive_append_equalfirst))) /\ (((((exists ff_h_pvs_append_equalfirstnegative. ff_h_pvs_append_equalfirstnegative + S (dst_negative_append_equalfirst) = S ((S (dst_index_append_equal)) * dst_negative_scale_append_equalfirst)) /\ exists ff_q_pvs_append_equalfirstnegative. dst_negative_code_append_equalfirst = ff_q_pvs_append_equalfirstnegative * S ((S (dst_index_append_equal)) * dst_negative_scale_append_equalfirst) + (dst_negative_append_equalfirst))) /\ (exists ge_balance_positive_append_equalfirstvalue ge_balance_negative_append_equalfirstvalue. (((((dst_first_append_equal) = 2 * (ge_balance_positive_append_equalfirstvalue) /\ (ge_balance_negative_append_equalfirstvalue) = 0) \/ exists ge_signed_half_append_equalfirstvaluedecode. (((dst_first_append_equal) = 2 * ge_signed_half_append_equalfirstvaluedecode + 1 /\ (ge_balance_positive_append_equalfirstvalue) = 0) /\ (ge_balance_negative_append_equalfirstvalue) = S ge_signed_half_append_equalfirstvaluedecode))) /\ ((dst_positive_append_equalfirst) + ge_balance_negative_append_equalfirstvalue = (dst_negative_append_equalfirst) + ge_balance_positive_append_equalfirstvalue))))))))) -> (exists dst_positive_code_append_equalsecond dst_positive_scale_append_equalsecond dst_negative_code_append_equalsecond dst_negative_scale_append_equalsecond dst_positive_append_equalsecond dst_negative_append_equalsecond. (((H) = (((((dst_positive_code_append_equalsecond) + (dst_positive_scale_append_equalsecond)) * S ((dst_positive_code_append_equalsecond) + (dst_positive_scale_append_equalsecond)) + ((dst_positive_scale_append_equalsecond) + (dst_positive_scale_append_equalsecond))) + (((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) * S ((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) + ((dst_negative_scale_append_equalsecond) + (dst_negative_scale_append_equalsecond)))) * S ((((dst_positive_code_append_equalsecond) + (dst_positive_scale_append_equalsecond)) * S ((dst_positive_code_append_equalsecond) + (dst_positive_scale_append_equalsecond)) + ((dst_positive_scale_append_equalsecond) + (dst_positive_scale_append_equalsecond))) + (((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) * S ((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) + ((dst_negative_scale_append_equalsecond) + (dst_negative_scale_append_equalsecond)))) + ((((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) * S ((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) + ((dst_negative_scale_append_equalsecond) + (dst_negative_scale_append_equalsecond))) + (((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) * S ((dst_negative_code_append_equalsecond) + (dst_negative_scale_append_equalsecond)) + ((dst_negative_scale_append_equalsecond) + (dst_negative_scale_append_equalsecond)))))) /\ (((((exists ff_h_pvs_append_equalsecondpositive. ff_h_pvs_append_equalsecondpositive + S (dst_positive_append_equalsecond) = S ((S (dst_index_append_equal)) * dst_positive_scale_append_equalsecond)) /\ exists ff_q_pvs_append_equalsecondpositive. dst_positive_code_append_equalsecond = ff_q_pvs_append_equalsecondpositive * S ((S (dst_index_append_equal)) * dst_positive_scale_append_equalsecond) + (dst_positive_append_equalsecond))) /\ (((((exists ff_h_pvs_append_equalsecondnegative. ff_h_pvs_append_equalsecondnegative + S (dst_negative_append_equalsecond) = S ((S (dst_index_append_equal)) * dst_negative_scale_append_equalsecond)) /\ exists ff_q_pvs_append_equalsecondnegative. dst_negative_code_append_equalsecond = ff_q_pvs_append_equalsecondnegative * S ((S (dst_index_append_equal)) * dst_negative_scale_append_equalsecond) + (dst_negative_append_equalsecond))) /\ (exists ge_balance_positive_append_equalsecondvalue ge_balance_negative_append_equalsecondvalue. (((((dst_second_append_equal) = 2 * (ge_balance_positive_append_equalsecondvalue) /\ (ge_balance_negative_append_equalsecondvalue) = 0) \/ exists ge_signed_half_append_equalsecondvaluedecode. (((dst_second_append_equal) = 2 * ge_signed_half_append_equalsecondvaluedecode + 1 /\ (ge_balance_positive_append_equalsecondvalue) = 0) /\ (ge_balance_negative_append_equalsecondvalue) = S ge_signed_half_append_equalsecondvaluedecode))) /\ ((dst_positive_append_equalsecond) + ge_balance_negative_append_equalsecondvalue = (dst_negative_append_equalsecond) + ge_balance_positive_append_equalsecondvalue))))))))) -> dst_first_append_equal = dst_second_append_equal)

Complete tactic proof in conservative notation

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

85 script commands · 19 reading checkpoints · 6 local claims

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

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

01Fix variables and assumptionsL1–8

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro l
  5. L5
    intro M
  6. L6
    intro z
  7. L7
    intro hm
  8. L8
    intro hz
02Separate the logical casesL9–9

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

  1. L9
    cases hm
03Establish hextL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table append.

  1. L10
    have hext : ∃ H. ArithTable(S l,H) ∧ (ArithTableEqual(M,H,S l) ∧ ArithAt(H,S l,z))Definitions: ArithTable(S l,H)ArithTableEqual(M,H,S l)ArithAt(H,S l,z)Original native command in the exact edition
  2. L11
    specialize arithmetic_signed_table_append (l)
  3. L12
    specialize arithmetic_signed_table_append (M)
  4. L13
    specialize arithmetic_signed_table_append (z)
  5. L14
    apply arithmetic_signed_table_append
  6. L15
    exact hm_left
04Separate the logical casesL16–18

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

  1. L16
    cases hext
  2. L17
    cases hext_witness
  3. L18
    cases hext_witness_right
05Construct an explicit witnessL19–19

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

  1. L19
    exists x
06Separate the logical casesL20–21

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

  1. L20
    split
  2. L21
    split
07Use earlier factsL22–22

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

  1. L22
    exact hext_witness_left
08Fix variables and assumptionsL23–26

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

  1. L23
    intro d
  2. L24
    intro u
  3. L25
    intro hd
  4. L26
    intro hu
09Establish hcL27–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L27
    have hc : d = S l ∨ Lt(d,S l)Definitions: Lt(d,S l)Original native command in the exact edition
  2. L28
    specialize le_eq_or_lt (d)
  3. L29
    specialize le_eq_or_lt (S l)
  4. L30
    apply le_eq_or_lt
  5. L31
    exact hd
10Separate the logical casesL32–32

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

  1. L32
    cases hc
11Calculate and transport equalitiesL33–36

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

  1. L33
    rewrite hc_left at hu
  2. L34
    rewrite hc_left at hu
  3. L35
    rewrite hc_left at hu
  4. L36
    rewrite hc_left at hu
12Establish heqL37–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L37
    have heq : z=u
  2. L38
    specialize divisor_signed_table_at_functional (x)
  3. L39
    specialize divisor_signed_table_at_functional (S l)
  4. L40
    specialize divisor_signed_table_at_functional (z)
  5. L41
    specialize divisor_signed_table_at_functional (u)
  6. L42
    apply divisor_signed_table_at_functional
  7. L43
    exact hext_witness_right_right
  8. L44
    exact hu
  9. L45
    rewrite heq at hz
  10. L46
    rewrite heq at hz
13Calculate and transport equalitiesL47–55

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

  1. L47
    rewrite heq at hz
  2. L48
    rewrite hc_left
  3. L49
    rewrite hc_left
  4. L50
    rewrite hc_left
  5. L51
    rewrite hc_left
  6. L52
    rewrite hc_left
  7. L53
    rewrite hc_left
  8. L54
    rewrite hc_left
  9. L55
    rewrite hc_left
14Use earlier factsL56–56

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

  1. L56
    exact hz
15Establish hboundL57–61

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L57
    have hbound : Le(d,l)Definitions: Le(d,l)Original native command in the exact edition
  2. L58
    specialize le_of_succ_le_succ (d)
  3. L59
    specialize le_of_succ_le_succ (l)
  4. L60
    apply le_of_succ_le_succ
  5. L61
    exact hc_right
16Establish hvL62–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.

  1. L62
    have hv : ∃ v. ArithAt(M,d,v)Definitions: ArithAt(M,d,v)Original native command in the exact edition
  2. L63
    specialize divisor_signed_table_lookup (l)
  3. L64
    specialize divisor_signed_table_lookup (M)
  4. L65
    specialize divisor_signed_table_lookup (d)
  5. L66
    apply divisor_signed_table_lookup
  6. L67
    exact hm_left
  7. L68
    exact hbound
17Separate the logical casesL69–69

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

  1. L69
    cases hv
18Establish heqL70–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hext witness right left.

  1. L70
    have heq : x1=u
  2. L71
    specialize hext_witness_right_left (d)
  3. L72
    specialize hext_witness_right_left (x1)
  4. L73
    specialize hext_witness_right_left (u)
  5. L74
    apply hext_witness_right_left
  6. L75
    exact hc_right
  7. L76
    exact hv_witness
  8. L77
    exact hu
  9. L78
    rewrite heq at hv_witness
  10. L79
    rewrite heq at hv_witness
19Use earlier factsL80–85

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

  1. L80
    specialize hm_right (d)
  2. L81
    specialize hm_right (u)
  3. L82
    apply hm_right
  4. L83
    exact hbound
  5. L84
    exact hv_witness
  6. L85
    exact hext_witness_right_left

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro l
  5. 0005intro M
  6. 0006intro z
  7. 0007intro hm
  8. 0008intro hz
  9. 0009cases hm
  10. 0010have hext : ∃ H. ArithTable(S l,H) ∧ (ArithTableEqual(M,H,S l) ∧ ArithAt(H,S l,z))
  11. 0011specialize arithmetic_signed_table_append (l)
  12. 0012specialize arithmetic_signed_table_append (M)
  13. 0013specialize arithmetic_signed_table_append (z)
  14. 0014apply arithmetic_signed_table_append
  15. 0015exact hm_left
  16. 0016cases hext
  17. 0017cases hext_witness
  18. 0018cases hext_witness_right
  19. 0019exists x
  20. 0020split
  21. 0021split
  22. 0022exact hext_witness_left
  23. 0023intro d
  24. 0024intro u
  25. 0025intro hd
  26. 0026intro hu
  27. 0027have hc : d = S l ∨ Lt(d,S l)
  28. 0028specialize le_eq_or_lt (d)
  29. 0029specialize le_eq_or_lt (S l)
  30. 0030apply le_eq_or_lt
  31. 0031exact hd
  32. 0032cases hc
  33. 0033rewrite hc_left at hu
  34. 0034rewrite hc_left at hu
  35. 0035rewrite hc_left at hu
  36. 0036rewrite hc_left at hu
  37. 0037have heq : z=u
  38. 0038specialize divisor_signed_table_at_functional (x)
  39. 0039specialize divisor_signed_table_at_functional (S l)
  40. 0040specialize divisor_signed_table_at_functional (z)
  41. 0041specialize divisor_signed_table_at_functional (u)
  42. 0042apply divisor_signed_table_at_functional
  43. 0043exact hext_witness_right_right
  44. 0044exact hu
  45. 0045rewrite heq at hz
  46. 0046rewrite heq at hz
  47. 0047rewrite heq at hz
  48. 0048rewrite hc_left
  49. 0049rewrite hc_left
  50. 0050rewrite hc_left
  51. 0051rewrite hc_left
  52. 0052rewrite hc_left
  53. 0053rewrite hc_left
  54. 0054rewrite hc_left
  55. 0055rewrite hc_left
  56. 0056exact hz
  57. 0057have hbound : Le(d,l)
  58. 0058specialize le_of_succ_le_succ (d)
  59. 0059specialize le_of_succ_le_succ (l)
  60. 0060apply le_of_succ_le_succ
  61. 0061exact hc_right
  62. 0062have hv : ∃ v. ArithAt(M,d,v)
  63. 0063specialize divisor_signed_table_lookup (l)
  64. 0064specialize divisor_signed_table_lookup (M)
  65. 0065specialize divisor_signed_table_lookup (d)
  66. 0066apply divisor_signed_table_lookup
  67. 0067exact hm_left
  68. 0068exact hbound
  69. 0069cases hv
  70. 0070have heq : x1=u
  71. 0071specialize hext_witness_right_left (d)
  72. 0072specialize hext_witness_right_left (x1)
  73. 0073specialize hext_witness_right_left (u)
  74. 0074apply hext_witness_right_left
  75. 0075exact hc_right
  76. 0076exact hv_witness
  77. 0077exact hu
  78. 0078rewrite heq at hv_witness
  79. 0079rewrite heq at hv_witness
  80. 0080specialize hm_right (d)
  81. 0081specialize hm_right (u)
  82. 0082apply hm_right
  83. 0083exact hbound
  84. 0084exact hv_witness
  85. 0085exact hext_witness_right_left