DV0024

signed_divisor_sum_one

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

At n=1, the real two-entry masked fold is 0+F(1), so its exact value is F(1) regardless of F(0).

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 a. (exists dst_positive_code_sum_one_input dst_positive_scale_sum_one_input dst_negative_code_sum_one_input dst_negative_scale_sum_one_input. (((F) = (((((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) * S ((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) + ((dst_positive_scale_sum_one_input) + (dst_positive_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))) * S ((((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) * S ((dst_positive_code_sum_one_input) + (dst_positive_scale_sum_one_input)) + ((dst_positive_scale_sum_one_input) + (dst_positive_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))) + ((((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input))) + (((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) * S ((dst_negative_code_sum_one_input) + (dst_negative_scale_sum_one_input)) + ((dst_negative_scale_sum_one_input) + (dst_negative_scale_sum_one_input)))))) /\ (forall dst_index_sum_one_input. (exists pvs_le_gap_sum_one_inputdomain. pvs_le_gap_sum_one_inputdomain + (dst_index_sum_one_input) = (N)) -> exists dst_positive_sum_one_input dst_negative_sum_one_input dst_value_sum_one_input. ((((exists ff_h_pvs_sum_one_inputentrypositive. ff_h_pvs_sum_one_inputentrypositive + S (dst_positive_sum_one_input) = S ((S (dst_index_sum_one_input)) * dst_positive_scale_sum_one_input)) /\ exists ff_q_pvs_sum_one_inputentrypositive. dst_positive_code_sum_one_input = ff_q_pvs_sum_one_inputentrypositive * S ((S (dst_index_sum_one_input)) * dst_positive_scale_sum_one_input) + (dst_positive_sum_one_input))) /\ (((((exists ff_h_pvs_sum_one_inputentrynegative. ff_h_pvs_sum_one_inputentrynegative + S (dst_negative_sum_one_input) = S ((S (dst_index_sum_one_input)) * dst_negative_scale_sum_one_input)) /\ exists ff_q_pvs_sum_one_inputentrynegative. dst_negative_code_sum_one_input = ff_q_pvs_sum_one_inputentrynegative * S ((S (dst_index_sum_one_input)) * dst_negative_scale_sum_one_input) + (dst_negative_sum_one_input))) /\ (exists ge_balance_positive_sum_one_inputentryvalue ge_balance_negative_sum_one_inputentryvalue. (((((dst_value_sum_one_input) = 2 * (ge_balance_positive_sum_one_inputentryvalue) /\ (ge_balance_negative_sum_one_inputentryvalue) = 0) \/ exists ge_signed_half_sum_one_inputentryvaluedecode. (((dst_value_sum_one_input) = 2 * ge_signed_half_sum_one_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_one_inputentryvalue) = 0) /\ (ge_balance_negative_sum_one_inputentryvalue) = S ge_signed_half_sum_one_inputentryvaluedecode))) /\ ((dst_positive_sum_one_input) + ge_balance_negative_sum_one_inputentryvalue = (dst_negative_sum_one_input) + ge_balance_positive_sum_one_inputentryvalue))))))))) -> (exists pvs_le_gap_sum_one_bound. pvs_le_gap_sum_one_bound + (1) = (N)) -> (exists dst_positive_code_sum_one_entry dst_positive_scale_sum_one_entry dst_negative_code_sum_one_entry dst_negative_scale_sum_one_entry dst_positive_sum_one_entry dst_negative_sum_one_entry. (((F) = (((((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) * S ((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) + ((dst_positive_scale_sum_one_entry) + (dst_positive_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))) * S ((((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) * S ((dst_positive_code_sum_one_entry) + (dst_positive_scale_sum_one_entry)) + ((dst_positive_scale_sum_one_entry) + (dst_positive_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))) + ((((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry))) + (((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) * S ((dst_negative_code_sum_one_entry) + (dst_negative_scale_sum_one_entry)) + ((dst_negative_scale_sum_one_entry) + (dst_negative_scale_sum_one_entry)))))) /\ (((((exists ff_h_pvs_sum_one_entrypositive. ff_h_pvs_sum_one_entrypositive + S (dst_positive_sum_one_entry) = S ((S (1)) * dst_positive_scale_sum_one_entry)) /\ exists ff_q_pvs_sum_one_entrypositive. dst_positive_code_sum_one_entry = ff_q_pvs_sum_one_entrypositive * S ((S (1)) * dst_positive_scale_sum_one_entry) + (dst_positive_sum_one_entry))) /\ (((((exists ff_h_pvs_sum_one_entrynegative. ff_h_pvs_sum_one_entrynegative + S (dst_negative_sum_one_entry) = S ((S (1)) * dst_negative_scale_sum_one_entry)) /\ exists ff_q_pvs_sum_one_entrynegative. dst_negative_code_sum_one_entry = ff_q_pvs_sum_one_entrynegative * S ((S (1)) * dst_negative_scale_sum_one_entry) + (dst_negative_sum_one_entry))) /\ (exists ge_balance_positive_sum_one_entryvalue ge_balance_negative_sum_one_entryvalue. (((((a) = 2 * (ge_balance_positive_sum_one_entryvalue) /\ (ge_balance_negative_sum_one_entryvalue) = 0) \/ exists ge_signed_half_sum_one_entryvaluedecode. (((a) = 2 * ge_signed_half_sum_one_entryvaluedecode + 1 /\ (ge_balance_positive_sum_one_entryvalue) = 0) /\ (ge_balance_negative_sum_one_entryvalue) = S ge_signed_half_sum_one_entryvaluedecode))) /\ ((dst_positive_sum_one_entry) + ge_balance_negative_sum_one_entryvalue = (dst_negative_sum_one_entry) + ge_balance_positive_sum_one_entryvalue))))))))) -> (((~((1)=0)) /\ (exists dm_mask_table_sum_one_result. ((((exists dst_positive_code_sum_one_resultmasktable dst_positive_scale_sum_one_resultmasktable dst_negative_code_sum_one_resultmasktable dst_negative_scale_sum_one_resultmasktable. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) * S ((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) + ((dst_positive_scale_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))) * S ((((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) * S ((dst_positive_code_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable)) + ((dst_positive_scale_sum_one_resultmasktable) + (dst_positive_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))) + ((((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable))) + (((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) * S ((dst_negative_code_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)) + ((dst_negative_scale_sum_one_resultmasktable) + (dst_negative_scale_sum_one_resultmasktable)))))) /\ (forall dst_index_sum_one_resultmasktable. (exists pvs_le_gap_sum_one_resultmasktabledomain. pvs_le_gap_sum_one_resultmasktabledomain + (dst_index_sum_one_resultmasktable) = (1)) -> exists dst_positive_sum_one_resultmasktable dst_negative_sum_one_resultmasktable dst_value_sum_one_resultmasktable. ((((exists ff_h_pvs_sum_one_resultmasktableentrypositive. ff_h_pvs_sum_one_resultmasktableentrypositive + S (dst_positive_sum_one_resultmasktable) = S ((S (dst_index_sum_one_resultmasktable)) * dst_positive_scale_sum_one_resultmasktable)) /\ exists ff_q_pvs_sum_one_resultmasktableentrypositive. dst_positive_code_sum_one_resultmasktable = ff_q_pvs_sum_one_resultmasktableentrypositive * S ((S (dst_index_sum_one_resultmasktable)) * dst_positive_scale_sum_one_resultmasktable) + (dst_positive_sum_one_resultmasktable))) /\ (((((exists ff_h_pvs_sum_one_resultmasktableentrynegative. ff_h_pvs_sum_one_resultmasktableentrynegative + S (dst_negative_sum_one_resultmasktable) = S ((S (dst_index_sum_one_resultmasktable)) * dst_negative_scale_sum_one_resultmasktable)) /\ exists ff_q_pvs_sum_one_resultmasktableentrynegative. dst_negative_code_sum_one_resultmasktable = ff_q_pvs_sum_one_resultmasktableentrynegative * S ((S (dst_index_sum_one_resultmasktable)) * dst_negative_scale_sum_one_resultmasktable) + (dst_negative_sum_one_resultmasktable))) /\ (exists ge_balance_positive_sum_one_resultmasktableentryvalue ge_balance_negative_sum_one_resultmasktableentryvalue. (((((dst_value_sum_one_resultmasktable) = 2 * (ge_balance_positive_sum_one_resultmasktableentryvalue) /\ (ge_balance_negative_sum_one_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_one_resultmasktableentryvaluedecode. (((dst_value_sum_one_resultmasktable) = 2 * ge_signed_half_sum_one_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_one_resultmasktableentryvalue) = S ge_signed_half_sum_one_resultmasktableentryvaluedecode))) /\ ((dst_positive_sum_one_resultmasktable) + ge_balance_negative_sum_one_resultmasktableentryvalue = (dst_negative_sum_one_resultmasktable) + ge_balance_positive_sum_one_resultmasktableentryvalue))))))))) /\ (forall dm_index_sum_one_resultmask dm_value_sum_one_resultmask. (exists pvs_le_gap_sum_one_resultmaskdomain. pvs_le_gap_sum_one_resultmaskdomain + (dm_index_sum_one_resultmask) = (1)) -> (exists dst_positive_code_sum_one_resultmasklookup dst_positive_scale_sum_one_resultmasklookup dst_negative_code_sum_one_resultmasklookup dst_negative_scale_sum_one_resultmasklookup dst_positive_sum_one_resultmasklookup dst_negative_sum_one_resultmasklookup. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) * S ((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) + ((dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))) * S ((((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) * S ((dst_positive_code_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup)) + ((dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))) + ((((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup))) + (((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) * S ((dst_negative_code_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)) + ((dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_scale_sum_one_resultmasklookup)))))) /\ (((((exists ff_h_pvs_sum_one_resultmasklookuppositive. ff_h_pvs_sum_one_resultmasklookuppositive + S (dst_positive_sum_one_resultmasklookup) = S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmasklookup)) /\ exists ff_q_pvs_sum_one_resultmasklookuppositive. dst_positive_code_sum_one_resultmasklookup = ff_q_pvs_sum_one_resultmasklookuppositive * S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmasklookup) + (dst_positive_sum_one_resultmasklookup))) /\ (((((exists ff_h_pvs_sum_one_resultmasklookupnegative. ff_h_pvs_sum_one_resultmasklookupnegative + S (dst_negative_sum_one_resultmasklookup) = S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmasklookup)) /\ exists ff_q_pvs_sum_one_resultmasklookupnegative. dst_negative_code_sum_one_resultmasklookup = ff_q_pvs_sum_one_resultmasklookupnegative * S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmasklookup) + (dst_negative_sum_one_resultmasklookup))) /\ (exists ge_balance_positive_sum_one_resultmasklookupvalue ge_balance_negative_sum_one_resultmasklookupvalue. (((((dm_value_sum_one_resultmask) = 2 * (ge_balance_positive_sum_one_resultmasklookupvalue) /\ (ge_balance_negative_sum_one_resultmasklookupvalue) = 0) \/ exists ge_signed_half_sum_one_resultmasklookupvaluedecode. (((dm_value_sum_one_resultmask) = 2 * ge_signed_half_sum_one_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmasklookupvalue) = 0) /\ (ge_balance_negative_sum_one_resultmasklookupvalue) = S ge_signed_half_sum_one_resultmasklookupvaluedecode))) /\ ((dst_positive_sum_one_resultmasklookup) + ge_balance_negative_sum_one_resultmasklookupvalue = (dst_negative_sum_one_resultmasklookup) + ge_balance_positive_sum_one_resultmasklookupvalue))))))))) -> ((((~((dm_index_sum_one_resultmask)=0)) /\ (exists dm_quotient_sum_one_resultmaskentry. (((1)=(dm_index_sum_one_resultmask)*dm_quotient_sum_one_resultmaskentry) /\ (exists dst_positive_code_sum_one_resultmaskentryinput dst_positive_scale_sum_one_resultmaskentryinput dst_negative_code_sum_one_resultmaskentryinput dst_negative_scale_sum_one_resultmaskentryinput dst_positive_sum_one_resultmaskentryinput dst_negative_sum_one_resultmaskentryinput. (((F) = (((((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) * S ((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) + ((dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))) * S ((((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) * S ((dst_positive_code_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput)) + ((dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))) + ((((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput))) + (((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) * S ((dst_negative_code_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)) + ((dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_scale_sum_one_resultmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_one_resultmaskentryinputpositive. ff_h_pvs_sum_one_resultmaskentryinputpositive + S (dst_positive_sum_one_resultmaskentryinput) = S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmaskentryinput)) /\ exists ff_q_pvs_sum_one_resultmaskentryinputpositive. dst_positive_code_sum_one_resultmaskentryinput = ff_q_pvs_sum_one_resultmaskentryinputpositive * S ((S (dm_index_sum_one_resultmask)) * dst_positive_scale_sum_one_resultmaskentryinput) + (dst_positive_sum_one_resultmaskentryinput))) /\ (((((exists ff_h_pvs_sum_one_resultmaskentryinputnegative. ff_h_pvs_sum_one_resultmaskentryinputnegative + S (dst_negative_sum_one_resultmaskentryinput) = S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmaskentryinput)) /\ exists ff_q_pvs_sum_one_resultmaskentryinputnegative. dst_negative_code_sum_one_resultmaskentryinput = ff_q_pvs_sum_one_resultmaskentryinputnegative * S ((S (dm_index_sum_one_resultmask)) * dst_negative_scale_sum_one_resultmaskentryinput) + (dst_negative_sum_one_resultmaskentryinput))) /\ (exists ge_balance_positive_sum_one_resultmaskentryinputvalue ge_balance_negative_sum_one_resultmaskentryinputvalue. (((((dm_value_sum_one_resultmask) = 2 * (ge_balance_positive_sum_one_resultmaskentryinputvalue) /\ (ge_balance_negative_sum_one_resultmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_one_resultmaskentryinputvaluedecode. (((dm_value_sum_one_resultmask) = 2 * ge_signed_half_sum_one_resultmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_one_resultmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_one_resultmaskentryinputvalue) = S ge_signed_half_sum_one_resultmaskentryinputvaluedecode))) /\ ((dst_positive_sum_one_resultmaskentryinput) + ge_balance_negative_sum_one_resultmaskentryinputvalue = (dst_negative_sum_one_resultmaskentryinput) + ge_balance_positive_sum_one_resultmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_one_resultmask)=0 \/ ~(exists pvs_factor_sum_one_resultmaskentrynondivisor. (1) = (dm_index_sum_one_resultmask) * pvs_factor_sum_one_resultmaskentrynondivisor)) /\ ((dm_value_sum_one_resultmask)=0))))))) /\ (exists dst_positive_code_sum_one_resultfold dst_positive_scale_sum_one_resultfold dst_negative_code_sum_one_resultfold dst_negative_scale_sum_one_resultfold dst_positive_sum_sum_one_resultfold dst_negative_sum_sum_one_resultfold. (((dm_mask_table_sum_one_result) = (((((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) * S ((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) + ((dst_positive_scale_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))) * S ((((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) * S ((dst_positive_code_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold)) + ((dst_positive_scale_sum_one_resultfold) + (dst_positive_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))) + ((((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold))) + (((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) * S ((dst_negative_code_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)) + ((dst_negative_scale_sum_one_resultfold) + (dst_negative_scale_sum_one_resultfold)))))) /\ (((exists fs_u_dst_sum_one_resultfoldpositive fs_v_dst_sum_one_resultfoldpositive. ((((exists fs_h_dst_sum_one_resultfoldpositive_body_start. fs_h_dst_sum_one_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_start. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_one_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_terminal. fs_h_dst_sum_one_resultfoldpositive_body_terminal + S (dst_positive_sum_sum_one_resultfold) = S ((S (S (1))) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_terminal. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_sum_one_resultfoldpositive) + (dst_positive_sum_sum_one_resultfold))) /\ forall fs_i_dst_sum_one_resultfoldpositive_body_steps. (exists fs_lt_dst_sum_one_resultfoldpositive_body_steps_bound. fs_lt_dst_sum_one_resultfoldpositive_body_steps_bound + S fs_i_dst_sum_one_resultfoldpositive_body_steps = S (1)) -> exists fs_a_dst_sum_one_resultfoldpositive_body_steps fs_r_dst_sum_one_resultfoldpositive_body_steps fs_s_dst_sum_one_resultfoldpositive_body_steps. ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_summand. fs_h_dst_sum_one_resultfoldpositive_body_steps_summand + S (fs_a_dst_sum_one_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * dst_positive_scale_sum_one_resultfold)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_summand. dst_positive_code_sum_one_resultfold = fs_q_dst_sum_one_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * dst_positive_scale_sum_one_resultfold) + (fs_a_dst_sum_one_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_partial. fs_h_dst_sum_one_resultfoldpositive_body_steps_partial + S (fs_r_dst_sum_one_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_partial. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive) + (fs_r_dst_sum_one_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldpositive_body_steps_successor. fs_h_dst_sum_one_resultfoldpositive_body_steps_successor + S (fs_s_dst_sum_one_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive)) /\ exists fs_q_dst_sum_one_resultfoldpositive_body_steps_successor. fs_u_dst_sum_one_resultfoldpositive = fs_q_dst_sum_one_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_one_resultfoldpositive_body_steps)) * fs_v_dst_sum_one_resultfoldpositive) + (fs_s_dst_sum_one_resultfoldpositive_body_steps))) /\ fs_s_dst_sum_one_resultfoldpositive_body_steps = fs_r_dst_sum_one_resultfoldpositive_body_steps + fs_a_dst_sum_one_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_one_resultfoldnegative fs_v_dst_sum_one_resultfoldnegative. ((((exists fs_h_dst_sum_one_resultfoldnegative_body_start. fs_h_dst_sum_one_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_start. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_one_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_terminal. fs_h_dst_sum_one_resultfoldnegative_body_terminal + S (dst_negative_sum_sum_one_resultfold) = S ((S (S (1))) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_terminal. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_sum_one_resultfoldnegative) + (dst_negative_sum_sum_one_resultfold))) /\ forall fs_i_dst_sum_one_resultfoldnegative_body_steps. (exists fs_lt_dst_sum_one_resultfoldnegative_body_steps_bound. fs_lt_dst_sum_one_resultfoldnegative_body_steps_bound + S fs_i_dst_sum_one_resultfoldnegative_body_steps = S (1)) -> exists fs_a_dst_sum_one_resultfoldnegative_body_steps fs_r_dst_sum_one_resultfoldnegative_body_steps fs_s_dst_sum_one_resultfoldnegative_body_steps. ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_summand. fs_h_dst_sum_one_resultfoldnegative_body_steps_summand + S (fs_a_dst_sum_one_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * dst_negative_scale_sum_one_resultfold)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_summand. dst_negative_code_sum_one_resultfold = fs_q_dst_sum_one_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * dst_negative_scale_sum_one_resultfold) + (fs_a_dst_sum_one_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_partial. fs_h_dst_sum_one_resultfoldnegative_body_steps_partial + S (fs_r_dst_sum_one_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_partial. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative) + (fs_r_dst_sum_one_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_resultfoldnegative_body_steps_successor. fs_h_dst_sum_one_resultfoldnegative_body_steps_successor + S (fs_s_dst_sum_one_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative)) /\ exists fs_q_dst_sum_one_resultfoldnegative_body_steps_successor. fs_u_dst_sum_one_resultfoldnegative = fs_q_dst_sum_one_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_one_resultfoldnegative_body_steps)) * fs_v_dst_sum_one_resultfoldnegative) + (fs_s_dst_sum_one_resultfoldnegative_body_steps))) /\ fs_s_dst_sum_one_resultfoldnegative_body_steps = fs_r_dst_sum_one_resultfoldnegative_body_steps + fs_a_dst_sum_one_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_one_resultfoldresult ge_balance_negative_sum_one_resultfoldresult. (((((a) = 2 * (ge_balance_positive_sum_one_resultfoldresult) /\ (ge_balance_negative_sum_one_resultfoldresult) = 0) \/ exists ge_signed_half_sum_one_resultfoldresultdecode. (((a) = 2 * ge_signed_half_sum_one_resultfoldresultdecode + 1 /\ (ge_balance_positive_sum_one_resultfoldresult) = 0) /\ (ge_balance_negative_sum_one_resultfoldresult) = S ge_signed_half_sum_one_resultfoldresultdecode))) /\ ((dst_positive_sum_sum_one_resultfold) + ge_balance_negative_sum_one_resultfoldresult = (dst_negative_sum_sum_one_resultfold) + ge_balance_positive_sum_one_resultfoldresult)))))))))))))

Constructive proof overview

Generated structural guide

At n=1, the real two-entry masked fold is 0+F(1), so its exact value is F(1) regardless of F(0).

The unchanged tactic script uses 10 declared prerequisites and contains 84 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 divisor_signed_sum_empty_value Alpha theorem; checked-use authorized divisor_signed_sum_successor_intro Alpha theorem; checked-use authorized DV001D divisor_mask_omitted_entry DV001C divisor_mask_positive_quotient_entry zero_le Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized signed_add_zero_left 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

84 script commands · 24 reading checkpoints · 4 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 (4)
divisor mask prefix existsarithmetic signed sum existsdivisor mask omitted entrydivisor mask positive quotient entry

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 a
  4. L4
    intro ht
  5. L5
    intro hbound
  6. L6
    intro ha
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,1,1,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 (1)
  5. L11
    specialize divisor_mask_prefix_exists (1)
  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 hzeroL17–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 hzero : ∃ z. SignedPrefixSum(x,0,z)Definitions: SignedPrefixSum
  2. L18
    specialize arithmetic_signed_sum_exists (1)
  3. L19
    specialize arithmetic_signed_sum_exists (x)
  4. L20
    specialize arithmetic_signed_sum_exists (0)
  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 hzero
06Establish heqL24–30

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

  1. L24
    have heq : x1=0
  2. L25
    specialize divisor_signed_sum_empty_value (x)
  3. L26
    specialize divisor_signed_sum_empty_value (x1)
  4. L27
    apply divisor_signed_sum_empty_value
  5. L28
    exact hzero_witness
  6. L29
    rewrite heq at hzero_witness
  7. L30
    rewrite heq at hzero_witness
07Establish hfirstL31–40

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

  1. L31
    have hfirst : SignedPrefixSum(x,1,0)Definitions: SignedPrefixSum
  2. L32
    specialize divisor_signed_sum_successor_intro (x)
  3. L33
    specialize divisor_signed_sum_successor_intro (0)
  4. L34
    specialize divisor_signed_sum_successor_intro (0)
  5. L35
    specialize divisor_signed_sum_successor_intro (0)
  6. L36
    specialize divisor_signed_sum_successor_intro (0)
  7. L37
    apply divisor_signed_sum_successor_intro
  8. L38
    exact hzero_witness
  9. L39
    specialize divisor_mask_omitted_entry (F)
  10. L40
    specialize divisor_mask_omitted_entry (1)
08Use earlier factsL41–47

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

  1. L41
    specialize divisor_mask_omitted_entry (1)
  2. L42
    specialize divisor_mask_omitted_entry (x)
  3. L43
    specialize divisor_mask_omitted_entry (0)
  4. L44
    apply divisor_mask_omitted_entry
  5. L45
    exact hm_witness
  6. L46
    specialize zero_le (1)
  7. L47
    apply zero_le
09Separate the logical casesL48–48

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

  1. L48
    left
10Calculate and transport equalitiesL49–49

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

  1. L49
    refl
11Use earlier factsL50–51

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

  1. L50
    specialize signed_add_zero_left (0)
  2. L51
    apply signed_add_zero_left
12Separate the logical casesL52–52

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

  1. L52
    split
13Fix variables and assumptionsL53–53

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

  1. L53
    intro hnzero
14Use earlier factsL54–55

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

  1. L54
    apply PA1
  2. L55
    exact hnzero
15Construct an explicit witnessL56–56

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

  1. L56
    exists x
16Separate the logical casesL57–57

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

  1. L57
    split
17Use earlier factsL58–67

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

  1. L58
    exact hm_witness
  2. L59
    specialize divisor_signed_sum_successor_intro (x)
  3. L60
    specialize divisor_signed_sum_successor_intro (1)
  4. L61
    specialize divisor_signed_sum_successor_intro (0)
  5. L62
    specialize divisor_signed_sum_successor_intro (a)
  6. L63
    specialize divisor_signed_sum_successor_intro (a)
  7. L64
    apply divisor_signed_sum_successor_intro
  8. L65
    exact hfirst
  9. L66
    specialize divisor_mask_positive_quotient_entry (F)
  10. L67
    specialize divisor_mask_positive_quotient_entry (1)
18Use earlier factsL68–74

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

  1. L68
    specialize divisor_mask_positive_quotient_entry (1)
  2. L69
    specialize divisor_mask_positive_quotient_entry (x)
  3. L70
    specialize divisor_mask_positive_quotient_entry (1)
  4. L71
    specialize divisor_mask_positive_quotient_entry (1)
  5. L72
    specialize divisor_mask_positive_quotient_entry (a)
  6. L73
    apply divisor_mask_positive_quotient_entry
  7. L74
    exact hm_witness
19Construct an explicit witnessL75–75

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

  1. L75
    exists 0
20Use earlier factsL76–76

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

  1. L76
    apply zero_add
21Fix variables and assumptionsL77–77

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

  1. L77
    intro hd0
22Use earlier factsL78–79

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

  1. L78
    apply PA1
  2. L79
    exact hd0
23Calculate and transport equalitiesL80–80

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

  1. L80
    symm
24Use earlier factsL81–84

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

  1. L81
    apply one_mul
  2. L82
    exact ha
  3. L83
    specialize signed_add_zero_left (a)
  4. L84
    apply signed_add_zero_left

Library-wide reading audit

Original exact command ledger · 84 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro a
  4. 0004intro ht
  5. 0005intro hbound
  6. 0006intro ha
  7. 0007have hm : exists M. (((exists dst_positive_code_sum_one_masktable dst_positive_scale_sum_one_masktable dst_negative_code_sum_one_masktable dst_negative_scale_sum_one_masktable. (((M) = (((((dst_positive_code_sum_one_masktable) + (dst_positive_scale_sum_one_masktable)) * S ((dst_positive_code_sum_one_masktable) + (dst_positive_scale_sum_one_masktable)) + ((dst_positive_scale_sum_one_masktable) + (dst_positive_scale_sum_one_masktable))) + (((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) * S ((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) + ((dst_negative_scale_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)))) * S ((((dst_positive_code_sum_one_masktable) + (dst_positive_scale_sum_one_masktable)) * S ((dst_positive_code_sum_one_masktable) + (dst_positive_scale_sum_one_masktable)) + ((dst_positive_scale_sum_one_masktable) + (dst_positive_scale_sum_one_masktable))) + (((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) * S ((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) + ((dst_negative_scale_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)))) + ((((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) * S ((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) + ((dst_negative_scale_sum_one_masktable) + (dst_negative_scale_sum_one_masktable))) + (((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) * S ((dst_negative_code_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)) + ((dst_negative_scale_sum_one_masktable) + (dst_negative_scale_sum_one_masktable)))))) /\ (forall dst_index_sum_one_masktable. (exists pvs_le_gap_sum_one_masktabledomain. pvs_le_gap_sum_one_masktabledomain + (dst_index_sum_one_masktable) = (1)) -> exists dst_positive_sum_one_masktable dst_negative_sum_one_masktable dst_value_sum_one_masktable. ((((exists ff_h_pvs_sum_one_masktableentrypositive. ff_h_pvs_sum_one_masktableentrypositive + S (dst_positive_sum_one_masktable) = S ((S (dst_index_sum_one_masktable)) * dst_positive_scale_sum_one_masktable)) /\ exists ff_q_pvs_sum_one_masktableentrypositive. dst_positive_code_sum_one_masktable = ff_q_pvs_sum_one_masktableentrypositive * S ((S (dst_index_sum_one_masktable)) * dst_positive_scale_sum_one_masktable) + (dst_positive_sum_one_masktable))) /\ (((((exists ff_h_pvs_sum_one_masktableentrynegative. ff_h_pvs_sum_one_masktableentrynegative + S (dst_negative_sum_one_masktable) = S ((S (dst_index_sum_one_masktable)) * dst_negative_scale_sum_one_masktable)) /\ exists ff_q_pvs_sum_one_masktableentrynegative. dst_negative_code_sum_one_masktable = ff_q_pvs_sum_one_masktableentrynegative * S ((S (dst_index_sum_one_masktable)) * dst_negative_scale_sum_one_masktable) + (dst_negative_sum_one_masktable))) /\ (exists ge_balance_positive_sum_one_masktableentryvalue ge_balance_negative_sum_one_masktableentryvalue. (((((dst_value_sum_one_masktable) = 2 * (ge_balance_positive_sum_one_masktableentryvalue) /\ (ge_balance_negative_sum_one_masktableentryvalue) = 0) \/ exists ge_signed_half_sum_one_masktableentryvaluedecode. (((dst_value_sum_one_masktable) = 2 * ge_signed_half_sum_one_masktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_one_masktableentryvalue) = 0) /\ (ge_balance_negative_sum_one_masktableentryvalue) = S ge_signed_half_sum_one_masktableentryvaluedecode))) /\ ((dst_positive_sum_one_masktable) + ge_balance_negative_sum_one_masktableentryvalue = (dst_negative_sum_one_masktable) + ge_balance_positive_sum_one_masktableentryvalue))))))))) /\ (forall dm_index_sum_one_mask dm_value_sum_one_mask. (exists pvs_le_gap_sum_one_maskdomain. pvs_le_gap_sum_one_maskdomain + (dm_index_sum_one_mask) = (1)) -> (exists dst_positive_code_sum_one_masklookup dst_positive_scale_sum_one_masklookup dst_negative_code_sum_one_masklookup dst_negative_scale_sum_one_masklookup dst_positive_sum_one_masklookup dst_negative_sum_one_masklookup. (((M) = (((((dst_positive_code_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup)) * S ((dst_positive_code_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup)) + ((dst_positive_scale_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup))) + (((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) * S ((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) + ((dst_negative_scale_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)))) * S ((((dst_positive_code_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup)) * S ((dst_positive_code_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup)) + ((dst_positive_scale_sum_one_masklookup) + (dst_positive_scale_sum_one_masklookup))) + (((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) * S ((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) + ((dst_negative_scale_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)))) + ((((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) * S ((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) + ((dst_negative_scale_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup))) + (((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) * S ((dst_negative_code_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)) + ((dst_negative_scale_sum_one_masklookup) + (dst_negative_scale_sum_one_masklookup)))))) /\ (((((exists ff_h_pvs_sum_one_masklookuppositive. ff_h_pvs_sum_one_masklookuppositive + S (dst_positive_sum_one_masklookup) = S ((S (dm_index_sum_one_mask)) * dst_positive_scale_sum_one_masklookup)) /\ exists ff_q_pvs_sum_one_masklookuppositive. dst_positive_code_sum_one_masklookup = ff_q_pvs_sum_one_masklookuppositive * S ((S (dm_index_sum_one_mask)) * dst_positive_scale_sum_one_masklookup) + (dst_positive_sum_one_masklookup))) /\ (((((exists ff_h_pvs_sum_one_masklookupnegative. ff_h_pvs_sum_one_masklookupnegative + S (dst_negative_sum_one_masklookup) = S ((S (dm_index_sum_one_mask)) * dst_negative_scale_sum_one_masklookup)) /\ exists ff_q_pvs_sum_one_masklookupnegative. dst_negative_code_sum_one_masklookup = ff_q_pvs_sum_one_masklookupnegative * S ((S (dm_index_sum_one_mask)) * dst_negative_scale_sum_one_masklookup) + (dst_negative_sum_one_masklookup))) /\ (exists ge_balance_positive_sum_one_masklookupvalue ge_balance_negative_sum_one_masklookupvalue. (((((dm_value_sum_one_mask) = 2 * (ge_balance_positive_sum_one_masklookupvalue) /\ (ge_balance_negative_sum_one_masklookupvalue) = 0) \/ exists ge_signed_half_sum_one_masklookupvaluedecode. (((dm_value_sum_one_mask) = 2 * ge_signed_half_sum_one_masklookupvaluedecode + 1 /\ (ge_balance_positive_sum_one_masklookupvalue) = 0) /\ (ge_balance_negative_sum_one_masklookupvalue) = S ge_signed_half_sum_one_masklookupvaluedecode))) /\ ((dst_positive_sum_one_masklookup) + ge_balance_negative_sum_one_masklookupvalue = (dst_negative_sum_one_masklookup) + ge_balance_positive_sum_one_masklookupvalue))))))))) -> ((((~((dm_index_sum_one_mask)=0)) /\ (exists dm_quotient_sum_one_maskentry. (((1)=(dm_index_sum_one_mask)*dm_quotient_sum_one_maskentry) /\ (exists dst_positive_code_sum_one_maskentryinput dst_positive_scale_sum_one_maskentryinput dst_negative_code_sum_one_maskentryinput dst_negative_scale_sum_one_maskentryinput dst_positive_sum_one_maskentryinput dst_negative_sum_one_maskentryinput. (((F) = (((((dst_positive_code_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput)) * S ((dst_positive_code_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput)) + ((dst_positive_scale_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput))) + (((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) * S ((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) + ((dst_negative_scale_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)))) * S ((((dst_positive_code_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput)) * S ((dst_positive_code_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput)) + ((dst_positive_scale_sum_one_maskentryinput) + (dst_positive_scale_sum_one_maskentryinput))) + (((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) * S ((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) + ((dst_negative_scale_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)))) + ((((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) * S ((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) + ((dst_negative_scale_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput))) + (((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) * S ((dst_negative_code_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)) + ((dst_negative_scale_sum_one_maskentryinput) + (dst_negative_scale_sum_one_maskentryinput)))))) /\ (((((exists ff_h_pvs_sum_one_maskentryinputpositive. ff_h_pvs_sum_one_maskentryinputpositive + S (dst_positive_sum_one_maskentryinput) = S ((S (dm_index_sum_one_mask)) * dst_positive_scale_sum_one_maskentryinput)) /\ exists ff_q_pvs_sum_one_maskentryinputpositive. dst_positive_code_sum_one_maskentryinput = ff_q_pvs_sum_one_maskentryinputpositive * S ((S (dm_index_sum_one_mask)) * dst_positive_scale_sum_one_maskentryinput) + (dst_positive_sum_one_maskentryinput))) /\ (((((exists ff_h_pvs_sum_one_maskentryinputnegative. ff_h_pvs_sum_one_maskentryinputnegative + S (dst_negative_sum_one_maskentryinput) = S ((S (dm_index_sum_one_mask)) * dst_negative_scale_sum_one_maskentryinput)) /\ exists ff_q_pvs_sum_one_maskentryinputnegative. dst_negative_code_sum_one_maskentryinput = ff_q_pvs_sum_one_maskentryinputnegative * S ((S (dm_index_sum_one_mask)) * dst_negative_scale_sum_one_maskentryinput) + (dst_negative_sum_one_maskentryinput))) /\ (exists ge_balance_positive_sum_one_maskentryinputvalue ge_balance_negative_sum_one_maskentryinputvalue. (((((dm_value_sum_one_mask) = 2 * (ge_balance_positive_sum_one_maskentryinputvalue) /\ (ge_balance_negative_sum_one_maskentryinputvalue) = 0) \/ exists ge_signed_half_sum_one_maskentryinputvaluedecode. (((dm_value_sum_one_mask) = 2 * ge_signed_half_sum_one_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_one_maskentryinputvalue) = 0) /\ (ge_balance_negative_sum_one_maskentryinputvalue) = S ge_signed_half_sum_one_maskentryinputvaluedecode))) /\ ((dst_positive_sum_one_maskentryinput) + ge_balance_negative_sum_one_maskentryinputvalue = (dst_negative_sum_one_maskentryinput) + ge_balance_positive_sum_one_maskentryinputvalue))))))))))))) \/ ((((dm_index_sum_one_mask)=0 \/ ~(exists pvs_factor_sum_one_maskentrynondivisor. (1) = (dm_index_sum_one_mask) * pvs_factor_sum_one_maskentrynondivisor)) /\ ((dm_value_sum_one_mask)=0)))))))
  8. 0008specialize divisor_mask_prefix_exists (N)
  9. 0009specialize divisor_mask_prefix_exists (F)
  10. 0010specialize divisor_mask_prefix_exists (1)
  11. 0011specialize divisor_mask_prefix_exists (1)
  12. 0012apply divisor_mask_prefix_exists
  13. 0013exact ht
  14. 0014exact hbound
  15. 0015cases hm
  16. 0016cases hm_witness
  17. 0017have hzero : exists z. (exists dst_positive_code_sum_one_empty dst_positive_scale_sum_one_empty dst_negative_code_sum_one_empty dst_negative_scale_sum_one_empty dst_positive_sum_sum_one_empty dst_negative_sum_sum_one_empty. (((x) = (((((dst_positive_code_sum_one_empty) + (dst_positive_scale_sum_one_empty)) * S ((dst_positive_code_sum_one_empty) + (dst_positive_scale_sum_one_empty)) + ((dst_positive_scale_sum_one_empty) + (dst_positive_scale_sum_one_empty))) + (((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) * S ((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) + ((dst_negative_scale_sum_one_empty) + (dst_negative_scale_sum_one_empty)))) * S ((((dst_positive_code_sum_one_empty) + (dst_positive_scale_sum_one_empty)) * S ((dst_positive_code_sum_one_empty) + (dst_positive_scale_sum_one_empty)) + ((dst_positive_scale_sum_one_empty) + (dst_positive_scale_sum_one_empty))) + (((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) * S ((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) + ((dst_negative_scale_sum_one_empty) + (dst_negative_scale_sum_one_empty)))) + ((((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) * S ((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) + ((dst_negative_scale_sum_one_empty) + (dst_negative_scale_sum_one_empty))) + (((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) * S ((dst_negative_code_sum_one_empty) + (dst_negative_scale_sum_one_empty)) + ((dst_negative_scale_sum_one_empty) + (dst_negative_scale_sum_one_empty)))))) /\ (((exists fs_u_dst_sum_one_emptypositive fs_v_dst_sum_one_emptypositive. ((((exists fs_h_dst_sum_one_emptypositive_body_start. fs_h_dst_sum_one_emptypositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_emptypositive)) /\ exists fs_q_dst_sum_one_emptypositive_body_start. fs_u_dst_sum_one_emptypositive = fs_q_dst_sum_one_emptypositive_body_start * S ((S (0)) * fs_v_dst_sum_one_emptypositive) + (0))) /\ ((((exists fs_h_dst_sum_one_emptypositive_body_terminal. fs_h_dst_sum_one_emptypositive_body_terminal + S (dst_positive_sum_sum_one_empty) = S ((S (0)) * fs_v_dst_sum_one_emptypositive)) /\ exists fs_q_dst_sum_one_emptypositive_body_terminal. fs_u_dst_sum_one_emptypositive = fs_q_dst_sum_one_emptypositive_body_terminal * S ((S (0)) * fs_v_dst_sum_one_emptypositive) + (dst_positive_sum_sum_one_empty))) /\ forall fs_i_dst_sum_one_emptypositive_body_steps. (exists fs_lt_dst_sum_one_emptypositive_body_steps_bound. fs_lt_dst_sum_one_emptypositive_body_steps_bound + S fs_i_dst_sum_one_emptypositive_body_steps = 0) -> exists fs_a_dst_sum_one_emptypositive_body_steps fs_r_dst_sum_one_emptypositive_body_steps fs_s_dst_sum_one_emptypositive_body_steps. ((((exists fs_h_dst_sum_one_emptypositive_body_steps_summand. fs_h_dst_sum_one_emptypositive_body_steps_summand + S (fs_a_dst_sum_one_emptypositive_body_steps) = S ((S (fs_i_dst_sum_one_emptypositive_body_steps)) * dst_positive_scale_sum_one_empty)) /\ exists fs_q_dst_sum_one_emptypositive_body_steps_summand. dst_positive_code_sum_one_empty = fs_q_dst_sum_one_emptypositive_body_steps_summand * S ((S (fs_i_dst_sum_one_emptypositive_body_steps)) * dst_positive_scale_sum_one_empty) + (fs_a_dst_sum_one_emptypositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_emptypositive_body_steps_partial. fs_h_dst_sum_one_emptypositive_body_steps_partial + S (fs_r_dst_sum_one_emptypositive_body_steps) = S ((S (fs_i_dst_sum_one_emptypositive_body_steps)) * fs_v_dst_sum_one_emptypositive)) /\ exists fs_q_dst_sum_one_emptypositive_body_steps_partial. fs_u_dst_sum_one_emptypositive = fs_q_dst_sum_one_emptypositive_body_steps_partial * S ((S (fs_i_dst_sum_one_emptypositive_body_steps)) * fs_v_dst_sum_one_emptypositive) + (fs_r_dst_sum_one_emptypositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_emptypositive_body_steps_successor. fs_h_dst_sum_one_emptypositive_body_steps_successor + S (fs_s_dst_sum_one_emptypositive_body_steps) = S ((S (S fs_i_dst_sum_one_emptypositive_body_steps)) * fs_v_dst_sum_one_emptypositive)) /\ exists fs_q_dst_sum_one_emptypositive_body_steps_successor. fs_u_dst_sum_one_emptypositive = fs_q_dst_sum_one_emptypositive_body_steps_successor * S ((S (S fs_i_dst_sum_one_emptypositive_body_steps)) * fs_v_dst_sum_one_emptypositive) + (fs_s_dst_sum_one_emptypositive_body_steps))) /\ fs_s_dst_sum_one_emptypositive_body_steps = fs_r_dst_sum_one_emptypositive_body_steps + fs_a_dst_sum_one_emptypositive_body_steps)))))) /\ (((exists fs_u_dst_sum_one_emptynegative fs_v_dst_sum_one_emptynegative. ((((exists fs_h_dst_sum_one_emptynegative_body_start. fs_h_dst_sum_one_emptynegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_emptynegative)) /\ exists fs_q_dst_sum_one_emptynegative_body_start. fs_u_dst_sum_one_emptynegative = fs_q_dst_sum_one_emptynegative_body_start * S ((S (0)) * fs_v_dst_sum_one_emptynegative) + (0))) /\ ((((exists fs_h_dst_sum_one_emptynegative_body_terminal. fs_h_dst_sum_one_emptynegative_body_terminal + S (dst_negative_sum_sum_one_empty) = S ((S (0)) * fs_v_dst_sum_one_emptynegative)) /\ exists fs_q_dst_sum_one_emptynegative_body_terminal. fs_u_dst_sum_one_emptynegative = fs_q_dst_sum_one_emptynegative_body_terminal * S ((S (0)) * fs_v_dst_sum_one_emptynegative) + (dst_negative_sum_sum_one_empty))) /\ forall fs_i_dst_sum_one_emptynegative_body_steps. (exists fs_lt_dst_sum_one_emptynegative_body_steps_bound. fs_lt_dst_sum_one_emptynegative_body_steps_bound + S fs_i_dst_sum_one_emptynegative_body_steps = 0) -> exists fs_a_dst_sum_one_emptynegative_body_steps fs_r_dst_sum_one_emptynegative_body_steps fs_s_dst_sum_one_emptynegative_body_steps. ((((exists fs_h_dst_sum_one_emptynegative_body_steps_summand. fs_h_dst_sum_one_emptynegative_body_steps_summand + S (fs_a_dst_sum_one_emptynegative_body_steps) = S ((S (fs_i_dst_sum_one_emptynegative_body_steps)) * dst_negative_scale_sum_one_empty)) /\ exists fs_q_dst_sum_one_emptynegative_body_steps_summand. dst_negative_code_sum_one_empty = fs_q_dst_sum_one_emptynegative_body_steps_summand * S ((S (fs_i_dst_sum_one_emptynegative_body_steps)) * dst_negative_scale_sum_one_empty) + (fs_a_dst_sum_one_emptynegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_emptynegative_body_steps_partial. fs_h_dst_sum_one_emptynegative_body_steps_partial + S (fs_r_dst_sum_one_emptynegative_body_steps) = S ((S (fs_i_dst_sum_one_emptynegative_body_steps)) * fs_v_dst_sum_one_emptynegative)) /\ exists fs_q_dst_sum_one_emptynegative_body_steps_partial. fs_u_dst_sum_one_emptynegative = fs_q_dst_sum_one_emptynegative_body_steps_partial * S ((S (fs_i_dst_sum_one_emptynegative_body_steps)) * fs_v_dst_sum_one_emptynegative) + (fs_r_dst_sum_one_emptynegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_emptynegative_body_steps_successor. fs_h_dst_sum_one_emptynegative_body_steps_successor + S (fs_s_dst_sum_one_emptynegative_body_steps) = S ((S (S fs_i_dst_sum_one_emptynegative_body_steps)) * fs_v_dst_sum_one_emptynegative)) /\ exists fs_q_dst_sum_one_emptynegative_body_steps_successor. fs_u_dst_sum_one_emptynegative = fs_q_dst_sum_one_emptynegative_body_steps_successor * S ((S (S fs_i_dst_sum_one_emptynegative_body_steps)) * fs_v_dst_sum_one_emptynegative) + (fs_s_dst_sum_one_emptynegative_body_steps))) /\ fs_s_dst_sum_one_emptynegative_body_steps = fs_r_dst_sum_one_emptynegative_body_steps + fs_a_dst_sum_one_emptynegative_body_steps)))))) /\ (exists ge_balance_positive_sum_one_emptyresult ge_balance_negative_sum_one_emptyresult. (((((z) = 2 * (ge_balance_positive_sum_one_emptyresult) /\ (ge_balance_negative_sum_one_emptyresult) = 0) \/ exists ge_signed_half_sum_one_emptyresultdecode. (((z) = 2 * ge_signed_half_sum_one_emptyresultdecode + 1 /\ (ge_balance_positive_sum_one_emptyresult) = 0) /\ (ge_balance_negative_sum_one_emptyresult) = S ge_signed_half_sum_one_emptyresultdecode))) /\ ((dst_positive_sum_sum_one_empty) + ge_balance_negative_sum_one_emptyresult = (dst_negative_sum_sum_one_empty) + ge_balance_positive_sum_one_emptyresult)))))))))
  18. 0018specialize arithmetic_signed_sum_exists (1)
  19. 0019specialize arithmetic_signed_sum_exists (x)
  20. 0020specialize arithmetic_signed_sum_exists (0)
  21. 0021apply arithmetic_signed_sum_exists
  22. 0022exact hm_witness_left
  23. 0023cases hzero
  24. 0024have heq : x1=0
  25. 0025specialize divisor_signed_sum_empty_value (x)
  26. 0026specialize divisor_signed_sum_empty_value (x1)
  27. 0027apply divisor_signed_sum_empty_value
  28. 0028exact hzero_witness
  29. 0029rewrite heq at hzero_witness
  30. 0030rewrite heq at hzero_witness
  31. 0031have hfirst : exists dst_positive_code_sum_one_first dst_positive_scale_sum_one_first dst_negative_code_sum_one_first dst_negative_scale_sum_one_first dst_positive_sum_sum_one_first dst_negative_sum_sum_one_first. (((x) = (((((dst_positive_code_sum_one_first) + (dst_positive_scale_sum_one_first)) * S ((dst_positive_code_sum_one_first) + (dst_positive_scale_sum_one_first)) + ((dst_positive_scale_sum_one_first) + (dst_positive_scale_sum_one_first))) + (((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) * S ((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) + ((dst_negative_scale_sum_one_first) + (dst_negative_scale_sum_one_first)))) * S ((((dst_positive_code_sum_one_first) + (dst_positive_scale_sum_one_first)) * S ((dst_positive_code_sum_one_first) + (dst_positive_scale_sum_one_first)) + ((dst_positive_scale_sum_one_first) + (dst_positive_scale_sum_one_first))) + (((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) * S ((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) + ((dst_negative_scale_sum_one_first) + (dst_negative_scale_sum_one_first)))) + ((((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) * S ((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) + ((dst_negative_scale_sum_one_first) + (dst_negative_scale_sum_one_first))) + (((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) * S ((dst_negative_code_sum_one_first) + (dst_negative_scale_sum_one_first)) + ((dst_negative_scale_sum_one_first) + (dst_negative_scale_sum_one_first)))))) /\ (((exists fs_u_dst_sum_one_firstpositive fs_v_dst_sum_one_firstpositive. ((((exists fs_h_dst_sum_one_firstpositive_body_start. fs_h_dst_sum_one_firstpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_firstpositive)) /\ exists fs_q_dst_sum_one_firstpositive_body_start. fs_u_dst_sum_one_firstpositive = fs_q_dst_sum_one_firstpositive_body_start * S ((S (0)) * fs_v_dst_sum_one_firstpositive) + (0))) /\ ((((exists fs_h_dst_sum_one_firstpositive_body_terminal. fs_h_dst_sum_one_firstpositive_body_terminal + S (dst_positive_sum_sum_one_first) = S ((S (1)) * fs_v_dst_sum_one_firstpositive)) /\ exists fs_q_dst_sum_one_firstpositive_body_terminal. fs_u_dst_sum_one_firstpositive = fs_q_dst_sum_one_firstpositive_body_terminal * S ((S (1)) * fs_v_dst_sum_one_firstpositive) + (dst_positive_sum_sum_one_first))) /\ forall fs_i_dst_sum_one_firstpositive_body_steps. (exists fs_lt_dst_sum_one_firstpositive_body_steps_bound. fs_lt_dst_sum_one_firstpositive_body_steps_bound + S fs_i_dst_sum_one_firstpositive_body_steps = 1) -> exists fs_a_dst_sum_one_firstpositive_body_steps fs_r_dst_sum_one_firstpositive_body_steps fs_s_dst_sum_one_firstpositive_body_steps. ((((exists fs_h_dst_sum_one_firstpositive_body_steps_summand. fs_h_dst_sum_one_firstpositive_body_steps_summand + S (fs_a_dst_sum_one_firstpositive_body_steps) = S ((S (fs_i_dst_sum_one_firstpositive_body_steps)) * dst_positive_scale_sum_one_first)) /\ exists fs_q_dst_sum_one_firstpositive_body_steps_summand. dst_positive_code_sum_one_first = fs_q_dst_sum_one_firstpositive_body_steps_summand * S ((S (fs_i_dst_sum_one_firstpositive_body_steps)) * dst_positive_scale_sum_one_first) + (fs_a_dst_sum_one_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_firstpositive_body_steps_partial. fs_h_dst_sum_one_firstpositive_body_steps_partial + S (fs_r_dst_sum_one_firstpositive_body_steps) = S ((S (fs_i_dst_sum_one_firstpositive_body_steps)) * fs_v_dst_sum_one_firstpositive)) /\ exists fs_q_dst_sum_one_firstpositive_body_steps_partial. fs_u_dst_sum_one_firstpositive = fs_q_dst_sum_one_firstpositive_body_steps_partial * S ((S (fs_i_dst_sum_one_firstpositive_body_steps)) * fs_v_dst_sum_one_firstpositive) + (fs_r_dst_sum_one_firstpositive_body_steps))) /\ ((((exists fs_h_dst_sum_one_firstpositive_body_steps_successor. fs_h_dst_sum_one_firstpositive_body_steps_successor + S (fs_s_dst_sum_one_firstpositive_body_steps) = S ((S (S fs_i_dst_sum_one_firstpositive_body_steps)) * fs_v_dst_sum_one_firstpositive)) /\ exists fs_q_dst_sum_one_firstpositive_body_steps_successor. fs_u_dst_sum_one_firstpositive = fs_q_dst_sum_one_firstpositive_body_steps_successor * S ((S (S fs_i_dst_sum_one_firstpositive_body_steps)) * fs_v_dst_sum_one_firstpositive) + (fs_s_dst_sum_one_firstpositive_body_steps))) /\ fs_s_dst_sum_one_firstpositive_body_steps = fs_r_dst_sum_one_firstpositive_body_steps + fs_a_dst_sum_one_firstpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_one_firstnegative fs_v_dst_sum_one_firstnegative. ((((exists fs_h_dst_sum_one_firstnegative_body_start. fs_h_dst_sum_one_firstnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_one_firstnegative)) /\ exists fs_q_dst_sum_one_firstnegative_body_start. fs_u_dst_sum_one_firstnegative = fs_q_dst_sum_one_firstnegative_body_start * S ((S (0)) * fs_v_dst_sum_one_firstnegative) + (0))) /\ ((((exists fs_h_dst_sum_one_firstnegative_body_terminal. fs_h_dst_sum_one_firstnegative_body_terminal + S (dst_negative_sum_sum_one_first) = S ((S (1)) * fs_v_dst_sum_one_firstnegative)) /\ exists fs_q_dst_sum_one_firstnegative_body_terminal. fs_u_dst_sum_one_firstnegative = fs_q_dst_sum_one_firstnegative_body_terminal * S ((S (1)) * fs_v_dst_sum_one_firstnegative) + (dst_negative_sum_sum_one_first))) /\ forall fs_i_dst_sum_one_firstnegative_body_steps. (exists fs_lt_dst_sum_one_firstnegative_body_steps_bound. fs_lt_dst_sum_one_firstnegative_body_steps_bound + S fs_i_dst_sum_one_firstnegative_body_steps = 1) -> exists fs_a_dst_sum_one_firstnegative_body_steps fs_r_dst_sum_one_firstnegative_body_steps fs_s_dst_sum_one_firstnegative_body_steps. ((((exists fs_h_dst_sum_one_firstnegative_body_steps_summand. fs_h_dst_sum_one_firstnegative_body_steps_summand + S (fs_a_dst_sum_one_firstnegative_body_steps) = S ((S (fs_i_dst_sum_one_firstnegative_body_steps)) * dst_negative_scale_sum_one_first)) /\ exists fs_q_dst_sum_one_firstnegative_body_steps_summand. dst_negative_code_sum_one_first = fs_q_dst_sum_one_firstnegative_body_steps_summand * S ((S (fs_i_dst_sum_one_firstnegative_body_steps)) * dst_negative_scale_sum_one_first) + (fs_a_dst_sum_one_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_firstnegative_body_steps_partial. fs_h_dst_sum_one_firstnegative_body_steps_partial + S (fs_r_dst_sum_one_firstnegative_body_steps) = S ((S (fs_i_dst_sum_one_firstnegative_body_steps)) * fs_v_dst_sum_one_firstnegative)) /\ exists fs_q_dst_sum_one_firstnegative_body_steps_partial. fs_u_dst_sum_one_firstnegative = fs_q_dst_sum_one_firstnegative_body_steps_partial * S ((S (fs_i_dst_sum_one_firstnegative_body_steps)) * fs_v_dst_sum_one_firstnegative) + (fs_r_dst_sum_one_firstnegative_body_steps))) /\ ((((exists fs_h_dst_sum_one_firstnegative_body_steps_successor. fs_h_dst_sum_one_firstnegative_body_steps_successor + S (fs_s_dst_sum_one_firstnegative_body_steps) = S ((S (S fs_i_dst_sum_one_firstnegative_body_steps)) * fs_v_dst_sum_one_firstnegative)) /\ exists fs_q_dst_sum_one_firstnegative_body_steps_successor. fs_u_dst_sum_one_firstnegative = fs_q_dst_sum_one_firstnegative_body_steps_successor * S ((S (S fs_i_dst_sum_one_firstnegative_body_steps)) * fs_v_dst_sum_one_firstnegative) + (fs_s_dst_sum_one_firstnegative_body_steps))) /\ fs_s_dst_sum_one_firstnegative_body_steps = fs_r_dst_sum_one_firstnegative_body_steps + fs_a_dst_sum_one_firstnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_one_firstresult ge_balance_negative_sum_one_firstresult. (((((0) = 2 * (ge_balance_positive_sum_one_firstresult) /\ (ge_balance_negative_sum_one_firstresult) = 0) \/ exists ge_signed_half_sum_one_firstresultdecode. (((0) = 2 * ge_signed_half_sum_one_firstresultdecode + 1 /\ (ge_balance_positive_sum_one_firstresult) = 0) /\ (ge_balance_negative_sum_one_firstresult) = S ge_signed_half_sum_one_firstresultdecode))) /\ ((dst_positive_sum_sum_one_first) + ge_balance_negative_sum_one_firstresult = (dst_negative_sum_sum_one_first) + ge_balance_positive_sum_one_firstresult))))))))
  32. 0032specialize divisor_signed_sum_successor_intro (x)
  33. 0033specialize divisor_signed_sum_successor_intro (0)
  34. 0034specialize divisor_signed_sum_successor_intro (0)
  35. 0035specialize divisor_signed_sum_successor_intro (0)
  36. 0036specialize divisor_signed_sum_successor_intro (0)
  37. 0037apply divisor_signed_sum_successor_intro
  38. 0038exact hzero_witness
  39. 0039specialize divisor_mask_omitted_entry (F)
  40. 0040specialize divisor_mask_omitted_entry (1)
  41. 0041specialize divisor_mask_omitted_entry (1)
  42. 0042specialize divisor_mask_omitted_entry (x)
  43. 0043specialize divisor_mask_omitted_entry (0)
  44. 0044apply divisor_mask_omitted_entry
  45. 0045exact hm_witness
  46. 0046specialize zero_le (1)
  47. 0047apply zero_le
  48. 0048left
  49. 0049refl
  50. 0050specialize signed_add_zero_left (0)
  51. 0051apply signed_add_zero_left
  52. 0052split
  53. 0053intro hnzero
  54. 0054apply PA1
  55. 0055exact hnzero
  56. 0056exists x
  57. 0057split
  58. 0058exact hm_witness
  59. 0059specialize divisor_signed_sum_successor_intro (x)
  60. 0060specialize divisor_signed_sum_successor_intro (1)
  61. 0061specialize divisor_signed_sum_successor_intro (0)
  62. 0062specialize divisor_signed_sum_successor_intro (a)
  63. 0063specialize divisor_signed_sum_successor_intro (a)
  64. 0064apply divisor_signed_sum_successor_intro
  65. 0065exact hfirst
  66. 0066specialize divisor_mask_positive_quotient_entry (F)
  67. 0067specialize divisor_mask_positive_quotient_entry (1)
  68. 0068specialize divisor_mask_positive_quotient_entry (1)
  69. 0069specialize divisor_mask_positive_quotient_entry (x)
  70. 0070specialize divisor_mask_positive_quotient_entry (1)
  71. 0071specialize divisor_mask_positive_quotient_entry (1)
  72. 0072specialize divisor_mask_positive_quotient_entry (a)
  73. 0073apply divisor_mask_positive_quotient_entry
  74. 0074exact hm_witness
  75. 0075exists 0
  76. 0076apply zero_add
  77. 0077intro hd0
  78. 0078apply PA1
  79. 0079exact hd0
  80. 0080symm
  81. 0081apply one_mul
  82. 0082exact ha
  83. 0083specialize signed_add_zero_left (a)
  84. 0084apply signed_add_zero_left