RS0008

signed_rectangular_slice_sum_exists

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

Construct an actual affine slice and actual positive/negative prefix-sum traces; the result is not a supplied sum oracle.

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 F o s l. (exists dst_positive_code_sum_exists_input dst_positive_scale_sum_exists_input dst_negative_code_sum_exists_input dst_negative_scale_sum_exists_input. (((F) = (((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) * S ((((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) * S ((dst_positive_code_sum_exists_input) + (dst_positive_scale_sum_exists_input)) + ((dst_positive_scale_sum_exists_input) + (dst_positive_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))) + ((((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input))) + (((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) * S ((dst_negative_code_sum_exists_input) + (dst_negative_scale_sum_exists_input)) + ((dst_negative_scale_sum_exists_input) + (dst_negative_scale_sum_exists_input)))))) /\ (forall dst_index_sum_exists_input. (exists pvs_le_gap_sum_exists_inputdomain. pvs_le_gap_sum_exists_inputdomain + (dst_index_sum_exists_input) = (0)) -> exists dst_positive_sum_exists_input dst_negative_sum_exists_input dst_value_sum_exists_input. ((((exists ff_h_pvs_sum_exists_inputentrypositive. ff_h_pvs_sum_exists_inputentrypositive + S (dst_positive_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrypositive. dst_positive_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrypositive * S ((S (dst_index_sum_exists_input)) * dst_positive_scale_sum_exists_input) + (dst_positive_sum_exists_input))) /\ (((((exists ff_h_pvs_sum_exists_inputentrynegative. ff_h_pvs_sum_exists_inputentrynegative + S (dst_negative_sum_exists_input) = S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input)) /\ exists ff_q_pvs_sum_exists_inputentrynegative. dst_negative_code_sum_exists_input = ff_q_pvs_sum_exists_inputentrynegative * S ((S (dst_index_sum_exists_input)) * dst_negative_scale_sum_exists_input) + (dst_negative_sum_exists_input))) /\ (exists ge_balance_positive_sum_exists_inputentryvalue ge_balance_negative_sum_exists_inputentryvalue. (((((dst_value_sum_exists_input) = 2 * (ge_balance_positive_sum_exists_inputentryvalue) /\ (ge_balance_negative_sum_exists_inputentryvalue) = 0) \/ exists ge_signed_half_sum_exists_inputentryvaluedecode. (((dst_value_sum_exists_input) = 2 * ge_signed_half_sum_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_inputentryvalue) = 0) /\ (ge_balance_negative_sum_exists_inputentryvalue) = S ge_signed_half_sum_exists_inputentryvaluedecode))) /\ ((dst_positive_sum_exists_input) + ge_balance_negative_sum_exists_inputentryvalue = (dst_negative_sum_exists_input) + ge_balance_positive_sum_exists_inputentryvalue))))))))) -> exists z. (exists srs_slice_sum_exists_result. ((((exists dst_positive_code_sum_exists_resultslicesource_table dst_positive_scale_sum_exists_resultslicesource_table dst_negative_code_sum_exists_resultslicesource_table dst_negative_scale_sum_exists_resultslicesource_table. (((F) = (((((dst_positive_code_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table)) * S ((dst_positive_code_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table)) + ((dst_positive_scale_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table))) + (((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) * S ((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) + ((dst_negative_scale_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)))) * S ((((dst_positive_code_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table)) * S ((dst_positive_code_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table)) + ((dst_positive_scale_sum_exists_resultslicesource_table) + (dst_positive_scale_sum_exists_resultslicesource_table))) + (((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) * S ((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) + ((dst_negative_scale_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)))) + ((((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) * S ((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) + ((dst_negative_scale_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table))) + (((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) * S ((dst_negative_code_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)) + ((dst_negative_scale_sum_exists_resultslicesource_table) + (dst_negative_scale_sum_exists_resultslicesource_table)))))) /\ (forall dst_index_sum_exists_resultslicesource_table. (exists pvs_le_gap_sum_exists_resultslicesource_tabledomain. pvs_le_gap_sum_exists_resultslicesource_tabledomain + (dst_index_sum_exists_resultslicesource_table) = (0)) -> exists dst_positive_sum_exists_resultslicesource_table dst_negative_sum_exists_resultslicesource_table dst_value_sum_exists_resultslicesource_table. ((((exists ff_h_pvs_sum_exists_resultslicesource_tableentrypositive. ff_h_pvs_sum_exists_resultslicesource_tableentrypositive + S (dst_positive_sum_exists_resultslicesource_table) = S ((S (dst_index_sum_exists_resultslicesource_table)) * dst_positive_scale_sum_exists_resultslicesource_table)) /\ exists ff_q_pvs_sum_exists_resultslicesource_tableentrypositive. dst_positive_code_sum_exists_resultslicesource_table = ff_q_pvs_sum_exists_resultslicesource_tableentrypositive * S ((S (dst_index_sum_exists_resultslicesource_table)) * dst_positive_scale_sum_exists_resultslicesource_table) + (dst_positive_sum_exists_resultslicesource_table))) /\ (((((exists ff_h_pvs_sum_exists_resultslicesource_tableentrynegative. ff_h_pvs_sum_exists_resultslicesource_tableentrynegative + S (dst_negative_sum_exists_resultslicesource_table) = S ((S (dst_index_sum_exists_resultslicesource_table)) * dst_negative_scale_sum_exists_resultslicesource_table)) /\ exists ff_q_pvs_sum_exists_resultslicesource_tableentrynegative. dst_negative_code_sum_exists_resultslicesource_table = ff_q_pvs_sum_exists_resultslicesource_tableentrynegative * S ((S (dst_index_sum_exists_resultslicesource_table)) * dst_negative_scale_sum_exists_resultslicesource_table) + (dst_negative_sum_exists_resultslicesource_table))) /\ (exists ge_balance_positive_sum_exists_resultslicesource_tableentryvalue ge_balance_negative_sum_exists_resultslicesource_tableentryvalue. (((((dst_value_sum_exists_resultslicesource_table) = 2 * (ge_balance_positive_sum_exists_resultslicesource_tableentryvalue) /\ (ge_balance_negative_sum_exists_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_exists_resultslicesource_tableentryvaluedecode. (((dst_value_sum_exists_resultslicesource_table) = 2 * ge_signed_half_sum_exists_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_exists_resultslicesource_tableentryvalue) = S ge_signed_half_sum_exists_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_exists_resultslicesource_table) + ge_balance_negative_sum_exists_resultslicesource_tableentryvalue = (dst_negative_sum_exists_resultslicesource_table) + ge_balance_positive_sum_exists_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_exists_resultsliceoutput_table dst_positive_scale_sum_exists_resultsliceoutput_table dst_negative_code_sum_exists_resultsliceoutput_table dst_negative_scale_sum_exists_resultsliceoutput_table. (((srs_slice_sum_exists_result) = (((((dst_positive_code_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table)) * S ((dst_positive_code_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table)) + ((dst_positive_scale_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table))) + (((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) * S ((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) + ((dst_negative_scale_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)))) * S ((((dst_positive_code_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table)) * S ((dst_positive_code_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table)) + ((dst_positive_scale_sum_exists_resultsliceoutput_table) + (dst_positive_scale_sum_exists_resultsliceoutput_table))) + (((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) * S ((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) + ((dst_negative_scale_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)))) + ((((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) * S ((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) + ((dst_negative_scale_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table))) + (((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) * S ((dst_negative_code_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)) + ((dst_negative_scale_sum_exists_resultsliceoutput_table) + (dst_negative_scale_sum_exists_resultsliceoutput_table)))))) /\ (forall dst_index_sum_exists_resultsliceoutput_table. (exists pvs_le_gap_sum_exists_resultsliceoutput_tabledomain. pvs_le_gap_sum_exists_resultsliceoutput_tabledomain + (dst_index_sum_exists_resultsliceoutput_table) = (l)) -> exists dst_positive_sum_exists_resultsliceoutput_table dst_negative_sum_exists_resultsliceoutput_table dst_value_sum_exists_resultsliceoutput_table. ((((exists ff_h_pvs_sum_exists_resultsliceoutput_tableentrypositive. ff_h_pvs_sum_exists_resultsliceoutput_tableentrypositive + S (dst_positive_sum_exists_resultsliceoutput_table) = S ((S (dst_index_sum_exists_resultsliceoutput_table)) * dst_positive_scale_sum_exists_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_exists_resultsliceoutput_tableentrypositive. dst_positive_code_sum_exists_resultsliceoutput_table = ff_q_pvs_sum_exists_resultsliceoutput_tableentrypositive * S ((S (dst_index_sum_exists_resultsliceoutput_table)) * dst_positive_scale_sum_exists_resultsliceoutput_table) + (dst_positive_sum_exists_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_exists_resultsliceoutput_tableentrynegative. ff_h_pvs_sum_exists_resultsliceoutput_tableentrynegative + S (dst_negative_sum_exists_resultsliceoutput_table) = S ((S (dst_index_sum_exists_resultsliceoutput_table)) * dst_negative_scale_sum_exists_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_exists_resultsliceoutput_tableentrynegative. dst_negative_code_sum_exists_resultsliceoutput_table = ff_q_pvs_sum_exists_resultsliceoutput_tableentrynegative * S ((S (dst_index_sum_exists_resultsliceoutput_table)) * dst_negative_scale_sum_exists_resultsliceoutput_table) + (dst_negative_sum_exists_resultsliceoutput_table))) /\ (exists ge_balance_positive_sum_exists_resultsliceoutput_tableentryvalue ge_balance_negative_sum_exists_resultsliceoutput_tableentryvalue. (((((dst_value_sum_exists_resultsliceoutput_table) = 2 * (ge_balance_positive_sum_exists_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_exists_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_exists_resultsliceoutput_tableentryvaluedecode. (((dst_value_sum_exists_resultsliceoutput_table) = 2 * ge_signed_half_sum_exists_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_exists_resultsliceoutput_tableentryvalue) = S ge_signed_half_sum_exists_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_exists_resultsliceoutput_table) + ge_balance_negative_sum_exists_resultsliceoutput_tableentryvalue = (dst_negative_sum_exists_resultsliceoutput_table) + ge_balance_positive_sum_exists_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_exists_resultslice. (exists pvs_gap_sum_exists_resultslicebound. pvs_gap_sum_exists_resultslicebound + S (srs_index_sum_exists_resultslice) = (l)) -> exists srs_value_sum_exists_resultslice. (((exists dst_positive_code_sum_exists_resultsliceentrysource dst_positive_scale_sum_exists_resultsliceentrysource dst_negative_code_sum_exists_resultsliceentrysource dst_negative_scale_sum_exists_resultsliceentrysource dst_positive_sum_exists_resultsliceentrysource dst_negative_sum_exists_resultsliceentrysource. (((F) = (((((dst_positive_code_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource)) * S ((dst_positive_code_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource)) + ((dst_positive_scale_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource))) + (((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) * S ((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) + ((dst_negative_scale_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)))) * S ((((dst_positive_code_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource)) * S ((dst_positive_code_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource)) + ((dst_positive_scale_sum_exists_resultsliceentrysource) + (dst_positive_scale_sum_exists_resultsliceentrysource))) + (((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) * S ((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) + ((dst_negative_scale_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)))) + ((((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) * S ((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) + ((dst_negative_scale_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource))) + (((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) * S ((dst_negative_code_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)) + ((dst_negative_scale_sum_exists_resultsliceentrysource) + (dst_negative_scale_sum_exists_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_exists_resultsliceentrysourcepositive. ff_h_pvs_sum_exists_resultsliceentrysourcepositive + S (dst_positive_sum_exists_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_exists_resultslice))))) * dst_positive_scale_sum_exists_resultsliceentrysource)) /\ exists ff_q_pvs_sum_exists_resultsliceentrysourcepositive. dst_positive_code_sum_exists_resultsliceentrysource = ff_q_pvs_sum_exists_resultsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_exists_resultslice))))) * dst_positive_scale_sum_exists_resultsliceentrysource) + (dst_positive_sum_exists_resultsliceentrysource))) /\ (((((exists ff_h_pvs_sum_exists_resultsliceentrysourcenegative. ff_h_pvs_sum_exists_resultsliceentrysourcenegative + S (dst_negative_sum_exists_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_exists_resultslice))))) * dst_negative_scale_sum_exists_resultsliceentrysource)) /\ exists ff_q_pvs_sum_exists_resultsliceentrysourcenegative. dst_negative_code_sum_exists_resultsliceentrysource = ff_q_pvs_sum_exists_resultsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_exists_resultslice))))) * dst_negative_scale_sum_exists_resultsliceentrysource) + (dst_negative_sum_exists_resultsliceentrysource))) /\ (exists ge_balance_positive_sum_exists_resultsliceentrysourcevalue ge_balance_negative_sum_exists_resultsliceentrysourcevalue. (((((srs_value_sum_exists_resultslice) = 2 * (ge_balance_positive_sum_exists_resultsliceentrysourcevalue) /\ (ge_balance_negative_sum_exists_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_exists_resultsliceentrysourcevaluedecode. (((srs_value_sum_exists_resultslice) = 2 * ge_signed_half_sum_exists_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_exists_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_exists_resultsliceentrysourcevalue) = S ge_signed_half_sum_exists_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_exists_resultsliceentrysource) + ge_balance_negative_sum_exists_resultsliceentrysourcevalue = (dst_negative_sum_exists_resultsliceentrysource) + ge_balance_positive_sum_exists_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_exists_resultsliceentryoutput dst_positive_scale_sum_exists_resultsliceentryoutput dst_negative_code_sum_exists_resultsliceentryoutput dst_negative_scale_sum_exists_resultsliceentryoutput dst_positive_sum_exists_resultsliceentryoutput dst_negative_sum_exists_resultsliceentryoutput. (((srs_slice_sum_exists_result) = (((((dst_positive_code_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput)) * S ((dst_positive_code_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput)) + ((dst_positive_scale_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput))) + (((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) * S ((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) + ((dst_negative_scale_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)))) * S ((((dst_positive_code_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput)) * S ((dst_positive_code_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput)) + ((dst_positive_scale_sum_exists_resultsliceentryoutput) + (dst_positive_scale_sum_exists_resultsliceentryoutput))) + (((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) * S ((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) + ((dst_negative_scale_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)))) + ((((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) * S ((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) + ((dst_negative_scale_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput))) + (((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) * S ((dst_negative_code_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)) + ((dst_negative_scale_sum_exists_resultsliceentryoutput) + (dst_negative_scale_sum_exists_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_exists_resultsliceentryoutputpositive. ff_h_pvs_sum_exists_resultsliceentryoutputpositive + S (dst_positive_sum_exists_resultsliceentryoutput) = S ((S (srs_index_sum_exists_resultslice)) * dst_positive_scale_sum_exists_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_exists_resultsliceentryoutputpositive. dst_positive_code_sum_exists_resultsliceentryoutput = ff_q_pvs_sum_exists_resultsliceentryoutputpositive * S ((S (srs_index_sum_exists_resultslice)) * dst_positive_scale_sum_exists_resultsliceentryoutput) + (dst_positive_sum_exists_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_exists_resultsliceentryoutputnegative. ff_h_pvs_sum_exists_resultsliceentryoutputnegative + S (dst_negative_sum_exists_resultsliceentryoutput) = S ((S (srs_index_sum_exists_resultslice)) * dst_negative_scale_sum_exists_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_exists_resultsliceentryoutputnegative. dst_negative_code_sum_exists_resultsliceentryoutput = ff_q_pvs_sum_exists_resultsliceentryoutputnegative * S ((S (srs_index_sum_exists_resultslice)) * dst_negative_scale_sum_exists_resultsliceentryoutput) + (dst_negative_sum_exists_resultsliceentryoutput))) /\ (exists ge_balance_positive_sum_exists_resultsliceentryoutputvalue ge_balance_negative_sum_exists_resultsliceentryoutputvalue. (((((srs_value_sum_exists_resultslice) = 2 * (ge_balance_positive_sum_exists_resultsliceentryoutputvalue) /\ (ge_balance_negative_sum_exists_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_exists_resultsliceentryoutputvaluedecode. (((srs_value_sum_exists_resultslice) = 2 * ge_signed_half_sum_exists_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_exists_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_exists_resultsliceentryoutputvalue) = S ge_signed_half_sum_exists_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_exists_resultsliceentryoutput) + ge_balance_negative_sum_exists_resultsliceentryoutputvalue = (dst_negative_sum_exists_resultsliceentryoutput) + ge_balance_positive_sum_exists_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_exists_resultsum dst_positive_scale_sum_exists_resultsum dst_negative_code_sum_exists_resultsum dst_negative_scale_sum_exists_resultsum dst_positive_sum_sum_exists_resultsum dst_negative_sum_sum_exists_resultsum. (((srs_slice_sum_exists_result) = (((((dst_positive_code_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum)) * S ((dst_positive_code_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum)) + ((dst_positive_scale_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum))) + (((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) * S ((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) + ((dst_negative_scale_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)))) * S ((((dst_positive_code_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum)) * S ((dst_positive_code_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum)) + ((dst_positive_scale_sum_exists_resultsum) + (dst_positive_scale_sum_exists_resultsum))) + (((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) * S ((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) + ((dst_negative_scale_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)))) + ((((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) * S ((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) + ((dst_negative_scale_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum))) + (((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) * S ((dst_negative_code_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)) + ((dst_negative_scale_sum_exists_resultsum) + (dst_negative_scale_sum_exists_resultsum)))))) /\ (((exists fs_u_dst_sum_exists_resultsumpositive fs_v_dst_sum_exists_resultsumpositive. ((((exists fs_h_dst_sum_exists_resultsumpositive_body_start. fs_h_dst_sum_exists_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_resultsumpositive)) /\ exists fs_q_dst_sum_exists_resultsumpositive_body_start. fs_u_dst_sum_exists_resultsumpositive = fs_q_dst_sum_exists_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_exists_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_exists_resultsumpositive_body_terminal. fs_h_dst_sum_exists_resultsumpositive_body_terminal + S (dst_positive_sum_sum_exists_resultsum) = S ((S (l)) * fs_v_dst_sum_exists_resultsumpositive)) /\ exists fs_q_dst_sum_exists_resultsumpositive_body_terminal. fs_u_dst_sum_exists_resultsumpositive = fs_q_dst_sum_exists_resultsumpositive_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_resultsumpositive) + (dst_positive_sum_sum_exists_resultsum))) /\ forall fs_i_dst_sum_exists_resultsumpositive_body_steps. (exists fs_lt_dst_sum_exists_resultsumpositive_body_steps_bound. fs_lt_dst_sum_exists_resultsumpositive_body_steps_bound + S fs_i_dst_sum_exists_resultsumpositive_body_steps = l) -> exists fs_a_dst_sum_exists_resultsumpositive_body_steps fs_r_dst_sum_exists_resultsumpositive_body_steps fs_s_dst_sum_exists_resultsumpositive_body_steps. ((((exists fs_h_dst_sum_exists_resultsumpositive_body_steps_summand. fs_h_dst_sum_exists_resultsumpositive_body_steps_summand + S (fs_a_dst_sum_exists_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_exists_resultsumpositive_body_steps)) * dst_positive_scale_sum_exists_resultsum)) /\ exists fs_q_dst_sum_exists_resultsumpositive_body_steps_summand. dst_positive_code_sum_exists_resultsum = fs_q_dst_sum_exists_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_exists_resultsumpositive_body_steps)) * dst_positive_scale_sum_exists_resultsum) + (fs_a_dst_sum_exists_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_resultsumpositive_body_steps_partial. fs_h_dst_sum_exists_resultsumpositive_body_steps_partial + S (fs_r_dst_sum_exists_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_exists_resultsumpositive_body_steps)) * fs_v_dst_sum_exists_resultsumpositive)) /\ exists fs_q_dst_sum_exists_resultsumpositive_body_steps_partial. fs_u_dst_sum_exists_resultsumpositive = fs_q_dst_sum_exists_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_exists_resultsumpositive_body_steps)) * fs_v_dst_sum_exists_resultsumpositive) + (fs_r_dst_sum_exists_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_resultsumpositive_body_steps_successor. fs_h_dst_sum_exists_resultsumpositive_body_steps_successor + S (fs_s_dst_sum_exists_resultsumpositive_body_steps) = S ((S (S fs_i_dst_sum_exists_resultsumpositive_body_steps)) * fs_v_dst_sum_exists_resultsumpositive)) /\ exists fs_q_dst_sum_exists_resultsumpositive_body_steps_successor. fs_u_dst_sum_exists_resultsumpositive = fs_q_dst_sum_exists_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_exists_resultsumpositive_body_steps)) * fs_v_dst_sum_exists_resultsumpositive) + (fs_s_dst_sum_exists_resultsumpositive_body_steps))) /\ fs_s_dst_sum_exists_resultsumpositive_body_steps = fs_r_dst_sum_exists_resultsumpositive_body_steps + fs_a_dst_sum_exists_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_exists_resultsumnegative fs_v_dst_sum_exists_resultsumnegative. ((((exists fs_h_dst_sum_exists_resultsumnegative_body_start. fs_h_dst_sum_exists_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_resultsumnegative)) /\ exists fs_q_dst_sum_exists_resultsumnegative_body_start. fs_u_dst_sum_exists_resultsumnegative = fs_q_dst_sum_exists_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_exists_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_exists_resultsumnegative_body_terminal. fs_h_dst_sum_exists_resultsumnegative_body_terminal + S (dst_negative_sum_sum_exists_resultsum) = S ((S (l)) * fs_v_dst_sum_exists_resultsumnegative)) /\ exists fs_q_dst_sum_exists_resultsumnegative_body_terminal. fs_u_dst_sum_exists_resultsumnegative = fs_q_dst_sum_exists_resultsumnegative_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_resultsumnegative) + (dst_negative_sum_sum_exists_resultsum))) /\ forall fs_i_dst_sum_exists_resultsumnegative_body_steps. (exists fs_lt_dst_sum_exists_resultsumnegative_body_steps_bound. fs_lt_dst_sum_exists_resultsumnegative_body_steps_bound + S fs_i_dst_sum_exists_resultsumnegative_body_steps = l) -> exists fs_a_dst_sum_exists_resultsumnegative_body_steps fs_r_dst_sum_exists_resultsumnegative_body_steps fs_s_dst_sum_exists_resultsumnegative_body_steps. ((((exists fs_h_dst_sum_exists_resultsumnegative_body_steps_summand. fs_h_dst_sum_exists_resultsumnegative_body_steps_summand + S (fs_a_dst_sum_exists_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_exists_resultsumnegative_body_steps)) * dst_negative_scale_sum_exists_resultsum)) /\ exists fs_q_dst_sum_exists_resultsumnegative_body_steps_summand. dst_negative_code_sum_exists_resultsum = fs_q_dst_sum_exists_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_exists_resultsumnegative_body_steps)) * dst_negative_scale_sum_exists_resultsum) + (fs_a_dst_sum_exists_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_resultsumnegative_body_steps_partial. fs_h_dst_sum_exists_resultsumnegative_body_steps_partial + S (fs_r_dst_sum_exists_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_exists_resultsumnegative_body_steps)) * fs_v_dst_sum_exists_resultsumnegative)) /\ exists fs_q_dst_sum_exists_resultsumnegative_body_steps_partial. fs_u_dst_sum_exists_resultsumnegative = fs_q_dst_sum_exists_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_exists_resultsumnegative_body_steps)) * fs_v_dst_sum_exists_resultsumnegative) + (fs_r_dst_sum_exists_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_resultsumnegative_body_steps_successor. fs_h_dst_sum_exists_resultsumnegative_body_steps_successor + S (fs_s_dst_sum_exists_resultsumnegative_body_steps) = S ((S (S fs_i_dst_sum_exists_resultsumnegative_body_steps)) * fs_v_dst_sum_exists_resultsumnegative)) /\ exists fs_q_dst_sum_exists_resultsumnegative_body_steps_successor. fs_u_dst_sum_exists_resultsumnegative = fs_q_dst_sum_exists_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_exists_resultsumnegative_body_steps)) * fs_v_dst_sum_exists_resultsumnegative) + (fs_s_dst_sum_exists_resultsumnegative_body_steps))) /\ fs_s_dst_sum_exists_resultsumnegative_body_steps = fs_r_dst_sum_exists_resultsumnegative_body_steps + fs_a_dst_sum_exists_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_exists_resultsumresult ge_balance_negative_sum_exists_resultsumresult. (((((z) = 2 * (ge_balance_positive_sum_exists_resultsumresult) /\ (ge_balance_negative_sum_exists_resultsumresult) = 0) \/ exists ge_signed_half_sum_exists_resultsumresultdecode. (((z) = 2 * ge_signed_half_sum_exists_resultsumresultdecode + 1 /\ (ge_balance_positive_sum_exists_resultsumresult) = 0) /\ (ge_balance_negative_sum_exists_resultsumresult) = S ge_signed_half_sum_exists_resultsumresultdecode))) /\ ((dst_positive_sum_sum_exists_resultsum) + ge_balance_negative_sum_exists_resultsumresult = (dst_negative_sum_sum_exists_resultsum) + ge_balance_positive_sum_exists_resultsumresult)))))))))))

Constructive proof overview

Generated structural guide

Construct an actual affine slice and actual positive/negative prefix-sum traces; the result is not a supplied sum oracle.

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

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

Proof neighborhood

Direct dependencies

RS0006 signed_rectangular_slice_exists arithmetic_signed_sum_exists Alpha theorem; checked-use authorized

Direct dependents

RS000B signed_rectangular_slice_sum_empty_exists RS000F signed_rectangular_slice_sum_exists_unique RS0015 signed_rectangular_row_sums_exists

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

27 script commands · 10 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
signed rectangular slice 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–5

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

  1. L1
    intro F
  2. L2
    intro o
  3. L3
    intro s
  4. L4
    intro l
  5. L5
    intro hF
02Establish hgL6–12

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

  1. L6
    have hg : ∃ G. ArithSlice(F,G,o,s,l)Definitions: ArithSlice
  2. L7
    specialize signed_rectangular_slice_exists (l)
  3. L8
    specialize signed_rectangular_slice_exists (F)
  4. L9
    specialize signed_rectangular_slice_exists (o)
  5. L10
    specialize signed_rectangular_slice_exists (s)
  6. L11
    apply signed_rectangular_slice_exists
  7. L12
    exact hF
03Separate the logical casesL13–13

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

  1. L13
    cases hg
04Establish hzL14–18

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

  1. L14
    have hz : ∃ z. SignedPrefixSum(x,l,z)Definitions: SignedPrefixSum
  2. L15
    specialize arithmetic_signed_sum_exists (l)
  3. L16
    specialize arithmetic_signed_sum_exists (x)
  4. L17
    specialize arithmetic_signed_sum_exists (l)
  5. L18
    apply arithmetic_signed_sum_exists
05Separate the logical casesL19–20

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

  1. L19
    cases hg_witness
  2. L20
    cases hg_witness_right
06Use earlier factsL21–21

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

  1. L21
    exact hg_witness_right_left
07Separate the logical casesL22–22

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

  1. L22
    cases hz
08Construct an explicit witnessL23–24

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

  1. L23
    exists x1
  2. L24
    exists x
09Separate the logical casesL25–25

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

  1. L25
    split
10Use earlier factsL26–27

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

  1. L26
    exact hg_witness
  2. L27
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 27 lines
  1. 0001intro F
  2. 0002intro o
  3. 0003intro s
  4. 0004intro l
  5. 0005intro hF
  6. 0006have hg : exists G. (((exists dst_positive_code_sum_exists_slicesource_table dst_positive_scale_sum_exists_slicesource_table dst_negative_code_sum_exists_slicesource_table dst_negative_scale_sum_exists_slicesource_table. (((F) = (((((dst_positive_code_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table)) * S ((dst_positive_code_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table)) + ((dst_positive_scale_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table))) + (((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) * S ((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) + ((dst_negative_scale_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)))) * S ((((dst_positive_code_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table)) * S ((dst_positive_code_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table)) + ((dst_positive_scale_sum_exists_slicesource_table) + (dst_positive_scale_sum_exists_slicesource_table))) + (((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) * S ((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) + ((dst_negative_scale_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)))) + ((((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) * S ((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) + ((dst_negative_scale_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table))) + (((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) * S ((dst_negative_code_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)) + ((dst_negative_scale_sum_exists_slicesource_table) + (dst_negative_scale_sum_exists_slicesource_table)))))) /\ (forall dst_index_sum_exists_slicesource_table. (exists pvs_le_gap_sum_exists_slicesource_tabledomain. pvs_le_gap_sum_exists_slicesource_tabledomain + (dst_index_sum_exists_slicesource_table) = (0)) -> exists dst_positive_sum_exists_slicesource_table dst_negative_sum_exists_slicesource_table dst_value_sum_exists_slicesource_table. ((((exists ff_h_pvs_sum_exists_slicesource_tableentrypositive. ff_h_pvs_sum_exists_slicesource_tableentrypositive + S (dst_positive_sum_exists_slicesource_table) = S ((S (dst_index_sum_exists_slicesource_table)) * dst_positive_scale_sum_exists_slicesource_table)) /\ exists ff_q_pvs_sum_exists_slicesource_tableentrypositive. dst_positive_code_sum_exists_slicesource_table = ff_q_pvs_sum_exists_slicesource_tableentrypositive * S ((S (dst_index_sum_exists_slicesource_table)) * dst_positive_scale_sum_exists_slicesource_table) + (dst_positive_sum_exists_slicesource_table))) /\ (((((exists ff_h_pvs_sum_exists_slicesource_tableentrynegative. ff_h_pvs_sum_exists_slicesource_tableentrynegative + S (dst_negative_sum_exists_slicesource_table) = S ((S (dst_index_sum_exists_slicesource_table)) * dst_negative_scale_sum_exists_slicesource_table)) /\ exists ff_q_pvs_sum_exists_slicesource_tableentrynegative. dst_negative_code_sum_exists_slicesource_table = ff_q_pvs_sum_exists_slicesource_tableentrynegative * S ((S (dst_index_sum_exists_slicesource_table)) * dst_negative_scale_sum_exists_slicesource_table) + (dst_negative_sum_exists_slicesource_table))) /\ (exists ge_balance_positive_sum_exists_slicesource_tableentryvalue ge_balance_negative_sum_exists_slicesource_tableentryvalue. (((((dst_value_sum_exists_slicesource_table) = 2 * (ge_balance_positive_sum_exists_slicesource_tableentryvalue) /\ (ge_balance_negative_sum_exists_slicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_exists_slicesource_tableentryvaluedecode. (((dst_value_sum_exists_slicesource_table) = 2 * ge_signed_half_sum_exists_slicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_slicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_exists_slicesource_tableentryvalue) = S ge_signed_half_sum_exists_slicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_exists_slicesource_table) + ge_balance_negative_sum_exists_slicesource_tableentryvalue = (dst_negative_sum_exists_slicesource_table) + ge_balance_positive_sum_exists_slicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_exists_sliceoutput_table dst_positive_scale_sum_exists_sliceoutput_table dst_negative_code_sum_exists_sliceoutput_table dst_negative_scale_sum_exists_sliceoutput_table. (((G) = (((((dst_positive_code_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table)) * S ((dst_positive_code_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table)) + ((dst_positive_scale_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table))) + (((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) * S ((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) + ((dst_negative_scale_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)))) * S ((((dst_positive_code_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table)) * S ((dst_positive_code_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table)) + ((dst_positive_scale_sum_exists_sliceoutput_table) + (dst_positive_scale_sum_exists_sliceoutput_table))) + (((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) * S ((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) + ((dst_negative_scale_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)))) + ((((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) * S ((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) + ((dst_negative_scale_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table))) + (((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) * S ((dst_negative_code_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)) + ((dst_negative_scale_sum_exists_sliceoutput_table) + (dst_negative_scale_sum_exists_sliceoutput_table)))))) /\ (forall dst_index_sum_exists_sliceoutput_table. (exists pvs_le_gap_sum_exists_sliceoutput_tabledomain. pvs_le_gap_sum_exists_sliceoutput_tabledomain + (dst_index_sum_exists_sliceoutput_table) = (l)) -> exists dst_positive_sum_exists_sliceoutput_table dst_negative_sum_exists_sliceoutput_table dst_value_sum_exists_sliceoutput_table. ((((exists ff_h_pvs_sum_exists_sliceoutput_tableentrypositive. ff_h_pvs_sum_exists_sliceoutput_tableentrypositive + S (dst_positive_sum_exists_sliceoutput_table) = S ((S (dst_index_sum_exists_sliceoutput_table)) * dst_positive_scale_sum_exists_sliceoutput_table)) /\ exists ff_q_pvs_sum_exists_sliceoutput_tableentrypositive. dst_positive_code_sum_exists_sliceoutput_table = ff_q_pvs_sum_exists_sliceoutput_tableentrypositive * S ((S (dst_index_sum_exists_sliceoutput_table)) * dst_positive_scale_sum_exists_sliceoutput_table) + (dst_positive_sum_exists_sliceoutput_table))) /\ (((((exists ff_h_pvs_sum_exists_sliceoutput_tableentrynegative. ff_h_pvs_sum_exists_sliceoutput_tableentrynegative + S (dst_negative_sum_exists_sliceoutput_table) = S ((S (dst_index_sum_exists_sliceoutput_table)) * dst_negative_scale_sum_exists_sliceoutput_table)) /\ exists ff_q_pvs_sum_exists_sliceoutput_tableentrynegative. dst_negative_code_sum_exists_sliceoutput_table = ff_q_pvs_sum_exists_sliceoutput_tableentrynegative * S ((S (dst_index_sum_exists_sliceoutput_table)) * dst_negative_scale_sum_exists_sliceoutput_table) + (dst_negative_sum_exists_sliceoutput_table))) /\ (exists ge_balance_positive_sum_exists_sliceoutput_tableentryvalue ge_balance_negative_sum_exists_sliceoutput_tableentryvalue. (((((dst_value_sum_exists_sliceoutput_table) = 2 * (ge_balance_positive_sum_exists_sliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_exists_sliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_exists_sliceoutput_tableentryvaluedecode. (((dst_value_sum_exists_sliceoutput_table) = 2 * ge_signed_half_sum_exists_sliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_exists_sliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_exists_sliceoutput_tableentryvalue) = S ge_signed_half_sum_exists_sliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_exists_sliceoutput_table) + ge_balance_negative_sum_exists_sliceoutput_tableentryvalue = (dst_negative_sum_exists_sliceoutput_table) + ge_balance_positive_sum_exists_sliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_exists_slice. (exists pvs_gap_sum_exists_slicebound. pvs_gap_sum_exists_slicebound + S (srs_index_sum_exists_slice) = (l)) -> exists srs_value_sum_exists_slice. (((exists dst_positive_code_sum_exists_sliceentrysource dst_positive_scale_sum_exists_sliceentrysource dst_negative_code_sum_exists_sliceentrysource dst_negative_scale_sum_exists_sliceentrysource dst_positive_sum_exists_sliceentrysource dst_negative_sum_exists_sliceentrysource. (((F) = (((((dst_positive_code_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource)) * S ((dst_positive_code_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource)) + ((dst_positive_scale_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource))) + (((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) * S ((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) + ((dst_negative_scale_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)))) * S ((((dst_positive_code_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource)) * S ((dst_positive_code_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource)) + ((dst_positive_scale_sum_exists_sliceentrysource) + (dst_positive_scale_sum_exists_sliceentrysource))) + (((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) * S ((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) + ((dst_negative_scale_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)))) + ((((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) * S ((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) + ((dst_negative_scale_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource))) + (((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) * S ((dst_negative_code_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)) + ((dst_negative_scale_sum_exists_sliceentrysource) + (dst_negative_scale_sum_exists_sliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_exists_sliceentrysourcepositive. ff_h_pvs_sum_exists_sliceentrysourcepositive + S (dst_positive_sum_exists_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_exists_slice))))) * dst_positive_scale_sum_exists_sliceentrysource)) /\ exists ff_q_pvs_sum_exists_sliceentrysourcepositive. dst_positive_code_sum_exists_sliceentrysource = ff_q_pvs_sum_exists_sliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_exists_slice))))) * dst_positive_scale_sum_exists_sliceentrysource) + (dst_positive_sum_exists_sliceentrysource))) /\ (((((exists ff_h_pvs_sum_exists_sliceentrysourcenegative. ff_h_pvs_sum_exists_sliceentrysourcenegative + S (dst_negative_sum_exists_sliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_exists_slice))))) * dst_negative_scale_sum_exists_sliceentrysource)) /\ exists ff_q_pvs_sum_exists_sliceentrysourcenegative. dst_negative_code_sum_exists_sliceentrysource = ff_q_pvs_sum_exists_sliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_exists_slice))))) * dst_negative_scale_sum_exists_sliceentrysource) + (dst_negative_sum_exists_sliceentrysource))) /\ (exists ge_balance_positive_sum_exists_sliceentrysourcevalue ge_balance_negative_sum_exists_sliceentrysourcevalue. (((((srs_value_sum_exists_slice) = 2 * (ge_balance_positive_sum_exists_sliceentrysourcevalue) /\ (ge_balance_negative_sum_exists_sliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_exists_sliceentrysourcevaluedecode. (((srs_value_sum_exists_slice) = 2 * ge_signed_half_sum_exists_sliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_exists_sliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_exists_sliceentrysourcevalue) = S ge_signed_half_sum_exists_sliceentrysourcevaluedecode))) /\ ((dst_positive_sum_exists_sliceentrysource) + ge_balance_negative_sum_exists_sliceentrysourcevalue = (dst_negative_sum_exists_sliceentrysource) + ge_balance_positive_sum_exists_sliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_exists_sliceentryoutput dst_positive_scale_sum_exists_sliceentryoutput dst_negative_code_sum_exists_sliceentryoutput dst_negative_scale_sum_exists_sliceentryoutput dst_positive_sum_exists_sliceentryoutput dst_negative_sum_exists_sliceentryoutput. (((G) = (((((dst_positive_code_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput)) * S ((dst_positive_code_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput)) + ((dst_positive_scale_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput))) + (((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) * S ((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) + ((dst_negative_scale_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)))) * S ((((dst_positive_code_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput)) * S ((dst_positive_code_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput)) + ((dst_positive_scale_sum_exists_sliceentryoutput) + (dst_positive_scale_sum_exists_sliceentryoutput))) + (((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) * S ((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) + ((dst_negative_scale_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)))) + ((((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) * S ((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) + ((dst_negative_scale_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput))) + (((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) * S ((dst_negative_code_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)) + ((dst_negative_scale_sum_exists_sliceentryoutput) + (dst_negative_scale_sum_exists_sliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_exists_sliceentryoutputpositive. ff_h_pvs_sum_exists_sliceentryoutputpositive + S (dst_positive_sum_exists_sliceentryoutput) = S ((S (srs_index_sum_exists_slice)) * dst_positive_scale_sum_exists_sliceentryoutput)) /\ exists ff_q_pvs_sum_exists_sliceentryoutputpositive. dst_positive_code_sum_exists_sliceentryoutput = ff_q_pvs_sum_exists_sliceentryoutputpositive * S ((S (srs_index_sum_exists_slice)) * dst_positive_scale_sum_exists_sliceentryoutput) + (dst_positive_sum_exists_sliceentryoutput))) /\ (((((exists ff_h_pvs_sum_exists_sliceentryoutputnegative. ff_h_pvs_sum_exists_sliceentryoutputnegative + S (dst_negative_sum_exists_sliceentryoutput) = S ((S (srs_index_sum_exists_slice)) * dst_negative_scale_sum_exists_sliceentryoutput)) /\ exists ff_q_pvs_sum_exists_sliceentryoutputnegative. dst_negative_code_sum_exists_sliceentryoutput = ff_q_pvs_sum_exists_sliceentryoutputnegative * S ((S (srs_index_sum_exists_slice)) * dst_negative_scale_sum_exists_sliceentryoutput) + (dst_negative_sum_exists_sliceentryoutput))) /\ (exists ge_balance_positive_sum_exists_sliceentryoutputvalue ge_balance_negative_sum_exists_sliceentryoutputvalue. (((((srs_value_sum_exists_slice) = 2 * (ge_balance_positive_sum_exists_sliceentryoutputvalue) /\ (ge_balance_negative_sum_exists_sliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_exists_sliceentryoutputvaluedecode. (((srs_value_sum_exists_slice) = 2 * ge_signed_half_sum_exists_sliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_exists_sliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_exists_sliceentryoutputvalue) = S ge_signed_half_sum_exists_sliceentryoutputvaluedecode))) /\ ((dst_positive_sum_exists_sliceentryoutput) + ge_balance_negative_sum_exists_sliceentryoutputvalue = (dst_negative_sum_exists_sliceentryoutput) + ge_balance_positive_sum_exists_sliceentryoutputvalue))))))))))))))))
  7. 0007specialize signed_rectangular_slice_exists (l)
  8. 0008specialize signed_rectangular_slice_exists (F)
  9. 0009specialize signed_rectangular_slice_exists (o)
  10. 0010specialize signed_rectangular_slice_exists (s)
  11. 0011apply signed_rectangular_slice_exists
  12. 0012exact hF
  13. 0013cases hg
  14. 0014have hz : exists z. (exists dst_positive_code_sum_exists_value dst_positive_scale_sum_exists_value dst_negative_code_sum_exists_value dst_negative_scale_sum_exists_value dst_positive_sum_sum_exists_value dst_negative_sum_sum_exists_value. (((x) = (((((dst_positive_code_sum_exists_value) + (dst_positive_scale_sum_exists_value)) * S ((dst_positive_code_sum_exists_value) + (dst_positive_scale_sum_exists_value)) + ((dst_positive_scale_sum_exists_value) + (dst_positive_scale_sum_exists_value))) + (((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) * S ((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) + ((dst_negative_scale_sum_exists_value) + (dst_negative_scale_sum_exists_value)))) * S ((((dst_positive_code_sum_exists_value) + (dst_positive_scale_sum_exists_value)) * S ((dst_positive_code_sum_exists_value) + (dst_positive_scale_sum_exists_value)) + ((dst_positive_scale_sum_exists_value) + (dst_positive_scale_sum_exists_value))) + (((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) * S ((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) + ((dst_negative_scale_sum_exists_value) + (dst_negative_scale_sum_exists_value)))) + ((((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) * S ((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) + ((dst_negative_scale_sum_exists_value) + (dst_negative_scale_sum_exists_value))) + (((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) * S ((dst_negative_code_sum_exists_value) + (dst_negative_scale_sum_exists_value)) + ((dst_negative_scale_sum_exists_value) + (dst_negative_scale_sum_exists_value)))))) /\ (((exists fs_u_dst_sum_exists_valuepositive fs_v_dst_sum_exists_valuepositive. ((((exists fs_h_dst_sum_exists_valuepositive_body_start. fs_h_dst_sum_exists_valuepositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_valuepositive)) /\ exists fs_q_dst_sum_exists_valuepositive_body_start. fs_u_dst_sum_exists_valuepositive = fs_q_dst_sum_exists_valuepositive_body_start * S ((S (0)) * fs_v_dst_sum_exists_valuepositive) + (0))) /\ ((((exists fs_h_dst_sum_exists_valuepositive_body_terminal. fs_h_dst_sum_exists_valuepositive_body_terminal + S (dst_positive_sum_sum_exists_value) = S ((S (l)) * fs_v_dst_sum_exists_valuepositive)) /\ exists fs_q_dst_sum_exists_valuepositive_body_terminal. fs_u_dst_sum_exists_valuepositive = fs_q_dst_sum_exists_valuepositive_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_valuepositive) + (dst_positive_sum_sum_exists_value))) /\ forall fs_i_dst_sum_exists_valuepositive_body_steps. (exists fs_lt_dst_sum_exists_valuepositive_body_steps_bound. fs_lt_dst_sum_exists_valuepositive_body_steps_bound + S fs_i_dst_sum_exists_valuepositive_body_steps = l) -> exists fs_a_dst_sum_exists_valuepositive_body_steps fs_r_dst_sum_exists_valuepositive_body_steps fs_s_dst_sum_exists_valuepositive_body_steps. ((((exists fs_h_dst_sum_exists_valuepositive_body_steps_summand. fs_h_dst_sum_exists_valuepositive_body_steps_summand + S (fs_a_dst_sum_exists_valuepositive_body_steps) = S ((S (fs_i_dst_sum_exists_valuepositive_body_steps)) * dst_positive_scale_sum_exists_value)) /\ exists fs_q_dst_sum_exists_valuepositive_body_steps_summand. dst_positive_code_sum_exists_value = fs_q_dst_sum_exists_valuepositive_body_steps_summand * S ((S (fs_i_dst_sum_exists_valuepositive_body_steps)) * dst_positive_scale_sum_exists_value) + (fs_a_dst_sum_exists_valuepositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_valuepositive_body_steps_partial. fs_h_dst_sum_exists_valuepositive_body_steps_partial + S (fs_r_dst_sum_exists_valuepositive_body_steps) = S ((S (fs_i_dst_sum_exists_valuepositive_body_steps)) * fs_v_dst_sum_exists_valuepositive)) /\ exists fs_q_dst_sum_exists_valuepositive_body_steps_partial. fs_u_dst_sum_exists_valuepositive = fs_q_dst_sum_exists_valuepositive_body_steps_partial * S ((S (fs_i_dst_sum_exists_valuepositive_body_steps)) * fs_v_dst_sum_exists_valuepositive) + (fs_r_dst_sum_exists_valuepositive_body_steps))) /\ ((((exists fs_h_dst_sum_exists_valuepositive_body_steps_successor. fs_h_dst_sum_exists_valuepositive_body_steps_successor + S (fs_s_dst_sum_exists_valuepositive_body_steps) = S ((S (S fs_i_dst_sum_exists_valuepositive_body_steps)) * fs_v_dst_sum_exists_valuepositive)) /\ exists fs_q_dst_sum_exists_valuepositive_body_steps_successor. fs_u_dst_sum_exists_valuepositive = fs_q_dst_sum_exists_valuepositive_body_steps_successor * S ((S (S fs_i_dst_sum_exists_valuepositive_body_steps)) * fs_v_dst_sum_exists_valuepositive) + (fs_s_dst_sum_exists_valuepositive_body_steps))) /\ fs_s_dst_sum_exists_valuepositive_body_steps = fs_r_dst_sum_exists_valuepositive_body_steps + fs_a_dst_sum_exists_valuepositive_body_steps)))))) /\ (((exists fs_u_dst_sum_exists_valuenegative fs_v_dst_sum_exists_valuenegative. ((((exists fs_h_dst_sum_exists_valuenegative_body_start. fs_h_dst_sum_exists_valuenegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_exists_valuenegative)) /\ exists fs_q_dst_sum_exists_valuenegative_body_start. fs_u_dst_sum_exists_valuenegative = fs_q_dst_sum_exists_valuenegative_body_start * S ((S (0)) * fs_v_dst_sum_exists_valuenegative) + (0))) /\ ((((exists fs_h_dst_sum_exists_valuenegative_body_terminal. fs_h_dst_sum_exists_valuenegative_body_terminal + S (dst_negative_sum_sum_exists_value) = S ((S (l)) * fs_v_dst_sum_exists_valuenegative)) /\ exists fs_q_dst_sum_exists_valuenegative_body_terminal. fs_u_dst_sum_exists_valuenegative = fs_q_dst_sum_exists_valuenegative_body_terminal * S ((S (l)) * fs_v_dst_sum_exists_valuenegative) + (dst_negative_sum_sum_exists_value))) /\ forall fs_i_dst_sum_exists_valuenegative_body_steps. (exists fs_lt_dst_sum_exists_valuenegative_body_steps_bound. fs_lt_dst_sum_exists_valuenegative_body_steps_bound + S fs_i_dst_sum_exists_valuenegative_body_steps = l) -> exists fs_a_dst_sum_exists_valuenegative_body_steps fs_r_dst_sum_exists_valuenegative_body_steps fs_s_dst_sum_exists_valuenegative_body_steps. ((((exists fs_h_dst_sum_exists_valuenegative_body_steps_summand. fs_h_dst_sum_exists_valuenegative_body_steps_summand + S (fs_a_dst_sum_exists_valuenegative_body_steps) = S ((S (fs_i_dst_sum_exists_valuenegative_body_steps)) * dst_negative_scale_sum_exists_value)) /\ exists fs_q_dst_sum_exists_valuenegative_body_steps_summand. dst_negative_code_sum_exists_value = fs_q_dst_sum_exists_valuenegative_body_steps_summand * S ((S (fs_i_dst_sum_exists_valuenegative_body_steps)) * dst_negative_scale_sum_exists_value) + (fs_a_dst_sum_exists_valuenegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_valuenegative_body_steps_partial. fs_h_dst_sum_exists_valuenegative_body_steps_partial + S (fs_r_dst_sum_exists_valuenegative_body_steps) = S ((S (fs_i_dst_sum_exists_valuenegative_body_steps)) * fs_v_dst_sum_exists_valuenegative)) /\ exists fs_q_dst_sum_exists_valuenegative_body_steps_partial. fs_u_dst_sum_exists_valuenegative = fs_q_dst_sum_exists_valuenegative_body_steps_partial * S ((S (fs_i_dst_sum_exists_valuenegative_body_steps)) * fs_v_dst_sum_exists_valuenegative) + (fs_r_dst_sum_exists_valuenegative_body_steps))) /\ ((((exists fs_h_dst_sum_exists_valuenegative_body_steps_successor. fs_h_dst_sum_exists_valuenegative_body_steps_successor + S (fs_s_dst_sum_exists_valuenegative_body_steps) = S ((S (S fs_i_dst_sum_exists_valuenegative_body_steps)) * fs_v_dst_sum_exists_valuenegative)) /\ exists fs_q_dst_sum_exists_valuenegative_body_steps_successor. fs_u_dst_sum_exists_valuenegative = fs_q_dst_sum_exists_valuenegative_body_steps_successor * S ((S (S fs_i_dst_sum_exists_valuenegative_body_steps)) * fs_v_dst_sum_exists_valuenegative) + (fs_s_dst_sum_exists_valuenegative_body_steps))) /\ fs_s_dst_sum_exists_valuenegative_body_steps = fs_r_dst_sum_exists_valuenegative_body_steps + fs_a_dst_sum_exists_valuenegative_body_steps)))))) /\ (exists ge_balance_positive_sum_exists_valueresult ge_balance_negative_sum_exists_valueresult. (((((z) = 2 * (ge_balance_positive_sum_exists_valueresult) /\ (ge_balance_negative_sum_exists_valueresult) = 0) \/ exists ge_signed_half_sum_exists_valueresultdecode. (((z) = 2 * ge_signed_half_sum_exists_valueresultdecode + 1 /\ (ge_balance_positive_sum_exists_valueresult) = 0) /\ (ge_balance_negative_sum_exists_valueresult) = S ge_signed_half_sum_exists_valueresultdecode))) /\ ((dst_positive_sum_sum_exists_value) + ge_balance_negative_sum_exists_valueresult = (dst_negative_sum_sum_exists_value) + ge_balance_positive_sum_exists_valueresult)))))))))
  15. 0015specialize arithmetic_signed_sum_exists (l)
  16. 0016specialize arithmetic_signed_sum_exists (x)
  17. 0017specialize arithmetic_signed_sum_exists (l)
  18. 0018apply arithmetic_signed_sum_exists
  19. 0019cases hg_witness
  20. 0020cases hg_witness_right
  21. 0021exact hg_witness_right_left
  22. 0022cases hz
  23. 0023exists x1
  24. 0024exists x
  25. 0025split
  26. 0026exact hg_witness
  27. 0027exact hz_witness