RS000B

signed_rectangular_slice_sum_empty_exists

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

A valid source actually admits an empty slice and its zero sum, rather than merely a vacuous uniqueness assertion.

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. (exists dst_positive_code_sum_empty_input dst_positive_scale_sum_empty_input dst_negative_code_sum_empty_input dst_negative_scale_sum_empty_input. (((F) = (((((dst_positive_code_sum_empty_input) + (dst_positive_scale_sum_empty_input)) * S ((dst_positive_code_sum_empty_input) + (dst_positive_scale_sum_empty_input)) + ((dst_positive_scale_sum_empty_input) + (dst_positive_scale_sum_empty_input))) + (((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) * S ((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) + ((dst_negative_scale_sum_empty_input) + (dst_negative_scale_sum_empty_input)))) * S ((((dst_positive_code_sum_empty_input) + (dst_positive_scale_sum_empty_input)) * S ((dst_positive_code_sum_empty_input) + (dst_positive_scale_sum_empty_input)) + ((dst_positive_scale_sum_empty_input) + (dst_positive_scale_sum_empty_input))) + (((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) * S ((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) + ((dst_negative_scale_sum_empty_input) + (dst_negative_scale_sum_empty_input)))) + ((((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) * S ((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) + ((dst_negative_scale_sum_empty_input) + (dst_negative_scale_sum_empty_input))) + (((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) * S ((dst_negative_code_sum_empty_input) + (dst_negative_scale_sum_empty_input)) + ((dst_negative_scale_sum_empty_input) + (dst_negative_scale_sum_empty_input)))))) /\ (forall dst_index_sum_empty_input. (exists pvs_le_gap_sum_empty_inputdomain. pvs_le_gap_sum_empty_inputdomain + (dst_index_sum_empty_input) = (0)) -> exists dst_positive_sum_empty_input dst_negative_sum_empty_input dst_value_sum_empty_input. ((((exists ff_h_pvs_sum_empty_inputentrypositive. ff_h_pvs_sum_empty_inputentrypositive + S (dst_positive_sum_empty_input) = S ((S (dst_index_sum_empty_input)) * dst_positive_scale_sum_empty_input)) /\ exists ff_q_pvs_sum_empty_inputentrypositive. dst_positive_code_sum_empty_input = ff_q_pvs_sum_empty_inputentrypositive * S ((S (dst_index_sum_empty_input)) * dst_positive_scale_sum_empty_input) + (dst_positive_sum_empty_input))) /\ (((((exists ff_h_pvs_sum_empty_inputentrynegative. ff_h_pvs_sum_empty_inputentrynegative + S (dst_negative_sum_empty_input) = S ((S (dst_index_sum_empty_input)) * dst_negative_scale_sum_empty_input)) /\ exists ff_q_pvs_sum_empty_inputentrynegative. dst_negative_code_sum_empty_input = ff_q_pvs_sum_empty_inputentrynegative * S ((S (dst_index_sum_empty_input)) * dst_negative_scale_sum_empty_input) + (dst_negative_sum_empty_input))) /\ (exists ge_balance_positive_sum_empty_inputentryvalue ge_balance_negative_sum_empty_inputentryvalue. (((((dst_value_sum_empty_input) = 2 * (ge_balance_positive_sum_empty_inputentryvalue) /\ (ge_balance_negative_sum_empty_inputentryvalue) = 0) \/ exists ge_signed_half_sum_empty_inputentryvaluedecode. (((dst_value_sum_empty_input) = 2 * ge_signed_half_sum_empty_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_inputentryvalue) = 0) /\ (ge_balance_negative_sum_empty_inputentryvalue) = S ge_signed_half_sum_empty_inputentryvaluedecode))) /\ ((dst_positive_sum_empty_input) + ge_balance_negative_sum_empty_inputentryvalue = (dst_negative_sum_empty_input) + ge_balance_positive_sum_empty_inputentryvalue))))))))) -> (exists srs_slice_sum_empty_result. ((((exists dst_positive_code_sum_empty_resultslicesource_table dst_positive_scale_sum_empty_resultslicesource_table dst_negative_code_sum_empty_resultslicesource_table dst_negative_scale_sum_empty_resultslicesource_table. (((F) = (((((dst_positive_code_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table)) * S ((dst_positive_code_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table)) + ((dst_positive_scale_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table))) + (((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) * S ((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) + ((dst_negative_scale_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)))) * S ((((dst_positive_code_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table)) * S ((dst_positive_code_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table)) + ((dst_positive_scale_sum_empty_resultslicesource_table) + (dst_positive_scale_sum_empty_resultslicesource_table))) + (((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) * S ((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) + ((dst_negative_scale_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)))) + ((((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) * S ((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) + ((dst_negative_scale_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table))) + (((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) * S ((dst_negative_code_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)) + ((dst_negative_scale_sum_empty_resultslicesource_table) + (dst_negative_scale_sum_empty_resultslicesource_table)))))) /\ (forall dst_index_sum_empty_resultslicesource_table. (exists pvs_le_gap_sum_empty_resultslicesource_tabledomain. pvs_le_gap_sum_empty_resultslicesource_tabledomain + (dst_index_sum_empty_resultslicesource_table) = (0)) -> exists dst_positive_sum_empty_resultslicesource_table dst_negative_sum_empty_resultslicesource_table dst_value_sum_empty_resultslicesource_table. ((((exists ff_h_pvs_sum_empty_resultslicesource_tableentrypositive. ff_h_pvs_sum_empty_resultslicesource_tableentrypositive + S (dst_positive_sum_empty_resultslicesource_table) = S ((S (dst_index_sum_empty_resultslicesource_table)) * dst_positive_scale_sum_empty_resultslicesource_table)) /\ exists ff_q_pvs_sum_empty_resultslicesource_tableentrypositive. dst_positive_code_sum_empty_resultslicesource_table = ff_q_pvs_sum_empty_resultslicesource_tableentrypositive * S ((S (dst_index_sum_empty_resultslicesource_table)) * dst_positive_scale_sum_empty_resultslicesource_table) + (dst_positive_sum_empty_resultslicesource_table))) /\ (((((exists ff_h_pvs_sum_empty_resultslicesource_tableentrynegative. ff_h_pvs_sum_empty_resultslicesource_tableentrynegative + S (dst_negative_sum_empty_resultslicesource_table) = S ((S (dst_index_sum_empty_resultslicesource_table)) * dst_negative_scale_sum_empty_resultslicesource_table)) /\ exists ff_q_pvs_sum_empty_resultslicesource_tableentrynegative. dst_negative_code_sum_empty_resultslicesource_table = ff_q_pvs_sum_empty_resultslicesource_tableentrynegative * S ((S (dst_index_sum_empty_resultslicesource_table)) * dst_negative_scale_sum_empty_resultslicesource_table) + (dst_negative_sum_empty_resultslicesource_table))) /\ (exists ge_balance_positive_sum_empty_resultslicesource_tableentryvalue ge_balance_negative_sum_empty_resultslicesource_tableentryvalue. (((((dst_value_sum_empty_resultslicesource_table) = 2 * (ge_balance_positive_sum_empty_resultslicesource_tableentryvalue) /\ (ge_balance_negative_sum_empty_resultslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_resultslicesource_tableentryvaluedecode. (((dst_value_sum_empty_resultslicesource_table) = 2 * ge_signed_half_sum_empty_resultslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_resultslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_resultslicesource_tableentryvalue) = S ge_signed_half_sum_empty_resultslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_resultslicesource_table) + ge_balance_negative_sum_empty_resultslicesource_tableentryvalue = (dst_negative_sum_empty_resultslicesource_table) + ge_balance_positive_sum_empty_resultslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_empty_resultsliceoutput_table dst_positive_scale_sum_empty_resultsliceoutput_table dst_negative_code_sum_empty_resultsliceoutput_table dst_negative_scale_sum_empty_resultsliceoutput_table. (((srs_slice_sum_empty_result) = (((((dst_positive_code_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table)) * S ((dst_positive_code_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table)) + ((dst_positive_scale_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table))) + (((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) * S ((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) + ((dst_negative_scale_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)))) * S ((((dst_positive_code_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table)) * S ((dst_positive_code_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table)) + ((dst_positive_scale_sum_empty_resultsliceoutput_table) + (dst_positive_scale_sum_empty_resultsliceoutput_table))) + (((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) * S ((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) + ((dst_negative_scale_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)))) + ((((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) * S ((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) + ((dst_negative_scale_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table))) + (((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) * S ((dst_negative_code_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)) + ((dst_negative_scale_sum_empty_resultsliceoutput_table) + (dst_negative_scale_sum_empty_resultsliceoutput_table)))))) /\ (forall dst_index_sum_empty_resultsliceoutput_table. (exists pvs_le_gap_sum_empty_resultsliceoutput_tabledomain. pvs_le_gap_sum_empty_resultsliceoutput_tabledomain + (dst_index_sum_empty_resultsliceoutput_table) = (0)) -> exists dst_positive_sum_empty_resultsliceoutput_table dst_negative_sum_empty_resultsliceoutput_table dst_value_sum_empty_resultsliceoutput_table. ((((exists ff_h_pvs_sum_empty_resultsliceoutput_tableentrypositive. ff_h_pvs_sum_empty_resultsliceoutput_tableentrypositive + S (dst_positive_sum_empty_resultsliceoutput_table) = S ((S (dst_index_sum_empty_resultsliceoutput_table)) * dst_positive_scale_sum_empty_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_resultsliceoutput_tableentrypositive. dst_positive_code_sum_empty_resultsliceoutput_table = ff_q_pvs_sum_empty_resultsliceoutput_tableentrypositive * S ((S (dst_index_sum_empty_resultsliceoutput_table)) * dst_positive_scale_sum_empty_resultsliceoutput_table) + (dst_positive_sum_empty_resultsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_empty_resultsliceoutput_tableentrynegative. ff_h_pvs_sum_empty_resultsliceoutput_tableentrynegative + S (dst_negative_sum_empty_resultsliceoutput_table) = S ((S (dst_index_sum_empty_resultsliceoutput_table)) * dst_negative_scale_sum_empty_resultsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_resultsliceoutput_tableentrynegative. dst_negative_code_sum_empty_resultsliceoutput_table = ff_q_pvs_sum_empty_resultsliceoutput_tableentrynegative * S ((S (dst_index_sum_empty_resultsliceoutput_table)) * dst_negative_scale_sum_empty_resultsliceoutput_table) + (dst_negative_sum_empty_resultsliceoutput_table))) /\ (exists ge_balance_positive_sum_empty_resultsliceoutput_tableentryvalue ge_balance_negative_sum_empty_resultsliceoutput_tableentryvalue. (((((dst_value_sum_empty_resultsliceoutput_table) = 2 * (ge_balance_positive_sum_empty_resultsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_empty_resultsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_resultsliceoutput_tableentryvaluedecode. (((dst_value_sum_empty_resultsliceoutput_table) = 2 * ge_signed_half_sum_empty_resultsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_resultsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_resultsliceoutput_tableentryvalue) = S ge_signed_half_sum_empty_resultsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_resultsliceoutput_table) + ge_balance_negative_sum_empty_resultsliceoutput_tableentryvalue = (dst_negative_sum_empty_resultsliceoutput_table) + ge_balance_positive_sum_empty_resultsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_empty_resultslice. (exists pvs_gap_sum_empty_resultslicebound. pvs_gap_sum_empty_resultslicebound + S (srs_index_sum_empty_resultslice) = (0)) -> exists srs_value_sum_empty_resultslice. (((exists dst_positive_code_sum_empty_resultsliceentrysource dst_positive_scale_sum_empty_resultsliceentrysource dst_negative_code_sum_empty_resultsliceentrysource dst_negative_scale_sum_empty_resultsliceentrysource dst_positive_sum_empty_resultsliceentrysource dst_negative_sum_empty_resultsliceentrysource. (((F) = (((((dst_positive_code_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource)) * S ((dst_positive_code_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource)) + ((dst_positive_scale_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource))) + (((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) * S ((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) + ((dst_negative_scale_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)))) * S ((((dst_positive_code_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource)) * S ((dst_positive_code_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource)) + ((dst_positive_scale_sum_empty_resultsliceentrysource) + (dst_positive_scale_sum_empty_resultsliceentrysource))) + (((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) * S ((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) + ((dst_negative_scale_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)))) + ((((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) * S ((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) + ((dst_negative_scale_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource))) + (((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) * S ((dst_negative_code_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)) + ((dst_negative_scale_sum_empty_resultsliceentrysource) + (dst_negative_scale_sum_empty_resultsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_empty_resultsliceentrysourcepositive. ff_h_pvs_sum_empty_resultsliceentrysourcepositive + S (dst_positive_sum_empty_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_resultslice))))) * dst_positive_scale_sum_empty_resultsliceentrysource)) /\ exists ff_q_pvs_sum_empty_resultsliceentrysourcepositive. dst_positive_code_sum_empty_resultsliceentrysource = ff_q_pvs_sum_empty_resultsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_empty_resultslice))))) * dst_positive_scale_sum_empty_resultsliceentrysource) + (dst_positive_sum_empty_resultsliceentrysource))) /\ (((((exists ff_h_pvs_sum_empty_resultsliceentrysourcenegative. ff_h_pvs_sum_empty_resultsliceentrysourcenegative + S (dst_negative_sum_empty_resultsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_resultslice))))) * dst_negative_scale_sum_empty_resultsliceentrysource)) /\ exists ff_q_pvs_sum_empty_resultsliceentrysourcenegative. dst_negative_code_sum_empty_resultsliceentrysource = ff_q_pvs_sum_empty_resultsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_empty_resultslice))))) * dst_negative_scale_sum_empty_resultsliceentrysource) + (dst_negative_sum_empty_resultsliceentrysource))) /\ (exists ge_balance_positive_sum_empty_resultsliceentrysourcevalue ge_balance_negative_sum_empty_resultsliceentrysourcevalue. (((((srs_value_sum_empty_resultslice) = 2 * (ge_balance_positive_sum_empty_resultsliceentrysourcevalue) /\ (ge_balance_negative_sum_empty_resultsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_empty_resultsliceentrysourcevaluedecode. (((srs_value_sum_empty_resultslice) = 2 * ge_signed_half_sum_empty_resultsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_empty_resultsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_empty_resultsliceentrysourcevalue) = S ge_signed_half_sum_empty_resultsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_empty_resultsliceentrysource) + ge_balance_negative_sum_empty_resultsliceentrysourcevalue = (dst_negative_sum_empty_resultsliceentrysource) + ge_balance_positive_sum_empty_resultsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_empty_resultsliceentryoutput dst_positive_scale_sum_empty_resultsliceentryoutput dst_negative_code_sum_empty_resultsliceentryoutput dst_negative_scale_sum_empty_resultsliceentryoutput dst_positive_sum_empty_resultsliceentryoutput dst_negative_sum_empty_resultsliceentryoutput. (((srs_slice_sum_empty_result) = (((((dst_positive_code_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput)) * S ((dst_positive_code_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput)) + ((dst_positive_scale_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput))) + (((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) * S ((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) + ((dst_negative_scale_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)))) * S ((((dst_positive_code_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput)) * S ((dst_positive_code_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput)) + ((dst_positive_scale_sum_empty_resultsliceentryoutput) + (dst_positive_scale_sum_empty_resultsliceentryoutput))) + (((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) * S ((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) + ((dst_negative_scale_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)))) + ((((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) * S ((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) + ((dst_negative_scale_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput))) + (((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) * S ((dst_negative_code_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)) + ((dst_negative_scale_sum_empty_resultsliceentryoutput) + (dst_negative_scale_sum_empty_resultsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_empty_resultsliceentryoutputpositive. ff_h_pvs_sum_empty_resultsliceentryoutputpositive + S (dst_positive_sum_empty_resultsliceentryoutput) = S ((S (srs_index_sum_empty_resultslice)) * dst_positive_scale_sum_empty_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_resultsliceentryoutputpositive. dst_positive_code_sum_empty_resultsliceentryoutput = ff_q_pvs_sum_empty_resultsliceentryoutputpositive * S ((S (srs_index_sum_empty_resultslice)) * dst_positive_scale_sum_empty_resultsliceentryoutput) + (dst_positive_sum_empty_resultsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_empty_resultsliceentryoutputnegative. ff_h_pvs_sum_empty_resultsliceentryoutputnegative + S (dst_negative_sum_empty_resultsliceentryoutput) = S ((S (srs_index_sum_empty_resultslice)) * dst_negative_scale_sum_empty_resultsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_resultsliceentryoutputnegative. dst_negative_code_sum_empty_resultsliceentryoutput = ff_q_pvs_sum_empty_resultsliceentryoutputnegative * S ((S (srs_index_sum_empty_resultslice)) * dst_negative_scale_sum_empty_resultsliceentryoutput) + (dst_negative_sum_empty_resultsliceentryoutput))) /\ (exists ge_balance_positive_sum_empty_resultsliceentryoutputvalue ge_balance_negative_sum_empty_resultsliceentryoutputvalue. (((((srs_value_sum_empty_resultslice) = 2 * (ge_balance_positive_sum_empty_resultsliceentryoutputvalue) /\ (ge_balance_negative_sum_empty_resultsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_empty_resultsliceentryoutputvaluedecode. (((srs_value_sum_empty_resultslice) = 2 * ge_signed_half_sum_empty_resultsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_empty_resultsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_empty_resultsliceentryoutputvalue) = S ge_signed_half_sum_empty_resultsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_empty_resultsliceentryoutput) + ge_balance_negative_sum_empty_resultsliceentryoutputvalue = (dst_negative_sum_empty_resultsliceentryoutput) + ge_balance_positive_sum_empty_resultsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_empty_resultsum dst_positive_scale_sum_empty_resultsum dst_negative_code_sum_empty_resultsum dst_negative_scale_sum_empty_resultsum dst_positive_sum_sum_empty_resultsum dst_negative_sum_sum_empty_resultsum. (((srs_slice_sum_empty_result) = (((((dst_positive_code_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum)) * S ((dst_positive_code_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum)) + ((dst_positive_scale_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum))) + (((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) * S ((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) + ((dst_negative_scale_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)))) * S ((((dst_positive_code_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum)) * S ((dst_positive_code_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum)) + ((dst_positive_scale_sum_empty_resultsum) + (dst_positive_scale_sum_empty_resultsum))) + (((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) * S ((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) + ((dst_negative_scale_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)))) + ((((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) * S ((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) + ((dst_negative_scale_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum))) + (((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) * S ((dst_negative_code_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)) + ((dst_negative_scale_sum_empty_resultsum) + (dst_negative_scale_sum_empty_resultsum)))))) /\ (((exists fs_u_dst_sum_empty_resultsumpositive fs_v_dst_sum_empty_resultsumpositive. ((((exists fs_h_dst_sum_empty_resultsumpositive_body_start. fs_h_dst_sum_empty_resultsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_resultsumpositive)) /\ exists fs_q_dst_sum_empty_resultsumpositive_body_start. fs_u_dst_sum_empty_resultsumpositive = fs_q_dst_sum_empty_resultsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_empty_resultsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_empty_resultsumpositive_body_terminal. fs_h_dst_sum_empty_resultsumpositive_body_terminal + S (dst_positive_sum_sum_empty_resultsum) = S ((S (0)) * fs_v_dst_sum_empty_resultsumpositive)) /\ exists fs_q_dst_sum_empty_resultsumpositive_body_terminal. fs_u_dst_sum_empty_resultsumpositive = fs_q_dst_sum_empty_resultsumpositive_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_resultsumpositive) + (dst_positive_sum_sum_empty_resultsum))) /\ forall fs_i_dst_sum_empty_resultsumpositive_body_steps. (exists fs_lt_dst_sum_empty_resultsumpositive_body_steps_bound. fs_lt_dst_sum_empty_resultsumpositive_body_steps_bound + S fs_i_dst_sum_empty_resultsumpositive_body_steps = 0) -> exists fs_a_dst_sum_empty_resultsumpositive_body_steps fs_r_dst_sum_empty_resultsumpositive_body_steps fs_s_dst_sum_empty_resultsumpositive_body_steps. ((((exists fs_h_dst_sum_empty_resultsumpositive_body_steps_summand. fs_h_dst_sum_empty_resultsumpositive_body_steps_summand + S (fs_a_dst_sum_empty_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_resultsumpositive_body_steps)) * dst_positive_scale_sum_empty_resultsum)) /\ exists fs_q_dst_sum_empty_resultsumpositive_body_steps_summand. dst_positive_code_sum_empty_resultsum = fs_q_dst_sum_empty_resultsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_empty_resultsumpositive_body_steps)) * dst_positive_scale_sum_empty_resultsum) + (fs_a_dst_sum_empty_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_resultsumpositive_body_steps_partial. fs_h_dst_sum_empty_resultsumpositive_body_steps_partial + S (fs_r_dst_sum_empty_resultsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_resultsumpositive_body_steps)) * fs_v_dst_sum_empty_resultsumpositive)) /\ exists fs_q_dst_sum_empty_resultsumpositive_body_steps_partial. fs_u_dst_sum_empty_resultsumpositive = fs_q_dst_sum_empty_resultsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_empty_resultsumpositive_body_steps)) * fs_v_dst_sum_empty_resultsumpositive) + (fs_r_dst_sum_empty_resultsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_resultsumpositive_body_steps_successor. fs_h_dst_sum_empty_resultsumpositive_body_steps_successor + S (fs_s_dst_sum_empty_resultsumpositive_body_steps) = S ((S (S fs_i_dst_sum_empty_resultsumpositive_body_steps)) * fs_v_dst_sum_empty_resultsumpositive)) /\ exists fs_q_dst_sum_empty_resultsumpositive_body_steps_successor. fs_u_dst_sum_empty_resultsumpositive = fs_q_dst_sum_empty_resultsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_empty_resultsumpositive_body_steps)) * fs_v_dst_sum_empty_resultsumpositive) + (fs_s_dst_sum_empty_resultsumpositive_body_steps))) /\ fs_s_dst_sum_empty_resultsumpositive_body_steps = fs_r_dst_sum_empty_resultsumpositive_body_steps + fs_a_dst_sum_empty_resultsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_empty_resultsumnegative fs_v_dst_sum_empty_resultsumnegative. ((((exists fs_h_dst_sum_empty_resultsumnegative_body_start. fs_h_dst_sum_empty_resultsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_resultsumnegative)) /\ exists fs_q_dst_sum_empty_resultsumnegative_body_start. fs_u_dst_sum_empty_resultsumnegative = fs_q_dst_sum_empty_resultsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_empty_resultsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_empty_resultsumnegative_body_terminal. fs_h_dst_sum_empty_resultsumnegative_body_terminal + S (dst_negative_sum_sum_empty_resultsum) = S ((S (0)) * fs_v_dst_sum_empty_resultsumnegative)) /\ exists fs_q_dst_sum_empty_resultsumnegative_body_terminal. fs_u_dst_sum_empty_resultsumnegative = fs_q_dst_sum_empty_resultsumnegative_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_resultsumnegative) + (dst_negative_sum_sum_empty_resultsum))) /\ forall fs_i_dst_sum_empty_resultsumnegative_body_steps. (exists fs_lt_dst_sum_empty_resultsumnegative_body_steps_bound. fs_lt_dst_sum_empty_resultsumnegative_body_steps_bound + S fs_i_dst_sum_empty_resultsumnegative_body_steps = 0) -> exists fs_a_dst_sum_empty_resultsumnegative_body_steps fs_r_dst_sum_empty_resultsumnegative_body_steps fs_s_dst_sum_empty_resultsumnegative_body_steps. ((((exists fs_h_dst_sum_empty_resultsumnegative_body_steps_summand. fs_h_dst_sum_empty_resultsumnegative_body_steps_summand + S (fs_a_dst_sum_empty_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_resultsumnegative_body_steps)) * dst_negative_scale_sum_empty_resultsum)) /\ exists fs_q_dst_sum_empty_resultsumnegative_body_steps_summand. dst_negative_code_sum_empty_resultsum = fs_q_dst_sum_empty_resultsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_empty_resultsumnegative_body_steps)) * dst_negative_scale_sum_empty_resultsum) + (fs_a_dst_sum_empty_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_resultsumnegative_body_steps_partial. fs_h_dst_sum_empty_resultsumnegative_body_steps_partial + S (fs_r_dst_sum_empty_resultsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_resultsumnegative_body_steps)) * fs_v_dst_sum_empty_resultsumnegative)) /\ exists fs_q_dst_sum_empty_resultsumnegative_body_steps_partial. fs_u_dst_sum_empty_resultsumnegative = fs_q_dst_sum_empty_resultsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_empty_resultsumnegative_body_steps)) * fs_v_dst_sum_empty_resultsumnegative) + (fs_r_dst_sum_empty_resultsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_resultsumnegative_body_steps_successor. fs_h_dst_sum_empty_resultsumnegative_body_steps_successor + S (fs_s_dst_sum_empty_resultsumnegative_body_steps) = S ((S (S fs_i_dst_sum_empty_resultsumnegative_body_steps)) * fs_v_dst_sum_empty_resultsumnegative)) /\ exists fs_q_dst_sum_empty_resultsumnegative_body_steps_successor. fs_u_dst_sum_empty_resultsumnegative = fs_q_dst_sum_empty_resultsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_empty_resultsumnegative_body_steps)) * fs_v_dst_sum_empty_resultsumnegative) + (fs_s_dst_sum_empty_resultsumnegative_body_steps))) /\ fs_s_dst_sum_empty_resultsumnegative_body_steps = fs_r_dst_sum_empty_resultsumnegative_body_steps + fs_a_dst_sum_empty_resultsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_empty_resultsumresult ge_balance_negative_sum_empty_resultsumresult. (((((0) = 2 * (ge_balance_positive_sum_empty_resultsumresult) /\ (ge_balance_negative_sum_empty_resultsumresult) = 0) \/ exists ge_signed_half_sum_empty_resultsumresultdecode. (((0) = 2 * ge_signed_half_sum_empty_resultsumresultdecode + 1 /\ (ge_balance_positive_sum_empty_resultsumresult) = 0) /\ (ge_balance_negative_sum_empty_resultsumresult) = S ge_signed_half_sum_empty_resultsumresultdecode))) /\ ((dst_positive_sum_sum_empty_resultsum) + ge_balance_negative_sum_empty_resultsumresult = (dst_negative_sum_sum_empty_resultsum) + ge_balance_positive_sum_empty_resultsumresult)))))))))))

Constructive proof overview

Generated structural guide

A valid source actually admits an empty slice and its zero sum, rather than merely a vacuous uniqueness assertion.

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

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

Proof neighborhood

Direct dependencies

RS0008 signed_rectangular_slice_sum_exists RS000A signed_rectangular_slice_sum_empty_value

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

22 script commands · 4 reading checkpoints · 2 local claims

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

Named ingredients (2)
signed rectangular slice sum existssigned rectangular slice sum empty value

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

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 hF
02Establish hzL5–11

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

  1. L5
    have hz : ∃ z. SignedSliceSum(F,o,s,0,z)Definitions: SignedSliceSum
  2. L6
    specialize signed_rectangular_slice_sum_exists (F)
  3. L7
    specialize signed_rectangular_slice_sum_exists (o)
  4. L8
    specialize signed_rectangular_slice_sum_exists (s)
  5. L9
    specialize signed_rectangular_slice_sum_exists (0)
  6. L10
    apply signed_rectangular_slice_sum_exists
  7. L11
    exact hF
03Separate the logical casesL12–12

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

  1. L12
    cases hz
04Establish heqL13–22

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

  1. L13
    have heq : x = 0
  2. L14
    specialize signed_rectangular_slice_sum_empty_value (F)
  3. L15
    specialize signed_rectangular_slice_sum_empty_value (o)
  4. L16
    specialize signed_rectangular_slice_sum_empty_value (s)
  5. L17
    specialize signed_rectangular_slice_sum_empty_value (x)
  6. L18
    apply signed_rectangular_slice_sum_empty_value
  7. L19
    exact hz_witness
  8. L20
    rewrite heq at hz_witness
  9. L21
    rewrite heq at hz_witness
  10. L22
    exact hz_witness

Library-wide reading audit

Original exact command ledger · 22 lines
  1. 0001intro F
  2. 0002intro o
  3. 0003intro s
  4. 0004intro hF
  5. 0005have hz : exists z. (exists srs_slice_sum_empty_construct. ((((exists dst_positive_code_sum_empty_constructslicesource_table dst_positive_scale_sum_empty_constructslicesource_table dst_negative_code_sum_empty_constructslicesource_table dst_negative_scale_sum_empty_constructslicesource_table. (((F) = (((((dst_positive_code_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table)) * S ((dst_positive_code_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table)) + ((dst_positive_scale_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table))) + (((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) * S ((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) + ((dst_negative_scale_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)))) * S ((((dst_positive_code_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table)) * S ((dst_positive_code_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table)) + ((dst_positive_scale_sum_empty_constructslicesource_table) + (dst_positive_scale_sum_empty_constructslicesource_table))) + (((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) * S ((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) + ((dst_negative_scale_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)))) + ((((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) * S ((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) + ((dst_negative_scale_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table))) + (((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) * S ((dst_negative_code_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)) + ((dst_negative_scale_sum_empty_constructslicesource_table) + (dst_negative_scale_sum_empty_constructslicesource_table)))))) /\ (forall dst_index_sum_empty_constructslicesource_table. (exists pvs_le_gap_sum_empty_constructslicesource_tabledomain. pvs_le_gap_sum_empty_constructslicesource_tabledomain + (dst_index_sum_empty_constructslicesource_table) = (0)) -> exists dst_positive_sum_empty_constructslicesource_table dst_negative_sum_empty_constructslicesource_table dst_value_sum_empty_constructslicesource_table. ((((exists ff_h_pvs_sum_empty_constructslicesource_tableentrypositive. ff_h_pvs_sum_empty_constructslicesource_tableentrypositive + S (dst_positive_sum_empty_constructslicesource_table) = S ((S (dst_index_sum_empty_constructslicesource_table)) * dst_positive_scale_sum_empty_constructslicesource_table)) /\ exists ff_q_pvs_sum_empty_constructslicesource_tableentrypositive. dst_positive_code_sum_empty_constructslicesource_table = ff_q_pvs_sum_empty_constructslicesource_tableentrypositive * S ((S (dst_index_sum_empty_constructslicesource_table)) * dst_positive_scale_sum_empty_constructslicesource_table) + (dst_positive_sum_empty_constructslicesource_table))) /\ (((((exists ff_h_pvs_sum_empty_constructslicesource_tableentrynegative. ff_h_pvs_sum_empty_constructslicesource_tableentrynegative + S (dst_negative_sum_empty_constructslicesource_table) = S ((S (dst_index_sum_empty_constructslicesource_table)) * dst_negative_scale_sum_empty_constructslicesource_table)) /\ exists ff_q_pvs_sum_empty_constructslicesource_tableentrynegative. dst_negative_code_sum_empty_constructslicesource_table = ff_q_pvs_sum_empty_constructslicesource_tableentrynegative * S ((S (dst_index_sum_empty_constructslicesource_table)) * dst_negative_scale_sum_empty_constructslicesource_table) + (dst_negative_sum_empty_constructslicesource_table))) /\ (exists ge_balance_positive_sum_empty_constructslicesource_tableentryvalue ge_balance_negative_sum_empty_constructslicesource_tableentryvalue. (((((dst_value_sum_empty_constructslicesource_table) = 2 * (ge_balance_positive_sum_empty_constructslicesource_tableentryvalue) /\ (ge_balance_negative_sum_empty_constructslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_constructslicesource_tableentryvaluedecode. (((dst_value_sum_empty_constructslicesource_table) = 2 * ge_signed_half_sum_empty_constructslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_constructslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_constructslicesource_tableentryvalue) = S ge_signed_half_sum_empty_constructslicesource_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_constructslicesource_table) + ge_balance_negative_sum_empty_constructslicesource_tableentryvalue = (dst_negative_sum_empty_constructslicesource_table) + ge_balance_positive_sum_empty_constructslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_sum_empty_constructsliceoutput_table dst_positive_scale_sum_empty_constructsliceoutput_table dst_negative_code_sum_empty_constructsliceoutput_table dst_negative_scale_sum_empty_constructsliceoutput_table. (((srs_slice_sum_empty_construct) = (((((dst_positive_code_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table)) * S ((dst_positive_code_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table)) + ((dst_positive_scale_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table))) + (((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) * S ((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) + ((dst_negative_scale_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)))) * S ((((dst_positive_code_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table)) * S ((dst_positive_code_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table)) + ((dst_positive_scale_sum_empty_constructsliceoutput_table) + (dst_positive_scale_sum_empty_constructsliceoutput_table))) + (((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) * S ((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) + ((dst_negative_scale_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)))) + ((((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) * S ((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) + ((dst_negative_scale_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table))) + (((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) * S ((dst_negative_code_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)) + ((dst_negative_scale_sum_empty_constructsliceoutput_table) + (dst_negative_scale_sum_empty_constructsliceoutput_table)))))) /\ (forall dst_index_sum_empty_constructsliceoutput_table. (exists pvs_le_gap_sum_empty_constructsliceoutput_tabledomain. pvs_le_gap_sum_empty_constructsliceoutput_tabledomain + (dst_index_sum_empty_constructsliceoutput_table) = (0)) -> exists dst_positive_sum_empty_constructsliceoutput_table dst_negative_sum_empty_constructsliceoutput_table dst_value_sum_empty_constructsliceoutput_table. ((((exists ff_h_pvs_sum_empty_constructsliceoutput_tableentrypositive. ff_h_pvs_sum_empty_constructsliceoutput_tableentrypositive + S (dst_positive_sum_empty_constructsliceoutput_table) = S ((S (dst_index_sum_empty_constructsliceoutput_table)) * dst_positive_scale_sum_empty_constructsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_constructsliceoutput_tableentrypositive. dst_positive_code_sum_empty_constructsliceoutput_table = ff_q_pvs_sum_empty_constructsliceoutput_tableentrypositive * S ((S (dst_index_sum_empty_constructsliceoutput_table)) * dst_positive_scale_sum_empty_constructsliceoutput_table) + (dst_positive_sum_empty_constructsliceoutput_table))) /\ (((((exists ff_h_pvs_sum_empty_constructsliceoutput_tableentrynegative. ff_h_pvs_sum_empty_constructsliceoutput_tableentrynegative + S (dst_negative_sum_empty_constructsliceoutput_table) = S ((S (dst_index_sum_empty_constructsliceoutput_table)) * dst_negative_scale_sum_empty_constructsliceoutput_table)) /\ exists ff_q_pvs_sum_empty_constructsliceoutput_tableentrynegative. dst_negative_code_sum_empty_constructsliceoutput_table = ff_q_pvs_sum_empty_constructsliceoutput_tableentrynegative * S ((S (dst_index_sum_empty_constructsliceoutput_table)) * dst_negative_scale_sum_empty_constructsliceoutput_table) + (dst_negative_sum_empty_constructsliceoutput_table))) /\ (exists ge_balance_positive_sum_empty_constructsliceoutput_tableentryvalue ge_balance_negative_sum_empty_constructsliceoutput_tableentryvalue. (((((dst_value_sum_empty_constructsliceoutput_table) = 2 * (ge_balance_positive_sum_empty_constructsliceoutput_tableentryvalue) /\ (ge_balance_negative_sum_empty_constructsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_sum_empty_constructsliceoutput_tableentryvaluedecode. (((dst_value_sum_empty_constructsliceoutput_table) = 2 * ge_signed_half_sum_empty_constructsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_sum_empty_constructsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_sum_empty_constructsliceoutput_tableentryvalue) = S ge_signed_half_sum_empty_constructsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_sum_empty_constructsliceoutput_table) + ge_balance_negative_sum_empty_constructsliceoutput_tableentryvalue = (dst_negative_sum_empty_constructsliceoutput_table) + ge_balance_positive_sum_empty_constructsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_sum_empty_constructslice. (exists pvs_gap_sum_empty_constructslicebound. pvs_gap_sum_empty_constructslicebound + S (srs_index_sum_empty_constructslice) = (0)) -> exists srs_value_sum_empty_constructslice. (((exists dst_positive_code_sum_empty_constructsliceentrysource dst_positive_scale_sum_empty_constructsliceentrysource dst_negative_code_sum_empty_constructsliceentrysource dst_negative_scale_sum_empty_constructsliceentrysource dst_positive_sum_empty_constructsliceentrysource dst_negative_sum_empty_constructsliceentrysource. (((F) = (((((dst_positive_code_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource)) * S ((dst_positive_code_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource)) + ((dst_positive_scale_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource))) + (((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) * S ((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) + ((dst_negative_scale_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)))) * S ((((dst_positive_code_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource)) * S ((dst_positive_code_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource)) + ((dst_positive_scale_sum_empty_constructsliceentrysource) + (dst_positive_scale_sum_empty_constructsliceentrysource))) + (((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) * S ((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) + ((dst_negative_scale_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)))) + ((((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) * S ((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) + ((dst_negative_scale_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource))) + (((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) * S ((dst_negative_code_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)) + ((dst_negative_scale_sum_empty_constructsliceentrysource) + (dst_negative_scale_sum_empty_constructsliceentrysource)))))) /\ (((((exists ff_h_pvs_sum_empty_constructsliceentrysourcepositive. ff_h_pvs_sum_empty_constructsliceentrysourcepositive + S (dst_positive_sum_empty_constructsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_constructslice))))) * dst_positive_scale_sum_empty_constructsliceentrysource)) /\ exists ff_q_pvs_sum_empty_constructsliceentrysourcepositive. dst_positive_code_sum_empty_constructsliceentrysource = ff_q_pvs_sum_empty_constructsliceentrysourcepositive * S ((S (((o) + ((s) * (srs_index_sum_empty_constructslice))))) * dst_positive_scale_sum_empty_constructsliceentrysource) + (dst_positive_sum_empty_constructsliceentrysource))) /\ (((((exists ff_h_pvs_sum_empty_constructsliceentrysourcenegative. ff_h_pvs_sum_empty_constructsliceentrysourcenegative + S (dst_negative_sum_empty_constructsliceentrysource) = S ((S (((o) + ((s) * (srs_index_sum_empty_constructslice))))) * dst_negative_scale_sum_empty_constructsliceentrysource)) /\ exists ff_q_pvs_sum_empty_constructsliceentrysourcenegative. dst_negative_code_sum_empty_constructsliceentrysource = ff_q_pvs_sum_empty_constructsliceentrysourcenegative * S ((S (((o) + ((s) * (srs_index_sum_empty_constructslice))))) * dst_negative_scale_sum_empty_constructsliceentrysource) + (dst_negative_sum_empty_constructsliceentrysource))) /\ (exists ge_balance_positive_sum_empty_constructsliceentrysourcevalue ge_balance_negative_sum_empty_constructsliceentrysourcevalue. (((((srs_value_sum_empty_constructslice) = 2 * (ge_balance_positive_sum_empty_constructsliceentrysourcevalue) /\ (ge_balance_negative_sum_empty_constructsliceentrysourcevalue) = 0) \/ exists ge_signed_half_sum_empty_constructsliceentrysourcevaluedecode. (((srs_value_sum_empty_constructslice) = 2 * ge_signed_half_sum_empty_constructsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_sum_empty_constructsliceentrysourcevalue) = 0) /\ (ge_balance_negative_sum_empty_constructsliceentrysourcevalue) = S ge_signed_half_sum_empty_constructsliceentrysourcevaluedecode))) /\ ((dst_positive_sum_empty_constructsliceentrysource) + ge_balance_negative_sum_empty_constructsliceentrysourcevalue = (dst_negative_sum_empty_constructsliceentrysource) + ge_balance_positive_sum_empty_constructsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_sum_empty_constructsliceentryoutput dst_positive_scale_sum_empty_constructsliceentryoutput dst_negative_code_sum_empty_constructsliceentryoutput dst_negative_scale_sum_empty_constructsliceentryoutput dst_positive_sum_empty_constructsliceentryoutput dst_negative_sum_empty_constructsliceentryoutput. (((srs_slice_sum_empty_construct) = (((((dst_positive_code_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput)) * S ((dst_positive_code_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput)) + ((dst_positive_scale_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput))) + (((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) * S ((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) + ((dst_negative_scale_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)))) * S ((((dst_positive_code_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput)) * S ((dst_positive_code_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput)) + ((dst_positive_scale_sum_empty_constructsliceentryoutput) + (dst_positive_scale_sum_empty_constructsliceentryoutput))) + (((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) * S ((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) + ((dst_negative_scale_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)))) + ((((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) * S ((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) + ((dst_negative_scale_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput))) + (((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) * S ((dst_negative_code_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)) + ((dst_negative_scale_sum_empty_constructsliceentryoutput) + (dst_negative_scale_sum_empty_constructsliceentryoutput)))))) /\ (((((exists ff_h_pvs_sum_empty_constructsliceentryoutputpositive. ff_h_pvs_sum_empty_constructsliceentryoutputpositive + S (dst_positive_sum_empty_constructsliceentryoutput) = S ((S (srs_index_sum_empty_constructslice)) * dst_positive_scale_sum_empty_constructsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_constructsliceentryoutputpositive. dst_positive_code_sum_empty_constructsliceentryoutput = ff_q_pvs_sum_empty_constructsliceentryoutputpositive * S ((S (srs_index_sum_empty_constructslice)) * dst_positive_scale_sum_empty_constructsliceentryoutput) + (dst_positive_sum_empty_constructsliceentryoutput))) /\ (((((exists ff_h_pvs_sum_empty_constructsliceentryoutputnegative. ff_h_pvs_sum_empty_constructsliceentryoutputnegative + S (dst_negative_sum_empty_constructsliceentryoutput) = S ((S (srs_index_sum_empty_constructslice)) * dst_negative_scale_sum_empty_constructsliceentryoutput)) /\ exists ff_q_pvs_sum_empty_constructsliceentryoutputnegative. dst_negative_code_sum_empty_constructsliceentryoutput = ff_q_pvs_sum_empty_constructsliceentryoutputnegative * S ((S (srs_index_sum_empty_constructslice)) * dst_negative_scale_sum_empty_constructsliceentryoutput) + (dst_negative_sum_empty_constructsliceentryoutput))) /\ (exists ge_balance_positive_sum_empty_constructsliceentryoutputvalue ge_balance_negative_sum_empty_constructsliceentryoutputvalue. (((((srs_value_sum_empty_constructslice) = 2 * (ge_balance_positive_sum_empty_constructsliceentryoutputvalue) /\ (ge_balance_negative_sum_empty_constructsliceentryoutputvalue) = 0) \/ exists ge_signed_half_sum_empty_constructsliceentryoutputvaluedecode. (((srs_value_sum_empty_constructslice) = 2 * ge_signed_half_sum_empty_constructsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_sum_empty_constructsliceentryoutputvalue) = 0) /\ (ge_balance_negative_sum_empty_constructsliceentryoutputvalue) = S ge_signed_half_sum_empty_constructsliceentryoutputvaluedecode))) /\ ((dst_positive_sum_empty_constructsliceentryoutput) + ge_balance_negative_sum_empty_constructsliceentryoutputvalue = (dst_negative_sum_empty_constructsliceentryoutput) + ge_balance_positive_sum_empty_constructsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_sum_empty_constructsum dst_positive_scale_sum_empty_constructsum dst_negative_code_sum_empty_constructsum dst_negative_scale_sum_empty_constructsum dst_positive_sum_sum_empty_constructsum dst_negative_sum_sum_empty_constructsum. (((srs_slice_sum_empty_construct) = (((((dst_positive_code_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum)) * S ((dst_positive_code_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum)) + ((dst_positive_scale_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum))) + (((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) * S ((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) + ((dst_negative_scale_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)))) * S ((((dst_positive_code_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum)) * S ((dst_positive_code_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum)) + ((dst_positive_scale_sum_empty_constructsum) + (dst_positive_scale_sum_empty_constructsum))) + (((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) * S ((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) + ((dst_negative_scale_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)))) + ((((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) * S ((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) + ((dst_negative_scale_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum))) + (((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) * S ((dst_negative_code_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)) + ((dst_negative_scale_sum_empty_constructsum) + (dst_negative_scale_sum_empty_constructsum)))))) /\ (((exists fs_u_dst_sum_empty_constructsumpositive fs_v_dst_sum_empty_constructsumpositive. ((((exists fs_h_dst_sum_empty_constructsumpositive_body_start. fs_h_dst_sum_empty_constructsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_constructsumpositive)) /\ exists fs_q_dst_sum_empty_constructsumpositive_body_start. fs_u_dst_sum_empty_constructsumpositive = fs_q_dst_sum_empty_constructsumpositive_body_start * S ((S (0)) * fs_v_dst_sum_empty_constructsumpositive) + (0))) /\ ((((exists fs_h_dst_sum_empty_constructsumpositive_body_terminal. fs_h_dst_sum_empty_constructsumpositive_body_terminal + S (dst_positive_sum_sum_empty_constructsum) = S ((S (0)) * fs_v_dst_sum_empty_constructsumpositive)) /\ exists fs_q_dst_sum_empty_constructsumpositive_body_terminal. fs_u_dst_sum_empty_constructsumpositive = fs_q_dst_sum_empty_constructsumpositive_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_constructsumpositive) + (dst_positive_sum_sum_empty_constructsum))) /\ forall fs_i_dst_sum_empty_constructsumpositive_body_steps. (exists fs_lt_dst_sum_empty_constructsumpositive_body_steps_bound. fs_lt_dst_sum_empty_constructsumpositive_body_steps_bound + S fs_i_dst_sum_empty_constructsumpositive_body_steps = 0) -> exists fs_a_dst_sum_empty_constructsumpositive_body_steps fs_r_dst_sum_empty_constructsumpositive_body_steps fs_s_dst_sum_empty_constructsumpositive_body_steps. ((((exists fs_h_dst_sum_empty_constructsumpositive_body_steps_summand. fs_h_dst_sum_empty_constructsumpositive_body_steps_summand + S (fs_a_dst_sum_empty_constructsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_constructsumpositive_body_steps)) * dst_positive_scale_sum_empty_constructsum)) /\ exists fs_q_dst_sum_empty_constructsumpositive_body_steps_summand. dst_positive_code_sum_empty_constructsum = fs_q_dst_sum_empty_constructsumpositive_body_steps_summand * S ((S (fs_i_dst_sum_empty_constructsumpositive_body_steps)) * dst_positive_scale_sum_empty_constructsum) + (fs_a_dst_sum_empty_constructsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_constructsumpositive_body_steps_partial. fs_h_dst_sum_empty_constructsumpositive_body_steps_partial + S (fs_r_dst_sum_empty_constructsumpositive_body_steps) = S ((S (fs_i_dst_sum_empty_constructsumpositive_body_steps)) * fs_v_dst_sum_empty_constructsumpositive)) /\ exists fs_q_dst_sum_empty_constructsumpositive_body_steps_partial. fs_u_dst_sum_empty_constructsumpositive = fs_q_dst_sum_empty_constructsumpositive_body_steps_partial * S ((S (fs_i_dst_sum_empty_constructsumpositive_body_steps)) * fs_v_dst_sum_empty_constructsumpositive) + (fs_r_dst_sum_empty_constructsumpositive_body_steps))) /\ ((((exists fs_h_dst_sum_empty_constructsumpositive_body_steps_successor. fs_h_dst_sum_empty_constructsumpositive_body_steps_successor + S (fs_s_dst_sum_empty_constructsumpositive_body_steps) = S ((S (S fs_i_dst_sum_empty_constructsumpositive_body_steps)) * fs_v_dst_sum_empty_constructsumpositive)) /\ exists fs_q_dst_sum_empty_constructsumpositive_body_steps_successor. fs_u_dst_sum_empty_constructsumpositive = fs_q_dst_sum_empty_constructsumpositive_body_steps_successor * S ((S (S fs_i_dst_sum_empty_constructsumpositive_body_steps)) * fs_v_dst_sum_empty_constructsumpositive) + (fs_s_dst_sum_empty_constructsumpositive_body_steps))) /\ fs_s_dst_sum_empty_constructsumpositive_body_steps = fs_r_dst_sum_empty_constructsumpositive_body_steps + fs_a_dst_sum_empty_constructsumpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_empty_constructsumnegative fs_v_dst_sum_empty_constructsumnegative. ((((exists fs_h_dst_sum_empty_constructsumnegative_body_start. fs_h_dst_sum_empty_constructsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_empty_constructsumnegative)) /\ exists fs_q_dst_sum_empty_constructsumnegative_body_start. fs_u_dst_sum_empty_constructsumnegative = fs_q_dst_sum_empty_constructsumnegative_body_start * S ((S (0)) * fs_v_dst_sum_empty_constructsumnegative) + (0))) /\ ((((exists fs_h_dst_sum_empty_constructsumnegative_body_terminal. fs_h_dst_sum_empty_constructsumnegative_body_terminal + S (dst_negative_sum_sum_empty_constructsum) = S ((S (0)) * fs_v_dst_sum_empty_constructsumnegative)) /\ exists fs_q_dst_sum_empty_constructsumnegative_body_terminal. fs_u_dst_sum_empty_constructsumnegative = fs_q_dst_sum_empty_constructsumnegative_body_terminal * S ((S (0)) * fs_v_dst_sum_empty_constructsumnegative) + (dst_negative_sum_sum_empty_constructsum))) /\ forall fs_i_dst_sum_empty_constructsumnegative_body_steps. (exists fs_lt_dst_sum_empty_constructsumnegative_body_steps_bound. fs_lt_dst_sum_empty_constructsumnegative_body_steps_bound + S fs_i_dst_sum_empty_constructsumnegative_body_steps = 0) -> exists fs_a_dst_sum_empty_constructsumnegative_body_steps fs_r_dst_sum_empty_constructsumnegative_body_steps fs_s_dst_sum_empty_constructsumnegative_body_steps. ((((exists fs_h_dst_sum_empty_constructsumnegative_body_steps_summand. fs_h_dst_sum_empty_constructsumnegative_body_steps_summand + S (fs_a_dst_sum_empty_constructsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_constructsumnegative_body_steps)) * dst_negative_scale_sum_empty_constructsum)) /\ exists fs_q_dst_sum_empty_constructsumnegative_body_steps_summand. dst_negative_code_sum_empty_constructsum = fs_q_dst_sum_empty_constructsumnegative_body_steps_summand * S ((S (fs_i_dst_sum_empty_constructsumnegative_body_steps)) * dst_negative_scale_sum_empty_constructsum) + (fs_a_dst_sum_empty_constructsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_constructsumnegative_body_steps_partial. fs_h_dst_sum_empty_constructsumnegative_body_steps_partial + S (fs_r_dst_sum_empty_constructsumnegative_body_steps) = S ((S (fs_i_dst_sum_empty_constructsumnegative_body_steps)) * fs_v_dst_sum_empty_constructsumnegative)) /\ exists fs_q_dst_sum_empty_constructsumnegative_body_steps_partial. fs_u_dst_sum_empty_constructsumnegative = fs_q_dst_sum_empty_constructsumnegative_body_steps_partial * S ((S (fs_i_dst_sum_empty_constructsumnegative_body_steps)) * fs_v_dst_sum_empty_constructsumnegative) + (fs_r_dst_sum_empty_constructsumnegative_body_steps))) /\ ((((exists fs_h_dst_sum_empty_constructsumnegative_body_steps_successor. fs_h_dst_sum_empty_constructsumnegative_body_steps_successor + S (fs_s_dst_sum_empty_constructsumnegative_body_steps) = S ((S (S fs_i_dst_sum_empty_constructsumnegative_body_steps)) * fs_v_dst_sum_empty_constructsumnegative)) /\ exists fs_q_dst_sum_empty_constructsumnegative_body_steps_successor. fs_u_dst_sum_empty_constructsumnegative = fs_q_dst_sum_empty_constructsumnegative_body_steps_successor * S ((S (S fs_i_dst_sum_empty_constructsumnegative_body_steps)) * fs_v_dst_sum_empty_constructsumnegative) + (fs_s_dst_sum_empty_constructsumnegative_body_steps))) /\ fs_s_dst_sum_empty_constructsumnegative_body_steps = fs_r_dst_sum_empty_constructsumnegative_body_steps + fs_a_dst_sum_empty_constructsumnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_empty_constructsumresult ge_balance_negative_sum_empty_constructsumresult. (((((z) = 2 * (ge_balance_positive_sum_empty_constructsumresult) /\ (ge_balance_negative_sum_empty_constructsumresult) = 0) \/ exists ge_signed_half_sum_empty_constructsumresultdecode. (((z) = 2 * ge_signed_half_sum_empty_constructsumresultdecode + 1 /\ (ge_balance_positive_sum_empty_constructsumresult) = 0) /\ (ge_balance_negative_sum_empty_constructsumresult) = S ge_signed_half_sum_empty_constructsumresultdecode))) /\ ((dst_positive_sum_sum_empty_constructsum) + ge_balance_negative_sum_empty_constructsumresult = (dst_negative_sum_sum_empty_constructsum) + ge_balance_positive_sum_empty_constructsumresult)))))))))))
  6. 0006specialize signed_rectangular_slice_sum_exists (F)
  7. 0007specialize signed_rectangular_slice_sum_exists (o)
  8. 0008specialize signed_rectangular_slice_sum_exists (s)
  9. 0009specialize signed_rectangular_slice_sum_exists (0)
  10. 0010apply signed_rectangular_slice_sum_exists
  11. 0011exact hF
  12. 0012cases hz
  13. 0013have heq : x = 0
  14. 0014specialize signed_rectangular_slice_sum_empty_value (F)
  15. 0015specialize signed_rectangular_slice_sum_empty_value (o)
  16. 0016specialize signed_rectangular_slice_sum_empty_value (s)
  17. 0017specialize signed_rectangular_slice_sum_empty_value (x)
  18. 0018apply signed_rectangular_slice_sum_empty_value
  19. 0019exact hz_witness
  20. 0020rewrite heq at hz_witness
  21. 0021rewrite heq at hz_witness
  22. 0022exact hz_witness