Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
ArithTable(0,F) ∧ (ArithTable(m,R) ∧ (∀ x. Lt(x,m) → ∃ y. ArithAt(R,x,y) ∧ SignedSliceSum(F,o + s · x,t,n,y)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists dst_positive_code_lowercontinuationsource_table dst_positive_scale_lowercontinuationsource_table dst_negative_code_lowercontinuationsource_table dst_negative_scale_lowercontinuationsource_table. ((((F)) = (((((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) * S ((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) + ((dst_positive_scale_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))) * S ((((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) * S ((dst_positive_code_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table)) + ((dst_positive_scale_lowercontinuationsource_table) + (dst_positive_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))) + ((((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table))) + (((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) * S ((dst_negative_code_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)) + ((dst_negative_scale_lowercontinuationsource_table) + (dst_negative_scale_lowercontinuationsource_table)))))) /\ (forall dst_index_lowercontinuationsource_table. (exists pvs_le_gap_lowercontinuationsource_tabledomain. pvs_le_gap_lowercontinuationsource_tabledomain + (dst_index_lowercontinuationsource_table) = (0)) -> exists dst_positive_lowercontinuationsource_table dst_negative_lowercontinuationsource_table dst_value_lowercontinuationsource_table. ((((exists ff_h_pvs_lowercontinuationsource_tableentrypositive. ff_h_pvs_lowercontinuationsource_tableentrypositive + S (dst_positive_lowercontinuationsource_table) = S ((S (dst_index_lowercontinuationsource_table)) * dst_positive_scale_lowercontinuationsource_table)) /\ exists ff_q_pvs_lowercontinuationsource_tableentrypositive. dst_positive_code_lowercontinuationsource_table = ff_q_pvs_lowercontinuationsource_tableentrypositive * S ((S (dst_index_lowercontinuationsource_table)) * dst_positive_scale_lowercontinuationsource_table) + (dst_positive_lowercontinuationsource_table))) /\ (((((exists ff_h_pvs_lowercontinuationsource_tableentrynegative. ff_h_pvs_lowercontinuationsource_tableentrynegative + S (dst_negative_lowercontinuationsource_table) = S ((S (dst_index_lowercontinuationsource_table)) * dst_negative_scale_lowercontinuationsource_table)) /\ exists ff_q_pvs_lowercontinuationsource_tableentrynegative. dst_negative_code_lowercontinuationsource_table = ff_q_pvs_lowercontinuationsource_tableentrynegative * S ((S (dst_index_lowercontinuationsource_table)) * dst_negative_scale_lowercontinuationsource_table) + (dst_negative_lowercontinuationsource_table))) /\ (exists ge_balance_positive_lowercontinuationsource_tableentryvalue ge_balance_negative_lowercontinuationsource_tableentryvalue. (((((dst_value_lowercontinuationsource_table) = 2 * (ge_balance_positive_lowercontinuationsource_tableentryvalue) /\ (ge_balance_negative_lowercontinuationsource_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationsource_tableentryvaluedecode. (((dst_value_lowercontinuationsource_table) = 2 * ge_signed_half_lowercontinuationsource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsource_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationsource_tableentryvalue) = S ge_signed_half_lowercontinuationsource_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationsource_table) + ge_balance_negative_lowercontinuationsource_tableentryvalue = (dst_negative_lowercontinuationsource_table) + ge_balance_positive_lowercontinuationsource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowercontinuationrow_table dst_positive_scale_lowercontinuationrow_table dst_negative_code_lowercontinuationrow_table dst_negative_scale_lowercontinuationrow_table. ((((R)) = (((((dst_positive_code_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table)) * S ((dst_positive_code_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table)) + ((dst_positive_scale_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table))) + (((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) * S ((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) + ((dst_negative_scale_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)))) * S ((((dst_positive_code_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table)) * S ((dst_positive_code_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table)) + ((dst_positive_scale_lowercontinuationrow_table) + (dst_positive_scale_lowercontinuationrow_table))) + (((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) * S ((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) + ((dst_negative_scale_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)))) + ((((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) * S ((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) + ((dst_negative_scale_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table))) + (((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) * S ((dst_negative_code_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)) + ((dst_negative_scale_lowercontinuationrow_table) + (dst_negative_scale_lowercontinuationrow_table)))))) /\ (forall dst_index_lowercontinuationrow_table. (exists pvs_le_gap_lowercontinuationrow_tabledomain. pvs_le_gap_lowercontinuationrow_tabledomain + (dst_index_lowercontinuationrow_table) = ((m))) -> exists dst_positive_lowercontinuationrow_table dst_negative_lowercontinuationrow_table dst_value_lowercontinuationrow_table. ((((exists ff_h_pvs_lowercontinuationrow_tableentrypositive. ff_h_pvs_lowercontinuationrow_tableentrypositive + S (dst_positive_lowercontinuationrow_table) = S ((S (dst_index_lowercontinuationrow_table)) * dst_positive_scale_lowercontinuationrow_table)) /\ exists ff_q_pvs_lowercontinuationrow_tableentrypositive. dst_positive_code_lowercontinuationrow_table = ff_q_pvs_lowercontinuationrow_tableentrypositive * S ((S (dst_index_lowercontinuationrow_table)) * dst_positive_scale_lowercontinuationrow_table) + (dst_positive_lowercontinuationrow_table))) /\ (((((exists ff_h_pvs_lowercontinuationrow_tableentrynegative. ff_h_pvs_lowercontinuationrow_tableentrynegative + S (dst_negative_lowercontinuationrow_table) = S ((S (dst_index_lowercontinuationrow_table)) * dst_negative_scale_lowercontinuationrow_table)) /\ exists ff_q_pvs_lowercontinuationrow_tableentrynegative. dst_negative_code_lowercontinuationrow_table = ff_q_pvs_lowercontinuationrow_tableentrynegative * S ((S (dst_index_lowercontinuationrow_table)) * dst_negative_scale_lowercontinuationrow_table) + (dst_negative_lowercontinuationrow_table))) /\ (exists ge_balance_positive_lowercontinuationrow_tableentryvalue ge_balance_negative_lowercontinuationrow_tableentryvalue. (((((dst_value_lowercontinuationrow_table) = 2 * (ge_balance_positive_lowercontinuationrow_tableentryvalue) /\ (ge_balance_negative_lowercontinuationrow_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationrow_tableentryvaluedecode. (((dst_value_lowercontinuationrow_table) = 2 * ge_signed_half_lowercontinuationrow_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrow_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationrow_tableentryvalue) = S ge_signed_half_lowercontinuationrow_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationrow_table) + ge_balance_negative_lowercontinuationrow_tableentryvalue = (dst_negative_lowercontinuationrow_table) + ge_balance_positive_lowercontinuationrow_tableentryvalue))))))))) /\ (forall srt_index_lowercontinuation. (exists pvs_gap_lowercontinuationbound. pvs_gap_lowercontinuationbound + S (srt_index_lowercontinuation) = ((m))) -> exists srt_value_lowercontinuation. (((exists dst_positive_code_lowercontinuationrowentry dst_positive_scale_lowercontinuationrowentry dst_negative_code_lowercontinuationrowentry dst_negative_scale_lowercontinuationrowentry dst_positive_lowercontinuationrowentry dst_negative_lowercontinuationrowentry. ((((R)) = (((((dst_positive_code_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry)) * S ((dst_positive_code_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry)) + ((dst_positive_scale_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry))) + (((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) * S ((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) + ((dst_negative_scale_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)))) * S ((((dst_positive_code_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry)) * S ((dst_positive_code_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry)) + ((dst_positive_scale_lowercontinuationrowentry) + (dst_positive_scale_lowercontinuationrowentry))) + (((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) * S ((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) + ((dst_negative_scale_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)))) + ((((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) * S ((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) + ((dst_negative_scale_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry))) + (((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) * S ((dst_negative_code_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)) + ((dst_negative_scale_lowercontinuationrowentry) + (dst_negative_scale_lowercontinuationrowentry)))))) /\ (((((exists ff_h_pvs_lowercontinuationrowentrypositive. ff_h_pvs_lowercontinuationrowentrypositive + S (dst_positive_lowercontinuationrowentry) = S ((S (srt_index_lowercontinuation)) * dst_positive_scale_lowercontinuationrowentry)) /\ exists ff_q_pvs_lowercontinuationrowentrypositive. dst_positive_code_lowercontinuationrowentry = ff_q_pvs_lowercontinuationrowentrypositive * S ((S (srt_index_lowercontinuation)) * dst_positive_scale_lowercontinuationrowentry) + (dst_positive_lowercontinuationrowentry))) /\ (((((exists ff_h_pvs_lowercontinuationrowentrynegative. ff_h_pvs_lowercontinuationrowentrynegative + S (dst_negative_lowercontinuationrowentry) = S ((S (srt_index_lowercontinuation)) * dst_negative_scale_lowercontinuationrowentry)) /\ exists ff_q_pvs_lowercontinuationrowentrynegative. dst_negative_code_lowercontinuationrowentry = ff_q_pvs_lowercontinuationrowentrynegative * S ((S (srt_index_lowercontinuation)) * dst_negative_scale_lowercontinuationrowentry) + (dst_negative_lowercontinuationrowentry))) /\ (exists ge_balance_positive_lowercontinuationrowentryvalue ge_balance_negative_lowercontinuationrowentryvalue. (((((srt_value_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationrowentryvalue) /\ (ge_balance_negative_lowercontinuationrowentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationrowentryvaluedecode. (((srt_value_lowercontinuation) = 2 * ge_signed_half_lowercontinuationrowentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrowentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationrowentryvalue) = S ge_signed_half_lowercontinuationrowentryvaluedecode))) /\ ((dst_positive_lowercontinuationrowentry) + ge_balance_negative_lowercontinuationrowentryvalue = (dst_negative_lowercontinuationrowentry) + ge_balance_positive_lowercontinuationrowentryvalue))))))))) /\ (exists srs_slice_lowercontinuationrowrow_sum. ((((exists dst_positive_code_lowercontinuationrowrow_sumslicesource_table dst_positive_scale_lowercontinuationrowrow_sumslicesource_table dst_negative_code_lowercontinuationrowrow_sumslicesource_table dst_negative_scale_lowercontinuationrowrow_sumslicesource_table. ((((F)) = (((((dst_positive_code_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_positive_code_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_positive_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table))) + (((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)))) * S ((((dst_positive_code_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_positive_code_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_positive_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_scale_lowercontinuationrowrow_sumslicesource_table))) + (((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)))) + ((((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table))) + (((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)))))) /\ (forall dst_index_lowercontinuationrowrow_sumslicesource_table. (exists pvs_le_gap_lowercontinuationrowrow_sumslicesource_tabledomain. pvs_le_gap_lowercontinuationrowrow_sumslicesource_tabledomain + (dst_index_lowercontinuationrowrow_sumslicesource_table) = (0)) -> exists dst_positive_lowercontinuationrowrow_sumslicesource_table dst_negative_lowercontinuationrowrow_sumslicesource_table dst_value_lowercontinuationrowrow_sumslicesource_table. ((((exists ff_h_pvs_lowercontinuationrowrow_sumslicesource_tableentrypositive. ff_h_pvs_lowercontinuationrowrow_sumslicesource_tableentrypositive + S (dst_positive_lowercontinuationrowrow_sumslicesource_table) = S ((S (dst_index_lowercontinuationrowrow_sumslicesource_table)) * dst_positive_scale_lowercontinuationrowrow_sumslicesource_table)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumslicesource_tableentrypositive. dst_positive_code_lowercontinuationrowrow_sumslicesource_table = ff_q_pvs_lowercontinuationrowrow_sumslicesource_tableentrypositive * S ((S (dst_index_lowercontinuationrowrow_sumslicesource_table)) * dst_positive_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_positive_lowercontinuationrowrow_sumslicesource_table))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumslicesource_tableentrynegative. ff_h_pvs_lowercontinuationrowrow_sumslicesource_tableentrynegative + S (dst_negative_lowercontinuationrowrow_sumslicesource_table) = S ((S (dst_index_lowercontinuationrowrow_sumslicesource_table)) * dst_negative_scale_lowercontinuationrowrow_sumslicesource_table)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumslicesource_tableentrynegative. dst_negative_code_lowercontinuationrowrow_sumslicesource_table = ff_q_pvs_lowercontinuationrowrow_sumslicesource_tableentrynegative * S ((S (dst_index_lowercontinuationrowrow_sumslicesource_table)) * dst_negative_scale_lowercontinuationrowrow_sumslicesource_table) + (dst_negative_lowercontinuationrowrow_sumslicesource_table))) /\ (exists ge_balance_positive_lowercontinuationrowrow_sumslicesource_tableentryvalue ge_balance_negative_lowercontinuationrowrow_sumslicesource_tableentryvalue. (((((dst_value_lowercontinuationrowrow_sumslicesource_table) = 2 * (ge_balance_positive_lowercontinuationrowrow_sumslicesource_tableentryvalue) /\ (ge_balance_negative_lowercontinuationrowrow_sumslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationrowrow_sumslicesource_tableentryvaluedecode. (((dst_value_lowercontinuationrowrow_sumslicesource_table) = 2 * ge_signed_half_lowercontinuationrowrow_sumslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrowrow_sumslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationrowrow_sumslicesource_tableentryvalue) = S ge_signed_half_lowercontinuationrowrow_sumslicesource_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationrowrow_sumslicesource_table) + ge_balance_negative_lowercontinuationrowrow_sumslicesource_tableentryvalue = (dst_negative_lowercontinuationrowrow_sumslicesource_table) + ge_balance_positive_lowercontinuationrowrow_sumslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table. (((srs_slice_lowercontinuationrowrow_sum) = (((((dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)))) * S ((((dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)))) + ((((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)))))) /\ (forall dst_index_lowercontinuationrowrow_sumsliceoutput_table. (exists pvs_le_gap_lowercontinuationrowrow_sumsliceoutput_tabledomain. pvs_le_gap_lowercontinuationrowrow_sumsliceoutput_tabledomain + (dst_index_lowercontinuationrowrow_sumsliceoutput_table) = ((n))) -> exists dst_positive_lowercontinuationrowrow_sumsliceoutput_table dst_negative_lowercontinuationrowrow_sumsliceoutput_table dst_value_lowercontinuationrowrow_sumsliceoutput_table. ((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrypositive. ff_h_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrypositive + S (dst_positive_lowercontinuationrowrow_sumsliceoutput_table) = S ((S (dst_index_lowercontinuationrowrow_sumsliceoutput_table)) * dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrypositive. dst_positive_code_lowercontinuationrowrow_sumsliceoutput_table = ff_q_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrypositive * S ((S (dst_index_lowercontinuationrowrow_sumsliceoutput_table)) * dst_positive_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_positive_lowercontinuationrowrow_sumsliceoutput_table))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrynegative. ff_h_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrynegative + S (dst_negative_lowercontinuationrowrow_sumsliceoutput_table) = S ((S (dst_index_lowercontinuationrowrow_sumsliceoutput_table)) * dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrynegative. dst_negative_code_lowercontinuationrowrow_sumsliceoutput_table = ff_q_pvs_lowercontinuationrowrow_sumsliceoutput_tableentrynegative * S ((S (dst_index_lowercontinuationrowrow_sumsliceoutput_table)) * dst_negative_scale_lowercontinuationrowrow_sumsliceoutput_table) + (dst_negative_lowercontinuationrowrow_sumsliceoutput_table))) /\ (exists ge_balance_positive_lowercontinuationrowrow_sumsliceoutput_tableentryvalue ge_balance_negative_lowercontinuationrowrow_sumsliceoutput_tableentryvalue. (((((dst_value_lowercontinuationrowrow_sumsliceoutput_table) = 2 * (ge_balance_positive_lowercontinuationrowrow_sumsliceoutput_tableentryvalue) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationrowrow_sumsliceoutput_tableentryvaluedecode. (((dst_value_lowercontinuationrowrow_sumsliceoutput_table) = 2 * ge_signed_half_lowercontinuationrowrow_sumsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrowrow_sumsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceoutput_tableentryvalue) = S ge_signed_half_lowercontinuationrowrow_sumsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationrowrow_sumsliceoutput_table) + ge_balance_negative_lowercontinuationrowrow_sumsliceoutput_tableentryvalue = (dst_negative_lowercontinuationrowrow_sumsliceoutput_table) + ge_balance_positive_lowercontinuationrowrow_sumsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_lowercontinuationrowrow_sumslice. (exists pvs_gap_lowercontinuationrowrow_sumslicebound. pvs_gap_lowercontinuationrowrow_sumslicebound + S (srs_index_lowercontinuationrowrow_sumslice) = ((n))) -> exists srs_value_lowercontinuationrowrow_sumslice. (((exists dst_positive_code_lowercontinuationrowrow_sumsliceentrysource dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource dst_negative_code_lowercontinuationrowrow_sumsliceentrysource dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource dst_positive_lowercontinuationrowrow_sumsliceentrysource dst_negative_lowercontinuationrowrow_sumsliceentrysource. ((((F)) = (((((dst_positive_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)))) * S ((((dst_positive_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)))) + ((((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)))))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceentrysourcepositive. ff_h_pvs_lowercontinuationrowrow_sumsliceentrysourcepositive + S (dst_positive_lowercontinuationrowrow_sumsliceentrysource) = S ((S ((((((o)) + (((s)) * (srt_index_lowercontinuation)))) + (((t)) * (srs_index_lowercontinuationrowrow_sumslice))))) * dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceentrysourcepositive. dst_positive_code_lowercontinuationrowrow_sumsliceentrysource = ff_q_pvs_lowercontinuationrowrow_sumsliceentrysourcepositive * S ((S ((((((o)) + (((s)) * (srt_index_lowercontinuation)))) + (((t)) * (srs_index_lowercontinuationrowrow_sumslice))))) * dst_positive_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_positive_lowercontinuationrowrow_sumsliceentrysource))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceentrysourcenegative. ff_h_pvs_lowercontinuationrowrow_sumsliceentrysourcenegative + S (dst_negative_lowercontinuationrowrow_sumsliceentrysource) = S ((S ((((((o)) + (((s)) * (srt_index_lowercontinuation)))) + (((t)) * (srs_index_lowercontinuationrowrow_sumslice))))) * dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceentrysourcenegative. dst_negative_code_lowercontinuationrowrow_sumsliceentrysource = ff_q_pvs_lowercontinuationrowrow_sumsliceentrysourcenegative * S ((S ((((((o)) + (((s)) * (srt_index_lowercontinuation)))) + (((t)) * (srs_index_lowercontinuationrowrow_sumslice))))) * dst_negative_scale_lowercontinuationrowrow_sumsliceentrysource) + (dst_negative_lowercontinuationrowrow_sumsliceentrysource))) /\ (exists ge_balance_positive_lowercontinuationrowrow_sumsliceentrysourcevalue ge_balance_negative_lowercontinuationrowrow_sumsliceentrysourcevalue. (((((srs_value_lowercontinuationrowrow_sumslice) = 2 * (ge_balance_positive_lowercontinuationrowrow_sumsliceentrysourcevalue) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceentrysourcevalue) = 0) \/ exists ge_signed_half_lowercontinuationrowrow_sumsliceentrysourcevaluedecode. (((srs_value_lowercontinuationrowrow_sumslice) = 2 * ge_signed_half_lowercontinuationrowrow_sumsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrowrow_sumsliceentrysourcevalue) = 0) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceentrysourcevalue) = S ge_signed_half_lowercontinuationrowrow_sumsliceentrysourcevaluedecode))) /\ ((dst_positive_lowercontinuationrowrow_sumsliceentrysource) + ge_balance_negative_lowercontinuationrowrow_sumsliceentrysourcevalue = (dst_negative_lowercontinuationrowrow_sumsliceentrysource) + ge_balance_positive_lowercontinuationrowrow_sumsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput dst_positive_lowercontinuationrowrow_sumsliceentryoutput dst_negative_lowercontinuationrowrow_sumsliceentryoutput. (((srs_slice_lowercontinuationrowrow_sum) = (((((dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)))) * S ((((dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)))) + ((((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput))) + (((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) * S ((dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) + ((dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)))))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceentryoutputpositive. ff_h_pvs_lowercontinuationrowrow_sumsliceentryoutputpositive + S (dst_positive_lowercontinuationrowrow_sumsliceentryoutput) = S ((S (srs_index_lowercontinuationrowrow_sumslice)) * dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceentryoutputpositive. dst_positive_code_lowercontinuationrowrow_sumsliceentryoutput = ff_q_pvs_lowercontinuationrowrow_sumsliceentryoutputpositive * S ((S (srs_index_lowercontinuationrowrow_sumslice)) * dst_positive_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_positive_lowercontinuationrowrow_sumsliceentryoutput))) /\ (((((exists ff_h_pvs_lowercontinuationrowrow_sumsliceentryoutputnegative. ff_h_pvs_lowercontinuationrowrow_sumsliceentryoutputnegative + S (dst_negative_lowercontinuationrowrow_sumsliceentryoutput) = S ((S (srs_index_lowercontinuationrowrow_sumslice)) * dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput)) /\ exists ff_q_pvs_lowercontinuationrowrow_sumsliceentryoutputnegative. dst_negative_code_lowercontinuationrowrow_sumsliceentryoutput = ff_q_pvs_lowercontinuationrowrow_sumsliceentryoutputnegative * S ((S (srs_index_lowercontinuationrowrow_sumslice)) * dst_negative_scale_lowercontinuationrowrow_sumsliceentryoutput) + (dst_negative_lowercontinuationrowrow_sumsliceentryoutput))) /\ (exists ge_balance_positive_lowercontinuationrowrow_sumsliceentryoutputvalue ge_balance_negative_lowercontinuationrowrow_sumsliceentryoutputvalue. (((((srs_value_lowercontinuationrowrow_sumslice) = 2 * (ge_balance_positive_lowercontinuationrowrow_sumsliceentryoutputvalue) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceentryoutputvalue) = 0) \/ exists ge_signed_half_lowercontinuationrowrow_sumsliceentryoutputvaluedecode. (((srs_value_lowercontinuationrowrow_sumslice) = 2 * ge_signed_half_lowercontinuationrowrow_sumsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationrowrow_sumsliceentryoutputvalue) = 0) /\ (ge_balance_negative_lowercontinuationrowrow_sumsliceentryoutputvalue) = S ge_signed_half_lowercontinuationrowrow_sumsliceentryoutputvaluedecode))) /\ ((dst_positive_lowercontinuationrowrow_sumsliceentryoutput) + ge_balance_negative_lowercontinuationrowrow_sumsliceentryoutputvalue = (dst_negative_lowercontinuationrowrow_sumsliceentryoutput) + ge_balance_positive_lowercontinuationrowrow_sumsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_lowercontinuationrowrow_sumsum dst_positive_scale_lowercontinuationrowrow_sumsum dst_negative_code_lowercontinuationrowrow_sumsum dst_negative_scale_lowercontinuationrowrow_sumsum dst_positive_sum_lowercontinuationrowrow_sumsum dst_negative_sum_lowercontinuationrowrow_sumsum. (((srs_slice_lowercontinuationrowrow_sum) = (((((dst_positive_code_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum)) * S ((dst_positive_code_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum)) + ((dst_positive_scale_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum))) + (((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) * S ((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) + ((dst_negative_scale_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)))) * S ((((dst_positive_code_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum)) * S ((dst_positive_code_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum)) + ((dst_positive_scale_lowercontinuationrowrow_sumsum) + (dst_positive_scale_lowercontinuationrowrow_sumsum))) + (((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) * S ((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) + ((dst_negative_scale_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)))) + ((((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) * S ((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) + ((dst_negative_scale_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum))) + (((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) * S ((dst_negative_code_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)) + ((dst_negative_scale_lowercontinuationrowrow_sumsum) + (dst_negative_scale_lowercontinuationrowrow_sumsum)))))) /\ (((exists fs_u_dst_lowercontinuationrowrow_sumsumpositive fs_v_dst_lowercontinuationrowrow_sumsumpositive. ((((exists fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_start. fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_start. fs_u_dst_lowercontinuationrowrow_sumsumpositive = fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_start * S ((S (0)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive) + (0))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_terminal. fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_terminal + S (dst_positive_sum_lowercontinuationrowrow_sumsum) = S ((S ((n))) * fs_v_dst_lowercontinuationrowrow_sumsumpositive)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_terminal. fs_u_dst_lowercontinuationrowrow_sumsumpositive = fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_terminal * S ((S ((n))) * fs_v_dst_lowercontinuationrowrow_sumsumpositive) + (dst_positive_sum_lowercontinuationrowrow_sumsum))) /\ forall fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps. (exists fs_lt_dst_lowercontinuationrowrow_sumsumpositive_body_steps_bound. fs_lt_dst_lowercontinuationrowrow_sumsumpositive_body_steps_bound + S fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps = (n)) -> exists fs_a_dst_lowercontinuationrowrow_sumsumpositive_body_steps fs_r_dst_lowercontinuationrowrow_sumsumpositive_body_steps fs_s_dst_lowercontinuationrowrow_sumsumpositive_body_steps. ((((exists fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_summand. fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_summand + S (fs_a_dst_lowercontinuationrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * dst_positive_scale_lowercontinuationrowrow_sumsum)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_summand. dst_positive_code_lowercontinuationrowrow_sumsum = fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_summand * S ((S (fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * dst_positive_scale_lowercontinuationrowrow_sumsum) + (fs_a_dst_lowercontinuationrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_partial. fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_partial + S (fs_r_dst_lowercontinuationrowrow_sumsumpositive_body_steps) = S ((S (fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_partial. fs_u_dst_lowercontinuationrowrow_sumsumpositive = fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_partial * S ((S (fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive) + (fs_r_dst_lowercontinuationrowrow_sumsumpositive_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_successor. fs_h_dst_lowercontinuationrowrow_sumsumpositive_body_steps_successor + S (fs_s_dst_lowercontinuationrowrow_sumsumpositive_body_steps) = S ((S (S fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_successor. fs_u_dst_lowercontinuationrowrow_sumsumpositive = fs_q_dst_lowercontinuationrowrow_sumsumpositive_body_steps_successor * S ((S (S fs_i_dst_lowercontinuationrowrow_sumsumpositive_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumpositive) + (fs_s_dst_lowercontinuationrowrow_sumsumpositive_body_steps))) /\ fs_s_dst_lowercontinuationrowrow_sumsumpositive_body_steps = fs_r_dst_lowercontinuationrowrow_sumsumpositive_body_steps + fs_a_dst_lowercontinuationrowrow_sumsumpositive_body_steps)))))) /\ (((exists fs_u_dst_lowercontinuationrowrow_sumsumnegative fs_v_dst_lowercontinuationrowrow_sumsumnegative. ((((exists fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_start. fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_start. fs_u_dst_lowercontinuationrowrow_sumsumnegative = fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_start * S ((S (0)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative) + (0))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_terminal. fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_terminal + S (dst_negative_sum_lowercontinuationrowrow_sumsum) = S ((S ((n))) * fs_v_dst_lowercontinuationrowrow_sumsumnegative)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_terminal. fs_u_dst_lowercontinuationrowrow_sumsumnegative = fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_terminal * S ((S ((n))) * fs_v_dst_lowercontinuationrowrow_sumsumnegative) + (dst_negative_sum_lowercontinuationrowrow_sumsum))) /\ forall fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps. (exists fs_lt_dst_lowercontinuationrowrow_sumsumnegative_body_steps_bound. fs_lt_dst_lowercontinuationrowrow_sumsumnegative_body_steps_bound + S fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps = (n)) -> exists fs_a_dst_lowercontinuationrowrow_sumsumnegative_body_steps fs_r_dst_lowercontinuationrowrow_sumsumnegative_body_steps fs_s_dst_lowercontinuationrowrow_sumsumnegative_body_steps. ((((exists fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_summand. fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_summand + S (fs_a_dst_lowercontinuationrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * dst_negative_scale_lowercontinuationrowrow_sumsum)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_summand. dst_negative_code_lowercontinuationrowrow_sumsum = fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_summand * S ((S (fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * dst_negative_scale_lowercontinuationrowrow_sumsum) + (fs_a_dst_lowercontinuationrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_partial. fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_partial + S (fs_r_dst_lowercontinuationrowrow_sumsumnegative_body_steps) = S ((S (fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_partial. fs_u_dst_lowercontinuationrowrow_sumsumnegative = fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_partial * S ((S (fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative) + (fs_r_dst_lowercontinuationrowrow_sumsumnegative_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_successor. fs_h_dst_lowercontinuationrowrow_sumsumnegative_body_steps_successor + S (fs_s_dst_lowercontinuationrowrow_sumsumnegative_body_steps) = S ((S (S fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative)) /\ exists fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_successor. fs_u_dst_lowercontinuationrowrow_sumsumnegative = fs_q_dst_lowercontinuationrowrow_sumsumnegative_body_steps_successor * S ((S (S fs_i_dst_lowercontinuationrowrow_sumsumnegative_body_steps)) * fs_v_dst_lowercontinuationrowrow_sumsumnegative) + (fs_s_dst_lowercontinuationrowrow_sumsumnegative_body_steps))) /\ fs_s_dst_lowercontinuationrowrow_sumsumnegative_body_steps = fs_r_dst_lowercontinuationrowrow_sumsumnegative_body_steps + fs_a_dst_lowercontinuationrowrow_sumsumnegative_body_steps)))))) /\ (exists ge_balance_positive_lowercontinuationrowrow_sumsumresult ge_balance_negative_lowercontinuationrowrow_sumsumresult. (((((srt_value_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationrowrow_sumsumresult) /\ (ge_balance_negative_lowercontinuationrowrow_sumsumresult) = 0) \/ exists ge_signed_half_lowercontinuationrowrow_sumsumresultdecode. (((srt_value_lowercontinuation) = 2 * ge_signed_half_lowercontinuationrowrow_sumsumresultdecode + 1 /\ (ge_balance_positive_lowercontinuationrowrow_sumsumresult) = 0) /\ (ge_balance_negative_lowercontinuationrowrow_sumsumresult) = S ge_signed_half_lowercontinuationrowrow_sumsumresultdecode))) /\ ((dst_positive_sum_lowercontinuationrowrow_sumsum) + ge_balance_negative_lowercontinuationrowrow_sumsumresult = (dst_negative_sum_lowercontinuationrowrow_sumsum) + ge_balance_positive_lowercontinuationrowrow_sumsumresult)))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.