CD0030

finite_modular_sumset_exists

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

Every pair of actual finite modular sets has an actual canonical sumset code with a witnessed exact cardinality.

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.

Exact expanded first-order arithmetic statement

forall b c d e p n m. ~(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))))) -> (((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)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (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)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> exists u v q. (((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 ((q)) = 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) + ((q)))) /\ 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_s_sumset. (exists fms_gap_sumset_s. fms_gap_sumset_s + S (fms_s_sumset) = (p)) -> ((((((exists fs_h_fms_sumset_result. fs_h_fms_sumset_result + S (1) = S ((S (fms_s_sumset)) * v)) /\ exists fs_q_fms_sumset_result. u = fs_q_fms_sumset_result * S ((S (fms_s_sumset)) * v) + (1))) -> (exists fms_i_sumset fms_j_sumset. ((((exists fms_gap_sumset_left. fms_gap_sumset_left + S (fms_i_sumset) = (p)) /\ (((exists fs_h_fms_sumset_left. fs_h_fms_sumset_left + S (1) = S ((S (fms_i_sumset)) * c)) /\ exists fs_q_fms_sumset_left. b = fs_q_fms_sumset_left * S ((S (fms_i_sumset)) * c) + (1))))) /\ ((((exists fms_gap_sumset_right. fms_gap_sumset_right + S (fms_j_sumset) = (p)) /\ (((exists fs_h_fms_sumset_right. fs_h_fms_sumset_right + S (1) = S ((S (fms_j_sumset)) * e)) /\ exists fs_q_fms_sumset_right. d = fs_q_fms_sumset_right * S ((S (fms_j_sumset)) * e) + (1))))) /\ (exists fms_u_sumset fms_v_sumset. (fms_i_sumset + fms_j_sumset) + (p) * fms_u_sumset = (fms_s_sumset) + (p) * fms_v_sumset))))) /\ ((exists fms_i_sumset fms_j_sumset. ((((exists fms_gap_sumset_left. fms_gap_sumset_left + S (fms_i_sumset) = (p)) /\ (((exists fs_h_fms_sumset_left. fs_h_fms_sumset_left + S (1) = S ((S (fms_i_sumset)) * c)) /\ exists fs_q_fms_sumset_left. b = fs_q_fms_sumset_left * S ((S (fms_i_sumset)) * c) + (1))))) /\ ((((exists fms_gap_sumset_right. fms_gap_sumset_right + S (fms_j_sumset) = (p)) /\ (((exists fs_h_fms_sumset_right. fs_h_fms_sumset_right + S (1) = S ((S (fms_j_sumset)) * e)) /\ exists fs_q_fms_sumset_right. d = fs_q_fms_sumset_right * S ((S (fms_j_sumset)) * e) + (1))))) /\ (exists fms_u_sumset fms_v_sumset. (fms_i_sumset + fms_j_sumset) + (p) * fms_u_sumset = (fms_s_sumset) + (p) * fms_v_sumset)))) -> (((exists fs_h_fms_sumset_result. fs_h_fms_sumset_result + S (1) = S ((S (fms_s_sumset)) * v)) /\ exists fs_q_fms_sumset_result. u = fs_q_fms_sumset_result * S ((S (fms_s_sumset)) * v) + (1)))))))

Constructive proof overview

Generated structural guide

Every pair of actual finite modular sets has an actual canonical sumset code with a witnessed exact cardinality.

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

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

Proof neighborhood

Direct dependencies

CD002F finite_modular_sumset_prefix_exists le_refl Stable theorem; checked-use authorized

Direct dependents

CD0048 prime_cauchy_davenport_sumset_exists

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

74 script commands · 30 reading checkpoints · 3 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)
finite modular sumset prefix exists

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

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
  7. L7
    intro m
  8. L8
    intro hp
  9. L9
    intro hA
  10. L10
    intro hB
