CD002E

finite_partial_sumset_succ_present

Adjoining the actual translated first set at a present second-coordinate bit gives the exact next partial sumset.

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. ∀ ub. ∀ uc. ∀ tb. ∀ tc. ∀ zb. ∀ zc. ∀ p. ∀ l. ∀ v. ¬p = 0 → Lt(l,p) → l + v = p → BetaAt(d,e,l,1) → (∀ x. Lt(x,p) → (BetaAt(ub,uc,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(ub,uc,x,1))) → ModularSetPullback(b,c,tb,tc,p,v) → ModularSetUnion(ub,uc,tb,tc,zb,zc,p) → ∀ x. Lt(x,p) → (BetaAt(zb,zc,x,1) → ∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,S l) ∧ ModEq(p,y + z,x)))) ∧ ((∃ y. ∃ z. ModularSetMember(b,c,p,y) ∧ (ModularSetMember(d,e,p,z) ∧ (Lt(z,S l) ∧ ModEq(p,y + z,x)))) → BetaAt(zb,zc,x,1))

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

Definition DAG

ModularSetMember(b,c,p,x) · 17ModularSetUnion(b,c,d,e,u,v,p) · 1ModularSetPullback(b,c,d,e,p,t) · 1Lt(a,b) · 11ModEq(m,a,b) · 10BetaAt(b,c,i,x) · 17

Actual proof prerequisites

finite_modular_pushforward_membership_witnessfinite_lt_succ_eq_or_lt · checked external prerequisitele_succ · checked external prerequisitele_refl · checked external prerequisite
Original expanded first-order statement 
forall b c d e ub uc tb tc zb zc p l v. ~(p=0) -> (exists fms_gap_lt. fms_gap_lt + S (l) = (p)) -> l+v=p -> (((exists fs_h_fms_present_bit. fs_h_fms_present_bit + S (1) = S ((S (l)) * e)) /\ exists fs_q_fms_present_bit. d = fs_q_fms_present_bit * S ((S (l)) * e) + (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)) * uc)) /\ exists fs_q_fms_partial_result. ub = fs_q_fms_partial_result * S ((S (fms_z_partial)) * uc) + (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)) * uc)) /\ exists fs_q_fms_partial_result. ub = fs_q_fms_partial_result * S ((S (fms_z_partial)) * uc) + (1))))))) -> (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + v) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (1))))))) -> (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (p)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * zc)) /\ exists fs_q_fms_binary_result. zb = fs_q_fms_binary_result * S ((S (fms_i_binary)) * zc) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_left. ub = fs_q_fms_binary_left * S ((S (fms_i_binary)) * uc) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_left. ub = fs_q_fms_binary_left * S ((S (fms_i_binary)) * uc) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * zc)) /\ exists fs_q_fms_binary_result. zb = fs_q_fms_binary_result * S ((S (fms_i_binary)) * zc) + (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)) * zc)) /\ exists fs_q_fms_partial_result. zb = fs_q_fms_partial_result * S ((S (fms_z_partial)) * zc) + (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) = (S 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) = (S 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)) * zc)) /\ exists fs_q_fms_partial_result. zb = fs_q_fms_partial_result * S ((S (fms_z_partial)) * zc) + (1)))))))

Complete tactic proof in conservative notation

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

122 script commands · 52 reading checkpoints · 7 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 (1)
finite modular pushforward membership witness
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 ub
  6. L6
    intro uc
  7. L7
    intro tb
  8. L8
    intro tc
  9. L9
    intro zb
  10. L10
    intro zc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro p
  2. L12
    intro l
  3. L13
    intro v
  4. L14
    intro hp
  5. L15
    intro hl
  6. L16
    intro hlv
  7. L17
    intro hB
  8. L18
    intro hprefix
  9. L19
    intro hpull
  10. L20
    intro hunion
03Fix variables and assumptionsL21–22

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

  1. L21
    intro z
  2. L22
    intro hz
