CE0016

signed_alternating_product_prefix_pointwise_functional

Both components of every arbitrary-arity signed alternating cofactor term are independent of all beta-recoding witnesses.

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. ∀ wb. ∀ wc. ∀ zb. ∀ zc. ∀ l. ∀ i. ∀ p. ∀ n. ∀ r. ∀ s. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) → SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,wb,wc,zb,zc,l) → Lt(i,l) → Beta(ub,uc,i,p) → Beta(vb,vc,i,n) → Beta(wb,wc,i,r) → Beta(zb,zc,i,s) → p = r ∧ n = s

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

Definition DAG

Beta(b,c,i,x) · 4SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) · 2Lt(a,b) · 1

Actual proof prerequisites

beta_at_exists · checked external prerequisitesigned_alternating_product_prefix_exact_termsigned_alternating_cofactor_term_functional
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc ub uc vb vc wb wc zb zc l i p n r s. (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))))))))))) -> (forall ff_index_mce_alternating_other. (exists ff_gap_mce_other_index. ff_gap_mce_other_index + S (ff_index_mce_alternating_other) = (l)) -> exists ff_ap_mce_alternating_other ff_an_mce_alternating_other ff_bp_mce_alternating_other ff_bn_mce_alternating_other ff_p_mce_alternating_other ff_n_mce_alternating_other. ((((exists ff_h_mce_other_ap. ff_h_mce_other_ap + S (ff_ap_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * ac)) /\ exists ff_q_mce_other_ap. ab = ff_q_mce_other_ap * S ((S (ff_index_mce_alternating_other)) * ac) + (ff_ap_mce_alternating_other))) /\ ((((exists ff_h_mce_other_an. ff_h_mce_other_an + S (ff_an_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * dc)) /\ exists ff_q_mce_other_an. db = ff_q_mce_other_an * S ((S (ff_index_mce_alternating_other)) * dc) + (ff_an_mce_alternating_other))) /\ ((((exists ff_h_mce_other_bp. ff_h_mce_other_bp + S (ff_bp_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * ec)) /\ exists ff_q_mce_other_bp. eb = ff_q_mce_other_bp * S ((S (ff_index_mce_alternating_other)) * ec) + (ff_bp_mce_alternating_other))) /\ ((((exists ff_h_mce_other_bn. ff_h_mce_other_bn + S (ff_bn_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * fc)) /\ exists ff_q_mce_other_bn. fb = ff_q_mce_other_bn * S ((S (ff_index_mce_alternating_other)) * fc) + (ff_bn_mce_alternating_other))) /\ ((((exists ff_h_mce_other_positive. ff_h_mce_other_positive + S (ff_p_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * wc)) /\ exists ff_q_mce_other_positive. wb = ff_q_mce_other_positive * S ((S (ff_index_mce_alternating_other)) * wc) + (ff_p_mce_alternating_other))) /\ ((((exists ff_h_mce_other_negative. ff_h_mce_other_negative + S (ff_n_mce_alternating_other) = S ((S (ff_index_mce_alternating_other)) * zc)) /\ exists ff_q_mce_other_negative. zb = ff_q_mce_other_negative * S ((S (ff_index_mce_alternating_other)) * zc) + (ff_n_mce_alternating_other))) /\ (((exists ff_even_mce_term_other_term. ff_index_mce_alternating_other = 2 * ff_even_mce_term_other_term) /\ (ff_p_mce_alternating_other = (ff_ap_mce_alternating_other) * (ff_bp_mce_alternating_other) + (ff_an_mce_alternating_other) * (ff_bn_mce_alternating_other) /\ ff_n_mce_alternating_other = (ff_ap_mce_alternating_other) * (ff_bn_mce_alternating_other) + (ff_an_mce_alternating_other) * (ff_bp_mce_alternating_other))) \/ ((exists ff_odd_mce_term_other_term. ff_index_mce_alternating_other = 2 * ff_odd_mce_term_other_term + 1) /\ (ff_p_mce_alternating_other = (ff_ap_mce_alternating_other) * (ff_bn_mce_alternating_other) + (ff_an_mce_alternating_other) * (ff_bp_mce_alternating_other) /\ ff_n_mce_alternating_other = (ff_ap_mce_alternating_other) * (ff_bp_mce_alternating_other) + (ff_an_mce_alternating_other) * (ff_bn_mce_alternating_other))))))))))) -> (exists ff_gap_mce_value_bound. ff_gap_mce_value_bound + S (i) = (l)) -> (((exists ff_h_mce_pointwise_first_positive. ff_h_mce_pointwise_first_positive + S (p) = S ((S (i)) * uc)) /\ exists ff_q_mce_pointwise_first_positive. ub = ff_q_mce_pointwise_first_positive * S ((S (i)) * uc) + (p))) -> (((exists ff_h_mce_pointwise_first_negative. ff_h_mce_pointwise_first_negative + S (n) = S ((S (i)) * vc)) /\ exists ff_q_mce_pointwise_first_negative. vb = ff_q_mce_pointwise_first_negative * S ((S (i)) * vc) + (n))) -> (((exists ff_h_mce_pointwise_second_positive. ff_h_mce_pointwise_second_positive + S (r) = S ((S (i)) * wc)) /\ exists ff_q_mce_pointwise_second_positive. wb = ff_q_mce_pointwise_second_positive * S ((S (i)) * wc) + (r))) -> (((exists ff_h_mce_pointwise_second_negative. ff_h_mce_pointwise_second_negative + S (s) = S ((S (i)) * zc)) /\ exists ff_q_mce_pointwise_second_negative. zb = ff_q_mce_pointwise_second_negative * S ((S (i)) * zc) + (s))) -> (p = r /\ n = s)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

