CE0017

signed_alternating_cofactor_fold_exists

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

Every arbitrary-length pair of signed beta-coded row/cofactor streams has exact positive and negative alternating Laplace-sum 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 l. exists p n. (exists ff_ub_mce_fold_result ff_uc_mce_fold_result ff_vb_mce_fold_result ff_vc_mce_fold_result. ((forall ff_index_mce_alternating_result_prefix. (exists ff_gap_mce_result_prefix_index. ff_gap_mce_result_prefix_index + S (ff_index_mce_alternating_result_prefix) = (l)) -> exists ff_ap_mce_alternating_result_prefix ff_an_mce_alternating_result_prefix ff_bp_mce_alternating_result_prefix ff_bn_mce_alternating_result_prefix ff_p_mce_alternating_result_prefix ff_n_mce_alternating_result_prefix. ((((exists ff_h_mce_result_prefix_ap. ff_h_mce_result_prefix_ap + S (ff_ap_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ac)) /\ exists ff_q_mce_result_prefix_ap. ab = ff_q_mce_result_prefix_ap * S ((S (ff_index_mce_alternating_result_prefix)) * ac) + (ff_ap_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_an. ff_h_mce_result_prefix_an + S (ff_an_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * dc)) /\ exists ff_q_mce_result_prefix_an. db = ff_q_mce_result_prefix_an * S ((S (ff_index_mce_alternating_result_prefix)) * dc) + (ff_an_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_bp. ff_h_mce_result_prefix_bp + S (ff_bp_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ec)) /\ exists ff_q_mce_result_prefix_bp. eb = ff_q_mce_result_prefix_bp * S ((S (ff_index_mce_alternating_result_prefix)) * ec) + (ff_bp_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_bn. ff_h_mce_result_prefix_bn + S (ff_bn_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * fc)) /\ exists ff_q_mce_result_prefix_bn. fb = ff_q_mce_result_prefix_bn * S ((S (ff_index_mce_alternating_result_prefix)) * fc) + (ff_bn_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_positive. ff_h_mce_result_prefix_positive + S (ff_p_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ff_uc_mce_fold_result)) /\ exists ff_q_mce_result_prefix_positive. ff_ub_mce_fold_result = ff_q_mce_result_prefix_positive * S ((S (ff_index_mce_alternating_result_prefix)) * ff_uc_mce_fold_result) + (ff_p_mce_alternating_result_prefix))) /\ ((((exists ff_h_mce_result_prefix_negative. ff_h_mce_result_prefix_negative + S (ff_n_mce_alternating_result_prefix) = S ((S (ff_index_mce_alternating_result_prefix)) * ff_vc_mce_fold_result)) /\ exists ff_q_mce_result_prefix_negative. ff_vb_mce_fold_result = ff_q_mce_result_prefix_negative * S ((S (ff_index_mce_alternating_result_prefix)) * ff_vc_mce_fold_result) + (ff_n_mce_alternating_result_prefix))) /\ (((exists ff_even_mce_term_result_prefix_term. ff_index_mce_alternating_result_prefix = 2 * ff_even_mce_term_result_prefix_term) /\ (ff_p_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) /\ ff_n_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix))) \/ ((exists ff_odd_mce_term_result_prefix_term. ff_index_mce_alternating_result_prefix = 2 * ff_odd_mce_term_result_prefix_term + 1) /\ (ff_p_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) /\ ff_n_mce_alternating_result_prefix = (ff_ap_mce_alternating_result_prefix) * (ff_bp_mce_alternating_result_prefix) + (ff_an_mce_alternating_result_prefix) * (ff_bn_mce_alternating_result_prefix))))))))))) /\ ((exists ff_u_mce_result_positive ff_v_mce_result_positive. ((((exists ff_h_mce_result_positive_start. ff_h_mce_result_positive_start + S (0) = S ((S (0)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_start. ff_u_mce_result_positive = ff_q_mce_result_positive_start * S ((S (0)) * ff_v_mce_result_positive) + (0))) /\ ((((exists ff_h_mce_result_positive_terminal. ff_h_mce_result_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_terminal. ff_u_mce_result_positive = ff_q_mce_result_positive_terminal * S ((S (l)) * ff_v_mce_result_positive) + (p))) /\ forall ff_i_mce_result_positive. (exists ff_lt_mce_result_positive_bound. ff_lt_mce_result_positive_bound + S ff_i_mce_result_positive = l) -> exists ff_a_mce_result_positive ff_r_mce_result_positive ff_s_mce_result_positive. ((((exists ff_h_mce_result_positive_summand. ff_h_mce_result_positive_summand + S (ff_a_mce_result_positive) = S ((S (ff_i_mce_result_positive)) * ff_uc_mce_fold_result)) /\ exists ff_q_mce_result_positive_summand. ff_ub_mce_fold_result = ff_q_mce_result_positive_summand * S ((S (ff_i_mce_result_positive)) * ff_uc_mce_fold_result) + (ff_a_mce_result_positive))) /\ ((((exists ff_h_mce_result_positive_partial. ff_h_mce_result_positive_partial + S (ff_r_mce_result_positive) = S ((S (ff_i_mce_result_positive)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_partial. ff_u_mce_result_positive = ff_q_mce_result_positive_partial * S ((S (ff_i_mce_result_positive)) * ff_v_mce_result_positive) + (ff_r_mce_result_positive))) /\ ((((exists ff_h_mce_result_positive_successor. ff_h_mce_result_positive_successor + S (ff_s_mce_result_positive) = S ((S (S ff_i_mce_result_positive)) * ff_v_mce_result_positive)) /\ exists ff_q_mce_result_positive_successor. ff_u_mce_result_positive = ff_q_mce_result_positive_successor * S ((S (S ff_i_mce_result_positive)) * ff_v_mce_result_positive) + (ff_s_mce_result_positive))) /\ ff_s_mce_result_positive = ff_r_mce_result_positive + ff_a_mce_result_positive)))))) /\ (exists ff_u_mce_result_negative ff_v_mce_result_negative. ((((exists ff_h_mce_result_negative_start. ff_h_mce_result_negative_start + S (0) = S ((S (0)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_start. ff_u_mce_result_negative = ff_q_mce_result_negative_start * S ((S (0)) * ff_v_mce_result_negative) + (0))) /\ ((((exists ff_h_mce_result_negative_terminal. ff_h_mce_result_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_terminal. ff_u_mce_result_negative = ff_q_mce_result_negative_terminal * S ((S (l)) * ff_v_mce_result_negative) + (n))) /\ forall ff_i_mce_result_negative. (exists ff_lt_mce_result_negative_bound. ff_lt_mce_result_negative_bound + S ff_i_mce_result_negative = l) -> exists ff_a_mce_result_negative ff_r_mce_result_negative ff_s_mce_result_negative. ((((exists ff_h_mce_result_negative_summand. ff_h_mce_result_negative_summand + S (ff_a_mce_result_negative) = S ((S (ff_i_mce_result_negative)) * ff_vc_mce_fold_result)) /\ exists ff_q_mce_result_negative_summand. ff_vb_mce_fold_result = ff_q_mce_result_negative_summand * S ((S (ff_i_mce_result_negative)) * ff_vc_mce_fold_result) + (ff_a_mce_result_negative))) /\ ((((exists ff_h_mce_result_negative_partial. ff_h_mce_result_negative_partial + S (ff_r_mce_result_negative) = S ((S (ff_i_mce_result_negative)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_partial. ff_u_mce_result_negative = ff_q_mce_result_negative_partial * S ((S (ff_i_mce_result_negative)) * ff_v_mce_result_negative) + (ff_r_mce_result_negative))) /\ ((((exists ff_h_mce_result_negative_successor. ff_h_mce_result_negative_successor + S (ff_s_mce_result_negative) = S ((S (S ff_i_mce_result_negative)) * ff_v_mce_result_negative)) /\ exists ff_q_mce_result_negative_successor. ff_u_mce_result_negative = ff_q_mce_result_negative_successor * S ((S (S ff_i_mce_result_negative)) * ff_v_mce_result_negative) + (ff_s_mce_result_negative))) /\ ff_s_mce_result_negative = ff_r_mce_result_negative + ff_a_mce_result_negative)))))))))

Constructive proof overview

Generated structural guide

Every arbitrary-length pair of signed beta-coded row/cofactor streams has exact positive and negative alternating Laplace-sum components.

The unchanged tactic script uses 2 declared prerequisites and contains 47 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CE0013 signed_alternating_product_prefix_exists beta_sum_exists Stable theorem; checked-use authorized

Direct dependents

CE0019 signed_alternating_cofactor_fold_exists_unique CE001C signed_first_row_cofactor_fold_exists

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

47 script commands · 13 reading checkpoints · 3 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)
signed alternating product prefix exists

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–9

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 l
02Establish hprefixL10–19

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have hprefix : ∃ ub. ∃ uc. ∃ vb. ∃ vc. SignedAlternatingProductPrefix(ab,ac,db,dc,eb,ec,fb,fc,ub,uc,vb,vc,l)Definitions: SignedAlternatingProductPrefix
  2. L11
    specialize signed_alternating_product_prefix_exists ab
  3. L12
    specialize signed_alternating_product_prefix_exists ac
  4. L13
    specialize signed_alternating_product_prefix_exists db
  5. L14
    specialize signed_alternating_product_prefix_exists dc
  6. L15
    specialize signed_alternating_product_prefix_exists eb
  7. L16
    specialize signed_alternating_product_prefix_exists ec
  8. L17
    specialize signed_alternating_product_prefix_exists fb
  9. L18
    specialize signed_alternating_product_prefix_exists fc
  10. L19
    specialize signed_alternating_product_prefix_exists l
03Use earlier factsL20–20

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

  1. L20
    exact signed_alternating_product_prefix_exists
04Separate the logical casesL21–24

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

  1. L21
    cases hprefix
  2. L22
    cases hprefix_witness
  3. L23
    cases hprefix_witness_witness
  4. L24
    cases hprefix_witness_witness_witness
05Establish hpositiveL25–29

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hpositive : ∃ p. Sum(x,x1,l,p)Definitions: Sum
  2. L26
    specialize beta_sum_exists x
  3. L27
    specialize beta_sum_exists x1
  4. L28
    specialize beta_sum_exists l
  5. L29
    exact beta_sum_exists
06Separate the logical casesL30–30

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

  1. L30
    cases hpositive
07Establish hnegativeL31–35

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hnegative : ∃ n. Sum(x2,x3,l,n)Definitions: Sum
  2. L32
    specialize beta_sum_exists x2
  3. L33
    specialize beta_sum_exists x3
  4. L34
    specialize beta_sum_exists l
  5. L35
    exact beta_sum_exists
08Separate the logical casesL36–36

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

  1. L36
    cases hnegative
09Construct an explicit witnessL37–42

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

  1. L37
    exists x4
  2. L38
    exists x5
  3. L39
    exists x
  4. L40
    exists x1
  5. L41
    exists x2
  6. L42
    exists x3
10Separate the logical casesL43–43

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

  1. L43
    split
11Use earlier factsL44–44

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

  1. L44
    exact hprefix_witness_witness_witness_witness
12Separate the logical casesL45–45

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

  1. L45
    split
13Use earlier factsL46–47

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

  1. L46
    exact hpositive_witness
  2. L47
    exact hnegative_witness

Library-wide reading audit

Original exact command ledger · 47 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 l
  10. 0010have hprefix : exists ub uc vb vc. (forall ff_index_mce_alternating_existence. (exists ff_gap_mce_existence_index. ff_gap_mce_existence_index + S (ff_index_mce_alternating_existence) = (l)) -> exists ff_ap_mce_alternating_existence ff_an_mce_alternating_existence ff_bp_mce_alternating_existence ff_bn_mce_alternating_existence ff_p_mce_alternating_existence ff_n_mce_alternating_existence. ((((exists ff_h_mce_existence_ap. ff_h_mce_existence_ap + S (ff_ap_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * ac)) /\ exists ff_q_mce_existence_ap. ab = ff_q_mce_existence_ap * S ((S (ff_index_mce_alternating_existence)) * ac) + (ff_ap_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_an. ff_h_mce_existence_an + S (ff_an_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * dc)) /\ exists ff_q_mce_existence_an. db = ff_q_mce_existence_an * S ((S (ff_index_mce_alternating_existence)) * dc) + (ff_an_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_bp. ff_h_mce_existence_bp + S (ff_bp_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * ec)) /\ exists ff_q_mce_existence_bp. eb = ff_q_mce_existence_bp * S ((S (ff_index_mce_alternating_existence)) * ec) + (ff_bp_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_bn. ff_h_mce_existence_bn + S (ff_bn_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * fc)) /\ exists ff_q_mce_existence_bn. fb = ff_q_mce_existence_bn * S ((S (ff_index_mce_alternating_existence)) * fc) + (ff_bn_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_positive. ff_h_mce_existence_positive + S (ff_p_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * uc)) /\ exists ff_q_mce_existence_positive. ub = ff_q_mce_existence_positive * S ((S (ff_index_mce_alternating_existence)) * uc) + (ff_p_mce_alternating_existence))) /\ ((((exists ff_h_mce_existence_negative. ff_h_mce_existence_negative + S (ff_n_mce_alternating_existence) = S ((S (ff_index_mce_alternating_existence)) * vc)) /\ exists ff_q_mce_existence_negative. vb = ff_q_mce_existence_negative * S ((S (ff_index_mce_alternating_existence)) * vc) + (ff_n_mce_alternating_existence))) /\ (((exists ff_even_mce_term_existence_term. ff_index_mce_alternating_existence = 2 * ff_even_mce_term_existence_term) /\ (ff_p_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bp_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bn_mce_alternating_existence) /\ ff_n_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bn_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bp_mce_alternating_existence))) \/ ((exists ff_odd_mce_term_existence_term. ff_index_mce_alternating_existence = 2 * ff_odd_mce_term_existence_term + 1) /\ (ff_p_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bn_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bp_mce_alternating_existence) /\ ff_n_mce_alternating_existence = (ff_ap_mce_alternating_existence) * (ff_bp_mce_alternating_existence) + (ff_an_mce_alternating_existence) * (ff_bn_mce_alternating_existence)))))))))))
  11. 0011specialize signed_alternating_product_prefix_exists ab
  12. 0012specialize signed_alternating_product_prefix_exists ac
  13. 0013specialize signed_alternating_product_prefix_exists db
  14. 0014specialize signed_alternating_product_prefix_exists dc
  15. 0015specialize signed_alternating_product_prefix_exists eb
  16. 0016specialize signed_alternating_product_prefix_exists ec
  17. 0017specialize signed_alternating_product_prefix_exists fb
  18. 0018specialize signed_alternating_product_prefix_exists fc
  19. 0019specialize signed_alternating_product_prefix_exists l
  20. 0020exact signed_alternating_product_prefix_exists
  21. 0021cases hprefix
  22. 0022cases hprefix_witness
  23. 0023cases hprefix_witness_witness
  24. 0024cases hprefix_witness_witness_witness
  25. 0025have hpositive : exists p. (exists ff_u_mce_fold_have_positive ff_v_mce_fold_have_positive. ((((exists ff_h_mce_fold_have_positive_start. ff_h_mce_fold_have_positive_start + S (0) = S ((S (0)) * ff_v_mce_fold_have_positive)) /\ exists ff_q_mce_fold_have_positive_start. ff_u_mce_fold_have_positive = ff_q_mce_fold_have_positive_start * S ((S (0)) * ff_v_mce_fold_have_positive) + (0))) /\ ((((exists ff_h_mce_fold_have_positive_terminal. ff_h_mce_fold_have_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_fold_have_positive)) /\ exists ff_q_mce_fold_have_positive_terminal. ff_u_mce_fold_have_positive = ff_q_mce_fold_have_positive_terminal * S ((S (l)) * ff_v_mce_fold_have_positive) + (p))) /\ forall ff_i_mce_fold_have_positive. (exists ff_lt_mce_fold_have_positive_bound. ff_lt_mce_fold_have_positive_bound + S ff_i_mce_fold_have_positive = l) -> exists ff_a_mce_fold_have_positive ff_r_mce_fold_have_positive ff_s_mce_fold_have_positive. ((((exists ff_h_mce_fold_have_positive_summand. ff_h_mce_fold_have_positive_summand + S (ff_a_mce_fold_have_positive) = S ((S (ff_i_mce_fold_have_positive)) * x1)) /\ exists ff_q_mce_fold_have_positive_summand. x = ff_q_mce_fold_have_positive_summand * S ((S (ff_i_mce_fold_have_positive)) * x1) + (ff_a_mce_fold_have_positive))) /\ ((((exists ff_h_mce_fold_have_positive_partial. ff_h_mce_fold_have_positive_partial + S (ff_r_mce_fold_have_positive) = S ((S (ff_i_mce_fold_have_positive)) * ff_v_mce_fold_have_positive)) /\ exists ff_q_mce_fold_have_positive_partial. ff_u_mce_fold_have_positive = ff_q_mce_fold_have_positive_partial * S ((S (ff_i_mce_fold_have_positive)) * ff_v_mce_fold_have_positive) + (ff_r_mce_fold_have_positive))) /\ ((((exists ff_h_mce_fold_have_positive_successor. ff_h_mce_fold_have_positive_successor + S (ff_s_mce_fold_have_positive) = S ((S (S ff_i_mce_fold_have_positive)) * ff_v_mce_fold_have_positive)) /\ exists ff_q_mce_fold_have_positive_successor. ff_u_mce_fold_have_positive = ff_q_mce_fold_have_positive_successor * S ((S (S ff_i_mce_fold_have_positive)) * ff_v_mce_fold_have_positive) + (ff_s_mce_fold_have_positive))) /\ ff_s_mce_fold_have_positive = ff_r_mce_fold_have_positive + ff_a_mce_fold_have_positive))))))
  26. 0026specialize beta_sum_exists x
  27. 0027specialize beta_sum_exists x1
  28. 0028specialize beta_sum_exists l
  29. 0029exact beta_sum_exists
  30. 0030cases hpositive
  31. 0031have hnegative : exists n. (exists ff_u_mce_fold_have_negative ff_v_mce_fold_have_negative. ((((exists ff_h_mce_fold_have_negative_start. ff_h_mce_fold_have_negative_start + S (0) = S ((S (0)) * ff_v_mce_fold_have_negative)) /\ exists ff_q_mce_fold_have_negative_start. ff_u_mce_fold_have_negative = ff_q_mce_fold_have_negative_start * S ((S (0)) * ff_v_mce_fold_have_negative) + (0))) /\ ((((exists ff_h_mce_fold_have_negative_terminal. ff_h_mce_fold_have_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_fold_have_negative)) /\ exists ff_q_mce_fold_have_negative_terminal. ff_u_mce_fold_have_negative = ff_q_mce_fold_have_negative_terminal * S ((S (l)) * ff_v_mce_fold_have_negative) + (n))) /\ forall ff_i_mce_fold_have_negative. (exists ff_lt_mce_fold_have_negative_bound. ff_lt_mce_fold_have_negative_bound + S ff_i_mce_fold_have_negative = l) -> exists ff_a_mce_fold_have_negative ff_r_mce_fold_have_negative ff_s_mce_fold_have_negative. ((((exists ff_h_mce_fold_have_negative_summand. ff_h_mce_fold_have_negative_summand + S (ff_a_mce_fold_have_negative) = S ((S (ff_i_mce_fold_have_negative)) * x3)) /\ exists ff_q_mce_fold_have_negative_summand. x2 = ff_q_mce_fold_have_negative_summand * S ((S (ff_i_mce_fold_have_negative)) * x3) + (ff_a_mce_fold_have_negative))) /\ ((((exists ff_h_mce_fold_have_negative_partial. ff_h_mce_fold_have_negative_partial + S (ff_r_mce_fold_have_negative) = S ((S (ff_i_mce_fold_have_negative)) * ff_v_mce_fold_have_negative)) /\ exists ff_q_mce_fold_have_negative_partial. ff_u_mce_fold_have_negative = ff_q_mce_fold_have_negative_partial * S ((S (ff_i_mce_fold_have_negative)) * ff_v_mce_fold_have_negative) + (ff_r_mce_fold_have_negative))) /\ ((((exists ff_h_mce_fold_have_negative_successor. ff_h_mce_fold_have_negative_successor + S (ff_s_mce_fold_have_negative) = S ((S (S ff_i_mce_fold_have_negative)) * ff_v_mce_fold_have_negative)) /\ exists ff_q_mce_fold_have_negative_successor. ff_u_mce_fold_have_negative = ff_q_mce_fold_have_negative_successor * S ((S (S ff_i_mce_fold_have_negative)) * ff_v_mce_fold_have_negative) + (ff_s_mce_fold_have_negative))) /\ ff_s_mce_fold_have_negative = ff_r_mce_fold_have_negative + ff_a_mce_fold_have_negative))))))
  32. 0032specialize beta_sum_exists x2
  33. 0033specialize beta_sum_exists x3
  34. 0034specialize beta_sum_exists l
  35. 0035exact beta_sum_exists
  36. 0036cases hnegative
  37. 0037exists x4
  38. 0038exists x5
  39. 0039exists x
  40. 0040exists x1
  41. 0041exists x2
  42. 0042exists x3
  43. 0043split
  44. 0044exact hprefix_witness_witness_witness_witness
  45. 0045split
  46. 0046exact hpositive_witness
  47. 0047exact hnegative_witness

Separate complete second-wave branches: Full T13 proof · Alpha v27.