PX001E

prime_field_polynomial_add_left_pad_transport

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

Common actual leading-zero padding preserves the genuine aligned add coefficient operation, including empty prefixes.

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 expanded first-order arithmetic statement

forall p ab ac bb bc cb cc L t AB AC BB BC CB CC. (~((p) = 1) /\ forall pfa_factor_left_pad_operation_prime pfa_factor_right_pad_operation_prime. (p) = pfa_factor_left_pad_operation_prime * pfa_factor_right_pad_operation_prime -> pfa_factor_left_pad_operation_prime = 1 \/ pfa_factor_right_pad_operation_prime = 1) -> (forall pfp_index_pad_operation_old. (exists pfa_gap_pad_operation_oldindex. pfa_gap_pad_operation_oldindex + S (pfp_index_pad_operation_old) = (L)) -> exists pfp_left_pad_operation_old pfp_right_pad_operation_old pfp_value_pad_operation_old. ((((exists ff_h_pfp_pad_operation_oldleft. ff_h_pfp_pad_operation_oldleft + S (pfp_left_pad_operation_old) = S ((S (pfp_index_pad_operation_old)) * ac)) /\ exists ff_q_pfp_pad_operation_oldleft. ab = ff_q_pfp_pad_operation_oldleft * S ((S (pfp_index_pad_operation_old)) * ac) + (pfp_left_pad_operation_old))) /\ (((((exists ff_h_pfp_pad_operation_oldright. ff_h_pfp_pad_operation_oldright + S (pfp_right_pad_operation_old) = S ((S (pfp_index_pad_operation_old)) * bc)) /\ exists ff_q_pfp_pad_operation_oldright. bb = ff_q_pfp_pad_operation_oldright * S ((S (pfp_index_pad_operation_old)) * bc) + (pfp_right_pad_operation_old))) /\ (((((exists ff_h_pfp_pad_operation_oldtarget. ff_h_pfp_pad_operation_oldtarget + S (pfp_value_pad_operation_old) = S ((S (pfp_index_pad_operation_old)) * cc)) /\ exists ff_q_pfp_pad_operation_oldtarget. cb = ff_q_pfp_pad_operation_oldtarget * S ((S (pfp_index_pad_operation_old)) * cc) + (pfp_value_pad_operation_old))) /\ ((((exists pfa_gap_pad_operation_oldoperationleft. pfa_gap_pad_operation_oldoperationleft + S (pfp_left_pad_operation_old) = (p)) /\ (((exists pfa_gap_pad_operation_oldoperationright. pfa_gap_pad_operation_oldoperationright + S (pfp_right_pad_operation_old) = (p)) /\ ((((exists pfa_gap_pad_operation_oldoperationresultbound. pfa_gap_pad_operation_oldoperationresultbound + S (pfp_value_pad_operation_old) = (p)) /\ ((exists pfa_offset_left_pad_operation_oldoperationresultcongruence pfa_offset_right_pad_operation_oldoperationresultcongruence. ((pfp_left_pad_operation_old) + (pfp_right_pad_operation_old)) + (p) * pfa_offset_left_pad_operation_oldoperationresultcongruence = (pfp_value_pad_operation_old) + (p) * pfa_offset_right_pad_operation_oldoperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_pad_operation_abzeros. (exists pfa_gap_pad_operation_abzerosindex. pfa_gap_pad_operation_abzerosindex + S (pfp_repeat_index_pad_operation_abzeros) = (t)) -> (((exists ff_h_pfp_pad_operation_abzerosentry. ff_h_pfp_pad_operation_abzerosentry + S (0) = S ((S (pfp_repeat_index_pad_operation_abzeros)) * AC)) /\ exists ff_q_pfp_pad_operation_abzerosentry. AB = ff_q_pfp_pad_operation_abzerosentry * S ((S (pfp_repeat_index_pad_operation_abzeros)) * AC) + (0)))) /\ ((forall pfrep_index_pad_operation_ab pfrep_value_pad_operation_ab. (exists pfa_gap_pad_operation_abbound. pfa_gap_pad_operation_abbound + S (pfrep_index_pad_operation_ab) = (L)) -> (((exists ff_h_pfp_pad_operation_abinput. ff_h_pfp_pad_operation_abinput + S (pfrep_value_pad_operation_ab) = S ((S (pfrep_index_pad_operation_ab)) * ac)) /\ exists ff_q_pfp_pad_operation_abinput. ab = ff_q_pfp_pad_operation_abinput * S ((S (pfrep_index_pad_operation_ab)) * ac) + (pfrep_value_pad_operation_ab))) -> (((exists ff_h_pfp_pad_operation_aboutput. ff_h_pfp_pad_operation_aboutput + S (pfrep_value_pad_operation_ab) = S ((S ((t)+pfrep_index_pad_operation_ab)) * AC)) /\ exists ff_q_pfp_pad_operation_aboutput. AB = ff_q_pfp_pad_operation_aboutput * S ((S ((t)+pfrep_index_pad_operation_ab)) * AC) + (pfrep_value_pad_operation_ab))))))) -> (((forall pfp_repeat_index_pad_operation_bbzeros. (exists pfa_gap_pad_operation_bbzerosindex. pfa_gap_pad_operation_bbzerosindex + S (pfp_repeat_index_pad_operation_bbzeros) = (t)) -> (((exists ff_h_pfp_pad_operation_bbzerosentry. ff_h_pfp_pad_operation_bbzerosentry + S (0) = S ((S (pfp_repeat_index_pad_operation_bbzeros)) * BC)) /\ exists ff_q_pfp_pad_operation_bbzerosentry. BB = ff_q_pfp_pad_operation_bbzerosentry * S ((S (pfp_repeat_index_pad_operation_bbzeros)) * BC) + (0)))) /\ ((forall pfrep_index_pad_operation_bb pfrep_value_pad_operation_bb. (exists pfa_gap_pad_operation_bbbound. pfa_gap_pad_operation_bbbound + S (pfrep_index_pad_operation_bb) = (L)) -> (((exists ff_h_pfp_pad_operation_bbinput. ff_h_pfp_pad_operation_bbinput + S (pfrep_value_pad_operation_bb) = S ((S (pfrep_index_pad_operation_bb)) * bc)) /\ exists ff_q_pfp_pad_operation_bbinput. bb = ff_q_pfp_pad_operation_bbinput * S ((S (pfrep_index_pad_operation_bb)) * bc) + (pfrep_value_pad_operation_bb))) -> (((exists ff_h_pfp_pad_operation_bboutput. ff_h_pfp_pad_operation_bboutput + S (pfrep_value_pad_operation_bb) = S ((S ((t)+pfrep_index_pad_operation_bb)) * BC)) /\ exists ff_q_pfp_pad_operation_bboutput. BB = ff_q_pfp_pad_operation_bboutput * S ((S ((t)+pfrep_index_pad_operation_bb)) * BC) + (pfrep_value_pad_operation_bb))))))) -> (((forall pfp_repeat_index_pad_operation_cbzeros. (exists pfa_gap_pad_operation_cbzerosindex. pfa_gap_pad_operation_cbzerosindex + S (pfp_repeat_index_pad_operation_cbzeros) = (t)) -> (((exists ff_h_pfp_pad_operation_cbzerosentry. ff_h_pfp_pad_operation_cbzerosentry + S (0) = S ((S (pfp_repeat_index_pad_operation_cbzeros)) * CC)) /\ exists ff_q_pfp_pad_operation_cbzerosentry. CB = ff_q_pfp_pad_operation_cbzerosentry * S ((S (pfp_repeat_index_pad_operation_cbzeros)) * CC) + (0)))) /\ ((forall pfrep_index_pad_operation_cb pfrep_value_pad_operation_cb. (exists pfa_gap_pad_operation_cbbound. pfa_gap_pad_operation_cbbound + S (pfrep_index_pad_operation_cb) = (L)) -> (((exists ff_h_pfp_pad_operation_cbinput. ff_h_pfp_pad_operation_cbinput + S (pfrep_value_pad_operation_cb) = S ((S (pfrep_index_pad_operation_cb)) * cc)) /\ exists ff_q_pfp_pad_operation_cbinput. cb = ff_q_pfp_pad_operation_cbinput * S ((S (pfrep_index_pad_operation_cb)) * cc) + (pfrep_value_pad_operation_cb))) -> (((exists ff_h_pfp_pad_operation_cboutput. ff_h_pfp_pad_operation_cboutput + S (pfrep_value_pad_operation_cb) = S ((S ((t)+pfrep_index_pad_operation_cb)) * CC)) /\ exists ff_q_pfp_pad_operation_cboutput. CB = ff_q_pfp_pad_operation_cboutput * S ((S ((t)+pfrep_index_pad_operation_cb)) * CC) + (pfrep_value_pad_operation_cb))))))) -> (forall pfp_index_pad_operation_new. (exists pfa_gap_pad_operation_newindex. pfa_gap_pad_operation_newindex + S (pfp_index_pad_operation_new) = (t+L)) -> exists pfp_left_pad_operation_new pfp_right_pad_operation_new pfp_value_pad_operation_new. ((((exists ff_h_pfp_pad_operation_newleft. ff_h_pfp_pad_operation_newleft + S (pfp_left_pad_operation_new) = S ((S (pfp_index_pad_operation_new)) * AC)) /\ exists ff_q_pfp_pad_operation_newleft. AB = ff_q_pfp_pad_operation_newleft * S ((S (pfp_index_pad_operation_new)) * AC) + (pfp_left_pad_operation_new))) /\ (((((exists ff_h_pfp_pad_operation_newright. ff_h_pfp_pad_operation_newright + S (pfp_right_pad_operation_new) = S ((S (pfp_index_pad_operation_new)) * BC)) /\ exists ff_q_pfp_pad_operation_newright. BB = ff_q_pfp_pad_operation_newright * S ((S (pfp_index_pad_operation_new)) * BC) + (pfp_right_pad_operation_new))) /\ (((((exists ff_h_pfp_pad_operation_newtarget. ff_h_pfp_pad_operation_newtarget + S (pfp_value_pad_operation_new) = S ((S (pfp_index_pad_operation_new)) * CC)) /\ exists ff_q_pfp_pad_operation_newtarget. CB = ff_q_pfp_pad_operation_newtarget * S ((S (pfp_index_pad_operation_new)) * CC) + (pfp_value_pad_operation_new))) /\ ((((exists pfa_gap_pad_operation_newoperationleft. pfa_gap_pad_operation_newoperationleft + S (pfp_left_pad_operation_new) = (p)) /\ (((exists pfa_gap_pad_operation_newoperationright. pfa_gap_pad_operation_newoperationright + S (pfp_right_pad_operation_new) = (p)) /\ ((((exists pfa_gap_pad_operation_newoperationresultbound. pfa_gap_pad_operation_newoperationresultbound + S (pfp_value_pad_operation_new) = (p)) /\ ((exists pfa_offset_left_pad_operation_newoperationresultcongruence pfa_offset_right_pad_operation_newoperationresultcongruence. ((pfp_left_pad_operation_new) + (pfp_right_pad_operation_new)) + (p) * pfa_offset_left_pad_operation_newoperationresultcongruence = (pfp_value_pad_operation_new) + (p) * pfa_offset_right_pad_operation_newoperationresultcongruence))))))))))))))))

Constructive proof overview

Generated structural guide

Common actual leading-zero padding preserves the genuine aligned add coefficient operation, including empty prefixes.

The unchanged tactic script uses 3 declared prerequisites and contains 94 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PX000A prime_field_polynomial_left_pad_index_cases prime_field_add_zero_right Alpha theorem; checked-use authorized prime_field_zero_below_prime Alpha theorem; checked-use authorized

Direct dependents

PX0073 prime_field_polynomial_add_left_pad_output

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

94 script commands · 26 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
prime field polynomial left pad index cases

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 p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro L
  9. L9
    intro t
  10. L10
    intro AB
02Fix variables and assumptionsL11–20

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

  1. L11
    intro AC
  2. L12
    intro BB
  3. L13
    intro BC
  4. L14
    intro CB
  5. L15
    intro CC
  6. L16
    intro hp
  7. L17
    intro hop
  8. L18
    intro h0
  9. L19
    intro h1
  10. L20
    intro h2
03Separate the logical casesL21–23

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

  1. L21
    cases h0
  2. L22
    cases h1
  3. L23
    cases h2
04Fix variables and assumptionsL24–25

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

  1. L24
    intro i
  2. L25
    intro hi
05Establish hcL26–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad index cases.

  1. L26
    have hc : (exists pfa_gap_pad_operation_zero. pfa_gap_pad_operation_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_pad_operation_source. pfa_gap_pad_operation_source + S (j) = (L)) /\ ((i=t+j))))
  2. L27
    specialize prime_field_polynomial_left_pad_index_cases (t)
  3. L28
    specialize prime_field_polynomial_left_pad_index_cases (L)
  4. L29
    specialize prime_field_polynomial_left_pad_index_cases (i)
  5. L30
    apply prime_field_polynomial_left_pad_index_cases
  6. L31
    exact hi
06Separate the logical casesL32–32

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

  1. L32
    cases hc
07Construct an explicit witnessL33–35

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

  1. L33
    exists 0
  2. L34
    exists 0
  3. L35
    exists 0
08Separate the logical casesL36–36

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

  1. L36
    split
09Use earlier factsL37–39

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

  1. L37
    specialize h0_left (i)
  2. L38
    apply h0_left
  3. L39
    exact hc_left
10Separate the logical casesL40–40

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

  1. L40
    split
11Use earlier factsL41–43

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

  1. L41
    specialize h1_left (i)
  2. L42
    apply h1_left
  3. L43
    exact hc_left
12Separate the logical casesL44–44

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

  1. L44
    split
13Use earlier factsL45–54

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

  1. L45
    specialize h2_left (i)
  2. L46
    apply h2_left
  3. L47
    exact hc_left
  4. L48
    specialize prime_field_add_zero_right (p)
  5. L49
    specialize prime_field_add_zero_right (0)
  6. L50
    apply prime_field_add_zero_right
  7. L51
    exact hp
  8. L52
    specialize prime_field_zero_below_prime (p)
  9. L53
    apply prime_field_zero_below_prime
  10. L54
    exact hp
14Separate the logical casesL55–56

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

  1. L55
    cases hc_right
  2. L56
    cases hc_right_witness
15Establish hvL57–60

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

  1. L57
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,x,a) ∧ (BetaAt(bb,bc,x,b) ∧ (BetaAt(cb,cc,x,r) ∧ FpAdd(p,a,b,r)))Definitions: FpAddBetaAt
  2. L58
    specialize hop (x)
  3. L59
    apply hop
  4. L60
    exact hc_right_witness_left
16Separate the logical casesL61–66

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

  1. L61
    cases hv
  2. L62
    cases hv_witness
  3. L63
    cases hv_witness_witness
  4. L64
    cases hv_witness_witness_witness
  5. L65
    cases hv_witness_witness_witness_right
  6. L66
    cases hv_witness_witness_witness_right_right
17Construct an explicit witnessL67–69

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

  1. L67
    exists x1
  2. L68
    exists x2
  3. L69
    exists x3
18Separate the logical casesL70–70

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

  1. L70
    split
19Calculate and transport equalitiesL71–72

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

  1. L71
    rewrite hc_right_witness_right
  2. L72
    rewrite hc_right_witness_right
20Use earlier factsL73–77

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

  1. L73
    specialize h0_right (x)
  2. L74
    specialize h0_right (x1)
  3. L75
    apply h0_right
  4. L76
    exact hc_right_witness_left
  5. L77
    exact hv_witness_witness_witness_left
21Separate the logical casesL78–78

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

  1. L78
    split
22Calculate and transport equalitiesL79–80

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

  1. L79
    rewrite hc_right_witness_right
  2. L80
    rewrite hc_right_witness_right
23Use earlier factsL81–85

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

  1. L81
    specialize h1_right (x)
  2. L82
    specialize h1_right (x2)
  3. L83
    apply h1_right
  4. L84
    exact hc_right_witness_left
  5. L85
    exact hv_witness_witness_witness_right_left
24Separate the logical casesL86–86

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

  1. L86
    split
25Calculate and transport equalitiesL87–88

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

  1. L87
    rewrite hc_right_witness_right
  2. L88
    rewrite hc_right_witness_right
26Use earlier factsL89–94

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

  1. L89
    specialize h2_right (x)
  2. L90
    specialize h2_right (x3)
  3. L91
    apply h2_right
  4. L92
    exact hc_right_witness_left
  5. L93
    exact hv_witness_witness_witness_right_right_left
  6. L94
    exact hv_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 94 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro L
  9. 0009intro t
  10. 0010intro AB
  11. 0011intro AC
  12. 0012intro BB
  13. 0013intro BC
  14. 0014intro CB
  15. 0015intro CC
  16. 0016intro hp
  17. 0017intro hop
  18. 0018intro h0
  19. 0019intro h1
  20. 0020intro h2
  21. 0021cases h0
  22. 0022cases h1
  23. 0023cases h2
  24. 0024intro i
  25. 0025intro hi
  26. 0026have hc : (exists pfa_gap_pad_operation_zero. pfa_gap_pad_operation_zero + S (i) = (t)) \/ exists j. (((exists pfa_gap_pad_operation_source. pfa_gap_pad_operation_source + S (j) = (L)) /\ ((i=t+j))))
  27. 0027specialize prime_field_polynomial_left_pad_index_cases (t)
  28. 0028specialize prime_field_polynomial_left_pad_index_cases (L)
  29. 0029specialize prime_field_polynomial_left_pad_index_cases (i)
  30. 0030apply prime_field_polynomial_left_pad_index_cases
  31. 0031exact hi
  32. 0032cases hc
  33. 0033exists 0
  34. 0034exists 0
  35. 0035exists 0
  36. 0036split
  37. 0037specialize h0_left (i)
  38. 0038apply h0_left
  39. 0039exact hc_left
  40. 0040split
  41. 0041specialize h1_left (i)
  42. 0042apply h1_left
  43. 0043exact hc_left
  44. 0044split
  45. 0045specialize h2_left (i)
  46. 0046apply h2_left
  47. 0047exact hc_left
  48. 0048specialize prime_field_add_zero_right (p)
  49. 0049specialize prime_field_add_zero_right (0)
  50. 0050apply prime_field_add_zero_right
  51. 0051exact hp
  52. 0052specialize prime_field_zero_below_prime (p)
  53. 0053apply prime_field_zero_below_prime
  54. 0054exact hp
  55. 0055cases hc_right
  56. 0056cases hc_right_witness
  57. 0057have hv : exists a b r. (((((exists ff_h_pfp_pad_operation_a. ff_h_pfp_pad_operation_a + S (a) = S ((S (x)) * ac)) /\ exists ff_q_pfp_pad_operation_a. ab = ff_q_pfp_pad_operation_a * S ((S (x)) * ac) + (a))) /\ (((((exists ff_h_pfp_pad_operation_b. ff_h_pfp_pad_operation_b + S (b) = S ((S (x)) * bc)) /\ exists ff_q_pfp_pad_operation_b. bb = ff_q_pfp_pad_operation_b * S ((S (x)) * bc) + (b))) /\ (((((exists ff_h_pfp_pad_operation_r. ff_h_pfp_pad_operation_r + S (r) = S ((S (x)) * cc)) /\ exists ff_q_pfp_pad_operation_r. cb = ff_q_pfp_pad_operation_r * S ((S (x)) * cc) + (r))) /\ ((((exists pfa_gap_pad_operation_pointleft. pfa_gap_pad_operation_pointleft + S (a) = (p)) /\ (((exists pfa_gap_pad_operation_pointright. pfa_gap_pad_operation_pointright + S (b) = (p)) /\ ((((exists pfa_gap_pad_operation_pointresultbound. pfa_gap_pad_operation_pointresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_pad_operation_pointresultcongruence pfa_offset_right_pad_operation_pointresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_pad_operation_pointresultcongruence = (r) + (p) * pfa_offset_right_pad_operation_pointresultcongruence))))))))))))))))
  58. 0058specialize hop (x)
  59. 0059apply hop
  60. 0060exact hc_right_witness_left
  61. 0061cases hv
  62. 0062cases hv_witness
  63. 0063cases hv_witness_witness
  64. 0064cases hv_witness_witness_witness
  65. 0065cases hv_witness_witness_witness_right
  66. 0066cases hv_witness_witness_witness_right_right
  67. 0067exists x1
  68. 0068exists x2
  69. 0069exists x3
  70. 0070split
  71. 0071rewrite hc_right_witness_right
  72. 0072rewrite hc_right_witness_right
  73. 0073specialize h0_right (x)
  74. 0074specialize h0_right (x1)
  75. 0075apply h0_right
  76. 0076exact hc_right_witness_left
  77. 0077exact hv_witness_witness_witness_left
  78. 0078split
  79. 0079rewrite hc_right_witness_right
  80. 0080rewrite hc_right_witness_right
  81. 0081specialize h1_right (x)
  82. 0082specialize h1_right (x2)
  83. 0083apply h1_right
  84. 0084exact hc_right_witness_left
  85. 0085exact hv_witness_witness_witness_right_left
  86. 0086split
  87. 0087rewrite hc_right_witness_right
  88. 0088rewrite hc_right_witness_right
  89. 0089specialize h2_right (x)
  90. 0090specialize h2_right (x3)
  91. 0091apply h2_right
  92. 0092exact hc_right_witness_left
  93. 0093exact hv_witness_witness_witness_right_right_left
  94. 0094exact hv_witness_witness_witness_right_right_right