125 script commands · 19 reading checkpoints · 6 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 (2)
signed alternating product prefix exact termsigned alternating cofactor term functional
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 wb
  4. L14
    intro wc
  5. L15
    intro zb
  6. L16
    intro zc
  7. L17
    intro l
  8. L18
    intro i
  9. L19
    intro p
  10. L20
    intro n
03Fix variables and assumptionsL21–29

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

  1. L21
    intro r
  2. L22
    intro s
  3. L23
    intro hfirst
  4. L24
    intro hsecond
  5. L25
    intro hbound
  6. L26
    intro hp
  7. L27
    intro hn
  8. L28
    intro hr
  9. L29
    intro hs
04Establish hapL30–34

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

  1. L30
    have hap : exists a. (((exists ff_h_mce_functional_ap. ff_h_mce_functional_ap + S (a) = S ((S (i)) * ac)) /\ exists ff_q_mce_functional_ap. ab = ff_q_mce_functional_ap * S ((S (i)) * ac) + (a)))
  2. L31
    specialize beta_at_exists ab
  3. L32
    specialize beta_at_exists ac
  4. L33
    specialize beta_at_exists i
  5. L34
    exact beta_at_exists
05Separate the logical casesL35–35

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

  1. L35
    cases hap
06Establish hanL36–40

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

  1. L36
    have han : exists a. (((exists ff_h_mce_functional_an. ff_h_mce_functional_an + S (a) = S ((S (i)) * dc)) /\ exists ff_q_mce_functional_an. db = ff_q_mce_functional_an * S ((S (i)) * dc) + (a)))
  2. L37
    specialize beta_at_exists db
  3. L38
    specialize beta_at_exists dc
  4. L39
    specialize beta_at_exists i
  5. L40
    exact beta_at_exists
07Separate the logical casesL41–41

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

  1. L41
    cases han
08Establish hbpL42–46

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

  1. L42
    have hbp : exists a. (((exists ff_h_mce_functional_bp. ff_h_mce_functional_bp + S (a) = S ((S (i)) * ec)) /\ exists ff_q_mce_functional_bp. eb = ff_q_mce_functional_bp * S ((S (i)) * ec) + (a)))
  2. L43
    specialize beta_at_exists eb
  3. L44
    specialize beta_at_exists ec
  4. L45
    specialize beta_at_exists i
  5. L46
    exact beta_at_exists
09Separate the logical casesL47–47

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

  1. L47
    cases hbp
10Establish hbnL48–52

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

  1. L48
    have hbn : exists a. (((exists ff_h_mce_functional_bn. ff_h_mce_functional_bn + S (a) = S ((S (i)) * fc)) /\ exists ff_q_mce_functional_bn. fb = ff_q_mce_functional_bn * S ((S (i)) * fc) + (a)))
  2. L49
    specialize beta_at_exists fb
  3. L50
    specialize beta_at_exists fc
  4. L51
    specialize beta_at_exists i
  5. L52
    exact beta_at_exists
11Separate the logical casesL53–53

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

  1. L53
    cases hbn