04Establish hpreL23–26

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

  1. L23
    have hpre : (BetaAt(ub,uc,z,1) → ∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,l) ∧ ModEq(p,x + y,z)))) ∧ ((∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,l) ∧ ModEq(p,x + y,z)))) → BetaAt(ub,uc,z,1))Definitions: BetaAt(ub,uc,z,1)ModularSetMember(b,c,p,x)ModularSetMember(d,e,p,y)Lt(y,l)ModEq(p,x + y,z)Original native command in the exact edition
  2. L24
    specialize hprefix z
  3. L25
    apply hprefix
  4. L26
    exact hz
05Separate the logical casesL27–27

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

  1. L27
    cases hpre
06Establish hshiftL28–37

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

  1. L28
    have hshift : (BetaAt(tb,tc,z,1) → ∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + l,z)) ∧ ((∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + l,z)) → BetaAt(tb,tc,z,1))Definitions: BetaAt(tb,tc,z,1)ModularSetMember(b,c,p,x)ModEq(p,x + l,z)Original native command in the exact edition
  2. L29
    specialize finite_modular_pushforward_membership_witness b
  3. L30
    specialize finite_modular_pushforward_membership_witness c
  4. L31
    specialize finite_modular_pushforward_membership_witness tb
  5. L32
    specialize finite_modular_pushforward_membership_witness tc
  6. L33
    specialize finite_modular_pushforward_membership_witness p
  7. L34
    specialize finite_modular_pushforward_membership_witness l
  8. L35
    specialize finite_modular_pushforward_membership_witness v
  9. L36
    specialize finite_modular_pushforward_membership_witness z
  10. L37
    apply finite_modular_pushforward_membership_witness
07Use earlier factsL38–41

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

  1. L38
    exact hp
  2. L39
    exact hlv
  3. L40
    exact hpull
  4. L41
    exact hz
08Separate the logical casesL42–42

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

  1. L42
    cases hshift
09Establish hunL43–46

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

  1. L43
    have hun : (BetaAt(zb,zc,z,1) → BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1)) ∧ (BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1) → BetaAt(zb,zc,z,1))Definitions: BetaAt(zb,zc,z,1)BetaAt(ub,uc,z,1)BetaAt(tb,tc,z,1)Original native command in the exact edition
  2. L44
    specialize hunion z
  3. L45
    apply hunion
  4. L46
    exact hz
10Separate the logical casesL47–48

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

  1. L47
    cases hun
  2. L48
    split
11Fix variables and assumptionsL49–49

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

  1. L49
    intro hnew
12Establish hcL50–52

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

  1. L50
    have hc : BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1)Definitions: BetaAt(ub,uc,z,1)BetaAt(tb,tc,z,1)Original native command in the exact edition
  2. L51
    apply hun_left
  3. L52
    exact hnew
13Separate the logical casesL53–53

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

  1. L53
    cases hc
14Establish hwL54–56

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

  1. L54
    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,l) ∧ ModEq(p,fms_first_partial + fms_second_partial,z)))Definitions: ModularSetMember(b,c,p,fms_first_partial)ModularSetMember(d,e,p,fms_second_partial)Lt(fms_second_partial,l)ModEq(p,fms_first_partial + fms_second_partial,z)Original native command in the exact edition
  2. L55
    apply hpre_left
  3. L56
    exact hc_left
15Separate the logical casesL57–61

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

  1. L57
    cases hw
  2. L58
    cases hw_witness
  3. L59
    cases hw_witness_witness
  4. L60
    cases hw_witness_witness_right
  5. L61
    cases hw_witness_witness_right_right
16Construct an explicit witnessL62–63

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

  1. L62
    exists x
  2. L63
    exists x1
17Separate the logical casesL64–64

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

  1. L64
    split
18Use earlier factsL65–65

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

  1. L65
    exact hw_witness_witness_left
19Separate the logical casesL66–66

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

  1. L66
    split
20Use earlier factsL67–67

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

  1. L67
    exact hw_witness_witness_right_left
21Separate the logical casesL68–68

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

  1. L68
    split
22Use earlier factsL69–73

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

  1. L69
    specialize le_succ S x1
  2. L70
    specialize le_succ l
  3. L71
    apply le_succ
  4. L72
    exact hw_witness_witness_right_right_left
  5. L73
    exact hw_witness_witness_right_right_right
