signed_prefix_sum_point_spike_value

Exact expanded first-order arithmetic statement

forall F l p a z. (exists dst_positive_code_point_table dst_positive_scale_point_table dst_negative_code_point_table dst_negative_scale_point_table. (((F) = (((((dst_positive_code_point_table) + (dst_positive_scale_point_table)) * S ((dst_positive_code_point_table) + (dst_positive_scale_point_table)) + ((dst_positive_scale_point_table) + (dst_positive_scale_point_table))) + (((dst_negative_code_point_table) + (dst_negative_scale_point_table)) * S ((dst_negative_code_point_table) + (dst_negative_scale_point_table)) + ((dst_negative_scale_point_table) + (dst_negative_scale_point_table)))) * S ((((dst_positive_code_point_table) + (dst_positive_scale_point_table)) * S ((dst_positive_code_point_table) + (dst_positive_scale_point_table)) + ((dst_positive_scale_point_table) + (dst_positive_scale_point_table))) + (((dst_negative_code_point_table) + (dst_negative_scale_point_table)) * S ((dst_negative_code_point_table) + (dst_negative_scale_point_table)) + ((dst_negative_scale_point_table) + (dst_negative_scale_point_table)))) + ((((dst_negative_code_point_table) + (dst_negative_scale_point_table)) * S ((dst_negative_code_point_table) + (dst_negative_scale_point_table)) + ((dst_negative_scale_point_table) + (dst_negative_scale_point_table))) + (((dst_negative_code_point_table) + (dst_negative_scale_point_table)) * S ((dst_negative_code_point_table) + (dst_negative_scale_point_table)) + ((dst_negative_scale_point_table) + (dst_negative_scale_point_table)))))) /\ (forall dst_index_point_table. (exists pvs_le_gap_point_tabledomain. pvs_le_gap_point_tabledomain + (dst_index_point_table) = (0)) -> exists dst_positive_point_table dst_negative_point_table dst_value_point_table. ((((exists ff_h_pvs_point_tableentrypositive. ff_h_pvs_point_tableentrypositive + S (dst_positive_point_table) = S ((S (dst_index_point_table)) * dst_positive_scale_point_table)) /\ exists ff_q_pvs_point_tableentrypositive. dst_positive_code_point_table = ff_q_pvs_point_tableentrypositive * S ((S (dst_index_point_table)) * dst_positive_scale_point_table) + (dst_positive_point_table))) /\ (((((exists ff_h_pvs_point_tableentrynegative. ff_h_pvs_point_tableentrynegative + S (dst_negative_point_table) = S ((S (dst_index_point_table)) * dst_negative_scale_point_table)) /\ exists ff_q_pvs_point_tableentrynegative. dst_negative_code_point_table = ff_q_pvs_point_tableentrynegative * S ((S (dst_index_point_table)) * dst_negative_scale_point_table) + (dst_negative_point_table))) /\ (exists ge_balance_positive_point_tableentryvalue ge_balance_negative_point_tableentryvalue. (((((dst_value_point_table) = 2 * (ge_balance_positive_point_tableentryvalue) /\ (ge_balance_negative_point_tableentryvalue) = 0) \/ exists ge_signed_half_point_tableentryvaluedecode. (((dst_value_point_table) = 2 * ge_signed_half_point_tableentryvaluedecode + 1 /\ (ge_balance_positive_point_tableentryvalue) = 0) /\ (ge_balance_negative_point_tableentryvalue) = S ge_signed_half_point_tableentryvaluedecode))) /\ ((dst_positive_point_table) + ge_balance_negative_point_tableentryvalue = (dst_negative_point_table) + ge_balance_positive_point_tableentryvalue))))))))) -> (exists pvs_gap_point_bound. pvs_gap_point_bound + S (p) = (l)) -> (exists dst_positive_code_point_value dst_positive_scale_point_value dst_negative_code_point_value dst_negative_scale_point_value dst_positive_point_value dst_negative_point_value. (((F) = (((((dst_positive_code_point_value) + (dst_positive_scale_point_value)) * S ((dst_positive_code_point_value) + (dst_positive_scale_point_value)) + ((dst_positive_scale_point_value) + (dst_positive_scale_point_value))) + (((dst_negative_code_point_value) + (dst_negative_scale_point_value)) * S ((dst_negative_code_point_value) + (dst_negative_scale_point_value)) + ((dst_negative_scale_point_value) + (dst_negative_scale_point_value)))) * S ((((dst_positive_code_point_value) + (dst_positive_scale_point_value)) * S ((dst_positive_code_point_value) + (dst_positive_scale_point_value)) + ((dst_positive_scale_point_value) + (dst_positive_scale_point_value))) + (((dst_negative_code_point_value) + (dst_negative_scale_point_value)) * S ((dst_negative_code_point_value) + (dst_negative_scale_point_value)) + ((dst_negative_scale_point_value) + (dst_negative_scale_point_value)))) + ((((dst_negative_code_point_value) + (dst_negative_scale_point_value)) * S ((dst_negative_code_point_value) + (dst_negative_scale_point_value)) + ((dst_negative_scale_point_value) + (dst_negative_scale_point_value))) + (((dst_negative_code_point_value) + (dst_negative_scale_point_value)) * S ((dst_negative_code_point_value) + (dst_negative_scale_point_value)) + ((dst_negative_scale_point_value) + (dst_negative_scale_point_value)))))) /\ (((((exists ff_h_pvs_point_valuepositive. ff_h_pvs_point_valuepositive + S (dst_positive_point_value) = S ((S (p)) * dst_positive_scale_point_value)) /\ exists ff_q_pvs_point_valuepositive. dst_positive_code_point_value = ff_q_pvs_point_valuepositive * S ((S (p)) * dst_positive_scale_point_value) + (dst_positive_point_value))) /\ (((((exists ff_h_pvs_point_valuenegative. ff_h_pvs_point_valuenegative + S (dst_negative_point_value) = S ((S (p)) * dst_negative_scale_point_value)) /\ exists ff_q_pvs_point_valuenegative. dst_negative_code_point_value = ff_q_pvs_point_valuenegative * S ((S (p)) * dst_negative_scale_point_value) + (dst_negative_point_value))) /\ (exists ge_balance_positive_point_valuevalue ge_balance_negative_point_valuevalue. (((((a) = 2 * (ge_balance_positive_point_valuevalue) /\ (ge_balance_negative_point_valuevalue) = 0) \/ exists ge_signed_half_point_valuevaluedecode. (((a) = 2 * ge_signed_half_point_valuevaluedecode + 1 /\ (ge_balance_positive_point_valuevalue) = 0) /\ (ge_balance_negative_point_valuevalue) = S ge_signed_half_point_valuevaluedecode))) /\ ((dst_positive_point_value) + ge_balance_negative_point_valuevalue = (dst_negative_point_value) + ge_balance_positive_point_valuevalue))))))))) -> (forall ssr_spike_index_point_other ssr_spike_value_point_other. (exists pvs_gap_point_otherbound. pvs_gap_point_otherbound + S (ssr_spike_index_point_other) = (l)) -> ~(ssr_spike_index_point_other=(p)) -> (exists dst_positive_code_point_otherentry dst_positive_scale_point_otherentry dst_negative_code_point_otherentry dst_negative_scale_point_otherentry dst_positive_point_otherentry dst_negative_point_otherentry. (((F) = (((((dst_positive_code_point_otherentry) + (dst_positive_scale_point_otherentry)) * S ((dst_positive_code_point_otherentry) + (dst_positive_scale_point_otherentry)) + ((dst_positive_scale_point_otherentry) + (dst_positive_scale_point_otherentry))) + (((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) * S ((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) + ((dst_negative_scale_point_otherentry) + (dst_negative_scale_point_otherentry)))) * S ((((dst_positive_code_point_otherentry) + (dst_positive_scale_point_otherentry)) * S ((dst_positive_code_point_otherentry) + (dst_positive_scale_point_otherentry)) + ((dst_positive_scale_point_otherentry) + (dst_positive_scale_point_otherentry))) + (((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) * S ((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) + ((dst_negative_scale_point_otherentry) + (dst_negative_scale_point_otherentry)))) + ((((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) * S ((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) + ((dst_negative_scale_point_otherentry) + (dst_negative_scale_point_otherentry))) + (((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) * S ((dst_negative_code_point_otherentry) + (dst_negative_scale_point_otherentry)) + ((dst_negative_scale_point_otherentry) + (dst_negative_scale_point_otherentry)))))) /\ (((((exists ff_h_pvs_point_otherentrypositive. ff_h_pvs_point_otherentrypositive + S (dst_positive_point_otherentry) = S ((S (ssr_spike_index_point_other)) * dst_positive_scale_point_otherentry)) /\ exists ff_q_pvs_point_otherentrypositive. dst_positive_code_point_otherentry = ff_q_pvs_point_otherentrypositive * S ((S (ssr_spike_index_point_other)) * dst_positive_scale_point_otherentry) + (dst_positive_point_otherentry))) /\ (((((exists ff_h_pvs_point_otherentrynegative. ff_h_pvs_point_otherentrynegative + S (dst_negative_point_otherentry) = S ((S (ssr_spike_index_point_other)) * dst_negative_scale_point_otherentry)) /\ exists ff_q_pvs_point_otherentrynegative. dst_negative_code_point_otherentry = ff_q_pvs_point_otherentrynegative * S ((S (ssr_spike_index_point_other)) * dst_negative_scale_point_otherentry) + (dst_negative_point_otherentry))) /\ (exists ge_balance_positive_point_otherentryvalue ge_balance_negative_point_otherentryvalue. (((((ssr_spike_value_point_other) = 2 * (ge_balance_positive_point_otherentryvalue) /\ (ge_balance_negative_point_otherentryvalue) = 0) \/ exists ge_signed_half_point_otherentryvaluedecode. (((ssr_spike_value_point_other) = 2 * ge_signed_half_point_otherentryvaluedecode + 1 /\ (ge_balance_positive_point_otherentryvalue) = 0) /\ (ge_balance_negative_point_otherentryvalue) = S ge_signed_half_point_otherentryvaluedecode))) /\ ((dst_positive_point_otherentry) + ge_balance_negative_point_otherentryvalue = (dst_negative_point_otherentry) + ge_balance_positive_point_otherentryvalue))))))))) -> ssr_spike_value_point_other=0) -> (exists dst_positive_code_point_sum dst_positive_scale_point_sum dst_negative_code_point_sum dst_negative_scale_point_sum dst_positive_sum_point_sum dst_negative_sum_point_sum. (((F) = (((((dst_positive_code_point_sum) + (dst_positive_scale_point_sum)) * S ((dst_positive_code_point_sum) + (dst_positive_scale_point_sum)) + ((dst_positive_scale_point_sum) + (dst_positive_scale_point_sum))) + (((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) * S ((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) + ((dst_negative_scale_point_sum) + (dst_negative_scale_point_sum)))) * S ((((dst_positive_code_point_sum) + (dst_positive_scale_point_sum)) * S ((dst_positive_code_point_sum) + (dst_positive_scale_point_sum)) + ((dst_positive_scale_point_sum) + (dst_positive_scale_point_sum))) + (((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) * S ((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) + ((dst_negative_scale_point_sum) + (dst_negative_scale_point_sum)))) + ((((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) * S ((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) + ((dst_negative_scale_point_sum) + (dst_negative_scale_point_sum))) + (((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) * S ((dst_negative_code_point_sum) + (dst_negative_scale_point_sum)) + ((dst_negative_scale_point_sum) + (dst_negative_scale_point_sum)))))) /\ (((exists fs_u_dst_point_sumpositive fs_v_dst_point_sumpositive. ((((exists fs_h_dst_point_sumpositive_body_start. fs_h_dst_point_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_point_sumpositive)) /\ exists fs_q_dst_point_sumpositive_body_start. fs_u_dst_point_sumpositive = fs_q_dst_point_sumpositive_body_start * S ((S (0)) * fs_v_dst_point_sumpositive) + (0))) /\ ((((exists fs_h_dst_point_sumpositive_body_terminal. fs_h_dst_point_sumpositive_body_terminal + S (dst_positive_sum_point_sum) = S ((S (l)) * fs_v_dst_point_sumpositive)) /\ exists fs_q_dst_point_sumpositive_body_terminal. fs_u_dst_point_sumpositive = fs_q_dst_point_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_point_sumpositive) + (dst_positive_sum_point_sum))) /\ forall fs_i_dst_point_sumpositive_body_steps. (exists fs_lt_dst_point_sumpositive_body_steps_bound. fs_lt_dst_point_sumpositive_body_steps_bound + S fs_i_dst_point_sumpositive_body_steps = l) -> exists fs_a_dst_point_sumpositive_body_steps fs_r_dst_point_sumpositive_body_steps fs_s_dst_point_sumpositive_body_steps. ((((exists fs_h_dst_point_sumpositive_body_steps_summand. fs_h_dst_point_sumpositive_body_steps_summand + S (fs_a_dst_point_sumpositive_body_steps) = S ((S (fs_i_dst_point_sumpositive_body_steps)) * dst_positive_scale_point_sum)) /\ exists fs_q_dst_point_sumpositive_body_steps_summand. dst_positive_code_point_sum = fs_q_dst_point_sumpositive_body_steps_summand * S ((S (fs_i_dst_point_sumpositive_body_steps)) * dst_positive_scale_point_sum) + (fs_a_dst_point_sumpositive_body_steps))) /\ ((((exists fs_h_dst_point_sumpositive_body_steps_partial. fs_h_dst_point_sumpositive_body_steps_partial + S (fs_r_dst_point_sumpositive_body_steps) = S ((S (fs_i_dst_point_sumpositive_body_steps)) * fs_v_dst_point_sumpositive)) /\ exists fs_q_dst_point_sumpositive_body_steps_partial. fs_u_dst_point_sumpositive = fs_q_dst_point_sumpositive_body_steps_partial * S ((S (fs_i_dst_point_sumpositive_body_steps)) * fs_v_dst_point_sumpositive) + (fs_r_dst_point_sumpositive_body_steps))) /\ ((((exists fs_h_dst_point_sumpositive_body_steps_successor. fs_h_dst_point_sumpositive_body_steps_successor + S (fs_s_dst_point_sumpositive_body_steps) = S ((S (S fs_i_dst_point_sumpositive_body_steps)) * fs_v_dst_point_sumpositive)) /\ exists fs_q_dst_point_sumpositive_body_steps_successor. fs_u_dst_point_sumpositive = fs_q_dst_point_sumpositive_body_steps_successor * S ((S (S fs_i_dst_point_sumpositive_body_steps)) * fs_v_dst_point_sumpositive) + (fs_s_dst_point_sumpositive_body_steps))) /\ fs_s_dst_point_sumpositive_body_steps = fs_r_dst_point_sumpositive_body_steps + fs_a_dst_point_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_point_sumnegative fs_v_dst_point_sumnegative. ((((exists fs_h_dst_point_sumnegative_body_start. fs_h_dst_point_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_point_sumnegative)) /\ exists fs_q_dst_point_sumnegative_body_start. fs_u_dst_point_sumnegative = fs_q_dst_point_sumnegative_body_start * S ((S (0)) * fs_v_dst_point_sumnegative) + (0))) /\ ((((exists fs_h_dst_point_sumnegative_body_terminal. fs_h_dst_point_sumnegative_body_terminal + S (dst_negative_sum_point_sum) = S ((S (l)) * fs_v_dst_point_sumnegative)) /\ exists fs_q_dst_point_sumnegative_body_terminal. fs_u_dst_point_sumnegative = fs_q_dst_point_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_point_sumnegative) + (dst_negative_sum_point_sum))) /\ forall fs_i_dst_point_sumnegative_body_steps. (exists fs_lt_dst_point_sumnegative_body_steps_bound. fs_lt_dst_point_sumnegative_body_steps_bound + S fs_i_dst_point_sumnegative_body_steps = l) -> exists fs_a_dst_point_sumnegative_body_steps fs_r_dst_point_sumnegative_body_steps fs_s_dst_point_sumnegative_body_steps. ((((exists fs_h_dst_point_sumnegative_body_steps_summand. fs_h_dst_point_sumnegative_body_steps_summand + S (fs_a_dst_point_sumnegative_body_steps) = S ((S (fs_i_dst_point_sumnegative_body_steps)) * dst_negative_scale_point_sum)) /\ exists fs_q_dst_point_sumnegative_body_steps_summand. dst_negative_code_point_sum = fs_q_dst_point_sumnegative_body_steps_summand * S ((S (fs_i_dst_point_sumnegative_body_steps)) * dst_negative_scale_point_sum) + (fs_a_dst_point_sumnegative_body_steps))) /\ ((((exists fs_h_dst_point_sumnegative_body_steps_partial. fs_h_dst_point_sumnegative_body_steps_partial + S (fs_r_dst_point_sumnegative_body_steps) = S ((S (fs_i_dst_point_sumnegative_body_steps)) * fs_v_dst_point_sumnegative)) /\ exists fs_q_dst_point_sumnegative_body_steps_partial. fs_u_dst_point_sumnegative = fs_q_dst_point_sumnegative_body_steps_partial * S ((S (fs_i_dst_point_sumnegative_body_steps)) * fs_v_dst_point_sumnegative) + (fs_r_dst_point_sumnegative_body_steps))) /\ ((((exists fs_h_dst_point_sumnegative_body_steps_successor. fs_h_dst_point_sumnegative_body_steps_successor + S (fs_s_dst_point_sumnegative_body_steps) = S ((S (S fs_i_dst_point_sumnegative_body_steps)) * fs_v_dst_point_sumnegative)) /\ exists fs_q_dst_point_sumnegative_body_steps_successor. fs_u_dst_point_sumnegative = fs_q_dst_point_sumnegative_body_steps_successor * S ((S (S fs_i_dst_point_sumnegative_body_steps)) * fs_v_dst_point_sumnegative) + (fs_s_dst_point_sumnegative_body_steps))) /\ fs_s_dst_point_sumnegative_body_steps = fs_r_dst_point_sumnegative_body_steps + fs_a_dst_point_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_point_sumresult ge_balance_negative_point_sumresult. (((((z) = 2 * (ge_balance_positive_point_sumresult) /\ (ge_balance_negative_point_sumresult) = 0) \/ exists ge_signed_half_point_sumresultdecode. (((z) = 2 * ge_signed_half_point_sumresultdecode + 1 /\ (ge_balance_positive_point_sumresult) = 0) /\ (ge_balance_negative_point_sumresult) = S ge_signed_half_point_sumresultdecode))) /\ ((dst_positive_sum_point_sum) + ge_balance_negative_point_sumresult = (dst_negative_sum_point_sum) + ge_balance_positive_point_sumresult))))))))) -> z=a