CE001C

signed_first_row_cofactor_fold_exists

The ACTUAL decoded first row of every signed square matrix has an exact arbitrary-arity alternating fold against any supplied signed cofactor values.

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

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.

Historical partial components only: this chapter proves genuine signed first-row minors and unique alternating folds, with supplied cofactor values. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with actual arbitrary determinant data, rank, and integer column spans; lattice index and normal forms are not claimed. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ q. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∃ p. ∃ n. SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n) · 1

Actual proof prerequisites

signed_matrix_first_row_components_existssigned_alternating_cofactor_fold_exists
Original expanded first-order statement 
forall pb pc nb nc q eb ec fb fc. exists p n. (exists ff_ab_mce_row_result ff_ac_mce_row_result ff_db_mce_row_result ff_dc_mce_row_result. ((forall ff_index_mcp_mce_result_positive ff_source_mcp_mce_result_positive ff_target_mcp_mce_result_positive. (exists mcp_gap_mce_result_positive_bound. mcp_gap_mce_result_positive_bound + S (ff_index_mcp_mce_result_positive) = (S (q))) -> (((exists fs_h_mcp_mce_result_positive_source. fs_h_mcp_mce_result_positive_source + S (ff_source_mcp_mce_result_positive) = S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc)) /\ exists fs_q_mcp_mce_result_positive_source. pb = fs_q_mcp_mce_result_positive_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc) + (ff_source_mcp_mce_result_positive))) -> (((exists fs_h_mcp_mce_result_positive_target. fs_h_mcp_mce_result_positive_target + S (ff_target_mcp_mce_result_positive) = S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result)) /\ exists fs_q_mcp_mce_result_positive_target. ff_ab_mce_row_result = fs_q_mcp_mce_result_positive_target * S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result) + (ff_target_mcp_mce_result_positive))) -> ff_target_mcp_mce_result_positive = ff_source_mcp_mce_result_positive) /\ ((forall ff_index_mcp_mce_result_negative ff_source_mcp_mce_result_negative ff_target_mcp_mce_result_negative. (exists mcp_gap_mce_result_negative_bound. mcp_gap_mce_result_negative_bound + S (ff_index_mcp_mce_result_negative) = (S (q))) -> (((exists fs_h_mcp_mce_result_negative_source. fs_h_mcp_mce_result_negative_source + S (ff_source_mcp_mce_result_negative) = S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc)) /\ exists fs_q_mcp_mce_result_negative_source. nb = fs_q_mcp_mce_result_negative_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc) + (ff_source_mcp_mce_result_negative))) -> (((exists fs_h_mcp_mce_result_negative_target. fs_h_mcp_mce_result_negative_target + S (ff_target_mcp_mce_result_negative) = S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result)) /\ exists fs_q_mcp_mce_result_negative_target. ff_db_mce_row_result = fs_q_mcp_mce_result_negative_target * S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result) + (ff_target_mcp_mce_result_negative))) -> ff_target_mcp_mce_result_negative = ff_source_mcp_mce_result_negative) /\ (exists ff_ub_mce_fold_result_fold ff_uc_mce_fold_result_fold ff_vb_mce_fold_result_fold ff_vc_mce_fold_result_fold. ((forall ff_index_mce_alternating_result_fold_prefix. (exists ff_gap_mce_result_fold_prefix_index. ff_gap_mce_result_fold_prefix_index + S (ff_index_mce_alternating_result_fold_prefix) = (S (q))) -> exists ff_ap_mce_alternating_result_fold_prefix ff_an_mce_alternating_result_fold_prefix ff_bp_mce_alternating_result_fold_prefix ff_bn_mce_alternating_result_fold_prefix ff_p_mce_alternating_result_fold_prefix ff_n_mce_alternating_result_fold_prefix. ((((exists ff_h_mce_result_fold_prefix_ap. ff_h_mce_result_fold_prefix_ap + S (ff_ap_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_ap. ff_ab_mce_row_result = ff_q_mce_result_fold_prefix_ap * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result) + (ff_ap_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_an. ff_h_mce_result_fold_prefix_an + S (ff_an_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_an. ff_db_mce_row_result = ff_q_mce_result_fold_prefix_an * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result) + (ff_an_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bp. ff_h_mce_result_fold_prefix_bp + S (ff_bp_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec)) /\ exists ff_q_mce_result_fold_prefix_bp. eb = ff_q_mce_result_fold_prefix_bp * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec) + (ff_bp_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bn. ff_h_mce_result_fold_prefix_bn + S (ff_bn_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc)) /\ exists ff_q_mce_result_fold_prefix_bn. fb = ff_q_mce_result_fold_prefix_bn * S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc) + (ff_bn_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_positive. ff_h_mce_result_fold_prefix_positive + S (ff_p_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_positive. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_prefix_positive * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold) + (ff_p_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_negative. ff_h_mce_result_fold_prefix_negative + S (ff_n_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_negative. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_prefix_negative * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold) + (ff_n_mce_alternating_result_fold_prefix))) /\ (((exists ff_even_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_even_mce_term_result_fold_prefix_term) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix))) \/ ((exists ff_odd_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_odd_mce_term_result_fold_prefix_term + 1) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix))))))))))) /\ ((exists ff_u_mce_result_fold_positive ff_v_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_start. ff_h_mce_result_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_start. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_start * S ((S (0)) * ff_v_mce_result_fold_positive) + (0))) /\ ((((exists ff_h_mce_result_fold_positive_terminal. ff_h_mce_result_fold_positive_terminal + S (p) = S ((S ((S (q)))) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_terminal. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_positive) + (p))) /\ forall ff_i_mce_result_fold_positive. (exists ff_lt_mce_result_fold_positive_bound. ff_lt_mce_result_fold_positive_bound + S ff_i_mce_result_fold_positive = (S (q))) -> exists ff_a_mce_result_fold_positive ff_r_mce_result_fold_positive ff_s_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_summand. ff_h_mce_result_fold_positive_summand + S (ff_a_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_positive_summand. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_positive_summand * S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold) + (ff_a_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_partial. ff_h_mce_result_fold_positive_partial + S (ff_r_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_partial. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_partial * S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_r_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_successor. ff_h_mce_result_fold_positive_successor + S (ff_s_mce_result_fold_positive) = S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_successor. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_successor * S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_s_mce_result_fold_positive))) /\ ff_s_mce_result_fold_positive = ff_r_mce_result_fold_positive + ff_a_mce_result_fold_positive)))))) /\ (exists ff_u_mce_result_fold_negative ff_v_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_start. ff_h_mce_result_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_start. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_start * S ((S (0)) * ff_v_mce_result_fold_negative) + (0))) /\ ((((exists ff_h_mce_result_fold_negative_terminal. ff_h_mce_result_fold_negative_terminal + S (n) = S ((S ((S (q)))) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_terminal. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_negative) + (n))) /\ forall ff_i_mce_result_fold_negative. (exists ff_lt_mce_result_fold_negative_bound. ff_lt_mce_result_fold_negative_bound + S ff_i_mce_result_fold_negative = (S (q))) -> exists ff_a_mce_result_fold_negative ff_r_mce_result_fold_negative ff_s_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_summand. ff_h_mce_result_fold_negative_summand + S (ff_a_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_negative_summand. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_negative_summand * S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold) + (ff_a_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_partial. ff_h_mce_result_fold_negative_partial + S (ff_r_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_partial. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_partial * S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_r_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_successor. ff_h_mce_result_fold_negative_successor + S (ff_s_mce_result_fold_negative) = S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_successor. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_successor * S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_s_mce_result_fold_negative))) /\ ff_s_mce_result_fold_negative = ff_r_mce_result_fold_negative + ff_a_mce_result_fold_negative))))))))))))

