DL0075

integer_vector_add_transport_inputs

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

Integer-vector addition respects genuine signed-difference equality of both inputs, not merely recoding of equal natural components.

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.

Exact expanded first-order arithmetic statement

forall ab ac db dc eb ec fb fc pb pc nb nc qb qc mb mc rb rc sb sc l. (forall ics_index_add_transport_first ics_value0_add_transport_first ics_value1_add_transport_first ics_value2_add_transport_first ics_value3_add_transport_first. (exists ics_gap_add_transport_first_bound. ics_gap_add_transport_first_bound + S (ics_index_add_transport_first) = (l)) -> (((exists fs_h_ics_add_transport_first_at0. fs_h_ics_add_transport_first_at0 + S (ics_value0_add_transport_first) = S ((S (ics_index_add_transport_first)) * ac)) /\ exists fs_q_ics_add_transport_first_at0. ab = fs_q_ics_add_transport_first_at0 * S ((S (ics_index_add_transport_first)) * ac) + (ics_value0_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at1. fs_h_ics_add_transport_first_at1 + S (ics_value1_add_transport_first) = S ((S (ics_index_add_transport_first)) * dc)) /\ exists fs_q_ics_add_transport_first_at1. db = fs_q_ics_add_transport_first_at1 * S ((S (ics_index_add_transport_first)) * dc) + (ics_value1_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at2. fs_h_ics_add_transport_first_at2 + S (ics_value2_add_transport_first) = S ((S (ics_index_add_transport_first)) * pc)) /\ exists fs_q_ics_add_transport_first_at2. pb = fs_q_ics_add_transport_first_at2 * S ((S (ics_index_add_transport_first)) * pc) + (ics_value2_add_transport_first))) -> (((exists fs_h_ics_add_transport_first_at3. fs_h_ics_add_transport_first_at3 + S (ics_value3_add_transport_first) = S ((S (ics_index_add_transport_first)) * nc)) /\ exists fs_q_ics_add_transport_first_at3. nb = fs_q_ics_add_transport_first_at3 * S ((S (ics_index_add_transport_first)) * nc) + (ics_value3_add_transport_first))) -> ics_value0_add_transport_first + ics_value3_add_transport_first = ics_value2_add_transport_first + ics_value1_add_transport_first) -> (forall ics_index_add_transport_second ics_value0_add_transport_second ics_value1_add_transport_second ics_value2_add_transport_second ics_value3_add_transport_second. (exists ics_gap_add_transport_second_bound. ics_gap_add_transport_second_bound + S (ics_index_add_transport_second) = (l)) -> (((exists fs_h_ics_add_transport_second_at0. fs_h_ics_add_transport_second_at0 + S (ics_value0_add_transport_second) = S ((S (ics_index_add_transport_second)) * ec)) /\ exists fs_q_ics_add_transport_second_at0. eb = fs_q_ics_add_transport_second_at0 * S ((S (ics_index_add_transport_second)) * ec) + (ics_value0_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at1. fs_h_ics_add_transport_second_at1 + S (ics_value1_add_transport_second) = S ((S (ics_index_add_transport_second)) * fc)) /\ exists fs_q_ics_add_transport_second_at1. fb = fs_q_ics_add_transport_second_at1 * S ((S (ics_index_add_transport_second)) * fc) + (ics_value1_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at2. fs_h_ics_add_transport_second_at2 + S (ics_value2_add_transport_second) = S ((S (ics_index_add_transport_second)) * qc)) /\ exists fs_q_ics_add_transport_second_at2. qb = fs_q_ics_add_transport_second_at2 * S ((S (ics_index_add_transport_second)) * qc) + (ics_value2_add_transport_second))) -> (((exists fs_h_ics_add_transport_second_at3. fs_h_ics_add_transport_second_at3 + S (ics_value3_add_transport_second) = S ((S (ics_index_add_transport_second)) * mc)) /\ exists fs_q_ics_add_transport_second_at3. mb = fs_q_ics_add_transport_second_at3 * S ((S (ics_index_add_transport_second)) * mc) + (ics_value3_add_transport_second))) -> ics_value0_add_transport_second + ics_value3_add_transport_second = ics_value2_add_transport_second + ics_value1_add_transport_second) -> (forall ics_index_add_transport_source ics_value0_add_transport_source ics_value1_add_transport_source ics_value2_add_transport_source ics_value3_add_transport_source ics_value4_add_transport_source ics_value5_add_transport_source. (exists ics_gap_add_transport_source_bound. ics_gap_add_transport_source_bound + S (ics_index_add_transport_source) = (l)) -> (((exists fs_h_ics_add_transport_source_at0. fs_h_ics_add_transport_source_at0 + S (ics_value0_add_transport_source) = S ((S (ics_index_add_transport_source)) * ac)) /\ exists fs_q_ics_add_transport_source_at0. ab = fs_q_ics_add_transport_source_at0 * S ((S (ics_index_add_transport_source)) * ac) + (ics_value0_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at1. fs_h_ics_add_transport_source_at1 + S (ics_value1_add_transport_source) = S ((S (ics_index_add_transport_source)) * dc)) /\ exists fs_q_ics_add_transport_source_at1. db = fs_q_ics_add_transport_source_at1 * S ((S (ics_index_add_transport_source)) * dc) + (ics_value1_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at2. fs_h_ics_add_transport_source_at2 + S (ics_value2_add_transport_source) = S ((S (ics_index_add_transport_source)) * ec)) /\ exists fs_q_ics_add_transport_source_at2. eb = fs_q_ics_add_transport_source_at2 * S ((S (ics_index_add_transport_source)) * ec) + (ics_value2_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at3. fs_h_ics_add_transport_source_at3 + S (ics_value3_add_transport_source) = S ((S (ics_index_add_transport_source)) * fc)) /\ exists fs_q_ics_add_transport_source_at3. fb = fs_q_ics_add_transport_source_at3 * S ((S (ics_index_add_transport_source)) * fc) + (ics_value3_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at4. fs_h_ics_add_transport_source_at4 + S (ics_value4_add_transport_source) = S ((S (ics_index_add_transport_source)) * rc)) /\ exists fs_q_ics_add_transport_source_at4. rb = fs_q_ics_add_transport_source_at4 * S ((S (ics_index_add_transport_source)) * rc) + (ics_value4_add_transport_source))) -> (((exists fs_h_ics_add_transport_source_at5. fs_h_ics_add_transport_source_at5 + S (ics_value5_add_transport_source) = S ((S (ics_index_add_transport_source)) * sc)) /\ exists fs_q_ics_add_transport_source_at5. sb = fs_q_ics_add_transport_source_at5 * S ((S (ics_index_add_transport_source)) * sc) + (ics_value5_add_transport_source))) -> ics_value4_add_transport_source + (ics_value1_add_transport_source + ics_value3_add_transport_source) = (ics_value0_add_transport_source + ics_value2_add_transport_source) + ics_value5_add_transport_source) -> (forall ics_index_add_transport_result ics_value0_add_transport_result ics_value1_add_transport_result ics_value2_add_transport_result ics_value3_add_transport_result ics_value4_add_transport_result ics_value5_add_transport_result. (exists ics_gap_add_transport_result_bound. ics_gap_add_transport_result_bound + S (ics_index_add_transport_result) = (l)) -> (((exists fs_h_ics_add_transport_result_at0. fs_h_ics_add_transport_result_at0 + S (ics_value0_add_transport_result) = S ((S (ics_index_add_transport_result)) * pc)) /\ exists fs_q_ics_add_transport_result_at0. pb = fs_q_ics_add_transport_result_at0 * S ((S (ics_index_add_transport_result)) * pc) + (ics_value0_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at1. fs_h_ics_add_transport_result_at1 + S (ics_value1_add_transport_result) = S ((S (ics_index_add_transport_result)) * nc)) /\ exists fs_q_ics_add_transport_result_at1. nb = fs_q_ics_add_transport_result_at1 * S ((S (ics_index_add_transport_result)) * nc) + (ics_value1_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at2. fs_h_ics_add_transport_result_at2 + S (ics_value2_add_transport_result) = S ((S (ics_index_add_transport_result)) * qc)) /\ exists fs_q_ics_add_transport_result_at2. qb = fs_q_ics_add_transport_result_at2 * S ((S (ics_index_add_transport_result)) * qc) + (ics_value2_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at3. fs_h_ics_add_transport_result_at3 + S (ics_value3_add_transport_result) = S ((S (ics_index_add_transport_result)) * mc)) /\ exists fs_q_ics_add_transport_result_at3. mb = fs_q_ics_add_transport_result_at3 * S ((S (ics_index_add_transport_result)) * mc) + (ics_value3_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at4. fs_h_ics_add_transport_result_at4 + S (ics_value4_add_transport_result) = S ((S (ics_index_add_transport_result)) * rc)) /\ exists fs_q_ics_add_transport_result_at4. rb = fs_q_ics_add_transport_result_at4 * S ((S (ics_index_add_transport_result)) * rc) + (ics_value4_add_transport_result))) -> (((exists fs_h_ics_add_transport_result_at5. fs_h_ics_add_transport_result_at5 + S (ics_value5_add_transport_result) = S ((S (ics_index_add_transport_result)) * sc)) /\ exists fs_q_ics_add_transport_result_at5. sb = fs_q_ics_add_transport_result_at5 * S ((S (ics_index_add_transport_result)) * sc) + (ics_value5_add_transport_result))) -> ics_value4_add_transport_result + (ics_value1_add_transport_result + ics_value3_add_transport_result) = (ics_value0_add_transport_result + ics_value2_add_transport_result) + ics_value5_add_transport_result)

