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 .
This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.
Exact theorem in conservative defined notation
∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ qb. ∀ qc. ∀ rb. ∀ rc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ wb. ∀ wc. ∀ zb. ∀ zc. ∀ l. (∀ x. ∀ y. Lt(x,l) → BetaAt(pb,pc,x,y) → BetaAt(qb,qc,x,y) ) → (∀ x. ∀ y. Lt(x,l) → BetaAt(nb,nc,x,y) → BetaAt(rb,rc,x,y) ) → (∀ x. ∀ y. Lt(x,l) → BetaAt(eb,ec,x,y) → BetaAt(ub,uc,x,y) ) → (∀ x. ∀ y. Lt(x,l) → BetaAt(fb,fc,x,y) → BetaAt(vb,vc,x,y) ) → SignedAlternatingProductPrefix(pb,pc,nb,nc,eb,ec,fb,fc,wb,wc,zb,zc,l) → SignedAlternatingProductPrefix(qb,qc,rb,rc,ub,uc,vb,vc,wb,wc,zb,zc,l) Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n) · 1 SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l) · 2 Lt(a,b) · 4 BetaAt(b,c,i,x) · 14 Actual proof prerequisites none
Original expanded first-order statement
forall pb pc nb nc eb ec fb fc qb qc rb rc ub uc vb vc wb wc zb zc l. (forall mdr_i_fold_input_0 mdr_a_fold_input_0. (exists mdr_gap_fold_input_0b. mdr_gap_fold_input_0b + S (mdr_i_fold_input_0) = (l)) -> (((exists ff_h_mdr_fold_input_0o. ff_h_mdr_fold_input_0o + S (mdr_a_fold_input_0) = S ((S (mdr_i_fold_input_0)) * pc)) /\ exists ff_q_mdr_fold_input_0o. pb = ff_q_mdr_fold_input_0o * S ((S (mdr_i_fold_input_0)) * pc) + (mdr_a_fold_input_0))) -> (((exists ff_h_mdr_fold_input_0n. ff_h_mdr_fold_input_0n + S (mdr_a_fold_input_0) = S ((S (mdr_i_fold_input_0)) * qc)) /\ exists ff_q_mdr_fold_input_0n. qb = ff_q_mdr_fold_input_0n * S ((S (mdr_i_fold_input_0)) * qc) + (mdr_a_fold_input_0)))) -> (forall mdr_i_fold_input_1 mdr_a_fold_input_1. (exists mdr_gap_fold_input_1b. mdr_gap_fold_input_1b + S (mdr_i_fold_input_1) = (l)) -> (((exists ff_h_mdr_fold_input_1o. ff_h_mdr_fold_input_1o + S (mdr_a_fold_input_1) = S ((S (mdr_i_fold_input_1)) * nc)) /\ exists ff_q_mdr_fold_input_1o. nb = ff_q_mdr_fold_input_1o * S ((S (mdr_i_fold_input_1)) * nc) + (mdr_a_fold_input_1))) -> (((exists ff_h_mdr_fold_input_1n. ff_h_mdr_fold_input_1n + S (mdr_a_fold_input_1) = S ((S (mdr_i_fold_input_1)) * rc)) /\ exists ff_q_mdr_fold_input_1n. rb = ff_q_mdr_fold_input_1n * S ((S (mdr_i_fold_input_1)) * rc) + (mdr_a_fold_input_1)))) -> (forall mdr_i_fold_input_2 mdr_a_fold_input_2. (exists mdr_gap_fold_input_2b. mdr_gap_fold_input_2b + S (mdr_i_fold_input_2) = (l)) -> (((exists ff_h_mdr_fold_input_2o. ff_h_mdr_fold_input_2o + S (mdr_a_fold_input_2) = S ((S (mdr_i_fold_input_2)) * ec)) /\ exists ff_q_mdr_fold_input_2o. eb = ff_q_mdr_fold_input_2o * S ((S (mdr_i_fold_input_2)) * ec) + (mdr_a_fold_input_2))) -> (((exists ff_h_mdr_fold_input_2n. ff_h_mdr_fold_input_2n + S (mdr_a_fold_input_2) = S ((S (mdr_i_fold_input_2)) * uc)) /\ exists ff_q_mdr_fold_input_2n. ub = ff_q_mdr_fold_input_2n * S ((S (mdr_i_fold_input_2)) * uc) + (mdr_a_fold_input_2)))) -> (forall mdr_i_fold_input_3 mdr_a_fold_input_3. (exists mdr_gap_fold_input_3b. mdr_gap_fold_input_3b + S (mdr_i_fold_input_3) = (l)) -> (((exists ff_h_mdr_fold_input_3o. ff_h_mdr_fold_input_3o + S (mdr_a_fold_input_3) = S ((S (mdr_i_fold_input_3)) * fc)) /\ exists ff_q_mdr_fold_input_3o. fb = ff_q_mdr_fold_input_3o * S ((S (mdr_i_fold_input_3)) * fc) + (mdr_a_fold_input_3))) -> (((exists ff_h_mdr_fold_input_3n. ff_h_mdr_fold_input_3n + S (mdr_a_fold_input_3) = S ((S (mdr_i_fold_input_3)) * vc)) /\ exists ff_q_mdr_fold_input_3n. vb = ff_q_mdr_fold_input_3n * S ((S (mdr_i_fold_input_3)) * vc) + (mdr_a_fold_input_3)))) -> (forall ff_index_mce_alternating_mdre_alt_source. (exists ff_gap_mce_mdre_alt_source_index. ff_gap_mce_mdre_alt_source_index + S (ff_index_mce_alternating_mdre_alt_source) = (l)) -> exists ff_ap_mce_alternating_mdre_alt_source ff_an_mce_alternating_mdre_alt_source ff_bp_mce_alternating_mdre_alt_source ff_bn_mce_alternating_mdre_alt_source ff_p_mce_alternating_mdre_alt_source ff_n_mce_alternating_mdre_alt_source. ((((exists ff_h_mce_mdre_alt_source_ap. ff_h_mce_mdre_alt_source_ap + S (ff_ap_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * pc)) /\ exists ff_q_mce_mdre_alt_source_ap. pb = ff_q_mce_mdre_alt_source_ap * S ((S (ff_index_mce_alternating_mdre_alt_source)) * pc) + (ff_ap_mce_alternating_mdre_alt_source))) /\ ((((exists ff_h_mce_mdre_alt_source_an. ff_h_mce_mdre_alt_source_an + S (ff_an_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * nc)) /\ exists ff_q_mce_mdre_alt_source_an. nb = ff_q_mce_mdre_alt_source_an * S ((S (ff_index_mce_alternating_mdre_alt_source)) * nc) + (ff_an_mce_alternating_mdre_alt_source))) /\ ((((exists ff_h_mce_mdre_alt_source_bp. ff_h_mce_mdre_alt_source_bp + S (ff_bp_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * ec)) /\ exists ff_q_mce_mdre_alt_source_bp. eb = ff_q_mce_mdre_alt_source_bp * S ((S (ff_index_mce_alternating_mdre_alt_source)) * ec) + (ff_bp_mce_alternating_mdre_alt_source))) /\ ((((exists ff_h_mce_mdre_alt_source_bn. ff_h_mce_mdre_alt_source_bn + S (ff_bn_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * fc)) /\ exists ff_q_mce_mdre_alt_source_bn. fb = ff_q_mce_mdre_alt_source_bn * S ((S (ff_index_mce_alternating_mdre_alt_source)) * fc) + (ff_bn_mce_alternating_mdre_alt_source))) /\ ((((exists ff_h_mce_mdre_alt_source_positive. ff_h_mce_mdre_alt_source_positive + S (ff_p_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * wc)) /\ exists ff_q_mce_mdre_alt_source_positive. wb = ff_q_mce_mdre_alt_source_positive * S ((S (ff_index_mce_alternating_mdre_alt_source)) * wc) + (ff_p_mce_alternating_mdre_alt_source))) /\ ((((exists ff_h_mce_mdre_alt_source_negative. ff_h_mce_mdre_alt_source_negative + S (ff_n_mce_alternating_mdre_alt_source) = S ((S (ff_index_mce_alternating_mdre_alt_source)) * zc)) /\ exists ff_q_mce_mdre_alt_source_negative. zb = ff_q_mce_mdre_alt_source_negative * S ((S (ff_index_mce_alternating_mdre_alt_source)) * zc) + (ff_n_mce_alternating_mdre_alt_source))) /\ (((exists ff_even_mce_term_mdre_alt_source_term. ff_index_mce_alternating_mdre_alt_source = 2 * ff_even_mce_term_mdre_alt_source_term) /\ (ff_p_mce_alternating_mdre_alt_source = (ff_ap_mce_alternating_mdre_alt_source) * (ff_bp_mce_alternating_mdre_alt_source) + (ff_an_mce_alternating_mdre_alt_source) * (ff_bn_mce_alternating_mdre_alt_source) /\ ff_n_mce_alternating_mdre_alt_source = (ff_ap_mce_alternating_mdre_alt_source) * (ff_bn_mce_alternating_mdre_alt_source) + (ff_an_mce_alternating_mdre_alt_source) * (ff_bp_mce_alternating_mdre_alt_source))) \/ ((exists ff_odd_mce_term_mdre_alt_source_term. ff_index_mce_alternating_mdre_alt_source = 2 * ff_odd_mce_term_mdre_alt_source_term + 1) /\ (ff_p_mce_alternating_mdre_alt_source = (ff_ap_mce_alternating_mdre_alt_source) * (ff_bn_mce_alternating_mdre_alt_source) + (ff_an_mce_alternating_mdre_alt_source) * (ff_bp_mce_alternating_mdre_alt_source) /\ ff_n_mce_alternating_mdre_alt_source = (ff_ap_mce_alternating_mdre_alt_source) * (ff_bp_mce_alternating_mdre_alt_source) + (ff_an_mce_alternating_mdre_alt_source) * (ff_bn_mce_alternating_mdre_alt_source))))))))))) -> (forall ff_index_mce_alternating_mdre_alt_target. (exists ff_gap_mce_mdre_alt_target_index. ff_gap_mce_mdre_alt_target_index + S (ff_index_mce_alternating_mdre_alt_target) = (l)) -> exists ff_ap_mce_alternating_mdre_alt_target ff_an_mce_alternating_mdre_alt_target ff_bp_mce_alternating_mdre_alt_target ff_bn_mce_alternating_mdre_alt_target ff_p_mce_alternating_mdre_alt_target ff_n_mce_alternating_mdre_alt_target. ((((exists ff_h_mce_mdre_alt_target_ap. ff_h_mce_mdre_alt_target_ap + S (ff_ap_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * qc)) /\ exists ff_q_mce_mdre_alt_target_ap. qb = ff_q_mce_mdre_alt_target_ap * S ((S (ff_index_mce_alternating_mdre_alt_target)) * qc) + (ff_ap_mce_alternating_mdre_alt_target))) /\ ((((exists ff_h_mce_mdre_alt_target_an. ff_h_mce_mdre_alt_target_an + S (ff_an_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * rc)) /\ exists ff_q_mce_mdre_alt_target_an. rb = ff_q_mce_mdre_alt_target_an * S ((S (ff_index_mce_alternating_mdre_alt_target)) * rc) + (ff_an_mce_alternating_mdre_alt_target))) /\ ((((exists ff_h_mce_mdre_alt_target_bp. ff_h_mce_mdre_alt_target_bp + S (ff_bp_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * uc)) /\ exists ff_q_mce_mdre_alt_target_bp. ub = ff_q_mce_mdre_alt_target_bp * S ((S (ff_index_mce_alternating_mdre_alt_target)) * uc) + (ff_bp_mce_alternating_mdre_alt_target))) /\ ((((exists ff_h_mce_mdre_alt_target_bn. ff_h_mce_mdre_alt_target_bn + S (ff_bn_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * vc)) /\ exists ff_q_mce_mdre_alt_target_bn. vb = ff_q_mce_mdre_alt_target_bn * S ((S (ff_index_mce_alternating_mdre_alt_target)) * vc) + (ff_bn_mce_alternating_mdre_alt_target))) /\ ((((exists ff_h_mce_mdre_alt_target_positive. ff_h_mce_mdre_alt_target_positive + S (ff_p_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * wc)) /\ exists ff_q_mce_mdre_alt_target_positive. wb = ff_q_mce_mdre_alt_target_positive * S ((S (ff_index_mce_alternating_mdre_alt_target)) * wc) + (ff_p_mce_alternating_mdre_alt_target))) /\ ((((exists ff_h_mce_mdre_alt_target_negative. ff_h_mce_mdre_alt_target_negative + S (ff_n_mce_alternating_mdre_alt_target) = S ((S (ff_index_mce_alternating_mdre_alt_target)) * zc)) /\ exists ff_q_mce_mdre_alt_target_negative. zb = ff_q_mce_mdre_alt_target_negative * S ((S (ff_index_mce_alternating_mdre_alt_target)) * zc) + (ff_n_mce_alternating_mdre_alt_target))) /\ (((exists ff_even_mce_term_mdre_alt_target_term. ff_index_mce_alternating_mdre_alt_target = 2 * ff_even_mce_term_mdre_alt_target_term) /\ (ff_p_mce_alternating_mdre_alt_target = (ff_ap_mce_alternating_mdre_alt_target) * (ff_bp_mce_alternating_mdre_alt_target) + (ff_an_mce_alternating_mdre_alt_target) * (ff_bn_mce_alternating_mdre_alt_target) /\ ff_n_mce_alternating_mdre_alt_target = (ff_ap_mce_alternating_mdre_alt_target) * (ff_bn_mce_alternating_mdre_alt_target) + (ff_an_mce_alternating_mdre_alt_target) * (ff_bp_mce_alternating_mdre_alt_target))) \/ ((exists ff_odd_mce_term_mdre_alt_target_term. ff_index_mce_alternating_mdre_alt_target = 2 * ff_odd_mce_term_mdre_alt_target_term + 1) /\ (ff_p_mce_alternating_mdre_alt_target = (ff_ap_mce_alternating_mdre_alt_target) * (ff_bn_mce_alternating_mdre_alt_target) + (ff_an_mce_alternating_mdre_alt_target) * (ff_bp_mce_alternating_mdre_alt_target) /\ ff_n_mce_alternating_mdre_alt_target = (ff_ap_mce_alternating_mdre_alt_target) * (ff_bp_mce_alternating_mdre_alt_target) + (ff_an_mce_alternating_mdre_alt_target) * (ff_bn_mce_alternating_mdre_alt_target)))))))))))Complete tactic proof in conservative notation
All 79 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints 79 script commands · 19 reading checkpoints · 1 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.
Expand checkpoints Collapse checkpoints Show original steps Find a step
01 Fix variables and assumptions L1–10 Work with arbitrary variables or the premises of the current implication.
L1 intro pb
L2 intro pc
L3 intro nb
L4 intro nc
L5 intro eb
L6 intro ec
L7 intro fb
L8 intro fc
L9 intro qb
L10 intro qc
02 Fix variables and assumptions L11–20 Work with arbitrary variables or the premises of the current implication.
L11 intro rb
L12 intro rc
L13 intro ub
L14 intro uc
L15 intro vb
L16 intro vc
L17 intro wb
L18 intro wc
L19 intro zb
L20 intro zc
03 Fix variables and assumptions L21–28 Work with arbitrary variables or the premises of the current implication.
L21 intro l
L22 intro hrowp
L23 intro hrown
L24 intro hcofp
L25 intro hcofn
L26 intro hprefix
L27 intro i
L28 intro hi
04 Establish hentry L29–32 Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
L29 have hentry : ∃ ap. ∃ an. ∃ bp. ∃ bn. ∃ p. ∃ n. BetaAt(pb,pc,i,ap) ∧ (BetaAt(nb,nc,i,an) ∧ (BetaAt(eb,ec,i,bp) ∧ (BetaAt(fb,fc,i,bn) ∧ (BetaAt(wb,wc,i,p) ∧ (BetaAt(zb,zc,i,n) ∧ SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n))))))Definitions: BetaAt(pb,pc,i,ap) BetaAt(nb,nc,i,an) BetaAt(eb,ec,i,bp) BetaAt(fb,fc,i,bn) BetaAt(wb,wc,i,p) BetaAt(zb,zc,i,n) SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n) Original native command in the exact edition L30 specialize hprefix (i)
L31 apply hprefix
L32 exact hi
05 Separate the logical cases L33–42 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L33 cases hentry
L34 cases hentry_witness
L35 cases hentry_witness_witness
L36 cases hentry_witness_witness_witness
L37 cases hentry_witness_witness_witness_witness
L38 cases hentry_witness_witness_witness_witness_witness
L39 cases hentry_witness_witness_witness_witness_witness_witness
L40 cases hentry_witness_witness_witness_witness_witness_witness_right
L41 cases hentry_witness_witness_witness_witness_witness_witness_right_right
L42 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right
06 Separate the logical cases L43–44 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L43 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right
L44 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right
07 Construct an explicit witness L45–50 Supply the displayed value, then prove that it has the required property.
L45 exists x
L46 exists x1
L47 exists x2
L48 exists x3
L49 exists x4
L50 exists x5
08 Separate the logical cases L51–51 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L51 split
09 Use earlier facts L52–56 Instantiate or apply named facts and discharge the corresponding proof obligations.
L52 specialize hrowp (i)
L53 specialize hrowp (x)
L54 apply hrowp
L55 exact hi
L56 exact hentry_witness_witness_witness_witness_witness_witness_left
10 Separate the logical cases L57–57 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L57 split
11 Use earlier facts L58–62 Instantiate or apply named facts and discharge the corresponding proof obligations.
L58 specialize hrown (i)
L59 specialize hrown (x1)
L60 apply hrown
L61 exact hi
L62 exact hentry_witness_witness_witness_witness_witness_witness_right_left
12 Separate the logical cases L63–63 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L63 split
13 Use earlier facts L64–68 Instantiate or apply named facts and discharge the corresponding proof obligations.
L64 specialize hcofp (i)
L65 specialize hcofp (x2)
L66 apply hcofp
L67 exact hi
L68 exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
14 Separate the logical cases L69–69 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L69 split
15 Use earlier facts L70–74 Instantiate or apply named facts and discharge the corresponding proof obligations.
L70 specialize hcofn (i)
L71 specialize hcofn (x3)
L72 apply hcofn
L73 exact hi
L74 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left
16 Separate the logical cases L75–75 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L75 split
17 Use earlier facts L76–76 Instantiate or apply named facts and discharge the corresponding proof obligations.
L76 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
18 Separate the logical cases L77–77 Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
L77 split
19 Use earlier facts L78–79 Instantiate or apply named facts and discharge the corresponding proof obligations.
L78 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
L79 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right
Library-wide reading audit
Original defined command ledger · 79 lines 0001 intro pb0002 intro pc0003 intro nb0004 intro nc0005 intro eb0006 intro ec0007 intro fb0008 intro fc0009 intro qb0010 intro qc0011 intro rb0012 intro rc0013 intro ub0014 intro uc0015 intro vb0016 intro vc0017 intro wb0018 intro wc0019 intro zb0020 intro zc0021 intro l0022 intro hrowp0023 intro hrown0024 intro hcofp0025 intro hcofn0026 intro hprefix0027 intro i0028 intro hi0029 have hentry : ∃ ap. ∃ an. ∃ bp. ∃ bn. ∃ p. ∃ n. BetaAt(pb,pc,i,ap) ∧ (BetaAt(nb,nc,i,an) ∧ (BetaAt(eb,ec,i,bp) ∧ (BetaAt(fb,fc,i,bn) ∧ (BetaAt(wb,wc,i,p) ∧ (BetaAt(zb,zc,i,n) ∧ SignedAlternatingCofactorTerm(ap,an,bp,bn,i,p,n) )))))0030 specialize hprefix (i)0031 apply hprefix0032 exact hi0033 cases hentry0034 cases hentry_witness0035 cases hentry_witness_witness0036 cases hentry_witness_witness_witness0037 cases hentry_witness_witness_witness_witness0038 cases hentry_witness_witness_witness_witness_witness0039 cases hentry_witness_witness_witness_witness_witness_witness0040 cases hentry_witness_witness_witness_witness_witness_witness_right0041 cases hentry_witness_witness_witness_witness_witness_witness_right_right0042 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right0043 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right0044 cases hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right0045 exists x0046 exists x10047 exists x20048 exists x30049 exists x40050 exists x50051 split0052 specialize hrowp (i)0053 specialize hrowp (x)0054 apply hrowp0055 exact hi0056 exact hentry_witness_witness_witness_witness_witness_witness_left0057 split0058 specialize hrown (i)0059 specialize hrown (x1)0060 apply hrown0061 exact hi0062 exact hentry_witness_witness_witness_witness_witness_witness_right_left0063 split0064 specialize hcofp (i)0065 specialize hcofp (x2)0066 apply hcofp0067 exact hi0068 exact hentry_witness_witness_witness_witness_witness_witness_right_right_left0069 split0070 specialize hcofn (i)0071 specialize hcofn (x3)0072 apply hcofn0073 exact hi0074 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left0075 split0076 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left0077 split0078 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left0079 exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right