Complete unchanged native tactic proof

All 45 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

45 script commands · 11 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
signed matrix first row components existssigned alternating cofactor fold 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 pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro q
  6. L6
    intro eb
  7. L7
    intro ec
  8. L8
    intro fb
  9. L9
    intro fc
02Establish hrowL10–16

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

  1. L10
    have hrow : ∃ ab. ∃ ac. ∃ db. ∃ dc. MatrixAffineSlice(pb,pc,0,1,ab,ac,S q) ∧ MatrixAffineSlice(nb,nc,0,1,db,dc,S q)Definitions: MatrixAffineSliceOriginal native command in the exact edition
  2. L11
    specialize signed_matrix_first_row_components_exists pb
  3. L12
    specialize signed_matrix_first_row_components_exists pc
  4. L13
    specialize signed_matrix_first_row_components_exists nb
  5. L14
    specialize signed_matrix_first_row_components_exists nc
  6. L15
    specialize signed_matrix_first_row_components_exists q
  7. L16
    exact signed_matrix_first_row_components_exists
03Separate the logical casesL17–21

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

  1. L17
    cases hrow
  2. L18
    cases hrow_witness
  3. L19
    cases hrow_witness_witness
  4. L20
    cases hrow_witness_witness_witness
  5. L21
    cases hrow_witness_witness_witness_witness
