CE0015

signed_alternating_product_prefix_exact_term

Any actual entries decoded from a signed alternating prefix satisfy the exact parity-correct signed cofactor term relation.

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. ∀ i. ∀ ap. ∀ an. ∀ bp. ∀ bn. ∀ p. ∀ n. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) → Lt(i,l) → 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)

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

Definition DAG

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

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc ub uc vb vc l i 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_gap_mce_value_bound. ff_gap_mce_value_bound + S (i) = (l)) -> (((exists ff_h_mce_value_ap. ff_h_mce_value_ap + S (ap) = S ((S (i)) * ac)) /\ exists ff_q_mce_value_ap. ab = ff_q_mce_value_ap * S ((S (i)) * ac) + (ap))) -> (((exists ff_h_mce_value_an. ff_h_mce_value_an + S (an) = S ((S (i)) * dc)) /\ exists ff_q_mce_value_an. db = ff_q_mce_value_an * S ((S (i)) * dc) + (an))) -> (((exists ff_h_mce_value_bp. ff_h_mce_value_bp + S (bp) = S ((S (i)) * ec)) /\ exists ff_q_mce_value_bp. eb = ff_q_mce_value_bp * S ((S (i)) * ec) + (bp))) -> (((exists ff_h_mce_value_bn. ff_h_mce_value_bn + S (bn) = S ((S (i)) * fc)) /\ exists ff_q_mce_value_bn. fb = ff_q_mce_value_bn * S ((S (i)) * fc) + (bn))) -> (((exists ff_h_mce_value_positive. ff_h_mce_value_positive + S (p) = S ((S (i)) * uc)) /\ exists ff_q_mce_value_positive. ub = ff_q_mce_value_positive * S ((S (i)) * uc) + (p))) -> (((exists ff_h_mce_value_negative. ff_h_mce_value_negative + S (n) = S ((S (i)) * vc)) /\ exists ff_q_mce_value_negative. vb = ff_q_mce_value_negative * S ((S (i)) * vc) + (n))) -> (((exists ff_even_mce_term_result. i = 2 * ff_even_mce_term_result) /\ (p = (ap) * (bp) + (an) * (bn) /\ n = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_result. i = 2 * ff_odd_mce_term_result + 1) /\ (p = (ap) * (bn) + (an) * (bp) /\ n = (ap) * (bp) + (an) * (bn))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

119 script commands · 15 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.

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 i
  5. L15
    intro ap
  6. L16
    intro an
  7. L17
    intro bp
  8. L18
    intro bn
  9. L19
    intro p
  10. L20
    intro n
03Fix variables and assumptionsL21–28

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

  1. L21
    intro hprefix
  2. L22
    intro hbound
  3. L23
    intro hap
  4. L24
    intro han
  5. L25
    intro hbp
  6. L26
    intro hbn
  7. L27
    intro hp
  8. L28
    intro hn
04Establish hentryL29–32

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

  1. L29
    have hentry : ∃ aa. ∃ dd. ∃ ee. ∃ ff. ∃ pp. ∃ nn. Beta(ab,ac,i,aa) ∧ (Beta(db,dc,i,dd) ∧ (Beta(eb,ec,i,ee) ∧ (Beta(fb,fc,i,ff) ∧ (Beta(ub,uc,i,pp) ∧ (Beta(vb,vc,i,nn) ∧ SignedAlternatingCofactorTerm(aa,dd,ee,ff,i,pp,nn))))))Definitions: BetaSignedAlternatingCofactorTermOriginal native command in the exact edition
  2. L30
    specialize hprefix i
  3. L31
    apply hprefix
  4. L32
    exact hbound
05Separate the logical casesL33–42

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

  1. L33
    cases hentry
  2. L34
    cases hentry_witness
  3. L35
    cases hentry_witness_witness
  4. L36
    cases hentry_witness_witness_witness
  5. L37
    cases hentry_witness_witness_witness_witness
  6. L38
    cases hentry_witness_witness_witness_witness_witness
  7. L39
    cases hentry_witness_witness_witness_witness_witness_witness
  8. L40
    cases hentry_witness_witness_witness_witness_witness_witness_right
  9. L41
    cases hentry_witness_witness_witness_witness_witness_witness_right_right
  10. L42
    cases hentry_witness_witness_witness_witness_witness_witness_right_right_right
06Separate the logical casesL43–44

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

  1. L43
    cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  2. L44
    cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
07Establish hapaL45–53

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

  1. L45
    have hapa : x = ap
  2. L46
    specialize beta_at_unique ab
  3. L47
    specialize beta_at_unique ac
  4. L48
    specialize beta_at_unique i
  5. L49
    specialize beta_at_unique x
  6. L50
    specialize beta_at_unique ap
  7. L51
    apply beta_at_unique
  8. L52
    exact hentry_witness_witness_witness_witness_witness_witness_left
  9. L53
    exact hap
08Establish hanaL54–62

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

  1. L54
    have hana : x1 = an
  2. L55
    specialize beta_at_unique db
  3. L56
    specialize beta_at_unique dc
  4. L57
    specialize beta_at_unique i
  5. L58
    specialize beta_at_unique x1
  6. L59
    specialize beta_at_unique an
  7. L60
    apply beta_at_unique
  8. L61
    exact hentry_witness_witness_witness_witness_witness_witness_right_left
  9. L62
    exact han
09Establish hbpaL63–71

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

  1. L63
    have hbpa : x2 = bp
  2. L64
    specialize beta_at_unique eb
  3. L65
    specialize beta_at_unique ec
  4. L66
    specialize beta_at_unique i
  5. L67
    specialize beta_at_unique x2
  6. L68
    specialize beta_at_unique bp
  7. L69
    apply beta_at_unique
  8. L70
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
  9. L71
    exact hbp
10Establish hbnaL72–80

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

  1. L72
    have hbna : x3 = bn
  2. L73
    specialize beta_at_unique fb
  3. L74
    specialize beta_at_unique fc
  4. L75
    specialize beta_at_unique i
  5. L76
    specialize beta_at_unique x3
  6. L77
    specialize beta_at_unique bn
  7. L78
    apply beta_at_unique
  8. L79
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  9. L80
    exact hbn
11Establish hpaL81–89

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

  1. L81
    have hpa : x4 = p
  2. L82
    specialize beta_at_unique ub
  3. L83
    specialize beta_at_unique uc
  4. L84
    specialize beta_at_unique i
  5. L85
    specialize beta_at_unique x4
  6. L86
    specialize beta_at_unique p
  7. L87
    apply beta_at_unique
  8. L88
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  9. L89
    exact hp
12Establish hnaL90–99

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

  1. L90
    have hna : x5 = n
  2. L91
    specialize beta_at_unique vb
  3. L92
    specialize beta_at_unique vc
  4. L93
    specialize beta_at_unique i
  5. L94
    specialize beta_at_unique x5
  6. L95
    specialize beta_at_unique n
  7. L96
    apply beta_at_unique
  8. L97
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  9. L98
    exact hn
  10. L99
    rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
13Calculate and transport equalitiesL100–109

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

  1. L100
    rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  2. L101
    rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  3. L102
    rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  4. L103
    rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  5. L104
    rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L105
    rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  7. L106
    rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  8. L107
    rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  9. L108
    rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  10. L109
    rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
14Calculate and transport equalitiesL110–118

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

  1. L110
    rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  2. L111
    rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  3. L112
    rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  4. L113
    rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  5. L114
    rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  6. L115
    rewrite hpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  7. L116
    rewrite hpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  8. L117
    rewrite hna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  9. L118
    rewrite hna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
15Use earlier factsL119–119

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

  1. L119
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 119 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 i
  15. 0015intro ap
  16. 0016intro an
  17. 0017intro bp
  18. 0018intro bn
  19. 0019intro p
  20. 0020intro n
  21. 0021intro hprefix
  22. 0022intro hbound
  23. 0023intro hap
  24. 0024intro han
  25. 0025intro hbp
  26. 0026intro hbn
  27. 0027intro hp
  28. 0028intro hn
  29. 0029have hentry : exists aa dd ee ff pp nn. ((((exists ff_h_mce_exact_ap. ff_h_mce_exact_ap + S (aa) = S ((S (i)) * ac)) /\ exists ff_q_mce_exact_ap. ab = ff_q_mce_exact_ap * S ((S (i)) * ac) + (aa))) /\ ((((exists ff_h_mce_exact_an. ff_h_mce_exact_an + S (dd) = S ((S (i)) * dc)) /\ exists ff_q_mce_exact_an. db = ff_q_mce_exact_an * S ((S (i)) * dc) + (dd))) /\ ((((exists ff_h_mce_exact_bp. ff_h_mce_exact_bp + S (ee) = S ((S (i)) * ec)) /\ exists ff_q_mce_exact_bp. eb = ff_q_mce_exact_bp * S ((S (i)) * ec) + (ee))) /\ ((((exists ff_h_mce_exact_bn. ff_h_mce_exact_bn + S (ff) = S ((S (i)) * fc)) /\ exists ff_q_mce_exact_bn. fb = ff_q_mce_exact_bn * S ((S (i)) * fc) + (ff))) /\ ((((exists ff_h_mce_exact_positive. ff_h_mce_exact_positive + S (pp) = S ((S (i)) * uc)) /\ exists ff_q_mce_exact_positive. ub = ff_q_mce_exact_positive * S ((S (i)) * uc) + (pp))) /\ ((((exists ff_h_mce_exact_negative. ff_h_mce_exact_negative + S (nn) = S ((S (i)) * vc)) /\ exists ff_q_mce_exact_negative. vb = ff_q_mce_exact_negative * S ((S (i)) * vc) + (nn))) /\ (((exists ff_even_mce_term_exact_term. i = 2 * ff_even_mce_term_exact_term) /\ (pp = (aa) * (ee) + (dd) * (ff) /\ nn = (aa) * (ff) + (dd) * (ee))) \/ ((exists ff_odd_mce_term_exact_term. i = 2 * ff_odd_mce_term_exact_term + 1) /\ (pp = (aa) * (ff) + (dd) * (ee) /\ nn = (aa) * (ee) + (dd) * (ff))))))))))
  30. 0030specialize hprefix i
  31. 0031apply hprefix
  32. 0032exact hbound
  33. 0033cases hentry
  34. 0034cases hentry_witness
  35. 0035cases hentry_witness_witness
  36. 0036cases hentry_witness_witness_witness
  37. 0037cases hentry_witness_witness_witness_witness
  38. 0038cases hentry_witness_witness_witness_witness_witness
  39. 0039cases hentry_witness_witness_witness_witness_witness_witness
  40. 0040cases hentry_witness_witness_witness_witness_witness_witness_right
  41. 0041cases hentry_witness_witness_witness_witness_witness_witness_right_right
  42. 0042cases hentry_witness_witness_witness_witness_witness_witness_right_right_right
  43. 0043cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right
  44. 0044cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  45. 0045have hapa : x = ap
  46. 0046specialize beta_at_unique ab
  47. 0047specialize beta_at_unique ac
  48. 0048specialize beta_at_unique i
  49. 0049specialize beta_at_unique x
  50. 0050specialize beta_at_unique ap
  51. 0051apply beta_at_unique
  52. 0052exact hentry_witness_witness_witness_witness_witness_witness_left
  53. 0053exact hap
  54. 0054have hana : x1 = an
  55. 0055specialize beta_at_unique db
  56. 0056specialize beta_at_unique dc
  57. 0057specialize beta_at_unique i
  58. 0058specialize beta_at_unique x1
  59. 0059specialize beta_at_unique an
  60. 0060apply beta_at_unique
  61. 0061exact hentry_witness_witness_witness_witness_witness_witness_right_left
  62. 0062exact han
  63. 0063have hbpa : x2 = bp
  64. 0064specialize beta_at_unique eb
  65. 0065specialize beta_at_unique ec
  66. 0066specialize beta_at_unique i
  67. 0067specialize beta_at_unique x2
  68. 0068specialize beta_at_unique bp
  69. 0069apply beta_at_unique
  70. 0070exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
  71. 0071exact hbp
  72. 0072have hbna : x3 = bn
  73. 0073specialize beta_at_unique fb
  74. 0074specialize beta_at_unique fc
  75. 0075specialize beta_at_unique i
  76. 0076specialize beta_at_unique x3
  77. 0077specialize beta_at_unique bn
  78. 0078apply beta_at_unique
  79. 0079exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  80. 0080exact hbn
  81. 0081have hpa : x4 = p
  82. 0082specialize beta_at_unique ub
  83. 0083specialize beta_at_unique uc
  84. 0084specialize beta_at_unique i
  85. 0085specialize beta_at_unique x4
  86. 0086specialize beta_at_unique p
  87. 0087apply beta_at_unique
  88. 0088exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  89. 0089exact hp
  90. 0090have hna : x5 = n
  91. 0091specialize beta_at_unique vb
  92. 0092specialize beta_at_unique vc
  93. 0093specialize beta_at_unique i
  94. 0094specialize beta_at_unique x5
  95. 0095specialize beta_at_unique n
  96. 0096apply beta_at_unique
  97. 0097exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  98. 0098exact hn
  99. 0099rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  100. 0100rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  101. 0101rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  102. 0102rewrite hapa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  103. 0103rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  104. 0104rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  105. 0105rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  106. 0106rewrite hana at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  107. 0107rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  108. 0108rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  109. 0109rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  110. 0110rewrite hbpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  111. 0111rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  112. 0112rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  113. 0113rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  114. 0114rewrite hbna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  115. 0115rewrite hpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  116. 0116rewrite hpa at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  117. 0117rewrite hna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  118. 0118rewrite hna at hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
  119. 0119exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right