DV0020

signed_divisor_sum_exists

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

For every positive n within the finite source domain, construct a real divisor mask and its S n-entry signed fold.

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 n. (exists dst_positive_code_sum_total_input dst_positive_scale_sum_total_input dst_negative_code_sum_total_input dst_negative_scale_sum_total_input. (((F) = (((((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) * S ((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) + ((dst_positive_scale_sum_total_input) + (dst_positive_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))) * S ((((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) * S ((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) + ((dst_positive_scale_sum_total_input) + (dst_positive_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))) + ((((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))))) /\ (forall dst_index_sum_total_input. (exists pvs_le_gap_sum_total_inputdomain. pvs_le_gap_sum_total_inputdomain + (dst_index_sum_total_input) = (N)) -> exists dst_positive_sum_total_input dst_negative_sum_total_input dst_value_sum_total_input. ((((exists ff_h_pvs_sum_total_inputentrypositive. ff_h_pvs_sum_total_inputentrypositive + S (dst_positive_sum_total_input) = S ((S (dst_index_sum_total_input)) * dst_positive_scale_sum_total_input)) /\ exists ff_q_pvs_sum_total_inputentrypositive. dst_positive_code_sum_total_input = ff_q_pvs_sum_total_inputentrypositive * S ((S (dst_index_sum_total_input)) * dst_positive_scale_sum_total_input) + (dst_positive_sum_total_input))) /\ (((((exists ff_h_pvs_sum_total_inputentrynegative. ff_h_pvs_sum_total_inputentrynegative + S (dst_negative_sum_total_input) = S ((S (dst_index_sum_total_input)) * dst_negative_scale_sum_total_input)) /\ exists ff_q_pvs_sum_total_inputentrynegative. dst_negative_code_sum_total_input = ff_q_pvs_sum_total_inputentrynegative * S ((S (dst_index_sum_total_input)) * dst_negative_scale_sum_total_input) + (dst_negative_sum_total_input))) /\ (exists ge_balance_positive_sum_total_inputentryvalue ge_balance_negative_sum_total_inputentryvalue. (((((dst_value_sum_total_input) = 2 * (ge_balance_positive_sum_total_inputentryvalue) /\ (ge_balance_negative_sum_total_inputentryvalue) = 0) \/ exists ge_signed_half_sum_total_inputentryvaluedecode. (((dst_value_sum_total_input) = 2 * ge_signed_half_sum_total_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_inputentryvalue) = 0) /\ (ge_balance_negative_sum_total_inputentryvalue) = S ge_signed_half_sum_total_inputentryvaluedecode))) /\ ((dst_positive_sum_total_input) + ge_balance_negative_sum_total_inputentryvalue = (dst_negative_sum_total_input) + ge_balance_positive_sum_total_inputentryvalue))))))))) -> ~(n=0) -> (exists pvs_le_gap_sum_total_bound. pvs_le_gap_sum_total_bound + (n) = (N)) -> exists z. (((~((n)=0)) /\ (exists dm_mask_table_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. (((dm_mask_table_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 dm_index_sum_total_resultmask dm_value_sum_total_resultmask. (exists pvs_le_gap_sum_total_resultmaskdomain. pvs_le_gap_sum_total_resultmaskdomain + (dm_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. (((dm_mask_table_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 (dm_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 (dm_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 (dm_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 (dm_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. (((((dm_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. (((dm_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))))))))) -> ((((~((dm_index_sum_total_resultmask)=0)) /\ (exists dm_quotient_sum_total_resultmaskentry. (((n)=(dm_index_sum_total_resultmask)*dm_quotient_sum_total_resultmaskentry) /\ (exists dst_positive_code_sum_total_resultmaskentryinput dst_positive_scale_sum_total_resultmaskentryinput dst_negative_code_sum_total_resultmaskentryinput dst_negative_scale_sum_total_resultmaskentryinput dst_positive_sum_total_resultmaskentryinput dst_negative_sum_total_resultmaskentryinput. (((F) = (((((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) * S ((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) + ((dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))) * S ((((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) * S ((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) + ((dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))) + ((((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryinputpositive. ff_h_pvs_sum_total_resultmaskentryinputpositive + S (dst_positive_sum_total_resultmaskentryinput) = S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryinput)) /\ exists ff_q_pvs_sum_total_resultmaskentryinputpositive. dst_positive_code_sum_total_resultmaskentryinput = ff_q_pvs_sum_total_resultmaskentryinputpositive * S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_sum_total_resultmaskentryinput))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryinputnegative. ff_h_pvs_sum_total_resultmaskentryinputnegative + S (dst_negative_sum_total_resultmaskentryinput) = S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryinput)) /\ exists ff_q_pvs_sum_total_resultmaskentryinputnegative. dst_negative_code_sum_total_resultmaskentryinput = ff_q_pvs_sum_total_resultmaskentryinputnegative * S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_sum_total_resultmaskentryinput))) /\ (exists ge_balance_positive_sum_total_resultmaskentryinputvalue ge_balance_negative_sum_total_resultmaskentryinputvalue. (((((dm_value_sum_total_resultmask) = 2 * (ge_balance_positive_sum_total_resultmaskentryinputvalue) /\ (ge_balance_negative_sum_total_resultmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryinputvaluedecode. (((dm_value_sum_total_resultmask) = 2 * ge_signed_half_sum_total_resultmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_total_resultmaskentryinputvalue) = S ge_signed_half_sum_total_resultmaskentryinputvaluedecode))) /\ ((dst_positive_sum_total_resultmaskentryinput) + ge_balance_negative_sum_total_resultmaskentryinputvalue = (dst_negative_sum_total_resultmaskentryinput) + ge_balance_positive_sum_total_resultmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_total_resultmask)=0 \/ ~(exists pvs_factor_sum_total_resultmaskentrynondivisor. (n) = (dm_index_sum_total_resultmask) * pvs_factor_sum_total_resultmaskentrynondivisor)) /\ ((dm_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. (((dm_mask_table_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

For every positive n within the finite source domain, construct a real divisor mask and its S n-entry signed fold.

The unchanged tactic script uses 2 declared prerequisites and contains 30 exact native proof lines.

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

Proof neighborhood

Direct dependencies

DV0019 divisor_mask_prefix_exists DV0006 arithmetic_signed_sum_exists

Direct dependents

DV0022 signed_divisor_sum_exists_unique

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

30 script commands · 11 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 (2)
divisor mask prefix existsarithmetic signed sum 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–6

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro n
  4. L4
    intro ht
  5. L5
    intro hn
  6. L6
    intro hbound
02Establish hmL7–14

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

  1. L7
    have hm : ∃ M. DivisorMask(F,n,n,M)Definitions: DivisorMask
  2. L8
    specialize divisor_mask_prefix_exists (N)
  3. L9
    specialize divisor_mask_prefix_exists (F)
  4. L10
    specialize divisor_mask_prefix_exists (n)
  5. L11
    specialize divisor_mask_prefix_exists (n)
  6. L12
    apply divisor_mask_prefix_exists
  7. L13
    exact ht
  8. L14
    exact hbound
03Separate the logical casesL15–16

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

  1. L15
    cases hm
  2. L16
    cases hm_witness
04Establish hzL17–22

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

  1. L17
    have hz : ∃ z. SignedPrefixSum(x,S n,z)Definitions: SignedPrefixSum
  2. L18
    specialize arithmetic_signed_sum_exists (n)
  3. L19
    specialize arithmetic_signed_sum_exists (x)
  4. L20
    specialize arithmetic_signed_sum_exists (S n)
  5. L21
    apply arithmetic_signed_sum_exists
  6. L22
    exact hm_witness_left
05Separate the logical casesL23–23

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

  1. L23
    cases hz
06Construct an explicit witnessL24–24

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

  1. L24
    exists x1
07Separate the logical casesL25–25

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

  1. L25
    split
08Use earlier factsL26–26

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

  1. L26
    exact hn
09Construct an explicit witnessL27–27

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

  1. L27
    exists x
10Separate the logical casesL28–28

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

  1. L28
    split
11Use earlier factsL29–30

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

  1. L29
    exact hm_witness
  2. L30
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro n
  4. 0004intro ht
  5. 0005intro hn
  6. 0006intro hbound
  7. 0007have hm : exists M. (((exists dst_positive_code_sum_total_masktable dst_positive_scale_sum_total_masktable dst_negative_code_sum_total_masktable dst_negative_scale_sum_total_masktable. (((M) = (((((dst_positive_code_sum_total_masktable) + (dst_positive_scale_sum_total_masktable)) * S ((dst_positive_code_sum_total_masktable) + (dst_positive_scale_sum_total_masktable)) + ((dst_positive_scale_sum_total_masktable) + (dst_positive_scale_sum_total_masktable))) + (((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) * S ((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) + ((dst_negative_scale_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)))) * S ((((dst_positive_code_sum_total_masktable) + (dst_positive_scale_sum_total_masktable)) * S ((dst_positive_code_sum_total_masktable) + (dst_positive_scale_sum_total_masktable)) + ((dst_positive_scale_sum_total_masktable) + (dst_positive_scale_sum_total_masktable))) + (((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) * S ((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) + ((dst_negative_scale_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)))) + ((((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) * S ((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) + ((dst_negative_scale_sum_total_masktable) + (dst_negative_scale_sum_total_masktable))) + (((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) * S ((dst_negative_code_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)) + ((dst_negative_scale_sum_total_masktable) + (dst_negative_scale_sum_total_masktable)))))) /\ (forall dst_index_sum_total_masktable. (exists pvs_le_gap_sum_total_masktabledomain. pvs_le_gap_sum_total_masktabledomain + (dst_index_sum_total_masktable) = (n)) -> exists dst_positive_sum_total_masktable dst_negative_sum_total_masktable dst_value_sum_total_masktable. ((((exists ff_h_pvs_sum_total_masktableentrypositive. ff_h_pvs_sum_total_masktableentrypositive + S (dst_positive_sum_total_masktable) = S ((S (dst_index_sum_total_masktable)) * dst_positive_scale_sum_total_masktable)) /\ exists ff_q_pvs_sum_total_masktableentrypositive. dst_positive_code_sum_total_masktable = ff_q_pvs_sum_total_masktableentrypositive * S ((S (dst_index_sum_total_masktable)) * dst_positive_scale_sum_total_masktable) + (dst_positive_sum_total_masktable))) /\ (((((exists ff_h_pvs_sum_total_masktableentrynegative. ff_h_pvs_sum_total_masktableentrynegative + S (dst_negative_sum_total_masktable) = S ((S (dst_index_sum_total_masktable)) * dst_negative_scale_sum_total_masktable)) /\ exists ff_q_pvs_sum_total_masktableentrynegative. dst_negative_code_sum_total_masktable = ff_q_pvs_sum_total_masktableentrynegative * S ((S (dst_index_sum_total_masktable)) * dst_negative_scale_sum_total_masktable) + (dst_negative_sum_total_masktable))) /\ (exists ge_balance_positive_sum_total_masktableentryvalue ge_balance_negative_sum_total_masktableentryvalue. (((((dst_value_sum_total_masktable) = 2 * (ge_balance_positive_sum_total_masktableentryvalue) /\ (ge_balance_negative_sum_total_masktableentryvalue) = 0) \/ exists ge_signed_half_sum_total_masktableentryvaluedecode. (((dst_value_sum_total_masktable) = 2 * ge_signed_half_sum_total_masktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_masktableentryvalue) = 0) /\ (ge_balance_negative_sum_total_masktableentryvalue) = S ge_signed_half_sum_total_masktableentryvaluedecode))) /\ ((dst_positive_sum_total_masktable) + ge_balance_negative_sum_total_masktableentryvalue = (dst_negative_sum_total_masktable) + ge_balance_positive_sum_total_masktableentryvalue))))))))) /\ (forall dm_index_sum_total_mask dm_value_sum_total_mask. (exists pvs_le_gap_sum_total_maskdomain. pvs_le_gap_sum_total_maskdomain + (dm_index_sum_total_mask) = (n)) -> (exists dst_positive_code_sum_total_masklookup dst_positive_scale_sum_total_masklookup dst_negative_code_sum_total_masklookup dst_negative_scale_sum_total_masklookup dst_positive_sum_total_masklookup dst_negative_sum_total_masklookup. (((M) = (((((dst_positive_code_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup)) * S ((dst_positive_code_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup)) + ((dst_positive_scale_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup))) + (((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) * S ((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) + ((dst_negative_scale_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)))) * S ((((dst_positive_code_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup)) * S ((dst_positive_code_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup)) + ((dst_positive_scale_sum_total_masklookup) + (dst_positive_scale_sum_total_masklookup))) + (((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) * S ((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) + ((dst_negative_scale_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)))) + ((((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) * S ((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) + ((dst_negative_scale_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup))) + (((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) * S ((dst_negative_code_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)) + ((dst_negative_scale_sum_total_masklookup) + (dst_negative_scale_sum_total_masklookup)))))) /\ (((((exists ff_h_pvs_sum_total_masklookuppositive. ff_h_pvs_sum_total_masklookuppositive + S (dst_positive_sum_total_masklookup) = S ((S (dm_index_sum_total_mask)) * dst_positive_scale_sum_total_masklookup)) /\ exists ff_q_pvs_sum_total_masklookuppositive. dst_positive_code_sum_total_masklookup = ff_q_pvs_sum_total_masklookuppositive * S ((S (dm_index_sum_total_mask)) * dst_positive_scale_sum_total_masklookup) + (dst_positive_sum_total_masklookup))) /\ (((((exists ff_h_pvs_sum_total_masklookupnegative. ff_h_pvs_sum_total_masklookupnegative + S (dst_negative_sum_total_masklookup) = S ((S (dm_index_sum_total_mask)) * dst_negative_scale_sum_total_masklookup)) /\ exists ff_q_pvs_sum_total_masklookupnegative. dst_negative_code_sum_total_masklookup = ff_q_pvs_sum_total_masklookupnegative * S ((S (dm_index_sum_total_mask)) * dst_negative_scale_sum_total_masklookup) + (dst_negative_sum_total_masklookup))) /\ (exists ge_balance_positive_sum_total_masklookupvalue ge_balance_negative_sum_total_masklookupvalue. (((((dm_value_sum_total_mask) = 2 * (ge_balance_positive_sum_total_masklookupvalue) /\ (ge_balance_negative_sum_total_masklookupvalue) = 0) \/ exists ge_signed_half_sum_total_masklookupvaluedecode. (((dm_value_sum_total_mask) = 2 * ge_signed_half_sum_total_masklookupvaluedecode + 1 /\ (ge_balance_positive_sum_total_masklookupvalue) = 0) /\ (ge_balance_negative_sum_total_masklookupvalue) = S ge_signed_half_sum_total_masklookupvaluedecode))) /\ ((dst_positive_sum_total_masklookup) + ge_balance_negative_sum_total_masklookupvalue = (dst_negative_sum_total_masklookup) + ge_balance_positive_sum_total_masklookupvalue))))))))) -> ((((~((dm_index_sum_total_mask)=0)) /\ (exists dm_quotient_sum_total_maskentry. (((n)=(dm_index_sum_total_mask)*dm_quotient_sum_total_maskentry) /\ (exists dst_positive_code_sum_total_maskentryinput dst_positive_scale_sum_total_maskentryinput dst_negative_code_sum_total_maskentryinput dst_negative_scale_sum_total_maskentryinput dst_positive_sum_total_maskentryinput dst_negative_sum_total_maskentryinput. (((F) = (((((dst_positive_code_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput)) * S ((dst_positive_code_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput)) + ((dst_positive_scale_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput))) + (((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) * S ((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) + ((dst_negative_scale_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)))) * S ((((dst_positive_code_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput)) * S ((dst_positive_code_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput)) + ((dst_positive_scale_sum_total_maskentryinput) + (dst_positive_scale_sum_total_maskentryinput))) + (((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) * S ((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) + ((dst_negative_scale_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)))) + ((((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) * S ((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) + ((dst_negative_scale_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput))) + (((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) * S ((dst_negative_code_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)) + ((dst_negative_scale_sum_total_maskentryinput) + (dst_negative_scale_sum_total_maskentryinput)))))) /\ (((((exists ff_h_pvs_sum_total_maskentryinputpositive. ff_h_pvs_sum_total_maskentryinputpositive + S (dst_positive_sum_total_maskentryinput) = S ((S (dm_index_sum_total_mask)) * dst_positive_scale_sum_total_maskentryinput)) /\ exists ff_q_pvs_sum_total_maskentryinputpositive. dst_positive_code_sum_total_maskentryinput = ff_q_pvs_sum_total_maskentryinputpositive * S ((S (dm_index_sum_total_mask)) * dst_positive_scale_sum_total_maskentryinput) + (dst_positive_sum_total_maskentryinput))) /\ (((((exists ff_h_pvs_sum_total_maskentryinputnegative. ff_h_pvs_sum_total_maskentryinputnegative + S (dst_negative_sum_total_maskentryinput) = S ((S (dm_index_sum_total_mask)) * dst_negative_scale_sum_total_maskentryinput)) /\ exists ff_q_pvs_sum_total_maskentryinputnegative. dst_negative_code_sum_total_maskentryinput = ff_q_pvs_sum_total_maskentryinputnegative * S ((S (dm_index_sum_total_mask)) * dst_negative_scale_sum_total_maskentryinput) + (dst_negative_sum_total_maskentryinput))) /\ (exists ge_balance_positive_sum_total_maskentryinputvalue ge_balance_negative_sum_total_maskentryinputvalue. (((((dm_value_sum_total_mask) = 2 * (ge_balance_positive_sum_total_maskentryinputvalue) /\ (ge_balance_negative_sum_total_maskentryinputvalue) = 0) \/ exists ge_signed_half_sum_total_maskentryinputvaluedecode. (((dm_value_sum_total_mask) = 2 * ge_signed_half_sum_total_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_total_maskentryinputvalue) = 0) /\ (ge_balance_negative_sum_total_maskentryinputvalue) = S ge_signed_half_sum_total_maskentryinputvaluedecode))) /\ ((dst_positive_sum_total_maskentryinput) + ge_balance_negative_sum_total_maskentryinputvalue = (dst_negative_sum_total_maskentryinput) + ge_balance_positive_sum_total_maskentryinputvalue))))))))))))) \/ ((((dm_index_sum_total_mask)=0 \/ ~(exists pvs_factor_sum_total_maskentrynondivisor. (n) = (dm_index_sum_total_mask) * pvs_factor_sum_total_maskentrynondivisor)) /\ ((dm_value_sum_total_mask)=0)))))))
  8. 0008specialize divisor_mask_prefix_exists (N)
  9. 0009specialize divisor_mask_prefix_exists (F)
  10. 0010specialize divisor_mask_prefix_exists (n)
  11. 0011specialize divisor_mask_prefix_exists (n)
  12. 0012apply divisor_mask_prefix_exists
  13. 0013exact ht
  14. 0014exact hbound
  15. 0015cases hm
  16. 0016cases hm_witness
  17. 0017have 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)))))))))
  18. 0018specialize arithmetic_signed_sum_exists (n)
  19. 0019specialize arithmetic_signed_sum_exists (x)
  20. 0020specialize arithmetic_signed_sum_exists (S n)
  21. 0021apply arithmetic_signed_sum_exists
  22. 0022exact hm_witness_left
  23. 0023cases hz
  24. 0024exists x1
  25. 0025split
  26. 0026exact hn
  27. 0027exists x
  28. 0028split
  29. 0029exact hm_witness
  30. 0030exact hz_witness