12Establish hleftL54–63

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

  1. L54
    have hleft : (((exists ff_even_mce_term_functional_left. i = 2 * ff_even_mce_term_functional_left) /\ (p = (x) * (x2) + (x1) * (x3) /\ n = (x) * (x3) + (x1) * (x2))) \/ ((exists ff_odd_mce_term_functional_left. i = 2 * ff_odd_mce_term_functional_left + 1) /\ (p = (x) * (x3) + (x1) * (x2) /\ n = (x) * (x2) + (x1) * (x3))))
  2. L55
    specialize signed_alternating_product_prefix_exact_term ab
  3. L56
    specialize signed_alternating_product_prefix_exact_term ac
  4. L57
    specialize signed_alternating_product_prefix_exact_term db
  5. L58
    specialize signed_alternating_product_prefix_exact_term dc
  6. L59
    specialize signed_alternating_product_prefix_exact_term eb
  7. L60
    specialize signed_alternating_product_prefix_exact_term ec
  8. L61
    specialize signed_alternating_product_prefix_exact_term fb
  9. L62
    specialize signed_alternating_product_prefix_exact_term fc
  10. L63
    specialize signed_alternating_product_prefix_exact_term ub
13Use earlier factsL64–73

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

  1. L64
    specialize signed_alternating_product_prefix_exact_term uc
  2. L65
    specialize signed_alternating_product_prefix_exact_term vb
  3. L66
    specialize signed_alternating_product_prefix_exact_term vc
  4. L67
    specialize signed_alternating_product_prefix_exact_term l
  5. L68
    specialize signed_alternating_product_prefix_exact_term i
  6. L69
    specialize signed_alternating_product_prefix_exact_term x
  7. L70
    specialize signed_alternating_product_prefix_exact_term x1
  8. L71
    specialize signed_alternating_product_prefix_exact_term x2
  9. L72
    specialize signed_alternating_product_prefix_exact_term x3
  10. L73
    specialize signed_alternating_product_prefix_exact_term p
14Use earlier factsL74–83

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

  1. L74
    specialize signed_alternating_product_prefix_exact_term n
  2. L75
    apply signed_alternating_product_prefix_exact_term
  3. L76
    exact hfirst
  4. L77
    exact hbound
  5. L78
    exact hap_witness
  6. L79
    exact han_witness
  7. L80
    exact hbp_witness
  8. L81
    exact hbn_witness
  9. L82
    exact hp
  10. L83
    exact hn
15Establish hrightL84–93

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

  1. L84
    have hright : (((exists ff_even_mce_term_functional_right. i = 2 * ff_even_mce_term_functional_right) /\ (r = (x) * (x2) + (x1) * (x3) /\ s = (x) * (x3) + (x1) * (x2))) \/ ((exists ff_odd_mce_term_functional_right. i = 2 * ff_odd_mce_term_functional_right + 1) /\ (r = (x) * (x3) + (x1) * (x2) /\ s = (x) * (x2) + (x1) * (x3))))
  2. L85
    specialize signed_alternating_product_prefix_exact_term ab
  3. L86
    specialize signed_alternating_product_prefix_exact_term ac
  4. L87
    specialize signed_alternating_product_prefix_exact_term db
  5. L88
    specialize signed_alternating_product_prefix_exact_term dc
  6. L89
    specialize signed_alternating_product_prefix_exact_term eb
  7. L90
    specialize signed_alternating_product_prefix_exact_term ec
  8. L91
    specialize signed_alternating_product_prefix_exact_term fb
  9. L92
    specialize signed_alternating_product_prefix_exact_term fc
  10. L93
    specialize signed_alternating_product_prefix_exact_term wb
16Use earlier factsL94–103

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

  1. L94
    specialize signed_alternating_product_prefix_exact_term wc
  2. L95
    specialize signed_alternating_product_prefix_exact_term zb
  3. L96
    specialize signed_alternating_product_prefix_exact_term zc
  4. L97
    specialize signed_alternating_product_prefix_exact_term l
  5. L98
    specialize signed_alternating_product_prefix_exact_term i
  6. L99
    specialize signed_alternating_product_prefix_exact_term x
  7. L100
    specialize signed_alternating_product_prefix_exact_term x1
  8. L101
    specialize signed_alternating_product_prefix_exact_term x2
  9. L102
    specialize signed_alternating_product_prefix_exact_term x3
  10. L103
    specialize signed_alternating_product_prefix_exact_term r
