DT0006

dirichlet_convolution_strict_prefix_exists

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

Actually construct the remainder prefix through k and its S k-entry fold even when the first input is only an inclusive k-table; the arbitrary value at S k is excluded.

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 k F G. (exists dst_positive_code_remainder_fixed_input dst_positive_scale_remainder_fixed_input dst_negative_code_remainder_fixed_input dst_negative_scale_remainder_fixed_input. (((F) = (((((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) * S ((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) + ((dst_positive_scale_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))) * S ((((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) * S ((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) + ((dst_positive_scale_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))) + ((((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))))) /\ (forall dst_index_remainder_fixed_input. (exists pvs_le_gap_remainder_fixed_inputdomain. pvs_le_gap_remainder_fixed_inputdomain + (dst_index_remainder_fixed_input) = (N)) -> exists dst_positive_remainder_fixed_input dst_negative_remainder_fixed_input dst_value_remainder_fixed_input. ((((exists ff_h_pvs_remainder_fixed_inputentrypositive. ff_h_pvs_remainder_fixed_inputentrypositive + S (dst_positive_remainder_fixed_input) = S ((S (dst_index_remainder_fixed_input)) * dst_positive_scale_remainder_fixed_input)) /\ exists ff_q_pvs_remainder_fixed_inputentrypositive. dst_positive_code_remainder_fixed_input = ff_q_pvs_remainder_fixed_inputentrypositive * S ((S (dst_index_remainder_fixed_input)) * dst_positive_scale_remainder_fixed_input) + (dst_positive_remainder_fixed_input))) /\ (((((exists ff_h_pvs_remainder_fixed_inputentrynegative. ff_h_pvs_remainder_fixed_inputentrynegative + S (dst_negative_remainder_fixed_input) = S ((S (dst_index_remainder_fixed_input)) * dst_negative_scale_remainder_fixed_input)) /\ exists ff_q_pvs_remainder_fixed_inputentrynegative. dst_negative_code_remainder_fixed_input = ff_q_pvs_remainder_fixed_inputentrynegative * S ((S (dst_index_remainder_fixed_input)) * dst_negative_scale_remainder_fixed_input) + (dst_negative_remainder_fixed_input))) /\ (exists ge_balance_positive_remainder_fixed_inputentryvalue ge_balance_negative_remainder_fixed_inputentryvalue. (((((dst_value_remainder_fixed_input) = 2 * (ge_balance_positive_remainder_fixed_inputentryvalue) /\ (ge_balance_negative_remainder_fixed_inputentryvalue) = 0) \/ exists ge_signed_half_remainder_fixed_inputentryvaluedecode. (((dst_value_remainder_fixed_input) = 2 * ge_signed_half_remainder_fixed_inputentryvaluedecode + 1 /\ (ge_balance_positive_remainder_fixed_inputentryvalue) = 0) /\ (ge_balance_negative_remainder_fixed_inputentryvalue) = S ge_signed_half_remainder_fixed_inputentryvaluedecode))) /\ ((dst_positive_remainder_fixed_input) + ge_balance_negative_remainder_fixed_inputentryvalue = (dst_negative_remainder_fixed_input) + ge_balance_positive_remainder_fixed_inputentryvalue))))))))) -> (exists dst_positive_code_remainder_partial_input dst_positive_scale_remainder_partial_input dst_negative_code_remainder_partial_input dst_negative_scale_remainder_partial_input. (((G) = (((((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) * S ((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) + ((dst_positive_scale_remainder_partial_input) + (dst_positive_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))) * S ((((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) * S ((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) + ((dst_positive_scale_remainder_partial_input) + (dst_positive_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))) + ((((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))))) /\ (forall dst_index_remainder_partial_input. (exists pvs_le_gap_remainder_partial_inputdomain. pvs_le_gap_remainder_partial_inputdomain + (dst_index_remainder_partial_input) = (k)) -> exists dst_positive_remainder_partial_input dst_negative_remainder_partial_input dst_value_remainder_partial_input. ((((exists ff_h_pvs_remainder_partial_inputentrypositive. ff_h_pvs_remainder_partial_inputentrypositive + S (dst_positive_remainder_partial_input) = S ((S (dst_index_remainder_partial_input)) * dst_positive_scale_remainder_partial_input)) /\ exists ff_q_pvs_remainder_partial_inputentrypositive. dst_positive_code_remainder_partial_input = ff_q_pvs_remainder_partial_inputentrypositive * S ((S (dst_index_remainder_partial_input)) * dst_positive_scale_remainder_partial_input) + (dst_positive_remainder_partial_input))) /\ (((((exists ff_h_pvs_remainder_partial_inputentrynegative. ff_h_pvs_remainder_partial_inputentrynegative + S (dst_negative_remainder_partial_input) = S ((S (dst_index_remainder_partial_input)) * dst_negative_scale_remainder_partial_input)) /\ exists ff_q_pvs_remainder_partial_inputentrynegative. dst_negative_code_remainder_partial_input = ff_q_pvs_remainder_partial_inputentrynegative * S ((S (dst_index_remainder_partial_input)) * dst_negative_scale_remainder_partial_input) + (dst_negative_remainder_partial_input))) /\ (exists ge_balance_positive_remainder_partial_inputentryvalue ge_balance_negative_remainder_partial_inputentryvalue. (((((dst_value_remainder_partial_input) = 2 * (ge_balance_positive_remainder_partial_inputentryvalue) /\ (ge_balance_negative_remainder_partial_inputentryvalue) = 0) \/ exists ge_signed_half_remainder_partial_inputentryvaluedecode. (((dst_value_remainder_partial_input) = 2 * ge_signed_half_remainder_partial_inputentryvaluedecode + 1 /\ (ge_balance_positive_remainder_partial_inputentryvalue) = 0) /\ (ge_balance_negative_remainder_partial_inputentryvalue) = S ge_signed_half_remainder_partial_inputentryvaluedecode))) /\ ((dst_positive_remainder_partial_input) + ge_balance_negative_remainder_partial_inputentryvalue = (dst_negative_remainder_partial_input) + ge_balance_positive_remainder_partial_inputentryvalue))))))))) -> exists M r. (((exists dst_positive_code_remainder_result_prefixtable dst_positive_scale_remainder_result_prefixtable dst_negative_code_remainder_result_prefixtable dst_negative_scale_remainder_result_prefixtable. (((M) = (((((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) * S ((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) + ((dst_positive_scale_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))) * S ((((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) * S ((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) + ((dst_positive_scale_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))) + ((((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))))) /\ (forall dst_index_remainder_result_prefixtable. (exists pvs_le_gap_remainder_result_prefixtabledomain. pvs_le_gap_remainder_result_prefixtabledomain + (dst_index_remainder_result_prefixtable) = (k)) -> exists dst_positive_remainder_result_prefixtable dst_negative_remainder_result_prefixtable dst_value_remainder_result_prefixtable. ((((exists ff_h_pvs_remainder_result_prefixtableentrypositive. ff_h_pvs_remainder_result_prefixtableentrypositive + S (dst_positive_remainder_result_prefixtable) = S ((S (dst_index_remainder_result_prefixtable)) * dst_positive_scale_remainder_result_prefixtable)) /\ exists ff_q_pvs_remainder_result_prefixtableentrypositive. dst_positive_code_remainder_result_prefixtable = ff_q_pvs_remainder_result_prefixtableentrypositive * S ((S (dst_index_remainder_result_prefixtable)) * dst_positive_scale_remainder_result_prefixtable) + (dst_positive_remainder_result_prefixtable))) /\ (((((exists ff_h_pvs_remainder_result_prefixtableentrynegative. ff_h_pvs_remainder_result_prefixtableentrynegative + S (dst_negative_remainder_result_prefixtable) = S ((S (dst_index_remainder_result_prefixtable)) * dst_negative_scale_remainder_result_prefixtable)) /\ exists ff_q_pvs_remainder_result_prefixtableentrynegative. dst_negative_code_remainder_result_prefixtable = ff_q_pvs_remainder_result_prefixtableentrynegative * S ((S (dst_index_remainder_result_prefixtable)) * dst_negative_scale_remainder_result_prefixtable) + (dst_negative_remainder_result_prefixtable))) /\ (exists ge_balance_positive_remainder_result_prefixtableentryvalue ge_balance_negative_remainder_result_prefixtableentryvalue. (((((dst_value_remainder_result_prefixtable) = 2 * (ge_balance_positive_remainder_result_prefixtableentryvalue) /\ (ge_balance_negative_remainder_result_prefixtableentryvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixtableentryvaluedecode. (((dst_value_remainder_result_prefixtable) = 2 * ge_signed_half_remainder_result_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixtableentryvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixtableentryvalue) = S ge_signed_half_remainder_result_prefixtableentryvaluedecode))) /\ ((dst_positive_remainder_result_prefixtable) + ge_balance_negative_remainder_result_prefixtableentryvalue = (dst_negative_remainder_result_prefixtable) + ge_balance_positive_remainder_result_prefixtableentryvalue))))))))) /\ (forall dc_index_remainder_result_prefix dc_value_remainder_result_prefix. (exists pvs_le_gap_remainder_result_prefixdomain. pvs_le_gap_remainder_result_prefixdomain + (dc_index_remainder_result_prefix) = (k)) -> (exists dst_positive_code_remainder_result_prefixlookup dst_positive_scale_remainder_result_prefixlookup dst_negative_code_remainder_result_prefixlookup dst_negative_scale_remainder_result_prefixlookup dst_positive_remainder_result_prefixlookup dst_negative_remainder_result_prefixlookup. (((M) = (((((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) * S ((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) + ((dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))) * S ((((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) * S ((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) + ((dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))) + ((((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixlookuppositive. ff_h_pvs_remainder_result_prefixlookuppositive + S (dst_positive_remainder_result_prefixlookup) = S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixlookup)) /\ exists ff_q_pvs_remainder_result_prefixlookuppositive. dst_positive_code_remainder_result_prefixlookup = ff_q_pvs_remainder_result_prefixlookuppositive * S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_remainder_result_prefixlookup))) /\ (((((exists ff_h_pvs_remainder_result_prefixlookupnegative. ff_h_pvs_remainder_result_prefixlookupnegative + S (dst_negative_remainder_result_prefixlookup) = S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixlookup)) /\ exists ff_q_pvs_remainder_result_prefixlookupnegative. dst_negative_code_remainder_result_prefixlookup = ff_q_pvs_remainder_result_prefixlookupnegative * S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_remainder_result_prefixlookup))) /\ (exists ge_balance_positive_remainder_result_prefixlookupvalue ge_balance_negative_remainder_result_prefixlookupvalue. (((((dc_value_remainder_result_prefix) = 2 * (ge_balance_positive_remainder_result_prefixlookupvalue) /\ (ge_balance_negative_remainder_result_prefixlookupvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixlookupvaluedecode. (((dc_value_remainder_result_prefix) = 2 * ge_signed_half_remainder_result_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixlookupvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixlookupvalue) = S ge_signed_half_remainder_result_prefixlookupvaluedecode))) /\ ((dst_positive_remainder_result_prefixlookup) + ge_balance_negative_remainder_result_prefixlookupvalue = (dst_negative_remainder_result_prefixlookup) + ge_balance_positive_remainder_result_prefixlookupvalue))))))))) -> ((((~((dc_index_remainder_result_prefix)=0)) /\ (exists dc_quotient_remainder_result_prefixentry dc_left_remainder_result_prefixentry dc_right_remainder_result_prefixentry. (((S k)=(dc_index_remainder_result_prefix)*dc_quotient_remainder_result_prefixentry) /\ (((exists dst_positive_code_remainder_result_prefixentryleft dst_positive_scale_remainder_result_prefixentryleft dst_negative_code_remainder_result_prefixentryleft dst_negative_scale_remainder_result_prefixentryleft dst_positive_remainder_result_prefixentryleft dst_negative_remainder_result_prefixentryleft. (((G) = (((((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) * S ((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) + ((dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))) * S ((((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) * S ((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) + ((dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))) + ((((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryleftpositive. ff_h_pvs_remainder_result_prefixentryleftpositive + S (dst_positive_remainder_result_prefixentryleft) = S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixentryleft)) /\ exists ff_q_pvs_remainder_result_prefixentryleftpositive. dst_positive_code_remainder_result_prefixentryleft = ff_q_pvs_remainder_result_prefixentryleftpositive * S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_remainder_result_prefixentryleft))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryleftnegative. ff_h_pvs_remainder_result_prefixentryleftnegative + S (dst_negative_remainder_result_prefixentryleft) = S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixentryleft)) /\ exists ff_q_pvs_remainder_result_prefixentryleftnegative. dst_negative_code_remainder_result_prefixentryleft = ff_q_pvs_remainder_result_prefixentryleftnegative * S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_remainder_result_prefixentryleft))) /\ (exists ge_balance_positive_remainder_result_prefixentryleftvalue ge_balance_negative_remainder_result_prefixentryleftvalue. (((((dc_left_remainder_result_prefixentry) = 2 * (ge_balance_positive_remainder_result_prefixentryleftvalue) /\ (ge_balance_negative_remainder_result_prefixentryleftvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixentryleftvaluedecode. (((dc_left_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixentryleftvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixentryleftvalue) = S ge_signed_half_remainder_result_prefixentryleftvaluedecode))) /\ ((dst_positive_remainder_result_prefixentryleft) + ge_balance_negative_remainder_result_prefixentryleftvalue = (dst_negative_remainder_result_prefixentryleft) + ge_balance_positive_remainder_result_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_remainder_result_prefixentryright dst_positive_scale_remainder_result_prefixentryright dst_negative_code_remainder_result_prefixentryright dst_negative_scale_remainder_result_prefixentryright dst_positive_remainder_result_prefixentryright dst_negative_remainder_result_prefixentryright. (((F) = (((((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) * S ((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) + ((dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))) * S ((((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) * S ((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) + ((dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))) + ((((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryrightpositive. ff_h_pvs_remainder_result_prefixentryrightpositive + S (dst_positive_remainder_result_prefixentryright) = S ((S (dc_quotient_remainder_result_prefixentry)) * dst_positive_scale_remainder_result_prefixentryright)) /\ exists ff_q_pvs_remainder_result_prefixentryrightpositive. dst_positive_code_remainder_result_prefixentryright = ff_q_pvs_remainder_result_prefixentryrightpositive * S ((S (dc_quotient_remainder_result_prefixentry)) * dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_remainder_result_prefixentryright))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryrightnegative. ff_h_pvs_remainder_result_prefixentryrightnegative + S (dst_negative_remainder_result_prefixentryright) = S ((S (dc_quotient_remainder_result_prefixentry)) * dst_negative_scale_remainder_result_prefixentryright)) /\ exists ff_q_pvs_remainder_result_prefixentryrightnegative. dst_negative_code_remainder_result_prefixentryright = ff_q_pvs_remainder_result_prefixentryrightnegative * S ((S (dc_quotient_remainder_result_prefixentry)) * dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_remainder_result_prefixentryright))) /\ (exists ge_balance_positive_remainder_result_prefixentryrightvalue ge_balance_negative_remainder_result_prefixentryrightvalue. (((((dc_right_remainder_result_prefixentry) = 2 * (ge_balance_positive_remainder_result_prefixentryrightvalue) /\ (ge_balance_negative_remainder_result_prefixentryrightvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixentryrightvaluedecode. (((dc_right_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixentryrightvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixentryrightvalue) = S ge_signed_half_remainder_result_prefixentryrightvaluedecode))) /\ ((dst_positive_remainder_result_prefixentryright) + ge_balance_negative_remainder_result_prefixentryrightvalue = (dst_negative_remainder_result_prefixentryright) + ge_balance_positive_remainder_result_prefixentryrightvalue))))))))) /\ (exists sto_ap_remainder_result_prefixentryproduct sto_an_remainder_result_prefixentryproduct sto_bp_remainder_result_prefixentryproduct sto_bn_remainder_result_prefixentryproduct sto_cp_remainder_result_prefixentryproduct sto_cn_remainder_result_prefixentryproduct. (((((dc_left_remainder_result_prefixentry) = 2 * (sto_ap_remainder_result_prefixentryproduct) /\ (sto_an_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductleft. (((dc_left_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryproductleft + 1 /\ (sto_ap_remainder_result_prefixentryproduct) = 0) /\ (sto_an_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductleft))) /\ ((((((dc_right_remainder_result_prefixentry) = 2 * (sto_bp_remainder_result_prefixentryproduct) /\ (sto_bn_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductright. (((dc_right_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryproductright + 1 /\ (sto_bp_remainder_result_prefixentryproduct) = 0) /\ (sto_bn_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductright))) /\ ((((((dc_value_remainder_result_prefix) = 2 * (sto_cp_remainder_result_prefixentryproduct) /\ (sto_cn_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductoutput. (((dc_value_remainder_result_prefix) = 2 * ge_signed_half_remainder_result_prefixentryproductoutput + 1 /\ (sto_cp_remainder_result_prefixentryproduct) = 0) /\ (sto_cn_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductoutput))) /\ ((sto_ap_remainder_result_prefixentryproduct * sto_bp_remainder_result_prefixentryproduct + sto_an_remainder_result_prefixentryproduct * sto_bn_remainder_result_prefixentryproduct) + sto_cn_remainder_result_prefixentryproduct = (sto_ap_remainder_result_prefixentryproduct * sto_bn_remainder_result_prefixentryproduct + sto_an_remainder_result_prefixentryproduct * sto_bp_remainder_result_prefixentryproduct) + sto_cp_remainder_result_prefixentryproduct))))))))))))))) \/ ((((dc_index_remainder_result_prefix)=0 \/ ~(exists pvs_factor_remainder_result_prefixentrynondivisor. (S k) = (dc_index_remainder_result_prefix) * pvs_factor_remainder_result_prefixentrynondivisor)) /\ ((dc_value_remainder_result_prefix)=0))))))) /\ (exists dst_positive_code_remainder_result_sum dst_positive_scale_remainder_result_sum dst_negative_code_remainder_result_sum dst_negative_scale_remainder_result_sum dst_positive_sum_remainder_result_sum dst_negative_sum_remainder_result_sum. (((M) = (((((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) * S ((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) + ((dst_positive_scale_remainder_result_sum) + (dst_positive_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))) * S ((((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) * S ((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) + ((dst_positive_scale_remainder_result_sum) + (dst_positive_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))) + ((((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))))) /\ (((exists fs_u_dst_remainder_result_sumpositive fs_v_dst_remainder_result_sumpositive. ((((exists fs_h_dst_remainder_result_sumpositive_body_start. fs_h_dst_remainder_result_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_start. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_start * S ((S (0)) * fs_v_dst_remainder_result_sumpositive) + (0))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_terminal. fs_h_dst_remainder_result_sumpositive_body_terminal + S (dst_positive_sum_remainder_result_sum) = S ((S (S k)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_terminal. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_terminal * S ((S (S k)) * fs_v_dst_remainder_result_sumpositive) + (dst_positive_sum_remainder_result_sum))) /\ forall fs_i_dst_remainder_result_sumpositive_body_steps. (exists fs_lt_dst_remainder_result_sumpositive_body_steps_bound. fs_lt_dst_remainder_result_sumpositive_body_steps_bound + S fs_i_dst_remainder_result_sumpositive_body_steps = S k) -> exists fs_a_dst_remainder_result_sumpositive_body_steps fs_r_dst_remainder_result_sumpositive_body_steps fs_s_dst_remainder_result_sumpositive_body_steps. ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_summand. fs_h_dst_remainder_result_sumpositive_body_steps_summand + S (fs_a_dst_remainder_result_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * dst_positive_scale_remainder_result_sum)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_summand. dst_positive_code_remainder_result_sum = fs_q_dst_remainder_result_sumpositive_body_steps_summand * S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * dst_positive_scale_remainder_result_sum) + (fs_a_dst_remainder_result_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_partial. fs_h_dst_remainder_result_sumpositive_body_steps_partial + S (fs_r_dst_remainder_result_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_partial. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_steps_partial * S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive) + (fs_r_dst_remainder_result_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_successor. fs_h_dst_remainder_result_sumpositive_body_steps_successor + S (fs_s_dst_remainder_result_sumpositive_body_steps) = S ((S (S fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_successor. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_steps_successor * S ((S (S fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive) + (fs_s_dst_remainder_result_sumpositive_body_steps))) /\ fs_s_dst_remainder_result_sumpositive_body_steps = fs_r_dst_remainder_result_sumpositive_body_steps + fs_a_dst_remainder_result_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_remainder_result_sumnegative fs_v_dst_remainder_result_sumnegative. ((((exists fs_h_dst_remainder_result_sumnegative_body_start. fs_h_dst_remainder_result_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_start. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_start * S ((S (0)) * fs_v_dst_remainder_result_sumnegative) + (0))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_terminal. fs_h_dst_remainder_result_sumnegative_body_terminal + S (dst_negative_sum_remainder_result_sum) = S ((S (S k)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_terminal. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_terminal * S ((S (S k)) * fs_v_dst_remainder_result_sumnegative) + (dst_negative_sum_remainder_result_sum))) /\ forall fs_i_dst_remainder_result_sumnegative_body_steps. (exists fs_lt_dst_remainder_result_sumnegative_body_steps_bound. fs_lt_dst_remainder_result_sumnegative_body_steps_bound + S fs_i_dst_remainder_result_sumnegative_body_steps = S k) -> exists fs_a_dst_remainder_result_sumnegative_body_steps fs_r_dst_remainder_result_sumnegative_body_steps fs_s_dst_remainder_result_sumnegative_body_steps. ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_summand. fs_h_dst_remainder_result_sumnegative_body_steps_summand + S (fs_a_dst_remainder_result_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * dst_negative_scale_remainder_result_sum)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_summand. dst_negative_code_remainder_result_sum = fs_q_dst_remainder_result_sumnegative_body_steps_summand * S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * dst_negative_scale_remainder_result_sum) + (fs_a_dst_remainder_result_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_partial. fs_h_dst_remainder_result_sumnegative_body_steps_partial + S (fs_r_dst_remainder_result_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_partial. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_steps_partial * S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative) + (fs_r_dst_remainder_result_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_successor. fs_h_dst_remainder_result_sumnegative_body_steps_successor + S (fs_s_dst_remainder_result_sumnegative_body_steps) = S ((S (S fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_successor. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_steps_successor * S ((S (S fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative) + (fs_s_dst_remainder_result_sumnegative_body_steps))) /\ fs_s_dst_remainder_result_sumnegative_body_steps = fs_r_dst_remainder_result_sumnegative_body_steps + fs_a_dst_remainder_result_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_remainder_result_sumresult ge_balance_negative_remainder_result_sumresult. (((((r) = 2 * (ge_balance_positive_remainder_result_sumresult) /\ (ge_balance_negative_remainder_result_sumresult) = 0) \/ exists ge_signed_half_remainder_result_sumresultdecode. (((r) = 2 * ge_signed_half_remainder_result_sumresultdecode + 1 /\ (ge_balance_positive_remainder_result_sumresult) = 0) /\ (ge_balance_negative_remainder_result_sumresult) = S ge_signed_half_remainder_result_sumresultdecode))) /\ ((dst_positive_sum_remainder_result_sum) + ge_balance_negative_remainder_result_sumresult = (dst_negative_sum_remainder_result_sum) + ge_balance_positive_remainder_result_sumresult)))))))))

Constructive proof overview

Generated structural guide

Actually construct the remainder prefix through k and its S k-entry fold even when the first input is only an inclusive k-table; the arbitrary value at S k is excluded.

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

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

Proof neighborhood

Direct dependencies

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

Direct dependents

none

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

36 script commands · 9 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.

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–6

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

  1. L1
    intro N
  2. L2
    intro k
  3. L3
    intro F
  4. L4
    intro G
  5. L5
    intro hF
  6. L6
    intro hG
02Establish hmL7–16

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

  1. L7
    have hm : ∃ M. DirichletPrefix(G,F,S k,k,M)Definitions: DirichletPrefix
  2. L8
    specialize dirichlet_convolution_prefix_exists (G)
  3. L9
    specialize dirichlet_convolution_prefix_exists (F)
  4. L10
    specialize dirichlet_convolution_prefix_exists (S k)
  5. L11
    specialize dirichlet_convolution_prefix_exists (k)
  6. L12
    apply dirichlet_convolution_prefix_exists
  7. L13
    specialize signed_table_domain_resize (k)
  8. L14
    specialize signed_table_domain_resize (0)
  9. L15
    specialize signed_table_domain_resize (G)
  10. L16
    apply signed_table_domain_resize
03Use earlier factsL17–22

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

  1. L17
    exact hG
  2. L18
    specialize signed_table_domain_resize (N)
  3. L19
    specialize signed_table_domain_resize (0)
  4. L20
    specialize signed_table_domain_resize (F)
  5. L21
    apply signed_table_domain_resize
  6. L22
    exact hF
04Separate the logical casesL23–24

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

  1. L23
    cases hm
  2. L24
    cases hm_witness
05Establish hsL25–30

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

  1. L25
    have hs : ∃ r. SignedPrefixSum(x,S k,r)Definitions: SignedPrefixSum
  2. L26
    specialize arithmetic_signed_sum_exists (k)
  3. L27
    specialize arithmetic_signed_sum_exists (x)
  4. L28
    specialize arithmetic_signed_sum_exists (S k)
  5. L29
    apply arithmetic_signed_sum_exists
  6. L30
    exact hm_witness_left
06Separate the logical casesL31–31

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

  1. L31
    cases hs
07Construct an explicit witnessL32–33

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

  1. L32
    exists x
  2. L33
    exists x1
08Separate the logical casesL34–34

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

  1. L34
    split
09Use earlier factsL35–36

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

  1. L35
    exact hm_witness
  2. L36
    exact hs_witness

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro N
  2. 0002intro k
  3. 0003intro F
  4. 0004intro G
  5. 0005intro hF
  6. 0006intro hG
  7. 0007have hm : exists M. (((exists dst_positive_code_remainder_actual_prefixtable dst_positive_scale_remainder_actual_prefixtable dst_negative_code_remainder_actual_prefixtable dst_negative_scale_remainder_actual_prefixtable. (((M) = (((((dst_positive_code_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable)) * S ((dst_positive_code_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable)) + ((dst_positive_scale_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable))) + (((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) * S ((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) + ((dst_negative_scale_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)))) * S ((((dst_positive_code_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable)) * S ((dst_positive_code_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable)) + ((dst_positive_scale_remainder_actual_prefixtable) + (dst_positive_scale_remainder_actual_prefixtable))) + (((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) * S ((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) + ((dst_negative_scale_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)))) + ((((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) * S ((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) + ((dst_negative_scale_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable))) + (((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) * S ((dst_negative_code_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)) + ((dst_negative_scale_remainder_actual_prefixtable) + (dst_negative_scale_remainder_actual_prefixtable)))))) /\ (forall dst_index_remainder_actual_prefixtable. (exists pvs_le_gap_remainder_actual_prefixtabledomain. pvs_le_gap_remainder_actual_prefixtabledomain + (dst_index_remainder_actual_prefixtable) = (k)) -> exists dst_positive_remainder_actual_prefixtable dst_negative_remainder_actual_prefixtable dst_value_remainder_actual_prefixtable. ((((exists ff_h_pvs_remainder_actual_prefixtableentrypositive. ff_h_pvs_remainder_actual_prefixtableentrypositive + S (dst_positive_remainder_actual_prefixtable) = S ((S (dst_index_remainder_actual_prefixtable)) * dst_positive_scale_remainder_actual_prefixtable)) /\ exists ff_q_pvs_remainder_actual_prefixtableentrypositive. dst_positive_code_remainder_actual_prefixtable = ff_q_pvs_remainder_actual_prefixtableentrypositive * S ((S (dst_index_remainder_actual_prefixtable)) * dst_positive_scale_remainder_actual_prefixtable) + (dst_positive_remainder_actual_prefixtable))) /\ (((((exists ff_h_pvs_remainder_actual_prefixtableentrynegative. ff_h_pvs_remainder_actual_prefixtableentrynegative + S (dst_negative_remainder_actual_prefixtable) = S ((S (dst_index_remainder_actual_prefixtable)) * dst_negative_scale_remainder_actual_prefixtable)) /\ exists ff_q_pvs_remainder_actual_prefixtableentrynegative. dst_negative_code_remainder_actual_prefixtable = ff_q_pvs_remainder_actual_prefixtableentrynegative * S ((S (dst_index_remainder_actual_prefixtable)) * dst_negative_scale_remainder_actual_prefixtable) + (dst_negative_remainder_actual_prefixtable))) /\ (exists ge_balance_positive_remainder_actual_prefixtableentryvalue ge_balance_negative_remainder_actual_prefixtableentryvalue. (((((dst_value_remainder_actual_prefixtable) = 2 * (ge_balance_positive_remainder_actual_prefixtableentryvalue) /\ (ge_balance_negative_remainder_actual_prefixtableentryvalue) = 0) \/ exists ge_signed_half_remainder_actual_prefixtableentryvaluedecode. (((dst_value_remainder_actual_prefixtable) = 2 * ge_signed_half_remainder_actual_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_remainder_actual_prefixtableentryvalue) = 0) /\ (ge_balance_negative_remainder_actual_prefixtableentryvalue) = S ge_signed_half_remainder_actual_prefixtableentryvaluedecode))) /\ ((dst_positive_remainder_actual_prefixtable) + ge_balance_negative_remainder_actual_prefixtableentryvalue = (dst_negative_remainder_actual_prefixtable) + ge_balance_positive_remainder_actual_prefixtableentryvalue))))))))) /\ (forall dc_index_remainder_actual_prefix dc_value_remainder_actual_prefix. (exists pvs_le_gap_remainder_actual_prefixdomain. pvs_le_gap_remainder_actual_prefixdomain + (dc_index_remainder_actual_prefix) = (k)) -> (exists dst_positive_code_remainder_actual_prefixlookup dst_positive_scale_remainder_actual_prefixlookup dst_negative_code_remainder_actual_prefixlookup dst_negative_scale_remainder_actual_prefixlookup dst_positive_remainder_actual_prefixlookup dst_negative_remainder_actual_prefixlookup. (((M) = (((((dst_positive_code_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup)) * S ((dst_positive_code_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup)) + ((dst_positive_scale_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup))) + (((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) * S ((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) + ((dst_negative_scale_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)))) * S ((((dst_positive_code_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup)) * S ((dst_positive_code_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup)) + ((dst_positive_scale_remainder_actual_prefixlookup) + (dst_positive_scale_remainder_actual_prefixlookup))) + (((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) * S ((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) + ((dst_negative_scale_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)))) + ((((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) * S ((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) + ((dst_negative_scale_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup))) + (((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) * S ((dst_negative_code_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)) + ((dst_negative_scale_remainder_actual_prefixlookup) + (dst_negative_scale_remainder_actual_prefixlookup)))))) /\ (((((exists ff_h_pvs_remainder_actual_prefixlookuppositive. ff_h_pvs_remainder_actual_prefixlookuppositive + S (dst_positive_remainder_actual_prefixlookup) = S ((S (dc_index_remainder_actual_prefix)) * dst_positive_scale_remainder_actual_prefixlookup)) /\ exists ff_q_pvs_remainder_actual_prefixlookuppositive. dst_positive_code_remainder_actual_prefixlookup = ff_q_pvs_remainder_actual_prefixlookuppositive * S ((S (dc_index_remainder_actual_prefix)) * dst_positive_scale_remainder_actual_prefixlookup) + (dst_positive_remainder_actual_prefixlookup))) /\ (((((exists ff_h_pvs_remainder_actual_prefixlookupnegative. ff_h_pvs_remainder_actual_prefixlookupnegative + S (dst_negative_remainder_actual_prefixlookup) = S ((S (dc_index_remainder_actual_prefix)) * dst_negative_scale_remainder_actual_prefixlookup)) /\ exists ff_q_pvs_remainder_actual_prefixlookupnegative. dst_negative_code_remainder_actual_prefixlookup = ff_q_pvs_remainder_actual_prefixlookupnegative * S ((S (dc_index_remainder_actual_prefix)) * dst_negative_scale_remainder_actual_prefixlookup) + (dst_negative_remainder_actual_prefixlookup))) /\ (exists ge_balance_positive_remainder_actual_prefixlookupvalue ge_balance_negative_remainder_actual_prefixlookupvalue. (((((dc_value_remainder_actual_prefix) = 2 * (ge_balance_positive_remainder_actual_prefixlookupvalue) /\ (ge_balance_negative_remainder_actual_prefixlookupvalue) = 0) \/ exists ge_signed_half_remainder_actual_prefixlookupvaluedecode. (((dc_value_remainder_actual_prefix) = 2 * ge_signed_half_remainder_actual_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_remainder_actual_prefixlookupvalue) = 0) /\ (ge_balance_negative_remainder_actual_prefixlookupvalue) = S ge_signed_half_remainder_actual_prefixlookupvaluedecode))) /\ ((dst_positive_remainder_actual_prefixlookup) + ge_balance_negative_remainder_actual_prefixlookupvalue = (dst_negative_remainder_actual_prefixlookup) + ge_balance_positive_remainder_actual_prefixlookupvalue))))))))) -> ((((~((dc_index_remainder_actual_prefix)=0)) /\ (exists dc_quotient_remainder_actual_prefixentry dc_left_remainder_actual_prefixentry dc_right_remainder_actual_prefixentry. (((S k)=(dc_index_remainder_actual_prefix)*dc_quotient_remainder_actual_prefixentry) /\ (((exists dst_positive_code_remainder_actual_prefixentryleft dst_positive_scale_remainder_actual_prefixentryleft dst_negative_code_remainder_actual_prefixentryleft dst_negative_scale_remainder_actual_prefixentryleft dst_positive_remainder_actual_prefixentryleft dst_negative_remainder_actual_prefixentryleft. (((G) = (((((dst_positive_code_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft)) * S ((dst_positive_code_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft)) + ((dst_positive_scale_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft))) + (((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) * S ((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) + ((dst_negative_scale_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)))) * S ((((dst_positive_code_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft)) * S ((dst_positive_code_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft)) + ((dst_positive_scale_remainder_actual_prefixentryleft) + (dst_positive_scale_remainder_actual_prefixentryleft))) + (((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) * S ((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) + ((dst_negative_scale_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)))) + ((((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) * S ((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) + ((dst_negative_scale_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft))) + (((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) * S ((dst_negative_code_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)) + ((dst_negative_scale_remainder_actual_prefixentryleft) + (dst_negative_scale_remainder_actual_prefixentryleft)))))) /\ (((((exists ff_h_pvs_remainder_actual_prefixentryleftpositive. ff_h_pvs_remainder_actual_prefixentryleftpositive + S (dst_positive_remainder_actual_prefixentryleft) = S ((S (dc_index_remainder_actual_prefix)) * dst_positive_scale_remainder_actual_prefixentryleft)) /\ exists ff_q_pvs_remainder_actual_prefixentryleftpositive. dst_positive_code_remainder_actual_prefixentryleft = ff_q_pvs_remainder_actual_prefixentryleftpositive * S ((S (dc_index_remainder_actual_prefix)) * dst_positive_scale_remainder_actual_prefixentryleft) + (dst_positive_remainder_actual_prefixentryleft))) /\ (((((exists ff_h_pvs_remainder_actual_prefixentryleftnegative. ff_h_pvs_remainder_actual_prefixentryleftnegative + S (dst_negative_remainder_actual_prefixentryleft) = S ((S (dc_index_remainder_actual_prefix)) * dst_negative_scale_remainder_actual_prefixentryleft)) /\ exists ff_q_pvs_remainder_actual_prefixentryleftnegative. dst_negative_code_remainder_actual_prefixentryleft = ff_q_pvs_remainder_actual_prefixentryleftnegative * S ((S (dc_index_remainder_actual_prefix)) * dst_negative_scale_remainder_actual_prefixentryleft) + (dst_negative_remainder_actual_prefixentryleft))) /\ (exists ge_balance_positive_remainder_actual_prefixentryleftvalue ge_balance_negative_remainder_actual_prefixentryleftvalue. (((((dc_left_remainder_actual_prefixentry) = 2 * (ge_balance_positive_remainder_actual_prefixentryleftvalue) /\ (ge_balance_negative_remainder_actual_prefixentryleftvalue) = 0) \/ exists ge_signed_half_remainder_actual_prefixentryleftvaluedecode. (((dc_left_remainder_actual_prefixentry) = 2 * ge_signed_half_remainder_actual_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_remainder_actual_prefixentryleftvalue) = 0) /\ (ge_balance_negative_remainder_actual_prefixentryleftvalue) = S ge_signed_half_remainder_actual_prefixentryleftvaluedecode))) /\ ((dst_positive_remainder_actual_prefixentryleft) + ge_balance_negative_remainder_actual_prefixentryleftvalue = (dst_negative_remainder_actual_prefixentryleft) + ge_balance_positive_remainder_actual_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_remainder_actual_prefixentryright dst_positive_scale_remainder_actual_prefixentryright dst_negative_code_remainder_actual_prefixentryright dst_negative_scale_remainder_actual_prefixentryright dst_positive_remainder_actual_prefixentryright dst_negative_remainder_actual_prefixentryright. (((F) = (((((dst_positive_code_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright)) * S ((dst_positive_code_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright)) + ((dst_positive_scale_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright))) + (((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) * S ((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) + ((dst_negative_scale_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)))) * S ((((dst_positive_code_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright)) * S ((dst_positive_code_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright)) + ((dst_positive_scale_remainder_actual_prefixentryright) + (dst_positive_scale_remainder_actual_prefixentryright))) + (((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) * S ((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) + ((dst_negative_scale_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)))) + ((((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) * S ((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) + ((dst_negative_scale_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright))) + (((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) * S ((dst_negative_code_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)) + ((dst_negative_scale_remainder_actual_prefixentryright) + (dst_negative_scale_remainder_actual_prefixentryright)))))) /\ (((((exists ff_h_pvs_remainder_actual_prefixentryrightpositive. ff_h_pvs_remainder_actual_prefixentryrightpositive + S (dst_positive_remainder_actual_prefixentryright) = S ((S (dc_quotient_remainder_actual_prefixentry)) * dst_positive_scale_remainder_actual_prefixentryright)) /\ exists ff_q_pvs_remainder_actual_prefixentryrightpositive. dst_positive_code_remainder_actual_prefixentryright = ff_q_pvs_remainder_actual_prefixentryrightpositive * S ((S (dc_quotient_remainder_actual_prefixentry)) * dst_positive_scale_remainder_actual_prefixentryright) + (dst_positive_remainder_actual_prefixentryright))) /\ (((((exists ff_h_pvs_remainder_actual_prefixentryrightnegative. ff_h_pvs_remainder_actual_prefixentryrightnegative + S (dst_negative_remainder_actual_prefixentryright) = S ((S (dc_quotient_remainder_actual_prefixentry)) * dst_negative_scale_remainder_actual_prefixentryright)) /\ exists ff_q_pvs_remainder_actual_prefixentryrightnegative. dst_negative_code_remainder_actual_prefixentryright = ff_q_pvs_remainder_actual_prefixentryrightnegative * S ((S (dc_quotient_remainder_actual_prefixentry)) * dst_negative_scale_remainder_actual_prefixentryright) + (dst_negative_remainder_actual_prefixentryright))) /\ (exists ge_balance_positive_remainder_actual_prefixentryrightvalue ge_balance_negative_remainder_actual_prefixentryrightvalue. (((((dc_right_remainder_actual_prefixentry) = 2 * (ge_balance_positive_remainder_actual_prefixentryrightvalue) /\ (ge_balance_negative_remainder_actual_prefixentryrightvalue) = 0) \/ exists ge_signed_half_remainder_actual_prefixentryrightvaluedecode. (((dc_right_remainder_actual_prefixentry) = 2 * ge_signed_half_remainder_actual_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_remainder_actual_prefixentryrightvalue) = 0) /\ (ge_balance_negative_remainder_actual_prefixentryrightvalue) = S ge_signed_half_remainder_actual_prefixentryrightvaluedecode))) /\ ((dst_positive_remainder_actual_prefixentryright) + ge_balance_negative_remainder_actual_prefixentryrightvalue = (dst_negative_remainder_actual_prefixentryright) + ge_balance_positive_remainder_actual_prefixentryrightvalue))))))))) /\ (exists sto_ap_remainder_actual_prefixentryproduct sto_an_remainder_actual_prefixentryproduct sto_bp_remainder_actual_prefixentryproduct sto_bn_remainder_actual_prefixentryproduct sto_cp_remainder_actual_prefixentryproduct sto_cn_remainder_actual_prefixentryproduct. (((((dc_left_remainder_actual_prefixentry) = 2 * (sto_ap_remainder_actual_prefixentryproduct) /\ (sto_an_remainder_actual_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_actual_prefixentryproductleft. (((dc_left_remainder_actual_prefixentry) = 2 * ge_signed_half_remainder_actual_prefixentryproductleft + 1 /\ (sto_ap_remainder_actual_prefixentryproduct) = 0) /\ (sto_an_remainder_actual_prefixentryproduct) = S ge_signed_half_remainder_actual_prefixentryproductleft))) /\ ((((((dc_right_remainder_actual_prefixentry) = 2 * (sto_bp_remainder_actual_prefixentryproduct) /\ (sto_bn_remainder_actual_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_actual_prefixentryproductright. (((dc_right_remainder_actual_prefixentry) = 2 * ge_signed_half_remainder_actual_prefixentryproductright + 1 /\ (sto_bp_remainder_actual_prefixentryproduct) = 0) /\ (sto_bn_remainder_actual_prefixentryproduct) = S ge_signed_half_remainder_actual_prefixentryproductright))) /\ ((((((dc_value_remainder_actual_prefix) = 2 * (sto_cp_remainder_actual_prefixentryproduct) /\ (sto_cn_remainder_actual_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_actual_prefixentryproductoutput. (((dc_value_remainder_actual_prefix) = 2 * ge_signed_half_remainder_actual_prefixentryproductoutput + 1 /\ (sto_cp_remainder_actual_prefixentryproduct) = 0) /\ (sto_cn_remainder_actual_prefixentryproduct) = S ge_signed_half_remainder_actual_prefixentryproductoutput))) /\ ((sto_ap_remainder_actual_prefixentryproduct * sto_bp_remainder_actual_prefixentryproduct + sto_an_remainder_actual_prefixentryproduct * sto_bn_remainder_actual_prefixentryproduct) + sto_cn_remainder_actual_prefixentryproduct = (sto_ap_remainder_actual_prefixentryproduct * sto_bn_remainder_actual_prefixentryproduct + sto_an_remainder_actual_prefixentryproduct * sto_bp_remainder_actual_prefixentryproduct) + sto_cp_remainder_actual_prefixentryproduct))))))))))))))) \/ ((((dc_index_remainder_actual_prefix)=0 \/ ~(exists pvs_factor_remainder_actual_prefixentrynondivisor. (S k) = (dc_index_remainder_actual_prefix) * pvs_factor_remainder_actual_prefixentrynondivisor)) /\ ((dc_value_remainder_actual_prefix)=0)))))))
  8. 0008specialize dirichlet_convolution_prefix_exists (G)
  9. 0009specialize dirichlet_convolution_prefix_exists (F)
  10. 0010specialize dirichlet_convolution_prefix_exists (S k)
  11. 0011specialize dirichlet_convolution_prefix_exists (k)
  12. 0012apply dirichlet_convolution_prefix_exists
  13. 0013specialize signed_table_domain_resize (k)
  14. 0014specialize signed_table_domain_resize (0)
  15. 0015specialize signed_table_domain_resize (G)
  16. 0016apply signed_table_domain_resize
  17. 0017exact hG
  18. 0018specialize signed_table_domain_resize (N)
  19. 0019specialize signed_table_domain_resize (0)
  20. 0020specialize signed_table_domain_resize (F)
  21. 0021apply signed_table_domain_resize
  22. 0022exact hF
  23. 0023cases hm
  24. 0024cases hm_witness
  25. 0025have hs : exists r. (exists dst_positive_code_remainder_actual_sum dst_positive_scale_remainder_actual_sum dst_negative_code_remainder_actual_sum dst_negative_scale_remainder_actual_sum dst_positive_sum_remainder_actual_sum dst_negative_sum_remainder_actual_sum. (((x) = (((((dst_positive_code_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum)) * S ((dst_positive_code_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum)) + ((dst_positive_scale_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum))) + (((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) * S ((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) + ((dst_negative_scale_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)))) * S ((((dst_positive_code_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum)) * S ((dst_positive_code_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum)) + ((dst_positive_scale_remainder_actual_sum) + (dst_positive_scale_remainder_actual_sum))) + (((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) * S ((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) + ((dst_negative_scale_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)))) + ((((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) * S ((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) + ((dst_negative_scale_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum))) + (((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) * S ((dst_negative_code_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)) + ((dst_negative_scale_remainder_actual_sum) + (dst_negative_scale_remainder_actual_sum)))))) /\ (((exists fs_u_dst_remainder_actual_sumpositive fs_v_dst_remainder_actual_sumpositive. ((((exists fs_h_dst_remainder_actual_sumpositive_body_start. fs_h_dst_remainder_actual_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_actual_sumpositive)) /\ exists fs_q_dst_remainder_actual_sumpositive_body_start. fs_u_dst_remainder_actual_sumpositive = fs_q_dst_remainder_actual_sumpositive_body_start * S ((S (0)) * fs_v_dst_remainder_actual_sumpositive) + (0))) /\ ((((exists fs_h_dst_remainder_actual_sumpositive_body_terminal. fs_h_dst_remainder_actual_sumpositive_body_terminal + S (dst_positive_sum_remainder_actual_sum) = S ((S (S k)) * fs_v_dst_remainder_actual_sumpositive)) /\ exists fs_q_dst_remainder_actual_sumpositive_body_terminal. fs_u_dst_remainder_actual_sumpositive = fs_q_dst_remainder_actual_sumpositive_body_terminal * S ((S (S k)) * fs_v_dst_remainder_actual_sumpositive) + (dst_positive_sum_remainder_actual_sum))) /\ forall fs_i_dst_remainder_actual_sumpositive_body_steps. (exists fs_lt_dst_remainder_actual_sumpositive_body_steps_bound. fs_lt_dst_remainder_actual_sumpositive_body_steps_bound + S fs_i_dst_remainder_actual_sumpositive_body_steps = S k) -> exists fs_a_dst_remainder_actual_sumpositive_body_steps fs_r_dst_remainder_actual_sumpositive_body_steps fs_s_dst_remainder_actual_sumpositive_body_steps. ((((exists fs_h_dst_remainder_actual_sumpositive_body_steps_summand. fs_h_dst_remainder_actual_sumpositive_body_steps_summand + S (fs_a_dst_remainder_actual_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_actual_sumpositive_body_steps)) * dst_positive_scale_remainder_actual_sum)) /\ exists fs_q_dst_remainder_actual_sumpositive_body_steps_summand. dst_positive_code_remainder_actual_sum = fs_q_dst_remainder_actual_sumpositive_body_steps_summand * S ((S (fs_i_dst_remainder_actual_sumpositive_body_steps)) * dst_positive_scale_remainder_actual_sum) + (fs_a_dst_remainder_actual_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_actual_sumpositive_body_steps_partial. fs_h_dst_remainder_actual_sumpositive_body_steps_partial + S (fs_r_dst_remainder_actual_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_actual_sumpositive_body_steps)) * fs_v_dst_remainder_actual_sumpositive)) /\ exists fs_q_dst_remainder_actual_sumpositive_body_steps_partial. fs_u_dst_remainder_actual_sumpositive = fs_q_dst_remainder_actual_sumpositive_body_steps_partial * S ((S (fs_i_dst_remainder_actual_sumpositive_body_steps)) * fs_v_dst_remainder_actual_sumpositive) + (fs_r_dst_remainder_actual_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_actual_sumpositive_body_steps_successor. fs_h_dst_remainder_actual_sumpositive_body_steps_successor + S (fs_s_dst_remainder_actual_sumpositive_body_steps) = S ((S (S fs_i_dst_remainder_actual_sumpositive_body_steps)) * fs_v_dst_remainder_actual_sumpositive)) /\ exists fs_q_dst_remainder_actual_sumpositive_body_steps_successor. fs_u_dst_remainder_actual_sumpositive = fs_q_dst_remainder_actual_sumpositive_body_steps_successor * S ((S (S fs_i_dst_remainder_actual_sumpositive_body_steps)) * fs_v_dst_remainder_actual_sumpositive) + (fs_s_dst_remainder_actual_sumpositive_body_steps))) /\ fs_s_dst_remainder_actual_sumpositive_body_steps = fs_r_dst_remainder_actual_sumpositive_body_steps + fs_a_dst_remainder_actual_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_remainder_actual_sumnegative fs_v_dst_remainder_actual_sumnegative. ((((exists fs_h_dst_remainder_actual_sumnegative_body_start. fs_h_dst_remainder_actual_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_actual_sumnegative)) /\ exists fs_q_dst_remainder_actual_sumnegative_body_start. fs_u_dst_remainder_actual_sumnegative = fs_q_dst_remainder_actual_sumnegative_body_start * S ((S (0)) * fs_v_dst_remainder_actual_sumnegative) + (0))) /\ ((((exists fs_h_dst_remainder_actual_sumnegative_body_terminal. fs_h_dst_remainder_actual_sumnegative_body_terminal + S (dst_negative_sum_remainder_actual_sum) = S ((S (S k)) * fs_v_dst_remainder_actual_sumnegative)) /\ exists fs_q_dst_remainder_actual_sumnegative_body_terminal. fs_u_dst_remainder_actual_sumnegative = fs_q_dst_remainder_actual_sumnegative_body_terminal * S ((S (S k)) * fs_v_dst_remainder_actual_sumnegative) + (dst_negative_sum_remainder_actual_sum))) /\ forall fs_i_dst_remainder_actual_sumnegative_body_steps. (exists fs_lt_dst_remainder_actual_sumnegative_body_steps_bound. fs_lt_dst_remainder_actual_sumnegative_body_steps_bound + S fs_i_dst_remainder_actual_sumnegative_body_steps = S k) -> exists fs_a_dst_remainder_actual_sumnegative_body_steps fs_r_dst_remainder_actual_sumnegative_body_steps fs_s_dst_remainder_actual_sumnegative_body_steps. ((((exists fs_h_dst_remainder_actual_sumnegative_body_steps_summand. fs_h_dst_remainder_actual_sumnegative_body_steps_summand + S (fs_a_dst_remainder_actual_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_actual_sumnegative_body_steps)) * dst_negative_scale_remainder_actual_sum)) /\ exists fs_q_dst_remainder_actual_sumnegative_body_steps_summand. dst_negative_code_remainder_actual_sum = fs_q_dst_remainder_actual_sumnegative_body_steps_summand * S ((S (fs_i_dst_remainder_actual_sumnegative_body_steps)) * dst_negative_scale_remainder_actual_sum) + (fs_a_dst_remainder_actual_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_actual_sumnegative_body_steps_partial. fs_h_dst_remainder_actual_sumnegative_body_steps_partial + S (fs_r_dst_remainder_actual_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_actual_sumnegative_body_steps)) * fs_v_dst_remainder_actual_sumnegative)) /\ exists fs_q_dst_remainder_actual_sumnegative_body_steps_partial. fs_u_dst_remainder_actual_sumnegative = fs_q_dst_remainder_actual_sumnegative_body_steps_partial * S ((S (fs_i_dst_remainder_actual_sumnegative_body_steps)) * fs_v_dst_remainder_actual_sumnegative) + (fs_r_dst_remainder_actual_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_actual_sumnegative_body_steps_successor. fs_h_dst_remainder_actual_sumnegative_body_steps_successor + S (fs_s_dst_remainder_actual_sumnegative_body_steps) = S ((S (S fs_i_dst_remainder_actual_sumnegative_body_steps)) * fs_v_dst_remainder_actual_sumnegative)) /\ exists fs_q_dst_remainder_actual_sumnegative_body_steps_successor. fs_u_dst_remainder_actual_sumnegative = fs_q_dst_remainder_actual_sumnegative_body_steps_successor * S ((S (S fs_i_dst_remainder_actual_sumnegative_body_steps)) * fs_v_dst_remainder_actual_sumnegative) + (fs_s_dst_remainder_actual_sumnegative_body_steps))) /\ fs_s_dst_remainder_actual_sumnegative_body_steps = fs_r_dst_remainder_actual_sumnegative_body_steps + fs_a_dst_remainder_actual_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_remainder_actual_sumresult ge_balance_negative_remainder_actual_sumresult. (((((r) = 2 * (ge_balance_positive_remainder_actual_sumresult) /\ (ge_balance_negative_remainder_actual_sumresult) = 0) \/ exists ge_signed_half_remainder_actual_sumresultdecode. (((r) = 2 * ge_signed_half_remainder_actual_sumresultdecode + 1 /\ (ge_balance_positive_remainder_actual_sumresult) = 0) /\ (ge_balance_negative_remainder_actual_sumresult) = S ge_signed_half_remainder_actual_sumresultdecode))) /\ ((dst_positive_sum_remainder_actual_sum) + ge_balance_negative_remainder_actual_sumresult = (dst_negative_sum_remainder_actual_sum) + ge_balance_positive_remainder_actual_sumresult)))))))))
  26. 0026specialize arithmetic_signed_sum_exists (k)
  27. 0027specialize arithmetic_signed_sum_exists (x)
  28. 0028specialize arithmetic_signed_sum_exists (S k)
  29. 0029apply arithmetic_signed_sum_exists
  30. 0030exact hm_witness_left
  31. 0031cases hs
  32. 0032exists x
  33. 0033exists x1
  34. 0034split
  35. 0035exact hm_witness
  36. 0036exact hs_witness