23Establish hwL74–76

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

  1. L74
    have hw : ∃ a. ModularSetMember(b,c,p,a) ∧ ModEq(p,a + l,z)Definitions: ModularSetMember(b,c,p,a)ModEq(p,a + l,z)Original native command in the exact edition
  2. L75
    apply hshift_left
  3. L76
    exact hc_right
24Separate the logical casesL77–78

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

  1. L77
    cases hw
  2. L78
    cases hw_witness
25Construct an explicit witnessL79–80

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

  1. L79
    exists x
  2. L80
    exists l
26Separate the logical casesL81–81

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

  1. L81
    split
27Use earlier factsL82–82

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

  1. L82
    exact hw_witness_left
28Separate the logical casesL83–84

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

  1. L83
    split
  2. L84
    split
29Use earlier factsL85–86

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

  1. L85
    exact hl
  2. L86
    exact hB
30Separate the logical casesL87–87

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

  1. L87
    split
31Use earlier factsL88–90

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

  1. L88
    specialize le_refl S l
  2. L89
    apply le_refl
  3. L90
    exact hw_witness_right
32Fix variables and assumptionsL91–91

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

  1. L91
    intro hw
33Separate the logical casesL92–96

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

  1. L92
    cases hw
  2. L93
    cases hw_witness
  3. L94
    cases hw_witness_witness
  4. L95
    cases hw_witness_witness_right
  5. L96
    cases hw_witness_witness_right_right
34Establish hcaseL97–101

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L97
    have hcase : x1 = l ∨ Lt(x1,l)Definitions: Lt(x1,l)Original native command in the exact edition
  2. L98
    specialize finite_lt_succ_eq_or_lt l
  3. L99
    specialize finite_lt_succ_eq_or_lt x1
  4. L100
    apply finite_lt_succ_eq_or_lt
  5. L101
    exact hw_witness_witness_right_right_left
35Separate the logical casesL102–102

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

  1. L102
    cases hcase
36Use earlier factsL103–103

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

  1. L103
    apply hun_right
37Separate the logical casesL104–104

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

  1. L104
    right
38Use earlier factsL105–105

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

  1. L105
    apply hshift_right
39Construct an explicit witnessL106–106

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

  1. L106
    exists x
40Separate the logical casesL107–107

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

  1. L107
    split
41Use earlier factsL108–108

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

  1. L108
    exact hw_witness_witness_left
42Calculate and transport equalitiesL109–109

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

  1. L109
    rewrite hcase_left at hw_witness_witness_right_right_right
43Use earlier factsL110–111

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

  1. L110
    exact hw_witness_witness_right_right_right
  2. L111
    apply hun_right
44Separate the logical casesL112–112

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

  1. L112
    left
45Use earlier factsL113–113

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

  1. L113
    apply hpre_right
46Construct an explicit witnessL114–115

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

  1. L114
    exists x
  2. L115
    exists x1
47Separate the logical casesL116–116

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

  1. L116
    split
48Use earlier factsL117–117

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

  1. L117
    exact hw_witness_witness_left
49Separate the logical casesL118–118

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

  1. L118
    split
50Use earlier factsL119–119

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

  1. L119
    exact hw_witness_witness_right_left
51Separate the logical casesL120–120

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

  1. L120
    split