17Use earlier factsL104–113

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

  1. L104
    specialize signed_alternating_product_prefix_exact_term s
  2. L105
    apply signed_alternating_product_prefix_exact_term
  3. L106
    exact hsecond
  4. L107
    exact hbound
  5. L108
    exact hap_witness
  6. L109
    exact han_witness
  7. L110
    exact hbp_witness
  8. L111
    exact hbn_witness
  9. L112
    exact hr
  10. L113
    exact hs
18Use earlier factsL114–123

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

  1. L114
    specialize signed_alternating_cofactor_term_functional x
  2. L115
    specialize signed_alternating_cofactor_term_functional x1
  3. L116
    specialize signed_alternating_cofactor_term_functional x2
  4. L117
    specialize signed_alternating_cofactor_term_functional x3
  5. L118
    specialize signed_alternating_cofactor_term_functional i
  6. L119
    specialize signed_alternating_cofactor_term_functional p
  7. L120
    specialize signed_alternating_cofactor_term_functional n
  8. L121
    specialize signed_alternating_cofactor_term_functional r
  9. L122
    specialize signed_alternating_cofactor_term_functional s
  10. L123
    apply signed_alternating_cofactor_term_functional
19Use earlier factsL124–125

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

  1. L124
    exact hleft
  2. L125
    exact hright

Library-wide reading audit