02Establish hprefixL11–20

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

  1. L11
    have hprefix : ∃ u. ∃ v. ∃ q. BitCount(u,v,p,q) ∧ (∀ x. Lt(x,p) → (BetaAt(u,v,x,1) → ∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,p) ∧ ModEq(p,y + z,x)))) ∧ ((∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,p) ∧ ModEq(p,y + z,x)))) → BetaAt(u,v,x,1)))Definitions: ModularSetMemberLtModEqBetaAtBitCount
  2. L12
    specialize finite_modular_sumset_prefix_exists b
  3. L13
    specialize finite_modular_sumset_prefix_exists c
  4. L14
    specialize finite_modular_sumset_prefix_exists d
  5. L15
    specialize finite_modular_sumset_prefix_exists e
  6. L16
    specialize finite_modular_sumset_prefix_exists p
  7. L17
    specialize finite_modular_sumset_prefix_exists n
  8. L18
    specialize finite_modular_sumset_prefix_exists p
  9. L19
    apply finite_modular_sumset_prefix_exists
  10. L20
    exact hp
03Use earlier factsL21–21

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

  1. L21
    exact hA
04Separate the logical casesL22–22

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

  1. L22
    cases hB
05Use earlier factsL23–25

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

  1. L23
    exact hB_right
  2. L24
    specialize le_refl p
  3. L25
    apply le_refl
06Separate the logical casesL26–29

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

  1. L26
    cases hprefix
  2. L27
    cases hprefix_witness
  3. L28
    cases hprefix_witness_witness
  4. L29
    cases hprefix_witness_witness_witness
07Construct an explicit witnessL30–32

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

  1. L30
    exists x
  2. L31
    exists x1
  3. L32
    exists x2
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–34

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

  1. L34
    exact hprefix_witness_witness_witness_left
10Fix variables and assumptionsL35–36

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

  1. L35
    intro z
  2. L36
    intro hz
11Establish heL37–40

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

  1. L37
    have he : (BetaAt(x,x1,z,1) → ∃ y. ∃ n. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,n) ∧ (Lt(n,p) ∧ ModEq(p,y + n,z)))) ∧ ((∃ y. ∃ n. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,n) ∧ (Lt(n,p) ∧ ModEq(p,y + n,z)))) → BetaAt(x,x1,z,1))Definitions: ModularSetMemberLtModEqBetaAt
  2. L38
    specialize hprefix_witness_witness_witness_right z
  3. L39
    apply hprefix_witness_witness_witness_right
  4. L40
    exact hz
12Separate the logical casesL41–42

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

  1. L41
    cases he
  2. L42
    split
13Fix variables and assumptionsL43–43

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

  1. L43
    intro hs
14Establish hwL44–46

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

  1. L44
    have hw : ∃ fms_first_partial. ∃ fms_second_partial. ModularSetMember(b,c,p,fms_first_partial) ∧ (ModularSetMember(d,e,p,fms_second_partial) ∧ (Lt(fms_second_partial,p) ∧ ModEq(p,fms_first_partial + fms_second_partial,z)))Definitions: ModularSetMemberLtModEq
  2. L45
    apply he_left
  3. L46
    exact hs
15Separate the logical casesL47–51

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

  1. L47
    cases hw
  2. L48
    cases hw_witness
  3. L49
    cases hw_witness_witness
  4. L50
    cases hw_witness_witness_right
  5. L51
    cases hw_witness_witness_right_right
16Construct an explicit witnessL52–53

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

  1. L52
    exists x3
  2. L53
    exists x4
17Separate the logical casesL54–54

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

  1. L54
    split
18Use earlier factsL55–55

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

  1. L55
    exact hw_witness_witness_left
19Separate the logical casesL56–56

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

  1. L56
    split
20Use earlier factsL57–58

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

  1. L57
    exact hw_witness_witness_right_left
  2. L58
    exact hw_witness_witness_right_right_right
21Fix variables and assumptionsL59–59

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

  1. L59
    intro hw
22Separate the logical casesL60–63

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

  1. L60
    cases hw
  2. L61
    cases hw_witness
  3. L62
    cases hw_witness_witness
  4. L63
    cases hw_witness_witness_right
23Use earlier factsL64–64

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

  1. L64
    apply he_right
24Construct an explicit witnessL65–66

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

  1. L65
    exists x3
  2. L66
    exists x4
25Separate the logical casesL67–67

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

  1. L67
    split
