DC0021

dirichlet_convolution_prefix_complement_reindex

The actual complement beta map pulls one constructed convolution-summand prefix into the factor-swapped prefix.

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. ∀ P. ∀ Q. ∀ r. ∀ s. ¬n = 0 → DirichletPrefix(F,G,n,n,P) → DirichletPrefix(G,F,n,n,Q) → DivisorComplementPrefix(n,r,s,S n) → ArithReindex(P,Q,r,s,S n)

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

Definition DAG

ArithReindex(F,G,r,s,l) · 1DivisorComplement(n,d,q) · 1DivisorComplementPrefix(n,b,c,l) · 1DirichletPrefix(F,G,n,l,M) · 2Le(a,b) · 2

Actual proof prerequisites

le_of_succ_le_succ · checked external prerequisitedivisor_complement_prefix_lookup · checked external prerequisitedivisor_complement_bounded · checked external prerequisitedirichlet_convolution_prefix_value_from_entrydirichlet_convolution_entry_complementdirichlet_convolution_prefix_lookup
Original expanded first-order statement 
forall F G n P Q r s. ~(n=0) -> (((exists dst_positive_code_pullback_firsttable dst_positive_scale_pullback_firsttable dst_negative_code_pullback_firsttable dst_negative_scale_pullback_firsttable. (((P) = (((((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) * S ((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) + ((dst_positive_scale_pullback_firsttable) + (dst_positive_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))) * S ((((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) * S ((dst_positive_code_pullback_firsttable) + (dst_positive_scale_pullback_firsttable)) + ((dst_positive_scale_pullback_firsttable) + (dst_positive_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))) + ((((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable))) + (((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) * S ((dst_negative_code_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)) + ((dst_negative_scale_pullback_firsttable) + (dst_negative_scale_pullback_firsttable)))))) /\ (forall dst_index_pullback_firsttable. (exists pvs_le_gap_pullback_firsttabledomain. pvs_le_gap_pullback_firsttabledomain + (dst_index_pullback_firsttable) = (n)) -> exists dst_positive_pullback_firsttable dst_negative_pullback_firsttable dst_value_pullback_firsttable. ((((exists ff_h_pvs_pullback_firsttableentrypositive. ff_h_pvs_pullback_firsttableentrypositive + S (dst_positive_pullback_firsttable) = S ((S (dst_index_pullback_firsttable)) * dst_positive_scale_pullback_firsttable)) /\ exists ff_q_pvs_pullback_firsttableentrypositive. dst_positive_code_pullback_firsttable = ff_q_pvs_pullback_firsttableentrypositive * S ((S (dst_index_pullback_firsttable)) * dst_positive_scale_pullback_firsttable) + (dst_positive_pullback_firsttable))) /\ (((((exists ff_h_pvs_pullback_firsttableentrynegative. ff_h_pvs_pullback_firsttableentrynegative + S (dst_negative_pullback_firsttable) = S ((S (dst_index_pullback_firsttable)) * dst_negative_scale_pullback_firsttable)) /\ exists ff_q_pvs_pullback_firsttableentrynegative. dst_negative_code_pullback_firsttable = ff_q_pvs_pullback_firsttableentrynegative * S ((S (dst_index_pullback_firsttable)) * dst_negative_scale_pullback_firsttable) + (dst_negative_pullback_firsttable))) /\ (exists ge_balance_positive_pullback_firsttableentryvalue ge_balance_negative_pullback_firsttableentryvalue. (((((dst_value_pullback_firsttable) = 2 * (ge_balance_positive_pullback_firsttableentryvalue) /\ (ge_balance_negative_pullback_firsttableentryvalue) = 0) \/ exists ge_signed_half_pullback_firsttableentryvaluedecode. (((dst_value_pullback_firsttable) = 2 * ge_signed_half_pullback_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_pullback_firsttableentryvalue) = 0) /\ (ge_balance_negative_pullback_firsttableentryvalue) = S ge_signed_half_pullback_firsttableentryvaluedecode))) /\ ((dst_positive_pullback_firsttable) + ge_balance_negative_pullback_firsttableentryvalue = (dst_negative_pullback_firsttable) + ge_balance_positive_pullback_firsttableentryvalue))))))))) /\ (forall dc_index_pullback_first dc_value_pullback_first. (exists pvs_le_gap_pullback_firstdomain. pvs_le_gap_pullback_firstdomain + (dc_index_pullback_first) = (n)) -> (exists dst_positive_code_pullback_firstlookup dst_positive_scale_pullback_firstlookup dst_negative_code_pullback_firstlookup dst_negative_scale_pullback_firstlookup dst_positive_pullback_firstlookup dst_negative_pullback_firstlookup. (((P) = (((((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) * S ((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) + ((dst_positive_scale_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))) * S ((((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) * S ((dst_positive_code_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup)) + ((dst_positive_scale_pullback_firstlookup) + (dst_positive_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))) + ((((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup))) + (((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) * S ((dst_negative_code_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)) + ((dst_negative_scale_pullback_firstlookup) + (dst_negative_scale_pullback_firstlookup)))))) /\ (((((exists ff_h_pvs_pullback_firstlookuppositive. ff_h_pvs_pullback_firstlookuppositive + S (dst_positive_pullback_firstlookup) = S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstlookup)) /\ exists ff_q_pvs_pullback_firstlookuppositive. dst_positive_code_pullback_firstlookup = ff_q_pvs_pullback_firstlookuppositive * S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstlookup) + (dst_positive_pullback_firstlookup))) /\ (((((exists ff_h_pvs_pullback_firstlookupnegative. ff_h_pvs_pullback_firstlookupnegative + S (dst_negative_pullback_firstlookup) = S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstlookup)) /\ exists ff_q_pvs_pullback_firstlookupnegative. dst_negative_code_pullback_firstlookup = ff_q_pvs_pullback_firstlookupnegative * S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstlookup) + (dst_negative_pullback_firstlookup))) /\ (exists ge_balance_positive_pullback_firstlookupvalue ge_balance_negative_pullback_firstlookupvalue. (((((dc_value_pullback_first) = 2 * (ge_balance_positive_pullback_firstlookupvalue) /\ (ge_balance_negative_pullback_firstlookupvalue) = 0) \/ exists ge_signed_half_pullback_firstlookupvaluedecode. (((dc_value_pullback_first) = 2 * ge_signed_half_pullback_firstlookupvaluedecode + 1 /\ (ge_balance_positive_pullback_firstlookupvalue) = 0) /\ (ge_balance_negative_pullback_firstlookupvalue) = S ge_signed_half_pullback_firstlookupvaluedecode))) /\ ((dst_positive_pullback_firstlookup) + ge_balance_negative_pullback_firstlookupvalue = (dst_negative_pullback_firstlookup) + ge_balance_positive_pullback_firstlookupvalue))))))))) -> ((((~((dc_index_pullback_first)=0)) /\ (exists dc_quotient_pullback_firstentry dc_left_pullback_firstentry dc_right_pullback_firstentry. (((n)=(dc_index_pullback_first)*dc_quotient_pullback_firstentry) /\ (((exists dst_positive_code_pullback_firstentryleft dst_positive_scale_pullback_firstentryleft dst_negative_code_pullback_firstentryleft dst_negative_scale_pullback_firstentryleft dst_positive_pullback_firstentryleft dst_negative_pullback_firstentryleft. (((F) = (((((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) * S ((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) + ((dst_positive_scale_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))) * S ((((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) * S ((dst_positive_code_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft)) + ((dst_positive_scale_pullback_firstentryleft) + (dst_positive_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))) + ((((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft))) + (((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) * S ((dst_negative_code_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)) + ((dst_negative_scale_pullback_firstentryleft) + (dst_negative_scale_pullback_firstentryleft)))))) /\ (((((exists ff_h_pvs_pullback_firstentryleftpositive. ff_h_pvs_pullback_firstentryleftpositive + S (dst_positive_pullback_firstentryleft) = S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstentryleft)) /\ exists ff_q_pvs_pullback_firstentryleftpositive. dst_positive_code_pullback_firstentryleft = ff_q_pvs_pullback_firstentryleftpositive * S ((S (dc_index_pullback_first)) * dst_positive_scale_pullback_firstentryleft) + (dst_positive_pullback_firstentryleft))) /\ (((((exists ff_h_pvs_pullback_firstentryleftnegative. ff_h_pvs_pullback_firstentryleftnegative + S (dst_negative_pullback_firstentryleft) = S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstentryleft)) /\ exists ff_q_pvs_pullback_firstentryleftnegative. dst_negative_code_pullback_firstentryleft = ff_q_pvs_pullback_firstentryleftnegative * S ((S (dc_index_pullback_first)) * dst_negative_scale_pullback_firstentryleft) + (dst_negative_pullback_firstentryleft))) /\ (exists ge_balance_positive_pullback_firstentryleftvalue ge_balance_negative_pullback_firstentryleftvalue. (((((dc_left_pullback_firstentry) = 2 * (ge_balance_positive_pullback_firstentryleftvalue) /\ (ge_balance_negative_pullback_firstentryleftvalue) = 0) \/ exists ge_signed_half_pullback_firstentryleftvaluedecode. (((dc_left_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryleftvaluedecode + 1 /\ (ge_balance_positive_pullback_firstentryleftvalue) = 0) /\ (ge_balance_negative_pullback_firstentryleftvalue) = S ge_signed_half_pullback_firstentryleftvaluedecode))) /\ ((dst_positive_pullback_firstentryleft) + ge_balance_negative_pullback_firstentryleftvalue = (dst_negative_pullback_firstentryleft) + ge_balance_positive_pullback_firstentryleftvalue))))))))) /\ (((exists dst_positive_code_pullback_firstentryright dst_positive_scale_pullback_firstentryright dst_negative_code_pullback_firstentryright dst_negative_scale_pullback_firstentryright dst_positive_pullback_firstentryright dst_negative_pullback_firstentryright. (((G) = (((((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) * S ((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) + ((dst_positive_scale_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))) * S ((((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) * S ((dst_positive_code_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright)) + ((dst_positive_scale_pullback_firstentryright) + (dst_positive_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))) + ((((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright))) + (((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) * S ((dst_negative_code_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)) + ((dst_negative_scale_pullback_firstentryright) + (dst_negative_scale_pullback_firstentryright)))))) /\ (((((exists ff_h_pvs_pullback_firstentryrightpositive. ff_h_pvs_pullback_firstentryrightpositive + S (dst_positive_pullback_firstentryright) = S ((S (dc_quotient_pullback_firstentry)) * dst_positive_scale_pullback_firstentryright)) /\ exists ff_q_pvs_pullback_firstentryrightpositive. dst_positive_code_pullback_firstentryright = ff_q_pvs_pullback_firstentryrightpositive * S ((S (dc_quotient_pullback_firstentry)) * dst_positive_scale_pullback_firstentryright) + (dst_positive_pullback_firstentryright))) /\ (((((exists ff_h_pvs_pullback_firstentryrightnegative. ff_h_pvs_pullback_firstentryrightnegative + S (dst_negative_pullback_firstentryright) = S ((S (dc_quotient_pullback_firstentry)) * dst_negative_scale_pullback_firstentryright)) /\ exists ff_q_pvs_pullback_firstentryrightnegative. dst_negative_code_pullback_firstentryright = ff_q_pvs_pullback_firstentryrightnegative * S ((S (dc_quotient_pullback_firstentry)) * dst_negative_scale_pullback_firstentryright) + (dst_negative_pullback_firstentryright))) /\ (exists ge_balance_positive_pullback_firstentryrightvalue ge_balance_negative_pullback_firstentryrightvalue. (((((dc_right_pullback_firstentry) = 2 * (ge_balance_positive_pullback_firstentryrightvalue) /\ (ge_balance_negative_pullback_firstentryrightvalue) = 0) \/ exists ge_signed_half_pullback_firstentryrightvaluedecode. (((dc_right_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryrightvaluedecode + 1 /\ (ge_balance_positive_pullback_firstentryrightvalue) = 0) /\ (ge_balance_negative_pullback_firstentryrightvalue) = S ge_signed_half_pullback_firstentryrightvaluedecode))) /\ ((dst_positive_pullback_firstentryright) + ge_balance_negative_pullback_firstentryrightvalue = (dst_negative_pullback_firstentryright) + ge_balance_positive_pullback_firstentryrightvalue))))))))) /\ (exists sto_ap_pullback_firstentryproduct sto_an_pullback_firstentryproduct sto_bp_pullback_firstentryproduct sto_bn_pullback_firstentryproduct sto_cp_pullback_firstentryproduct sto_cn_pullback_firstentryproduct. (((((dc_left_pullback_firstentry) = 2 * (sto_ap_pullback_firstentryproduct) /\ (sto_an_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductleft. (((dc_left_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryproductleft + 1 /\ (sto_ap_pullback_firstentryproduct) = 0) /\ (sto_an_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductleft))) /\ ((((((dc_right_pullback_firstentry) = 2 * (sto_bp_pullback_firstentryproduct) /\ (sto_bn_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductright. (((dc_right_pullback_firstentry) = 2 * ge_signed_half_pullback_firstentryproductright + 1 /\ (sto_bp_pullback_firstentryproduct) = 0) /\ (sto_bn_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductright))) /\ ((((((dc_value_pullback_first) = 2 * (sto_cp_pullback_firstentryproduct) /\ (sto_cn_pullback_firstentryproduct) = 0) \/ exists ge_signed_half_pullback_firstentryproductoutput. (((dc_value_pullback_first) = 2 * ge_signed_half_pullback_firstentryproductoutput + 1 /\ (sto_cp_pullback_firstentryproduct) = 0) /\ (sto_cn_pullback_firstentryproduct) = S ge_signed_half_pullback_firstentryproductoutput))) /\ ((sto_ap_pullback_firstentryproduct * sto_bp_pullback_firstentryproduct + sto_an_pullback_firstentryproduct * sto_bn_pullback_firstentryproduct) + sto_cn_pullback_firstentryproduct = (sto_ap_pullback_firstentryproduct * sto_bn_pullback_firstentryproduct + sto_an_pullback_firstentryproduct * sto_bp_pullback_firstentryproduct) + sto_cp_pullback_firstentryproduct))))))))))))))) \/ ((((dc_index_pullback_first)=0 \/ ~(exists pvs_factor_pullback_firstentrynondivisor. (n) = (dc_index_pullback_first) * pvs_factor_pullback_firstentrynondivisor)) /\ ((dc_value_pullback_first)=0))))))) -> (((exists dst_positive_code_pullback_secondtable dst_positive_scale_pullback_secondtable dst_negative_code_pullback_secondtable dst_negative_scale_pullback_secondtable. (((Q) = (((((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) * S ((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) + ((dst_positive_scale_pullback_secondtable) + (dst_positive_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))) * S ((((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) * S ((dst_positive_code_pullback_secondtable) + (dst_positive_scale_pullback_secondtable)) + ((dst_positive_scale_pullback_secondtable) + (dst_positive_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))) + ((((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable))) + (((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) * S ((dst_negative_code_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)) + ((dst_negative_scale_pullback_secondtable) + (dst_negative_scale_pullback_secondtable)))))) /\ (forall dst_index_pullback_secondtable. (exists pvs_le_gap_pullback_secondtabledomain. pvs_le_gap_pullback_secondtabledomain + (dst_index_pullback_secondtable) = (n)) -> exists dst_positive_pullback_secondtable dst_negative_pullback_secondtable dst_value_pullback_secondtable. ((((exists ff_h_pvs_pullback_secondtableentrypositive. ff_h_pvs_pullback_secondtableentrypositive + S (dst_positive_pullback_secondtable) = S ((S (dst_index_pullback_secondtable)) * dst_positive_scale_pullback_secondtable)) /\ exists ff_q_pvs_pullback_secondtableentrypositive. dst_positive_code_pullback_secondtable = ff_q_pvs_pullback_secondtableentrypositive * S ((S (dst_index_pullback_secondtable)) * dst_positive_scale_pullback_secondtable) + (dst_positive_pullback_secondtable))) /\ (((((exists ff_h_pvs_pullback_secondtableentrynegative. ff_h_pvs_pullback_secondtableentrynegative + S (dst_negative_pullback_secondtable) = S ((S (dst_index_pullback_secondtable)) * dst_negative_scale_pullback_secondtable)) /\ exists ff_q_pvs_pullback_secondtableentrynegative. dst_negative_code_pullback_secondtable = ff_q_pvs_pullback_secondtableentrynegative * S ((S (dst_index_pullback_secondtable)) * dst_negative_scale_pullback_secondtable) + (dst_negative_pullback_secondtable))) /\ (exists ge_balance_positive_pullback_secondtableentryvalue ge_balance_negative_pullback_secondtableentryvalue. (((((dst_value_pullback_secondtable) = 2 * (ge_balance_positive_pullback_secondtableentryvalue) /\ (ge_balance_negative_pullback_secondtableentryvalue) = 0) \/ exists ge_signed_half_pullback_secondtableentryvaluedecode. (((dst_value_pullback_secondtable) = 2 * ge_signed_half_pullback_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_pullback_secondtableentryvalue) = 0) /\ (ge_balance_negative_pullback_secondtableentryvalue) = S ge_signed_half_pullback_secondtableentryvaluedecode))) /\ ((dst_positive_pullback_secondtable) + ge_balance_negative_pullback_secondtableentryvalue = (dst_negative_pullback_secondtable) + ge_balance_positive_pullback_secondtableentryvalue))))))))) /\ (forall dc_index_pullback_second dc_value_pullback_second. (exists pvs_le_gap_pullback_seconddomain. pvs_le_gap_pullback_seconddomain + (dc_index_pullback_second) = (n)) -> (exists dst_positive_code_pullback_secondlookup dst_positive_scale_pullback_secondlookup dst_negative_code_pullback_secondlookup dst_negative_scale_pullback_secondlookup dst_positive_pullback_secondlookup dst_negative_pullback_secondlookup. (((Q) = (((((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) * S ((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) + ((dst_positive_scale_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))) * S ((((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) * S ((dst_positive_code_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup)) + ((dst_positive_scale_pullback_secondlookup) + (dst_positive_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))) + ((((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup))) + (((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) * S ((dst_negative_code_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)) + ((dst_negative_scale_pullback_secondlookup) + (dst_negative_scale_pullback_secondlookup)))))) /\ (((((exists ff_h_pvs_pullback_secondlookuppositive. ff_h_pvs_pullback_secondlookuppositive + S (dst_positive_pullback_secondlookup) = S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondlookup)) /\ exists ff_q_pvs_pullback_secondlookuppositive. dst_positive_code_pullback_secondlookup = ff_q_pvs_pullback_secondlookuppositive * S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondlookup) + (dst_positive_pullback_secondlookup))) /\ (((((exists ff_h_pvs_pullback_secondlookupnegative. ff_h_pvs_pullback_secondlookupnegative + S (dst_negative_pullback_secondlookup) = S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondlookup)) /\ exists ff_q_pvs_pullback_secondlookupnegative. dst_negative_code_pullback_secondlookup = ff_q_pvs_pullback_secondlookupnegative * S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondlookup) + (dst_negative_pullback_secondlookup))) /\ (exists ge_balance_positive_pullback_secondlookupvalue ge_balance_negative_pullback_secondlookupvalue. (((((dc_value_pullback_second) = 2 * (ge_balance_positive_pullback_secondlookupvalue) /\ (ge_balance_negative_pullback_secondlookupvalue) = 0) \/ exists ge_signed_half_pullback_secondlookupvaluedecode. (((dc_value_pullback_second) = 2 * ge_signed_half_pullback_secondlookupvaluedecode + 1 /\ (ge_balance_positive_pullback_secondlookupvalue) = 0) /\ (ge_balance_negative_pullback_secondlookupvalue) = S ge_signed_half_pullback_secondlookupvaluedecode))) /\ ((dst_positive_pullback_secondlookup) + ge_balance_negative_pullback_secondlookupvalue = (dst_negative_pullback_secondlookup) + ge_balance_positive_pullback_secondlookupvalue))))))))) -> ((((~((dc_index_pullback_second)=0)) /\ (exists dc_quotient_pullback_secondentry dc_left_pullback_secondentry dc_right_pullback_secondentry. (((n)=(dc_index_pullback_second)*dc_quotient_pullback_secondentry) /\ (((exists dst_positive_code_pullback_secondentryleft dst_positive_scale_pullback_secondentryleft dst_negative_code_pullback_secondentryleft dst_negative_scale_pullback_secondentryleft dst_positive_pullback_secondentryleft dst_negative_pullback_secondentryleft. (((G) = (((((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) * S ((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) + ((dst_positive_scale_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))) * S ((((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) * S ((dst_positive_code_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft)) + ((dst_positive_scale_pullback_secondentryleft) + (dst_positive_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))) + ((((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft))) + (((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) * S ((dst_negative_code_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)) + ((dst_negative_scale_pullback_secondentryleft) + (dst_negative_scale_pullback_secondentryleft)))))) /\ (((((exists ff_h_pvs_pullback_secondentryleftpositive. ff_h_pvs_pullback_secondentryleftpositive + S (dst_positive_pullback_secondentryleft) = S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondentryleft)) /\ exists ff_q_pvs_pullback_secondentryleftpositive. dst_positive_code_pullback_secondentryleft = ff_q_pvs_pullback_secondentryleftpositive * S ((S (dc_index_pullback_second)) * dst_positive_scale_pullback_secondentryleft) + (dst_positive_pullback_secondentryleft))) /\ (((((exists ff_h_pvs_pullback_secondentryleftnegative. ff_h_pvs_pullback_secondentryleftnegative + S (dst_negative_pullback_secondentryleft) = S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondentryleft)) /\ exists ff_q_pvs_pullback_secondentryleftnegative. dst_negative_code_pullback_secondentryleft = ff_q_pvs_pullback_secondentryleftnegative * S ((S (dc_index_pullback_second)) * dst_negative_scale_pullback_secondentryleft) + (dst_negative_pullback_secondentryleft))) /\ (exists ge_balance_positive_pullback_secondentryleftvalue ge_balance_negative_pullback_secondentryleftvalue. (((((dc_left_pullback_secondentry) = 2 * (ge_balance_positive_pullback_secondentryleftvalue) /\ (ge_balance_negative_pullback_secondentryleftvalue) = 0) \/ exists ge_signed_half_pullback_secondentryleftvaluedecode. (((dc_left_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryleftvaluedecode + 1 /\ (ge_balance_positive_pullback_secondentryleftvalue) = 0) /\ (ge_balance_negative_pullback_secondentryleftvalue) = S ge_signed_half_pullback_secondentryleftvaluedecode))) /\ ((dst_positive_pullback_secondentryleft) + ge_balance_negative_pullback_secondentryleftvalue = (dst_negative_pullback_secondentryleft) + ge_balance_positive_pullback_secondentryleftvalue))))))))) /\ (((exists dst_positive_code_pullback_secondentryright dst_positive_scale_pullback_secondentryright dst_negative_code_pullback_secondentryright dst_negative_scale_pullback_secondentryright dst_positive_pullback_secondentryright dst_negative_pullback_secondentryright. (((F) = (((((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) * S ((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) + ((dst_positive_scale_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))) * S ((((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) * S ((dst_positive_code_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright)) + ((dst_positive_scale_pullback_secondentryright) + (dst_positive_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))) + ((((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright))) + (((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) * S ((dst_negative_code_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)) + ((dst_negative_scale_pullback_secondentryright) + (dst_negative_scale_pullback_secondentryright)))))) /\ (((((exists ff_h_pvs_pullback_secondentryrightpositive. ff_h_pvs_pullback_secondentryrightpositive + S (dst_positive_pullback_secondentryright) = S ((S (dc_quotient_pullback_secondentry)) * dst_positive_scale_pullback_secondentryright)) /\ exists ff_q_pvs_pullback_secondentryrightpositive. dst_positive_code_pullback_secondentryright = ff_q_pvs_pullback_secondentryrightpositive * S ((S (dc_quotient_pullback_secondentry)) * dst_positive_scale_pullback_secondentryright) + (dst_positive_pullback_secondentryright))) /\ (((((exists ff_h_pvs_pullback_secondentryrightnegative. ff_h_pvs_pullback_secondentryrightnegative + S (dst_negative_pullback_secondentryright) = S ((S (dc_quotient_pullback_secondentry)) * dst_negative_scale_pullback_secondentryright)) /\ exists ff_q_pvs_pullback_secondentryrightnegative. dst_negative_code_pullback_secondentryright = ff_q_pvs_pullback_secondentryrightnegative * S ((S (dc_quotient_pullback_secondentry)) * dst_negative_scale_pullback_secondentryright) + (dst_negative_pullback_secondentryright))) /\ (exists ge_balance_positive_pullback_secondentryrightvalue ge_balance_negative_pullback_secondentryrightvalue. (((((dc_right_pullback_secondentry) = 2 * (ge_balance_positive_pullback_secondentryrightvalue) /\ (ge_balance_negative_pullback_secondentryrightvalue) = 0) \/ exists ge_signed_half_pullback_secondentryrightvaluedecode. (((dc_right_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryrightvaluedecode + 1 /\ (ge_balance_positive_pullback_secondentryrightvalue) = 0) /\ (ge_balance_negative_pullback_secondentryrightvalue) = S ge_signed_half_pullback_secondentryrightvaluedecode))) /\ ((dst_positive_pullback_secondentryright) + ge_balance_negative_pullback_secondentryrightvalue = (dst_negative_pullback_secondentryright) + ge_balance_positive_pullback_secondentryrightvalue))))))))) /\ (exists sto_ap_pullback_secondentryproduct sto_an_pullback_secondentryproduct sto_bp_pullback_secondentryproduct sto_bn_pullback_secondentryproduct sto_cp_pullback_secondentryproduct sto_cn_pullback_secondentryproduct. (((((dc_left_pullback_secondentry) = 2 * (sto_ap_pullback_secondentryproduct) /\ (sto_an_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductleft. (((dc_left_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryproductleft + 1 /\ (sto_ap_pullback_secondentryproduct) = 0) /\ (sto_an_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductleft))) /\ ((((((dc_right_pullback_secondentry) = 2 * (sto_bp_pullback_secondentryproduct) /\ (sto_bn_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductright. (((dc_right_pullback_secondentry) = 2 * ge_signed_half_pullback_secondentryproductright + 1 /\ (sto_bp_pullback_secondentryproduct) = 0) /\ (sto_bn_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductright))) /\ ((((((dc_value_pullback_second) = 2 * (sto_cp_pullback_secondentryproduct) /\ (sto_cn_pullback_secondentryproduct) = 0) \/ exists ge_signed_half_pullback_secondentryproductoutput. (((dc_value_pullback_second) = 2 * ge_signed_half_pullback_secondentryproductoutput + 1 /\ (sto_cp_pullback_secondentryproduct) = 0) /\ (sto_cn_pullback_secondentryproduct) = S ge_signed_half_pullback_secondentryproductoutput))) /\ ((sto_ap_pullback_secondentryproduct * sto_bp_pullback_secondentryproduct + sto_an_pullback_secondentryproduct * sto_bn_pullback_secondentryproduct) + sto_cn_pullback_secondentryproduct = (sto_ap_pullback_secondentryproduct * sto_bn_pullback_secondentryproduct + sto_an_pullback_secondentryproduct * sto_bp_pullback_secondentryproduct) + sto_cp_pullback_secondentryproduct))))))))))))))) \/ ((((dc_index_pullback_second)=0 \/ ~(exists pvs_factor_pullback_secondentrynondivisor. (n) = (dc_index_pullback_second) * pvs_factor_pullback_secondentrynondivisor)) /\ ((dc_value_pullback_second)=0))))))) -> (forall dvi_index_pullback_map. (exists pvs_gap_pullback_mapdomain. pvs_gap_pullback_mapdomain + S (dvi_index_pullback_map) = (S n)) -> exists dvi_value_pullback_map. ((((exists ff_h_pvs_pullback_mapentry. ff_h_pvs_pullback_mapentry + S (dvi_value_pullback_map) = S ((S (dvi_index_pullback_map)) * s)) /\ exists ff_q_pvs_pullback_mapentry. r = ff_q_pvs_pullback_mapentry * S ((S (dvi_index_pullback_map)) * s) + (dvi_value_pullback_map))) /\ ((((~((dvi_index_pullback_map)=0)) /\ ((n)=(dvi_index_pullback_map)*(dvi_value_pullback_map)))) \/ ((((dvi_index_pullback_map)=0 \/ ~(exists pvs_factor_pullback_mapgraphnondivisor. (n) = (dvi_index_pullback_map) * pvs_factor_pullback_mapgraphnondivisor)) /\ ((dvi_value_pullback_map)=(dvi_index_pullback_map))))))) -> (forall dsr_index_pullback_result dsr_image_pullback_result dsr_value_pullback_result. (exists pvs_gap_pullback_resultbound. pvs_gap_pullback_resultbound + S (dsr_index_pullback_result) = (S n)) -> (((exists ff_h_pvs_pullback_resultmap. ff_h_pvs_pullback_resultmap + S (dsr_image_pullback_result) = S ((S (dsr_index_pullback_result)) * s)) /\ exists ff_q_pvs_pullback_resultmap. r = ff_q_pvs_pullback_resultmap * S ((S (dsr_index_pullback_result)) * s) + (dsr_image_pullback_result))) -> (exists dst_positive_code_pullback_resultsource dst_positive_scale_pullback_resultsource dst_negative_code_pullback_resultsource dst_negative_scale_pullback_resultsource dst_positive_pullback_resultsource dst_negative_pullback_resultsource. (((P) = (((((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) * S ((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) + ((dst_positive_scale_pullback_resultsource) + (dst_positive_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))) * S ((((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) * S ((dst_positive_code_pullback_resultsource) + (dst_positive_scale_pullback_resultsource)) + ((dst_positive_scale_pullback_resultsource) + (dst_positive_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))) + ((((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource))) + (((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) * S ((dst_negative_code_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)) + ((dst_negative_scale_pullback_resultsource) + (dst_negative_scale_pullback_resultsource)))))) /\ (((((exists ff_h_pvs_pullback_resultsourcepositive. ff_h_pvs_pullback_resultsourcepositive + S (dst_positive_pullback_resultsource) = S ((S (dsr_image_pullback_result)) * dst_positive_scale_pullback_resultsource)) /\ exists ff_q_pvs_pullback_resultsourcepositive. dst_positive_code_pullback_resultsource = ff_q_pvs_pullback_resultsourcepositive * S ((S (dsr_image_pullback_result)) * dst_positive_scale_pullback_resultsource) + (dst_positive_pullback_resultsource))) /\ (((((exists ff_h_pvs_pullback_resultsourcenegative. ff_h_pvs_pullback_resultsourcenegative + S (dst_negative_pullback_resultsource) = S ((S (dsr_image_pullback_result)) * dst_negative_scale_pullback_resultsource)) /\ exists ff_q_pvs_pullback_resultsourcenegative. dst_negative_code_pullback_resultsource = ff_q_pvs_pullback_resultsourcenegative * S ((S (dsr_image_pullback_result)) * dst_negative_scale_pullback_resultsource) + (dst_negative_pullback_resultsource))) /\ (exists ge_balance_positive_pullback_resultsourcevalue ge_balance_negative_pullback_resultsourcevalue. (((((dsr_value_pullback_result) = 2 * (ge_balance_positive_pullback_resultsourcevalue) /\ (ge_balance_negative_pullback_resultsourcevalue) = 0) \/ exists ge_signed_half_pullback_resultsourcevaluedecode. (((dsr_value_pullback_result) = 2 * ge_signed_half_pullback_resultsourcevaluedecode + 1 /\ (ge_balance_positive_pullback_resultsourcevalue) = 0) /\ (ge_balance_negative_pullback_resultsourcevalue) = S ge_signed_half_pullback_resultsourcevaluedecode))) /\ ((dst_positive_pullback_resultsource) + ge_balance_negative_pullback_resultsourcevalue = (dst_negative_pullback_resultsource) + ge_balance_positive_pullback_resultsourcevalue))))))))) -> (exists dst_positive_code_pullback_resulttarget dst_positive_scale_pullback_resulttarget dst_negative_code_pullback_resulttarget dst_negative_scale_pullback_resulttarget dst_positive_pullback_resulttarget dst_negative_pullback_resulttarget. (((Q) = (((((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) * S ((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) + ((dst_positive_scale_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))) * S ((((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) * S ((dst_positive_code_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget)) + ((dst_positive_scale_pullback_resulttarget) + (dst_positive_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))) + ((((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget))) + (((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) * S ((dst_negative_code_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)) + ((dst_negative_scale_pullback_resulttarget) + (dst_negative_scale_pullback_resulttarget)))))) /\ (((((exists ff_h_pvs_pullback_resulttargetpositive. ff_h_pvs_pullback_resulttargetpositive + S (dst_positive_pullback_resulttarget) = S ((S (dsr_index_pullback_result)) * dst_positive_scale_pullback_resulttarget)) /\ exists ff_q_pvs_pullback_resulttargetpositive. dst_positive_code_pullback_resulttarget = ff_q_pvs_pullback_resulttargetpositive * S ((S (dsr_index_pullback_result)) * dst_positive_scale_pullback_resulttarget) + (dst_positive_pullback_resulttarget))) /\ (((((exists ff_h_pvs_pullback_resulttargetnegative. ff_h_pvs_pullback_resulttargetnegative + S (dst_negative_pullback_resulttarget) = S ((S (dsr_index_pullback_result)) * dst_negative_scale_pullback_resulttarget)) /\ exists ff_q_pvs_pullback_resulttargetnegative. dst_negative_code_pullback_resulttarget = ff_q_pvs_pullback_resulttargetnegative * S ((S (dsr_index_pullback_result)) * dst_negative_scale_pullback_resulttarget) + (dst_negative_pullback_resulttarget))) /\ (exists ge_balance_positive_pullback_resulttargetvalue ge_balance_negative_pullback_resulttargetvalue. (((((dsr_value_pullback_result) = 2 * (ge_balance_positive_pullback_resulttargetvalue) /\ (ge_balance_negative_pullback_resulttargetvalue) = 0) \/ exists ge_signed_half_pullback_resulttargetvaluedecode. (((dsr_value_pullback_result) = 2 * ge_signed_half_pullback_resulttargetvaluedecode + 1 /\ (ge_balance_positive_pullback_resulttargetvalue) = 0) /\ (ge_balance_negative_pullback_resulttargetvalue) = S ge_signed_half_pullback_resulttargetvaluedecode))) /\ ((dst_positive_pullback_resulttarget) + ge_balance_negative_pullback_resulttargetvalue = (dst_negative_pullback_resulttarget) + ge_balance_positive_pullback_resulttargetvalue))))))))))

Complete tactic proof in conservative notation

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

71 script commands · 9 reading checkpoints · 3 local claims

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

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

Named ingredients (3)
dirichlet convolution prefix value from entrydirichlet convolution entry complementdirichlet convolution prefix lookup
01Fix variables and assumptionsL1–10

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 P
  5. L5
    intro Q
  6. L6
    intro r
  7. L7
    intro s
  8. L8
    intro hn
  9. L9
    intro hP
  10. L10
    intro hQ
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hc
  2. L12
    intro d
  3. L13
    intro q
  4. L14
    intro z
  5. L15
    intro hd
  6. L16
    intro hmap
  7. L17
    intro hz
03Establish hdbL18–22

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

  1. L18
  2. L19
    specialize le_of_succ_le_succ (d)
  3. L20
    specialize le_of_succ_le_succ (n)
  4. L21
    apply le_of_succ_le_succ
  5. L22
    exact hd
04Establish hcompL23–32

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

  1. L23
    have hcomp : DivisorComplement(n,d,q)Definitions: DivisorComplement(n,d,q)Original native command in the exact edition
  2. L24
    specialize divisor_complement_prefix_lookup (n)
  3. L25
    specialize divisor_complement_prefix_lookup (r)
  4. L26
    specialize divisor_complement_prefix_lookup (s)
  5. L27
    specialize divisor_complement_prefix_lookup (S n)
  6. L28
    specialize divisor_complement_prefix_lookup (d)
  7. L29
    specialize divisor_complement_prefix_lookup (q)
  8. L30
    apply divisor_complement_prefix_lookup
  9. L31
    exact hc
  10. L32
    exact hd
05Use earlier factsL33–33

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

  1. L33
    exact hmap
06Establish hqbL34–43

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

  1. L34
  2. L35
    specialize divisor_complement_bounded (n)
  3. L36
    specialize divisor_complement_bounded (d)
  4. L37
    specialize divisor_complement_bounded (q)
  5. L38
    apply divisor_complement_bounded
  6. L39
    exact hn
  7. L40
    exact hdb
  8. L41
    exact hcomp
  9. L42
    specialize dirichlet_convolution_prefix_value_from_entry (G)
  10. L43
    specialize dirichlet_convolution_prefix_value_from_entry (F)
07Use earlier factsL44–53

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

  1. L44
    specialize dirichlet_convolution_prefix_value_from_entry (n)
  2. L45
    specialize dirichlet_convolution_prefix_value_from_entry (n)
  3. L46
    specialize dirichlet_convolution_prefix_value_from_entry (Q)
  4. L47
    specialize dirichlet_convolution_prefix_value_from_entry (d)
  5. L48
    specialize dirichlet_convolution_prefix_value_from_entry (z)
  6. L49
    apply dirichlet_convolution_prefix_value_from_entry
  7. L50
    exact hQ
  8. L51
    exact hdb
  9. L52
    specialize dirichlet_convolution_entry_complement (F)
  10. L53
    specialize dirichlet_convolution_entry_complement (G)
08Use earlier factsL54–63

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

  1. L54
    specialize dirichlet_convolution_entry_complement (n)
  2. L55
    specialize dirichlet_convolution_entry_complement (d)
  3. L56
    specialize dirichlet_convolution_entry_complement (q)
  4. L57
    specialize dirichlet_convolution_entry_complement (z)
  5. L58
    apply dirichlet_convolution_entry_complement
  6. L59
    exact hn
  7. L60
    exact hcomp
  8. L61
    specialize dirichlet_convolution_prefix_lookup (F)
  9. L62
    specialize dirichlet_convolution_prefix_lookup (G)
  10. L63
    specialize dirichlet_convolution_prefix_lookup (n)
09Use earlier factsL64–71

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

  1. L64
    specialize dirichlet_convolution_prefix_lookup (n)
  2. L65
    specialize dirichlet_convolution_prefix_lookup (P)
  3. L66
    specialize dirichlet_convolution_prefix_lookup (q)
  4. L67
    specialize dirichlet_convolution_prefix_lookup (z)
  5. L68
    apply dirichlet_convolution_prefix_lookup
  6. L69
    exact hP
  7. L70
    exact hqb
  8. L71
    exact hz

Library-wide reading audit

Original defined command ledger · 71 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro n
  4. 0004intro P
  5. 0005intro Q
  6. 0006intro r
  7. 0007intro s
  8. 0008intro hn
  9. 0009intro hP
  10. 0010intro hQ
  11. 0011intro hc
  12. 0012intro d
  13. 0013intro q
  14. 0014intro z
  15. 0015intro hd
  16. 0016intro hmap
  17. 0017intro hz
  18. 0018have hdb : Le(d,n)
  19. 0019specialize le_of_succ_le_succ (d)
  20. 0020specialize le_of_succ_le_succ (n)
  21. 0021apply le_of_succ_le_succ
  22. 0022exact hd
  23. 0023have hcomp : DivisorComplement(n,d,q)
  24. 0024specialize divisor_complement_prefix_lookup (n)
  25. 0025specialize divisor_complement_prefix_lookup (r)
  26. 0026specialize divisor_complement_prefix_lookup (s)
  27. 0027specialize divisor_complement_prefix_lookup (S n)
  28. 0028specialize divisor_complement_prefix_lookup (d)
  29. 0029specialize divisor_complement_prefix_lookup (q)
  30. 0030apply divisor_complement_prefix_lookup
  31. 0031exact hc
  32. 0032exact hd
  33. 0033exact hmap
  34. 0034have hqb : Le(q,n)
  35. 0035specialize divisor_complement_bounded (n)
  36. 0036specialize divisor_complement_bounded (d)
  37. 0037specialize divisor_complement_bounded (q)
  38. 0038apply divisor_complement_bounded
  39. 0039exact hn
  40. 0040exact hdb
  41. 0041exact hcomp
  42. 0042specialize dirichlet_convolution_prefix_value_from_entry (G)
  43. 0043specialize dirichlet_convolution_prefix_value_from_entry (F)
  44. 0044specialize dirichlet_convolution_prefix_value_from_entry (n)
  45. 0045specialize dirichlet_convolution_prefix_value_from_entry (n)
  46. 0046specialize dirichlet_convolution_prefix_value_from_entry (Q)
  47. 0047specialize dirichlet_convolution_prefix_value_from_entry (d)
  48. 0048specialize dirichlet_convolution_prefix_value_from_entry (z)
  49. 0049apply dirichlet_convolution_prefix_value_from_entry
  50. 0050exact hQ
  51. 0051exact hdb
  52. 0052specialize dirichlet_convolution_entry_complement (F)
  53. 0053specialize dirichlet_convolution_entry_complement (G)
  54. 0054specialize dirichlet_convolution_entry_complement (n)
  55. 0055specialize dirichlet_convolution_entry_complement (d)
  56. 0056specialize dirichlet_convolution_entry_complement (q)
  57. 0057specialize dirichlet_convolution_entry_complement (z)
  58. 0058apply dirichlet_convolution_entry_complement
  59. 0059exact hn
  60. 0060exact hcomp
  61. 0061specialize dirichlet_convolution_prefix_lookup (F)
  62. 0062specialize dirichlet_convolution_prefix_lookup (G)
  63. 0063specialize dirichlet_convolution_prefix_lookup (n)
  64. 0064specialize dirichlet_convolution_prefix_lookup (n)
  65. 0065specialize dirichlet_convolution_prefix_lookup (P)
  66. 0066specialize dirichlet_convolution_prefix_lookup (q)
  67. 0067specialize dirichlet_convolution_prefix_lookup (z)
  68. 0068apply dirichlet_convolution_prefix_lookup
  69. 0069exact hP
  70. 0070exact hqb
  71. 0071exact hz