Constructive proof overview

Generated structural guide

Integer-vector addition respects genuine signed-difference equality of both inputs, not merely recoding of equal natural components.

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

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

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized DL006C integer_span_pair_equal_transitive DL006D integer_span_pair_add_congruence

Direct dependents

DL007B integer_matrix_vector_add_coefficients

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

115 script commands · 18 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.

Named ingredients (2)
integer span pair equal transitiveinteger span pair add congruence
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 pb
  10. L10
    intro pc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro nb
  2. L12
    intro nc
  3. L13
    intro qb
  4. L14
    intro qc
  5. L15
    intro mb
  6. L16
    intro mc
  7. L17
    intro rb
  8. L18
    intro rc
  9. L19
    intro sb
  10. L20
    intro sc
03Fix variables and assumptionsL21–30

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

  1. L21
    intro l
  2. L22
    intro hfirst
  3. L23
    intro hsecond
  4. L24
    intro hadd
  5. L25
    intro i
  6. L26
    intro a
  7. L27
    intro b
  8. L28
    intro c
  9. L29
    intro d
  10. L30
    intro e
04Fix variables and assumptionsL31–38

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

  1. L31
    intro f
  2. L32
    intro hi
  3. L33
    intro ha
  4. L34
    intro hb
  5. L35
    intro hc
  6. L36
    intro hd
  7. L37
    intro he
  8. L38
    intro hf