52Use earlier factsL121–122

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

  1. L121
    exact hcase_right
  2. L122
    exact hw_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 122 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro ub
  6. 0006intro uc
  7. 0007intro tb
  8. 0008intro tc
  9. 0009intro zb
  10. 0010intro zc
  11. 0011intro p
  12. 0012intro l
  13. 0013intro v
  14. 0014intro hp
  15. 0015intro hl
  16. 0016intro hlv
  17. 0017intro hB
  18. 0018intro hprefix
  19. 0019intro hpull
  20. 0020intro hunion
  21. 0021intro z
  22. 0022intro hz
  23. 0023have hpre : (BetaAt(ub,uc,z,1) → ∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,l) ∧ ModEq(p,x + y,z)))) ∧ ((∃ x. ∃ y. ModularSetMember(b,c,p,x) ∧ (ModularSetMember(d,e,p,y) ∧ (Lt(y,l) ∧ ModEq(p,x + y,z)))) → BetaAt(ub,uc,z,1))
  24. 0024specialize hprefix z
  25. 0025apply hprefix
  26. 0026exact hz
  27. 0027cases hpre
  28. 0028have hshift : (BetaAt(tb,tc,z,1) → ∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + l,z)) ∧ ((∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + l,z)) → BetaAt(tb,tc,z,1))
  29. 0029specialize finite_modular_pushforward_membership_witness b
  30. 0030specialize finite_modular_pushforward_membership_witness c
  31. 0031specialize finite_modular_pushforward_membership_witness tb
  32. 0032specialize finite_modular_pushforward_membership_witness tc
  33. 0033specialize finite_modular_pushforward_membership_witness p
  34. 0034specialize finite_modular_pushforward_membership_witness l
  35. 0035specialize finite_modular_pushforward_membership_witness v
  36. 0036specialize finite_modular_pushforward_membership_witness z
  37. 0037apply finite_modular_pushforward_membership_witness
  38. 0038exact hp
  39. 0039exact hlv
  40. 0040exact hpull
  41. 0041exact hz
  42. 0042cases hshift
  43. 0043have hun : (BetaAt(zb,zc,z,1) → BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1)) ∧ (BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1) → BetaAt(zb,zc,z,1))
  44. 0044specialize hunion z
  45. 0045apply hunion
  46. 0046exact hz
  47. 0047cases hun
  48. 0048split
  49. 0049intro hnew
  50. 0050have hc : BetaAt(ub,uc,z,1) ∨ BetaAt(tb,tc,z,1)
  51. 0051apply hun_left
  52. 0052exact hnew
  53. 0053cases hc
  54. 0054have 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,l) ∧ ModEq(p,fms_first_partial + fms_second_partial,z)))
  55. 0055apply hpre_left
  56. 0056exact hc_left
  57. 0057cases hw
  58. 0058cases hw_witness
  59. 0059cases hw_witness_witness
  60. 0060cases hw_witness_witness_right
  61. 0061cases hw_witness_witness_right_right
  62. 0062exists x
  63. 0063exists x1
  64. 0064split
  65. 0065exact hw_witness_witness_left
  66. 0066split
  67. 0067exact hw_witness_witness_right_left
  68. 0068split
  69. 0069specialize le_succ S x1
  70. 0070specialize le_succ l
  71. 0071apply le_succ
  72. 0072exact hw_witness_witness_right_right_left
  73. 0073exact hw_witness_witness_right_right_right
  74. 0074have hw : ∃ a. ModularSetMember(b,c,p,a) ∧ ModEq(p,a + l,z)
  75. 0075apply hshift_left
  76. 0076exact hc_right
  77. 0077cases hw
  78. 0078cases hw_witness
  79. 0079exists x
  80. 0080exists l
  81. 0081split
  82. 0082exact hw_witness_left
  83. 0083split
  84. 0084split
  85. 0085exact hl
  86. 0086exact hB
  87. 0087split
  88. 0088specialize le_refl S l
  89. 0089apply le_refl
  90. 0090exact hw_witness_right
  91. 0091intro hw
  92. 0092cases hw
  93. 0093cases hw_witness
  94. 0094cases hw_witness_witness
  95. 0095cases hw_witness_witness_right
  96. 0096cases hw_witness_witness_right_right
  97. 0097have hcase : x1 = l ∨ Lt(x1,l)
  98. 0098specialize finite_lt_succ_eq_or_lt l
  99. 0099specialize finite_lt_succ_eq_or_lt x1
  100. 0100apply finite_lt_succ_eq_or_lt
  101. 0101exact hw_witness_witness_right_right_left
  102. 0102cases hcase
  103. 0103apply hun_right
  104. 0104right
  105. 0105apply hshift_right
  106. 0106exists x
  107. 0107split
  108. 0108exact hw_witness_witness_left
  109. 0109rewrite hcase_left at hw_witness_witness_right_right_right
  110. 0110exact hw_witness_witness_right_right_right
  111. 0111apply hun_right
  112. 0112left
  113. 0113apply hpre_right
  114. 0114exists x
  115. 0115exists x1
  116. 0116split
  117. 0117exact hw_witness_witness_left
  118. 0118split
  119. 0119exact hw_witness_witness_right_left
  120. 0120split
  121. 0121exact hcase_right
  122. 0122exact hw_witness_witness_right_right_right