CD002F

finite_modular_sumset_prefix_exists

Genuine finite induction constructs every bounded prefix of the exact modular sumset, including all beta codes and cardinality traces.

Alpha v34 checked-use · first admitted v27 · 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. Exact original first-admission records.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ p. ∀ n. ∀ l. ¬p = 0 → BitCount(b,c,p,n) → AllBits(d,e,p) → Le(l,p) → ∃ x. ∃ y. ∃ z. BitCount(x,y,p,z) ∧ (∀ m. Lt(m,p) → (BetaAt(x,y,m,1) → ∃ k. ∃ i. ModularSetMember(b,c,p,k) ∧ (ModularSetMember(d,e,p,i) ∧ (Lt(i,l) ∧ ModEq(p,k + i,m)))) ∧ ((∃ k. ∃ i. ModularSetMember(b,c,p,k) ∧ (ModularSetMember(d,e,p,i) ∧ (Lt(i,l) ∧ ModEq(p,k + i,m)))) → BetaAt(x,y,m,1)))

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

Definition DAG

ModularSetMember(b,c,p,x) · 8ModularSetUnion(b,c,d,e,u,v,p) · 1ModularSetPullback(b,c,d,e,p,t) · 1Le(a,b) · 1Lt(a,b) · 6ModEq(m,a,b) · 4BetaAt(b,c,i,x) · 6AllBits(b,c,l) · 1BitCount(b,c,l,z) · 5

Actual proof prerequisites

finite_bit_empty_countfinite_partial_sumset_emptyle_trans · checked external prerequisitele_succ_self · checked external prerequisitefinite_bit_membership_decidablefinite_modular_additive_complementfinite_modular_set_pullback_existsfinite_bit_union_existsfinite_partial_sumset_succ_presentfinite_partial_sumset_succ_absent
Original expanded first-order statement 
forall b c d e p n l. ~(p=0) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (p)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (e))) /\ exists ff_q_fms_bits_decoded. (d) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (e)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (exists fms_gap_le. fms_gap_le + (l) = (p)) -> exists u v m. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_summand. (u) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (v)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_decoded. (u) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (v)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_z_partial. (exists fms_gap_partial_bound. fms_gap_partial_bound + S (fms_z_partial) = (p)) -> ((((((exists fs_h_fms_partial_result. fs_h_fms_partial_result + S (1) = S ((S (fms_z_partial)) * v)) /\ exists fs_q_fms_partial_result. u = fs_q_fms_partial_result * S ((S (fms_z_partial)) * v) + (1))) -> (exists fms_first_partial fms_second_partial. (((exists fms_gap_partial_left. fms_gap_partial_left + S (fms_first_partial) = (p)) /\ (((exists fs_h_fms_partial_left. fs_h_fms_partial_left + S (1) = S ((S (fms_first_partial)) * c)) /\ exists fs_q_fms_partial_left. b = fs_q_fms_partial_left * S ((S (fms_first_partial)) * c) + (1))))) /\ ((((exists fms_gap_partial_right. fms_gap_partial_right + S (fms_second_partial) = (p)) /\ (((exists fs_h_fms_partial_right. fs_h_fms_partial_right + S (1) = S ((S (fms_second_partial)) * e)) /\ exists fs_q_fms_partial_right. d = fs_q_fms_partial_right * S ((S (fms_second_partial)) * e) + (1))))) /\ ((exists fms_gap_partial_cutoff. fms_gap_partial_cutoff + S (fms_second_partial) = (l)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (fms_z_partial) + (p) * fms_v_partial_congruence))))) /\ ((exists fms_first_partial fms_second_partial. (((exists fms_gap_partial_left. fms_gap_partial_left + S (fms_first_partial) = (p)) /\ (((exists fs_h_fms_partial_left. fs_h_fms_partial_left + S (1) = S ((S (fms_first_partial)) * c)) /\ exists fs_q_fms_partial_left. b = fs_q_fms_partial_left * S ((S (fms_first_partial)) * c) + (1))))) /\ ((((exists fms_gap_partial_right. fms_gap_partial_right + S (fms_second_partial) = (p)) /\ (((exists fs_h_fms_partial_right. fs_h_fms_partial_right + S (1) = S ((S (fms_second_partial)) * e)) /\ exists fs_q_fms_partial_right. d = fs_q_fms_partial_right * S ((S (fms_second_partial)) * e) + (1))))) /\ ((exists fms_gap_partial_cutoff. fms_gap_partial_cutoff + S (fms_second_partial) = (l)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (fms_z_partial) + (p) * fms_v_partial_congruence)))) -> (((exists fs_h_fms_partial_result. fs_h_fms_partial_result + S (1) = S ((S (fms_z_partial)) * v)) /\ exists fs_q_fms_partial_result. u = fs_q_fms_partial_result * S ((S (fms_z_partial)) * v) + (1)))))))