05Establish hraw0L39–43

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

  1. L39
    have hraw0 : exists value. (((exists fs_h_ics_add_transport_raw0. fs_h_ics_add_transport_raw0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_add_transport_raw0. ab = fs_q_ics_add_transport_raw0 * S ((S (i)) * ac) + (value)))
  2. L40
    specialize beta_at_exists (ab)
  3. L41
    specialize beta_at_exists (ac)
  4. L42
    specialize beta_at_exists (i)
  5. L43
    apply beta_at_exists
06Separate the logical casesL44–44

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

  1. L44
    cases hraw0
07Establish hraw1L45–49

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

  1. L45
    have hraw1 : exists value. (((exists fs_h_ics_add_transport_raw1. fs_h_ics_add_transport_raw1 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_add_transport_raw1. db = fs_q_ics_add_transport_raw1 * S ((S (i)) * dc) + (value)))
  2. L46
    specialize beta_at_exists (db)
  3. L47
    specialize beta_at_exists (dc)
  4. L48
    specialize beta_at_exists (i)
  5. L49
    apply beta_at_exists
08Separate the logical casesL50–50

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

  1. L50
    cases hraw1
09Establish hraw2L51–55

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

  1. L51
    have hraw2 : exists value. (((exists fs_h_ics_add_transport_raw2. fs_h_ics_add_transport_raw2 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_add_transport_raw2. eb = fs_q_ics_add_transport_raw2 * S ((S (i)) * ec) + (value)))
  2. L52
    specialize beta_at_exists (eb)
  3. L53
    specialize beta_at_exists (ec)
  4. L54
    specialize beta_at_exists (i)
  5. L55
    apply beta_at_exists
10Separate the logical casesL56–56

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

  1. L56
    cases hraw2
11Establish hraw3L57–61

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

  1. L57
    have hraw3 : exists value. (((exists fs_h_ics_add_transport_raw3. fs_h_ics_add_transport_raw3 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_add_transport_raw3. fb = fs_q_ics_add_transport_raw3 * S ((S (i)) * fc) + (value)))
  2. L58
    specialize beta_at_exists (fb)
  3. L59
    specialize beta_at_exists (fc)
  4. L60
    specialize beta_at_exists (i)
  5. L61
    apply beta_at_exists
12Separate the logical casesL62–62

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

  1. L62
    cases hraw3
13Use earlier factsL63–72

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

  1. L63
    specialize integer_span_pair_equal_transitive (e)
  2. L64
    specialize integer_span_pair_equal_transitive (f)
  3. L65
    specialize integer_span_pair_equal_transitive (x + x2)
  4. L66
    specialize integer_span_pair_equal_transitive (x1 + x3)
  5. L67
    specialize integer_span_pair_equal_transitive (a + c)
  6. L68
    specialize integer_span_pair_equal_transitive (b + d)
  7. L69
    apply integer_span_pair_equal_transitive
  8. L70
    specialize hadd (i)
  9. L71
    specialize hadd (x)
  10. L72
    specialize hadd (x1)
14Use earlier factsL73–82

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

  1. L73
    specialize hadd (x2)
  2. L74
    specialize hadd (x3)
  3. L75
    specialize hadd (e)
  4. L76
    specialize hadd (f)
  5. L77
    apply hadd
  6. L78
    exact hi
  7. L79
    exact hraw0_witness
  8. L80
    exact hraw1_witness
  9. L81
    exact hraw2_witness
  10. L82
    exact hraw3_witness
15Use earlier factsL83–92

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

  1. L83
    exact he
  2. L84
    exact hf
  3. L85
    specialize integer_span_pair_add_congruence (x)
  4. L86
    specialize integer_span_pair_add_congruence (x1)
  5. L87
    specialize integer_span_pair_add_congruence (x2)
  6. L88
    specialize integer_span_pair_add_congruence (x3)
  7. L89
    specialize integer_span_pair_add_congruence (a)
  8. L90
    specialize integer_span_pair_add_congruence (b)
  9. L91
    specialize integer_span_pair_add_congruence (c)
  10. L92
    specialize integer_span_pair_add_congruence (d)
16Use earlier factsL93–102

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

  1. L93
    apply integer_span_pair_add_congruence
  2. L94
    specialize hfirst (i)
  3. L95
    specialize hfirst (x)
  4. L96
    specialize hfirst (x1)
  5. L97
    specialize hfirst (a)
  6. L98
    specialize hfirst (b)
  7. L99
    apply hfirst
  8. L100
    exact hi
  9. L101
    exact hraw0_witness
  10. L102
    exact hraw1_witness
17Use earlier factsL103–112

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

  1. L103
    exact ha
  2. L104
    exact hb
  3. L105
    specialize hsecond (i)
  4. L106
    specialize hsecond (x2)
  5. L107
    specialize hsecond (x3)
  6. L108
    specialize hsecond (c)
  7. L109
    specialize hsecond (d)
  8. L110
    apply hsecond
  9. L111
    exact hi
  10. L112
    exact hraw2_witness
18Use earlier factsL113–115

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

  1. L113
    exact hraw3_witness
  2. L114
    exact hc
  3. L115
    exact hd

Library-wide reading audit

Original exact command ledger · 115 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 pb
  10. 0010intro pc
  11. 0011intro nb
  12. 0012intro nc
  13. 0013intro qb
  14. 0014intro qc
  15. 0015intro mb
  16. 0016intro mc
  17. 0017intro rb
  18. 0018intro rc
  19. 0019intro sb
  20. 0020intro sc
  21. 0021intro l
  22. 0022intro hfirst
  23. 0023intro hsecond
  24. 0024intro hadd
  25. 0025intro i
  26. 0026intro a
  27. 0027intro b
  28. 0028intro c
  29. 0029intro d
  30. 0030intro e
  31. 0031intro f
  32. 0032intro hi
  33. 0033intro ha
  34. 0034intro hb
  35. 0035intro hc
  36. 0036intro hd
  37. 0037intro he
  38. 0038intro hf
  39. 0039have hraw0 : exists value. (((exists fs_h_ics_add_transport_raw0. fs_h_ics_add_transport_raw0 + S (value) = S ((S (i)) * ac)) /\ exists fs_q_ics_add_transport_raw0. ab = fs_q_ics_add_transport_raw0 * S ((S (i)) * ac) + (value)))
  40. 0040specialize beta_at_exists (ab)
  41. 0041specialize beta_at_exists (ac)
  42. 0042specialize beta_at_exists (i)
  43. 0043apply beta_at_exists
  44. 0044cases hraw0
  45. 0045have hraw1 : exists value. (((exists fs_h_ics_add_transport_raw1. fs_h_ics_add_transport_raw1 + S (value) = S ((S (i)) * dc)) /\ exists fs_q_ics_add_transport_raw1. db = fs_q_ics_add_transport_raw1 * S ((S (i)) * dc) + (value)))
  46. 0046specialize beta_at_exists (db)
  47. 0047specialize beta_at_exists (dc)
  48. 0048specialize beta_at_exists (i)
  49. 0049apply beta_at_exists
  50. 0050cases hraw1
  51. 0051have hraw2 : exists value. (((exists fs_h_ics_add_transport_raw2. fs_h_ics_add_transport_raw2 + S (value) = S ((S (i)) * ec)) /\ exists fs_q_ics_add_transport_raw2. eb = fs_q_ics_add_transport_raw2 * S ((S (i)) * ec) + (value)))
  52. 0052specialize beta_at_exists (eb)
  53. 0053specialize beta_at_exists (ec)
  54. 0054specialize beta_at_exists (i)
  55. 0055apply beta_at_exists
  56. 0056cases hraw2
  57. 0057have hraw3 : exists value. (((exists fs_h_ics_add_transport_raw3. fs_h_ics_add_transport_raw3 + S (value) = S ((S (i)) * fc)) /\ exists fs_q_ics_add_transport_raw3. fb = fs_q_ics_add_transport_raw3 * S ((S (i)) * fc) + (value)))
  58. 0058specialize beta_at_exists (fb)
  59. 0059specialize beta_at_exists (fc)
  60. 0060specialize beta_at_exists (i)
  61. 0061apply beta_at_exists
  62. 0062cases hraw3
  63. 0063specialize integer_span_pair_equal_transitive (e)
  64. 0064specialize integer_span_pair_equal_transitive (f)
  65. 0065specialize integer_span_pair_equal_transitive (x + x2)
  66. 0066specialize integer_span_pair_equal_transitive (x1 + x3)
  67. 0067specialize integer_span_pair_equal_transitive (a + c)
  68. 0068specialize integer_span_pair_equal_transitive (b + d)
  69. 0069apply integer_span_pair_equal_transitive
  70. 0070specialize hadd (i)
  71. 0071specialize hadd (x)
  72. 0072specialize hadd (x1)
  73. 0073specialize hadd (x2)
  74. 0074specialize hadd (x3)
  75. 0075specialize hadd (e)
  76. 0076specialize hadd (f)
  77. 0077apply hadd
  78. 0078exact hi
  79. 0079exact hraw0_witness
  80. 0080exact hraw1_witness
  81. 0081exact hraw2_witness
  82. 0082exact hraw3_witness
  83. 0083exact he
  84. 0084exact hf
  85. 0085specialize integer_span_pair_add_congruence (x)
  86. 0086specialize integer_span_pair_add_congruence (x1)
  87. 0087specialize integer_span_pair_add_congruence (x2)
  88. 0088specialize integer_span_pair_add_congruence (x3)
  89. 0089specialize integer_span_pair_add_congruence (a)
  90. 0090specialize integer_span_pair_add_congruence (b)
  91. 0091specialize integer_span_pair_add_congruence (c)
  92. 0092specialize integer_span_pair_add_congruence (d)
  93. 0093apply integer_span_pair_add_congruence
  94. 0094specialize hfirst (i)
  95. 0095specialize hfirst (x)
  96. 0096specialize hfirst (x1)
  97. 0097specialize hfirst (a)
  98. 0098specialize hfirst (b)
  99. 0099apply hfirst
  100. 0100exact hi
  101. 0101exact hraw0_witness
  102. 0102exact hraw1_witness
  103. 0103exact ha
  104. 0104exact hb
  105. 0105specialize hsecond (i)
  106. 0106specialize hsecond (x2)
  107. 0107specialize hsecond (x3)
  108. 0108specialize hsecond (c)
  109. 0109specialize hsecond (d)
  110. 0110apply hsecond
  111. 0111exact hi
  112. 0112exact hraw2_witness
  113. 0113exact hraw3_witness
  114. 0114exact hc
  115. 0115exact hd