DT000A

dirichlet_convolution_at_one_iff

Actual convolution at input one is exactly the actual signed product F(1)*G(1); both implications construct or inspect the real two-entry masked fold.

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.

The strict remainder is an actual inclusive prefix through k with an S k-entry fold; the future input at S k is excluded. A genuine table extension supplies the endpoint. The at-one identity inspects or constructs the real two-entry masked sum. No recurrence, inverse, or omitted summand value is assumed as a conclusion-bearing premise.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ a. ∀ b. ∀ z. ArithAt(F,1,a) → ArithAt(G,1,b) → (DirichletSum(F,G,1,z) → SignedMul(a,b,z)) ∧ (SignedMul(a,b,z) → DirichletSum(F,G,1,z))

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

Definition DAG

SignedAdd(a,b,c) · 1SignedMul(a,b,c) · 5ArithTable(N,F) · 1ArithAt(F,i,z) · 4SignedPrefixSum(F,l,z) · 2DirichletEntry(F,G,n,d,z) · 2DirichletPrefix(F,G,n,l,M) · 1DirichletSum(F,G,n,z) · 2

Actual proof prerequisites

dirichlet_convolution_zero_prefix_sumdirichlet_convolution_prefix_restrict · checked external prerequisitezero_le · checked external prerequisitedivisor_signed_sum_successor_decompose · checked external prerequisitedivisor_signed_sum_functional · checked external prerequisitesigned_add_functional · checked external prerequisitesigned_add_zero_left · checked external prerequisitedirichlet_convolution_last_entry_iffdirichlet_convolution_prefix_lookup · checked external prerequisitele_refl · checked external prerequisitearithmetic_signed_table_singleton · checked external prerequisitedirichlet_convolution_prefix_zero_constructor · checked external prerequisitedirichlet_convolution_prefix_last_step
Original expanded first-order statement 
forall F G a b z. (exists dst_positive_code_one_first dst_positive_scale_one_first dst_negative_code_one_first dst_negative_scale_one_first dst_positive_one_first dst_negative_one_first. (((F) = (((((dst_positive_code_one_first) + (dst_positive_scale_one_first)) * S ((dst_positive_code_one_first) + (dst_positive_scale_one_first)) + ((dst_positive_scale_one_first) + (dst_positive_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))) * S ((((dst_positive_code_one_first) + (dst_positive_scale_one_first)) * S ((dst_positive_code_one_first) + (dst_positive_scale_one_first)) + ((dst_positive_scale_one_first) + (dst_positive_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))) + ((((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))))) /\ (((((exists ff_h_pvs_one_firstpositive. ff_h_pvs_one_firstpositive + S (dst_positive_one_first) = S ((S (1)) * dst_positive_scale_one_first)) /\ exists ff_q_pvs_one_firstpositive. dst_positive_code_one_first = ff_q_pvs_one_firstpositive * S ((S (1)) * dst_positive_scale_one_first) + (dst_positive_one_first))) /\ (((((exists ff_h_pvs_one_firstnegative. ff_h_pvs_one_firstnegative + S (dst_negative_one_first) = S ((S (1)) * dst_negative_scale_one_first)) /\ exists ff_q_pvs_one_firstnegative. dst_negative_code_one_first = ff_q_pvs_one_firstnegative * S ((S (1)) * dst_negative_scale_one_first) + (dst_negative_one_first))) /\ (exists ge_balance_positive_one_firstvalue ge_balance_negative_one_firstvalue. (((((a) = 2 * (ge_balance_positive_one_firstvalue) /\ (ge_balance_negative_one_firstvalue) = 0) \/ exists ge_signed_half_one_firstvaluedecode. (((a) = 2 * ge_signed_half_one_firstvaluedecode + 1 /\ (ge_balance_positive_one_firstvalue) = 0) /\ (ge_balance_negative_one_firstvalue) = S ge_signed_half_one_firstvaluedecode))) /\ ((dst_positive_one_first) + ge_balance_negative_one_firstvalue = (dst_negative_one_first) + ge_balance_positive_one_firstvalue))))))))) -> (exists dst_positive_code_one_second dst_positive_scale_one_second dst_negative_code_one_second dst_negative_scale_one_second dst_positive_one_second dst_negative_one_second. (((G) = (((((dst_positive_code_one_second) + (dst_positive_scale_one_second)) * S ((dst_positive_code_one_second) + (dst_positive_scale_one_second)) + ((dst_positive_scale_one_second) + (dst_positive_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))) * S ((((dst_positive_code_one_second) + (dst_positive_scale_one_second)) * S ((dst_positive_code_one_second) + (dst_positive_scale_one_second)) + ((dst_positive_scale_one_second) + (dst_positive_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))) + ((((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))))) /\ (((((exists ff_h_pvs_one_secondpositive. ff_h_pvs_one_secondpositive + S (dst_positive_one_second) = S ((S (1)) * dst_positive_scale_one_second)) /\ exists ff_q_pvs_one_secondpositive. dst_positive_code_one_second = ff_q_pvs_one_secondpositive * S ((S (1)) * dst_positive_scale_one_second) + (dst_positive_one_second))) /\ (((((exists ff_h_pvs_one_secondnegative. ff_h_pvs_one_secondnegative + S (dst_negative_one_second) = S ((S (1)) * dst_negative_scale_one_second)) /\ exists ff_q_pvs_one_secondnegative. dst_negative_code_one_second = ff_q_pvs_one_secondnegative * S ((S (1)) * dst_negative_scale_one_second) + (dst_negative_one_second))) /\ (exists ge_balance_positive_one_secondvalue ge_balance_negative_one_secondvalue. (((((b) = 2 * (ge_balance_positive_one_secondvalue) /\ (ge_balance_negative_one_secondvalue) = 0) \/ exists ge_signed_half_one_secondvaluedecode. (((b) = 2 * ge_signed_half_one_secondvaluedecode + 1 /\ (ge_balance_positive_one_secondvalue) = 0) /\ (ge_balance_negative_one_secondvalue) = S ge_signed_half_one_secondvaluedecode))) /\ ((dst_positive_one_second) + ge_balance_negative_one_secondvalue = (dst_negative_one_second) + ge_balance_positive_one_secondvalue))))))))) -> (((((~((1)=0)) /\ (exists dc_mask_one_convolution. ((((exists dst_positive_code_one_convolutionmasktable dst_positive_scale_one_convolutionmasktable dst_negative_code_one_convolutionmasktable dst_negative_scale_one_convolutionmasktable. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) * S ((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) + ((((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))))) /\ (forall dst_index_one_convolutionmasktable. (exists pvs_le_gap_one_convolutionmasktabledomain. pvs_le_gap_one_convolutionmasktabledomain + (dst_index_one_convolutionmasktable) = (1)) -> exists dst_positive_one_convolutionmasktable dst_negative_one_convolutionmasktable dst_value_one_convolutionmasktable. ((((exists ff_h_pvs_one_convolutionmasktableentrypositive. ff_h_pvs_one_convolutionmasktableentrypositive + S (dst_positive_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrypositive. dst_positive_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrypositive * S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable) + (dst_positive_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_one_convolutionmasktableentrynegative. ff_h_pvs_one_convolutionmasktableentrynegative + S (dst_negative_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrynegative. dst_negative_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrynegative * S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable) + (dst_negative_one_convolutionmasktable))) /\ (exists ge_balance_positive_one_convolutionmasktableentryvalue ge_balance_negative_one_convolutionmasktableentryvalue. (((((dst_value_one_convolutionmasktable) = 2 * (ge_balance_positive_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_one_convolutionmasktableentryvaluedecode. (((dst_value_one_convolutionmasktable) = 2 * ge_signed_half_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = S ge_signed_half_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_one_convolutionmasktable) + ge_balance_negative_one_convolutionmasktableentryvalue = (dst_negative_one_convolutionmasktable) + ge_balance_positive_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_one_convolutionmask dc_value_one_convolutionmask. (exists pvs_le_gap_one_convolutionmaskdomain. pvs_le_gap_one_convolutionmaskdomain + (dc_index_one_convolutionmask) = (1)) -> (exists dst_positive_code_one_convolutionmasklookup dst_positive_scale_one_convolutionmasklookup dst_negative_code_one_convolutionmasklookup dst_negative_scale_one_convolutionmasklookup dst_positive_one_convolutionmasklookup dst_negative_one_convolutionmasklookup. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) * S ((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) + ((((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_one_convolutionmasklookuppositive. ff_h_pvs_one_convolutionmasklookuppositive + S (dst_positive_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookuppositive. dst_positive_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookuppositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup) + (dst_positive_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_one_convolutionmasklookupnegative. ff_h_pvs_one_convolutionmasklookupnegative + S (dst_negative_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookupnegative. dst_negative_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookupnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup) + (dst_negative_one_convolutionmasklookup))) /\ (exists ge_balance_positive_one_convolutionmasklookupvalue ge_balance_negative_one_convolutionmasklookupvalue. (((((dc_value_one_convolutionmask) = 2 * (ge_balance_positive_one_convolutionmasklookupvalue) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_one_convolutionmasklookupvaluedecode. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = S ge_signed_half_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_one_convolutionmasklookup) + ge_balance_negative_one_convolutionmasklookupvalue = (dst_negative_one_convolutionmasklookup) + ge_balance_positive_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_one_convolutionmask)=0)) /\ (exists dc_quotient_one_convolutionmaskentry dc_left_one_convolutionmaskentry dc_right_one_convolutionmaskentry. (((1)=(dc_index_one_convolutionmask)*dc_quotient_one_convolutionmaskentry) /\ (((exists dst_positive_code_one_convolutionmaskentryleft dst_positive_scale_one_convolutionmaskentryleft dst_negative_code_one_convolutionmaskentryleft dst_negative_scale_one_convolutionmaskentryleft dst_positive_one_convolutionmaskentryleft dst_negative_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) + ((((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftpositive. ff_h_pvs_one_convolutionmaskentryleftpositive + S (dst_positive_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftpositive. dst_positive_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftpositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftnegative. ff_h_pvs_one_convolutionmaskentryleftnegative + S (dst_negative_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftnegative. dst_negative_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_one_convolutionmaskentryleftvalue ge_balance_negative_one_convolutionmaskentryleftvalue. (((((dc_left_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryleftvaluedecode. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = S ge_signed_half_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryleft) + ge_balance_negative_one_convolutionmaskentryleftvalue = (dst_negative_one_convolutionmaskentryleft) + ge_balance_positive_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_one_convolutionmaskentryright dst_positive_scale_one_convolutionmaskentryright dst_negative_code_one_convolutionmaskentryright dst_negative_scale_one_convolutionmaskentryright dst_positive_one_convolutionmaskentryright dst_negative_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) * S ((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) + ((((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightpositive. ff_h_pvs_one_convolutionmaskentryrightpositive + S (dst_positive_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightpositive. dst_positive_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightnegative. ff_h_pvs_one_convolutionmaskentryrightnegative + S (dst_negative_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightnegative. dst_negative_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_one_convolutionmaskentryrightvalue ge_balance_negative_one_convolutionmaskentryrightvalue. (((((dc_right_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryrightvaluedecode. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = S ge_signed_half_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryright) + ge_balance_negative_one_convolutionmaskentryrightvalue = (dst_negative_one_convolutionmaskentryright) + ge_balance_positive_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_one_convolutionmaskentryproduct sto_an_one_convolutionmaskentryproduct sto_bp_one_convolutionmaskentryproduct sto_bn_one_convolutionmaskentryproduct sto_cp_one_convolutionmaskentryproduct sto_cn_one_convolutionmaskentryproduct. (((((dc_left_one_convolutionmaskentry) = 2 * (sto_ap_one_convolutionmaskentryproduct) /\ (sto_an_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductleft. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_one_convolutionmaskentryproduct) = 0) /\ (sto_an_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_one_convolutionmaskentry) = 2 * (sto_bp_one_convolutionmaskentryproduct) /\ (sto_bn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductright. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductright + 1 /\ (sto_bp_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductright))) /\ ((((((dc_value_one_convolutionmask) = 2 * (sto_cp_one_convolutionmaskentryproduct) /\ (sto_cn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductoutput. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct) + sto_cn_one_convolutionmaskentryproduct = (sto_ap_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct) + sto_cp_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_one_convolutionmask)=0 \/ ~(exists pvs_factor_one_convolutionmaskentrynondivisor. (1) = (dc_index_one_convolutionmask) * pvs_factor_one_convolutionmaskentrynondivisor)) /\ ((dc_value_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_one_convolutionfold dst_positive_scale_one_convolutionfold dst_negative_code_one_convolutionfold dst_negative_scale_one_convolutionfold dst_positive_sum_one_convolutionfold dst_negative_sum_one_convolutionfold. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) * S ((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) + ((((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))))) /\ (((exists fs_u_dst_one_convolutionfoldpositive fs_v_dst_one_convolutionfoldpositive. ((((exists fs_h_dst_one_convolutionfoldpositive_body_start. fs_h_dst_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_start. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_terminal. fs_h_dst_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_terminal. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive) + (dst_positive_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldpositive_body_steps fs_r_dst_one_convolutionfoldpositive_body_steps fs_s_dst_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_one_convolutionfold = fs_q_dst_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_r_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_s_dst_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_one_convolutionfoldpositive_body_steps = fs_r_dst_one_convolutionfoldpositive_body_steps + fs_a_dst_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_one_convolutionfoldnegative fs_v_dst_one_convolutionfoldnegative. ((((exists fs_h_dst_one_convolutionfoldnegative_body_start. fs_h_dst_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_start. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_terminal. fs_h_dst_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_terminal. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative) + (dst_negative_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldnegative_body_steps fs_r_dst_one_convolutionfoldnegative_body_steps fs_s_dst_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_one_convolutionfold = fs_q_dst_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_r_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_s_dst_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_one_convolutionfoldnegative_body_steps = fs_r_dst_one_convolutionfoldnegative_body_steps + fs_a_dst_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_one_convolutionfoldresult ge_balance_negative_one_convolutionfoldresult. (((((z) = 2 * (ge_balance_positive_one_convolutionfoldresult) /\ (ge_balance_negative_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_one_convolutionfoldresultdecode. (((z) = 2 * ge_signed_half_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_one_convolutionfoldresult) = S ge_signed_half_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_one_convolutionfold) + ge_balance_negative_one_convolutionfoldresult = (dst_negative_sum_one_convolutionfold) + ge_balance_positive_one_convolutionfoldresult))))))))))))) -> (exists sto_ap_one_product sto_an_one_product sto_bp_one_product sto_bn_one_product sto_cp_one_product sto_cn_one_product. (((((a) = 2 * (sto_ap_one_product) /\ (sto_an_one_product) = 0) \/ exists ge_signed_half_one_productleft. (((a) = 2 * ge_signed_half_one_productleft + 1 /\ (sto_ap_one_product) = 0) /\ (sto_an_one_product) = S ge_signed_half_one_productleft))) /\ ((((((b) = 2 * (sto_bp_one_product) /\ (sto_bn_one_product) = 0) \/ exists ge_signed_half_one_productright. (((b) = 2 * ge_signed_half_one_productright + 1 /\ (sto_bp_one_product) = 0) /\ (sto_bn_one_product) = S ge_signed_half_one_productright))) /\ ((((((z) = 2 * (sto_cp_one_product) /\ (sto_cn_one_product) = 0) \/ exists ge_signed_half_one_productoutput. (((z) = 2 * ge_signed_half_one_productoutput + 1 /\ (sto_cp_one_product) = 0) /\ (sto_cn_one_product) = S ge_signed_half_one_productoutput))) /\ ((sto_ap_one_product * sto_bp_one_product + sto_an_one_product * sto_bn_one_product) + sto_cn_one_product = (sto_ap_one_product * sto_bn_one_product + sto_an_one_product * sto_bp_one_product) + sto_cp_one_product)))))))) /\ ((exists sto_ap_one_product sto_an_one_product sto_bp_one_product sto_bn_one_product sto_cp_one_product sto_cn_one_product. (((((a) = 2 * (sto_ap_one_product) /\ (sto_an_one_product) = 0) \/ exists ge_signed_half_one_productleft. (((a) = 2 * ge_signed_half_one_productleft + 1 /\ (sto_ap_one_product) = 0) /\ (sto_an_one_product) = S ge_signed_half_one_productleft))) /\ ((((((b) = 2 * (sto_bp_one_product) /\ (sto_bn_one_product) = 0) \/ exists ge_signed_half_one_productright. (((b) = 2 * ge_signed_half_one_productright + 1 /\ (sto_bp_one_product) = 0) /\ (sto_bn_one_product) = S ge_signed_half_one_productright))) /\ ((((((z) = 2 * (sto_cp_one_product) /\ (sto_cn_one_product) = 0) \/ exists ge_signed_half_one_productoutput. (((z) = 2 * ge_signed_half_one_productoutput + 1 /\ (sto_cp_one_product) = 0) /\ (sto_cn_one_product) = S ge_signed_half_one_productoutput))) /\ ((sto_ap_one_product * sto_bp_one_product + sto_an_one_product * sto_bn_one_product) + sto_cn_one_product = (sto_ap_one_product * sto_bn_one_product + sto_an_one_product * sto_bp_one_product) + sto_cp_one_product))))))) -> (((~((1)=0)) /\ (exists dc_mask_one_convolution. ((((exists dst_positive_code_one_convolutionmasktable dst_positive_scale_one_convolutionmasktable dst_negative_code_one_convolutionmasktable dst_negative_scale_one_convolutionmasktable. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) * S ((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) + ((((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))))) /\ (forall dst_index_one_convolutionmasktable. (exists pvs_le_gap_one_convolutionmasktabledomain. pvs_le_gap_one_convolutionmasktabledomain + (dst_index_one_convolutionmasktable) = (1)) -> exists dst_positive_one_convolutionmasktable dst_negative_one_convolutionmasktable dst_value_one_convolutionmasktable. ((((exists ff_h_pvs_one_convolutionmasktableentrypositive. ff_h_pvs_one_convolutionmasktableentrypositive + S (dst_positive_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrypositive. dst_positive_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrypositive * S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable) + (dst_positive_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_one_convolutionmasktableentrynegative. ff_h_pvs_one_convolutionmasktableentrynegative + S (dst_negative_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrynegative. dst_negative_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrynegative * S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable) + (dst_negative_one_convolutionmasktable))) /\ (exists ge_balance_positive_one_convolutionmasktableentryvalue ge_balance_negative_one_convolutionmasktableentryvalue. (((((dst_value_one_convolutionmasktable) = 2 * (ge_balance_positive_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_one_convolutionmasktableentryvaluedecode. (((dst_value_one_convolutionmasktable) = 2 * ge_signed_half_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = S ge_signed_half_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_one_convolutionmasktable) + ge_balance_negative_one_convolutionmasktableentryvalue = (dst_negative_one_convolutionmasktable) + ge_balance_positive_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_one_convolutionmask dc_value_one_convolutionmask. (exists pvs_le_gap_one_convolutionmaskdomain. pvs_le_gap_one_convolutionmaskdomain + (dc_index_one_convolutionmask) = (1)) -> (exists dst_positive_code_one_convolutionmasklookup dst_positive_scale_one_convolutionmasklookup dst_negative_code_one_convolutionmasklookup dst_negative_scale_one_convolutionmasklookup dst_positive_one_convolutionmasklookup dst_negative_one_convolutionmasklookup. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) * S ((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) + ((((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_one_convolutionmasklookuppositive. ff_h_pvs_one_convolutionmasklookuppositive + S (dst_positive_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookuppositive. dst_positive_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookuppositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup) + (dst_positive_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_one_convolutionmasklookupnegative. ff_h_pvs_one_convolutionmasklookupnegative + S (dst_negative_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookupnegative. dst_negative_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookupnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup) + (dst_negative_one_convolutionmasklookup))) /\ (exists ge_balance_positive_one_convolutionmasklookupvalue ge_balance_negative_one_convolutionmasklookupvalue. (((((dc_value_one_convolutionmask) = 2 * (ge_balance_positive_one_convolutionmasklookupvalue) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_one_convolutionmasklookupvaluedecode. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = S ge_signed_half_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_one_convolutionmasklookup) + ge_balance_negative_one_convolutionmasklookupvalue = (dst_negative_one_convolutionmasklookup) + ge_balance_positive_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_one_convolutionmask)=0)) /\ (exists dc_quotient_one_convolutionmaskentry dc_left_one_convolutionmaskentry dc_right_one_convolutionmaskentry. (((1)=(dc_index_one_convolutionmask)*dc_quotient_one_convolutionmaskentry) /\ (((exists dst_positive_code_one_convolutionmaskentryleft dst_positive_scale_one_convolutionmaskentryleft dst_negative_code_one_convolutionmaskentryleft dst_negative_scale_one_convolutionmaskentryleft dst_positive_one_convolutionmaskentryleft dst_negative_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) + ((((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftpositive. ff_h_pvs_one_convolutionmaskentryleftpositive + S (dst_positive_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftpositive. dst_positive_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftpositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftnegative. ff_h_pvs_one_convolutionmaskentryleftnegative + S (dst_negative_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftnegative. dst_negative_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_one_convolutionmaskentryleftvalue ge_balance_negative_one_convolutionmaskentryleftvalue. (((((dc_left_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryleftvaluedecode. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = S ge_signed_half_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryleft) + ge_balance_negative_one_convolutionmaskentryleftvalue = (dst_negative_one_convolutionmaskentryleft) + ge_balance_positive_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_one_convolutionmaskentryright dst_positive_scale_one_convolutionmaskentryright dst_negative_code_one_convolutionmaskentryright dst_negative_scale_one_convolutionmaskentryright dst_positive_one_convolutionmaskentryright dst_negative_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) * S ((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) + ((((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightpositive. ff_h_pvs_one_convolutionmaskentryrightpositive + S (dst_positive_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightpositive. dst_positive_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightnegative. ff_h_pvs_one_convolutionmaskentryrightnegative + S (dst_negative_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightnegative. dst_negative_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_one_convolutionmaskentryrightvalue ge_balance_negative_one_convolutionmaskentryrightvalue. (((((dc_right_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryrightvaluedecode. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = S ge_signed_half_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryright) + ge_balance_negative_one_convolutionmaskentryrightvalue = (dst_negative_one_convolutionmaskentryright) + ge_balance_positive_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_one_convolutionmaskentryproduct sto_an_one_convolutionmaskentryproduct sto_bp_one_convolutionmaskentryproduct sto_bn_one_convolutionmaskentryproduct sto_cp_one_convolutionmaskentryproduct sto_cn_one_convolutionmaskentryproduct. (((((dc_left_one_convolutionmaskentry) = 2 * (sto_ap_one_convolutionmaskentryproduct) /\ (sto_an_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductleft. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_one_convolutionmaskentryproduct) = 0) /\ (sto_an_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_one_convolutionmaskentry) = 2 * (sto_bp_one_convolutionmaskentryproduct) /\ (sto_bn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductright. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductright + 1 /\ (sto_bp_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductright))) /\ ((((((dc_value_one_convolutionmask) = 2 * (sto_cp_one_convolutionmaskentryproduct) /\ (sto_cn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductoutput. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct) + sto_cn_one_convolutionmaskentryproduct = (sto_ap_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct) + sto_cp_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_one_convolutionmask)=0 \/ ~(exists pvs_factor_one_convolutionmaskentrynondivisor. (1) = (dc_index_one_convolutionmask) * pvs_factor_one_convolutionmaskentrynondivisor)) /\ ((dc_value_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_one_convolutionfold dst_positive_scale_one_convolutionfold dst_negative_code_one_convolutionfold dst_negative_scale_one_convolutionfold dst_positive_sum_one_convolutionfold dst_negative_sum_one_convolutionfold. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) * S ((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) + ((((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))))) /\ (((exists fs_u_dst_one_convolutionfoldpositive fs_v_dst_one_convolutionfoldpositive. ((((exists fs_h_dst_one_convolutionfoldpositive_body_start. fs_h_dst_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_start. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_terminal. fs_h_dst_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_terminal. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive) + (dst_positive_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldpositive_body_steps fs_r_dst_one_convolutionfoldpositive_body_steps fs_s_dst_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_one_convolutionfold = fs_q_dst_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_r_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_s_dst_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_one_convolutionfoldpositive_body_steps = fs_r_dst_one_convolutionfoldpositive_body_steps + fs_a_dst_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_one_convolutionfoldnegative fs_v_dst_one_convolutionfoldnegative. ((((exists fs_h_dst_one_convolutionfoldnegative_body_start. fs_h_dst_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_start. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_terminal. fs_h_dst_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_terminal. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative) + (dst_negative_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldnegative_body_steps fs_r_dst_one_convolutionfoldnegative_body_steps fs_s_dst_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_one_convolutionfold = fs_q_dst_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_r_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_s_dst_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_one_convolutionfoldnegative_body_steps = fs_r_dst_one_convolutionfoldnegative_body_steps + fs_a_dst_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_one_convolutionfoldresult ge_balance_negative_one_convolutionfoldresult. (((((z) = 2 * (ge_balance_positive_one_convolutionfoldresult) /\ (ge_balance_negative_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_one_convolutionfoldresultdecode. (((z) = 2 * ge_signed_half_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_one_convolutionfoldresult) = S ge_signed_half_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_one_convolutionfold) + ge_balance_negative_one_convolutionfoldresult = (dst_negative_sum_one_convolutionfold) + ge_balance_positive_one_convolutionfoldresult)))))))))))))))

Complete tactic proof in conservative notation

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

125 script commands · 23 reading checkpoints · 8 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 zero prefix sumdirichlet convolution last entry iffdirichlet convolution prefix last step
01Fix variables and assumptionsL1–7

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro z
  6. L6
    intro ha
  7. L7
    intro hb
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–9

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

  1. L9
    intro hc
04Separate the logical casesL10–12

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

  1. L10
    cases hc
  2. L11
    cases hc_right
  3. L12
    cases hc_right_witness
05Establish hzeroL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution zero prefix sum.

  1. L13
    have hzero : SignedPrefixSum(x,1,0)Definitions: SignedPrefixSum(x,1,0)Original native command in the exact edition
  2. L14
    specialize dirichlet_convolution_zero_prefix_sum (F)
  3. L15
    specialize dirichlet_convolution_zero_prefix_sum (G)
  4. L16
    specialize dirichlet_convolution_zero_prefix_sum (1)
  5. L17
    specialize dirichlet_convolution_zero_prefix_sum (x)
  6. L18
    apply dirichlet_convolution_zero_prefix_sum
  7. L19
    specialize dirichlet_convolution_prefix_restrict (F)
  8. L20
    specialize dirichlet_convolution_prefix_restrict (G)
  9. L21
    specialize dirichlet_convolution_prefix_restrict (1)
  10. L22
    specialize dirichlet_convolution_prefix_restrict (1)
06Use earlier factsL23–28

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

  1. L23
    specialize dirichlet_convolution_prefix_restrict (0)
  2. L24
    specialize dirichlet_convolution_prefix_restrict (x)
  3. L25
    apply dirichlet_convolution_prefix_restrict
  4. L26
    exact hc_right_witness_left
  5. L27
    specialize zero_le (1)
  6. L28
    apply zero_le
07Establish hdL29–34

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

  1. L29
    have hd : ∃ r. ∃ v. SignedPrefixSum(x,1,r) ∧ (ArithAt(x,1,v) ∧ SignedAdd(r,v,z))Definitions: SignedPrefixSum(x,1,r)ArithAt(x,1,v)SignedAdd(r,v,z)Original native command in the exact edition
  2. L30
    specialize divisor_signed_sum_successor_decompose (x)
  3. L31
    specialize divisor_signed_sum_successor_decompose (1)
  4. L32
    specialize divisor_signed_sum_successor_decompose (z)
  5. L33
    apply divisor_signed_sum_successor_decompose
  6. L34
    exact hc_right_witness_right
08Separate the logical casesL35–38

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

  1. L35
    cases hd
  2. L36
    cases hd_witness
  3. L37
    cases hd_witness_witness
  4. L38
    cases hd_witness_witness_right
09Establish hr0L39–48

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

  1. L39
    have hr0 : x1=0
  2. L40
    specialize divisor_signed_sum_functional (x)
  3. L41
    specialize divisor_signed_sum_functional (1)
  4. L42
    specialize divisor_signed_sum_functional (x1)
  5. L43
    specialize divisor_signed_sum_functional (0)
  6. L44
    apply divisor_signed_sum_functional
  7. L45
    exact hd_witness_witness_left
  8. L46
    exact hzero
  9. L47
    rewrite hr0 at hd_witness_witness_right_right
  10. L48
    rewrite hr0 at hd_witness_witness_right_right
10Establish hvL49–58

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

  1. L49
    have hv : x2=z
  2. L50
    symm
  3. L51
    specialize signed_add_functional (0)
  4. L52
    specialize signed_add_functional (x2)
  5. L53
    specialize signed_add_functional (z)
  6. L54
    specialize signed_add_functional (x2)
  7. L55
    apply signed_add_functional
  8. L56
    exact hd_witness_witness_right_right
  9. L57
    specialize signed_add_zero_left (x2)
  10. L58
    apply signed_add_zero_left
11Establish heL59–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution last entry iff.

  1. L59
    have he : (DirichletEntry(F,G,1,1,x2) → SignedMul(a,b,x2)) ∧ (SignedMul(a,b,x2) → DirichletEntry(F,G,1,1,x2))Definitions: DirichletEntry(F,G,1,1,x2)SignedMul(a,b,x2)Original native command in the exact edition
  2. L60
    specialize dirichlet_convolution_last_entry_iff (F)
  3. L61
    specialize dirichlet_convolution_last_entry_iff (G)
  4. L62
    specialize dirichlet_convolution_last_entry_iff (1)
  5. L63
    specialize dirichlet_convolution_last_entry_iff (a)
  6. L64
    specialize dirichlet_convolution_last_entry_iff (b)
  7. L65
    specialize dirichlet_convolution_last_entry_iff (x2)
  8. L66
    apply dirichlet_convolution_last_entry_iff
  9. L67
    intro hn
  10. L68
    apply PA1
12Use earlier factsL69–71

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

  1. L69
    exact hn
  2. L70
    exact ha
  3. L71
    exact hb
13Separate the logical casesL72–72

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

  1. L72
    cases he
14Establish hpL73–82

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

  1. L73
  2. L74
    apply he_left
  3. L75
    specialize dirichlet_convolution_prefix_lookup (F)
  4. L76
    specialize dirichlet_convolution_prefix_lookup (G)
  5. L77
    specialize dirichlet_convolution_prefix_lookup (1)
  6. L78
    specialize dirichlet_convolution_prefix_lookup (1)
  7. L79
    specialize dirichlet_convolution_prefix_lookup (x)
  8. L80
    specialize dirichlet_convolution_prefix_lookup (1)
  9. L81
    specialize dirichlet_convolution_prefix_lookup (x2)
  10. L82
    apply dirichlet_convolution_prefix_lookup
15Use earlier factsL83–86

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

  1. L83
    exact hc_right_witness_left
  2. L84
    specialize le_refl (1)
  3. L85
    apply le_refl
  4. L86
    exact hd_witness_witness_right_left
16Calculate and transport equalitiesL87–88

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

  1. L87
    rewrite hv at hp
  2. L88
    rewrite hv at hp
17Use earlier factsL89–89

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

  1. L89
    exact hp
18Fix variables and assumptionsL90–90

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

  1. L90
    intro hp
19Establish hmL91–93

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

  1. L91
    have hm : ∃ M. ArithTable(0,M) ∧ ArithAt(M,0,0)Definitions: ArithTable(0,M)ArithAt(M,0,0)Original native command in the exact edition
  2. L92
    specialize arithmetic_signed_table_singleton (0)
  3. L93
    apply arithmetic_signed_table_singleton
20Separate the logical casesL94–95

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

  1. L94
    cases hm
  2. L95
    cases hm_witness
21Establish hprefixL96–105

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution prefix zero constructor.

  1. L96
    have hprefix : DirichletPrefix(F,G,1,0,x)Definitions: DirichletPrefix(F,G,1,0,x)Original native command in the exact edition
  2. L97
    specialize dirichlet_convolution_prefix_zero_constructor (F)
  3. L98
    specialize dirichlet_convolution_prefix_zero_constructor (G)
  4. L99
    specialize dirichlet_convolution_prefix_zero_constructor (1)
  5. L100
    specialize dirichlet_convolution_prefix_zero_constructor (x)
  6. L101
    apply dirichlet_convolution_prefix_zero_constructor
  7. L102
    exact hm_witness_left
  8. L103
    exact hm_witness_right
  9. L104
    specialize dirichlet_convolution_prefix_last_step (F)
  10. L105
    specialize dirichlet_convolution_prefix_last_step (G)
22Use earlier factsL106–115

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

  1. L106
    specialize dirichlet_convolution_prefix_last_step (0)
  2. L107
    specialize dirichlet_convolution_prefix_last_step (x)
  3. L108
    specialize dirichlet_convolution_prefix_last_step (0)
  4. L109
    specialize dirichlet_convolution_prefix_last_step (a)
  5. L110
    specialize dirichlet_convolution_prefix_last_step (b)
  6. L111
    specialize dirichlet_convolution_prefix_last_step (z)
  7. L112
    specialize dirichlet_convolution_prefix_last_step (z)
  8. L113
    apply dirichlet_convolution_prefix_last_step
  9. L114
    exact hprefix
  10. L115
    specialize dirichlet_convolution_zero_prefix_sum (F)
23Use earlier factsL116–125

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

  1. L116
    specialize dirichlet_convolution_zero_prefix_sum (G)
  2. L117
    specialize dirichlet_convolution_zero_prefix_sum (1)
  3. L118
    specialize dirichlet_convolution_zero_prefix_sum (x)
  4. L119
    apply dirichlet_convolution_zero_prefix_sum
  5. L120
    exact hprefix
  6. L121
    exact ha
  7. L122
    exact hb
  8. L123
    exact hp
  9. L124
    specialize signed_add_zero_left (z)
  10. L125
    apply signed_add_zero_left

Library-wide reading audit

Original defined command ledger · 125 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro a
  4. 0004intro b
  5. 0005intro z
  6. 0006intro ha
  7. 0007intro hb
  8. 0008split
  9. 0009intro hc
  10. 0010cases hc
  11. 0011cases hc_right
  12. 0012cases hc_right_witness
  13. 0013have hzero : SignedPrefixSum(x,1,0)
  14. 0014specialize dirichlet_convolution_zero_prefix_sum (F)
  15. 0015specialize dirichlet_convolution_zero_prefix_sum (G)
  16. 0016specialize dirichlet_convolution_zero_prefix_sum (1)
  17. 0017specialize dirichlet_convolution_zero_prefix_sum (x)
  18. 0018apply dirichlet_convolution_zero_prefix_sum
  19. 0019specialize dirichlet_convolution_prefix_restrict (F)
  20. 0020specialize dirichlet_convolution_prefix_restrict (G)
  21. 0021specialize dirichlet_convolution_prefix_restrict (1)
  22. 0022specialize dirichlet_convolution_prefix_restrict (1)
  23. 0023specialize dirichlet_convolution_prefix_restrict (0)
  24. 0024specialize dirichlet_convolution_prefix_restrict (x)
  25. 0025apply dirichlet_convolution_prefix_restrict
  26. 0026exact hc_right_witness_left
  27. 0027specialize zero_le (1)
  28. 0028apply zero_le
  29. 0029have hd : ∃ r. ∃ v. SignedPrefixSum(x,1,r) ∧ (ArithAt(x,1,v) ∧ SignedAdd(r,v,z))
  30. 0030specialize divisor_signed_sum_successor_decompose (x)
  31. 0031specialize divisor_signed_sum_successor_decompose (1)
  32. 0032specialize divisor_signed_sum_successor_decompose (z)
  33. 0033apply divisor_signed_sum_successor_decompose
  34. 0034exact hc_right_witness_right
  35. 0035cases hd
  36. 0036cases hd_witness
  37. 0037cases hd_witness_witness
  38. 0038cases hd_witness_witness_right
  39. 0039have hr0 : x1=0
  40. 0040specialize divisor_signed_sum_functional (x)
  41. 0041specialize divisor_signed_sum_functional (1)
  42. 0042specialize divisor_signed_sum_functional (x1)
  43. 0043specialize divisor_signed_sum_functional (0)
  44. 0044apply divisor_signed_sum_functional
  45. 0045exact hd_witness_witness_left
  46. 0046exact hzero
  47. 0047rewrite hr0 at hd_witness_witness_right_right
  48. 0048rewrite hr0 at hd_witness_witness_right_right
  49. 0049have hv : x2=z
  50. 0050symm
  51. 0051specialize signed_add_functional (0)
  52. 0052specialize signed_add_functional (x2)
  53. 0053specialize signed_add_functional (z)
  54. 0054specialize signed_add_functional (x2)
  55. 0055apply signed_add_functional
  56. 0056exact hd_witness_witness_right_right
  57. 0057specialize signed_add_zero_left (x2)
  58. 0058apply signed_add_zero_left
  59. 0059have he : (DirichletEntry(F,G,1,1,x2) → SignedMul(a,b,x2)) ∧ (SignedMul(a,b,x2) → DirichletEntry(F,G,1,1,x2))
  60. 0060specialize dirichlet_convolution_last_entry_iff (F)
  61. 0061specialize dirichlet_convolution_last_entry_iff (G)
  62. 0062specialize dirichlet_convolution_last_entry_iff (1)
  63. 0063specialize dirichlet_convolution_last_entry_iff (a)
  64. 0064specialize dirichlet_convolution_last_entry_iff (b)
  65. 0065specialize dirichlet_convolution_last_entry_iff (x2)
  66. 0066apply dirichlet_convolution_last_entry_iff
  67. 0067intro hn
  68. 0068apply PA1
  69. 0069exact hn
  70. 0070exact ha
  71. 0071exact hb
  72. 0072cases he
  73. 0073have hp : SignedMul(a,b,x2)
  74. 0074apply he_left
  75. 0075specialize dirichlet_convolution_prefix_lookup (F)
  76. 0076specialize dirichlet_convolution_prefix_lookup (G)
  77. 0077specialize dirichlet_convolution_prefix_lookup (1)
  78. 0078specialize dirichlet_convolution_prefix_lookup (1)
  79. 0079specialize dirichlet_convolution_prefix_lookup (x)
  80. 0080specialize dirichlet_convolution_prefix_lookup (1)
  81. 0081specialize dirichlet_convolution_prefix_lookup (x2)
  82. 0082apply dirichlet_convolution_prefix_lookup
  83. 0083exact hc_right_witness_left
  84. 0084specialize le_refl (1)
  85. 0085apply le_refl
  86. 0086exact hd_witness_witness_right_left
  87. 0087rewrite hv at hp
  88. 0088rewrite hv at hp
  89. 0089exact hp
  90. 0090intro hp
  91. 0091have hm : ∃ M. ArithTable(0,M) ∧ ArithAt(M,0,0)
  92. 0092specialize arithmetic_signed_table_singleton (0)
  93. 0093apply arithmetic_signed_table_singleton
  94. 0094cases hm
  95. 0095cases hm_witness
  96. 0096have hprefix : DirichletPrefix(F,G,1,0,x)
  97. 0097specialize dirichlet_convolution_prefix_zero_constructor (F)
  98. 0098specialize dirichlet_convolution_prefix_zero_constructor (G)
  99. 0099specialize dirichlet_convolution_prefix_zero_constructor (1)
  100. 0100specialize dirichlet_convolution_prefix_zero_constructor (x)
  101. 0101apply dirichlet_convolution_prefix_zero_constructor
  102. 0102exact hm_witness_left
  103. 0103exact hm_witness_right
  104. 0104specialize dirichlet_convolution_prefix_last_step (F)
  105. 0105specialize dirichlet_convolution_prefix_last_step (G)
  106. 0106specialize dirichlet_convolution_prefix_last_step (0)
  107. 0107specialize dirichlet_convolution_prefix_last_step (x)
  108. 0108specialize dirichlet_convolution_prefix_last_step (0)
  109. 0109specialize dirichlet_convolution_prefix_last_step (a)
  110. 0110specialize dirichlet_convolution_prefix_last_step (b)
  111. 0111specialize dirichlet_convolution_prefix_last_step (z)
  112. 0112specialize dirichlet_convolution_prefix_last_step (z)
  113. 0113apply dirichlet_convolution_prefix_last_step
  114. 0114exact hprefix
  115. 0115specialize dirichlet_convolution_zero_prefix_sum (F)
  116. 0116specialize dirichlet_convolution_zero_prefix_sum (G)
  117. 0117specialize dirichlet_convolution_zero_prefix_sum (1)
  118. 0118specialize dirichlet_convolution_zero_prefix_sum (x)
  119. 0119apply dirichlet_convolution_zero_prefix_sum
  120. 0120exact hprefix
  121. 0121exact ha
  122. 0122exact hb
  123. 0123exact hp
  124. 0124specialize signed_add_zero_left (z)
  125. 0125apply signed_add_zero_left