ZS0007

signed_prefix_sum_last_value

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

If a prefix is zero, its next actual sum is precisely the actual last entry, including the l=0 boundary.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall F l a z. (forall sfs_index_last_zeros sfs_value_last_zeros. (exists pvs_le_gap_last_zeroslower. pvs_le_gap_last_zeroslower + (0) = (sfs_index_last_zeros)) -> (exists pvs_gap_last_zerosupper. pvs_gap_last_zerosupper + S (sfs_index_last_zeros) = (l)) -> (exists dst_positive_code_last_zerosentry dst_positive_scale_last_zerosentry dst_negative_code_last_zerosentry dst_negative_scale_last_zerosentry dst_positive_last_zerosentry dst_negative_last_zerosentry. (((F) = (((((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) * S ((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) + ((dst_positive_scale_last_zerosentry) + (dst_positive_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))) * S ((((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) * S ((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) + ((dst_positive_scale_last_zerosentry) + (dst_positive_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))) + ((((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))))) /\ (((((exists ff_h_pvs_last_zerosentrypositive. ff_h_pvs_last_zerosentrypositive + S (dst_positive_last_zerosentry) = S ((S (sfs_index_last_zeros)) * dst_positive_scale_last_zerosentry)) /\ exists ff_q_pvs_last_zerosentrypositive. dst_positive_code_last_zerosentry = ff_q_pvs_last_zerosentrypositive * S ((S (sfs_index_last_zeros)) * dst_positive_scale_last_zerosentry) + (dst_positive_last_zerosentry))) /\ (((((exists ff_h_pvs_last_zerosentrynegative. ff_h_pvs_last_zerosentrynegative + S (dst_negative_last_zerosentry) = S ((S (sfs_index_last_zeros)) * dst_negative_scale_last_zerosentry)) /\ exists ff_q_pvs_last_zerosentrynegative. dst_negative_code_last_zerosentry = ff_q_pvs_last_zerosentrynegative * S ((S (sfs_index_last_zeros)) * dst_negative_scale_last_zerosentry) + (dst_negative_last_zerosentry))) /\ (exists ge_balance_positive_last_zerosentryvalue ge_balance_negative_last_zerosentryvalue. (((((sfs_value_last_zeros) = 2 * (ge_balance_positive_last_zerosentryvalue) /\ (ge_balance_negative_last_zerosentryvalue) = 0) \/ exists ge_signed_half_last_zerosentryvaluedecode. (((sfs_value_last_zeros) = 2 * ge_signed_half_last_zerosentryvaluedecode + 1 /\ (ge_balance_positive_last_zerosentryvalue) = 0) /\ (ge_balance_negative_last_zerosentryvalue) = S ge_signed_half_last_zerosentryvaluedecode))) /\ ((dst_positive_last_zerosentry) + ge_balance_negative_last_zerosentryvalue = (dst_negative_last_zerosentry) + ge_balance_positive_last_zerosentryvalue))))))))) -> sfs_value_last_zeros=0) -> (exists dst_positive_code_last_value dst_positive_scale_last_value dst_negative_code_last_value dst_negative_scale_last_value dst_positive_last_value dst_negative_last_value. (((F) = (((((dst_positive_code_last_value) + (dst_positive_scale_last_value)) * S ((dst_positive_code_last_value) + (dst_positive_scale_last_value)) + ((dst_positive_scale_last_value) + (dst_positive_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))) * S ((((dst_positive_code_last_value) + (dst_positive_scale_last_value)) * S ((dst_positive_code_last_value) + (dst_positive_scale_last_value)) + ((dst_positive_scale_last_value) + (dst_positive_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))) + ((((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))))) /\ (((((exists ff_h_pvs_last_valuepositive. ff_h_pvs_last_valuepositive + S (dst_positive_last_value) = S ((S (l)) * dst_positive_scale_last_value)) /\ exists ff_q_pvs_last_valuepositive. dst_positive_code_last_value = ff_q_pvs_last_valuepositive * S ((S (l)) * dst_positive_scale_last_value) + (dst_positive_last_value))) /\ (((((exists ff_h_pvs_last_valuenegative. ff_h_pvs_last_valuenegative + S (dst_negative_last_value) = S ((S (l)) * dst_negative_scale_last_value)) /\ exists ff_q_pvs_last_valuenegative. dst_negative_code_last_value = ff_q_pvs_last_valuenegative * S ((S (l)) * dst_negative_scale_last_value) + (dst_negative_last_value))) /\ (exists ge_balance_positive_last_valuevalue ge_balance_negative_last_valuevalue. (((((a) = 2 * (ge_balance_positive_last_valuevalue) /\ (ge_balance_negative_last_valuevalue) = 0) \/ exists ge_signed_half_last_valuevaluedecode. (((a) = 2 * ge_signed_half_last_valuevaluedecode + 1 /\ (ge_balance_positive_last_valuevalue) = 0) /\ (ge_balance_negative_last_valuevalue) = S ge_signed_half_last_valuevaluedecode))) /\ ((dst_positive_last_value) + ge_balance_negative_last_valuevalue = (dst_negative_last_value) + ge_balance_positive_last_valuevalue))))))))) -> (exists dst_positive_code_last_sum dst_positive_scale_last_sum dst_negative_code_last_sum dst_negative_scale_last_sum dst_positive_sum_last_sum dst_negative_sum_last_sum. (((F) = (((((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) * S ((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) + ((dst_positive_scale_last_sum) + (dst_positive_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))) * S ((((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) * S ((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) + ((dst_positive_scale_last_sum) + (dst_positive_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))) + ((((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))))) /\ (((exists fs_u_dst_last_sumpositive fs_v_dst_last_sumpositive. ((((exists fs_h_dst_last_sumpositive_body_start. fs_h_dst_last_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_start. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_start * S ((S (0)) * fs_v_dst_last_sumpositive) + (0))) /\ ((((exists fs_h_dst_last_sumpositive_body_terminal. fs_h_dst_last_sumpositive_body_terminal + S (dst_positive_sum_last_sum) = S ((S (S l)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_terminal. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_terminal * S ((S (S l)) * fs_v_dst_last_sumpositive) + (dst_positive_sum_last_sum))) /\ forall fs_i_dst_last_sumpositive_body_steps. (exists fs_lt_dst_last_sumpositive_body_steps_bound. fs_lt_dst_last_sumpositive_body_steps_bound + S fs_i_dst_last_sumpositive_body_steps = S l) -> exists fs_a_dst_last_sumpositive_body_steps fs_r_dst_last_sumpositive_body_steps fs_s_dst_last_sumpositive_body_steps. ((((exists fs_h_dst_last_sumpositive_body_steps_summand. fs_h_dst_last_sumpositive_body_steps_summand + S (fs_a_dst_last_sumpositive_body_steps) = S ((S (fs_i_dst_last_sumpositive_body_steps)) * dst_positive_scale_last_sum)) /\ exists fs_q_dst_last_sumpositive_body_steps_summand. dst_positive_code_last_sum = fs_q_dst_last_sumpositive_body_steps_summand * S ((S (fs_i_dst_last_sumpositive_body_steps)) * dst_positive_scale_last_sum) + (fs_a_dst_last_sumpositive_body_steps))) /\ ((((exists fs_h_dst_last_sumpositive_body_steps_partial. fs_h_dst_last_sumpositive_body_steps_partial + S (fs_r_dst_last_sumpositive_body_steps) = S ((S (fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_steps_partial. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_steps_partial * S ((S (fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive) + (fs_r_dst_last_sumpositive_body_steps))) /\ ((((exists fs_h_dst_last_sumpositive_body_steps_successor. fs_h_dst_last_sumpositive_body_steps_successor + S (fs_s_dst_last_sumpositive_body_steps) = S ((S (S fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_steps_successor. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_steps_successor * S ((S (S fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive) + (fs_s_dst_last_sumpositive_body_steps))) /\ fs_s_dst_last_sumpositive_body_steps = fs_r_dst_last_sumpositive_body_steps + fs_a_dst_last_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_last_sumnegative fs_v_dst_last_sumnegative. ((((exists fs_h_dst_last_sumnegative_body_start. fs_h_dst_last_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_start. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_start * S ((S (0)) * fs_v_dst_last_sumnegative) + (0))) /\ ((((exists fs_h_dst_last_sumnegative_body_terminal. fs_h_dst_last_sumnegative_body_terminal + S (dst_negative_sum_last_sum) = S ((S (S l)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_terminal. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_terminal * S ((S (S l)) * fs_v_dst_last_sumnegative) + (dst_negative_sum_last_sum))) /\ forall fs_i_dst_last_sumnegative_body_steps. (exists fs_lt_dst_last_sumnegative_body_steps_bound. fs_lt_dst_last_sumnegative_body_steps_bound + S fs_i_dst_last_sumnegative_body_steps = S l) -> exists fs_a_dst_last_sumnegative_body_steps fs_r_dst_last_sumnegative_body_steps fs_s_dst_last_sumnegative_body_steps. ((((exists fs_h_dst_last_sumnegative_body_steps_summand. fs_h_dst_last_sumnegative_body_steps_summand + S (fs_a_dst_last_sumnegative_body_steps) = S ((S (fs_i_dst_last_sumnegative_body_steps)) * dst_negative_scale_last_sum)) /\ exists fs_q_dst_last_sumnegative_body_steps_summand. dst_negative_code_last_sum = fs_q_dst_last_sumnegative_body_steps_summand * S ((S (fs_i_dst_last_sumnegative_body_steps)) * dst_negative_scale_last_sum) + (fs_a_dst_last_sumnegative_body_steps))) /\ ((((exists fs_h_dst_last_sumnegative_body_steps_partial. fs_h_dst_last_sumnegative_body_steps_partial + S (fs_r_dst_last_sumnegative_body_steps) = S ((S (fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_steps_partial. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_steps_partial * S ((S (fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative) + (fs_r_dst_last_sumnegative_body_steps))) /\ ((((exists fs_h_dst_last_sumnegative_body_steps_successor. fs_h_dst_last_sumnegative_body_steps_successor + S (fs_s_dst_last_sumnegative_body_steps) = S ((S (S fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_steps_successor. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_steps_successor * S ((S (S fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative) + (fs_s_dst_last_sumnegative_body_steps))) /\ fs_s_dst_last_sumnegative_body_steps = fs_r_dst_last_sumnegative_body_steps + fs_a_dst_last_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_last_sumresult ge_balance_negative_last_sumresult. (((((z) = 2 * (ge_balance_positive_last_sumresult) /\ (ge_balance_negative_last_sumresult) = 0) \/ exists ge_signed_half_last_sumresultdecode. (((z) = 2 * ge_signed_half_last_sumresultdecode + 1 /\ (ge_balance_positive_last_sumresult) = 0) /\ (ge_balance_negative_last_sumresult) = S ge_signed_half_last_sumresultdecode))) /\ ((dst_positive_sum_last_sum) + ge_balance_negative_last_sumresult = (dst_negative_sum_last_sum) + ge_balance_positive_last_sumresult))))))))) -> z=a

Constructive proof overview

Generated structural guide

If a prefix is zero, its next actual sum is precisely the actual last entry, including the l=0 boundary.

The unchanged tactic script uses 5 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

divisor_signed_sum_successor_decompose Alpha theorem; checked-use authorized ZS0005 signed_prefix_sum_zero_value divisor_signed_table_at_functional Alpha theorem; checked-use authorized signed_add_functional Alpha theorem; checked-use authorized signed_add_zero_left Alpha theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

44 script commands · 7 reading checkpoints · 3 local claims

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

Named ingredients (1)
signed prefix sum zero value

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro a
  4. L4
    intro z
  5. L5
    intro hz
  6. L6
    intro ha
  7. L7
    intro hs
02Establish hdL8–13

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

  1. L8
    have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,z))Definitions: SignedAddArithAtSignedPrefixSum
  2. L9
    specialize divisor_signed_sum_successor_decompose (F)
  3. L10
    specialize divisor_signed_sum_successor_decompose (l)
  4. L11
    specialize divisor_signed_sum_successor_decompose (z)
  5. L12
    apply divisor_signed_sum_successor_decompose
  6. L13
    exact hs
03Separate the logical casesL14–17

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

  1. L14
    cases hd
  2. L15
    cases hd_witness
  3. L16
    cases hd_witness_witness
  4. L17
    cases hd_witness_witness_right
04Establish hpL18–24

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

  1. L18
    have hp : x=0
  2. L19
    specialize signed_prefix_sum_zero_value (F)
  3. L20
    specialize signed_prefix_sum_zero_value (l)
  4. L21
    specialize signed_prefix_sum_zero_value (x)
  5. L22
    apply signed_prefix_sum_zero_value
  6. L23
    exact hz
  7. L24
    exact hd_witness_witness_left
05Establish heL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L25
    have he : x1=a
  2. L26
    specialize divisor_signed_table_at_functional (F)
  3. L27
    specialize divisor_signed_table_at_functional (l)
  4. L28
    specialize divisor_signed_table_at_functional (x1)
  5. L29
    specialize divisor_signed_table_at_functional (a)
  6. L30
    apply divisor_signed_table_at_functional
  7. L31
    exact hd_witness_witness_right_left
  8. L32
    exact ha
  9. L33
    rewrite hp at hd_witness_witness_right_right
  10. L34
    rewrite hp at hd_witness_witness_right_right
06Calculate and transport equalitiesL35–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L35
    rewrite he at hd_witness_witness_right_right
  2. L36
    rewrite he at hd_witness_witness_right_right
07Use earlier factsL37–44

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

  1. L37
    specialize signed_add_functional (0)
  2. L38
    specialize signed_add_functional (a)
  3. L39
    specialize signed_add_functional (z)
  4. L40
    specialize signed_add_functional (a)
  5. L41
    apply signed_add_functional
  6. L42
    exact hd_witness_witness_right_right
  7. L43
    specialize signed_add_zero_left (a)
  8. L44
    apply signed_add_zero_left

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro a
  4. 0004intro z
  5. 0005intro hz
  6. 0006intro ha
  7. 0007intro hs
  8. 0008have hd : exists u v. (((exists dst_positive_code_last_prefix dst_positive_scale_last_prefix dst_negative_code_last_prefix dst_negative_scale_last_prefix dst_positive_sum_last_prefix dst_negative_sum_last_prefix. (((F) = (((((dst_positive_code_last_prefix) + (dst_positive_scale_last_prefix)) * S ((dst_positive_code_last_prefix) + (dst_positive_scale_last_prefix)) + ((dst_positive_scale_last_prefix) + (dst_positive_scale_last_prefix))) + (((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) * S ((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) + ((dst_negative_scale_last_prefix) + (dst_negative_scale_last_prefix)))) * S ((((dst_positive_code_last_prefix) + (dst_positive_scale_last_prefix)) * S ((dst_positive_code_last_prefix) + (dst_positive_scale_last_prefix)) + ((dst_positive_scale_last_prefix) + (dst_positive_scale_last_prefix))) + (((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) * S ((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) + ((dst_negative_scale_last_prefix) + (dst_negative_scale_last_prefix)))) + ((((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) * S ((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) + ((dst_negative_scale_last_prefix) + (dst_negative_scale_last_prefix))) + (((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) * S ((dst_negative_code_last_prefix) + (dst_negative_scale_last_prefix)) + ((dst_negative_scale_last_prefix) + (dst_negative_scale_last_prefix)))))) /\ (((exists fs_u_dst_last_prefixpositive fs_v_dst_last_prefixpositive. ((((exists fs_h_dst_last_prefixpositive_body_start. fs_h_dst_last_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_last_prefixpositive)) /\ exists fs_q_dst_last_prefixpositive_body_start. fs_u_dst_last_prefixpositive = fs_q_dst_last_prefixpositive_body_start * S ((S (0)) * fs_v_dst_last_prefixpositive) + (0))) /\ ((((exists fs_h_dst_last_prefixpositive_body_terminal. fs_h_dst_last_prefixpositive_body_terminal + S (dst_positive_sum_last_prefix) = S ((S (l)) * fs_v_dst_last_prefixpositive)) /\ exists fs_q_dst_last_prefixpositive_body_terminal. fs_u_dst_last_prefixpositive = fs_q_dst_last_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_last_prefixpositive) + (dst_positive_sum_last_prefix))) /\ forall fs_i_dst_last_prefixpositive_body_steps. (exists fs_lt_dst_last_prefixpositive_body_steps_bound. fs_lt_dst_last_prefixpositive_body_steps_bound + S fs_i_dst_last_prefixpositive_body_steps = l) -> exists fs_a_dst_last_prefixpositive_body_steps fs_r_dst_last_prefixpositive_body_steps fs_s_dst_last_prefixpositive_body_steps. ((((exists fs_h_dst_last_prefixpositive_body_steps_summand. fs_h_dst_last_prefixpositive_body_steps_summand + S (fs_a_dst_last_prefixpositive_body_steps) = S ((S (fs_i_dst_last_prefixpositive_body_steps)) * dst_positive_scale_last_prefix)) /\ exists fs_q_dst_last_prefixpositive_body_steps_summand. dst_positive_code_last_prefix = fs_q_dst_last_prefixpositive_body_steps_summand * S ((S (fs_i_dst_last_prefixpositive_body_steps)) * dst_positive_scale_last_prefix) + (fs_a_dst_last_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_last_prefixpositive_body_steps_partial. fs_h_dst_last_prefixpositive_body_steps_partial + S (fs_r_dst_last_prefixpositive_body_steps) = S ((S (fs_i_dst_last_prefixpositive_body_steps)) * fs_v_dst_last_prefixpositive)) /\ exists fs_q_dst_last_prefixpositive_body_steps_partial. fs_u_dst_last_prefixpositive = fs_q_dst_last_prefixpositive_body_steps_partial * S ((S (fs_i_dst_last_prefixpositive_body_steps)) * fs_v_dst_last_prefixpositive) + (fs_r_dst_last_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_last_prefixpositive_body_steps_successor. fs_h_dst_last_prefixpositive_body_steps_successor + S (fs_s_dst_last_prefixpositive_body_steps) = S ((S (S fs_i_dst_last_prefixpositive_body_steps)) * fs_v_dst_last_prefixpositive)) /\ exists fs_q_dst_last_prefixpositive_body_steps_successor. fs_u_dst_last_prefixpositive = fs_q_dst_last_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_last_prefixpositive_body_steps)) * fs_v_dst_last_prefixpositive) + (fs_s_dst_last_prefixpositive_body_steps))) /\ fs_s_dst_last_prefixpositive_body_steps = fs_r_dst_last_prefixpositive_body_steps + fs_a_dst_last_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_last_prefixnegative fs_v_dst_last_prefixnegative. ((((exists fs_h_dst_last_prefixnegative_body_start. fs_h_dst_last_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_last_prefixnegative)) /\ exists fs_q_dst_last_prefixnegative_body_start. fs_u_dst_last_prefixnegative = fs_q_dst_last_prefixnegative_body_start * S ((S (0)) * fs_v_dst_last_prefixnegative) + (0))) /\ ((((exists fs_h_dst_last_prefixnegative_body_terminal. fs_h_dst_last_prefixnegative_body_terminal + S (dst_negative_sum_last_prefix) = S ((S (l)) * fs_v_dst_last_prefixnegative)) /\ exists fs_q_dst_last_prefixnegative_body_terminal. fs_u_dst_last_prefixnegative = fs_q_dst_last_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_last_prefixnegative) + (dst_negative_sum_last_prefix))) /\ forall fs_i_dst_last_prefixnegative_body_steps. (exists fs_lt_dst_last_prefixnegative_body_steps_bound. fs_lt_dst_last_prefixnegative_body_steps_bound + S fs_i_dst_last_prefixnegative_body_steps = l) -> exists fs_a_dst_last_prefixnegative_body_steps fs_r_dst_last_prefixnegative_body_steps fs_s_dst_last_prefixnegative_body_steps. ((((exists fs_h_dst_last_prefixnegative_body_steps_summand. fs_h_dst_last_prefixnegative_body_steps_summand + S (fs_a_dst_last_prefixnegative_body_steps) = S ((S (fs_i_dst_last_prefixnegative_body_steps)) * dst_negative_scale_last_prefix)) /\ exists fs_q_dst_last_prefixnegative_body_steps_summand. dst_negative_code_last_prefix = fs_q_dst_last_prefixnegative_body_steps_summand * S ((S (fs_i_dst_last_prefixnegative_body_steps)) * dst_negative_scale_last_prefix) + (fs_a_dst_last_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_last_prefixnegative_body_steps_partial. fs_h_dst_last_prefixnegative_body_steps_partial + S (fs_r_dst_last_prefixnegative_body_steps) = S ((S (fs_i_dst_last_prefixnegative_body_steps)) * fs_v_dst_last_prefixnegative)) /\ exists fs_q_dst_last_prefixnegative_body_steps_partial. fs_u_dst_last_prefixnegative = fs_q_dst_last_prefixnegative_body_steps_partial * S ((S (fs_i_dst_last_prefixnegative_body_steps)) * fs_v_dst_last_prefixnegative) + (fs_r_dst_last_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_last_prefixnegative_body_steps_successor. fs_h_dst_last_prefixnegative_body_steps_successor + S (fs_s_dst_last_prefixnegative_body_steps) = S ((S (S fs_i_dst_last_prefixnegative_body_steps)) * fs_v_dst_last_prefixnegative)) /\ exists fs_q_dst_last_prefixnegative_body_steps_successor. fs_u_dst_last_prefixnegative = fs_q_dst_last_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_last_prefixnegative_body_steps)) * fs_v_dst_last_prefixnegative) + (fs_s_dst_last_prefixnegative_body_steps))) /\ fs_s_dst_last_prefixnegative_body_steps = fs_r_dst_last_prefixnegative_body_steps + fs_a_dst_last_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_last_prefixresult ge_balance_negative_last_prefixresult. (((((u) = 2 * (ge_balance_positive_last_prefixresult) /\ (ge_balance_negative_last_prefixresult) = 0) \/ exists ge_signed_half_last_prefixresultdecode. (((u) = 2 * ge_signed_half_last_prefixresultdecode + 1 /\ (ge_balance_positive_last_prefixresult) = 0) /\ (ge_balance_negative_last_prefixresult) = S ge_signed_half_last_prefixresultdecode))) /\ ((dst_positive_sum_last_prefix) + ge_balance_negative_last_prefixresult = (dst_negative_sum_last_prefix) + ge_balance_positive_last_prefixresult))))))))) /\ (((exists dst_positive_code_last_entry dst_positive_scale_last_entry dst_negative_code_last_entry dst_negative_scale_last_entry dst_positive_last_entry dst_negative_last_entry. (((F) = (((((dst_positive_code_last_entry) + (dst_positive_scale_last_entry)) * S ((dst_positive_code_last_entry) + (dst_positive_scale_last_entry)) + ((dst_positive_scale_last_entry) + (dst_positive_scale_last_entry))) + (((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) * S ((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) + ((dst_negative_scale_last_entry) + (dst_negative_scale_last_entry)))) * S ((((dst_positive_code_last_entry) + (dst_positive_scale_last_entry)) * S ((dst_positive_code_last_entry) + (dst_positive_scale_last_entry)) + ((dst_positive_scale_last_entry) + (dst_positive_scale_last_entry))) + (((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) * S ((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) + ((dst_negative_scale_last_entry) + (dst_negative_scale_last_entry)))) + ((((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) * S ((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) + ((dst_negative_scale_last_entry) + (dst_negative_scale_last_entry))) + (((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) * S ((dst_negative_code_last_entry) + (dst_negative_scale_last_entry)) + ((dst_negative_scale_last_entry) + (dst_negative_scale_last_entry)))))) /\ (((((exists ff_h_pvs_last_entrypositive. ff_h_pvs_last_entrypositive + S (dst_positive_last_entry) = S ((S (l)) * dst_positive_scale_last_entry)) /\ exists ff_q_pvs_last_entrypositive. dst_positive_code_last_entry = ff_q_pvs_last_entrypositive * S ((S (l)) * dst_positive_scale_last_entry) + (dst_positive_last_entry))) /\ (((((exists ff_h_pvs_last_entrynegative. ff_h_pvs_last_entrynegative + S (dst_negative_last_entry) = S ((S (l)) * dst_negative_scale_last_entry)) /\ exists ff_q_pvs_last_entrynegative. dst_negative_code_last_entry = ff_q_pvs_last_entrynegative * S ((S (l)) * dst_negative_scale_last_entry) + (dst_negative_last_entry))) /\ (exists ge_balance_positive_last_entryvalue ge_balance_negative_last_entryvalue. (((((v) = 2 * (ge_balance_positive_last_entryvalue) /\ (ge_balance_negative_last_entryvalue) = 0) \/ exists ge_signed_half_last_entryvaluedecode. (((v) = 2 * ge_signed_half_last_entryvaluedecode + 1 /\ (ge_balance_positive_last_entryvalue) = 0) /\ (ge_balance_negative_last_entryvalue) = S ge_signed_half_last_entryvaluedecode))) /\ ((dst_positive_last_entry) + ge_balance_negative_last_entryvalue = (dst_negative_last_entry) + ge_balance_positive_last_entryvalue))))))))) /\ (exists dsa_ap_last_add dsa_an_last_add dsa_bp_last_add dsa_bn_last_add dsa_cp_last_add dsa_cn_last_add. (((((u) = 2 * (dsa_ap_last_add) /\ (dsa_an_last_add) = 0) \/ exists ge_signed_half_last_addleft. (((u) = 2 * ge_signed_half_last_addleft + 1 /\ (dsa_ap_last_add) = 0) /\ (dsa_an_last_add) = S ge_signed_half_last_addleft))) /\ ((((((v) = 2 * (dsa_bp_last_add) /\ (dsa_bn_last_add) = 0) \/ exists ge_signed_half_last_addright. (((v) = 2 * ge_signed_half_last_addright + 1 /\ (dsa_bp_last_add) = 0) /\ (dsa_bn_last_add) = S ge_signed_half_last_addright))) /\ ((((((z) = 2 * (dsa_cp_last_add) /\ (dsa_cn_last_add) = 0) \/ exists ge_signed_half_last_addoutput. (((z) = 2 * ge_signed_half_last_addoutput + 1 /\ (dsa_cp_last_add) = 0) /\ (dsa_cn_last_add) = S ge_signed_half_last_addoutput))) /\ ((dsa_ap_last_add + dsa_bp_last_add) + dsa_cn_last_add = (dsa_an_last_add + dsa_bn_last_add) + dsa_cp_last_add)))))))))))
  9. 0009specialize divisor_signed_sum_successor_decompose (F)
  10. 0010specialize divisor_signed_sum_successor_decompose (l)
  11. 0011specialize divisor_signed_sum_successor_decompose (z)
  12. 0012apply divisor_signed_sum_successor_decompose
  13. 0013exact hs
  14. 0014cases hd
  15. 0015cases hd_witness
  16. 0016cases hd_witness_witness
  17. 0017cases hd_witness_witness_right
  18. 0018have hp : x=0
  19. 0019specialize signed_prefix_sum_zero_value (F)
  20. 0020specialize signed_prefix_sum_zero_value (l)
  21. 0021specialize signed_prefix_sum_zero_value (x)
  22. 0022apply signed_prefix_sum_zero_value
  23. 0023exact hz
  24. 0024exact hd_witness_witness_left
  25. 0025have he : x1=a
  26. 0026specialize divisor_signed_table_at_functional (F)
  27. 0027specialize divisor_signed_table_at_functional (l)
  28. 0028specialize divisor_signed_table_at_functional (x1)
  29. 0029specialize divisor_signed_table_at_functional (a)
  30. 0030apply divisor_signed_table_at_functional
  31. 0031exact hd_witness_witness_right_left
  32. 0032exact ha
  33. 0033rewrite hp at hd_witness_witness_right_right
  34. 0034rewrite hp at hd_witness_witness_right_right
  35. 0035rewrite he at hd_witness_witness_right_right
  36. 0036rewrite he at hd_witness_witness_right_right
  37. 0037specialize signed_add_functional (0)
  38. 0038specialize signed_add_functional (a)
  39. 0039specialize signed_add_functional (z)
  40. 0040specialize signed_add_functional (a)
  41. 0041apply signed_add_functional
  42. 0042exact hd_witness_witness_right_right
  43. 0043specialize signed_add_zero_left (a)
  44. 0044apply signed_add_zero_left