Complete tactic proof in conservative notation

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

127 script commands · 27 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 (8)
finite bit empty countfinite partial sumset emptyfinite bit membership decidablefinite modular additive complementfinite modular set pullback existsfinite bit union existsfinite partial sumset succ presentfinite partial sumset succ absent
01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro p
  6. L6
    intro n
02Induction on lL7–11

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

  1. L7
    induction l
  2. L8
    intro hp
  3. L9
    intro hA
  4. L10
    intro hbitsB
  5. L11
    intro hl
03Construct an explicit witnessL12–14

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

  1. L12
    exists 0
  2. L13
    exists 0
  3. L14
    exists 0
04Separate the logical casesL15–15

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

  1. L15
    split
05Use earlier factsL16–23

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

  1. L16
    specialize finite_bit_empty_count p
  2. L17
    apply finite_bit_empty_count
  3. L18
    specialize finite_partial_sumset_empty b
  4. L19
    specialize finite_partial_sumset_empty c
  5. L20
    specialize finite_partial_sumset_empty d
  6. L21
    specialize finite_partial_sumset_empty e
  7. L22
    specialize finite_partial_sumset_empty p
  8. L23
    apply finite_partial_sumset_empty
06Fix variables and assumptionsL24–27

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

  1. L24
    intro hp
  2. L25
    intro hA
  3. L26
    intro hbitsB
  4. L27
    intro hbound
07Establish hprefixL28–37

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

  1. L28
    have hprefix : ∃ u. ∃ v. ∃ m. BitCount(u,v,p,m) ∧ (∀ x. Lt(x,p) → (BetaAt(u,v,x,1) → ∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,l) ∧ ModEq(p,y + z,x)))) ∧ ((∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,l) ∧ ModEq(p,y + z,x)))) → BetaAt(u,v,x,1)))Definitions: BitCount(u,v,p,m)Lt(x,p)BetaAt(u,v,x,1)ModularSetMember(b,c,p,y)ModularSetMember(d,e,p,z)Lt(z,l)ModEq(p,y + z,x)Original native command in the exact edition
  2. L29
    apply IH
  3. L30
    exact hp
  4. L31
    exact hA
  5. L32
    exact hbitsB
  6. L33
    specialize le_trans l
  7. L34
    specialize le_trans S l
  8. L35
    specialize le_trans p
  9. L36
    apply le_trans
  10. L37
    specialize le_succ_self l
08Use earlier factsL38–39

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

  1. L38
    apply le_succ_self
  2. L39
    exact hbound
09Separate the logical casesL40–43

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

  1. L40
    cases hprefix
  2. L41
    cases hprefix_witness
  3. L42
    cases hprefix_witness_witness
  4. L43
    cases hprefix_witness_witness_witness
10Establish hdecL44–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit membership decidable.

  1. L44
    have hdec : BetaAt(d,e,l,1) ∨ ¬BetaAt(d,e,l,1)Definitions: BetaAt(d,e,l,1)Original native command in the exact edition
  2. L45
    specialize finite_bit_membership_decidable d
  3. L46
    specialize finite_bit_membership_decidable e
  4. L47
    specialize finite_bit_membership_decidable p
  5. L48
    specialize finite_bit_membership_decidable l
  6. L49
    apply finite_bit_membership_decidable
  7. L50
    exact hbitsB
  8. L51
    exact hbound
