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
∃ srs_slice_lowercontinuation. ArithSlice(F,srs_slice_lowercontinuation,o,s,l) ∧ SignedPrefixSum(srs_slice_lowercontinuation,l,z)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists srs_slice_lowercontinuation. ((((exists dst_positive_code_lowercontinuationslicesource_table dst_positive_scale_lowercontinuationslicesource_table dst_negative_code_lowercontinuationslicesource_table dst_negative_scale_lowercontinuationslicesource_table. ((((F)) = (((((dst_positive_code_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table)) * S ((dst_positive_code_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table)) + ((dst_positive_scale_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table))) + (((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) * S ((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) + ((dst_negative_scale_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)))) * S ((((dst_positive_code_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table)) * S ((dst_positive_code_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table)) + ((dst_positive_scale_lowercontinuationslicesource_table) + (dst_positive_scale_lowercontinuationslicesource_table))) + (((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) * S ((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) + ((dst_negative_scale_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)))) + ((((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) * S ((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) + ((dst_negative_scale_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table))) + (((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) * S ((dst_negative_code_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)) + ((dst_negative_scale_lowercontinuationslicesource_table) + (dst_negative_scale_lowercontinuationslicesource_table)))))) /\ (forall dst_index_lowercontinuationslicesource_table. (exists pvs_le_gap_lowercontinuationslicesource_tabledomain. pvs_le_gap_lowercontinuationslicesource_tabledomain + (dst_index_lowercontinuationslicesource_table) = (0)) -> exists dst_positive_lowercontinuationslicesource_table dst_negative_lowercontinuationslicesource_table dst_value_lowercontinuationslicesource_table. ((((exists ff_h_pvs_lowercontinuationslicesource_tableentrypositive. ff_h_pvs_lowercontinuationslicesource_tableentrypositive + S (dst_positive_lowercontinuationslicesource_table) = S ((S (dst_index_lowercontinuationslicesource_table)) * dst_positive_scale_lowercontinuationslicesource_table)) /\ exists ff_q_pvs_lowercontinuationslicesource_tableentrypositive. dst_positive_code_lowercontinuationslicesource_table = ff_q_pvs_lowercontinuationslicesource_tableentrypositive * S ((S (dst_index_lowercontinuationslicesource_table)) * dst_positive_scale_lowercontinuationslicesource_table) + (dst_positive_lowercontinuationslicesource_table))) /\ (((((exists ff_h_pvs_lowercontinuationslicesource_tableentrynegative. ff_h_pvs_lowercontinuationslicesource_tableentrynegative + S (dst_negative_lowercontinuationslicesource_table) = S ((S (dst_index_lowercontinuationslicesource_table)) * dst_negative_scale_lowercontinuationslicesource_table)) /\ exists ff_q_pvs_lowercontinuationslicesource_tableentrynegative. dst_negative_code_lowercontinuationslicesource_table = ff_q_pvs_lowercontinuationslicesource_tableentrynegative * S ((S (dst_index_lowercontinuationslicesource_table)) * dst_negative_scale_lowercontinuationslicesource_table) + (dst_negative_lowercontinuationslicesource_table))) /\ (exists ge_balance_positive_lowercontinuationslicesource_tableentryvalue ge_balance_negative_lowercontinuationslicesource_tableentryvalue. (((((dst_value_lowercontinuationslicesource_table) = 2 * (ge_balance_positive_lowercontinuationslicesource_tableentryvalue) /\ (ge_balance_negative_lowercontinuationslicesource_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationslicesource_tableentryvaluedecode. (((dst_value_lowercontinuationslicesource_table) = 2 * ge_signed_half_lowercontinuationslicesource_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationslicesource_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationslicesource_tableentryvalue) = S ge_signed_half_lowercontinuationslicesource_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationslicesource_table) + ge_balance_negative_lowercontinuationslicesource_tableentryvalue = (dst_negative_lowercontinuationslicesource_table) + ge_balance_positive_lowercontinuationslicesource_tableentryvalue))))))))) /\ (((exists dst_positive_code_lowercontinuationsliceoutput_table dst_positive_scale_lowercontinuationsliceoutput_table dst_negative_code_lowercontinuationsliceoutput_table dst_negative_scale_lowercontinuationsliceoutput_table. (((srs_slice_lowercontinuation) = (((((dst_positive_code_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table)) * S ((dst_positive_code_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table)) + ((dst_positive_scale_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table))) + (((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) * S ((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) + ((dst_negative_scale_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)))) * S ((((dst_positive_code_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table)) * S ((dst_positive_code_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table)) + ((dst_positive_scale_lowercontinuationsliceoutput_table) + (dst_positive_scale_lowercontinuationsliceoutput_table))) + (((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) * S ((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) + ((dst_negative_scale_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)))) + ((((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) * S ((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) + ((dst_negative_scale_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table))) + (((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) * S ((dst_negative_code_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)) + ((dst_negative_scale_lowercontinuationsliceoutput_table) + (dst_negative_scale_lowercontinuationsliceoutput_table)))))) /\ (forall dst_index_lowercontinuationsliceoutput_table. (exists pvs_le_gap_lowercontinuationsliceoutput_tabledomain. pvs_le_gap_lowercontinuationsliceoutput_tabledomain + (dst_index_lowercontinuationsliceoutput_table) = ((l))) -> exists dst_positive_lowercontinuationsliceoutput_table dst_negative_lowercontinuationsliceoutput_table dst_value_lowercontinuationsliceoutput_table. ((((exists ff_h_pvs_lowercontinuationsliceoutput_tableentrypositive. ff_h_pvs_lowercontinuationsliceoutput_tableentrypositive + S (dst_positive_lowercontinuationsliceoutput_table) = S ((S (dst_index_lowercontinuationsliceoutput_table)) * dst_positive_scale_lowercontinuationsliceoutput_table)) /\ exists ff_q_pvs_lowercontinuationsliceoutput_tableentrypositive. dst_positive_code_lowercontinuationsliceoutput_table = ff_q_pvs_lowercontinuationsliceoutput_tableentrypositive * S ((S (dst_index_lowercontinuationsliceoutput_table)) * dst_positive_scale_lowercontinuationsliceoutput_table) + (dst_positive_lowercontinuationsliceoutput_table))) /\ (((((exists ff_h_pvs_lowercontinuationsliceoutput_tableentrynegative. ff_h_pvs_lowercontinuationsliceoutput_tableentrynegative + S (dst_negative_lowercontinuationsliceoutput_table) = S ((S (dst_index_lowercontinuationsliceoutput_table)) * dst_negative_scale_lowercontinuationsliceoutput_table)) /\ exists ff_q_pvs_lowercontinuationsliceoutput_tableentrynegative. dst_negative_code_lowercontinuationsliceoutput_table = ff_q_pvs_lowercontinuationsliceoutput_tableentrynegative * S ((S (dst_index_lowercontinuationsliceoutput_table)) * dst_negative_scale_lowercontinuationsliceoutput_table) + (dst_negative_lowercontinuationsliceoutput_table))) /\ (exists ge_balance_positive_lowercontinuationsliceoutput_tableentryvalue ge_balance_negative_lowercontinuationsliceoutput_tableentryvalue. (((((dst_value_lowercontinuationsliceoutput_table) = 2 * (ge_balance_positive_lowercontinuationsliceoutput_tableentryvalue) /\ (ge_balance_negative_lowercontinuationsliceoutput_tableentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationsliceoutput_tableentryvaluedecode. (((dst_value_lowercontinuationsliceoutput_table) = 2 * ge_signed_half_lowercontinuationsliceoutput_tableentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsliceoutput_tableentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationsliceoutput_tableentryvalue) = S ge_signed_half_lowercontinuationsliceoutput_tableentryvaluedecode))) /\ ((dst_positive_lowercontinuationsliceoutput_table) + ge_balance_negative_lowercontinuationsliceoutput_tableentryvalue = (dst_negative_lowercontinuationsliceoutput_table) + ge_balance_positive_lowercontinuationsliceoutput_tableentryvalue))))))))) /\ (forall srs_index_lowercontinuationslice. (exists pvs_gap_lowercontinuationslicebound. pvs_gap_lowercontinuationslicebound + S (srs_index_lowercontinuationslice) = ((l))) -> exists srs_value_lowercontinuationslice. (((exists dst_positive_code_lowercontinuationsliceentrysource dst_positive_scale_lowercontinuationsliceentrysource dst_negative_code_lowercontinuationsliceentrysource dst_negative_scale_lowercontinuationsliceentrysource dst_positive_lowercontinuationsliceentrysource dst_negative_lowercontinuationsliceentrysource. ((((F)) = (((((dst_positive_code_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource)) * S ((dst_positive_code_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource)) + ((dst_positive_scale_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource))) + (((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) * S ((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) + ((dst_negative_scale_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)))) * S ((((dst_positive_code_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource)) * S ((dst_positive_code_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource)) + ((dst_positive_scale_lowercontinuationsliceentrysource) + (dst_positive_scale_lowercontinuationsliceentrysource))) + (((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) * S ((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) + ((dst_negative_scale_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)))) + ((((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) * S ((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) + ((dst_negative_scale_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource))) + (((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) * S ((dst_negative_code_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)) + ((dst_negative_scale_lowercontinuationsliceentrysource) + (dst_negative_scale_lowercontinuationsliceentrysource)))))) /\ (((((exists ff_h_pvs_lowercontinuationsliceentrysourcepositive. ff_h_pvs_lowercontinuationsliceentrysourcepositive + S (dst_positive_lowercontinuationsliceentrysource) = S ((S ((((o)) + (((s)) * (srs_index_lowercontinuationslice))))) * dst_positive_scale_lowercontinuationsliceentrysource)) /\ exists ff_q_pvs_lowercontinuationsliceentrysourcepositive. dst_positive_code_lowercontinuationsliceentrysource = ff_q_pvs_lowercontinuationsliceentrysourcepositive * S ((S ((((o)) + (((s)) * (srs_index_lowercontinuationslice))))) * dst_positive_scale_lowercontinuationsliceentrysource) + (dst_positive_lowercontinuationsliceentrysource))) /\ (((((exists ff_h_pvs_lowercontinuationsliceentrysourcenegative. ff_h_pvs_lowercontinuationsliceentrysourcenegative + S (dst_negative_lowercontinuationsliceentrysource) = S ((S ((((o)) + (((s)) * (srs_index_lowercontinuationslice))))) * dst_negative_scale_lowercontinuationsliceentrysource)) /\ exists ff_q_pvs_lowercontinuationsliceentrysourcenegative. dst_negative_code_lowercontinuationsliceentrysource = ff_q_pvs_lowercontinuationsliceentrysourcenegative * S ((S ((((o)) + (((s)) * (srs_index_lowercontinuationslice))))) * dst_negative_scale_lowercontinuationsliceentrysource) + (dst_negative_lowercontinuationsliceentrysource))) /\ (exists ge_balance_positive_lowercontinuationsliceentrysourcevalue ge_balance_negative_lowercontinuationsliceentrysourcevalue. (((((srs_value_lowercontinuationslice) = 2 * (ge_balance_positive_lowercontinuationsliceentrysourcevalue) /\ (ge_balance_negative_lowercontinuationsliceentrysourcevalue) = 0) \/ exists ge_signed_half_lowercontinuationsliceentrysourcevaluedecode. (((srs_value_lowercontinuationslice) = 2 * ge_signed_half_lowercontinuationsliceentrysourcevaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsliceentrysourcevalue) = 0) /\ (ge_balance_negative_lowercontinuationsliceentrysourcevalue) = S ge_signed_half_lowercontinuationsliceentrysourcevaluedecode))) /\ ((dst_positive_lowercontinuationsliceentrysource) + ge_balance_negative_lowercontinuationsliceentrysourcevalue = (dst_negative_lowercontinuationsliceentrysource) + ge_balance_positive_lowercontinuationsliceentrysourcevalue))))))))) /\ (exists dst_positive_code_lowercontinuationsliceentryoutput dst_positive_scale_lowercontinuationsliceentryoutput dst_negative_code_lowercontinuationsliceentryoutput dst_negative_scale_lowercontinuationsliceentryoutput dst_positive_lowercontinuationsliceentryoutput dst_negative_lowercontinuationsliceentryoutput. (((srs_slice_lowercontinuation) = (((((dst_positive_code_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput)) * S ((dst_positive_code_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput)) + ((dst_positive_scale_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput))) + (((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) * S ((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) + ((dst_negative_scale_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)))) * S ((((dst_positive_code_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput)) * S ((dst_positive_code_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput)) + ((dst_positive_scale_lowercontinuationsliceentryoutput) + (dst_positive_scale_lowercontinuationsliceentryoutput))) + (((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) * S ((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) + ((dst_negative_scale_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)))) + ((((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) * S ((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) + ((dst_negative_scale_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput))) + (((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) * S ((dst_negative_code_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)) + ((dst_negative_scale_lowercontinuationsliceentryoutput) + (dst_negative_scale_lowercontinuationsliceentryoutput)))))) /\ (((((exists ff_h_pvs_lowercontinuationsliceentryoutputpositive. ff_h_pvs_lowercontinuationsliceentryoutputpositive + S (dst_positive_lowercontinuationsliceentryoutput) = S ((S (srs_index_lowercontinuationslice)) * dst_positive_scale_lowercontinuationsliceentryoutput)) /\ exists ff_q_pvs_lowercontinuationsliceentryoutputpositive. dst_positive_code_lowercontinuationsliceentryoutput = ff_q_pvs_lowercontinuationsliceentryoutputpositive * S ((S (srs_index_lowercontinuationslice)) * dst_positive_scale_lowercontinuationsliceentryoutput) + (dst_positive_lowercontinuationsliceentryoutput))) /\ (((((exists ff_h_pvs_lowercontinuationsliceentryoutputnegative. ff_h_pvs_lowercontinuationsliceentryoutputnegative + S (dst_negative_lowercontinuationsliceentryoutput) = S ((S (srs_index_lowercontinuationslice)) * dst_negative_scale_lowercontinuationsliceentryoutput)) /\ exists ff_q_pvs_lowercontinuationsliceentryoutputnegative. dst_negative_code_lowercontinuationsliceentryoutput = ff_q_pvs_lowercontinuationsliceentryoutputnegative * S ((S (srs_index_lowercontinuationslice)) * dst_negative_scale_lowercontinuationsliceentryoutput) + (dst_negative_lowercontinuationsliceentryoutput))) /\ (exists ge_balance_positive_lowercontinuationsliceentryoutputvalue ge_balance_negative_lowercontinuationsliceentryoutputvalue. (((((srs_value_lowercontinuationslice) = 2 * (ge_balance_positive_lowercontinuationsliceentryoutputvalue) /\ (ge_balance_negative_lowercontinuationsliceentryoutputvalue) = 0) \/ exists ge_signed_half_lowercontinuationsliceentryoutputvaluedecode. (((srs_value_lowercontinuationslice) = 2 * ge_signed_half_lowercontinuationsliceentryoutputvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationsliceentryoutputvalue) = 0) /\ (ge_balance_negative_lowercontinuationsliceentryoutputvalue) = S ge_signed_half_lowercontinuationsliceentryoutputvaluedecode))) /\ ((dst_positive_lowercontinuationsliceentryoutput) + ge_balance_negative_lowercontinuationsliceentryoutputvalue = (dst_negative_lowercontinuationsliceentryoutput) + ge_balance_positive_lowercontinuationsliceentryoutputvalue)))))))))))))))) /\ (exists dst_positive_code_lowercontinuationsum dst_positive_scale_lowercontinuationsum dst_negative_code_lowercontinuationsum dst_negative_scale_lowercontinuationsum dst_positive_sum_lowercontinuationsum dst_negative_sum_lowercontinuationsum. (((srs_slice_lowercontinuation) = (((((dst_positive_code_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum)) * S ((dst_positive_code_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum)) + ((dst_positive_scale_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum))) + (((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) * S ((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) + ((dst_negative_scale_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)))) * S ((((dst_positive_code_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum)) * S ((dst_positive_code_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum)) + ((dst_positive_scale_lowercontinuationsum) + (dst_positive_scale_lowercontinuationsum))) + (((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) * S ((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) + ((dst_negative_scale_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)))) + ((((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) * S ((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) + ((dst_negative_scale_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum))) + (((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) * S ((dst_negative_code_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)) + ((dst_negative_scale_lowercontinuationsum) + (dst_negative_scale_lowercontinuationsum)))))) /\ (((exists fs_u_dst_lowercontinuationsumpositive fs_v_dst_lowercontinuationsumpositive. ((((exists fs_h_dst_lowercontinuationsumpositive_body_start. fs_h_dst_lowercontinuationsumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_lowercontinuationsumpositive)) /\ exists fs_q_dst_lowercontinuationsumpositive_body_start. fs_u_dst_lowercontinuationsumpositive = fs_q_dst_lowercontinuationsumpositive_body_start * S ((S (0)) * fs_v_dst_lowercontinuationsumpositive) + (0))) /\ ((((exists fs_h_dst_lowercontinuationsumpositive_body_terminal. fs_h_dst_lowercontinuationsumpositive_body_terminal + S (dst_positive_sum_lowercontinuationsum) = S ((S ((l))) * fs_v_dst_lowercontinuationsumpositive)) /\ exists fs_q_dst_lowercontinuationsumpositive_body_terminal. fs_u_dst_lowercontinuationsumpositive = fs_q_dst_lowercontinuationsumpositive_body_terminal * S ((S ((l))) * fs_v_dst_lowercontinuationsumpositive) + (dst_positive_sum_lowercontinuationsum))) /\ forall fs_i_dst_lowercontinuationsumpositive_body_steps. (exists fs_lt_dst_lowercontinuationsumpositive_body_steps_bound. fs_lt_dst_lowercontinuationsumpositive_body_steps_bound + S fs_i_dst_lowercontinuationsumpositive_body_steps = (l)) -> exists fs_a_dst_lowercontinuationsumpositive_body_steps fs_r_dst_lowercontinuationsumpositive_body_steps fs_s_dst_lowercontinuationsumpositive_body_steps. ((((exists fs_h_dst_lowercontinuationsumpositive_body_steps_summand. fs_h_dst_lowercontinuationsumpositive_body_steps_summand + S (fs_a_dst_lowercontinuationsumpositive_body_steps) = S ((S (fs_i_dst_lowercontinuationsumpositive_body_steps)) * dst_positive_scale_lowercontinuationsum)) /\ exists fs_q_dst_lowercontinuationsumpositive_body_steps_summand. dst_positive_code_lowercontinuationsum = fs_q_dst_lowercontinuationsumpositive_body_steps_summand * S ((S (fs_i_dst_lowercontinuationsumpositive_body_steps)) * dst_positive_scale_lowercontinuationsum) + (fs_a_dst_lowercontinuationsumpositive_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationsumpositive_body_steps_partial. fs_h_dst_lowercontinuationsumpositive_body_steps_partial + S (fs_r_dst_lowercontinuationsumpositive_body_steps) = S ((S (fs_i_dst_lowercontinuationsumpositive_body_steps)) * fs_v_dst_lowercontinuationsumpositive)) /\ exists fs_q_dst_lowercontinuationsumpositive_body_steps_partial. fs_u_dst_lowercontinuationsumpositive = fs_q_dst_lowercontinuationsumpositive_body_steps_partial * S ((S (fs_i_dst_lowercontinuationsumpositive_body_steps)) * fs_v_dst_lowercontinuationsumpositive) + (fs_r_dst_lowercontinuationsumpositive_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationsumpositive_body_steps_successor. fs_h_dst_lowercontinuationsumpositive_body_steps_successor + S (fs_s_dst_lowercontinuationsumpositive_body_steps) = S ((S (S fs_i_dst_lowercontinuationsumpositive_body_steps)) * fs_v_dst_lowercontinuationsumpositive)) /\ exists fs_q_dst_lowercontinuationsumpositive_body_steps_successor. fs_u_dst_lowercontinuationsumpositive = fs_q_dst_lowercontinuationsumpositive_body_steps_successor * S ((S (S fs_i_dst_lowercontinuationsumpositive_body_steps)) * fs_v_dst_lowercontinuationsumpositive) + (fs_s_dst_lowercontinuationsumpositive_body_steps))) /\ fs_s_dst_lowercontinuationsumpositive_body_steps = fs_r_dst_lowercontinuationsumpositive_body_steps + fs_a_dst_lowercontinuationsumpositive_body_steps)))))) /\ (((exists fs_u_dst_lowercontinuationsumnegative fs_v_dst_lowercontinuationsumnegative. ((((exists fs_h_dst_lowercontinuationsumnegative_body_start. fs_h_dst_lowercontinuationsumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_lowercontinuationsumnegative)) /\ exists fs_q_dst_lowercontinuationsumnegative_body_start. fs_u_dst_lowercontinuationsumnegative = fs_q_dst_lowercontinuationsumnegative_body_start * S ((S (0)) * fs_v_dst_lowercontinuationsumnegative) + (0))) /\ ((((exists fs_h_dst_lowercontinuationsumnegative_body_terminal. fs_h_dst_lowercontinuationsumnegative_body_terminal + S (dst_negative_sum_lowercontinuationsum) = S ((S ((l))) * fs_v_dst_lowercontinuationsumnegative)) /\ exists fs_q_dst_lowercontinuationsumnegative_body_terminal. fs_u_dst_lowercontinuationsumnegative = fs_q_dst_lowercontinuationsumnegative_body_terminal * S ((S ((l))) * fs_v_dst_lowercontinuationsumnegative) + (dst_negative_sum_lowercontinuationsum))) /\ forall fs_i_dst_lowercontinuationsumnegative_body_steps. (exists fs_lt_dst_lowercontinuationsumnegative_body_steps_bound. fs_lt_dst_lowercontinuationsumnegative_body_steps_bound + S fs_i_dst_lowercontinuationsumnegative_body_steps = (l)) -> exists fs_a_dst_lowercontinuationsumnegative_body_steps fs_r_dst_lowercontinuationsumnegative_body_steps fs_s_dst_lowercontinuationsumnegative_body_steps. ((((exists fs_h_dst_lowercontinuationsumnegative_body_steps_summand. fs_h_dst_lowercontinuationsumnegative_body_steps_summand + S (fs_a_dst_lowercontinuationsumnegative_body_steps) = S ((S (fs_i_dst_lowercontinuationsumnegative_body_steps)) * dst_negative_scale_lowercontinuationsum)) /\ exists fs_q_dst_lowercontinuationsumnegative_body_steps_summand. dst_negative_code_lowercontinuationsum = fs_q_dst_lowercontinuationsumnegative_body_steps_summand * S ((S (fs_i_dst_lowercontinuationsumnegative_body_steps)) * dst_negative_scale_lowercontinuationsum) + (fs_a_dst_lowercontinuationsumnegative_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationsumnegative_body_steps_partial. fs_h_dst_lowercontinuationsumnegative_body_steps_partial + S (fs_r_dst_lowercontinuationsumnegative_body_steps) = S ((S (fs_i_dst_lowercontinuationsumnegative_body_steps)) * fs_v_dst_lowercontinuationsumnegative)) /\ exists fs_q_dst_lowercontinuationsumnegative_body_steps_partial. fs_u_dst_lowercontinuationsumnegative = fs_q_dst_lowercontinuationsumnegative_body_steps_partial * S ((S (fs_i_dst_lowercontinuationsumnegative_body_steps)) * fs_v_dst_lowercontinuationsumnegative) + (fs_r_dst_lowercontinuationsumnegative_body_steps))) /\ ((((exists fs_h_dst_lowercontinuationsumnegative_body_steps_successor. fs_h_dst_lowercontinuationsumnegative_body_steps_successor + S (fs_s_dst_lowercontinuationsumnegative_body_steps) = S ((S (S fs_i_dst_lowercontinuationsumnegative_body_steps)) * fs_v_dst_lowercontinuationsumnegative)) /\ exists fs_q_dst_lowercontinuationsumnegative_body_steps_successor. fs_u_dst_lowercontinuationsumnegative = fs_q_dst_lowercontinuationsumnegative_body_steps_successor * S ((S (S fs_i_dst_lowercontinuationsumnegative_body_steps)) * fs_v_dst_lowercontinuationsumnegative) + (fs_s_dst_lowercontinuationsumnegative_body_steps))) /\ fs_s_dst_lowercontinuationsumnegative_body_steps = fs_r_dst_lowercontinuationsumnegative_body_steps + fs_a_dst_lowercontinuationsumnegative_body_steps)))))) /\ (exists ge_balance_positive_lowercontinuationsumresult ge_balance_negative_lowercontinuationsumresult. ((((((z)) = 2 * (ge_balance_positive_lowercontinuationsumresult) /\ (ge_balance_negative_lowercontinuationsumresult) = 0) \/ exists ge_signed_half_lowercontinuationsumresultdecode. ((((z)) = 2 * ge_signed_half_lowercontinuationsumresultdecode + 1 /\ (ge_balance_positive_lowercontinuationsumresult) = 0) /\ (ge_balance_negative_lowercontinuationsumresult) = S ge_signed_half_lowercontinuationsumresultdecode))) /\ ((dst_positive_sum_lowercontinuationsum) + ge_balance_negative_lowercontinuationsumresult = (dst_negative_sum_lowercontinuationsum) + ge_balance_positive_lowercontinuationsumresult))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.