ZS0004

signed_prefix_sum_zero_tail

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

Ordinary finite induction proves that a genuinely zero tail changes no actual canonical signed prefix sum.

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 k l a b. (exists pvs_le_gap_tail_order. pvs_le_gap_tail_order + (k) = (l)) -> (forall sfs_index_tail_window sfs_value_tail_window. (exists pvs_le_gap_tail_windowlower. pvs_le_gap_tail_windowlower + (k) = (sfs_index_tail_window)) -> (exists pvs_gap_tail_windowupper. pvs_gap_tail_windowupper + S (sfs_index_tail_window) = (l)) -> (exists dst_positive_code_tail_windowentry dst_positive_scale_tail_windowentry dst_negative_code_tail_windowentry dst_negative_scale_tail_windowentry dst_positive_tail_windowentry dst_negative_tail_windowentry. (((F) = (((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) * S ((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) + ((((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))))) /\ (((((exists ff_h_pvs_tail_windowentrypositive. ff_h_pvs_tail_windowentrypositive + S (dst_positive_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrypositive. dst_positive_code_tail_windowentry = ff_q_pvs_tail_windowentrypositive * S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry) + (dst_positive_tail_windowentry))) /\ (((((exists ff_h_pvs_tail_windowentrynegative. ff_h_pvs_tail_windowentrynegative + S (dst_negative_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrynegative. dst_negative_code_tail_windowentry = ff_q_pvs_tail_windowentrynegative * S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry) + (dst_negative_tail_windowentry))) /\ (exists ge_balance_positive_tail_windowentryvalue ge_balance_negative_tail_windowentryvalue. (((((sfs_value_tail_window) = 2 * (ge_balance_positive_tail_windowentryvalue) /\ (ge_balance_negative_tail_windowentryvalue) = 0) \/ exists ge_signed_half_tail_windowentryvaluedecode. (((sfs_value_tail_window) = 2 * ge_signed_half_tail_windowentryvaluedecode + 1 /\ (ge_balance_positive_tail_windowentryvalue) = 0) /\ (ge_balance_negative_tail_windowentryvalue) = S ge_signed_half_tail_windowentryvaluedecode))) /\ ((dst_positive_tail_windowentry) + ge_balance_negative_tail_windowentryvalue = (dst_negative_tail_windowentry) + ge_balance_positive_tail_windowentryvalue))))))))) -> sfs_value_tail_window=0) -> (exists dst_positive_code_tail_short dst_positive_scale_tail_short dst_negative_code_tail_short dst_negative_scale_tail_short dst_positive_sum_tail_short dst_negative_sum_tail_short. (((F) = (((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) * S ((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) + ((((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))))) /\ (((exists fs_u_dst_tail_shortpositive fs_v_dst_tail_shortpositive. ((((exists fs_h_dst_tail_shortpositive_body_start. fs_h_dst_tail_shortpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_start. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_start * S ((S (0)) * fs_v_dst_tail_shortpositive) + (0))) /\ ((((exists fs_h_dst_tail_shortpositive_body_terminal. fs_h_dst_tail_shortpositive_body_terminal + S (dst_positive_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_terminal. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_terminal * S ((S (k)) * fs_v_dst_tail_shortpositive) + (dst_positive_sum_tail_short))) /\ forall fs_i_dst_tail_shortpositive_body_steps. (exists fs_lt_dst_tail_shortpositive_body_steps_bound. fs_lt_dst_tail_shortpositive_body_steps_bound + S fs_i_dst_tail_shortpositive_body_steps = k) -> exists fs_a_dst_tail_shortpositive_body_steps fs_r_dst_tail_shortpositive_body_steps fs_s_dst_tail_shortpositive_body_steps. ((((exists fs_h_dst_tail_shortpositive_body_steps_summand. fs_h_dst_tail_shortpositive_body_steps_summand + S (fs_a_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short)) /\ exists fs_q_dst_tail_shortpositive_body_steps_summand. dst_positive_code_tail_short = fs_q_dst_tail_shortpositive_body_steps_summand * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short) + (fs_a_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_partial. fs_h_dst_tail_shortpositive_body_steps_partial + S (fs_r_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_partial. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_partial * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_r_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_successor. fs_h_dst_tail_shortpositive_body_steps_successor + S (fs_s_dst_tail_shortpositive_body_steps) = S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_successor. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_successor * S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_s_dst_tail_shortpositive_body_steps))) /\ fs_s_dst_tail_shortpositive_body_steps = fs_r_dst_tail_shortpositive_body_steps + fs_a_dst_tail_shortpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_shortnegative fs_v_dst_tail_shortnegative. ((((exists fs_h_dst_tail_shortnegative_body_start. fs_h_dst_tail_shortnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_start. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_start * S ((S (0)) * fs_v_dst_tail_shortnegative) + (0))) /\ ((((exists fs_h_dst_tail_shortnegative_body_terminal. fs_h_dst_tail_shortnegative_body_terminal + S (dst_negative_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_terminal. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_terminal * S ((S (k)) * fs_v_dst_tail_shortnegative) + (dst_negative_sum_tail_short))) /\ forall fs_i_dst_tail_shortnegative_body_steps. (exists fs_lt_dst_tail_shortnegative_body_steps_bound. fs_lt_dst_tail_shortnegative_body_steps_bound + S fs_i_dst_tail_shortnegative_body_steps = k) -> exists fs_a_dst_tail_shortnegative_body_steps fs_r_dst_tail_shortnegative_body_steps fs_s_dst_tail_shortnegative_body_steps. ((((exists fs_h_dst_tail_shortnegative_body_steps_summand. fs_h_dst_tail_shortnegative_body_steps_summand + S (fs_a_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short)) /\ exists fs_q_dst_tail_shortnegative_body_steps_summand. dst_negative_code_tail_short = fs_q_dst_tail_shortnegative_body_steps_summand * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short) + (fs_a_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_partial. fs_h_dst_tail_shortnegative_body_steps_partial + S (fs_r_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_partial. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_partial * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_r_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_successor. fs_h_dst_tail_shortnegative_body_steps_successor + S (fs_s_dst_tail_shortnegative_body_steps) = S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_successor. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_successor * S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_s_dst_tail_shortnegative_body_steps))) /\ fs_s_dst_tail_shortnegative_body_steps = fs_r_dst_tail_shortnegative_body_steps + fs_a_dst_tail_shortnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_shortresult ge_balance_negative_tail_shortresult. (((((a) = 2 * (ge_balance_positive_tail_shortresult) /\ (ge_balance_negative_tail_shortresult) = 0) \/ exists ge_signed_half_tail_shortresultdecode. (((a) = 2 * ge_signed_half_tail_shortresultdecode + 1 /\ (ge_balance_positive_tail_shortresult) = 0) /\ (ge_balance_negative_tail_shortresult) = S ge_signed_half_tail_shortresultdecode))) /\ ((dst_positive_sum_tail_short) + ge_balance_negative_tail_shortresult = (dst_negative_sum_tail_short) + ge_balance_positive_tail_shortresult))))))))) -> (exists dst_positive_code_tail_long dst_positive_scale_tail_long dst_negative_code_tail_long dst_negative_scale_tail_long dst_positive_sum_tail_long dst_negative_sum_tail_long. (((F) = (((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) * S ((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) + ((((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))))) /\ (((exists fs_u_dst_tail_longpositive fs_v_dst_tail_longpositive. ((((exists fs_h_dst_tail_longpositive_body_start. fs_h_dst_tail_longpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_start. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_start * S ((S (0)) * fs_v_dst_tail_longpositive) + (0))) /\ ((((exists fs_h_dst_tail_longpositive_body_terminal. fs_h_dst_tail_longpositive_body_terminal + S (dst_positive_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_terminal. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_terminal * S ((S (l)) * fs_v_dst_tail_longpositive) + (dst_positive_sum_tail_long))) /\ forall fs_i_dst_tail_longpositive_body_steps. (exists fs_lt_dst_tail_longpositive_body_steps_bound. fs_lt_dst_tail_longpositive_body_steps_bound + S fs_i_dst_tail_longpositive_body_steps = l) -> exists fs_a_dst_tail_longpositive_body_steps fs_r_dst_tail_longpositive_body_steps fs_s_dst_tail_longpositive_body_steps. ((((exists fs_h_dst_tail_longpositive_body_steps_summand. fs_h_dst_tail_longpositive_body_steps_summand + S (fs_a_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long)) /\ exists fs_q_dst_tail_longpositive_body_steps_summand. dst_positive_code_tail_long = fs_q_dst_tail_longpositive_body_steps_summand * S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long) + (fs_a_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_partial. fs_h_dst_tail_longpositive_body_steps_partial + S (fs_r_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_partial. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_partial * S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_r_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_successor. fs_h_dst_tail_longpositive_body_steps_successor + S (fs_s_dst_tail_longpositive_body_steps) = S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_successor. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_successor * S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_s_dst_tail_longpositive_body_steps))) /\ fs_s_dst_tail_longpositive_body_steps = fs_r_dst_tail_longpositive_body_steps + fs_a_dst_tail_longpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_longnegative fs_v_dst_tail_longnegative. ((((exists fs_h_dst_tail_longnegative_body_start. fs_h_dst_tail_longnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_start. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_start * S ((S (0)) * fs_v_dst_tail_longnegative) + (0))) /\ ((((exists fs_h_dst_tail_longnegative_body_terminal. fs_h_dst_tail_longnegative_body_terminal + S (dst_negative_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_terminal. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_terminal * S ((S (l)) * fs_v_dst_tail_longnegative) + (dst_negative_sum_tail_long))) /\ forall fs_i_dst_tail_longnegative_body_steps. (exists fs_lt_dst_tail_longnegative_body_steps_bound. fs_lt_dst_tail_longnegative_body_steps_bound + S fs_i_dst_tail_longnegative_body_steps = l) -> exists fs_a_dst_tail_longnegative_body_steps fs_r_dst_tail_longnegative_body_steps fs_s_dst_tail_longnegative_body_steps. ((((exists fs_h_dst_tail_longnegative_body_steps_summand. fs_h_dst_tail_longnegative_body_steps_summand + S (fs_a_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long)) /\ exists fs_q_dst_tail_longnegative_body_steps_summand. dst_negative_code_tail_long = fs_q_dst_tail_longnegative_body_steps_summand * S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long) + (fs_a_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_partial. fs_h_dst_tail_longnegative_body_steps_partial + S (fs_r_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_partial. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_partial * S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_r_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_successor. fs_h_dst_tail_longnegative_body_steps_successor + S (fs_s_dst_tail_longnegative_body_steps) = S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_successor. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_successor * S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_s_dst_tail_longnegative_body_steps))) /\ fs_s_dst_tail_longnegative_body_steps = fs_r_dst_tail_longnegative_body_steps + fs_a_dst_tail_longnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_longresult ge_balance_negative_tail_longresult. (((((b) = 2 * (ge_balance_positive_tail_longresult) /\ (ge_balance_negative_tail_longresult) = 0) \/ exists ge_signed_half_tail_longresultdecode. (((b) = 2 * ge_signed_half_tail_longresultdecode + 1 /\ (ge_balance_positive_tail_longresult) = 0) /\ (ge_balance_negative_tail_longresult) = S ge_signed_half_tail_longresultdecode))) /\ ((dst_positive_sum_tail_long) + ge_balance_negative_tail_longresult = (dst_negative_sum_tail_long) + ge_balance_positive_tail_longresult))))))))) -> a=b

Constructive proof overview

Generated structural guide

Ordinary finite induction proves that a genuinely zero tail changes no actual canonical signed prefix sum.

The unchanged tactic script uses 10 declared prerequisites and contains 103 exact native proof lines.

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

Proof neighborhood

Direct dependencies

le_zero Stable theorem; checked-use authorized divisor_signed_sum_functional Alpha theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized divisor_signed_sum_successor_decompose Alpha theorem; checked-use authorized ZS0002 signed_zero_window_restrict le_succ_self Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized signed_add_functional Alpha theorem; checked-use authorized signed_add_zero_right Alpha theorem; checked-use authorized

Direct dependents

ZS0005 signed_prefix_sum_zero_value ZS0008 signed_prefix_sum_zero_padding_iff

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

103 script commands · 19 reading checkpoints · 6 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 zero window restrict

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

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

  1. L1
    intro F
  2. L2
    intro k
  3. L3
    intro l
02Induction on lL4–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro a
  3. L6
    intro b
  4. L7
    intro hkl
  5. L8
    intro hz
  6. L9
    intro ha
  7. L10
    intro hb
03Establish hkL11–20

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

  1. L11
    have hk : k=0
  2. L12
    specialize le_zero (k)
  3. L13
    apply le_zero
  4. L14
    exact hkl
  5. L15
    rewrite hk at ha
  6. L16
    rewrite hk at ha
  7. L17
    rewrite hk at ha
  8. L18
    rewrite hk at ha
  9. L19
    rewrite hk at ha
  10. L20
    rewrite hk at ha
04Use earlier factsL21–27

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

  1. L21
    specialize divisor_signed_sum_functional (F)
  2. L22
    specialize divisor_signed_sum_functional (0)
  3. L23
    specialize divisor_signed_sum_functional (a)
  4. L24
    specialize divisor_signed_sum_functional (b)
  5. L25
    apply divisor_signed_sum_functional
  6. L26
    exact ha
  7. L27
    exact hb
05Fix variables and assumptionsL28–33

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

  1. L28
    intro a
  2. L29
    intro b
  3. L30
    intro hkl
  4. L31
    intro hz
  5. L32
    intro ha
  6. L33
    intro hb
06Establish hcL34–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L34
    have hc : k=S l \/ (exists pvs_gap_tail_cases. pvs_gap_tail_cases + S (k) = (S l))
  2. L35
    specialize le_eq_or_lt (k)
  3. L36
    specialize le_eq_or_lt (S l)
  4. L37
    apply le_eq_or_lt
  5. L38
    exact hkl
07Separate the logical casesL39–39

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

  1. L39
    cases hc
08Calculate and transport equalitiesL40–45

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

  1. L40
    rewrite hc_left at ha
  2. L41
    rewrite hc_left at ha
  3. L42
    rewrite hc_left at ha
  4. L43
    rewrite hc_left at ha
  5. L44
    rewrite hc_left at ha
  6. L45
    rewrite hc_left at ha
09Use earlier factsL46–52

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

  1. L46
    specialize divisor_signed_sum_functional (F)
  2. L47
    specialize divisor_signed_sum_functional (S l)
  3. L48
    specialize divisor_signed_sum_functional (a)
  4. L49
    specialize divisor_signed_sum_functional (b)
  5. L50
    apply divisor_signed_sum_functional
  6. L51
    exact ha
  7. L52
    exact hb
10Establish hsmallL53–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L53
    have hsmall : exists pvs_le_gap_tail_small. pvs_le_gap_tail_small + (k) = (l)
  2. L54
    specialize le_of_succ_le_succ (k)
  3. L55
    specialize le_of_succ_le_succ (l)
  4. L56
    apply le_of_succ_le_succ
  5. L57
    exact hc_right
11Establish hdL58–63

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

  1. L58
    have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,b))Definitions: SignedAddArithAtSignedPrefixSum
  2. L59
    specialize divisor_signed_sum_successor_decompose (F)
  3. L60
    specialize divisor_signed_sum_successor_decompose (l)
  4. L61
    specialize divisor_signed_sum_successor_decompose (b)
  5. L62
    apply divisor_signed_sum_successor_decompose
  6. L63
    exact hb
12Separate the logical casesL64–67

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

  1. L64
    cases hd
  2. L65
    cases hd_witness
  3. L66
    cases hd_witness_witness
  4. L67
    cases hd_witness_witness_right
13Establish hpL68–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

  1. L68
    have hp : a=x
  2. L69
    specialize IH (a)
  3. L70
    specialize IH (x)
  4. L71
    apply IH
  5. L72
    exact hsmall
  6. L73
    specialize signed_zero_window_restrict (F)
  7. L74
    specialize signed_zero_window_restrict (k)
  8. L75
    specialize signed_zero_window_restrict (l)
  9. L76
    specialize signed_zero_window_restrict (S l)
  10. L77
    apply signed_zero_window_restrict
14Use earlier factsL78–82

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

  1. L78
    specialize le_succ_self (l)
  2. L79
    apply le_succ_self
  3. L80
    exact hz
  4. L81
    exact ha
  5. L82
    exact hd_witness_witness_left
15Establish hlastL83–92

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hz.

  1. L83
    have hlast : x1=0
  2. L84
    specialize hz (l)
  3. L85
    specialize hz (x1)
  4. L86
    apply hz
  5. L87
    exact hsmall
  6. L88
    specialize le_refl (S l)
  7. L89
    apply le_refl
  8. L90
    exact hd_witness_witness_right_left
  9. L91
    rewrite hlast at hd_witness_witness_right_right
  10. L92
    rewrite hlast at hd_witness_witness_right_right
16Calculate and transport equalitiesL93–93

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

  1. L93
    trans x
17Use earlier factsL94–94

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

  1. L94
    exact hp
18Calculate and transport equalitiesL95–95

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

  1. L95
    symm
19Use earlier factsL96–103

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

  1. L96
    specialize signed_add_functional (x)
  2. L97
    specialize signed_add_functional (0)
  3. L98
    specialize signed_add_functional (b)
  4. L99
    specialize signed_add_functional (x)
  5. L100
    apply signed_add_functional
  6. L101
    exact hd_witness_witness_right_right
  7. L102
    specialize signed_add_zero_right (x)
  8. L103
    apply signed_add_zero_right

Library-wide reading audit

Original exact command ledger · 103 lines
  1. 0001intro F
  2. 0002intro k
  3. 0003intro l
  4. 0004induction l
  5. 0005intro a
  6. 0006intro b
  7. 0007intro hkl
  8. 0008intro hz
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hk : k=0
  12. 0012specialize le_zero (k)
  13. 0013apply le_zero
  14. 0014exact hkl
  15. 0015rewrite hk at ha
  16. 0016rewrite hk at ha
  17. 0017rewrite hk at ha
  18. 0018rewrite hk at ha
  19. 0019rewrite hk at ha
  20. 0020rewrite hk at ha
  21. 0021specialize divisor_signed_sum_functional (F)
  22. 0022specialize divisor_signed_sum_functional (0)
  23. 0023specialize divisor_signed_sum_functional (a)
  24. 0024specialize divisor_signed_sum_functional (b)
  25. 0025apply divisor_signed_sum_functional
  26. 0026exact ha
  27. 0027exact hb
  28. 0028intro a
  29. 0029intro b
  30. 0030intro hkl
  31. 0031intro hz
  32. 0032intro ha
  33. 0033intro hb
  34. 0034have hc : k=S l \/ (exists pvs_gap_tail_cases. pvs_gap_tail_cases + S (k) = (S l))
  35. 0035specialize le_eq_or_lt (k)
  36. 0036specialize le_eq_or_lt (S l)
  37. 0037apply le_eq_or_lt
  38. 0038exact hkl
  39. 0039cases hc
  40. 0040rewrite hc_left at ha
  41. 0041rewrite hc_left at ha
  42. 0042rewrite hc_left at ha
  43. 0043rewrite hc_left at ha
  44. 0044rewrite hc_left at ha
  45. 0045rewrite hc_left at ha
  46. 0046specialize divisor_signed_sum_functional (F)
  47. 0047specialize divisor_signed_sum_functional (S l)
  48. 0048specialize divisor_signed_sum_functional (a)
  49. 0049specialize divisor_signed_sum_functional (b)
  50. 0050apply divisor_signed_sum_functional
  51. 0051exact ha
  52. 0052exact hb
  53. 0053have hsmall : exists pvs_le_gap_tail_small. pvs_le_gap_tail_small + (k) = (l)
  54. 0054specialize le_of_succ_le_succ (k)
  55. 0055specialize le_of_succ_le_succ (l)
  56. 0056apply le_of_succ_le_succ
  57. 0057exact hc_right
  58. 0058have hd : exists u v. (((exists dst_positive_code_tail_prefix dst_positive_scale_tail_prefix dst_negative_code_tail_prefix dst_negative_scale_tail_prefix dst_positive_sum_tail_prefix dst_negative_sum_tail_prefix. (((F) = (((((dst_positive_code_tail_prefix) + (dst_positive_scale_tail_prefix)) * S ((dst_positive_code_tail_prefix) + (dst_positive_scale_tail_prefix)) + ((dst_positive_scale_tail_prefix) + (dst_positive_scale_tail_prefix))) + (((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) * S ((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) + ((dst_negative_scale_tail_prefix) + (dst_negative_scale_tail_prefix)))) * S ((((dst_positive_code_tail_prefix) + (dst_positive_scale_tail_prefix)) * S ((dst_positive_code_tail_prefix) + (dst_positive_scale_tail_prefix)) + ((dst_positive_scale_tail_prefix) + (dst_positive_scale_tail_prefix))) + (((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) * S ((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) + ((dst_negative_scale_tail_prefix) + (dst_negative_scale_tail_prefix)))) + ((((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) * S ((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) + ((dst_negative_scale_tail_prefix) + (dst_negative_scale_tail_prefix))) + (((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) * S ((dst_negative_code_tail_prefix) + (dst_negative_scale_tail_prefix)) + ((dst_negative_scale_tail_prefix) + (dst_negative_scale_tail_prefix)))))) /\ (((exists fs_u_dst_tail_prefixpositive fs_v_dst_tail_prefixpositive. ((((exists fs_h_dst_tail_prefixpositive_body_start. fs_h_dst_tail_prefixpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_prefixpositive)) /\ exists fs_q_dst_tail_prefixpositive_body_start. fs_u_dst_tail_prefixpositive = fs_q_dst_tail_prefixpositive_body_start * S ((S (0)) * fs_v_dst_tail_prefixpositive) + (0))) /\ ((((exists fs_h_dst_tail_prefixpositive_body_terminal. fs_h_dst_tail_prefixpositive_body_terminal + S (dst_positive_sum_tail_prefix) = S ((S (l)) * fs_v_dst_tail_prefixpositive)) /\ exists fs_q_dst_tail_prefixpositive_body_terminal. fs_u_dst_tail_prefixpositive = fs_q_dst_tail_prefixpositive_body_terminal * S ((S (l)) * fs_v_dst_tail_prefixpositive) + (dst_positive_sum_tail_prefix))) /\ forall fs_i_dst_tail_prefixpositive_body_steps. (exists fs_lt_dst_tail_prefixpositive_body_steps_bound. fs_lt_dst_tail_prefixpositive_body_steps_bound + S fs_i_dst_tail_prefixpositive_body_steps = l) -> exists fs_a_dst_tail_prefixpositive_body_steps fs_r_dst_tail_prefixpositive_body_steps fs_s_dst_tail_prefixpositive_body_steps. ((((exists fs_h_dst_tail_prefixpositive_body_steps_summand. fs_h_dst_tail_prefixpositive_body_steps_summand + S (fs_a_dst_tail_prefixpositive_body_steps) = S ((S (fs_i_dst_tail_prefixpositive_body_steps)) * dst_positive_scale_tail_prefix)) /\ exists fs_q_dst_tail_prefixpositive_body_steps_summand. dst_positive_code_tail_prefix = fs_q_dst_tail_prefixpositive_body_steps_summand * S ((S (fs_i_dst_tail_prefixpositive_body_steps)) * dst_positive_scale_tail_prefix) + (fs_a_dst_tail_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_tail_prefixpositive_body_steps_partial. fs_h_dst_tail_prefixpositive_body_steps_partial + S (fs_r_dst_tail_prefixpositive_body_steps) = S ((S (fs_i_dst_tail_prefixpositive_body_steps)) * fs_v_dst_tail_prefixpositive)) /\ exists fs_q_dst_tail_prefixpositive_body_steps_partial. fs_u_dst_tail_prefixpositive = fs_q_dst_tail_prefixpositive_body_steps_partial * S ((S (fs_i_dst_tail_prefixpositive_body_steps)) * fs_v_dst_tail_prefixpositive) + (fs_r_dst_tail_prefixpositive_body_steps))) /\ ((((exists fs_h_dst_tail_prefixpositive_body_steps_successor. fs_h_dst_tail_prefixpositive_body_steps_successor + S (fs_s_dst_tail_prefixpositive_body_steps) = S ((S (S fs_i_dst_tail_prefixpositive_body_steps)) * fs_v_dst_tail_prefixpositive)) /\ exists fs_q_dst_tail_prefixpositive_body_steps_successor. fs_u_dst_tail_prefixpositive = fs_q_dst_tail_prefixpositive_body_steps_successor * S ((S (S fs_i_dst_tail_prefixpositive_body_steps)) * fs_v_dst_tail_prefixpositive) + (fs_s_dst_tail_prefixpositive_body_steps))) /\ fs_s_dst_tail_prefixpositive_body_steps = fs_r_dst_tail_prefixpositive_body_steps + fs_a_dst_tail_prefixpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_prefixnegative fs_v_dst_tail_prefixnegative. ((((exists fs_h_dst_tail_prefixnegative_body_start. fs_h_dst_tail_prefixnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_prefixnegative)) /\ exists fs_q_dst_tail_prefixnegative_body_start. fs_u_dst_tail_prefixnegative = fs_q_dst_tail_prefixnegative_body_start * S ((S (0)) * fs_v_dst_tail_prefixnegative) + (0))) /\ ((((exists fs_h_dst_tail_prefixnegative_body_terminal. fs_h_dst_tail_prefixnegative_body_terminal + S (dst_negative_sum_tail_prefix) = S ((S (l)) * fs_v_dst_tail_prefixnegative)) /\ exists fs_q_dst_tail_prefixnegative_body_terminal. fs_u_dst_tail_prefixnegative = fs_q_dst_tail_prefixnegative_body_terminal * S ((S (l)) * fs_v_dst_tail_prefixnegative) + (dst_negative_sum_tail_prefix))) /\ forall fs_i_dst_tail_prefixnegative_body_steps. (exists fs_lt_dst_tail_prefixnegative_body_steps_bound. fs_lt_dst_tail_prefixnegative_body_steps_bound + S fs_i_dst_tail_prefixnegative_body_steps = l) -> exists fs_a_dst_tail_prefixnegative_body_steps fs_r_dst_tail_prefixnegative_body_steps fs_s_dst_tail_prefixnegative_body_steps. ((((exists fs_h_dst_tail_prefixnegative_body_steps_summand. fs_h_dst_tail_prefixnegative_body_steps_summand + S (fs_a_dst_tail_prefixnegative_body_steps) = S ((S (fs_i_dst_tail_prefixnegative_body_steps)) * dst_negative_scale_tail_prefix)) /\ exists fs_q_dst_tail_prefixnegative_body_steps_summand. dst_negative_code_tail_prefix = fs_q_dst_tail_prefixnegative_body_steps_summand * S ((S (fs_i_dst_tail_prefixnegative_body_steps)) * dst_negative_scale_tail_prefix) + (fs_a_dst_tail_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_tail_prefixnegative_body_steps_partial. fs_h_dst_tail_prefixnegative_body_steps_partial + S (fs_r_dst_tail_prefixnegative_body_steps) = S ((S (fs_i_dst_tail_prefixnegative_body_steps)) * fs_v_dst_tail_prefixnegative)) /\ exists fs_q_dst_tail_prefixnegative_body_steps_partial. fs_u_dst_tail_prefixnegative = fs_q_dst_tail_prefixnegative_body_steps_partial * S ((S (fs_i_dst_tail_prefixnegative_body_steps)) * fs_v_dst_tail_prefixnegative) + (fs_r_dst_tail_prefixnegative_body_steps))) /\ ((((exists fs_h_dst_tail_prefixnegative_body_steps_successor. fs_h_dst_tail_prefixnegative_body_steps_successor + S (fs_s_dst_tail_prefixnegative_body_steps) = S ((S (S fs_i_dst_tail_prefixnegative_body_steps)) * fs_v_dst_tail_prefixnegative)) /\ exists fs_q_dst_tail_prefixnegative_body_steps_successor. fs_u_dst_tail_prefixnegative = fs_q_dst_tail_prefixnegative_body_steps_successor * S ((S (S fs_i_dst_tail_prefixnegative_body_steps)) * fs_v_dst_tail_prefixnegative) + (fs_s_dst_tail_prefixnegative_body_steps))) /\ fs_s_dst_tail_prefixnegative_body_steps = fs_r_dst_tail_prefixnegative_body_steps + fs_a_dst_tail_prefixnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_prefixresult ge_balance_negative_tail_prefixresult. (((((u) = 2 * (ge_balance_positive_tail_prefixresult) /\ (ge_balance_negative_tail_prefixresult) = 0) \/ exists ge_signed_half_tail_prefixresultdecode. (((u) = 2 * ge_signed_half_tail_prefixresultdecode + 1 /\ (ge_balance_positive_tail_prefixresult) = 0) /\ (ge_balance_negative_tail_prefixresult) = S ge_signed_half_tail_prefixresultdecode))) /\ ((dst_positive_sum_tail_prefix) + ge_balance_negative_tail_prefixresult = (dst_negative_sum_tail_prefix) + ge_balance_positive_tail_prefixresult))))))))) /\ (((exists dst_positive_code_tail_entry dst_positive_scale_tail_entry dst_negative_code_tail_entry dst_negative_scale_tail_entry dst_positive_tail_entry dst_negative_tail_entry. (((F) = (((((dst_positive_code_tail_entry) + (dst_positive_scale_tail_entry)) * S ((dst_positive_code_tail_entry) + (dst_positive_scale_tail_entry)) + ((dst_positive_scale_tail_entry) + (dst_positive_scale_tail_entry))) + (((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) * S ((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) + ((dst_negative_scale_tail_entry) + (dst_negative_scale_tail_entry)))) * S ((((dst_positive_code_tail_entry) + (dst_positive_scale_tail_entry)) * S ((dst_positive_code_tail_entry) + (dst_positive_scale_tail_entry)) + ((dst_positive_scale_tail_entry) + (dst_positive_scale_tail_entry))) + (((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) * S ((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) + ((dst_negative_scale_tail_entry) + (dst_negative_scale_tail_entry)))) + ((((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) * S ((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) + ((dst_negative_scale_tail_entry) + (dst_negative_scale_tail_entry))) + (((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) * S ((dst_negative_code_tail_entry) + (dst_negative_scale_tail_entry)) + ((dst_negative_scale_tail_entry) + (dst_negative_scale_tail_entry)))))) /\ (((((exists ff_h_pvs_tail_entrypositive. ff_h_pvs_tail_entrypositive + S (dst_positive_tail_entry) = S ((S (l)) * dst_positive_scale_tail_entry)) /\ exists ff_q_pvs_tail_entrypositive. dst_positive_code_tail_entry = ff_q_pvs_tail_entrypositive * S ((S (l)) * dst_positive_scale_tail_entry) + (dst_positive_tail_entry))) /\ (((((exists ff_h_pvs_tail_entrynegative. ff_h_pvs_tail_entrynegative + S (dst_negative_tail_entry) = S ((S (l)) * dst_negative_scale_tail_entry)) /\ exists ff_q_pvs_tail_entrynegative. dst_negative_code_tail_entry = ff_q_pvs_tail_entrynegative * S ((S (l)) * dst_negative_scale_tail_entry) + (dst_negative_tail_entry))) /\ (exists ge_balance_positive_tail_entryvalue ge_balance_negative_tail_entryvalue. (((((v) = 2 * (ge_balance_positive_tail_entryvalue) /\ (ge_balance_negative_tail_entryvalue) = 0) \/ exists ge_signed_half_tail_entryvaluedecode. (((v) = 2 * ge_signed_half_tail_entryvaluedecode + 1 /\ (ge_balance_positive_tail_entryvalue) = 0) /\ (ge_balance_negative_tail_entryvalue) = S ge_signed_half_tail_entryvaluedecode))) /\ ((dst_positive_tail_entry) + ge_balance_negative_tail_entryvalue = (dst_negative_tail_entry) + ge_balance_positive_tail_entryvalue))))))))) /\ (exists dsa_ap_tail_add dsa_an_tail_add dsa_bp_tail_add dsa_bn_tail_add dsa_cp_tail_add dsa_cn_tail_add. (((((u) = 2 * (dsa_ap_tail_add) /\ (dsa_an_tail_add) = 0) \/ exists ge_signed_half_tail_addleft. (((u) = 2 * ge_signed_half_tail_addleft + 1 /\ (dsa_ap_tail_add) = 0) /\ (dsa_an_tail_add) = S ge_signed_half_tail_addleft))) /\ ((((((v) = 2 * (dsa_bp_tail_add) /\ (dsa_bn_tail_add) = 0) \/ exists ge_signed_half_tail_addright. (((v) = 2 * ge_signed_half_tail_addright + 1 /\ (dsa_bp_tail_add) = 0) /\ (dsa_bn_tail_add) = S ge_signed_half_tail_addright))) /\ ((((((b) = 2 * (dsa_cp_tail_add) /\ (dsa_cn_tail_add) = 0) \/ exists ge_signed_half_tail_addoutput. (((b) = 2 * ge_signed_half_tail_addoutput + 1 /\ (dsa_cp_tail_add) = 0) /\ (dsa_cn_tail_add) = S ge_signed_half_tail_addoutput))) /\ ((dsa_ap_tail_add + dsa_bp_tail_add) + dsa_cn_tail_add = (dsa_an_tail_add + dsa_bn_tail_add) + dsa_cp_tail_add)))))))))))
  59. 0059specialize divisor_signed_sum_successor_decompose (F)
  60. 0060specialize divisor_signed_sum_successor_decompose (l)
  61. 0061specialize divisor_signed_sum_successor_decompose (b)
  62. 0062apply divisor_signed_sum_successor_decompose
  63. 0063exact hb
  64. 0064cases hd
  65. 0065cases hd_witness
  66. 0066cases hd_witness_witness
  67. 0067cases hd_witness_witness_right
  68. 0068have hp : a=x
  69. 0069specialize IH (a)
  70. 0070specialize IH (x)
  71. 0071apply IH
  72. 0072exact hsmall
  73. 0073specialize signed_zero_window_restrict (F)
  74. 0074specialize signed_zero_window_restrict (k)
  75. 0075specialize signed_zero_window_restrict (l)
  76. 0076specialize signed_zero_window_restrict (S l)
  77. 0077apply signed_zero_window_restrict
  78. 0078specialize le_succ_self (l)
  79. 0079apply le_succ_self
  80. 0080exact hz
  81. 0081exact ha
  82. 0082exact hd_witness_witness_left
  83. 0083have hlast : x1=0
  84. 0084specialize hz (l)
  85. 0085specialize hz (x1)
  86. 0086apply hz
  87. 0087exact hsmall
  88. 0088specialize le_refl (S l)
  89. 0089apply le_refl
  90. 0090exact hd_witness_witness_right_left
  91. 0091rewrite hlast at hd_witness_witness_right_right
  92. 0092rewrite hlast at hd_witness_witness_right_right
  93. 0093trans x
  94. 0094exact hp
  95. 0095symm
  96. 0096specialize signed_add_functional (x)
  97. 0097specialize signed_add_functional (0)
  98. 0098specialize signed_add_functional (b)
  99. 0099specialize signed_add_functional (x)
  100. 0100apply signed_add_functional
  101. 0101exact hd_witness_witness_right_right
  102. 0102specialize signed_add_zero_right (x)
  103. 0103apply signed_add_zero_right