11Separate the logical casesL52–52

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

  1. L52
    cases hdec
12Establish hdL53–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular additive complement.

  1. L53
    have hd : exists v. l+v=p
  2. L54
    specialize finite_modular_additive_complement p
  3. L55
    specialize finite_modular_additive_complement l
  4. L56
    apply finite_modular_additive_complement
  5. L57
    exact hbound
13Separate the logical casesL58–58

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

  1. L58
    cases hd
14Establish htranslateL59–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular set pullback exists.

  1. L59
    have htranslate : ∃ u. ∃ v. BitCount(u,v,p,n) ∧ ModularSetPullback(b,c,u,v,p,x3)Definitions: BitCount(u,v,p,n)ModularSetPullback(b,c,u,v,p,x3)Original native command in the exact edition
  2. L60
    specialize finite_modular_set_pullback_exists b
  3. L61
    specialize finite_modular_set_pullback_exists c
  4. L62
    specialize finite_modular_set_pullback_exists p
  5. L63
    specialize finite_modular_set_pullback_exists n
  6. L64
    specialize finite_modular_set_pullback_exists x3
  7. L65
    apply finite_modular_set_pullback_exists
  8. L66
    exact hp
  9. L67
    exact hA
15Separate the logical casesL68–70

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

  1. L68
    cases htranslate
  2. L69
    cases htranslate_witness
  3. L70
    cases htranslate_witness_witness
16Establish hunionL71–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit union exists.

  1. L71
    have hunion : ∃ u. ∃ v. ∃ m. BitCount(u,v,p,m) ∧ ModularSetUnion(x,x1,x4,x5,u,v,p)Definitions: BitCount(u,v,p,m)ModularSetUnion(x,x1,x4,x5,u,v,p)Original native command in the exact edition
  2. L72
    specialize finite_bit_union_exists x
  3. L73
    specialize finite_bit_union_exists x1
  4. L74
    specialize finite_bit_union_exists x4
  5. L75
    specialize finite_bit_union_exists x5
  6. L76
    specialize finite_bit_union_exists p
  7. L77
    specialize finite_bit_union_exists x2
  8. L78
    specialize finite_bit_union_exists n
  9. L79
    apply finite_bit_union_exists
  10. L80
    exact hprefix_witness_witness_witness_left
17Use earlier factsL81–81

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

  1. L81
    exact htranslate_witness_witness_left
18Separate the logical casesL82–85

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

  1. L82
    cases hunion
  2. L83
    cases hunion_witness
  3. L84
    cases hunion_witness_witness
  4. L85
    cases hunion_witness_witness_witness
19Construct an explicit witnessL86–88

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

  1. L86
    exists x6
  2. L87
    exists x7
  3. L88
    exists x8
20Separate the logical casesL89–89

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

  1. L89
    split
21Use earlier factsL90–99

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

  1. L90
    exact hunion_witness_witness_witness_left
  2. L91
    specialize finite_partial_sumset_succ_present b
  3. L92
    specialize finite_partial_sumset_succ_present c
  4. L93
    specialize finite_partial_sumset_succ_present d
  5. L94
    specialize finite_partial_sumset_succ_present e
  6. L95
    specialize finite_partial_sumset_succ_present x
  7. L96
    specialize finite_partial_sumset_succ_present x1
  8. L97
    specialize finite_partial_sumset_succ_present x4
  9. L98
    specialize finite_partial_sumset_succ_present x5
  10. L99
    specialize finite_partial_sumset_succ_present x6