Original defined command ledger · 125 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 wb
  14. 0014intro wc
  15. 0015intro zb
  16. 0016intro zc
  17. 0017intro l
  18. 0018intro i
  19. 0019intro p
  20. 0020intro n
  21. 0021intro r
  22. 0022intro s
  23. 0023intro hfirst
  24. 0024intro hsecond
  25. 0025intro hbound
  26. 0026intro hp
  27. 0027intro hn
  28. 0028intro hr
  29. 0029intro hs
  30. 0030have hap : exists a. (((exists ff_h_mce_functional_ap. ff_h_mce_functional_ap + S (a) = S ((S (i)) * ac)) /\ exists ff_q_mce_functional_ap. ab = ff_q_mce_functional_ap * S ((S (i)) * ac) + (a)))
  31. 0031specialize beta_at_exists ab
  32. 0032specialize beta_at_exists ac
  33. 0033specialize beta_at_exists i
  34. 0034exact beta_at_exists
  35. 0035cases hap
  36. 0036have han : exists a. (((exists ff_h_mce_functional_an. ff_h_mce_functional_an + S (a) = S ((S (i)) * dc)) /\ exists ff_q_mce_functional_an. db = ff_q_mce_functional_an * S ((S (i)) * dc) + (a)))
  37. 0037specialize beta_at_exists db
  38. 0038specialize beta_at_exists dc
  39. 0039specialize beta_at_exists i
  40. 0040exact beta_at_exists
  41. 0041cases han
  42. 0042have hbp : exists a. (((exists ff_h_mce_functional_bp. ff_h_mce_functional_bp + S (a) = S ((S (i)) * ec)) /\ exists ff_q_mce_functional_bp. eb = ff_q_mce_functional_bp * S ((S (i)) * ec) + (a)))
  43. 0043specialize beta_at_exists eb
  44. 0044specialize beta_at_exists ec
  45. 0045specialize beta_at_exists i
  46. 0046exact beta_at_exists
  47. 0047cases hbp
  48. 0048have hbn : exists a. (((exists ff_h_mce_functional_bn. ff_h_mce_functional_bn + S (a) = S ((S (i)) * fc)) /\ exists ff_q_mce_functional_bn. fb = ff_q_mce_functional_bn * S ((S (i)) * fc) + (a)))
  49. 0049specialize beta_at_exists fb
  50. 0050specialize beta_at_exists fc
  51. 0051specialize beta_at_exists i
  52. 0052exact beta_at_exists
  53. 0053cases hbn
  54. 0054have hleft : (((exists ff_even_mce_term_functional_left. i = 2 * ff_even_mce_term_functional_left) /\ (p = (x) * (x2) + (x1) * (x3) /\ n = (x) * (x3) + (x1) * (x2))) \/ ((exists ff_odd_mce_term_functional_left. i = 2 * ff_odd_mce_term_functional_left + 1) /\ (p = (x) * (x3) + (x1) * (x2) /\ n = (x) * (x2) + (x1) * (x3))))
  55. 0055specialize signed_alternating_product_prefix_exact_term ab
  56. 0056specialize signed_alternating_product_prefix_exact_term ac
  57. 0057specialize signed_alternating_product_prefix_exact_term db
  58. 0058specialize signed_alternating_product_prefix_exact_term dc
  59. 0059specialize signed_alternating_product_prefix_exact_term eb
  60. 0060specialize signed_alternating_product_prefix_exact_term ec
  61. 0061specialize signed_alternating_product_prefix_exact_term fb
  62. 0062specialize signed_alternating_product_prefix_exact_term fc
  63. 0063specialize signed_alternating_product_prefix_exact_term ub
  64. 0064specialize signed_alternating_product_prefix_exact_term uc
  65. 0065specialize signed_alternating_product_prefix_exact_term vb
  66. 0066specialize signed_alternating_product_prefix_exact_term vc
  67. 0067specialize signed_alternating_product_prefix_exact_term l
  68. 0068specialize signed_alternating_product_prefix_exact_term i
  69. 0069specialize signed_alternating_product_prefix_exact_term x
  70. 0070specialize signed_alternating_product_prefix_exact_term x1
  71. 0071specialize signed_alternating_product_prefix_exact_term x2
  72. 0072specialize signed_alternating_product_prefix_exact_term x3
  73. 0073specialize signed_alternating_product_prefix_exact_term p
  74. 0074specialize signed_alternating_product_prefix_exact_term n
  75. 0075apply signed_alternating_product_prefix_exact_term
  76. 0076exact hfirst
  77. 0077exact hbound
  78. 0078exact hap_witness
  79. 0079exact han_witness
  80. 0080exact hbp_witness
  81. 0081exact hbn_witness
  82. 0082exact hp
  83. 0083exact hn
  84. 0084have hright : (((exists ff_even_mce_term_functional_right. i = 2 * ff_even_mce_term_functional_right) /\ (r = (x) * (x2) + (x1) * (x3) /\ s = (x) * (x3) + (x1) * (x2))) \/ ((exists ff_odd_mce_term_functional_right. i = 2 * ff_odd_mce_term_functional_right + 1) /\ (r = (x) * (x3) + (x1) * (x2) /\ s = (x) * (x2) + (x1) * (x3))))
  85. 0085specialize signed_alternating_product_prefix_exact_term ab
  86. 0086specialize signed_alternating_product_prefix_exact_term ac
  87. 0087specialize signed_alternating_product_prefix_exact_term db
  88. 0088specialize signed_alternating_product_prefix_exact_term dc
  89. 0089specialize signed_alternating_product_prefix_exact_term eb
  90. 0090specialize signed_alternating_product_prefix_exact_term ec
  91. 0091specialize signed_alternating_product_prefix_exact_term fb
  92. 0092specialize signed_alternating_product_prefix_exact_term fc
  93. 0093specialize signed_alternating_product_prefix_exact_term wb
  94. 0094specialize signed_alternating_product_prefix_exact_term wc
  95. 0095specialize signed_alternating_product_prefix_exact_term zb
  96. 0096specialize signed_alternating_product_prefix_exact_term zc
  97. 0097specialize signed_alternating_product_prefix_exact_term l
  98. 0098specialize signed_alternating_product_prefix_exact_term i
  99. 0099specialize signed_alternating_product_prefix_exact_term x
  100. 0100specialize signed_alternating_product_prefix_exact_term x1
  101. 0101specialize signed_alternating_product_prefix_exact_term x2
  102. 0102specialize signed_alternating_product_prefix_exact_term x3
  103. 0103specialize signed_alternating_product_prefix_exact_term r
  104. 0104specialize signed_alternating_product_prefix_exact_term s
  105. 0105apply signed_alternating_product_prefix_exact_term
  106. 0106exact hsecond
  107. 0107exact hbound
  108. 0108exact hap_witness
  109. 0109exact han_witness
  110. 0110exact hbp_witness
  111. 0111exact hbn_witness
  112. 0112exact hr
  113. 0113exact hs
  114. 0114specialize signed_alternating_cofactor_term_functional x
  115. 0115specialize signed_alternating_cofactor_term_functional x1
  116. 0116specialize signed_alternating_cofactor_term_functional x2
  117. 0117specialize signed_alternating_cofactor_term_functional x3
  118. 0118specialize signed_alternating_cofactor_term_functional i
  119. 0119specialize signed_alternating_cofactor_term_functional p
  120. 0120specialize signed_alternating_cofactor_term_functional n
  121. 0121specialize signed_alternating_cofactor_term_functional r
  122. 0122specialize signed_alternating_cofactor_term_functional s
  123. 0123apply signed_alternating_cofactor_term_functional
  124. 0124exact hleft
  125. 0125exact hright