CE0012

signed_alternating_product_prefix_extend

Two beta recodings simultaneously append the exact parity-correct signed cofactor product and preserve all earlier terms.

Alpha v34 checked-use · first admitted v25 · 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.

Historical partial components only: this chapter proves genuine signed first-row minors and unique alternating folds, with supplied cofactor values. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with actual arbitrary determinant data, rank, and integer column spans; lattice index and normal forms are not claimed. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ l. ∀ ap. ∀ an. ∀ bp. ∀ bn. ∀ p. ∀ n. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) → Beta(ab,ac,l,ap) → Beta(db,dc,l,an) → Beta(eb,ec,l,bp) → Beta(fb,fc,l,bn) → SignedAlternatingCofactorTerm(ap,an,bp,bn,l,p,n) → ∃ x. ∃ y. ∃ z. ∃ m. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,x,y,z,m,S l)

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

Definition DAG

Beta(b,c,i,x) · 4SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n) · 1SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) · 2

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc ub uc vb vc l ap an bp bn p n. (forall ff_index_mce_alternating_before. (exists ff_gap_mce_before_index. ff_gap_mce_before_index + S (ff_index_mce_alternating_before) = (l)) -> exists ff_ap_mce_alternating_before ff_an_mce_alternating_before ff_bp_mce_alternating_before ff_bn_mce_alternating_before ff_p_mce_alternating_before ff_n_mce_alternating_before. ((((exists ff_h_mce_before_ap. ff_h_mce_before_ap + S (ff_ap_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * ac)) /\ exists ff_q_mce_before_ap. ab = ff_q_mce_before_ap * S ((S (ff_index_mce_alternating_before)) * ac) + (ff_ap_mce_alternating_before))) /\ ((((exists ff_h_mce_before_an. ff_h_mce_before_an + S (ff_an_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * dc)) /\ exists ff_q_mce_before_an. db = ff_q_mce_before_an * S ((S (ff_index_mce_alternating_before)) * dc) + (ff_an_mce_alternating_before))) /\ ((((exists ff_h_mce_before_bp. ff_h_mce_before_bp + S (ff_bp_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * ec)) /\ exists ff_q_mce_before_bp. eb = ff_q_mce_before_bp * S ((S (ff_index_mce_alternating_before)) * ec) + (ff_bp_mce_alternating_before))) /\ ((((exists ff_h_mce_before_bn. ff_h_mce_before_bn + S (ff_bn_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * fc)) /\ exists ff_q_mce_before_bn. fb = ff_q_mce_before_bn * S ((S (ff_index_mce_alternating_before)) * fc) + (ff_bn_mce_alternating_before))) /\ ((((exists ff_h_mce_before_positive. ff_h_mce_before_positive + S (ff_p_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * uc)) /\ exists ff_q_mce_before_positive. ub = ff_q_mce_before_positive * S ((S (ff_index_mce_alternating_before)) * uc) + (ff_p_mce_alternating_before))) /\ ((((exists ff_h_mce_before_negative. ff_h_mce_before_negative + S (ff_n_mce_alternating_before) = S ((S (ff_index_mce_alternating_before)) * vc)) /\ exists ff_q_mce_before_negative. vb = ff_q_mce_before_negative * S ((S (ff_index_mce_alternating_before)) * vc) + (ff_n_mce_alternating_before))) /\ (((exists ff_even_mce_term_before_term. ff_index_mce_alternating_before = 2 * ff_even_mce_term_before_term) /\ (ff_p_mce_alternating_before = (ff_ap_mce_alternating_before) * (ff_bp_mce_alternating_before) + (ff_an_mce_alternating_before) * (ff_bn_mce_alternating_before) /\ ff_n_mce_alternating_before = (ff_ap_mce_alternating_before) * (ff_bn_mce_alternating_before) + (ff_an_mce_alternating_before) * (ff_bp_mce_alternating_before))) \/ ((exists ff_odd_mce_term_before_term. ff_index_mce_alternating_before = 2 * ff_odd_mce_term_before_term + 1) /\ (ff_p_mce_alternating_before = (ff_ap_mce_alternating_before) * (ff_bn_mce_alternating_before) + (ff_an_mce_alternating_before) * (ff_bp_mce_alternating_before) /\ ff_n_mce_alternating_before = (ff_ap_mce_alternating_before) * (ff_bp_mce_alternating_before) + (ff_an_mce_alternating_before) * (ff_bn_mce_alternating_before))))))))))) -> (((exists ff_h_mce_last_ap. ff_h_mce_last_ap + S (ap) = S ((S (l)) * ac)) /\ exists ff_q_mce_last_ap. ab = ff_q_mce_last_ap * S ((S (l)) * ac) + (ap))) -> (((exists ff_h_mce_last_an. ff_h_mce_last_an + S (an) = S ((S (l)) * dc)) /\ exists ff_q_mce_last_an. db = ff_q_mce_last_an * S ((S (l)) * dc) + (an))) -> (((exists ff_h_mce_last_bp. ff_h_mce_last_bp + S (bp) = S ((S (l)) * ec)) /\ exists ff_q_mce_last_bp. eb = ff_q_mce_last_bp * S ((S (l)) * ec) + (bp))) -> (((exists ff_h_mce_last_bn. ff_h_mce_last_bn + S (bn) = S ((S (l)) * fc)) /\ exists ff_q_mce_last_bn. fb = ff_q_mce_last_bn * S ((S (l)) * fc) + (bn))) -> (((exists ff_even_mce_term_last. l = 2 * ff_even_mce_term_last) /\ (p = (ap) * (bp) + (an) * (bn) /\ n = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_last. l = 2 * ff_odd_mce_term_last + 1) /\ (p = (ap) * (bn) + (an) * (bp) /\ n = (ap) * (bp) + (an) * (bn)))) -> exists xb xc yb yc. (forall ff_index_mce_alternating_after. (exists ff_gap_mce_after_index. ff_gap_mce_after_index + S (ff_index_mce_alternating_after) = (S l)) -> exists ff_ap_mce_alternating_after ff_an_mce_alternating_after ff_bp_mce_alternating_after ff_bn_mce_alternating_after ff_p_mce_alternating_after ff_n_mce_alternating_after. ((((exists ff_h_mce_after_ap. ff_h_mce_after_ap + S (ff_ap_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * ac)) /\ exists ff_q_mce_after_ap. ab = ff_q_mce_after_ap * S ((S (ff_index_mce_alternating_after)) * ac) + (ff_ap_mce_alternating_after))) /\ ((((exists ff_h_mce_after_an. ff_h_mce_after_an + S (ff_an_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * dc)) /\ exists ff_q_mce_after_an. db = ff_q_mce_after_an * S ((S (ff_index_mce_alternating_after)) * dc) + (ff_an_mce_alternating_after))) /\ ((((exists ff_h_mce_after_bp. ff_h_mce_after_bp + S (ff_bp_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * ec)) /\ exists ff_q_mce_after_bp. eb = ff_q_mce_after_bp * S ((S (ff_index_mce_alternating_after)) * ec) + (ff_bp_mce_alternating_after))) /\ ((((exists ff_h_mce_after_bn. ff_h_mce_after_bn + S (ff_bn_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * fc)) /\ exists ff_q_mce_after_bn. fb = ff_q_mce_after_bn * S ((S (ff_index_mce_alternating_after)) * fc) + (ff_bn_mce_alternating_after))) /\ ((((exists ff_h_mce_after_positive. ff_h_mce_after_positive + S (ff_p_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * xc)) /\ exists ff_q_mce_after_positive. xb = ff_q_mce_after_positive * S ((S (ff_index_mce_alternating_after)) * xc) + (ff_p_mce_alternating_after))) /\ ((((exists ff_h_mce_after_negative. ff_h_mce_after_negative + S (ff_n_mce_alternating_after) = S ((S (ff_index_mce_alternating_after)) * yc)) /\ exists ff_q_mce_after_negative. yb = ff_q_mce_after_negative * S ((S (ff_index_mce_alternating_after)) * yc) + (ff_n_mce_alternating_after))) /\ (((exists ff_even_mce_term_after_term. ff_index_mce_alternating_after = 2 * ff_even_mce_term_after_term) /\ (ff_p_mce_alternating_after = (ff_ap_mce_alternating_after) * (ff_bp_mce_alternating_after) + (ff_an_mce_alternating_after) * (ff_bn_mce_alternating_after) /\ ff_n_mce_alternating_after = (ff_ap_mce_alternating_after) * (ff_bn_mce_alternating_after) + (ff_an_mce_alternating_after) * (ff_bp_mce_alternating_after))) \/ ((exists ff_odd_mce_term_after_term. ff_index_mce_alternating_after = 2 * ff_odd_mce_term_after_term + 1) /\ (ff_p_mce_alternating_after = (ff_ap_mce_alternating_after) * (ff_bn_mce_alternating_after) + (ff_an_mce_alternating_after) * (ff_bp_mce_alternating_after) /\ ff_n_mce_alternating_after = (ff_ap_mce_alternating_after) * (ff_bp_mce_alternating_after) + (ff_an_mce_alternating_after) * (ff_bn_mce_alternating_after)))))))))))