22Use earlier factsL100–109

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

  1. L100
    specialize finite_partial_sumset_succ_present x7
  2. L101
    specialize finite_partial_sumset_succ_present p
  3. L102
    specialize finite_partial_sumset_succ_present l
  4. L103
    specialize finite_partial_sumset_succ_present x3
  5. L104
    apply finite_partial_sumset_succ_present
  6. L105
    exact hp
  7. L106
    exact hbound
  8. L107
    exact hd_witness
  9. L108
    exact hdec_left
  10. L109
    exact hprefix_witness_witness_witness_right
23Use earlier factsL110–111

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

  1. L110
    exact htranslate_witness_witness_right
  2. L111
    exact hunion_witness_witness_witness_right
24Construct an explicit witnessL112–114

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

  1. L112
    exists x
  2. L113
    exists x1
  3. L114
    exists x2
25Separate the logical casesL115–115

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

  1. L115
    split
26Use earlier factsL116–125

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

  1. L116
    exact hprefix_witness_witness_witness_left
  2. L117
    specialize finite_partial_sumset_succ_absent b
  3. L118
    specialize finite_partial_sumset_succ_absent c
  4. L119
    specialize finite_partial_sumset_succ_absent d
  5. L120
    specialize finite_partial_sumset_succ_absent e
  6. L121
    specialize finite_partial_sumset_succ_absent x
  7. L122
    specialize finite_partial_sumset_succ_absent x1
  8. L123
    specialize finite_partial_sumset_succ_absent p
  9. L124
    specialize finite_partial_sumset_succ_absent l
  10. L125
    apply finite_partial_sumset_succ_absent
27Use earlier factsL126–127

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

  1. L126
    exact hprefix_witness_witness_witness_right
  2. L127
    exact hdec_right

Library-wide reading audit

