DV001C

divisor_mask_positive_quotient_entry

The constructed mask retains precisely the canonical input value at every witnessed positive divisor inside its finite domain.

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

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

A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.

Exact theorem in conservative defined notation

∀ F. ∀ n. ∀ l. ∀ M. ∀ d. ∀ q. ∀ z. DivisorMask(F,n,l,M) → Le(d,l) → ¬d = 0 → n = d · q → ArithAt(F,d,z) → ArithAt(M,d,z)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ArithAt(F,i,z) · 3DivisorMask(F,n,l,M) · 1Le(a,b) · 1

Actual proof prerequisites

divisor_signed_table_lookup · checked external prerequisitedivisor_mask_entry_functionaldivisor_mask_entry_from_quotient
Original expanded first-order statement 
forall F n l M d q z. (((exists dst_positive_code_keep_masktable dst_positive_scale_keep_masktable dst_negative_code_keep_masktable dst_negative_scale_keep_masktable. (((M) = (((((dst_positive_code_keep_masktable) + (dst_positive_scale_keep_masktable)) * S ((dst_positive_code_keep_masktable) + (dst_positive_scale_keep_masktable)) + ((dst_positive_scale_keep_masktable) + (dst_positive_scale_keep_masktable))) + (((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) * S ((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) + ((dst_negative_scale_keep_masktable) + (dst_negative_scale_keep_masktable)))) * S ((((dst_positive_code_keep_masktable) + (dst_positive_scale_keep_masktable)) * S ((dst_positive_code_keep_masktable) + (dst_positive_scale_keep_masktable)) + ((dst_positive_scale_keep_masktable) + (dst_positive_scale_keep_masktable))) + (((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) * S ((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) + ((dst_negative_scale_keep_masktable) + (dst_negative_scale_keep_masktable)))) + ((((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) * S ((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) + ((dst_negative_scale_keep_masktable) + (dst_negative_scale_keep_masktable))) + (((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) * S ((dst_negative_code_keep_masktable) + (dst_negative_scale_keep_masktable)) + ((dst_negative_scale_keep_masktable) + (dst_negative_scale_keep_masktable)))))) /\ (forall dst_index_keep_masktable. (exists pvs_le_gap_keep_masktabledomain. pvs_le_gap_keep_masktabledomain + (dst_index_keep_masktable) = (l)) -> exists dst_positive_keep_masktable dst_negative_keep_masktable dst_value_keep_masktable. ((((exists ff_h_pvs_keep_masktableentrypositive. ff_h_pvs_keep_masktableentrypositive + S (dst_positive_keep_masktable) = S ((S (dst_index_keep_masktable)) * dst_positive_scale_keep_masktable)) /\ exists ff_q_pvs_keep_masktableentrypositive. dst_positive_code_keep_masktable = ff_q_pvs_keep_masktableentrypositive * S ((S (dst_index_keep_masktable)) * dst_positive_scale_keep_masktable) + (dst_positive_keep_masktable))) /\ (((((exists ff_h_pvs_keep_masktableentrynegative. ff_h_pvs_keep_masktableentrynegative + S (dst_negative_keep_masktable) = S ((S (dst_index_keep_masktable)) * dst_negative_scale_keep_masktable)) /\ exists ff_q_pvs_keep_masktableentrynegative. dst_negative_code_keep_masktable = ff_q_pvs_keep_masktableentrynegative * S ((S (dst_index_keep_masktable)) * dst_negative_scale_keep_masktable) + (dst_negative_keep_masktable))) /\ (exists ge_balance_positive_keep_masktableentryvalue ge_balance_negative_keep_masktableentryvalue. (((((dst_value_keep_masktable) = 2 * (ge_balance_positive_keep_masktableentryvalue) /\ (ge_balance_negative_keep_masktableentryvalue) = 0) \/ exists ge_signed_half_keep_masktableentryvaluedecode. (((dst_value_keep_masktable) = 2 * ge_signed_half_keep_masktableentryvaluedecode + 1 /\ (ge_balance_positive_keep_masktableentryvalue) = 0) /\ (ge_balance_negative_keep_masktableentryvalue) = S ge_signed_half_keep_masktableentryvaluedecode))) /\ ((dst_positive_keep_masktable) + ge_balance_negative_keep_masktableentryvalue = (dst_negative_keep_masktable) + ge_balance_positive_keep_masktableentryvalue))))))))) /\ (forall dm_index_keep_mask dm_value_keep_mask. (exists pvs_le_gap_keep_maskdomain. pvs_le_gap_keep_maskdomain + (dm_index_keep_mask) = (l)) -> (exists dst_positive_code_keep_masklookup dst_positive_scale_keep_masklookup dst_negative_code_keep_masklookup dst_negative_scale_keep_masklookup dst_positive_keep_masklookup dst_negative_keep_masklookup. (((M) = (((((dst_positive_code_keep_masklookup) + (dst_positive_scale_keep_masklookup)) * S ((dst_positive_code_keep_masklookup) + (dst_positive_scale_keep_masklookup)) + ((dst_positive_scale_keep_masklookup) + (dst_positive_scale_keep_masklookup))) + (((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) * S ((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) + ((dst_negative_scale_keep_masklookup) + (dst_negative_scale_keep_masklookup)))) * S ((((dst_positive_code_keep_masklookup) + (dst_positive_scale_keep_masklookup)) * S ((dst_positive_code_keep_masklookup) + (dst_positive_scale_keep_masklookup)) + ((dst_positive_scale_keep_masklookup) + (dst_positive_scale_keep_masklookup))) + (((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) * S ((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) + ((dst_negative_scale_keep_masklookup) + (dst_negative_scale_keep_masklookup)))) + ((((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) * S ((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) + ((dst_negative_scale_keep_masklookup) + (dst_negative_scale_keep_masklookup))) + (((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) * S ((dst_negative_code_keep_masklookup) + (dst_negative_scale_keep_masklookup)) + ((dst_negative_scale_keep_masklookup) + (dst_negative_scale_keep_masklookup)))))) /\ (((((exists ff_h_pvs_keep_masklookuppositive. ff_h_pvs_keep_masklookuppositive + S (dst_positive_keep_masklookup) = S ((S (dm_index_keep_mask)) * dst_positive_scale_keep_masklookup)) /\ exists ff_q_pvs_keep_masklookuppositive. dst_positive_code_keep_masklookup = ff_q_pvs_keep_masklookuppositive * S ((S (dm_index_keep_mask)) * dst_positive_scale_keep_masklookup) + (dst_positive_keep_masklookup))) /\ (((((exists ff_h_pvs_keep_masklookupnegative. ff_h_pvs_keep_masklookupnegative + S (dst_negative_keep_masklookup) = S ((S (dm_index_keep_mask)) * dst_negative_scale_keep_masklookup)) /\ exists ff_q_pvs_keep_masklookupnegative. dst_negative_code_keep_masklookup = ff_q_pvs_keep_masklookupnegative * S ((S (dm_index_keep_mask)) * dst_negative_scale_keep_masklookup) + (dst_negative_keep_masklookup))) /\ (exists ge_balance_positive_keep_masklookupvalue ge_balance_negative_keep_masklookupvalue. (((((dm_value_keep_mask) = 2 * (ge_balance_positive_keep_masklookupvalue) /\ (ge_balance_negative_keep_masklookupvalue) = 0) \/ exists ge_signed_half_keep_masklookupvaluedecode. (((dm_value_keep_mask) = 2 * ge_signed_half_keep_masklookupvaluedecode + 1 /\ (ge_balance_positive_keep_masklookupvalue) = 0) /\ (ge_balance_negative_keep_masklookupvalue) = S ge_signed_half_keep_masklookupvaluedecode))) /\ ((dst_positive_keep_masklookup) + ge_balance_negative_keep_masklookupvalue = (dst_negative_keep_masklookup) + ge_balance_positive_keep_masklookupvalue))))))))) -> ((((~((dm_index_keep_mask)=0)) /\ (exists dm_quotient_keep_maskentry. (((n)=(dm_index_keep_mask)*dm_quotient_keep_maskentry) /\ (exists dst_positive_code_keep_maskentryinput dst_positive_scale_keep_maskentryinput dst_negative_code_keep_maskentryinput dst_negative_scale_keep_maskentryinput dst_positive_keep_maskentryinput dst_negative_keep_maskentryinput. (((F) = (((((dst_positive_code_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput)) * S ((dst_positive_code_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput)) + ((dst_positive_scale_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput))) + (((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) * S ((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) + ((dst_negative_scale_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)))) * S ((((dst_positive_code_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput)) * S ((dst_positive_code_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput)) + ((dst_positive_scale_keep_maskentryinput) + (dst_positive_scale_keep_maskentryinput))) + (((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) * S ((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) + ((dst_negative_scale_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)))) + ((((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) * S ((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) + ((dst_negative_scale_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput))) + (((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) * S ((dst_negative_code_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)) + ((dst_negative_scale_keep_maskentryinput) + (dst_negative_scale_keep_maskentryinput)))))) /\ (((((exists ff_h_pvs_keep_maskentryinputpositive. ff_h_pvs_keep_maskentryinputpositive + S (dst_positive_keep_maskentryinput) = S ((S (dm_index_keep_mask)) * dst_positive_scale_keep_maskentryinput)) /\ exists ff_q_pvs_keep_maskentryinputpositive. dst_positive_code_keep_maskentryinput = ff_q_pvs_keep_maskentryinputpositive * S ((S (dm_index_keep_mask)) * dst_positive_scale_keep_maskentryinput) + (dst_positive_keep_maskentryinput))) /\ (((((exists ff_h_pvs_keep_maskentryinputnegative. ff_h_pvs_keep_maskentryinputnegative + S (dst_negative_keep_maskentryinput) = S ((S (dm_index_keep_mask)) * dst_negative_scale_keep_maskentryinput)) /\ exists ff_q_pvs_keep_maskentryinputnegative. dst_negative_code_keep_maskentryinput = ff_q_pvs_keep_maskentryinputnegative * S ((S (dm_index_keep_mask)) * dst_negative_scale_keep_maskentryinput) + (dst_negative_keep_maskentryinput))) /\ (exists ge_balance_positive_keep_maskentryinputvalue ge_balance_negative_keep_maskentryinputvalue. (((((dm_value_keep_mask) = 2 * (ge_balance_positive_keep_maskentryinputvalue) /\ (ge_balance_negative_keep_maskentryinputvalue) = 0) \/ exists ge_signed_half_keep_maskentryinputvaluedecode. (((dm_value_keep_mask) = 2 * ge_signed_half_keep_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_keep_maskentryinputvalue) = 0) /\ (ge_balance_negative_keep_maskentryinputvalue) = S ge_signed_half_keep_maskentryinputvaluedecode))) /\ ((dst_positive_keep_maskentryinput) + ge_balance_negative_keep_maskentryinputvalue = (dst_negative_keep_maskentryinput) + ge_balance_positive_keep_maskentryinputvalue))))))))))))) \/ ((((dm_index_keep_mask)=0 \/ ~(exists pvs_factor_keep_maskentrynondivisor. (n) = (dm_index_keep_mask) * pvs_factor_keep_maskentrynondivisor)) /\ ((dm_value_keep_mask)=0))))))) -> (exists pvs_le_gap_keep_bound. pvs_le_gap_keep_bound + (d) = (l)) -> ~(d=0) -> n=d*q -> (exists dst_positive_code_keep_source dst_positive_scale_keep_source dst_negative_code_keep_source dst_negative_scale_keep_source dst_positive_keep_source dst_negative_keep_source. (((F) = (((((dst_positive_code_keep_source) + (dst_positive_scale_keep_source)) * S ((dst_positive_code_keep_source) + (dst_positive_scale_keep_source)) + ((dst_positive_scale_keep_source) + (dst_positive_scale_keep_source))) + (((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) * S ((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) + ((dst_negative_scale_keep_source) + (dst_negative_scale_keep_source)))) * S ((((dst_positive_code_keep_source) + (dst_positive_scale_keep_source)) * S ((dst_positive_code_keep_source) + (dst_positive_scale_keep_source)) + ((dst_positive_scale_keep_source) + (dst_positive_scale_keep_source))) + (((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) * S ((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) + ((dst_negative_scale_keep_source) + (dst_negative_scale_keep_source)))) + ((((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) * S ((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) + ((dst_negative_scale_keep_source) + (dst_negative_scale_keep_source))) + (((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) * S ((dst_negative_code_keep_source) + (dst_negative_scale_keep_source)) + ((dst_negative_scale_keep_source) + (dst_negative_scale_keep_source)))))) /\ (((((exists ff_h_pvs_keep_sourcepositive. ff_h_pvs_keep_sourcepositive + S (dst_positive_keep_source) = S ((S (d)) * dst_positive_scale_keep_source)) /\ exists ff_q_pvs_keep_sourcepositive. dst_positive_code_keep_source = ff_q_pvs_keep_sourcepositive * S ((S (d)) * dst_positive_scale_keep_source) + (dst_positive_keep_source))) /\ (((((exists ff_h_pvs_keep_sourcenegative. ff_h_pvs_keep_sourcenegative + S (dst_negative_keep_source) = S ((S (d)) * dst_negative_scale_keep_source)) /\ exists ff_q_pvs_keep_sourcenegative. dst_negative_code_keep_source = ff_q_pvs_keep_sourcenegative * S ((S (d)) * dst_negative_scale_keep_source) + (dst_negative_keep_source))) /\ (exists ge_balance_positive_keep_sourcevalue ge_balance_negative_keep_sourcevalue. (((((z) = 2 * (ge_balance_positive_keep_sourcevalue) /\ (ge_balance_negative_keep_sourcevalue) = 0) \/ exists ge_signed_half_keep_sourcevaluedecode. (((z) = 2 * ge_signed_half_keep_sourcevaluedecode + 1 /\ (ge_balance_positive_keep_sourcevalue) = 0) /\ (ge_balance_negative_keep_sourcevalue) = S ge_signed_half_keep_sourcevaluedecode))) /\ ((dst_positive_keep_source) + ge_balance_negative_keep_sourcevalue = (dst_negative_keep_source) + ge_balance_positive_keep_sourcevalue))))))))) -> (exists dst_positive_code_keep_mask_entry dst_positive_scale_keep_mask_entry dst_negative_code_keep_mask_entry dst_negative_scale_keep_mask_entry dst_positive_keep_mask_entry dst_negative_keep_mask_entry. (((M) = (((((dst_positive_code_keep_mask_entry) + (dst_positive_scale_keep_mask_entry)) * S ((dst_positive_code_keep_mask_entry) + (dst_positive_scale_keep_mask_entry)) + ((dst_positive_scale_keep_mask_entry) + (dst_positive_scale_keep_mask_entry))) + (((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) * S ((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) + ((dst_negative_scale_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)))) * S ((((dst_positive_code_keep_mask_entry) + (dst_positive_scale_keep_mask_entry)) * S ((dst_positive_code_keep_mask_entry) + (dst_positive_scale_keep_mask_entry)) + ((dst_positive_scale_keep_mask_entry) + (dst_positive_scale_keep_mask_entry))) + (((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) * S ((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) + ((dst_negative_scale_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)))) + ((((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) * S ((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) + ((dst_negative_scale_keep_mask_entry) + (dst_negative_scale_keep_mask_entry))) + (((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) * S ((dst_negative_code_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)) + ((dst_negative_scale_keep_mask_entry) + (dst_negative_scale_keep_mask_entry)))))) /\ (((((exists ff_h_pvs_keep_mask_entrypositive. ff_h_pvs_keep_mask_entrypositive + S (dst_positive_keep_mask_entry) = S ((S (d)) * dst_positive_scale_keep_mask_entry)) /\ exists ff_q_pvs_keep_mask_entrypositive. dst_positive_code_keep_mask_entry = ff_q_pvs_keep_mask_entrypositive * S ((S (d)) * dst_positive_scale_keep_mask_entry) + (dst_positive_keep_mask_entry))) /\ (((((exists ff_h_pvs_keep_mask_entrynegative. ff_h_pvs_keep_mask_entrynegative + S (dst_negative_keep_mask_entry) = S ((S (d)) * dst_negative_scale_keep_mask_entry)) /\ exists ff_q_pvs_keep_mask_entrynegative. dst_negative_code_keep_mask_entry = ff_q_pvs_keep_mask_entrynegative * S ((S (d)) * dst_negative_scale_keep_mask_entry) + (dst_negative_keep_mask_entry))) /\ (exists ge_balance_positive_keep_mask_entryvalue ge_balance_negative_keep_mask_entryvalue. (((((z) = 2 * (ge_balance_positive_keep_mask_entryvalue) /\ (ge_balance_negative_keep_mask_entryvalue) = 0) \/ exists ge_signed_half_keep_mask_entryvaluedecode. (((z) = 2 * ge_signed_half_keep_mask_entryvaluedecode + 1 /\ (ge_balance_positive_keep_mask_entryvalue) = 0) /\ (ge_balance_negative_keep_mask_entryvalue) = S ge_signed_half_keep_mask_entryvaluedecode))) /\ ((dst_positive_keep_mask_entry) + ge_balance_negative_keep_mask_entryvalue = (dst_negative_keep_mask_entry) + ge_balance_positive_keep_mask_entryvalue)))))))))

Complete tactic proof in conservative notation

All 45 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

45 script commands · 10 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
divisor mask entry functionaldivisor mask entry from quotient
01Fix variables and assumptionsL1–10

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 q
  7. L7
    intro z
  8. L8
    intro hm
  9. L9
    intro hbound
  10. L10
    intro hd
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hq
  2. L12
    intro hz
03Separate the logical casesL13–13

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

  1. L13
    cases hm
04Establish huL14–20

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

  1. L14
    have hu : ∃ u. ArithAt(M,d,u)Definitions: ArithAt(M,d,u)Original native command in the exact edition
  2. L15
    specialize divisor_signed_table_lookup (l)
  3. L16
    specialize divisor_signed_table_lookup (M)
  4. L17
    specialize divisor_signed_table_lookup (d)
  5. L18
    apply divisor_signed_table_lookup
  6. L19
    exact hm_left
  7. L20
    exact hbound
05Separate the logical casesL21–21

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

  1. L21
    cases hu
06Establish heqL22–31

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

  1. L22
    have heq : x=z
  2. L23
    specialize divisor_mask_entry_functional (F)
  3. L24
    specialize divisor_mask_entry_functional (n)
  4. L25
    specialize divisor_mask_entry_functional (d)
  5. L26
    specialize divisor_mask_entry_functional (x)
  6. L27
    specialize divisor_mask_entry_functional (z)
  7. L28
    apply divisor_mask_entry_functional
  8. L29
    specialize hm_right (d)
  9. L30
    specialize hm_right (x)
  10. L31
    apply hm_right
07Use earlier factsL32–41

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

  1. L32
    exact hbound
  2. L33
    exact hu_witness
  3. L34
    specialize divisor_mask_entry_from_quotient (F)
  4. L35
    specialize divisor_mask_entry_from_quotient (n)
  5. L36
    specialize divisor_mask_entry_from_quotient (d)
  6. L37
    specialize divisor_mask_entry_from_quotient (q)
  7. L38
    specialize divisor_mask_entry_from_quotient (z)
  8. L39
    apply divisor_mask_entry_from_quotient
  9. L40
    exact hd
  10. L41
    exact hq
08Use earlier factsL42–42

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

  1. L42
    exact hz
09Calculate and transport equalitiesL43–44

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

  1. L43
    rewrite heq at hu_witness
  2. L44
    rewrite heq at hu_witness
10Use earlier factsL45–45

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

  1. L45
    exact hu_witness

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro F
  2. 0002intro n
  3. 0003intro l
  4. 0004intro M
  5. 0005intro d
  6. 0006intro q
  7. 0007intro z
  8. 0008intro hm
  9. 0009intro hbound
  10. 0010intro hd
  11. 0011intro hq
  12. 0012intro hz
  13. 0013cases hm
  14. 0014have hu : ∃ u. ArithAt(M,d,u)
  15. 0015specialize divisor_signed_table_lookup (l)
  16. 0016specialize divisor_signed_table_lookup (M)
  17. 0017specialize divisor_signed_table_lookup (d)
  18. 0018apply divisor_signed_table_lookup
  19. 0019exact hm_left
  20. 0020exact hbound
  21. 0021cases hu
  22. 0022have heq : x=z
  23. 0023specialize divisor_mask_entry_functional (F)
  24. 0024specialize divisor_mask_entry_functional (n)
  25. 0025specialize divisor_mask_entry_functional (d)
  26. 0026specialize divisor_mask_entry_functional (x)
  27. 0027specialize divisor_mask_entry_functional (z)
  28. 0028apply divisor_mask_entry_functional
  29. 0029specialize hm_right (d)
  30. 0030specialize hm_right (x)
  31. 0031apply hm_right
  32. 0032exact hbound
  33. 0033exact hu_witness
  34. 0034specialize divisor_mask_entry_from_quotient (F)
  35. 0035specialize divisor_mask_entry_from_quotient (n)
  36. 0036specialize divisor_mask_entry_from_quotient (d)
  37. 0037specialize divisor_mask_entry_from_quotient (q)
  38. 0038specialize divisor_mask_entry_from_quotient (z)
  39. 0039apply divisor_mask_entry_from_quotient
  40. 0040exact hd
  41. 0041exact hq
  42. 0042exact hz
  43. 0043rewrite heq at hu_witness
  44. 0044rewrite heq at hu_witness
  45. 0045exact hu_witness