DL0020

matrix_recursive_alternating_prefix_transport

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

The exact signed parity-correct product stream is unchanged when all four finite input streams preserve their actual entries.

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 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)))))))))))

Constructive proof overview

Generated structural guide

The exact signed parity-correct product stream is unchanged when all four finite input streams preserve their actual entries.

The unchanged tactic script uses 0 declared prerequisites and contains 79 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

DL0021 matrix_recursive_alternating_fold_transport

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

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.

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 pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro eb
  6. L6
    intro ec
  7. L7
    intro fb
  8. L8
    intro fc
  9. L9
    intro qb
  10. L10
    intro qc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro rb
  2. L12
    intro rc
  3. L13
    intro ub
  4. L14
    intro uc
  5. L15
    intro vb
  6. L16
    intro vc
  7. L17
    intro wb
  8. L18
    intro wc
  9. L19
    intro zb
  10. L20
    intro zc
03Fix variables and assumptionsL21–28

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

  1. L21
    intro l
  2. L22
    intro hrowp
  3. L23
    intro hrown
  4. L24
    intro hcofp
  5. L25
    intro hcofn
  6. L26
    intro hprefix
  7. L27
    intro i
  8. L28
    intro hi
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 : ∃ 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: SignedAlternatingCofactorTermBetaAt
  2. L30
    specialize hprefix (i)
  3. L31
    apply hprefix
  4. L32
    exact hi
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
07Construct an explicit witnessL45–50

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

  1. L45
    exists x
  2. L46
    exists x1
  3. L47
    exists x2
  4. L48
    exists x3
  5. L49
    exists x4
  6. L50
    exists x5
08Separate the logical casesL51–51

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

  1. L51
    split
09Use earlier factsL52–56

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

  1. L52
    specialize hrowp (i)
  2. L53
    specialize hrowp (x)
  3. L54
    apply hrowp
  4. L55
    exact hi
  5. L56
    exact hentry_witness_witness_witness_witness_witness_witness_left
10Separate the logical casesL57–57

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

  1. L57
    split
11Use earlier factsL58–62

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

  1. L58
    specialize hrown (i)
  2. L59
    specialize hrown (x1)
  3. L60
    apply hrown
  4. L61
    exact hi
  5. L62
    exact hentry_witness_witness_witness_witness_witness_witness_right_left
12Separate the logical casesL63–63

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

  1. L63
    split
13Use earlier factsL64–68

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

  1. L64
    specialize hcofp (i)
  2. L65
    specialize hcofp (x2)
  3. L66
    apply hcofp
  4. L67
    exact hi
  5. L68
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
14Separate the logical casesL69–69

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

  1. L69
    split
15Use earlier factsL70–74

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

  1. L70
    specialize hcofn (i)
  2. L71
    specialize hcofn (x3)
  3. L72
    apply hcofn
  4. L73
    exact hi
  5. L74
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left
16Separate the logical casesL75–75

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

  1. L75
    split
17Use earlier factsL76–76

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

  1. L76
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
18Separate the logical casesL77–77

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

  1. L77
    split
19Use earlier factsL78–79

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

  1. L78
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  2. L79
    exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original exact command ledger · 79 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro eb
  6. 0006intro ec
  7. 0007intro fb
  8. 0008intro fc
  9. 0009intro qb
  10. 0010intro qc
  11. 0011intro rb
  12. 0012intro rc
  13. 0013intro ub
  14. 0014intro uc
  15. 0015intro vb
  16. 0016intro vc
  17. 0017intro wb
  18. 0018intro wc
  19. 0019intro zb
  20. 0020intro zc
  21. 0021intro l
  22. 0022intro hrowp
  23. 0023intro hrown
  24. 0024intro hcofp
  25. 0025intro hcofn
  26. 0026intro hprefix
  27. 0027intro i
  28. 0028intro hi
  29. 0029have hentry : exists ap an bp bn p n. ((((exists ff_h_mdr_fold_entry_0. ff_h_mdr_fold_entry_0 + S (ap) = S ((S (i)) * pc)) /\ exists ff_q_mdr_fold_entry_0. pb = ff_q_mdr_fold_entry_0 * S ((S (i)) * pc) + (ap))) /\ ((((exists ff_h_mdr_fold_entry_1. ff_h_mdr_fold_entry_1 + S (an) = S ((S (i)) * nc)) /\ exists ff_q_mdr_fold_entry_1. nb = ff_q_mdr_fold_entry_1 * S ((S (i)) * nc) + (an))) /\ ((((exists ff_h_mdr_fold_entry_2. ff_h_mdr_fold_entry_2 + S (bp) = S ((S (i)) * ec)) /\ exists ff_q_mdr_fold_entry_2. eb = ff_q_mdr_fold_entry_2 * S ((S (i)) * ec) + (bp))) /\ ((((exists ff_h_mdr_fold_entry_3. ff_h_mdr_fold_entry_3 + S (bn) = S ((S (i)) * fc)) /\ exists ff_q_mdr_fold_entry_3. fb = ff_q_mdr_fold_entry_3 * S ((S (i)) * fc) + (bn))) /\ ((((exists ff_h_mdr_fold_entry_p. ff_h_mdr_fold_entry_p + S (p) = S ((S (i)) * wc)) /\ exists ff_q_mdr_fold_entry_p. wb = ff_q_mdr_fold_entry_p * S ((S (i)) * wc) + (p))) /\ ((((exists ff_h_mdr_fold_entry_n. ff_h_mdr_fold_entry_n + S (n) = S ((S (i)) * zc)) /\ exists ff_q_mdr_fold_entry_n. zb = ff_q_mdr_fold_entry_n * S ((S (i)) * zc) + (n))) /\ (((exists ff_even_mce_term_mdre_fold_entry. i = 2 * ff_even_mce_term_mdre_fold_entry) /\ (p = (ap) * (bp) + (an) * (bn) /\ n = (ap) * (bn) + (an) * (bp))) \/ ((exists ff_odd_mce_term_mdre_fold_entry. i = 2 * ff_odd_mce_term_mdre_fold_entry + 1) /\ (p = (ap) * (bn) + (an) * (bp) /\ n = (ap) * (bp) + (an) * (bn))))))))))
  30. 0030specialize hprefix (i)
  31. 0031apply hprefix
  32. 0032exact hi
  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. 0045exists x
  46. 0046exists x1
  47. 0047exists x2
  48. 0048exists x3
  49. 0049exists x4
  50. 0050exists x5
  51. 0051split
  52. 0052specialize hrowp (i)
  53. 0053specialize hrowp (x)
  54. 0054apply hrowp
  55. 0055exact hi
  56. 0056exact hentry_witness_witness_witness_witness_witness_witness_left
  57. 0057split
  58. 0058specialize hrown (i)
  59. 0059specialize hrown (x1)
  60. 0060apply hrown
  61. 0061exact hi
  62. 0062exact hentry_witness_witness_witness_witness_witness_witness_right_left
  63. 0063split
  64. 0064specialize hcofp (i)
  65. 0065specialize hcofp (x2)
  66. 0066apply hcofp
  67. 0067exact hi
  68. 0068exact hentry_witness_witness_witness_witness_witness_witness_right_right_left
  69. 0069split
  70. 0070specialize hcofn (i)
  71. 0071specialize hcofn (x3)
  72. 0072apply hcofn
  73. 0073exact hi
  74. 0074exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_left
  75. 0075split
  76. 0076exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  77. 0077split
  78. 0078exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  79. 0079exact hentry_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right