04Establish hfoldL22–31

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

  1. L22
    have hfold : ∃ p. ∃ n. SignedAlternatingCofactorFold(x,x1,x2,x3,eb,ec,fb,fc,S q,p,n)Definitions: SignedAlternatingCofactorFoldOriginal native command in the exact edition
  2. L23
    specialize signed_alternating_cofactor_fold_exists x
  3. L24
    specialize signed_alternating_cofactor_fold_exists x1
  4. L25
    specialize signed_alternating_cofactor_fold_exists x2
  5. L26
    specialize signed_alternating_cofactor_fold_exists x3
  6. L27
    specialize signed_alternating_cofactor_fold_exists eb
  7. L28
    specialize signed_alternating_cofactor_fold_exists ec
  8. L29
    specialize signed_alternating_cofactor_fold_exists fb
  9. L30
    specialize signed_alternating_cofactor_fold_exists fc
  10. L31
    specialize signed_alternating_cofactor_fold_exists (S q)
05Use earlier factsL32–32

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

  1. L32
    exact signed_alternating_cofactor_fold_exists
06Separate the logical casesL33–34

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

  1. L33
    cases hfold
  2. L34
    cases hfold_witness
07Construct an explicit witnessL35–40

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

  1. L35
    exists x4
  2. L36
    exists x5
  3. L37
    exists x
  4. L38
    exists x1
  5. L39
    exists x2
  6. L40
    exists x3
08Separate the logical casesL41–41

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

  1. L41
    split
09Use earlier factsL42–42

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

  1. L42
    exact hrow_witness_witness_witness_witness_left
10Separate the logical casesL43–43

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

  1. L43
    split
