DV001D

divisor_mask_omitted_entry

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

Every actual mask explicitly has zero at index zero and at each nondivisor; the source value there is not constrained.

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 n l M d. (((exists dst_positive_code_omit_masktable dst_positive_scale_omit_masktable dst_negative_code_omit_masktable dst_negative_scale_omit_masktable. (((M) = (((((dst_positive_code_omit_masktable) + (dst_positive_scale_omit_masktable)) * S ((dst_positive_code_omit_masktable) + (dst_positive_scale_omit_masktable)) + ((dst_positive_scale_omit_masktable) + (dst_positive_scale_omit_masktable))) + (((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) * S ((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) + ((dst_negative_scale_omit_masktable) + (dst_negative_scale_omit_masktable)))) * S ((((dst_positive_code_omit_masktable) + (dst_positive_scale_omit_masktable)) * S ((dst_positive_code_omit_masktable) + (dst_positive_scale_omit_masktable)) + ((dst_positive_scale_omit_masktable) + (dst_positive_scale_omit_masktable))) + (((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) * S ((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) + ((dst_negative_scale_omit_masktable) + (dst_negative_scale_omit_masktable)))) + ((((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) * S ((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) + ((dst_negative_scale_omit_masktable) + (dst_negative_scale_omit_masktable))) + (((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) * S ((dst_negative_code_omit_masktable) + (dst_negative_scale_omit_masktable)) + ((dst_negative_scale_omit_masktable) + (dst_negative_scale_omit_masktable)))))) /\ (forall dst_index_omit_masktable. (exists pvs_le_gap_omit_masktabledomain. pvs_le_gap_omit_masktabledomain + (dst_index_omit_masktable) = (l)) -> exists dst_positive_omit_masktable dst_negative_omit_masktable dst_value_omit_masktable. ((((exists ff_h_pvs_omit_masktableentrypositive. ff_h_pvs_omit_masktableentrypositive + S (dst_positive_omit_masktable) = S ((S (dst_index_omit_masktable)) * dst_positive_scale_omit_masktable)) /\ exists ff_q_pvs_omit_masktableentrypositive. dst_positive_code_omit_masktable = ff_q_pvs_omit_masktableentrypositive * S ((S (dst_index_omit_masktable)) * dst_positive_scale_omit_masktable) + (dst_positive_omit_masktable))) /\ (((((exists ff_h_pvs_omit_masktableentrynegative. ff_h_pvs_omit_masktableentrynegative + S (dst_negative_omit_masktable) = S ((S (dst_index_omit_masktable)) * dst_negative_scale_omit_masktable)) /\ exists ff_q_pvs_omit_masktableentrynegative. dst_negative_code_omit_masktable = ff_q_pvs_omit_masktableentrynegative * S ((S (dst_index_omit_masktable)) * dst_negative_scale_omit_masktable) + (dst_negative_omit_masktable))) /\ (exists ge_balance_positive_omit_masktableentryvalue ge_balance_negative_omit_masktableentryvalue. (((((dst_value_omit_masktable) = 2 * (ge_balance_positive_omit_masktableentryvalue) /\ (ge_balance_negative_omit_masktableentryvalue) = 0) \/ exists ge_signed_half_omit_masktableentryvaluedecode. (((dst_value_omit_masktable) = 2 * ge_signed_half_omit_masktableentryvaluedecode + 1 /\ (ge_balance_positive_omit_masktableentryvalue) = 0) /\ (ge_balance_negative_omit_masktableentryvalue) = S ge_signed_half_omit_masktableentryvaluedecode))) /\ ((dst_positive_omit_masktable) + ge_balance_negative_omit_masktableentryvalue = (dst_negative_omit_masktable) + ge_balance_positive_omit_masktableentryvalue))))))))) /\ (forall dm_index_omit_mask dm_value_omit_mask. (exists pvs_le_gap_omit_maskdomain. pvs_le_gap_omit_maskdomain + (dm_index_omit_mask) = (l)) -> (exists dst_positive_code_omit_masklookup dst_positive_scale_omit_masklookup dst_negative_code_omit_masklookup dst_negative_scale_omit_masklookup dst_positive_omit_masklookup dst_negative_omit_masklookup. (((M) = (((((dst_positive_code_omit_masklookup) + (dst_positive_scale_omit_masklookup)) * S ((dst_positive_code_omit_masklookup) + (dst_positive_scale_omit_masklookup)) + ((dst_positive_scale_omit_masklookup) + (dst_positive_scale_omit_masklookup))) + (((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) * S ((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) + ((dst_negative_scale_omit_masklookup) + (dst_negative_scale_omit_masklookup)))) * S ((((dst_positive_code_omit_masklookup) + (dst_positive_scale_omit_masklookup)) * S ((dst_positive_code_omit_masklookup) + (dst_positive_scale_omit_masklookup)) + ((dst_positive_scale_omit_masklookup) + (dst_positive_scale_omit_masklookup))) + (((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) * S ((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) + ((dst_negative_scale_omit_masklookup) + (dst_negative_scale_omit_masklookup)))) + ((((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) * S ((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) + ((dst_negative_scale_omit_masklookup) + (dst_negative_scale_omit_masklookup))) + (((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) * S ((dst_negative_code_omit_masklookup) + (dst_negative_scale_omit_masklookup)) + ((dst_negative_scale_omit_masklookup) + (dst_negative_scale_omit_masklookup)))))) /\ (((((exists ff_h_pvs_omit_masklookuppositive. ff_h_pvs_omit_masklookuppositive + S (dst_positive_omit_masklookup) = S ((S (dm_index_omit_mask)) * dst_positive_scale_omit_masklookup)) /\ exists ff_q_pvs_omit_masklookuppositive. dst_positive_code_omit_masklookup = ff_q_pvs_omit_masklookuppositive * S ((S (dm_index_omit_mask)) * dst_positive_scale_omit_masklookup) + (dst_positive_omit_masklookup))) /\ (((((exists ff_h_pvs_omit_masklookupnegative. ff_h_pvs_omit_masklookupnegative + S (dst_negative_omit_masklookup) = S ((S (dm_index_omit_mask)) * dst_negative_scale_omit_masklookup)) /\ exists ff_q_pvs_omit_masklookupnegative. dst_negative_code_omit_masklookup = ff_q_pvs_omit_masklookupnegative * S ((S (dm_index_omit_mask)) * dst_negative_scale_omit_masklookup) + (dst_negative_omit_masklookup))) /\ (exists ge_balance_positive_omit_masklookupvalue ge_balance_negative_omit_masklookupvalue. (((((dm_value_omit_mask) = 2 * (ge_balance_positive_omit_masklookupvalue) /\ (ge_balance_negative_omit_masklookupvalue) = 0) \/ exists ge_signed_half_omit_masklookupvaluedecode. (((dm_value_omit_mask) = 2 * ge_signed_half_omit_masklookupvaluedecode + 1 /\ (ge_balance_positive_omit_masklookupvalue) = 0) /\ (ge_balance_negative_omit_masklookupvalue) = S ge_signed_half_omit_masklookupvaluedecode))) /\ ((dst_positive_omit_masklookup) + ge_balance_negative_omit_masklookupvalue = (dst_negative_omit_masklookup) + ge_balance_positive_omit_masklookupvalue))))))))) -> ((((~((dm_index_omit_mask)=0)) /\ (exists dm_quotient_omit_maskentry. (((n)=(dm_index_omit_mask)*dm_quotient_omit_maskentry) /\ (exists dst_positive_code_omit_maskentryinput dst_positive_scale_omit_maskentryinput dst_negative_code_omit_maskentryinput dst_negative_scale_omit_maskentryinput dst_positive_omit_maskentryinput dst_negative_omit_maskentryinput. (((F) = (((((dst_positive_code_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput)) * S ((dst_positive_code_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput)) + ((dst_positive_scale_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput))) + (((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) * S ((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) + ((dst_negative_scale_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)))) * S ((((dst_positive_code_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput)) * S ((dst_positive_code_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput)) + ((dst_positive_scale_omit_maskentryinput) + (dst_positive_scale_omit_maskentryinput))) + (((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) * S ((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) + ((dst_negative_scale_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)))) + ((((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) * S ((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) + ((dst_negative_scale_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput))) + (((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) * S ((dst_negative_code_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)) + ((dst_negative_scale_omit_maskentryinput) + (dst_negative_scale_omit_maskentryinput)))))) /\ (((((exists ff_h_pvs_omit_maskentryinputpositive. ff_h_pvs_omit_maskentryinputpositive + S (dst_positive_omit_maskentryinput) = S ((S (dm_index_omit_mask)) * dst_positive_scale_omit_maskentryinput)) /\ exists ff_q_pvs_omit_maskentryinputpositive. dst_positive_code_omit_maskentryinput = ff_q_pvs_omit_maskentryinputpositive * S ((S (dm_index_omit_mask)) * dst_positive_scale_omit_maskentryinput) + (dst_positive_omit_maskentryinput))) /\ (((((exists ff_h_pvs_omit_maskentryinputnegative. ff_h_pvs_omit_maskentryinputnegative + S (dst_negative_omit_maskentryinput) = S ((S (dm_index_omit_mask)) * dst_negative_scale_omit_maskentryinput)) /\ exists ff_q_pvs_omit_maskentryinputnegative. dst_negative_code_omit_maskentryinput = ff_q_pvs_omit_maskentryinputnegative * S ((S (dm_index_omit_mask)) * dst_negative_scale_omit_maskentryinput) + (dst_negative_omit_maskentryinput))) /\ (exists ge_balance_positive_omit_maskentryinputvalue ge_balance_negative_omit_maskentryinputvalue. (((((dm_value_omit_mask) = 2 * (ge_balance_positive_omit_maskentryinputvalue) /\ (ge_balance_negative_omit_maskentryinputvalue) = 0) \/ exists ge_signed_half_omit_maskentryinputvaluedecode. (((dm_value_omit_mask) = 2 * ge_signed_half_omit_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_omit_maskentryinputvalue) = 0) /\ (ge_balance_negative_omit_maskentryinputvalue) = S ge_signed_half_omit_maskentryinputvaluedecode))) /\ ((dst_positive_omit_maskentryinput) + ge_balance_negative_omit_maskentryinputvalue = (dst_negative_omit_maskentryinput) + ge_balance_positive_omit_maskentryinputvalue))))))))))))) \/ ((((dm_index_omit_mask)=0 \/ ~(exists pvs_factor_omit_maskentrynondivisor. (n) = (dm_index_omit_mask) * pvs_factor_omit_maskentrynondivisor)) /\ ((dm_value_omit_mask)=0))))))) -> (exists pvs_le_gap_omit_bound. pvs_le_gap_omit_bound + (d) = (l)) -> (d=0 \/ ~(exists pvs_factor_omit_reason. (n) = (d) * pvs_factor_omit_reason)) -> (exists dst_positive_code_omit_mask_entry dst_positive_scale_omit_mask_entry dst_negative_code_omit_mask_entry dst_negative_scale_omit_mask_entry dst_positive_omit_mask_entry dst_negative_omit_mask_entry. (((M) = (((((dst_positive_code_omit_mask_entry) + (dst_positive_scale_omit_mask_entry)) * S ((dst_positive_code_omit_mask_entry) + (dst_positive_scale_omit_mask_entry)) + ((dst_positive_scale_omit_mask_entry) + (dst_positive_scale_omit_mask_entry))) + (((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) * S ((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) + ((dst_negative_scale_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)))) * S ((((dst_positive_code_omit_mask_entry) + (dst_positive_scale_omit_mask_entry)) * S ((dst_positive_code_omit_mask_entry) + (dst_positive_scale_omit_mask_entry)) + ((dst_positive_scale_omit_mask_entry) + (dst_positive_scale_omit_mask_entry))) + (((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) * S ((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) + ((dst_negative_scale_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)))) + ((((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) * S ((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) + ((dst_negative_scale_omit_mask_entry) + (dst_negative_scale_omit_mask_entry))) + (((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) * S ((dst_negative_code_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)) + ((dst_negative_scale_omit_mask_entry) + (dst_negative_scale_omit_mask_entry)))))) /\ (((((exists ff_h_pvs_omit_mask_entrypositive. ff_h_pvs_omit_mask_entrypositive + S (dst_positive_omit_mask_entry) = S ((S (d)) * dst_positive_scale_omit_mask_entry)) /\ exists ff_q_pvs_omit_mask_entrypositive. dst_positive_code_omit_mask_entry = ff_q_pvs_omit_mask_entrypositive * S ((S (d)) * dst_positive_scale_omit_mask_entry) + (dst_positive_omit_mask_entry))) /\ (((((exists ff_h_pvs_omit_mask_entrynegative. ff_h_pvs_omit_mask_entrynegative + S (dst_negative_omit_mask_entry) = S ((S (d)) * dst_negative_scale_omit_mask_entry)) /\ exists ff_q_pvs_omit_mask_entrynegative. dst_negative_code_omit_mask_entry = ff_q_pvs_omit_mask_entrynegative * S ((S (d)) * dst_negative_scale_omit_mask_entry) + (dst_negative_omit_mask_entry))) /\ (exists ge_balance_positive_omit_mask_entryvalue ge_balance_negative_omit_mask_entryvalue. (((((0) = 2 * (ge_balance_positive_omit_mask_entryvalue) /\ (ge_balance_negative_omit_mask_entryvalue) = 0) \/ exists ge_signed_half_omit_mask_entryvaluedecode. (((0) = 2 * ge_signed_half_omit_mask_entryvaluedecode + 1 /\ (ge_balance_positive_omit_mask_entryvalue) = 0) /\ (ge_balance_negative_omit_mask_entryvalue) = S ge_signed_half_omit_mask_entryvaluedecode))) /\ ((dst_positive_omit_mask_entry) + ge_balance_negative_omit_mask_entryvalue = (dst_negative_omit_mask_entry) + ge_balance_positive_omit_mask_entryvalue)))))))))

Constructive proof overview

Generated structural guide

Every actual mask explicitly has zero at index zero and at each nondivisor; the source value there is not constrained.

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

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

Proof neighborhood

Direct dependencies

divisor_signed_table_lookup Alpha theorem; checked-use authorized DV0016 divisor_mask_entry_omitted_value

Direct dependents

DV0024 signed_divisor_sum_one

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

32 script commands · 8 reading checkpoints · 2 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)
divisor mask entry omitted 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–8

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

  1. L1
    intro F
  2. L2
    intro n
  3. L3
    intro l
  4. L4
    intro M
  5. L5
    intro d
  6. L6
    intro hm
  7. L7
    intro hbound
  8. L8
    intro hc
02Separate the logical casesL9–9

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

  1. L9
    cases hm
03Establish huL10–16

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

  1. L10
    have hu : ∃ u. ArithAt(M,d,u)Definitions: ArithAt
  2. L11
    specialize divisor_signed_table_lookup (l)
  3. L12
    specialize divisor_signed_table_lookup (M)
  4. L13
    specialize divisor_signed_table_lookup (d)
  5. L14
    apply divisor_signed_table_lookup
  6. L15
    exact hm_left
  7. L16
    exact hbound
04Separate the logical casesL17–17

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

  1. L17
    cases hu
05Establish heqL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor mask entry omitted value.

  1. L18
    have heq : x=0
  2. L19
    specialize divisor_mask_entry_omitted_value (F)
  3. L20
    specialize divisor_mask_entry_omitted_value (n)
  4. L21
    specialize divisor_mask_entry_omitted_value (d)
  5. L22
    specialize divisor_mask_entry_omitted_value (x)
  6. L23
    apply divisor_mask_entry_omitted_value
  7. L24
    exact hc
  8. L25
    specialize hm_right (d)
  9. L26
    specialize hm_right (x)
  10. L27
    apply hm_right
06Use earlier factsL28–29

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

  1. L28
    exact hbound
  2. L29
    exact hu_witness
07Calculate and transport equalitiesL30–31

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

  1. L30
    rewrite heq at hu_witness
  2. L31
    rewrite heq at hu_witness
08Use earlier factsL32–32

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

  1. L32
    exact hu_witness

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro F
  2. 0002intro n
  3. 0003intro l
  4. 0004intro M
  5. 0005intro d
  6. 0006intro hm
  7. 0007intro hbound
  8. 0008intro hc
  9. 0009cases hm
  10. 0010have hu : exists u. (exists dst_positive_code_omit_actual_lookup dst_positive_scale_omit_actual_lookup dst_negative_code_omit_actual_lookup dst_negative_scale_omit_actual_lookup dst_positive_omit_actual_lookup dst_negative_omit_actual_lookup. (((M) = (((((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) * S ((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) + ((dst_positive_scale_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))) * S ((((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) * S ((dst_positive_code_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup)) + ((dst_positive_scale_omit_actual_lookup) + (dst_positive_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))) + ((((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup))) + (((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) * S ((dst_negative_code_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)) + ((dst_negative_scale_omit_actual_lookup) + (dst_negative_scale_omit_actual_lookup)))))) /\ (((((exists ff_h_pvs_omit_actual_lookuppositive. ff_h_pvs_omit_actual_lookuppositive + S (dst_positive_omit_actual_lookup) = S ((S (d)) * dst_positive_scale_omit_actual_lookup)) /\ exists ff_q_pvs_omit_actual_lookuppositive. dst_positive_code_omit_actual_lookup = ff_q_pvs_omit_actual_lookuppositive * S ((S (d)) * dst_positive_scale_omit_actual_lookup) + (dst_positive_omit_actual_lookup))) /\ (((((exists ff_h_pvs_omit_actual_lookupnegative. ff_h_pvs_omit_actual_lookupnegative + S (dst_negative_omit_actual_lookup) = S ((S (d)) * dst_negative_scale_omit_actual_lookup)) /\ exists ff_q_pvs_omit_actual_lookupnegative. dst_negative_code_omit_actual_lookup = ff_q_pvs_omit_actual_lookupnegative * S ((S (d)) * dst_negative_scale_omit_actual_lookup) + (dst_negative_omit_actual_lookup))) /\ (exists ge_balance_positive_omit_actual_lookupvalue ge_balance_negative_omit_actual_lookupvalue. (((((u) = 2 * (ge_balance_positive_omit_actual_lookupvalue) /\ (ge_balance_negative_omit_actual_lookupvalue) = 0) \/ exists ge_signed_half_omit_actual_lookupvaluedecode. (((u) = 2 * ge_signed_half_omit_actual_lookupvaluedecode + 1 /\ (ge_balance_positive_omit_actual_lookupvalue) = 0) /\ (ge_balance_negative_omit_actual_lookupvalue) = S ge_signed_half_omit_actual_lookupvaluedecode))) /\ ((dst_positive_omit_actual_lookup) + ge_balance_negative_omit_actual_lookupvalue = (dst_negative_omit_actual_lookup) + ge_balance_positive_omit_actual_lookupvalue)))))))))
  11. 0011specialize divisor_signed_table_lookup (l)
  12. 0012specialize divisor_signed_table_lookup (M)
  13. 0013specialize divisor_signed_table_lookup (d)
  14. 0014apply divisor_signed_table_lookup
  15. 0015exact hm_left
  16. 0016exact hbound
  17. 0017cases hu
  18. 0018have heq : x=0
  19. 0019specialize divisor_mask_entry_omitted_value (F)
  20. 0020specialize divisor_mask_entry_omitted_value (n)
  21. 0021specialize divisor_mask_entry_omitted_value (d)
  22. 0022specialize divisor_mask_entry_omitted_value (x)
  23. 0023apply divisor_mask_entry_omitted_value
  24. 0024exact hc
  25. 0025specialize hm_right (d)
  26. 0026specialize hm_right (x)
  27. 0027apply hm_right
  28. 0028exact hbound
  29. 0029exact hu_witness
  30. 0030rewrite heq at hu_witness
  31. 0031rewrite heq at hu_witness
  32. 0032exact hu_witness