26Use earlier factsL68–68

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

  1. L68
    exact hw_witness_witness_left
27Separate the logical casesL69–69

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

  1. L69
    split
28Use earlier factsL70–70

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

  1. L70
    exact hw_witness_witness_right_left
29Separate the logical casesL71–72

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

  1. L71
    split
  2. L72
    cases hw_witness_witness_right_left
30Use earlier factsL73–74

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

  1. L73
    exact hw_witness_witness_right_left_left
  2. L74
    exact hw_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro p
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hp
  9. 0009intro hA
  10. 0010intro hB
  11. 0011have hprefix : exists u v q. (((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 ((q)) = 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) + ((q)))) /\ 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) = (p)) /\ (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) = (p)) /\ (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)))))))
  12. 0012specialize finite_modular_sumset_prefix_exists b
  13. 0013specialize finite_modular_sumset_prefix_exists c
  14. 0014specialize finite_modular_sumset_prefix_exists d
  15. 0015specialize finite_modular_sumset_prefix_exists e
  16. 0016specialize finite_modular_sumset_prefix_exists p
  17. 0017specialize finite_modular_sumset_prefix_exists n
  18. 0018specialize finite_modular_sumset_prefix_exists p
  19. 0019apply finite_modular_sumset_prefix_exists
  20. 0020exact hp
  21. 0021exact hA
  22. 0022cases hB
  23. 0023exact hB_right
  24. 0024specialize le_refl p
  25. 0025apply le_refl
  26. 0026cases hprefix
  27. 0027cases hprefix_witness
  28. 0028cases hprefix_witness_witness
  29. 0029cases hprefix_witness_witness_witness
  30. 0030exists x
  31. 0031exists x1
  32. 0032exists x2
  33. 0033split
  34. 0034exact hprefix_witness_witness_witness_left
  35. 0035intro z
  36. 0036intro hz
  37. 0037have he : (((((exists fs_h_fms_sumset_final. fs_h_fms_sumset_final + S (1) = S ((S (z)) * x1)) /\ exists fs_q_fms_sumset_final. x = fs_q_fms_sumset_final * S ((S (z)) * x1) + (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) = (p)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (z) + (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) = (p)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (z) + (p) * fms_v_partial_congruence)))) -> (((exists fs_h_fms_sumset_final. fs_h_fms_sumset_final + S (1) = S ((S (z)) * x1)) /\ exists fs_q_fms_sumset_final. x = fs_q_fms_sumset_final * S ((S (z)) * x1) + (1)))))
  38. 0038specialize hprefix_witness_witness_witness_right z
  39. 0039apply hprefix_witness_witness_witness_right
  40. 0040exact hz
  41. 0041cases he
  42. 0042split
  43. 0043intro hs
  44. 0044have hw : 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) = (p)) /\ (exists fms_u_partial_congruence fms_v_partial_congruence. (fms_first_partial+fms_second_partial) + (p) * fms_u_partial_congruence = (z) + (p) * fms_v_partial_congruence)))
  45. 0045apply he_left
  46. 0046exact hs
  47. 0047cases hw
  48. 0048cases hw_witness
  49. 0049cases hw_witness_witness
  50. 0050cases hw_witness_witness_right
  51. 0051cases hw_witness_witness_right_right
  52. 0052exists x3
  53. 0053exists x4
  54. 0054split
  55. 0055exact hw_witness_witness_left
  56. 0056split
  57. 0057exact hw_witness_witness_right_left
  58. 0058exact hw_witness_witness_right_right_right
  59. 0059intro hw
  60. 0060cases hw
  61. 0061cases hw_witness
  62. 0062cases hw_witness_witness
  63. 0063cases hw_witness_witness_right
  64. 0064apply he_right
  65. 0065exists x3
  66. 0066exists x4
  67. 0067split
  68. 0068exact hw_witness_witness_left
  69. 0069split
  70. 0070exact hw_witness_witness_right_left
  71. 0071split
  72. 0072cases hw_witness_witness_right_left
  73. 0073exact hw_witness_witness_right_left_left
  74. 0074exact hw_witness_witness_right_right