CE0018

signed_alternating_cofactor_fold_functional

Both components of an arbitrary finite signed alternating Laplace cofactor fold are independent of every beta-coding and finite-sum witness.

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

∀ ab. ∀ ac. ∀ db. ∀ dc. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∀ l. ∀ p. ∀ n. ∀ r. ∀ s. SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,p,n) → SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,r,s) → p = r ∧ n = s

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

Definition DAG

SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,p,n) · 2

Actual proof prerequisites

beta_at_exists · checked external prerequisitebeta_sum_transport_prefix · checked external prerequisitebeta_sum_functional · checked external prerequisitesigned_alternating_product_prefix_pointwise_functional
Original expanded first-order statement 
forall ab ac db dc eb ec fb fc l p n r s. (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))))))))) -> (exists ff_ub_mce_fold_other ff_uc_mce_fold_other ff_vb_mce_fold_other ff_vc_mce_fold_other. ((forall ff_index_mce_alternating_other_prefix. (exists ff_gap_mce_other_prefix_index. ff_gap_mce_other_prefix_index + S (ff_index_mce_alternating_other_prefix) = (l)) -> exists ff_ap_mce_alternating_other_prefix ff_an_mce_alternating_other_prefix ff_bp_mce_alternating_other_prefix ff_bn_mce_alternating_other_prefix ff_p_mce_alternating_other_prefix ff_n_mce_alternating_other_prefix. ((((exists ff_h_mce_other_prefix_ap. ff_h_mce_other_prefix_ap + S (ff_ap_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ac)) /\ exists ff_q_mce_other_prefix_ap. ab = ff_q_mce_other_prefix_ap * S ((S (ff_index_mce_alternating_other_prefix)) * ac) + (ff_ap_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_an. ff_h_mce_other_prefix_an + S (ff_an_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * dc)) /\ exists ff_q_mce_other_prefix_an. db = ff_q_mce_other_prefix_an * S ((S (ff_index_mce_alternating_other_prefix)) * dc) + (ff_an_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_bp. ff_h_mce_other_prefix_bp + S (ff_bp_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ec)) /\ exists ff_q_mce_other_prefix_bp. eb = ff_q_mce_other_prefix_bp * S ((S (ff_index_mce_alternating_other_prefix)) * ec) + (ff_bp_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_bn. ff_h_mce_other_prefix_bn + S (ff_bn_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * fc)) /\ exists ff_q_mce_other_prefix_bn. fb = ff_q_mce_other_prefix_bn * S ((S (ff_index_mce_alternating_other_prefix)) * fc) + (ff_bn_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_positive. ff_h_mce_other_prefix_positive + S (ff_p_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ff_uc_mce_fold_other)) /\ exists ff_q_mce_other_prefix_positive. ff_ub_mce_fold_other = ff_q_mce_other_prefix_positive * S ((S (ff_index_mce_alternating_other_prefix)) * ff_uc_mce_fold_other) + (ff_p_mce_alternating_other_prefix))) /\ ((((exists ff_h_mce_other_prefix_negative. ff_h_mce_other_prefix_negative + S (ff_n_mce_alternating_other_prefix) = S ((S (ff_index_mce_alternating_other_prefix)) * ff_vc_mce_fold_other)) /\ exists ff_q_mce_other_prefix_negative. ff_vb_mce_fold_other = ff_q_mce_other_prefix_negative * S ((S (ff_index_mce_alternating_other_prefix)) * ff_vc_mce_fold_other) + (ff_n_mce_alternating_other_prefix))) /\ (((exists ff_even_mce_term_other_prefix_term. ff_index_mce_alternating_other_prefix = 2 * ff_even_mce_term_other_prefix_term) /\ (ff_p_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) /\ ff_n_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix))) \/ ((exists ff_odd_mce_term_other_prefix_term. ff_index_mce_alternating_other_prefix = 2 * ff_odd_mce_term_other_prefix_term + 1) /\ (ff_p_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) /\ ff_n_mce_alternating_other_prefix = (ff_ap_mce_alternating_other_prefix) * (ff_bp_mce_alternating_other_prefix) + (ff_an_mce_alternating_other_prefix) * (ff_bn_mce_alternating_other_prefix))))))))))) /\ ((exists ff_u_mce_other_positive ff_v_mce_other_positive. ((((exists ff_h_mce_other_positive_start. ff_h_mce_other_positive_start + S (0) = S ((S (0)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_start. ff_u_mce_other_positive = ff_q_mce_other_positive_start * S ((S (0)) * ff_v_mce_other_positive) + (0))) /\ ((((exists ff_h_mce_other_positive_terminal. ff_h_mce_other_positive_terminal + S (r) = S ((S (l)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_terminal. ff_u_mce_other_positive = ff_q_mce_other_positive_terminal * S ((S (l)) * ff_v_mce_other_positive) + (r))) /\ forall ff_i_mce_other_positive. (exists ff_lt_mce_other_positive_bound. ff_lt_mce_other_positive_bound + S ff_i_mce_other_positive = l) -> exists ff_a_mce_other_positive ff_r_mce_other_positive ff_s_mce_other_positive. ((((exists ff_h_mce_other_positive_summand. ff_h_mce_other_positive_summand + S (ff_a_mce_other_positive) = S ((S (ff_i_mce_other_positive)) * ff_uc_mce_fold_other)) /\ exists ff_q_mce_other_positive_summand. ff_ub_mce_fold_other = ff_q_mce_other_positive_summand * S ((S (ff_i_mce_other_positive)) * ff_uc_mce_fold_other) + (ff_a_mce_other_positive))) /\ ((((exists ff_h_mce_other_positive_partial. ff_h_mce_other_positive_partial + S (ff_r_mce_other_positive) = S ((S (ff_i_mce_other_positive)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_partial. ff_u_mce_other_positive = ff_q_mce_other_positive_partial * S ((S (ff_i_mce_other_positive)) * ff_v_mce_other_positive) + (ff_r_mce_other_positive))) /\ ((((exists ff_h_mce_other_positive_successor. ff_h_mce_other_positive_successor + S (ff_s_mce_other_positive) = S ((S (S ff_i_mce_other_positive)) * ff_v_mce_other_positive)) /\ exists ff_q_mce_other_positive_successor. ff_u_mce_other_positive = ff_q_mce_other_positive_successor * S ((S (S ff_i_mce_other_positive)) * ff_v_mce_other_positive) + (ff_s_mce_other_positive))) /\ ff_s_mce_other_positive = ff_r_mce_other_positive + ff_a_mce_other_positive)))))) /\ (exists ff_u_mce_other_negative ff_v_mce_other_negative. ((((exists ff_h_mce_other_negative_start. ff_h_mce_other_negative_start + S (0) = S ((S (0)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_start. ff_u_mce_other_negative = ff_q_mce_other_negative_start * S ((S (0)) * ff_v_mce_other_negative) + (0))) /\ ((((exists ff_h_mce_other_negative_terminal. ff_h_mce_other_negative_terminal + S (s) = S ((S (l)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_terminal. ff_u_mce_other_negative = ff_q_mce_other_negative_terminal * S ((S (l)) * ff_v_mce_other_negative) + (s))) /\ forall ff_i_mce_other_negative. (exists ff_lt_mce_other_negative_bound. ff_lt_mce_other_negative_bound + S ff_i_mce_other_negative = l) -> exists ff_a_mce_other_negative ff_r_mce_other_negative ff_s_mce_other_negative. ((((exists ff_h_mce_other_negative_summand. ff_h_mce_other_negative_summand + S (ff_a_mce_other_negative) = S ((S (ff_i_mce_other_negative)) * ff_vc_mce_fold_other)) /\ exists ff_q_mce_other_negative_summand. ff_vb_mce_fold_other = ff_q_mce_other_negative_summand * S ((S (ff_i_mce_other_negative)) * ff_vc_mce_fold_other) + (ff_a_mce_other_negative))) /\ ((((exists ff_h_mce_other_negative_partial. ff_h_mce_other_negative_partial + S (ff_r_mce_other_negative) = S ((S (ff_i_mce_other_negative)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_partial. ff_u_mce_other_negative = ff_q_mce_other_negative_partial * S ((S (ff_i_mce_other_negative)) * ff_v_mce_other_negative) + (ff_r_mce_other_negative))) /\ ((((exists ff_h_mce_other_negative_successor. ff_h_mce_other_negative_successor + S (ff_s_mce_other_negative) = S ((S (S ff_i_mce_other_negative)) * ff_v_mce_other_negative)) /\ exists ff_q_mce_other_negative_successor. ff_u_mce_other_negative = ff_q_mce_other_negative_successor * S ((S (S ff_i_mce_other_negative)) * ff_v_mce_other_negative) + (ff_s_mce_other_negative))) /\ ff_s_mce_other_negative = ff_r_mce_other_negative + ff_a_mce_other_negative))))))))) -> (p = r /\ n = s)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

176 script commands · 37 reading checkpoints · 10 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 (1)
signed alternating product prefix pointwise functional

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 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
  10. L10
    intro p
02Fix variables and assumptionsL11–15

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

  1. L11
    intro n
  2. L12
    intro r
  3. L13
    intro s
  4. L14
    intro hfirst
  5. L15
    intro hsecond
03Separate the logical casesL16–25

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

  1. L16
    cases hfirst
  2. L17
    cases hfirst_witness
  3. L18
    cases hfirst_witness_witness
  4. L19
    cases hfirst_witness_witness_witness
  5. L20
    cases hfirst_witness_witness_witness_witness
  6. L21
    cases hfirst_witness_witness_witness_witness_right
  7. L22
    cases hsecond
  8. L23
    cases hsecond_witness
  9. L24
    cases hsecond_witness_witness
  10. L25
    cases hsecond_witness_witness_witness
04Separate the logical casesL26–27

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

  1. L26
    cases hsecond_witness_witness_witness_witness
  2. L27
    cases hsecond_witness_witness_witness_witness_right
05Establish htransport_positiveL28–37

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

  1. L28
    have htransport_positive : Sum(x4,x5,l,p)Definitions: SumOriginal native command in the exact edition
  2. L29
    specialize beta_sum_transport_prefix x
  3. L30
    specialize beta_sum_transport_prefix x1
  4. L31
    specialize beta_sum_transport_prefix x4
  5. L32
    specialize beta_sum_transport_prefix x5
  6. L33
    specialize beta_sum_transport_prefix l
  7. L34
    specialize beta_sum_transport_prefix p
  8. L35
    apply beta_sum_transport_prefix
  9. L36
    exact hfirst_witness_witness_witness_witness_right_left
  10. L37
    intro i
06Fix variables and assumptionsL38–40

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

  1. L38
    intro a
  2. L39
    intro hi
  3. L40
    intro ha
07Establish holdotherL41–45

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

  1. L41
    have holdother : exists z. (((exists ff_h_mce_transport_old_other_p. ff_h_mce_transport_old_other_p + S (z) = S ((S (i)) * x3)) /\ exists ff_q_mce_transport_old_other_p. x2 = ff_q_mce_transport_old_other_p * S ((S (i)) * x3) + (z)))
  2. L42
    specialize beta_at_exists x2
  3. L43
    specialize beta_at_exists x3
  4. L44
    specialize beta_at_exists i
  5. L45
    exact beta_at_exists
08Separate the logical casesL46–46

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

  1. L46
    cases holdother
09Establish hnewpositiveL47–51

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

  1. L47
    have hnewpositive : exists z. (((exists ff_h_mce_transport_new_positive_p. ff_h_mce_transport_new_positive_p + S (z) = S ((S (i)) * x5)) /\ exists ff_q_mce_transport_new_positive_p. x4 = ff_q_mce_transport_new_positive_p * S ((S (i)) * x5) + (z)))
  2. L48
    specialize beta_at_exists x4
  3. L49
    specialize beta_at_exists x5
  4. L50
    specialize beta_at_exists i
  5. L51
    exact beta_at_exists
10Separate the logical casesL52–52

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

  1. L52
    cases hnewpositive
11Establish hnewnegativeL53–57

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

  1. L53
    have hnewnegative : exists z. (((exists ff_h_mce_transport_new_negative_p. ff_h_mce_transport_new_negative_p + S (z) = S ((S (i)) * x7)) /\ exists ff_q_mce_transport_new_negative_p. x6 = ff_q_mce_transport_new_negative_p * S ((S (i)) * x7) + (z)))
  2. L54
    specialize beta_at_exists x6
  3. L55
    specialize beta_at_exists x7
  4. L56
    specialize beta_at_exists i
  5. L57
    exact beta_at_exists
12Separate the logical casesL58–58

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

  1. L58
    cases hnewnegative
13Establish hequalL59–68

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

  1. L59
    have hequal : a = x9 /\ x8 = x10
  2. L60
    specialize signed_alternating_product_prefix_pointwise_functional ab
  3. L61
    specialize signed_alternating_product_prefix_pointwise_functional ac
  4. L62
    specialize signed_alternating_product_prefix_pointwise_functional db
  5. L63
    specialize signed_alternating_product_prefix_pointwise_functional dc
  6. L64
    specialize signed_alternating_product_prefix_pointwise_functional eb
  7. L65
    specialize signed_alternating_product_prefix_pointwise_functional ec
  8. L66
    specialize signed_alternating_product_prefix_pointwise_functional fb
  9. L67
    specialize signed_alternating_product_prefix_pointwise_functional fc
  10. L68
    specialize signed_alternating_product_prefix_pointwise_functional x
14Use earlier factsL69–78

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

  1. L69
    specialize signed_alternating_product_prefix_pointwise_functional x1
  2. L70
    specialize signed_alternating_product_prefix_pointwise_functional x2
  3. L71
    specialize signed_alternating_product_prefix_pointwise_functional x3
  4. L72
    specialize signed_alternating_product_prefix_pointwise_functional x4
  5. L73
    specialize signed_alternating_product_prefix_pointwise_functional x5
  6. L74
    specialize signed_alternating_product_prefix_pointwise_functional x6
  7. L75
    specialize signed_alternating_product_prefix_pointwise_functional x7
  8. L76
    specialize signed_alternating_product_prefix_pointwise_functional l
  9. L77
    specialize signed_alternating_product_prefix_pointwise_functional i
  10. L78
    specialize signed_alternating_product_prefix_pointwise_functional a
15Use earlier factsL79–88

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

  1. L79
    specialize signed_alternating_product_prefix_pointwise_functional x8
  2. L80
    specialize signed_alternating_product_prefix_pointwise_functional x9
  3. L81
    specialize signed_alternating_product_prefix_pointwise_functional x10
  4. L82
    apply signed_alternating_product_prefix_pointwise_functional
  5. L83
    exact hfirst_witness_witness_witness_witness_left
  6. L84
    exact hsecond_witness_witness_witness_witness_left
  7. L85
    exact hi
  8. L86
    exact ha
  9. L87
    exact holdother_witness
  10. L88
    exact hnewpositive_witness
16Use earlier factsL89–89

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

  1. L89
    exact hnewnegative_witness
17Separate the logical casesL90–90

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

  1. L90
    cases hequal
18Calculate and transport equalitiesL91–92

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L91
    rewrite hequal_left
  2. L92
    rewrite hequal_left
19Use earlier factsL93–93

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

  1. L93
    exact hnewpositive_witness
20Establish htransport_negativeL94–103

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

  1. L94
    have htransport_negative : Sum(x6,x7,l,n)Definitions: SumOriginal native command in the exact edition
  2. L95
    specialize beta_sum_transport_prefix x2
  3. L96
    specialize beta_sum_transport_prefix x3
  4. L97
    specialize beta_sum_transport_prefix x6
  5. L98
    specialize beta_sum_transport_prefix x7
  6. L99
    specialize beta_sum_transport_prefix l
  7. L100
    specialize beta_sum_transport_prefix n
  8. L101
    apply beta_sum_transport_prefix
  9. L102
    exact hfirst_witness_witness_witness_witness_right_right
  10. L103
    intro i
21Fix variables and assumptionsL104–106

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

  1. L104
    intro a
  2. L105
    intro hi
  3. L106
    intro ha
22Establish holdotherL107–111

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

  1. L107
    have holdother : exists z. (((exists ff_h_mce_transport_old_other_n. ff_h_mce_transport_old_other_n + S (z) = S ((S (i)) * x1)) /\ exists ff_q_mce_transport_old_other_n. x = ff_q_mce_transport_old_other_n * S ((S (i)) * x1) + (z)))
  2. L108
    specialize beta_at_exists x
  3. L109
    specialize beta_at_exists x1
  4. L110
    specialize beta_at_exists i
  5. L111
    exact beta_at_exists
23Separate the logical casesL112–112

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

  1. L112
    cases holdother
24Establish hnewpositiveL113–117

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

  1. L113
    have hnewpositive : exists z. (((exists ff_h_mce_transport_new_positive_n. ff_h_mce_transport_new_positive_n + S (z) = S ((S (i)) * x5)) /\ exists ff_q_mce_transport_new_positive_n. x4 = ff_q_mce_transport_new_positive_n * S ((S (i)) * x5) + (z)))
  2. L114
    specialize beta_at_exists x4
  3. L115
    specialize beta_at_exists x5
  4. L116
    specialize beta_at_exists i
  5. L117
    exact beta_at_exists
25Separate the logical casesL118–118

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

  1. L118
    cases hnewpositive
26Establish hnewnegativeL119–123

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

  1. L119
    have hnewnegative : exists z. (((exists ff_h_mce_transport_new_negative_n. ff_h_mce_transport_new_negative_n + S (z) = S ((S (i)) * x7)) /\ exists ff_q_mce_transport_new_negative_n. x6 = ff_q_mce_transport_new_negative_n * S ((S (i)) * x7) + (z)))
  2. L120
    specialize beta_at_exists x6
  3. L121
    specialize beta_at_exists x7
  4. L122
    specialize beta_at_exists i
  5. L123
    exact beta_at_exists
27Separate the logical casesL124–124

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

  1. L124
    cases hnewnegative
28Establish hequalL125–134

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

  1. L125
    have hequal : x8 = x9 /\ a = x10
  2. L126
    specialize signed_alternating_product_prefix_pointwise_functional ab
  3. L127
    specialize signed_alternating_product_prefix_pointwise_functional ac
  4. L128
    specialize signed_alternating_product_prefix_pointwise_functional db
  5. L129
    specialize signed_alternating_product_prefix_pointwise_functional dc
  6. L130
    specialize signed_alternating_product_prefix_pointwise_functional eb
  7. L131
    specialize signed_alternating_product_prefix_pointwise_functional ec
  8. L132
    specialize signed_alternating_product_prefix_pointwise_functional fb
  9. L133
    specialize signed_alternating_product_prefix_pointwise_functional fc
  10. L134
    specialize signed_alternating_product_prefix_pointwise_functional x
29Use earlier factsL135–144

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

  1. L135
    specialize signed_alternating_product_prefix_pointwise_functional x1
  2. L136
    specialize signed_alternating_product_prefix_pointwise_functional x2
  3. L137
    specialize signed_alternating_product_prefix_pointwise_functional x3
  4. L138
    specialize signed_alternating_product_prefix_pointwise_functional x4
  5. L139
    specialize signed_alternating_product_prefix_pointwise_functional x5
  6. L140
    specialize signed_alternating_product_prefix_pointwise_functional x6
  7. L141
    specialize signed_alternating_product_prefix_pointwise_functional x7
  8. L142
    specialize signed_alternating_product_prefix_pointwise_functional l
  9. L143
    specialize signed_alternating_product_prefix_pointwise_functional i
  10. L144
    specialize signed_alternating_product_prefix_pointwise_functional x8
30Use earlier factsL145–154

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

  1. L145
    specialize signed_alternating_product_prefix_pointwise_functional a
  2. L146
    specialize signed_alternating_product_prefix_pointwise_functional x9
  3. L147
    specialize signed_alternating_product_prefix_pointwise_functional x10
  4. L148
    apply signed_alternating_product_prefix_pointwise_functional
  5. L149
    exact hfirst_witness_witness_witness_witness_left
  6. L150
    exact hsecond_witness_witness_witness_witness_left
  7. L151
    exact hi
  8. L152
    exact holdother_witness
  9. L153
    exact ha
  10. L154
    exact hnewpositive_witness
31Use earlier factsL155–155

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

  1. L155
    exact hnewnegative_witness
32Separate the logical casesL156–156

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

  1. L156
    cases hequal
33Calculate and transport equalitiesL157–158

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L157
    rewrite hequal_right
  2. L158
    rewrite hequal_right
34Use earlier factsL159–159

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

  1. L159
    exact hnewnegative_witness
35Separate the logical casesL160–160

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

  1. L160
    split
36Use earlier factsL161–170

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

  1. L161
    specialize beta_sum_functional x4
  2. L162
    specialize beta_sum_functional x5
  3. L163
    specialize beta_sum_functional l
  4. L164
    specialize beta_sum_functional p
  5. L165
    specialize beta_sum_functional r
  6. L166
    apply beta_sum_functional
  7. L167
    exact htransport_positive
  8. L168
    exact hsecond_witness_witness_witness_witness_right_left
  9. L169
    specialize beta_sum_functional x6
  10. L170
    specialize beta_sum_functional x7
37Use earlier factsL171–176

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

  1. L171
    specialize beta_sum_functional l
  2. L172
    specialize beta_sum_functional n
  3. L173
    specialize beta_sum_functional s
  4. L174
    apply beta_sum_functional
  5. L175
    exact htransport_negative
  6. L176
    exact hsecond_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 176 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. 0010intro p
  11. 0011intro n
  12. 0012intro r
  13. 0013intro s
  14. 0014intro hfirst
  15. 0015intro hsecond
  16. 0016cases hfirst
  17. 0017cases hfirst_witness
  18. 0018cases hfirst_witness_witness
  19. 0019cases hfirst_witness_witness_witness
  20. 0020cases hfirst_witness_witness_witness_witness
  21. 0021cases hfirst_witness_witness_witness_witness_right
  22. 0022cases hsecond
  23. 0023cases hsecond_witness
  24. 0024cases hsecond_witness_witness
  25. 0025cases hsecond_witness_witness_witness
  26. 0026cases hsecond_witness_witness_witness_witness
  27. 0027cases hsecond_witness_witness_witness_witness_right
  28. 0028have htransport_positive : (exists ff_u_mce_transport_positive ff_v_mce_transport_positive. ((((exists ff_h_mce_transport_positive_start. ff_h_mce_transport_positive_start + S (0) = S ((S (0)) * ff_v_mce_transport_positive)) /\ exists ff_q_mce_transport_positive_start. ff_u_mce_transport_positive = ff_q_mce_transport_positive_start * S ((S (0)) * ff_v_mce_transport_positive) + (0))) /\ ((((exists ff_h_mce_transport_positive_terminal. ff_h_mce_transport_positive_terminal + S (p) = S ((S (l)) * ff_v_mce_transport_positive)) /\ exists ff_q_mce_transport_positive_terminal. ff_u_mce_transport_positive = ff_q_mce_transport_positive_terminal * S ((S (l)) * ff_v_mce_transport_positive) + (p))) /\ forall ff_i_mce_transport_positive. (exists ff_lt_mce_transport_positive_bound. ff_lt_mce_transport_positive_bound + S ff_i_mce_transport_positive = l) -> exists ff_a_mce_transport_positive ff_r_mce_transport_positive ff_s_mce_transport_positive. ((((exists ff_h_mce_transport_positive_summand. ff_h_mce_transport_positive_summand + S (ff_a_mce_transport_positive) = S ((S (ff_i_mce_transport_positive)) * x5)) /\ exists ff_q_mce_transport_positive_summand. x4 = ff_q_mce_transport_positive_summand * S ((S (ff_i_mce_transport_positive)) * x5) + (ff_a_mce_transport_positive))) /\ ((((exists ff_h_mce_transport_positive_partial. ff_h_mce_transport_positive_partial + S (ff_r_mce_transport_positive) = S ((S (ff_i_mce_transport_positive)) * ff_v_mce_transport_positive)) /\ exists ff_q_mce_transport_positive_partial. ff_u_mce_transport_positive = ff_q_mce_transport_positive_partial * S ((S (ff_i_mce_transport_positive)) * ff_v_mce_transport_positive) + (ff_r_mce_transport_positive))) /\ ((((exists ff_h_mce_transport_positive_successor. ff_h_mce_transport_positive_successor + S (ff_s_mce_transport_positive) = S ((S (S ff_i_mce_transport_positive)) * ff_v_mce_transport_positive)) /\ exists ff_q_mce_transport_positive_successor. ff_u_mce_transport_positive = ff_q_mce_transport_positive_successor * S ((S (S ff_i_mce_transport_positive)) * ff_v_mce_transport_positive) + (ff_s_mce_transport_positive))) /\ ff_s_mce_transport_positive = ff_r_mce_transport_positive + ff_a_mce_transport_positive))))))
  29. 0029specialize beta_sum_transport_prefix x
  30. 0030specialize beta_sum_transport_prefix x1
  31. 0031specialize beta_sum_transport_prefix x4
  32. 0032specialize beta_sum_transport_prefix x5
  33. 0033specialize beta_sum_transport_prefix l
  34. 0034specialize beta_sum_transport_prefix p
  35. 0035apply beta_sum_transport_prefix
  36. 0036exact hfirst_witness_witness_witness_witness_right_left
  37. 0037intro i
  38. 0038intro a
  39. 0039intro hi
  40. 0040intro ha
  41. 0041have holdother : exists z. (((exists ff_h_mce_transport_old_other_p. ff_h_mce_transport_old_other_p + S (z) = S ((S (i)) * x3)) /\ exists ff_q_mce_transport_old_other_p. x2 = ff_q_mce_transport_old_other_p * S ((S (i)) * x3) + (z)))
  42. 0042specialize beta_at_exists x2
  43. 0043specialize beta_at_exists x3
  44. 0044specialize beta_at_exists i
  45. 0045exact beta_at_exists
  46. 0046cases holdother
  47. 0047have hnewpositive : exists z. (((exists ff_h_mce_transport_new_positive_p. ff_h_mce_transport_new_positive_p + S (z) = S ((S (i)) * x5)) /\ exists ff_q_mce_transport_new_positive_p. x4 = ff_q_mce_transport_new_positive_p * S ((S (i)) * x5) + (z)))
  48. 0048specialize beta_at_exists x4
  49. 0049specialize beta_at_exists x5
  50. 0050specialize beta_at_exists i
  51. 0051exact beta_at_exists
  52. 0052cases hnewpositive
  53. 0053have hnewnegative : exists z. (((exists ff_h_mce_transport_new_negative_p. ff_h_mce_transport_new_negative_p + S (z) = S ((S (i)) * x7)) /\ exists ff_q_mce_transport_new_negative_p. x6 = ff_q_mce_transport_new_negative_p * S ((S (i)) * x7) + (z)))
  54. 0054specialize beta_at_exists x6
  55. 0055specialize beta_at_exists x7
  56. 0056specialize beta_at_exists i
  57. 0057exact beta_at_exists
  58. 0058cases hnewnegative
  59. 0059have hequal : a = x9 /\ x8 = x10
  60. 0060specialize signed_alternating_product_prefix_pointwise_functional ab
  61. 0061specialize signed_alternating_product_prefix_pointwise_functional ac
  62. 0062specialize signed_alternating_product_prefix_pointwise_functional db
  63. 0063specialize signed_alternating_product_prefix_pointwise_functional dc
  64. 0064specialize signed_alternating_product_prefix_pointwise_functional eb
  65. 0065specialize signed_alternating_product_prefix_pointwise_functional ec
  66. 0066specialize signed_alternating_product_prefix_pointwise_functional fb
  67. 0067specialize signed_alternating_product_prefix_pointwise_functional fc
  68. 0068specialize signed_alternating_product_prefix_pointwise_functional x
  69. 0069specialize signed_alternating_product_prefix_pointwise_functional x1
  70. 0070specialize signed_alternating_product_prefix_pointwise_functional x2
  71. 0071specialize signed_alternating_product_prefix_pointwise_functional x3
  72. 0072specialize signed_alternating_product_prefix_pointwise_functional x4
  73. 0073specialize signed_alternating_product_prefix_pointwise_functional x5
  74. 0074specialize signed_alternating_product_prefix_pointwise_functional x6
  75. 0075specialize signed_alternating_product_prefix_pointwise_functional x7
  76. 0076specialize signed_alternating_product_prefix_pointwise_functional l
  77. 0077specialize signed_alternating_product_prefix_pointwise_functional i
  78. 0078specialize signed_alternating_product_prefix_pointwise_functional a
  79. 0079specialize signed_alternating_product_prefix_pointwise_functional x8
  80. 0080specialize signed_alternating_product_prefix_pointwise_functional x9
  81. 0081specialize signed_alternating_product_prefix_pointwise_functional x10
  82. 0082apply signed_alternating_product_prefix_pointwise_functional
  83. 0083exact hfirst_witness_witness_witness_witness_left
  84. 0084exact hsecond_witness_witness_witness_witness_left
  85. 0085exact hi
  86. 0086exact ha
  87. 0087exact holdother_witness
  88. 0088exact hnewpositive_witness
  89. 0089exact hnewnegative_witness
  90. 0090cases hequal
  91. 0091rewrite hequal_left
  92. 0092rewrite hequal_left
  93. 0093exact hnewpositive_witness
  94. 0094have htransport_negative : (exists ff_u_mce_transport_negative ff_v_mce_transport_negative. ((((exists ff_h_mce_transport_negative_start. ff_h_mce_transport_negative_start + S (0) = S ((S (0)) * ff_v_mce_transport_negative)) /\ exists ff_q_mce_transport_negative_start. ff_u_mce_transport_negative = ff_q_mce_transport_negative_start * S ((S (0)) * ff_v_mce_transport_negative) + (0))) /\ ((((exists ff_h_mce_transport_negative_terminal. ff_h_mce_transport_negative_terminal + S (n) = S ((S (l)) * ff_v_mce_transport_negative)) /\ exists ff_q_mce_transport_negative_terminal. ff_u_mce_transport_negative = ff_q_mce_transport_negative_terminal * S ((S (l)) * ff_v_mce_transport_negative) + (n))) /\ forall ff_i_mce_transport_negative. (exists ff_lt_mce_transport_negative_bound. ff_lt_mce_transport_negative_bound + S ff_i_mce_transport_negative = l) -> exists ff_a_mce_transport_negative ff_r_mce_transport_negative ff_s_mce_transport_negative. ((((exists ff_h_mce_transport_negative_summand. ff_h_mce_transport_negative_summand + S (ff_a_mce_transport_negative) = S ((S (ff_i_mce_transport_negative)) * x7)) /\ exists ff_q_mce_transport_negative_summand. x6 = ff_q_mce_transport_negative_summand * S ((S (ff_i_mce_transport_negative)) * x7) + (ff_a_mce_transport_negative))) /\ ((((exists ff_h_mce_transport_negative_partial. ff_h_mce_transport_negative_partial + S (ff_r_mce_transport_negative) = S ((S (ff_i_mce_transport_negative)) * ff_v_mce_transport_negative)) /\ exists ff_q_mce_transport_negative_partial. ff_u_mce_transport_negative = ff_q_mce_transport_negative_partial * S ((S (ff_i_mce_transport_negative)) * ff_v_mce_transport_negative) + (ff_r_mce_transport_negative))) /\ ((((exists ff_h_mce_transport_negative_successor. ff_h_mce_transport_negative_successor + S (ff_s_mce_transport_negative) = S ((S (S ff_i_mce_transport_negative)) * ff_v_mce_transport_negative)) /\ exists ff_q_mce_transport_negative_successor. ff_u_mce_transport_negative = ff_q_mce_transport_negative_successor * S ((S (S ff_i_mce_transport_negative)) * ff_v_mce_transport_negative) + (ff_s_mce_transport_negative))) /\ ff_s_mce_transport_negative = ff_r_mce_transport_negative + ff_a_mce_transport_negative))))))
  95. 0095specialize beta_sum_transport_prefix x2
  96. 0096specialize beta_sum_transport_prefix x3
  97. 0097specialize beta_sum_transport_prefix x6
  98. 0098specialize beta_sum_transport_prefix x7
  99. 0099specialize beta_sum_transport_prefix l
  100. 0100specialize beta_sum_transport_prefix n
  101. 0101apply beta_sum_transport_prefix
  102. 0102exact hfirst_witness_witness_witness_witness_right_right
  103. 0103intro i
  104. 0104intro a
  105. 0105intro hi
  106. 0106intro ha
  107. 0107have holdother : exists z. (((exists ff_h_mce_transport_old_other_n. ff_h_mce_transport_old_other_n + S (z) = S ((S (i)) * x1)) /\ exists ff_q_mce_transport_old_other_n. x = ff_q_mce_transport_old_other_n * S ((S (i)) * x1) + (z)))
  108. 0108specialize beta_at_exists x
  109. 0109specialize beta_at_exists x1
  110. 0110specialize beta_at_exists i
  111. 0111exact beta_at_exists
  112. 0112cases holdother
  113. 0113have hnewpositive : exists z. (((exists ff_h_mce_transport_new_positive_n. ff_h_mce_transport_new_positive_n + S (z) = S ((S (i)) * x5)) /\ exists ff_q_mce_transport_new_positive_n. x4 = ff_q_mce_transport_new_positive_n * S ((S (i)) * x5) + (z)))
  114. 0114specialize beta_at_exists x4
  115. 0115specialize beta_at_exists x5
  116. 0116specialize beta_at_exists i
  117. 0117exact beta_at_exists
  118. 0118cases hnewpositive
  119. 0119have hnewnegative : exists z. (((exists ff_h_mce_transport_new_negative_n. ff_h_mce_transport_new_negative_n + S (z) = S ((S (i)) * x7)) /\ exists ff_q_mce_transport_new_negative_n. x6 = ff_q_mce_transport_new_negative_n * S ((S (i)) * x7) + (z)))
  120. 0120specialize beta_at_exists x6
  121. 0121specialize beta_at_exists x7
  122. 0122specialize beta_at_exists i
  123. 0123exact beta_at_exists
  124. 0124cases hnewnegative
  125. 0125have hequal : x8 = x9 /\ a = x10
  126. 0126specialize signed_alternating_product_prefix_pointwise_functional ab
  127. 0127specialize signed_alternating_product_prefix_pointwise_functional ac
  128. 0128specialize signed_alternating_product_prefix_pointwise_functional db
  129. 0129specialize signed_alternating_product_prefix_pointwise_functional dc
  130. 0130specialize signed_alternating_product_prefix_pointwise_functional eb
  131. 0131specialize signed_alternating_product_prefix_pointwise_functional ec
  132. 0132specialize signed_alternating_product_prefix_pointwise_functional fb
  133. 0133specialize signed_alternating_product_prefix_pointwise_functional fc
  134. 0134specialize signed_alternating_product_prefix_pointwise_functional x
  135. 0135specialize signed_alternating_product_prefix_pointwise_functional x1
  136. 0136specialize signed_alternating_product_prefix_pointwise_functional x2
  137. 0137specialize signed_alternating_product_prefix_pointwise_functional x3
  138. 0138specialize signed_alternating_product_prefix_pointwise_functional x4
  139. 0139specialize signed_alternating_product_prefix_pointwise_functional x5
  140. 0140specialize signed_alternating_product_prefix_pointwise_functional x6
  141. 0141specialize signed_alternating_product_prefix_pointwise_functional x7
  142. 0142specialize signed_alternating_product_prefix_pointwise_functional l
  143. 0143specialize signed_alternating_product_prefix_pointwise_functional i
  144. 0144specialize signed_alternating_product_prefix_pointwise_functional x8
  145. 0145specialize signed_alternating_product_prefix_pointwise_functional a
  146. 0146specialize signed_alternating_product_prefix_pointwise_functional x9
  147. 0147specialize signed_alternating_product_prefix_pointwise_functional x10
  148. 0148apply signed_alternating_product_prefix_pointwise_functional
  149. 0149exact hfirst_witness_witness_witness_witness_left
  150. 0150exact hsecond_witness_witness_witness_witness_left
  151. 0151exact hi
  152. 0152exact holdother_witness
  153. 0153exact ha
  154. 0154exact hnewpositive_witness
  155. 0155exact hnewnegative_witness
  156. 0156cases hequal
  157. 0157rewrite hequal_right
  158. 0158rewrite hequal_right
  159. 0159exact hnewnegative_witness
  160. 0160split
  161. 0161specialize beta_sum_functional x4
  162. 0162specialize beta_sum_functional x5
  163. 0163specialize beta_sum_functional l
  164. 0164specialize beta_sum_functional p
  165. 0165specialize beta_sum_functional r
  166. 0166apply beta_sum_functional
  167. 0167exact htransport_positive
  168. 0168exact hsecond_witness_witness_witness_witness_right_left
  169. 0169specialize beta_sum_functional x6
  170. 0170specialize beta_sum_functional x7
  171. 0171specialize beta_sum_functional l
  172. 0172specialize beta_sum_functional n
  173. 0173specialize beta_sum_functional s
  174. 0174apply beta_sum_functional
  175. 0175exact htransport_negative
  176. 0176exact hsecond_witness_witness_witness_witness_right_right