DC0010

dirichlet_convolution_sum_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Construct the actual weighted divisor prefix and its S n-entry signed fold at every positive in-domain input.

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

Exact expanded first-order arithmetic statement

forall N F G n. (exists dst_positive_code_sum_total_left dst_positive_scale_sum_total_left dst_negative_code_sum_total_left dst_negative_scale_sum_total_left. (((F) = (((((dst_positive_code_sum_total_left) + (dst_positive_scale_sum_total_left)) * S ((dst_positive_code_sum_total_left) + (dst_positive_scale_sum_total_left)) + ((dst_positive_scale_sum_total_left) + (dst_positive_scale_sum_total_left))) + (((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) * S ((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) + ((dst_negative_scale_sum_total_left) + (dst_negative_scale_sum_total_left)))) * S ((((dst_positive_code_sum_total_left) + (dst_positive_scale_sum_total_left)) * S ((dst_positive_code_sum_total_left) + (dst_positive_scale_sum_total_left)) + ((dst_positive_scale_sum_total_left) + (dst_positive_scale_sum_total_left))) + (((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) * S ((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) + ((dst_negative_scale_sum_total_left) + (dst_negative_scale_sum_total_left)))) + ((((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) * S ((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) + ((dst_negative_scale_sum_total_left) + (dst_negative_scale_sum_total_left))) + (((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) * S ((dst_negative_code_sum_total_left) + (dst_negative_scale_sum_total_left)) + ((dst_negative_scale_sum_total_left) + (dst_negative_scale_sum_total_left)))))) /\ (forall dst_index_sum_total_left. (exists pvs_le_gap_sum_total_leftdomain. pvs_le_gap_sum_total_leftdomain + (dst_index_sum_total_left) = (N)) -> exists dst_positive_sum_total_left dst_negative_sum_total_left dst_value_sum_total_left. ((((exists ff_h_pvs_sum_total_leftentrypositive. ff_h_pvs_sum_total_leftentrypositive + S (dst_positive_sum_total_left) = S ((S (dst_index_sum_total_left)) * dst_positive_scale_sum_total_left)) /\ exists ff_q_pvs_sum_total_leftentrypositive. dst_positive_code_sum_total_left = ff_q_pvs_sum_total_leftentrypositive * S ((S (dst_index_sum_total_left)) * dst_positive_scale_sum_total_left) + (dst_positive_sum_total_left))) /\ (((((exists ff_h_pvs_sum_total_leftentrynegative. ff_h_pvs_sum_total_leftentrynegative + S (dst_negative_sum_total_left) = S ((S (dst_index_sum_total_left)) * dst_negative_scale_sum_total_left)) /\ exists ff_q_pvs_sum_total_leftentrynegative. dst_negative_code_sum_total_left = ff_q_pvs_sum_total_leftentrynegative * S ((S (dst_index_sum_total_left)) * dst_negative_scale_sum_total_left) + (dst_negative_sum_total_left))) /\ (exists ge_balance_positive_sum_total_leftentryvalue ge_balance_negative_sum_total_leftentryvalue. (((((dst_value_sum_total_left) = 2 * (ge_balance_positive_sum_total_leftentryvalue) /\ (ge_balance_negative_sum_total_leftentryvalue) = 0) \/ exists ge_signed_half_sum_total_leftentryvaluedecode. (((dst_value_sum_total_left) = 2 * ge_signed_half_sum_total_leftentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_leftentryvalue) = 0) /\ (ge_balance_negative_sum_total_leftentryvalue) = S ge_signed_half_sum_total_leftentryvaluedecode))) /\ ((dst_positive_sum_total_left) + ge_balance_negative_sum_total_leftentryvalue = (dst_negative_sum_total_left) + ge_balance_positive_sum_total_leftentryvalue))))))))) -> (exists dst_positive_code_sum_total_right dst_positive_scale_sum_total_right dst_negative_code_sum_total_right dst_negative_scale_sum_total_right. (((G) = (((((dst_positive_code_sum_total_right) + (dst_positive_scale_sum_total_right)) * S ((dst_positive_code_sum_total_right) + (dst_positive_scale_sum_total_right)) + ((dst_positive_scale_sum_total_right) + (dst_positive_scale_sum_total_right))) + (((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) * S ((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) + ((dst_negative_scale_sum_total_right) + (dst_negative_scale_sum_total_right)))) * S ((((dst_positive_code_sum_total_right) + (dst_positive_scale_sum_total_right)) * S ((dst_positive_code_sum_total_right) + (dst_positive_scale_sum_total_right)) + ((dst_positive_scale_sum_total_right) + (dst_positive_scale_sum_total_right))) + (((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) * S ((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) + ((dst_negative_scale_sum_total_right) + (dst_negative_scale_sum_total_right)))) + ((((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) * S ((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) + ((dst_negative_scale_sum_total_right) + (dst_negative_scale_sum_total_right))) + (((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) * S ((dst_negative_code_sum_total_right) + (dst_negative_scale_sum_total_right)) + ((dst_negative_scale_sum_total_right) + (dst_negative_scale_sum_total_right)))))) /\ (forall dst_index_sum_total_right. (exists pvs_le_gap_sum_total_rightdomain. pvs_le_gap_sum_total_rightdomain + (dst_index_sum_total_right) = (N)) -> exists dst_positive_sum_total_right dst_negative_sum_total_right dst_value_sum_total_right. ((((exists ff_h_pvs_sum_total_rightentrypositive. ff_h_pvs_sum_total_rightentrypositive + S (dst_positive_sum_total_right) = S ((S (dst_index_sum_total_right)) * dst_positive_scale_sum_total_right)) /\ exists ff_q_pvs_sum_total_rightentrypositive. dst_positive_code_sum_total_right = ff_q_pvs_sum_total_rightentrypositive * S ((S (dst_index_sum_total_right)) * dst_positive_scale_sum_total_right) + (dst_positive_sum_total_right))) /\ (((((exists ff_h_pvs_sum_total_rightentrynegative. ff_h_pvs_sum_total_rightentrynegative + S (dst_negative_sum_total_right) = S ((S (dst_index_sum_total_right)) * dst_negative_scale_sum_total_right)) /\ exists ff_q_pvs_sum_total_rightentrynegative. dst_negative_code_sum_total_right = ff_q_pvs_sum_total_rightentrynegative * S ((S (dst_index_sum_total_right)) * dst_negative_scale_sum_total_right) + (dst_negative_sum_total_right))) /\ (exists ge_balance_positive_sum_total_rightentryvalue ge_balance_negative_sum_total_rightentryvalue. (((((dst_value_sum_total_right) = 2 * (ge_balance_positive_sum_total_rightentryvalue) /\ (ge_balance_negative_sum_total_rightentryvalue) = 0) \/ exists ge_signed_half_sum_total_rightentryvaluedecode. (((dst_value_sum_total_right) = 2 * ge_signed_half_sum_total_rightentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_rightentryvalue) = 0) /\ (ge_balance_negative_sum_total_rightentryvalue) = S ge_signed_half_sum_total_rightentryvaluedecode))) /\ ((dst_positive_sum_total_right) + ge_balance_negative_sum_total_rightentryvalue = (dst_negative_sum_total_right) + ge_balance_positive_sum_total_rightentryvalue))))))))) -> ~(n=0) -> (exists pvs_le_gap_sum_total_bound. pvs_le_gap_sum_total_bound + (n) = (N)) -> exists z. (((~((n)=0)) /\ (exists dc_mask_sum_total_result. ((((exists dst_positive_code_sum_total_resultmasktable dst_positive_scale_sum_total_resultmasktable dst_negative_code_sum_total_resultmasktable dst_negative_scale_sum_total_resultmasktable. (((dc_mask_sum_total_result) = (((((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) * S ((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) + ((dst_positive_scale_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))) * S ((((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) * S ((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) + ((dst_positive_scale_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))) + ((((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))))) /\ (forall dst_index_sum_total_resultmasktable. (exists pvs_le_gap_sum_total_resultmasktabledomain. pvs_le_gap_sum_total_resultmasktabledomain + (dst_index_sum_total_resultmasktable) = (n)) -> exists dst_positive_sum_total_resultmasktable dst_negative_sum_total_resultmasktable dst_value_sum_total_resultmasktable. ((((exists ff_h_pvs_sum_total_resultmasktableentrypositive. ff_h_pvs_sum_total_resultmasktableentrypositive + S (dst_positive_sum_total_resultmasktable) = S ((S (dst_index_sum_total_resultmasktable)) * dst_positive_scale_sum_total_resultmasktable)) /\ exists ff_q_pvs_sum_total_resultmasktableentrypositive. dst_positive_code_sum_total_resultmasktable = ff_q_pvs_sum_total_resultmasktableentrypositive * S ((S (dst_index_sum_total_resultmasktable)) * dst_positive_scale_sum_total_resultmasktable) + (dst_positive_sum_total_resultmasktable))) /\ (((((exists ff_h_pvs_sum_total_resultmasktableentrynegative. ff_h_pvs_sum_total_resultmasktableentrynegative + S (dst_negative_sum_total_resultmasktable) = S ((S (dst_index_sum_total_resultmasktable)) * dst_negative_scale_sum_total_resultmasktable)) /\ exists ff_q_pvs_sum_total_resultmasktableentrynegative. dst_negative_code_sum_total_resultmasktable = ff_q_pvs_sum_total_resultmasktableentrynegative * S ((S (dst_index_sum_total_resultmasktable)) * dst_negative_scale_sum_total_resultmasktable) + (dst_negative_sum_total_resultmasktable))) /\ (exists ge_balance_positive_sum_total_resultmasktableentryvalue ge_balance_negative_sum_total_resultmasktableentryvalue. (((((dst_value_sum_total_resultmasktable) = 2 * (ge_balance_positive_sum_total_resultmasktableentryvalue) /\ (ge_balance_negative_sum_total_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_total_resultmasktableentryvaluedecode. (((dst_value_sum_total_resultmasktable) = 2 * ge_signed_half_sum_total_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_total_resultmasktableentryvalue) = S ge_signed_half_sum_total_resultmasktableentryvaluedecode))) /\ ((dst_positive_sum_total_resultmasktable) + ge_balance_negative_sum_total_resultmasktableentryvalue = (dst_negative_sum_total_resultmasktable) + ge_balance_positive_sum_total_resultmasktableentryvalue))))))))) /\ (forall dc_index_sum_total_resultmask dc_value_sum_total_resultmask. (exists pvs_le_gap_sum_total_resultmaskdomain. pvs_le_gap_sum_total_resultmaskdomain + (dc_index_sum_total_resultmask) = (n)) -> (exists dst_positive_code_sum_total_resultmasklookup dst_positive_scale_sum_total_resultmasklookup dst_negative_code_sum_total_resultmasklookup dst_negative_scale_sum_total_resultmasklookup dst_positive_sum_total_resultmasklookup dst_negative_sum_total_resultmasklookup. (((dc_mask_sum_total_result) = (((((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) * S ((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) + ((dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))) * S ((((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) * S ((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) + ((dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))) + ((((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))))) /\ (((((exists ff_h_pvs_sum_total_resultmasklookuppositive. ff_h_pvs_sum_total_resultmasklookuppositive + S (dst_positive_sum_total_resultmasklookup) = S ((S (dc_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmasklookup)) /\ exists ff_q_pvs_sum_total_resultmasklookuppositive. dst_positive_code_sum_total_resultmasklookup = ff_q_pvs_sum_total_resultmasklookuppositive * S ((S (dc_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_sum_total_resultmasklookup))) /\ (((((exists ff_h_pvs_sum_total_resultmasklookupnegative. ff_h_pvs_sum_total_resultmasklookupnegative + S (dst_negative_sum_total_resultmasklookup) = S ((S (dc_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmasklookup)) /\ exists ff_q_pvs_sum_total_resultmasklookupnegative. dst_negative_code_sum_total_resultmasklookup = ff_q_pvs_sum_total_resultmasklookupnegative * S ((S (dc_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_sum_total_resultmasklookup))) /\ (exists ge_balance_positive_sum_total_resultmasklookupvalue ge_balance_negative_sum_total_resultmasklookupvalue. (((((dc_value_sum_total_resultmask) = 2 * (ge_balance_positive_sum_total_resultmasklookupvalue) /\ (ge_balance_negative_sum_total_resultmasklookupvalue) = 0) \/ exists ge_signed_half_sum_total_resultmasklookupvaluedecode. (((dc_value_sum_total_resultmask) = 2 * ge_signed_half_sum_total_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmasklookupvalue) = 0) /\ (ge_balance_negative_sum_total_resultmasklookupvalue) = S ge_signed_half_sum_total_resultmasklookupvaluedecode))) /\ ((dst_positive_sum_total_resultmasklookup) + ge_balance_negative_sum_total_resultmasklookupvalue = (dst_negative_sum_total_resultmasklookup) + ge_balance_positive_sum_total_resultmasklookupvalue))))))))) -> ((((~((dc_index_sum_total_resultmask)=0)) /\ (exists dc_quotient_sum_total_resultmaskentry dc_left_sum_total_resultmaskentry dc_right_sum_total_resultmaskentry. (((n)=(dc_index_sum_total_resultmask)*dc_quotient_sum_total_resultmaskentry) /\ (((exists dst_positive_code_sum_total_resultmaskentryleft dst_positive_scale_sum_total_resultmaskentryleft dst_negative_code_sum_total_resultmaskentryleft dst_negative_scale_sum_total_resultmaskentryleft dst_positive_sum_total_resultmaskentryleft dst_negative_sum_total_resultmaskentryleft. (((F) = (((((dst_positive_code_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft)) * S ((dst_positive_code_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft)) + ((dst_positive_scale_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft))) + (((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) * S ((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) + ((dst_negative_scale_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)))) * S ((((dst_positive_code_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft)) * S ((dst_positive_code_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft)) + ((dst_positive_scale_sum_total_resultmaskentryleft) + (dst_positive_scale_sum_total_resultmaskentryleft))) + (((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) * S ((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) + ((dst_negative_scale_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)))) + ((((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) * S ((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) + ((dst_negative_scale_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft))) + (((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) * S ((dst_negative_code_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)) + ((dst_negative_scale_sum_total_resultmaskentryleft) + (dst_negative_scale_sum_total_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryleftpositive. ff_h_pvs_sum_total_resultmaskentryleftpositive + S (dst_positive_sum_total_resultmaskentryleft) = S ((S (dc_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryleft)) /\ exists ff_q_pvs_sum_total_resultmaskentryleftpositive. dst_positive_code_sum_total_resultmaskentryleft = ff_q_pvs_sum_total_resultmaskentryleftpositive * S ((S (dc_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryleft) + (dst_positive_sum_total_resultmaskentryleft))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryleftnegative. ff_h_pvs_sum_total_resultmaskentryleftnegative + S (dst_negative_sum_total_resultmaskentryleft) = S ((S (dc_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryleft)) /\ exists ff_q_pvs_sum_total_resultmaskentryleftnegative. dst_negative_code_sum_total_resultmaskentryleft = ff_q_pvs_sum_total_resultmaskentryleftnegative * S ((S (dc_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryleft) + (dst_negative_sum_total_resultmaskentryleft))) /\ (exists ge_balance_positive_sum_total_resultmaskentryleftvalue ge_balance_negative_sum_total_resultmaskentryleftvalue. (((((dc_left_sum_total_resultmaskentry) = 2 * (ge_balance_positive_sum_total_resultmaskentryleftvalue) /\ (ge_balance_negative_sum_total_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryleftvaluedecode. (((dc_left_sum_total_resultmaskentry) = 2 * ge_signed_half_sum_total_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_total_resultmaskentryleftvalue) = S ge_signed_half_sum_total_resultmaskentryleftvaluedecode))) /\ ((dst_positive_sum_total_resultmaskentryleft) + ge_balance_negative_sum_total_resultmaskentryleftvalue = (dst_negative_sum_total_resultmaskentryleft) + ge_balance_positive_sum_total_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_total_resultmaskentryright dst_positive_scale_sum_total_resultmaskentryright dst_negative_code_sum_total_resultmaskentryright dst_negative_scale_sum_total_resultmaskentryright dst_positive_sum_total_resultmaskentryright dst_negative_sum_total_resultmaskentryright. (((G) = (((((dst_positive_code_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright)) * S ((dst_positive_code_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright)) + ((dst_positive_scale_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright))) + (((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) * S ((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) + ((dst_negative_scale_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)))) * S ((((dst_positive_code_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright)) * S ((dst_positive_code_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright)) + ((dst_positive_scale_sum_total_resultmaskentryright) + (dst_positive_scale_sum_total_resultmaskentryright))) + (((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) * S ((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) + ((dst_negative_scale_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)))) + ((((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) * S ((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) + ((dst_negative_scale_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright))) + (((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) * S ((dst_negative_code_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)) + ((dst_negative_scale_sum_total_resultmaskentryright) + (dst_negative_scale_sum_total_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryrightpositive. ff_h_pvs_sum_total_resultmaskentryrightpositive + S (dst_positive_sum_total_resultmaskentryright) = S ((S (dc_quotient_sum_total_resultmaskentry)) * dst_positive_scale_sum_total_resultmaskentryright)) /\ exists ff_q_pvs_sum_total_resultmaskentryrightpositive. dst_positive_code_sum_total_resultmaskentryright = ff_q_pvs_sum_total_resultmaskentryrightpositive * S ((S (dc_quotient_sum_total_resultmaskentry)) * dst_positive_scale_sum_total_resultmaskentryright) + (dst_positive_sum_total_resultmaskentryright))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryrightnegative. ff_h_pvs_sum_total_resultmaskentryrightnegative + S (dst_negative_sum_total_resultmaskentryright) = S ((S (dc_quotient_sum_total_resultmaskentry)) * dst_negative_scale_sum_total_resultmaskentryright)) /\ exists ff_q_pvs_sum_total_resultmaskentryrightnegative. dst_negative_code_sum_total_resultmaskentryright = ff_q_pvs_sum_total_resultmaskentryrightnegative * S ((S (dc_quotient_sum_total_resultmaskentry)) * dst_negative_scale_sum_total_resultmaskentryright) + (dst_negative_sum_total_resultmaskentryright))) /\ (exists ge_balance_positive_sum_total_resultmaskentryrightvalue ge_balance_negative_sum_total_resultmaskentryrightvalue. (((((dc_right_sum_total_resultmaskentry) = 2 * (ge_balance_positive_sum_total_resultmaskentryrightvalue) /\ (ge_balance_negative_sum_total_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryrightvaluedecode. (((dc_right_sum_total_resultmaskentry) = 2 * ge_signed_half_sum_total_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_total_resultmaskentryrightvalue) = S ge_signed_half_sum_total_resultmaskentryrightvaluedecode))) /\ ((dst_positive_sum_total_resultmaskentryright) + ge_balance_negative_sum_total_resultmaskentryrightvalue = (dst_negative_sum_total_resultmaskentryright) + ge_balance_positive_sum_total_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_sum_total_resultmaskentryproduct sto_an_sum_total_resultmaskentryproduct sto_bp_sum_total_resultmaskentryproduct sto_bn_sum_total_resultmaskentryproduct sto_cp_sum_total_resultmaskentryproduct sto_cn_sum_total_resultmaskentryproduct. (((((dc_left_sum_total_resultmaskentry) = 2 * (sto_ap_sum_total_resultmaskentryproduct) /\ (sto_an_sum_total_resultmaskentryproduct) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryproductleft. (((dc_left_sum_total_resultmaskentry) = 2 * ge_signed_half_sum_total_resultmaskentryproductleft + 1 /\ (sto_ap_sum_total_resultmaskentryproduct) = 0) /\ (sto_an_sum_total_resultmaskentryproduct) = S ge_signed_half_sum_total_resultmaskentryproductleft))) /\ ((((((dc_right_sum_total_resultmaskentry) = 2 * (sto_bp_sum_total_resultmaskentryproduct) /\ (sto_bn_sum_total_resultmaskentryproduct) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryproductright. (((dc_right_sum_total_resultmaskentry) = 2 * ge_signed_half_sum_total_resultmaskentryproductright + 1 /\ (sto_bp_sum_total_resultmaskentryproduct) = 0) /\ (sto_bn_sum_total_resultmaskentryproduct) = S ge_signed_half_sum_total_resultmaskentryproductright))) /\ ((((((dc_value_sum_total_resultmask) = 2 * (sto_cp_sum_total_resultmaskentryproduct) /\ (sto_cn_sum_total_resultmaskentryproduct) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryproductoutput. (((dc_value_sum_total_resultmask) = 2 * ge_signed_half_sum_total_resultmaskentryproductoutput + 1 /\ (sto_cp_sum_total_resultmaskentryproduct) = 0) /\ (sto_cn_sum_total_resultmaskentryproduct) = S ge_signed_half_sum_total_resultmaskentryproductoutput))) /\ ((sto_ap_sum_total_resultmaskentryproduct * sto_bp_sum_total_resultmaskentryproduct + sto_an_sum_total_resultmaskentryproduct * sto_bn_sum_total_resultmaskentryproduct) + sto_cn_sum_total_resultmaskentryproduct = (sto_ap_sum_total_resultmaskentryproduct * sto_bn_sum_total_resultmaskentryproduct + sto_an_sum_total_resultmaskentryproduct * sto_bp_sum_total_resultmaskentryproduct) + sto_cp_sum_total_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_sum_total_resultmask)=0 \/ ~(exists pvs_factor_sum_total_resultmaskentrynondivisor. (n) = (dc_index_sum_total_resultmask) * pvs_factor_sum_total_resultmaskentrynondivisor)) /\ ((dc_value_sum_total_resultmask)=0))))))) /\ (exists dst_positive_code_sum_total_resultfold dst_positive_scale_sum_total_resultfold dst_negative_code_sum_total_resultfold dst_negative_scale_sum_total_resultfold dst_positive_sum_sum_total_resultfold dst_negative_sum_sum_total_resultfold. (((dc_mask_sum_total_result) = (((((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) * S ((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) + ((dst_positive_scale_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))) * S ((((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) * S ((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) + ((dst_positive_scale_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))) + ((((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))))) /\ (((exists fs_u_dst_sum_total_resultfoldpositive fs_v_dst_sum_total_resultfoldpositive. ((((exists fs_h_dst_sum_total_resultfoldpositive_body_start. fs_h_dst_sum_total_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_start. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_total_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_terminal. fs_h_dst_sum_total_resultfoldpositive_body_terminal + S (dst_positive_sum_sum_total_resultfold) = S ((S (S (n))) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_terminal. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_total_resultfoldpositive) + (dst_positive_sum_sum_total_resultfold))) /\ forall fs_i_dst_sum_total_resultfoldpositive_body_steps. (exists fs_lt_dst_sum_total_resultfoldpositive_body_steps_bound. fs_lt_dst_sum_total_resultfoldpositive_body_steps_bound + S fs_i_dst_sum_total_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_total_resultfoldpositive_body_steps fs_r_dst_sum_total_resultfoldpositive_body_steps fs_s_dst_sum_total_resultfoldpositive_body_steps. ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_summand. fs_h_dst_sum_total_resultfoldpositive_body_steps_summand + S (fs_a_dst_sum_total_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * dst_positive_scale_sum_total_resultfold)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_summand. dst_positive_code_sum_total_resultfold = fs_q_dst_sum_total_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * dst_positive_scale_sum_total_resultfold) + (fs_a_dst_sum_total_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_partial. fs_h_dst_sum_total_resultfoldpositive_body_steps_partial + S (fs_r_dst_sum_total_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_partial. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive) + (fs_r_dst_sum_total_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_successor. fs_h_dst_sum_total_resultfoldpositive_body_steps_successor + S (fs_s_dst_sum_total_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_successor. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive) + (fs_s_dst_sum_total_resultfoldpositive_body_steps))) /\ fs_s_dst_sum_total_resultfoldpositive_body_steps = fs_r_dst_sum_total_resultfoldpositive_body_steps + fs_a_dst_sum_total_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_total_resultfoldnegative fs_v_dst_sum_total_resultfoldnegative. ((((exists fs_h_dst_sum_total_resultfoldnegative_body_start. fs_h_dst_sum_total_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_start. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_total_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_terminal. fs_h_dst_sum_total_resultfoldnegative_body_terminal + S (dst_negative_sum_sum_total_resultfold) = S ((S (S (n))) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_terminal. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_total_resultfoldnegative) + (dst_negative_sum_sum_total_resultfold))) /\ forall fs_i_dst_sum_total_resultfoldnegative_body_steps. (exists fs_lt_dst_sum_total_resultfoldnegative_body_steps_bound. fs_lt_dst_sum_total_resultfoldnegative_body_steps_bound + S fs_i_dst_sum_total_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_total_resultfoldnegative_body_steps fs_r_dst_sum_total_resultfoldnegative_body_steps fs_s_dst_sum_total_resultfoldnegative_body_steps. ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_summand. fs_h_dst_sum_total_resultfoldnegative_body_steps_summand + S (fs_a_dst_sum_total_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * dst_negative_scale_sum_total_resultfold)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_summand. dst_negative_code_sum_total_resultfold = fs_q_dst_sum_total_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * dst_negative_scale_sum_total_resultfold) + (fs_a_dst_sum_total_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_partial. fs_h_dst_sum_total_resultfoldnegative_body_steps_partial + S (fs_r_dst_sum_total_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_partial. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative) + (fs_r_dst_sum_total_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_successor. fs_h_dst_sum_total_resultfoldnegative_body_steps_successor + S (fs_s_dst_sum_total_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_successor. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative) + (fs_s_dst_sum_total_resultfoldnegative_body_steps))) /\ fs_s_dst_sum_total_resultfoldnegative_body_steps = fs_r_dst_sum_total_resultfoldnegative_body_steps + fs_a_dst_sum_total_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_total_resultfoldresult ge_balance_negative_sum_total_resultfoldresult. (((((z) = 2 * (ge_balance_positive_sum_total_resultfoldresult) /\ (ge_balance_negative_sum_total_resultfoldresult) = 0) \/ exists ge_signed_half_sum_total_resultfoldresultdecode. (((z) = 2 * ge_signed_half_sum_total_resultfoldresultdecode + 1 /\ (ge_balance_positive_sum_total_resultfoldresult) = 0) /\ (ge_balance_negative_sum_total_resultfoldresult) = S ge_signed_half_sum_total_resultfoldresultdecode))) /\ ((dst_positive_sum_sum_total_resultfold) + ge_balance_negative_sum_total_resultfoldresult = (dst_negative_sum_sum_total_resultfold) + ge_balance_positive_sum_total_resultfoldresult)))))))))))))

Constructive proof overview

Generated structural guide

Construct the actual weighted divisor prefix and its S n-entry signed fold at every positive in-domain input.

The unchanged tactic script uses 3 declared prerequisites and contains 40 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DC000A dirichlet_convolution_prefix_exists signed_table_domain_resize Alpha theorem; checked-use authorized arithmetic_signed_sum_exists Alpha theorem; checked-use authorized

Direct dependents

DC0012 dirichlet_convolution_sum_exists_unique DC0017 dirichlet_convolution_positive_source_transport DC001A dirichlet_convolution_table_exists DC0023 dirichlet_convolution_sum_swap

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

40 script commands · 12 reading checkpoints · 2 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.

Named ingredients (1)
dirichlet convolution prefix exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro n
  5. L5
    intro hF
  6. L6
    intro hG
  7. L7
    intro hn
  8. L8
    intro hbound
02Establish hmL9–18

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

  1. L9
    have hm : ∃ M. DirichletPrefix(F,G,n,n,M)Definitions: DirichletPrefix
  2. L10
    specialize dirichlet_convolution_prefix_exists (F)
  3. L11
    specialize dirichlet_convolution_prefix_exists (G)
  4. L12
    specialize dirichlet_convolution_prefix_exists (n)
  5. L13
    specialize dirichlet_convolution_prefix_exists (n)
  6. L14
    apply dirichlet_convolution_prefix_exists
  7. L15
    specialize signed_table_domain_resize (N)
  8. L16
    specialize signed_table_domain_resize (0)
  9. L17
    specialize signed_table_domain_resize (F)
  10. L18
    apply signed_table_domain_resize
03Use earlier factsL19–24

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

  1. L19
    exact hF
  2. L20
    specialize signed_table_domain_resize (N)
  3. L21
    specialize signed_table_domain_resize (0)
  4. L22
    specialize signed_table_domain_resize (G)
  5. L23
    apply signed_table_domain_resize
  6. L24
    exact hG
04Separate the logical casesL25–26

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

  1. L25
    cases hm
  2. L26
    cases hm_witness
05Establish hzL27–32

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

  1. L27
    have hz : ∃ z. SignedPrefixSum(x,S n,z)Definitions: SignedPrefixSum
  2. L28
    specialize arithmetic_signed_sum_exists (n)
  3. L29
    specialize arithmetic_signed_sum_exists (x)
  4. L30
    specialize arithmetic_signed_sum_exists (S n)
  5. L31
    apply arithmetic_signed_sum_exists
  6. L32
    exact hm_witness_left
06Separate the logical casesL33–33

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

  1. L33
    cases hz
07Construct an explicit witnessL34–34

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

  1. L34
    exists x1
08Separate the logical casesL35–35

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

  1. L35
    split
09Use earlier factsL36–36

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

  1. L36
    exact hn
10Construct an explicit witnessL37–37

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

  1. L37
    exists x
11Separate the logical casesL38–38

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

  1. L38
    split
12Use earlier factsL39–40

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

  1. L39
    exact hm_witness
  2. L40
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 40 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro G
  4. 0004intro n
  5. 0005intro hF
  6. 0006intro hG
  7. 0007intro hn
  8. 0008intro hbound
  9. 0009have hm : exists M. (((exists dst_positive_code_sum_total_prefixtable dst_positive_scale_sum_total_prefixtable dst_negative_code_sum_total_prefixtable dst_negative_scale_sum_total_prefixtable. (((M) = (((((dst_positive_code_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable)) * S ((dst_positive_code_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable)) + ((dst_positive_scale_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable))) + (((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) * S ((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) + ((dst_negative_scale_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)))) * S ((((dst_positive_code_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable)) * S ((dst_positive_code_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable)) + ((dst_positive_scale_sum_total_prefixtable) + (dst_positive_scale_sum_total_prefixtable))) + (((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) * S ((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) + ((dst_negative_scale_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)))) + ((((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) * S ((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) + ((dst_negative_scale_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable))) + (((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) * S ((dst_negative_code_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)) + ((dst_negative_scale_sum_total_prefixtable) + (dst_negative_scale_sum_total_prefixtable)))))) /\ (forall dst_index_sum_total_prefixtable. (exists pvs_le_gap_sum_total_prefixtabledomain. pvs_le_gap_sum_total_prefixtabledomain + (dst_index_sum_total_prefixtable) = (n)) -> exists dst_positive_sum_total_prefixtable dst_negative_sum_total_prefixtable dst_value_sum_total_prefixtable. ((((exists ff_h_pvs_sum_total_prefixtableentrypositive. ff_h_pvs_sum_total_prefixtableentrypositive + S (dst_positive_sum_total_prefixtable) = S ((S (dst_index_sum_total_prefixtable)) * dst_positive_scale_sum_total_prefixtable)) /\ exists ff_q_pvs_sum_total_prefixtableentrypositive. dst_positive_code_sum_total_prefixtable = ff_q_pvs_sum_total_prefixtableentrypositive * S ((S (dst_index_sum_total_prefixtable)) * dst_positive_scale_sum_total_prefixtable) + (dst_positive_sum_total_prefixtable))) /\ (((((exists ff_h_pvs_sum_total_prefixtableentrynegative. ff_h_pvs_sum_total_prefixtableentrynegative + S (dst_negative_sum_total_prefixtable) = S ((S (dst_index_sum_total_prefixtable)) * dst_negative_scale_sum_total_prefixtable)) /\ exists ff_q_pvs_sum_total_prefixtableentrynegative. dst_negative_code_sum_total_prefixtable = ff_q_pvs_sum_total_prefixtableentrynegative * S ((S (dst_index_sum_total_prefixtable)) * dst_negative_scale_sum_total_prefixtable) + (dst_negative_sum_total_prefixtable))) /\ (exists ge_balance_positive_sum_total_prefixtableentryvalue ge_balance_negative_sum_total_prefixtableentryvalue. (((((dst_value_sum_total_prefixtable) = 2 * (ge_balance_positive_sum_total_prefixtableentryvalue) /\ (ge_balance_negative_sum_total_prefixtableentryvalue) = 0) \/ exists ge_signed_half_sum_total_prefixtableentryvaluedecode. (((dst_value_sum_total_prefixtable) = 2 * ge_signed_half_sum_total_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_prefixtableentryvalue) = 0) /\ (ge_balance_negative_sum_total_prefixtableentryvalue) = S ge_signed_half_sum_total_prefixtableentryvaluedecode))) /\ ((dst_positive_sum_total_prefixtable) + ge_balance_negative_sum_total_prefixtableentryvalue = (dst_negative_sum_total_prefixtable) + ge_balance_positive_sum_total_prefixtableentryvalue))))))))) /\ (forall dc_index_sum_total_prefix dc_value_sum_total_prefix. (exists pvs_le_gap_sum_total_prefixdomain. pvs_le_gap_sum_total_prefixdomain + (dc_index_sum_total_prefix) = (n)) -> (exists dst_positive_code_sum_total_prefixlookup dst_positive_scale_sum_total_prefixlookup dst_negative_code_sum_total_prefixlookup dst_negative_scale_sum_total_prefixlookup dst_positive_sum_total_prefixlookup dst_negative_sum_total_prefixlookup. (((M) = (((((dst_positive_code_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup)) * S ((dst_positive_code_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup)) + ((dst_positive_scale_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup))) + (((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) * S ((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) + ((dst_negative_scale_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)))) * S ((((dst_positive_code_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup)) * S ((dst_positive_code_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup)) + ((dst_positive_scale_sum_total_prefixlookup) + (dst_positive_scale_sum_total_prefixlookup))) + (((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) * S ((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) + ((dst_negative_scale_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)))) + ((((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) * S ((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) + ((dst_negative_scale_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup))) + (((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) * S ((dst_negative_code_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)) + ((dst_negative_scale_sum_total_prefixlookup) + (dst_negative_scale_sum_total_prefixlookup)))))) /\ (((((exists ff_h_pvs_sum_total_prefixlookuppositive. ff_h_pvs_sum_total_prefixlookuppositive + S (dst_positive_sum_total_prefixlookup) = S ((S (dc_index_sum_total_prefix)) * dst_positive_scale_sum_total_prefixlookup)) /\ exists ff_q_pvs_sum_total_prefixlookuppositive. dst_positive_code_sum_total_prefixlookup = ff_q_pvs_sum_total_prefixlookuppositive * S ((S (dc_index_sum_total_prefix)) * dst_positive_scale_sum_total_prefixlookup) + (dst_positive_sum_total_prefixlookup))) /\ (((((exists ff_h_pvs_sum_total_prefixlookupnegative. ff_h_pvs_sum_total_prefixlookupnegative + S (dst_negative_sum_total_prefixlookup) = S ((S (dc_index_sum_total_prefix)) * dst_negative_scale_sum_total_prefixlookup)) /\ exists ff_q_pvs_sum_total_prefixlookupnegative. dst_negative_code_sum_total_prefixlookup = ff_q_pvs_sum_total_prefixlookupnegative * S ((S (dc_index_sum_total_prefix)) * dst_negative_scale_sum_total_prefixlookup) + (dst_negative_sum_total_prefixlookup))) /\ (exists ge_balance_positive_sum_total_prefixlookupvalue ge_balance_negative_sum_total_prefixlookupvalue. (((((dc_value_sum_total_prefix) = 2 * (ge_balance_positive_sum_total_prefixlookupvalue) /\ (ge_balance_negative_sum_total_prefixlookupvalue) = 0) \/ exists ge_signed_half_sum_total_prefixlookupvaluedecode. (((dc_value_sum_total_prefix) = 2 * ge_signed_half_sum_total_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_sum_total_prefixlookupvalue) = 0) /\ (ge_balance_negative_sum_total_prefixlookupvalue) = S ge_signed_half_sum_total_prefixlookupvaluedecode))) /\ ((dst_positive_sum_total_prefixlookup) + ge_balance_negative_sum_total_prefixlookupvalue = (dst_negative_sum_total_prefixlookup) + ge_balance_positive_sum_total_prefixlookupvalue))))))))) -> ((((~((dc_index_sum_total_prefix)=0)) /\ (exists dc_quotient_sum_total_prefixentry dc_left_sum_total_prefixentry dc_right_sum_total_prefixentry. (((n)=(dc_index_sum_total_prefix)*dc_quotient_sum_total_prefixentry) /\ (((exists dst_positive_code_sum_total_prefixentryleft dst_positive_scale_sum_total_prefixentryleft dst_negative_code_sum_total_prefixentryleft dst_negative_scale_sum_total_prefixentryleft dst_positive_sum_total_prefixentryleft dst_negative_sum_total_prefixentryleft. (((F) = (((((dst_positive_code_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft)) * S ((dst_positive_code_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft)) + ((dst_positive_scale_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft))) + (((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) * S ((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) + ((dst_negative_scale_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)))) * S ((((dst_positive_code_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft)) * S ((dst_positive_code_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft)) + ((dst_positive_scale_sum_total_prefixentryleft) + (dst_positive_scale_sum_total_prefixentryleft))) + (((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) * S ((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) + ((dst_negative_scale_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)))) + ((((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) * S ((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) + ((dst_negative_scale_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft))) + (((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) * S ((dst_negative_code_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)) + ((dst_negative_scale_sum_total_prefixentryleft) + (dst_negative_scale_sum_total_prefixentryleft)))))) /\ (((((exists ff_h_pvs_sum_total_prefixentryleftpositive. ff_h_pvs_sum_total_prefixentryleftpositive + S (dst_positive_sum_total_prefixentryleft) = S ((S (dc_index_sum_total_prefix)) * dst_positive_scale_sum_total_prefixentryleft)) /\ exists ff_q_pvs_sum_total_prefixentryleftpositive. dst_positive_code_sum_total_prefixentryleft = ff_q_pvs_sum_total_prefixentryleftpositive * S ((S (dc_index_sum_total_prefix)) * dst_positive_scale_sum_total_prefixentryleft) + (dst_positive_sum_total_prefixentryleft))) /\ (((((exists ff_h_pvs_sum_total_prefixentryleftnegative. ff_h_pvs_sum_total_prefixentryleftnegative + S (dst_negative_sum_total_prefixentryleft) = S ((S (dc_index_sum_total_prefix)) * dst_negative_scale_sum_total_prefixentryleft)) /\ exists ff_q_pvs_sum_total_prefixentryleftnegative. dst_negative_code_sum_total_prefixentryleft = ff_q_pvs_sum_total_prefixentryleftnegative * S ((S (dc_index_sum_total_prefix)) * dst_negative_scale_sum_total_prefixentryleft) + (dst_negative_sum_total_prefixentryleft))) /\ (exists ge_balance_positive_sum_total_prefixentryleftvalue ge_balance_negative_sum_total_prefixentryleftvalue. (((((dc_left_sum_total_prefixentry) = 2 * (ge_balance_positive_sum_total_prefixentryleftvalue) /\ (ge_balance_negative_sum_total_prefixentryleftvalue) = 0) \/ exists ge_signed_half_sum_total_prefixentryleftvaluedecode. (((dc_left_sum_total_prefixentry) = 2 * ge_signed_half_sum_total_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_total_prefixentryleftvalue) = 0) /\ (ge_balance_negative_sum_total_prefixentryleftvalue) = S ge_signed_half_sum_total_prefixentryleftvaluedecode))) /\ ((dst_positive_sum_total_prefixentryleft) + ge_balance_negative_sum_total_prefixentryleftvalue = (dst_negative_sum_total_prefixentryleft) + ge_balance_positive_sum_total_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_total_prefixentryright dst_positive_scale_sum_total_prefixentryright dst_negative_code_sum_total_prefixentryright dst_negative_scale_sum_total_prefixentryright dst_positive_sum_total_prefixentryright dst_negative_sum_total_prefixentryright. (((G) = (((((dst_positive_code_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright)) * S ((dst_positive_code_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright)) + ((dst_positive_scale_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright))) + (((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) * S ((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) + ((dst_negative_scale_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)))) * S ((((dst_positive_code_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright)) * S ((dst_positive_code_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright)) + ((dst_positive_scale_sum_total_prefixentryright) + (dst_positive_scale_sum_total_prefixentryright))) + (((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) * S ((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) + ((dst_negative_scale_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)))) + ((((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) * S ((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) + ((dst_negative_scale_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright))) + (((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) * S ((dst_negative_code_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)) + ((dst_negative_scale_sum_total_prefixentryright) + (dst_negative_scale_sum_total_prefixentryright)))))) /\ (((((exists ff_h_pvs_sum_total_prefixentryrightpositive. ff_h_pvs_sum_total_prefixentryrightpositive + S (dst_positive_sum_total_prefixentryright) = S ((S (dc_quotient_sum_total_prefixentry)) * dst_positive_scale_sum_total_prefixentryright)) /\ exists ff_q_pvs_sum_total_prefixentryrightpositive. dst_positive_code_sum_total_prefixentryright = ff_q_pvs_sum_total_prefixentryrightpositive * S ((S (dc_quotient_sum_total_prefixentry)) * dst_positive_scale_sum_total_prefixentryright) + (dst_positive_sum_total_prefixentryright))) /\ (((((exists ff_h_pvs_sum_total_prefixentryrightnegative. ff_h_pvs_sum_total_prefixentryrightnegative + S (dst_negative_sum_total_prefixentryright) = S ((S (dc_quotient_sum_total_prefixentry)) * dst_negative_scale_sum_total_prefixentryright)) /\ exists ff_q_pvs_sum_total_prefixentryrightnegative. dst_negative_code_sum_total_prefixentryright = ff_q_pvs_sum_total_prefixentryrightnegative * S ((S (dc_quotient_sum_total_prefixentry)) * dst_negative_scale_sum_total_prefixentryright) + (dst_negative_sum_total_prefixentryright))) /\ (exists ge_balance_positive_sum_total_prefixentryrightvalue ge_balance_negative_sum_total_prefixentryrightvalue. (((((dc_right_sum_total_prefixentry) = 2 * (ge_balance_positive_sum_total_prefixentryrightvalue) /\ (ge_balance_negative_sum_total_prefixentryrightvalue) = 0) \/ exists ge_signed_half_sum_total_prefixentryrightvaluedecode. (((dc_right_sum_total_prefixentry) = 2 * ge_signed_half_sum_total_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_total_prefixentryrightvalue) = 0) /\ (ge_balance_negative_sum_total_prefixentryrightvalue) = S ge_signed_half_sum_total_prefixentryrightvaluedecode))) /\ ((dst_positive_sum_total_prefixentryright) + ge_balance_negative_sum_total_prefixentryrightvalue = (dst_negative_sum_total_prefixentryright) + ge_balance_positive_sum_total_prefixentryrightvalue))))))))) /\ (exists sto_ap_sum_total_prefixentryproduct sto_an_sum_total_prefixentryproduct sto_bp_sum_total_prefixentryproduct sto_bn_sum_total_prefixentryproduct sto_cp_sum_total_prefixentryproduct sto_cn_sum_total_prefixentryproduct. (((((dc_left_sum_total_prefixentry) = 2 * (sto_ap_sum_total_prefixentryproduct) /\ (sto_an_sum_total_prefixentryproduct) = 0) \/ exists ge_signed_half_sum_total_prefixentryproductleft. (((dc_left_sum_total_prefixentry) = 2 * ge_signed_half_sum_total_prefixentryproductleft + 1 /\ (sto_ap_sum_total_prefixentryproduct) = 0) /\ (sto_an_sum_total_prefixentryproduct) = S ge_signed_half_sum_total_prefixentryproductleft))) /\ ((((((dc_right_sum_total_prefixentry) = 2 * (sto_bp_sum_total_prefixentryproduct) /\ (sto_bn_sum_total_prefixentryproduct) = 0) \/ exists ge_signed_half_sum_total_prefixentryproductright. (((dc_right_sum_total_prefixentry) = 2 * ge_signed_half_sum_total_prefixentryproductright + 1 /\ (sto_bp_sum_total_prefixentryproduct) = 0) /\ (sto_bn_sum_total_prefixentryproduct) = S ge_signed_half_sum_total_prefixentryproductright))) /\ ((((((dc_value_sum_total_prefix) = 2 * (sto_cp_sum_total_prefixentryproduct) /\ (sto_cn_sum_total_prefixentryproduct) = 0) \/ exists ge_signed_half_sum_total_prefixentryproductoutput. (((dc_value_sum_total_prefix) = 2 * ge_signed_half_sum_total_prefixentryproductoutput + 1 /\ (sto_cp_sum_total_prefixentryproduct) = 0) /\ (sto_cn_sum_total_prefixentryproduct) = S ge_signed_half_sum_total_prefixentryproductoutput))) /\ ((sto_ap_sum_total_prefixentryproduct * sto_bp_sum_total_prefixentryproduct + sto_an_sum_total_prefixentryproduct * sto_bn_sum_total_prefixentryproduct) + sto_cn_sum_total_prefixentryproduct = (sto_ap_sum_total_prefixentryproduct * sto_bn_sum_total_prefixentryproduct + sto_an_sum_total_prefixentryproduct * sto_bp_sum_total_prefixentryproduct) + sto_cp_sum_total_prefixentryproduct))))))))))))))) \/ ((((dc_index_sum_total_prefix)=0 \/ ~(exists pvs_factor_sum_total_prefixentrynondivisor. (n) = (dc_index_sum_total_prefix) * pvs_factor_sum_total_prefixentrynondivisor)) /\ ((dc_value_sum_total_prefix)=0)))))))
  10. 0010specialize dirichlet_convolution_prefix_exists (F)
  11. 0011specialize dirichlet_convolution_prefix_exists (G)
  12. 0012specialize dirichlet_convolution_prefix_exists (n)
  13. 0013specialize dirichlet_convolution_prefix_exists (n)
  14. 0014apply dirichlet_convolution_prefix_exists
  15. 0015specialize signed_table_domain_resize (N)
  16. 0016specialize signed_table_domain_resize (0)
  17. 0017specialize signed_table_domain_resize (F)
  18. 0018apply signed_table_domain_resize
  19. 0019exact hF
  20. 0020specialize signed_table_domain_resize (N)
  21. 0021specialize signed_table_domain_resize (0)
  22. 0022specialize signed_table_domain_resize (G)
  23. 0023apply signed_table_domain_resize
  24. 0024exact hG
  25. 0025cases hm
  26. 0026cases hm_witness
  27. 0027have hz : exists z. (exists dst_positive_code_sum_total_fold dst_positive_scale_sum_total_fold dst_negative_code_sum_total_fold dst_negative_scale_sum_total_fold dst_positive_sum_sum_total_fold dst_negative_sum_sum_total_fold. (((x) = (((((dst_positive_code_sum_total_fold) + (dst_positive_scale_sum_total_fold)) * S ((dst_positive_code_sum_total_fold) + (dst_positive_scale_sum_total_fold)) + ((dst_positive_scale_sum_total_fold) + (dst_positive_scale_sum_total_fold))) + (((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) * S ((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) + ((dst_negative_scale_sum_total_fold) + (dst_negative_scale_sum_total_fold)))) * S ((((dst_positive_code_sum_total_fold) + (dst_positive_scale_sum_total_fold)) * S ((dst_positive_code_sum_total_fold) + (dst_positive_scale_sum_total_fold)) + ((dst_positive_scale_sum_total_fold) + (dst_positive_scale_sum_total_fold))) + (((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) * S ((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) + ((dst_negative_scale_sum_total_fold) + (dst_negative_scale_sum_total_fold)))) + ((((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) * S ((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) + ((dst_negative_scale_sum_total_fold) + (dst_negative_scale_sum_total_fold))) + (((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) * S ((dst_negative_code_sum_total_fold) + (dst_negative_scale_sum_total_fold)) + ((dst_negative_scale_sum_total_fold) + (dst_negative_scale_sum_total_fold)))))) /\ (((exists fs_u_dst_sum_total_foldpositive fs_v_dst_sum_total_foldpositive. ((((exists fs_h_dst_sum_total_foldpositive_body_start. fs_h_dst_sum_total_foldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_foldpositive)) /\ exists fs_q_dst_sum_total_foldpositive_body_start. fs_u_dst_sum_total_foldpositive = fs_q_dst_sum_total_foldpositive_body_start * S ((S (0)) * fs_v_dst_sum_total_foldpositive) + (0))) /\ ((((exists fs_h_dst_sum_total_foldpositive_body_terminal. fs_h_dst_sum_total_foldpositive_body_terminal + S (dst_positive_sum_sum_total_fold) = S ((S (S n)) * fs_v_dst_sum_total_foldpositive)) /\ exists fs_q_dst_sum_total_foldpositive_body_terminal. fs_u_dst_sum_total_foldpositive = fs_q_dst_sum_total_foldpositive_body_terminal * S ((S (S n)) * fs_v_dst_sum_total_foldpositive) + (dst_positive_sum_sum_total_fold))) /\ forall fs_i_dst_sum_total_foldpositive_body_steps. (exists fs_lt_dst_sum_total_foldpositive_body_steps_bound. fs_lt_dst_sum_total_foldpositive_body_steps_bound + S fs_i_dst_sum_total_foldpositive_body_steps = S n) -> exists fs_a_dst_sum_total_foldpositive_body_steps fs_r_dst_sum_total_foldpositive_body_steps fs_s_dst_sum_total_foldpositive_body_steps. ((((exists fs_h_dst_sum_total_foldpositive_body_steps_summand. fs_h_dst_sum_total_foldpositive_body_steps_summand + S (fs_a_dst_sum_total_foldpositive_body_steps) = S ((S (fs_i_dst_sum_total_foldpositive_body_steps)) * dst_positive_scale_sum_total_fold)) /\ exists fs_q_dst_sum_total_foldpositive_body_steps_summand. dst_positive_code_sum_total_fold = fs_q_dst_sum_total_foldpositive_body_steps_summand * S ((S (fs_i_dst_sum_total_foldpositive_body_steps)) * dst_positive_scale_sum_total_fold) + (fs_a_dst_sum_total_foldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_foldpositive_body_steps_partial. fs_h_dst_sum_total_foldpositive_body_steps_partial + S (fs_r_dst_sum_total_foldpositive_body_steps) = S ((S (fs_i_dst_sum_total_foldpositive_body_steps)) * fs_v_dst_sum_total_foldpositive)) /\ exists fs_q_dst_sum_total_foldpositive_body_steps_partial. fs_u_dst_sum_total_foldpositive = fs_q_dst_sum_total_foldpositive_body_steps_partial * S ((S (fs_i_dst_sum_total_foldpositive_body_steps)) * fs_v_dst_sum_total_foldpositive) + (fs_r_dst_sum_total_foldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_foldpositive_body_steps_successor. fs_h_dst_sum_total_foldpositive_body_steps_successor + S (fs_s_dst_sum_total_foldpositive_body_steps) = S ((S (S fs_i_dst_sum_total_foldpositive_body_steps)) * fs_v_dst_sum_total_foldpositive)) /\ exists fs_q_dst_sum_total_foldpositive_body_steps_successor. fs_u_dst_sum_total_foldpositive = fs_q_dst_sum_total_foldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_total_foldpositive_body_steps)) * fs_v_dst_sum_total_foldpositive) + (fs_s_dst_sum_total_foldpositive_body_steps))) /\ fs_s_dst_sum_total_foldpositive_body_steps = fs_r_dst_sum_total_foldpositive_body_steps + fs_a_dst_sum_total_foldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_total_foldnegative fs_v_dst_sum_total_foldnegative. ((((exists fs_h_dst_sum_total_foldnegative_body_start. fs_h_dst_sum_total_foldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_foldnegative)) /\ exists fs_q_dst_sum_total_foldnegative_body_start. fs_u_dst_sum_total_foldnegative = fs_q_dst_sum_total_foldnegative_body_start * S ((S (0)) * fs_v_dst_sum_total_foldnegative) + (0))) /\ ((((exists fs_h_dst_sum_total_foldnegative_body_terminal. fs_h_dst_sum_total_foldnegative_body_terminal + S (dst_negative_sum_sum_total_fold) = S ((S (S n)) * fs_v_dst_sum_total_foldnegative)) /\ exists fs_q_dst_sum_total_foldnegative_body_terminal. fs_u_dst_sum_total_foldnegative = fs_q_dst_sum_total_foldnegative_body_terminal * S ((S (S n)) * fs_v_dst_sum_total_foldnegative) + (dst_negative_sum_sum_total_fold))) /\ forall fs_i_dst_sum_total_foldnegative_body_steps. (exists fs_lt_dst_sum_total_foldnegative_body_steps_bound. fs_lt_dst_sum_total_foldnegative_body_steps_bound + S fs_i_dst_sum_total_foldnegative_body_steps = S n) -> exists fs_a_dst_sum_total_foldnegative_body_steps fs_r_dst_sum_total_foldnegative_body_steps fs_s_dst_sum_total_foldnegative_body_steps. ((((exists fs_h_dst_sum_total_foldnegative_body_steps_summand. fs_h_dst_sum_total_foldnegative_body_steps_summand + S (fs_a_dst_sum_total_foldnegative_body_steps) = S ((S (fs_i_dst_sum_total_foldnegative_body_steps)) * dst_negative_scale_sum_total_fold)) /\ exists fs_q_dst_sum_total_foldnegative_body_steps_summand. dst_negative_code_sum_total_fold = fs_q_dst_sum_total_foldnegative_body_steps_summand * S ((S (fs_i_dst_sum_total_foldnegative_body_steps)) * dst_negative_scale_sum_total_fold) + (fs_a_dst_sum_total_foldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_foldnegative_body_steps_partial. fs_h_dst_sum_total_foldnegative_body_steps_partial + S (fs_r_dst_sum_total_foldnegative_body_steps) = S ((S (fs_i_dst_sum_total_foldnegative_body_steps)) * fs_v_dst_sum_total_foldnegative)) /\ exists fs_q_dst_sum_total_foldnegative_body_steps_partial. fs_u_dst_sum_total_foldnegative = fs_q_dst_sum_total_foldnegative_body_steps_partial * S ((S (fs_i_dst_sum_total_foldnegative_body_steps)) * fs_v_dst_sum_total_foldnegative) + (fs_r_dst_sum_total_foldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_foldnegative_body_steps_successor. fs_h_dst_sum_total_foldnegative_body_steps_successor + S (fs_s_dst_sum_total_foldnegative_body_steps) = S ((S (S fs_i_dst_sum_total_foldnegative_body_steps)) * fs_v_dst_sum_total_foldnegative)) /\ exists fs_q_dst_sum_total_foldnegative_body_steps_successor. fs_u_dst_sum_total_foldnegative = fs_q_dst_sum_total_foldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_total_foldnegative_body_steps)) * fs_v_dst_sum_total_foldnegative) + (fs_s_dst_sum_total_foldnegative_body_steps))) /\ fs_s_dst_sum_total_foldnegative_body_steps = fs_r_dst_sum_total_foldnegative_body_steps + fs_a_dst_sum_total_foldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_total_foldresult ge_balance_negative_sum_total_foldresult. (((((z) = 2 * (ge_balance_positive_sum_total_foldresult) /\ (ge_balance_negative_sum_total_foldresult) = 0) \/ exists ge_signed_half_sum_total_foldresultdecode. (((z) = 2 * ge_signed_half_sum_total_foldresultdecode + 1 /\ (ge_balance_positive_sum_total_foldresult) = 0) /\ (ge_balance_negative_sum_total_foldresult) = S ge_signed_half_sum_total_foldresultdecode))) /\ ((dst_positive_sum_sum_total_fold) + ge_balance_negative_sum_total_foldresult = (dst_negative_sum_sum_total_fold) + ge_balance_positive_sum_total_foldresult)))))))))
  28. 0028specialize arithmetic_signed_sum_exists (n)
  29. 0029specialize arithmetic_signed_sum_exists (x)
  30. 0030specialize arithmetic_signed_sum_exists (S n)
  31. 0031apply arithmetic_signed_sum_exists
  32. 0032exact hm_witness_left
  33. 0033cases hz
  34. 0034exists x1
  35. 0035split
  36. 0036exact hn
  37. 0037exists x
  38. 0038split
  39. 0039exact hm_witness
  40. 0040exact hz_witness