DV0019

divisor_mask_prefix_exists

Ordinary prefix induction constructs every finite divisor mask inside the actual source domain, with explicit beta extensions at each step.

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

∀ N. ∀ F. ∀ n. ∀ l. ArithTable(N,F) → Le(l,N) → ∃ x. DivisorMask(F,n,l,x)

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

Definition DAG

ArithTable(N,F) · 2ArithAt(F,i,z) · 1ArithTableEqual(F,G,l) · 1DivisorMaskEntry(F,n,d,z) · 1DivisorMask(F,n,l,M) · 3Le(a,b) · 2

Actual proof prerequisites

arithmetic_signed_table_singletondivisor_mask_prefix_zero_constructorle_trans · checked external prerequisitele_succ_self · checked external prerequisitedivisor_mask_entry_existsdivisor_mask_prefix_append
Original expanded first-order statement 
forall N F n l. (exists dst_positive_code_exists_input dst_positive_scale_exists_input dst_negative_code_exists_input dst_negative_scale_exists_input. (((F) = (((((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) * S ((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) + ((dst_positive_scale_exists_input) + (dst_positive_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))) * S ((((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) * S ((dst_positive_code_exists_input) + (dst_positive_scale_exists_input)) + ((dst_positive_scale_exists_input) + (dst_positive_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))) + ((((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input))) + (((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) * S ((dst_negative_code_exists_input) + (dst_negative_scale_exists_input)) + ((dst_negative_scale_exists_input) + (dst_negative_scale_exists_input)))))) /\ (forall dst_index_exists_input. (exists pvs_le_gap_exists_inputdomain. pvs_le_gap_exists_inputdomain + (dst_index_exists_input) = (N)) -> exists dst_positive_exists_input dst_negative_exists_input dst_value_exists_input. ((((exists ff_h_pvs_exists_inputentrypositive. ff_h_pvs_exists_inputentrypositive + S (dst_positive_exists_input) = S ((S (dst_index_exists_input)) * dst_positive_scale_exists_input)) /\ exists ff_q_pvs_exists_inputentrypositive. dst_positive_code_exists_input = ff_q_pvs_exists_inputentrypositive * S ((S (dst_index_exists_input)) * dst_positive_scale_exists_input) + (dst_positive_exists_input))) /\ (((((exists ff_h_pvs_exists_inputentrynegative. ff_h_pvs_exists_inputentrynegative + S (dst_negative_exists_input) = S ((S (dst_index_exists_input)) * dst_negative_scale_exists_input)) /\ exists ff_q_pvs_exists_inputentrynegative. dst_negative_code_exists_input = ff_q_pvs_exists_inputentrynegative * S ((S (dst_index_exists_input)) * dst_negative_scale_exists_input) + (dst_negative_exists_input))) /\ (exists ge_balance_positive_exists_inputentryvalue ge_balance_negative_exists_inputentryvalue. (((((dst_value_exists_input) = 2 * (ge_balance_positive_exists_inputentryvalue) /\ (ge_balance_negative_exists_inputentryvalue) = 0) \/ exists ge_signed_half_exists_inputentryvaluedecode. (((dst_value_exists_input) = 2 * ge_signed_half_exists_inputentryvaluedecode + 1 /\ (ge_balance_positive_exists_inputentryvalue) = 0) /\ (ge_balance_negative_exists_inputentryvalue) = S ge_signed_half_exists_inputentryvaluedecode))) /\ ((dst_positive_exists_input) + ge_balance_negative_exists_inputentryvalue = (dst_negative_exists_input) + ge_balance_positive_exists_inputentryvalue))))))))) -> (exists pvs_le_gap_exists_bound. pvs_le_gap_exists_bound + (l) = (N)) -> exists M. (((exists dst_positive_code_exists_masktable dst_positive_scale_exists_masktable dst_negative_code_exists_masktable dst_negative_scale_exists_masktable. (((M) = (((((dst_positive_code_exists_masktable) + (dst_positive_scale_exists_masktable)) * S ((dst_positive_code_exists_masktable) + (dst_positive_scale_exists_masktable)) + ((dst_positive_scale_exists_masktable) + (dst_positive_scale_exists_masktable))) + (((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) * S ((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) + ((dst_negative_scale_exists_masktable) + (dst_negative_scale_exists_masktable)))) * S ((((dst_positive_code_exists_masktable) + (dst_positive_scale_exists_masktable)) * S ((dst_positive_code_exists_masktable) + (dst_positive_scale_exists_masktable)) + ((dst_positive_scale_exists_masktable) + (dst_positive_scale_exists_masktable))) + (((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) * S ((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) + ((dst_negative_scale_exists_masktable) + (dst_negative_scale_exists_masktable)))) + ((((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) * S ((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) + ((dst_negative_scale_exists_masktable) + (dst_negative_scale_exists_masktable))) + (((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) * S ((dst_negative_code_exists_masktable) + (dst_negative_scale_exists_masktable)) + ((dst_negative_scale_exists_masktable) + (dst_negative_scale_exists_masktable)))))) /\ (forall dst_index_exists_masktable. (exists pvs_le_gap_exists_masktabledomain. pvs_le_gap_exists_masktabledomain + (dst_index_exists_masktable) = (l)) -> exists dst_positive_exists_masktable dst_negative_exists_masktable dst_value_exists_masktable. ((((exists ff_h_pvs_exists_masktableentrypositive. ff_h_pvs_exists_masktableentrypositive + S (dst_positive_exists_masktable) = S ((S (dst_index_exists_masktable)) * dst_positive_scale_exists_masktable)) /\ exists ff_q_pvs_exists_masktableentrypositive. dst_positive_code_exists_masktable = ff_q_pvs_exists_masktableentrypositive * S ((S (dst_index_exists_masktable)) * dst_positive_scale_exists_masktable) + (dst_positive_exists_masktable))) /\ (((((exists ff_h_pvs_exists_masktableentrynegative. ff_h_pvs_exists_masktableentrynegative + S (dst_negative_exists_masktable) = S ((S (dst_index_exists_masktable)) * dst_negative_scale_exists_masktable)) /\ exists ff_q_pvs_exists_masktableentrynegative. dst_negative_code_exists_masktable = ff_q_pvs_exists_masktableentrynegative * S ((S (dst_index_exists_masktable)) * dst_negative_scale_exists_masktable) + (dst_negative_exists_masktable))) /\ (exists ge_balance_positive_exists_masktableentryvalue ge_balance_negative_exists_masktableentryvalue. (((((dst_value_exists_masktable) = 2 * (ge_balance_positive_exists_masktableentryvalue) /\ (ge_balance_negative_exists_masktableentryvalue) = 0) \/ exists ge_signed_half_exists_masktableentryvaluedecode. (((dst_value_exists_masktable) = 2 * ge_signed_half_exists_masktableentryvaluedecode + 1 /\ (ge_balance_positive_exists_masktableentryvalue) = 0) /\ (ge_balance_negative_exists_masktableentryvalue) = S ge_signed_half_exists_masktableentryvaluedecode))) /\ ((dst_positive_exists_masktable) + ge_balance_negative_exists_masktableentryvalue = (dst_negative_exists_masktable) + ge_balance_positive_exists_masktableentryvalue))))))))) /\ (forall dm_index_exists_mask dm_value_exists_mask. (exists pvs_le_gap_exists_maskdomain. pvs_le_gap_exists_maskdomain + (dm_index_exists_mask) = (l)) -> (exists dst_positive_code_exists_masklookup dst_positive_scale_exists_masklookup dst_negative_code_exists_masklookup dst_negative_scale_exists_masklookup dst_positive_exists_masklookup dst_negative_exists_masklookup. (((M) = (((((dst_positive_code_exists_masklookup) + (dst_positive_scale_exists_masklookup)) * S ((dst_positive_code_exists_masklookup) + (dst_positive_scale_exists_masklookup)) + ((dst_positive_scale_exists_masklookup) + (dst_positive_scale_exists_masklookup))) + (((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) * S ((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) + ((dst_negative_scale_exists_masklookup) + (dst_negative_scale_exists_masklookup)))) * S ((((dst_positive_code_exists_masklookup) + (dst_positive_scale_exists_masklookup)) * S ((dst_positive_code_exists_masklookup) + (dst_positive_scale_exists_masklookup)) + ((dst_positive_scale_exists_masklookup) + (dst_positive_scale_exists_masklookup))) + (((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) * S ((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) + ((dst_negative_scale_exists_masklookup) + (dst_negative_scale_exists_masklookup)))) + ((((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) * S ((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) + ((dst_negative_scale_exists_masklookup) + (dst_negative_scale_exists_masklookup))) + (((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) * S ((dst_negative_code_exists_masklookup) + (dst_negative_scale_exists_masklookup)) + ((dst_negative_scale_exists_masklookup) + (dst_negative_scale_exists_masklookup)))))) /\ (((((exists ff_h_pvs_exists_masklookuppositive. ff_h_pvs_exists_masklookuppositive + S (dst_positive_exists_masklookup) = S ((S (dm_index_exists_mask)) * dst_positive_scale_exists_masklookup)) /\ exists ff_q_pvs_exists_masklookuppositive. dst_positive_code_exists_masklookup = ff_q_pvs_exists_masklookuppositive * S ((S (dm_index_exists_mask)) * dst_positive_scale_exists_masklookup) + (dst_positive_exists_masklookup))) /\ (((((exists ff_h_pvs_exists_masklookupnegative. ff_h_pvs_exists_masklookupnegative + S (dst_negative_exists_masklookup) = S ((S (dm_index_exists_mask)) * dst_negative_scale_exists_masklookup)) /\ exists ff_q_pvs_exists_masklookupnegative. dst_negative_code_exists_masklookup = ff_q_pvs_exists_masklookupnegative * S ((S (dm_index_exists_mask)) * dst_negative_scale_exists_masklookup) + (dst_negative_exists_masklookup))) /\ (exists ge_balance_positive_exists_masklookupvalue ge_balance_negative_exists_masklookupvalue. (((((dm_value_exists_mask) = 2 * (ge_balance_positive_exists_masklookupvalue) /\ (ge_balance_negative_exists_masklookupvalue) = 0) \/ exists ge_signed_half_exists_masklookupvaluedecode. (((dm_value_exists_mask) = 2 * ge_signed_half_exists_masklookupvaluedecode + 1 /\ (ge_balance_positive_exists_masklookupvalue) = 0) /\ (ge_balance_negative_exists_masklookupvalue) = S ge_signed_half_exists_masklookupvaluedecode))) /\ ((dst_positive_exists_masklookup) + ge_balance_negative_exists_masklookupvalue = (dst_negative_exists_masklookup) + ge_balance_positive_exists_masklookupvalue))))))))) -> ((((~((dm_index_exists_mask)=0)) /\ (exists dm_quotient_exists_maskentry. (((n)=(dm_index_exists_mask)*dm_quotient_exists_maskentry) /\ (exists dst_positive_code_exists_maskentryinput dst_positive_scale_exists_maskentryinput dst_negative_code_exists_maskentryinput dst_negative_scale_exists_maskentryinput dst_positive_exists_maskentryinput dst_negative_exists_maskentryinput. (((F) = (((((dst_positive_code_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput)) * S ((dst_positive_code_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput)) + ((dst_positive_scale_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput))) + (((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) * S ((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) + ((dst_negative_scale_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)))) * S ((((dst_positive_code_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput)) * S ((dst_positive_code_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput)) + ((dst_positive_scale_exists_maskentryinput) + (dst_positive_scale_exists_maskentryinput))) + (((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) * S ((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) + ((dst_negative_scale_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)))) + ((((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) * S ((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) + ((dst_negative_scale_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput))) + (((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) * S ((dst_negative_code_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)) + ((dst_negative_scale_exists_maskentryinput) + (dst_negative_scale_exists_maskentryinput)))))) /\ (((((exists ff_h_pvs_exists_maskentryinputpositive. ff_h_pvs_exists_maskentryinputpositive + S (dst_positive_exists_maskentryinput) = S ((S (dm_index_exists_mask)) * dst_positive_scale_exists_maskentryinput)) /\ exists ff_q_pvs_exists_maskentryinputpositive. dst_positive_code_exists_maskentryinput = ff_q_pvs_exists_maskentryinputpositive * S ((S (dm_index_exists_mask)) * dst_positive_scale_exists_maskentryinput) + (dst_positive_exists_maskentryinput))) /\ (((((exists ff_h_pvs_exists_maskentryinputnegative. ff_h_pvs_exists_maskentryinputnegative + S (dst_negative_exists_maskentryinput) = S ((S (dm_index_exists_mask)) * dst_negative_scale_exists_maskentryinput)) /\ exists ff_q_pvs_exists_maskentryinputnegative. dst_negative_code_exists_maskentryinput = ff_q_pvs_exists_maskentryinputnegative * S ((S (dm_index_exists_mask)) * dst_negative_scale_exists_maskentryinput) + (dst_negative_exists_maskentryinput))) /\ (exists ge_balance_positive_exists_maskentryinputvalue ge_balance_negative_exists_maskentryinputvalue. (((((dm_value_exists_mask) = 2 * (ge_balance_positive_exists_maskentryinputvalue) /\ (ge_balance_negative_exists_maskentryinputvalue) = 0) \/ exists ge_signed_half_exists_maskentryinputvaluedecode. (((dm_value_exists_mask) = 2 * ge_signed_half_exists_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_exists_maskentryinputvalue) = 0) /\ (ge_balance_negative_exists_maskentryinputvalue) = S ge_signed_half_exists_maskentryinputvaluedecode))) /\ ((dst_positive_exists_maskentryinput) + ge_balance_negative_exists_maskentryinputvalue = (dst_negative_exists_maskentryinput) + ge_balance_positive_exists_maskentryinputvalue))))))))))))) \/ ((((dm_index_exists_mask)=0 \/ ~(exists pvs_factor_exists_maskentrynondivisor. (n) = (dm_index_exists_mask) * pvs_factor_exists_maskentrynondivisor)) /\ ((dm_value_exists_mask)=0)))))))

Complete tactic proof in conservative notation

All 56 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

56 script commands · 16 reading checkpoints · 5 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 (4)
arithmetic signed table singletondivisor mask prefix zero constructordivisor mask entry existsdivisor mask prefix append
01Fix variables and assumptionsL1–4

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro n
  4. L4
    intro l
02Induction on lL5–7

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

  1. L5
    induction l
  2. L6
    intro ht
  3. L7
    intro hbound
03Establish hzeroL8–10

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

  1. L8
    have hzero : ∃ M. ArithTable(0,M) ∧ ArithAt(M,0,0)Definitions: ArithTable(0,M)ArithAt(M,0,0)Original native command in the exact edition
  2. L9
    specialize arithmetic_signed_table_singleton (0)
  3. L10
    apply arithmetic_signed_table_singleton
04Separate the logical casesL11–12

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

  1. L11
    cases hzero
  2. L12
    cases hzero_witness
05Construct an explicit witnessL13–13

Supply the displayed value, then prove that it has the required property.

  1. L13
    exists x
06Use earlier factsL14–19

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

  1. L14
    specialize divisor_mask_prefix_zero_constructor (F)
  2. L15
    specialize divisor_mask_prefix_zero_constructor (n)
  3. L16
    specialize divisor_mask_prefix_zero_constructor (x)
  4. L17
    apply divisor_mask_prefix_zero_constructor
  5. L18
    exact hzero_witness_left
  6. L19
    exact hzero_witness_right
07Fix variables and assumptionsL20–21

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

  1. L20
    intro ht
  2. L21
    intro hbound
08Establish hlowL22–29

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

  1. L22
  2. L23
    specialize le_trans (l)
  3. L24
    specialize le_trans (S l)
  4. L25
    specialize le_trans (N)
  5. L26
    apply le_trans
  6. L27
    specialize le_succ_self (l)
  7. L28
    apply le_succ_self
  8. L29
    exact hbound
09Establish hprevL30–33

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

  1. L30
    have hprev : ∃ M. DivisorMask(F,n,l,M)Definitions: DivisorMask(F,n,l,M)Original native command in the exact edition
  2. L31
    apply IH
  3. L32
    exact ht
  4. L33
    exact hlow
10Separate the logical casesL34–34

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

  1. L34
    cases hprev
11Establish hzL35–42

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

  1. L35
    have hz : ∃ z. DivisorMaskEntry(F,n,S l,z)Definitions: DivisorMaskEntry(F,n,S l,z)Original native command in the exact edition
  2. L36
    specialize divisor_mask_entry_exists (N)
  3. L37
    specialize divisor_mask_entry_exists (F)
  4. L38
    specialize divisor_mask_entry_exists (n)
  5. L39
    specialize divisor_mask_entry_exists (S l)
  6. L40
    apply divisor_mask_entry_exists
  7. L41
    exact ht
  8. L42
    exact hbound
12Separate the logical casesL43–43

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

  1. L43
    cases hz
13Establish hnextL44–52

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

  1. L44
    have hnext : ∃ G. DivisorMask(F,n,S l,G) ∧ ArithTableEqual(x,G,S l)Definitions: DivisorMask(F,n,S l,G)ArithTableEqual(x,G,S l)Original native command in the exact edition
  2. L45
    specialize divisor_mask_prefix_append (F)
  3. L46
    specialize divisor_mask_prefix_append (n)
  4. L47
    specialize divisor_mask_prefix_append (l)
  5. L48
    specialize divisor_mask_prefix_append (x)
  6. L49
    specialize divisor_mask_prefix_append (x1)
  7. L50
    apply divisor_mask_prefix_append
  8. L51
    exact hprev_witness
  9. L52
    exact hz_witness
14Separate the logical casesL53–54

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

  1. L53
    cases hnext
  2. L54
    cases hnext_witness
15Construct an explicit witnessL55–55

Supply the displayed value, then prove that it has the required property.

  1. L55
    exists x2
16Use earlier factsL56–56

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

  1. L56
    exact hnext_witness_left

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro n
  4. 0004intro l
  5. 0005induction l
  6. 0006intro ht
  7. 0007intro hbound
  8. 0008have hzero : ∃ M. ArithTable(0,M) ∧ ArithAt(M,0,0)
  9. 0009specialize arithmetic_signed_table_singleton (0)
  10. 0010apply arithmetic_signed_table_singleton
  11. 0011cases hzero
  12. 0012cases hzero_witness
  13. 0013exists x
  14. 0014specialize divisor_mask_prefix_zero_constructor (F)
  15. 0015specialize divisor_mask_prefix_zero_constructor (n)
  16. 0016specialize divisor_mask_prefix_zero_constructor (x)
  17. 0017apply divisor_mask_prefix_zero_constructor
  18. 0018exact hzero_witness_left
  19. 0019exact hzero_witness_right
  20. 0020intro ht
  21. 0021intro hbound
  22. 0022have hlow : Le(l,N)
  23. 0023specialize le_trans (l)
  24. 0024specialize le_trans (S l)
  25. 0025specialize le_trans (N)
  26. 0026apply le_trans
  27. 0027specialize le_succ_self (l)
  28. 0028apply le_succ_self
  29. 0029exact hbound
  30. 0030have hprev : ∃ M. DivisorMask(F,n,l,M)
  31. 0031apply IH
  32. 0032exact ht
  33. 0033exact hlow
  34. 0034cases hprev
  35. 0035have hz : ∃ z. DivisorMaskEntry(F,n,S l,z)
  36. 0036specialize divisor_mask_entry_exists (N)
  37. 0037specialize divisor_mask_entry_exists (F)
  38. 0038specialize divisor_mask_entry_exists (n)
  39. 0039specialize divisor_mask_entry_exists (S l)
  40. 0040apply divisor_mask_entry_exists
  41. 0041exact ht
  42. 0042exact hbound
  43. 0043cases hz
  44. 0044have hnext : ∃ G. DivisorMask(F,n,S l,G) ∧ ArithTableEqual(x,G,S l)
  45. 0045specialize divisor_mask_prefix_append (F)
  46. 0046specialize divisor_mask_prefix_append (n)
  47. 0047specialize divisor_mask_prefix_append (l)
  48. 0048specialize divisor_mask_prefix_append (x)
  49. 0049specialize divisor_mask_prefix_append (x1)
  50. 0050apply divisor_mask_prefix_append
  51. 0051exact hprev_witness
  52. 0052exact hz_witness
  53. 0053cases hnext
  54. 0054cases hnext_witness
  55. 0055exists x2
  56. 0056exact hnext_witness_left