Original defined command ledger · 127 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro p
  6. 0006intro n
  7. 0007induction l
  8. 0008intro hp
  9. 0009intro hA
  10. 0010intro hbitsB
  11. 0011intro hl
  12. 0012exists 0
  13. 0013exists 0
  14. 0014exists 0
  15. 0015split
  16. 0016specialize finite_bit_empty_count p
  17. 0017apply finite_bit_empty_count
  18. 0018specialize finite_partial_sumset_empty b
  19. 0019specialize finite_partial_sumset_empty c
  20. 0020specialize finite_partial_sumset_empty d
  21. 0021specialize finite_partial_sumset_empty e
  22. 0022specialize finite_partial_sumset_empty p
  23. 0023apply finite_partial_sumset_empty
  24. 0024intro hp
  25. 0025intro hA
  26. 0026intro hbitsB
  27. 0027intro hbound
  28. 0028have hprefix : ∃ u. ∃ v. ∃ m. BitCount(u,v,p,m) ∧ (∀ x. Lt(x,p) → (BetaAt(u,v,x,1) → ∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,l) ∧ ModEq(p,y + z,x)))) ∧ ((∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,l) ∧ ModEq(p,y + z,x)))) → BetaAt(u,v,x,1)))
  29. 0029apply IH
  30. 0030exact hp
  31. 0031exact hA
  32. 0032exact hbitsB
  33. 0033specialize le_trans l
  34. 0034specialize le_trans S l
  35. 0035specialize le_trans p
  36. 0036apply le_trans
  37. 0037specialize le_succ_self l
  38. 0038apply le_succ_self
  39. 0039exact hbound
  40. 0040cases hprefix
  41. 0041cases hprefix_witness
  42. 0042cases hprefix_witness_witness
  43. 0043cases hprefix_witness_witness_witness
  44. 0044have hdec : BetaAt(d,e,l,1) ∨ ¬BetaAt(d,e,l,1)
  45. 0045specialize finite_bit_membership_decidable d
  46. 0046specialize finite_bit_membership_decidable e
  47. 0047specialize finite_bit_membership_decidable p
  48. 0048specialize finite_bit_membership_decidable l
  49. 0049apply finite_bit_membership_decidable
  50. 0050exact hbitsB
  51. 0051exact hbound
  52. 0052cases hdec
  53. 0053have hd : exists v. l+v=p
  54. 0054specialize finite_modular_additive_complement p
  55. 0055specialize finite_modular_additive_complement l
  56. 0056apply finite_modular_additive_complement
  57. 0057exact hbound
  58. 0058cases hd
  59. 0059have htranslate : ∃ u. ∃ v. BitCount(u,v,p,n) ∧ ModularSetPullback(b,c,u,v,p,x3)
  60. 0060specialize finite_modular_set_pullback_exists b
  61. 0061specialize finite_modular_set_pullback_exists c
  62. 0062specialize finite_modular_set_pullback_exists p
  63. 0063specialize finite_modular_set_pullback_exists n
  64. 0064specialize finite_modular_set_pullback_exists x3
  65. 0065apply finite_modular_set_pullback_exists
  66. 0066exact hp
  67. 0067exact hA
  68. 0068cases htranslate
  69. 0069cases htranslate_witness
  70. 0070cases htranslate_witness_witness
  71. 0071have hunion : ∃ u. ∃ v. ∃ m. BitCount(u,v,p,m) ∧ ModularSetUnion(x,x1,x4,x5,u,v,p)
  72. 0072specialize finite_bit_union_exists x
  73. 0073specialize finite_bit_union_exists x1
  74. 0074specialize finite_bit_union_exists x4
  75. 0075specialize finite_bit_union_exists x5
  76. 0076specialize finite_bit_union_exists p
  77. 0077specialize finite_bit_union_exists x2
  78. 0078specialize finite_bit_union_exists n
  79. 0079apply finite_bit_union_exists
  80. 0080exact hprefix_witness_witness_witness_left
  81. 0081exact htranslate_witness_witness_left
  82. 0082cases hunion
  83. 0083cases hunion_witness
  84. 0084cases hunion_witness_witness
  85. 0085cases hunion_witness_witness_witness
  86. 0086exists x6
  87. 0087exists x7
  88. 0088exists x8
  89. 0089split
  90. 0090exact hunion_witness_witness_witness_left
  91. 0091specialize finite_partial_sumset_succ_present b
  92. 0092specialize finite_partial_sumset_succ_present c
  93. 0093specialize finite_partial_sumset_succ_present d
  94. 0094specialize finite_partial_sumset_succ_present e
  95. 0095specialize finite_partial_sumset_succ_present x
  96. 0096specialize finite_partial_sumset_succ_present x1
  97. 0097specialize finite_partial_sumset_succ_present x4
  98. 0098specialize finite_partial_sumset_succ_present x5
  99. 0099specialize finite_partial_sumset_succ_present x6
  100. 0100specialize finite_partial_sumset_succ_present x7
  101. 0101specialize finite_partial_sumset_succ_present p
  102. 0102specialize finite_partial_sumset_succ_present l
  103. 0103specialize finite_partial_sumset_succ_present x3
  104. 0104apply finite_partial_sumset_succ_present
  105. 0105exact hp
  106. 0106exact hbound
  107. 0107exact hd_witness
  108. 0108exact hdec_left
  109. 0109exact hprefix_witness_witness_witness_right
  110. 0110exact htranslate_witness_witness_right
  111. 0111exact hunion_witness_witness_witness_right
  112. 0112exists x
  113. 0113exists x1
  114. 0114exists x2
  115. 0115split
  116. 0116exact hprefix_witness_witness_witness_left
  117. 0117specialize finite_partial_sumset_succ_absent b
  118. 0118specialize finite_partial_sumset_succ_absent c
  119. 0119specialize finite_partial_sumset_succ_absent d
  120. 0120specialize finite_partial_sumset_succ_absent e
  121. 0121specialize finite_partial_sumset_succ_absent x
  122. 0122specialize finite_partial_sumset_succ_absent x1
  123. 0123specialize finite_partial_sumset_succ_absent p
  124. 0124specialize finite_partial_sumset_succ_absent l
  125. 0125apply finite_partial_sumset_succ_absent
  126. 0126exact hprefix_witness_witness_witness_right
  127. 0127exact hdec_right