11Use earlier factsL44–45

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

  1. L44
    exact hrow_witness_witness_witness_witness_right
  2. L45
    exact hfold_witness_witness

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006intro eb
  7. 0007intro ec
  8. 0008intro fb
  9. 0009intro fc
  10. 0010have hrow : exists ab ac db dc. ((forall ff_index_mcp_mce_actual_row_positive ff_source_mcp_mce_actual_row_positive ff_target_mcp_mce_actual_row_positive. (exists mcp_gap_mce_actual_row_positive_bound. mcp_gap_mce_actual_row_positive_bound + S (ff_index_mcp_mce_actual_row_positive) = (S q)) -> (((exists fs_h_mcp_mce_actual_row_positive_source. fs_h_mcp_mce_actual_row_positive_source + S (ff_source_mcp_mce_actual_row_positive) = S ((S ((0) + (1) * ff_index_mcp_mce_actual_row_positive)) * pc)) /\ exists fs_q_mcp_mce_actual_row_positive_source. pb = fs_q_mcp_mce_actual_row_positive_source * S ((S ((0) + (1) * ff_index_mcp_mce_actual_row_positive)) * pc) + (ff_source_mcp_mce_actual_row_positive))) -> (((exists fs_h_mcp_mce_actual_row_positive_target. fs_h_mcp_mce_actual_row_positive_target + S (ff_target_mcp_mce_actual_row_positive) = S ((S (ff_index_mcp_mce_actual_row_positive)) * ac)) /\ exists fs_q_mcp_mce_actual_row_positive_target. ab = fs_q_mcp_mce_actual_row_positive_target * S ((S (ff_index_mcp_mce_actual_row_positive)) * ac) + (ff_target_mcp_mce_actual_row_positive))) -> ff_target_mcp_mce_actual_row_positive = ff_source_mcp_mce_actual_row_positive) /\ (forall ff_index_mcp_mce_actual_row_negative ff_source_mcp_mce_actual_row_negative ff_target_mcp_mce_actual_row_negative. (exists mcp_gap_mce_actual_row_negative_bound. mcp_gap_mce_actual_row_negative_bound + S (ff_index_mcp_mce_actual_row_negative) = (S q)) -> (((exists fs_h_mcp_mce_actual_row_negative_source. fs_h_mcp_mce_actual_row_negative_source + S (ff_source_mcp_mce_actual_row_negative) = S ((S ((0) + (1) * ff_index_mcp_mce_actual_row_negative)) * nc)) /\ exists fs_q_mcp_mce_actual_row_negative_source. nb = fs_q_mcp_mce_actual_row_negative_source * S ((S ((0) + (1) * ff_index_mcp_mce_actual_row_negative)) * nc) + (ff_source_mcp_mce_actual_row_negative))) -> (((exists fs_h_mcp_mce_actual_row_negative_target. fs_h_mcp_mce_actual_row_negative_target + S (ff_target_mcp_mce_actual_row_negative) = S ((S (ff_index_mcp_mce_actual_row_negative)) * dc)) /\ exists fs_q_mcp_mce_actual_row_negative_target. db = fs_q_mcp_mce_actual_row_negative_target * S ((S (ff_index_mcp_mce_actual_row_negative)) * dc) + (ff_target_mcp_mce_actual_row_negative))) -> ff_target_mcp_mce_actual_row_negative = ff_source_mcp_mce_actual_row_negative))
  11. 0011specialize signed_matrix_first_row_components_exists pb
  12. 0012specialize signed_matrix_first_row_components_exists pc
  13. 0013specialize signed_matrix_first_row_components_exists nb
  14. 0014specialize signed_matrix_first_row_components_exists nc
  15. 0015specialize signed_matrix_first_row_components_exists q
  16. 0016exact signed_matrix_first_row_components_exists
  17. 0017cases hrow
  18. 0018cases hrow_witness
  19. 0019cases hrow_witness_witness
  20. 0020cases hrow_witness_witness_witness
  21. 0021cases hrow_witness_witness_witness_witness
  22. 0022have hfold : exists p n. (exists ff_ub_mce_fold_actual_fold ff_uc_mce_fold_actual_fold ff_vb_mce_fold_actual_fold ff_vc_mce_fold_actual_fold. ((forall ff_index_mce_alternating_actual_fold_prefix. (exists ff_gap_mce_actual_fold_prefix_index. ff_gap_mce_actual_fold_prefix_index + S (ff_index_mce_alternating_actual_fold_prefix) = (S q)) -> exists ff_ap_mce_alternating_actual_fold_prefix ff_an_mce_alternating_actual_fold_prefix ff_bp_mce_alternating_actual_fold_prefix ff_bn_mce_alternating_actual_fold_prefix ff_p_mce_alternating_actual_fold_prefix ff_n_mce_alternating_actual_fold_prefix. ((((exists ff_h_mce_actual_fold_prefix_ap. ff_h_mce_actual_fold_prefix_ap + S (ff_ap_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * x1)) /\ exists ff_q_mce_actual_fold_prefix_ap. x = ff_q_mce_actual_fold_prefix_ap * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * x1) + (ff_ap_mce_alternating_actual_fold_prefix))) /\ ((((exists ff_h_mce_actual_fold_prefix_an. ff_h_mce_actual_fold_prefix_an + S (ff_an_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * x3)) /\ exists ff_q_mce_actual_fold_prefix_an. x2 = ff_q_mce_actual_fold_prefix_an * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * x3) + (ff_an_mce_alternating_actual_fold_prefix))) /\ ((((exists ff_h_mce_actual_fold_prefix_bp. ff_h_mce_actual_fold_prefix_bp + S (ff_bp_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ec)) /\ exists ff_q_mce_actual_fold_prefix_bp. eb = ff_q_mce_actual_fold_prefix_bp * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ec) + (ff_bp_mce_alternating_actual_fold_prefix))) /\ ((((exists ff_h_mce_actual_fold_prefix_bn. ff_h_mce_actual_fold_prefix_bn + S (ff_bn_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * fc)) /\ exists ff_q_mce_actual_fold_prefix_bn. fb = ff_q_mce_actual_fold_prefix_bn * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * fc) + (ff_bn_mce_alternating_actual_fold_prefix))) /\ ((((exists ff_h_mce_actual_fold_prefix_positive. ff_h_mce_actual_fold_prefix_positive + S (ff_p_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ff_uc_mce_fold_actual_fold)) /\ exists ff_q_mce_actual_fold_prefix_positive. ff_ub_mce_fold_actual_fold = ff_q_mce_actual_fold_prefix_positive * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ff_uc_mce_fold_actual_fold) + (ff_p_mce_alternating_actual_fold_prefix))) /\ ((((exists ff_h_mce_actual_fold_prefix_negative. ff_h_mce_actual_fold_prefix_negative + S (ff_n_mce_alternating_actual_fold_prefix) = S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ff_vc_mce_fold_actual_fold)) /\ exists ff_q_mce_actual_fold_prefix_negative. ff_vb_mce_fold_actual_fold = ff_q_mce_actual_fold_prefix_negative * S ((S (ff_index_mce_alternating_actual_fold_prefix)) * ff_vc_mce_fold_actual_fold) + (ff_n_mce_alternating_actual_fold_prefix))) /\ (((exists ff_even_mce_term_actual_fold_prefix_term. ff_index_mce_alternating_actual_fold_prefix = 2 * ff_even_mce_term_actual_fold_prefix_term) /\ (ff_p_mce_alternating_actual_fold_prefix = (ff_ap_mce_alternating_actual_fold_prefix) * (ff_bp_mce_alternating_actual_fold_prefix) + (ff_an_mce_alternating_actual_fold_prefix) * (ff_bn_mce_alternating_actual_fold_prefix) /\ ff_n_mce_alternating_actual_fold_prefix = (ff_ap_mce_alternating_actual_fold_prefix) * (ff_bn_mce_alternating_actual_fold_prefix) + (ff_an_mce_alternating_actual_fold_prefix) * (ff_bp_mce_alternating_actual_fold_prefix))) \/ ((exists ff_odd_mce_term_actual_fold_prefix_term. ff_index_mce_alternating_actual_fold_prefix = 2 * ff_odd_mce_term_actual_fold_prefix_term + 1) /\ (ff_p_mce_alternating_actual_fold_prefix = (ff_ap_mce_alternating_actual_fold_prefix) * (ff_bn_mce_alternating_actual_fold_prefix) + (ff_an_mce_alternating_actual_fold_prefix) * (ff_bp_mce_alternating_actual_fold_prefix) /\ ff_n_mce_alternating_actual_fold_prefix = (ff_ap_mce_alternating_actual_fold_prefix) * (ff_bp_mce_alternating_actual_fold_prefix) + (ff_an_mce_alternating_actual_fold_prefix) * (ff_bn_mce_alternating_actual_fold_prefix))))))))))) /\ ((exists ff_u_mce_actual_fold_positive ff_v_mce_actual_fold_positive. ((((exists ff_h_mce_actual_fold_positive_start. ff_h_mce_actual_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_actual_fold_positive)) /\ exists ff_q_mce_actual_fold_positive_start. ff_u_mce_actual_fold_positive = ff_q_mce_actual_fold_positive_start * S ((S (0)) * ff_v_mce_actual_fold_positive) + (0))) /\ ((((exists ff_h_mce_actual_fold_positive_terminal. ff_h_mce_actual_fold_positive_terminal + S (p) = S ((S ((S q))) * ff_v_mce_actual_fold_positive)) /\ exists ff_q_mce_actual_fold_positive_terminal. ff_u_mce_actual_fold_positive = ff_q_mce_actual_fold_positive_terminal * S ((S ((S q))) * ff_v_mce_actual_fold_positive) + (p))) /\ forall ff_i_mce_actual_fold_positive. (exists ff_lt_mce_actual_fold_positive_bound. ff_lt_mce_actual_fold_positive_bound + S ff_i_mce_actual_fold_positive = (S q)) -> exists ff_a_mce_actual_fold_positive ff_r_mce_actual_fold_positive ff_s_mce_actual_fold_positive. ((((exists ff_h_mce_actual_fold_positive_summand. ff_h_mce_actual_fold_positive_summand + S (ff_a_mce_actual_fold_positive) = S ((S (ff_i_mce_actual_fold_positive)) * ff_uc_mce_fold_actual_fold)) /\ exists ff_q_mce_actual_fold_positive_summand. ff_ub_mce_fold_actual_fold = ff_q_mce_actual_fold_positive_summand * S ((S (ff_i_mce_actual_fold_positive)) * ff_uc_mce_fold_actual_fold) + (ff_a_mce_actual_fold_positive))) /\ ((((exists ff_h_mce_actual_fold_positive_partial. ff_h_mce_actual_fold_positive_partial + S (ff_r_mce_actual_fold_positive) = S ((S (ff_i_mce_actual_fold_positive)) * ff_v_mce_actual_fold_positive)) /\ exists ff_q_mce_actual_fold_positive_partial. ff_u_mce_actual_fold_positive = ff_q_mce_actual_fold_positive_partial * S ((S (ff_i_mce_actual_fold_positive)) * ff_v_mce_actual_fold_positive) + (ff_r_mce_actual_fold_positive))) /\ ((((exists ff_h_mce_actual_fold_positive_successor. ff_h_mce_actual_fold_positive_successor + S (ff_s_mce_actual_fold_positive) = S ((S (S ff_i_mce_actual_fold_positive)) * ff_v_mce_actual_fold_positive)) /\ exists ff_q_mce_actual_fold_positive_successor. ff_u_mce_actual_fold_positive = ff_q_mce_actual_fold_positive_successor * S ((S (S ff_i_mce_actual_fold_positive)) * ff_v_mce_actual_fold_positive) + (ff_s_mce_actual_fold_positive))) /\ ff_s_mce_actual_fold_positive = ff_r_mce_actual_fold_positive + ff_a_mce_actual_fold_positive)))))) /\ (exists ff_u_mce_actual_fold_negative ff_v_mce_actual_fold_negative. ((((exists ff_h_mce_actual_fold_negative_start. ff_h_mce_actual_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_actual_fold_negative)) /\ exists ff_q_mce_actual_fold_negative_start. ff_u_mce_actual_fold_negative = ff_q_mce_actual_fold_negative_start * S ((S (0)) * ff_v_mce_actual_fold_negative) + (0))) /\ ((((exists ff_h_mce_actual_fold_negative_terminal. ff_h_mce_actual_fold_negative_terminal + S (n) = S ((S ((S q))) * ff_v_mce_actual_fold_negative)) /\ exists ff_q_mce_actual_fold_negative_terminal. ff_u_mce_actual_fold_negative = ff_q_mce_actual_fold_negative_terminal * S ((S ((S q))) * ff_v_mce_actual_fold_negative) + (n))) /\ forall ff_i_mce_actual_fold_negative. (exists ff_lt_mce_actual_fold_negative_bound. ff_lt_mce_actual_fold_negative_bound + S ff_i_mce_actual_fold_negative = (S q)) -> exists ff_a_mce_actual_fold_negative ff_r_mce_actual_fold_negative ff_s_mce_actual_fold_negative. ((((exists ff_h_mce_actual_fold_negative_summand. ff_h_mce_actual_fold_negative_summand + S (ff_a_mce_actual_fold_negative) = S ((S (ff_i_mce_actual_fold_negative)) * ff_vc_mce_fold_actual_fold)) /\ exists ff_q_mce_actual_fold_negative_summand. ff_vb_mce_fold_actual_fold = ff_q_mce_actual_fold_negative_summand * S ((S (ff_i_mce_actual_fold_negative)) * ff_vc_mce_fold_actual_fold) + (ff_a_mce_actual_fold_negative))) /\ ((((exists ff_h_mce_actual_fold_negative_partial. ff_h_mce_actual_fold_negative_partial + S (ff_r_mce_actual_fold_negative) = S ((S (ff_i_mce_actual_fold_negative)) * ff_v_mce_actual_fold_negative)) /\ exists ff_q_mce_actual_fold_negative_partial. ff_u_mce_actual_fold_negative = ff_q_mce_actual_fold_negative_partial * S ((S (ff_i_mce_actual_fold_negative)) * ff_v_mce_actual_fold_negative) + (ff_r_mce_actual_fold_negative))) /\ ((((exists ff_h_mce_actual_fold_negative_successor. ff_h_mce_actual_fold_negative_successor + S (ff_s_mce_actual_fold_negative) = S ((S (S ff_i_mce_actual_fold_negative)) * ff_v_mce_actual_fold_negative)) /\ exists ff_q_mce_actual_fold_negative_successor. ff_u_mce_actual_fold_negative = ff_q_mce_actual_fold_negative_successor * S ((S (S ff_i_mce_actual_fold_negative)) * ff_v_mce_actual_fold_negative) + (ff_s_mce_actual_fold_negative))) /\ ff_s_mce_actual_fold_negative = ff_r_mce_actual_fold_negative + ff_a_mce_actual_fold_negative)))))))))
  23. 0023specialize signed_alternating_cofactor_fold_exists x
  24. 0024specialize signed_alternating_cofactor_fold_exists x1
  25. 0025specialize signed_alternating_cofactor_fold_exists x2
  26. 0026specialize signed_alternating_cofactor_fold_exists x3
  27. 0027specialize signed_alternating_cofactor_fold_exists eb
  28. 0028specialize signed_alternating_cofactor_fold_exists ec
  29. 0029specialize signed_alternating_cofactor_fold_exists fb
  30. 0030specialize signed_alternating_cofactor_fold_exists fc
  31. 0031specialize signed_alternating_cofactor_fold_exists (S q)
  32. 0032exact signed_alternating_cofactor_fold_exists
  33. 0033cases hfold
  34. 0034cases hfold_witness
  35. 0035exists x4
  36. 0036exists x5
  37. 0037exists x
  38. 0038exists x1
  39. 0039exists x2
  40. 0040exists x3
  41. 0041split
  42. 0042exact hrow_witness_witness_witness_witness_left
  43. 0043split
  44. 0044exact hrow_witness_witness_witness_witness_right
  45. 0045exact hfold_witness_witness