Complete unchanged native tactic proof

All 131 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

131 script commands · 48 reading checkpoints · 4 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.

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 ab
  2. L2
    intro ac
  3. L3
    intro db
  4. L4
    intro dc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro ub
  10. L10
    intro uc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro vb
  2. L12
    intro vc
  3. L13
    intro l
  4. L14
    intro ap
  5. L15
    intro an
  6. L16
    intro bp
  7. L17
    intro bn
  8. L18
    intro p
  9. L19
    intro n
  10. L20
    intro hprefix
03Fix variables and assumptionsL21–25

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

  1. L21
    intro hap
  2. L22
    intro han
  3. L23
    intro hbp
  4. L24
    intro hbn
  5. L25
    intro hterm
04Establish hposL26–31

Establish this local claim before using it. It is not an additional assumption.

  1. L26
    have hpos : ∃ xb. ∃ xc. Beta(xb,xc,l,p) ∧ (∀ x. ∀ y. Lt(x,l) → Beta(ub,uc,x,y) → Beta(xb,xc,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L27
    specialize beta_prefix_extend l
  3. L28
    specialize beta_prefix_extend ub
  4. L29
    specialize beta_prefix_extend uc
  5. L30
    specialize beta_prefix_extend p
  6. L31
    exact beta_prefix_extend
05Separate the logical casesL32–34

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

  1. L32
    cases hpos
  2. L33
    cases hpos_witness
  3. L34
    cases hpos_witness_witness
06Establish hnegL35–40

Establish this local claim before using it. It is not an additional assumption.

  1. L35
    have hneg : ∃ yb. ∃ yc. Beta(yb,yc,l,n) ∧ (∀ x. ∀ y. Lt(x,l) → Beta(vb,vc,x,y) → Beta(yb,yc,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L36
    specialize beta_prefix_extend l
  3. L37
    specialize beta_prefix_extend vb
  4. L38
    specialize beta_prefix_extend vc
  5. L39
    specialize beta_prefix_extend n
  6. L40
    exact beta_prefix_extend
07Separate the logical casesL41–43

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

  1. L41
    cases hneg
  2. L42
    cases hneg_witness
  3. L43
    cases hneg_witness_witness
08Construct an explicit witnessL44–47

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

  1. L44
    exists x
  2. L45
    exists x1
  3. L46
    exists x2
  4. L47
    exists x3
09Fix variables and assumptionsL48–49

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

  1. L48
    intro i
  2. L49
    intro hi
10Establish hsplitL50–54

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. L50
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L51
    specialize finite_lt_succ_eq_or_lt l
  3. L52
    specialize finite_lt_succ_eq_or_lt i
  4. L53
    apply finite_lt_succ_eq_or_lt
  5. L54
    exact hi
11Separate the logical casesL55–55

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

  1. L55
    cases hsplit
12Construct an explicit witnessL56–61

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

  1. L56
    exists ap
  2. L57
    exists an
  3. L58
    exists bp
  4. L59
    exists bn
  5. L60
    exists p
  6. L61
    exists n
13Separate the logical casesL62–62

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

  1. L62
    split
14Calculate and transport equalitiesL63–64

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

  1. L63
    rewrite hsplit_left
  2. L64
    rewrite hsplit_left
15Use earlier factsL65–65

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

  1. L65
    exact hap
16Separate the logical casesL66–66

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

  1. L66
    split
17Calculate and transport equalitiesL67–68

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

  1. L67
    rewrite hsplit_left
  2. L68
    rewrite hsplit_left
18Use earlier factsL69–69

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

  1. L69
    exact han
19Separate the logical casesL70–70

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

  1. L70
    split
20Calculate and transport equalitiesL71–72

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

  1. L71
    rewrite hsplit_left
  2. L72
    rewrite hsplit_left
21Use earlier factsL73–73

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

  1. L73
    exact hbp
22Separate the logical casesL74–74

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

  1. L74
    split
23Calculate and transport equalitiesL75–76

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

  1. L75
    rewrite hsplit_left
  2. L76
    rewrite hsplit_left
24Use earlier factsL77–77

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

  1. L77
    exact hbn
25Separate the logical casesL78–78

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

  1. L78
    split
26Calculate and transport equalitiesL79–80

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

  1. L79
    rewrite hsplit_left
  2. L80
    rewrite hsplit_left
27Use earlier factsL81–81

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

  1. L81
    exact hpos_witness_witness_left
28Separate the logical casesL82–82

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

  1. L82
    split
29Calculate and transport equalitiesL83–84

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

  1. L83
    rewrite hsplit_left
  2. L84
    rewrite hsplit_left
30Use earlier factsL85–85

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

  1. L85
    exact hneg_witness_witness_left
31Calculate and transport equalitiesL86–87

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

  1. L86
    rewrite hsplit_left
  2. L87
    rewrite hsplit_left
32Use earlier factsL88–88

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

  1. L88
    exact hterm
33Establish hpreviousL89–92

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

  1. L89
    have hprevious : ∃ ap. ∃ an. ∃ bp. ∃ bn. ∃ p. ∃ n. Beta(ab,ac,i,ap) ∧ (Beta(db,dc,i,an) ∧ (Beta(eb,ec,i,bp) ∧ (Beta(fb,fc,i,bn) ∧ (Beta(ub,uc,i,p) ∧ (Beta(vb,vc,i,n) ∧ SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n))))))Definitions: BetaSignedAlternatingCofactorTermOriginal native command in the exact edition
  2. L90
    specialize hprefix i
  3. L91
    apply hprefix
  4. L92
    exact hsplit_right
34Separate the logical casesL93–102

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

  1. L93
    cases hprevious
  2. L94
    cases hprevious_witness
  3. L95
    cases hprevious_witness_witness
  4. L96
    cases hprevious_witness_witness_witness
  5. L97
    cases hprevious_witness_witness_witness_witness
  6. L98
    cases hprevious_witness_witness_witness_witness_witness
  7. L99
    cases hprevious_witness_witness_witness_witness_witness_witness
  8. L100
    cases hprevious_witness_witness_witness_witness_witness_witness_right
  9. L101
    cases hprevious_witness_witness_witness_witness_witness_witness_right_right
  10. L102
    cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right
35Separate the logical casesL103–104

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

  1. L103
    cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L104
    cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right
36Construct an explicit witnessL105–110

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

  1. L105
    exists x4
  2. L106
    exists x5
  3. L107
    exists x6
  4. L108
    exists x7
  5. L109
    exists x8
  6. L110
    exists x9
37Separate the logical casesL111–111

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

  1. L111
    split
38Use earlier factsL112–112

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

  1. L112
    exact hprevious_witness_witness_witness_witness_witness_witness_left
39Separate the logical casesL113–113

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

  1. L113
    split
40Use earlier factsL114–114

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

  1. L114
    exact hprevious_witness_witness_witness_witness_witness_witness_right_left
41Separate the logical casesL115–115

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

  1. L115
    split
42Use earlier factsL116–116

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

  1. L116
    exact hprevious_witness_witness_witness_witness_witness_witness_right_right_left
43Separate the logical casesL117–117

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

  1. L117
    split
44Use earlier factsL118–118

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

  1. L118
    exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_left
45Separate the logical casesL119–119

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

  1. L119
    split
46Use earlier factsL120–124

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

  1. L120
    specialize hpos_witness_witness_right i
  2. L121
    specialize hpos_witness_witness_right x8
  3. L122
    apply hpos_witness_witness_right
  4. L123
    exact hsplit_right
  5. L124
    exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_left
47Separate the logical casesL125–125

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

  1. L125
    split
48Use earlier factsL126–131

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

  1. L126
    specialize hneg_witness_witness_right i
  2. L127
    specialize hneg_witness_witness_right x9
  3. L128
    apply hneg_witness_witness_right
  4. L129
    exact hsplit_right
  5. L130
    exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  6. L131
    exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 131 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro db
  4. 0004intro dc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro ub
  10. 0010intro uc
  11. 0011intro vb
  12. 0012intro vc
  13. 0013intro l
  14. 0014intro ap
  15. 0015intro an
  16. 0016intro bp
  17. 0017intro bn
  18. 0018intro p
  19. 0019intro n
  20. 0020intro hprefix
  21. 0021intro hap
  22. 0022intro han
  23. 0023intro hbp
  24. 0024intro hbn
  25. 0025intro hterm
  26. 0026have hpos : exists xb xc. ((((exists ff_h_mce_extend_positive. ff_h_mce_extend_positive + S (p) = S ((S (l)) * xc)) /\ exists ff_q_mce_extend_positive. xb = ff_q_mce_extend_positive * S ((S (l)) * xc) + (p))) /\ forall i a. (exists ff_gap_mce_extend_positive_bound. ff_gap_mce_extend_positive_bound + S (i) = (l)) -> (((exists ff_h_mce_extend_positive_old. ff_h_mce_extend_positive_old + S (a) = S ((S (i)) * uc)) /\ exists ff_q_mce_extend_positive_old. ub = ff_q_mce_extend_positive_old * S ((S (i)) * uc) + (a))) -> (((exists ff_h_mce_extend_positive_new. ff_h_mce_extend_positive_new + S (a) = S ((S (i)) * xc)) /\ exists ff_q_mce_extend_positive_new. xb = ff_q_mce_extend_positive_new * S ((S (i)) * xc) + (a))))
  27. 0027specialize beta_prefix_extend l
  28. 0028specialize beta_prefix_extend ub
  29. 0029specialize beta_prefix_extend uc
  30. 0030specialize beta_prefix_extend p
  31. 0031exact beta_prefix_extend
  32. 0032cases hpos
  33. 0033cases hpos_witness
  34. 0034cases hpos_witness_witness
  35. 0035have hneg : exists yb yc. ((((exists ff_h_mce_extend_negative. ff_h_mce_extend_negative + S (n) = S ((S (l)) * yc)) /\ exists ff_q_mce_extend_negative. yb = ff_q_mce_extend_negative * S ((S (l)) * yc) + (n))) /\ forall i a. (exists ff_gap_mce_extend_negative_bound. ff_gap_mce_extend_negative_bound + S (i) = (l)) -> (((exists ff_h_mce_extend_negative_old. ff_h_mce_extend_negative_old + S (a) = S ((S (i)) * vc)) /\ exists ff_q_mce_extend_negative_old. vb = ff_q_mce_extend_negative_old * S ((S (i)) * vc) + (a))) -> (((exists ff_h_mce_extend_negative_new. ff_h_mce_extend_negative_new + S (a) = S ((S (i)) * yc)) /\ exists ff_q_mce_extend_negative_new. yb = ff_q_mce_extend_negative_new * S ((S (i)) * yc) + (a))))
  36. 0036specialize beta_prefix_extend l
  37. 0037specialize beta_prefix_extend vb
  38. 0038specialize beta_prefix_extend vc
  39. 0039specialize beta_prefix_extend n
  40. 0040exact beta_prefix_extend
  41. 0041cases hneg
  42. 0042cases hneg_witness
  43. 0043cases hneg_witness_witness
  44. 0044exists x
  45. 0045exists x1
  46. 0046exists x2
  47. 0047exists x3
  48. 0048intro i
  49. 0049intro hi
  50. 0050have hsplit : i = l \/ exists gap. gap + S i = l
  51. 0051specialize finite_lt_succ_eq_or_lt l
  52. 0052specialize finite_lt_succ_eq_or_lt i
  53. 0053apply finite_lt_succ_eq_or_lt
  54. 0054exact hi
  55. 0055cases hsplit
  56. 0056exists ap
  57. 0057exists an
  58. 0058exists bp
  59. 0059exists bn
  60. 0060exists p
  61. 0061exists n
  62. 0062split
  63. 0063rewrite hsplit_left
  64. 0064rewrite hsplit_left
  65. 0065exact hap
  66. 0066split
  67. 0067rewrite hsplit_left
  68. 0068rewrite hsplit_left
  69. 0069exact han
  70. 0070split
  71. 0071rewrite hsplit_left
  72. 0072rewrite hsplit_left
  73. 0073exact hbp
  74. 0074split
  75. 0075rewrite hsplit_left
  76. 0076rewrite hsplit_left
  77. 0077exact hbn
  78. 0078split
  79. 0079rewrite hsplit_left
  80. 0080rewrite hsplit_left
  81. 0081exact hpos_witness_witness_left
  82. 0082split
  83. 0083rewrite hsplit_left
  84. 0084rewrite hsplit_left
  85. 0085exact hneg_witness_witness_left
  86. 0086rewrite hsplit_left
  87. 0087rewrite hsplit_left
  88. 0088exact hterm
  89. 0089have hprevious : exists ap an bp bn p n. ((((exists ff_h_mce_previous_ap. ff_h_mce_previous_ap + S (ap) = S ((S (i)) * ac)) /\ exists ff_q_mce_previous_ap. ab = ff_q_mce_previous_ap * S ((S (i)) * ac) + (ap))) /\ ((((exists ff_h_mce_previous_an. ff_h_mce_previous_an + S (an) = S ((S (i)) * dc)) /\ exists ff_q_mce_previous_an. db = ff_q_mce_previous_an * S ((S (i)) * dc) + (an))) /\ ((((exists ff_h_mce_previous_bp. ff_h_mce_previous_bp + S (bp) = S ((S (i)) * ec)) /\ exists ff_q_mce_previous_bp. eb = ff_q_mce_previous_bp * S ((S (i)) * ec) + (bp))) /\ ((((exists ff_h_mce_previous_bn. ff_h_mce_previous_bn + S (bn) = S ((S (i)) * fc)) /\ exists ff_q_mce_previous_bn. fb = ff_q_mce_previous_bn * S ((S (i)) * fc) + (bn))) /\ ((((exists ff_h_mce_previous_positive. ff_h_mce_previous_positive + S (p) = S ((S (i)) * uc)) /\ exists ff_q_mce_previous_positive. ub = ff_q_mce_previous_positive * S ((S (i)) * uc) + (p))) /\ ((((exists ff_h_mce_previous_negative. ff_h_mce_previous_negative + S (n) = S ((S (i)) * vc)) /\ exists ff_q_mce_previous_negative. vb = ff_q_mce_previous_negative * S ((S (i)) * vc) + (n))) /\ (((exists ff_even_mce_term_previous_term. i = 2 * ff_even_mce_term_previous_term) /\ (p = (ap) * (bp) + (an) * (bn) /\ n = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_previous_term. i = 2 * ff_odd_mce_term_previous_term + 1) /\ (p = (ap) * (bn) + (an) * (bp) /\ n = (ap) * (bp) + (an) * (bn))))))))))
  90. 0090specialize hprefix i
  91. 0091apply hprefix
  92. 0092exact hsplit_right
  93. 0093cases hprevious
  94. 0094cases hprevious_witness
  95. 0095cases hprevious_witness_witness
  96. 0096cases hprevious_witness_witness_witness
  97. 0097cases hprevious_witness_witness_witness_witness
  98. 0098cases hprevious_witness_witness_witness_witness_witness
  99. 0099cases hprevious_witness_witness_witness_witness_witness_witness
  100. 0100cases hprevious_witness_witness_witness_witness_witness_witness_right
  101. 0101cases hprevious_witness_witness_witness_witness_witness_witness_right_right
  102. 0102cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right
  103. 0103cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right
  104. 0104cases hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  105. 0105exists x4
  106. 0106exists x5
  107. 0107exists x6
  108. 0108exists x7
  109. 0109exists x8
  110. 0110exists x9
  111. 0111split
  112. 0112exact hprevious_witness_witness_witness_witness_witness_witness_left
  113. 0113split
  114. 0114exact hprevious_witness_witness_witness_witness_witness_witness_right_left
  115. 0115split
  116. 0116exact hprevious_witness_witness_witness_witness_witness_witness_right_right_left
  117. 0117split
  118. 0118exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_left
  119. 0119split
  120. 0120specialize hpos_witness_witness_right i
  121. 0121specialize hpos_witness_witness_right x8
  122. 0122apply hpos_witness_witness_right
  123. 0123exact hsplit_right
  124. 0124exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  125. 0125split
  126. 0126specialize hneg_witness_witness_right i
  127. 0127specialize hneg_witness_witness_right x9
  128. 0128apply hneg_witness_witness_right
  129. 0129exact hsplit_right
  130. 0130exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  131. 0131exact hprevious_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right