PX0007

polynomial_diagonal_sum_left_append

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

Compare two independently coded actual antidiagonal sums: their first N terms agree and their last terms are zero and the new leading product.

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 expanded first-order arithmetic statement

forall ab ac AB AC bb bc d N a b db dc eb ec u v. (forall mdr_i_pfp_tri_sum_equal mdr_a_pfp_tri_sum_equal. (exists mdr_gap_pfp_tri_sum_equalb. mdr_gap_pfp_tri_sum_equalb + S (mdr_i_pfp_tri_sum_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_sum_equalo. ff_h_mdr_pfp_tri_sum_equalo + S (mdr_a_pfp_tri_sum_equal) = S ((S (mdr_i_pfp_tri_sum_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_sum_equalo. ab = ff_q_mdr_pfp_tri_sum_equalo * S ((S (mdr_i_pfp_tri_sum_equal)) * ac) + (mdr_a_pfp_tri_sum_equal))) -> (((exists ff_h_mdr_pfp_tri_sum_equaln. ff_h_mdr_pfp_tri_sum_equaln + S (mdr_a_pfp_tri_sum_equal) = S ((S (mdr_i_pfp_tri_sum_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_sum_equaln. AB = ff_q_mdr_pfp_tri_sum_equaln * S ((S (mdr_i_pfp_tri_sum_equal)) * AC) + (mdr_a_pfp_tri_sum_equal)))) -> (((exists ff_h_pfp_tri_sum_appended. ff_h_pfp_tri_sum_appended + S (a) = S ((S (N)) * AC)) /\ exists ff_q_pfp_tri_sum_appended. AB = ff_q_pfp_tri_sum_appended * S ((S (N)) * AC) + (a))) -> (((exists ff_h_pfp_tri_sum_head. ff_h_pfp_tri_sum_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_tri_sum_head. bb = ff_q_pfp_tri_sum_head * S ((S (0)) * bc) + (b))) -> (forall pfc_index_tri_sum_old_table. (exists pfa_gap_tri_sum_old_tablebound. pfa_gap_tri_sum_old_tablebound + S (pfc_index_tri_sum_old_table) = (S N)) -> exists pfc_value_tri_sum_old_table. ((((exists ff_h_pfp_tri_sum_old_tableentry. ff_h_pfp_tri_sum_old_tableentry + S (pfc_value_tri_sum_old_table) = S ((S (pfc_index_tri_sum_old_table)) * dc)) /\ exists ff_q_pfp_tri_sum_old_tableentry. db = ff_q_pfp_tri_sum_old_tableentry * S ((S (pfc_index_tri_sum_old_table)) * dc) + (pfc_value_tri_sum_old_table))) /\ ((exists pfc_complement_tri_sum_old_tableterm pfc_left_tri_sum_old_tableterm pfc_right_tri_sum_old_tableterm. (((pfc_index_tri_sum_old_table)+pfc_complement_tri_sum_old_tableterm=(N)) /\ ((((((exists pfa_gap_tri_sum_old_tabletermleftinside. pfa_gap_tri_sum_old_tabletermleftinside + S (pfc_index_tri_sum_old_table) = (N)) /\ ((((exists ff_h_pfp_tri_sum_old_tabletermleftentry. ff_h_pfp_tri_sum_old_tabletermleftentry + S (pfc_left_tri_sum_old_tableterm) = S ((S (pfc_index_tri_sum_old_table)) * ac)) /\ exists ff_q_pfp_tri_sum_old_tabletermleftentry. ab = ff_q_pfp_tri_sum_old_tabletermleftentry * S ((S (pfc_index_tri_sum_old_table)) * ac) + (pfc_left_tri_sum_old_tableterm)))))) \/ (((exists pfc_gap_tri_sum_old_tabletermleftoutside. pfc_gap_tri_sum_old_tabletermleftoutside+(N)=(pfc_index_tri_sum_old_table)) /\ (((pfc_left_tri_sum_old_tableterm)=0))))) /\ ((((((exists pfa_gap_tri_sum_old_tabletermrightinside. pfa_gap_tri_sum_old_tabletermrightinside + S (pfc_complement_tri_sum_old_tableterm) = (S d)) /\ ((((exists ff_h_pfp_tri_sum_old_tabletermrightentry. ff_h_pfp_tri_sum_old_tabletermrightentry + S (pfc_right_tri_sum_old_tableterm) = S ((S (pfc_complement_tri_sum_old_tableterm)) * bc)) /\ exists ff_q_pfp_tri_sum_old_tabletermrightentry. bb = ff_q_pfp_tri_sum_old_tabletermrightentry * S ((S (pfc_complement_tri_sum_old_tableterm)) * bc) + (pfc_right_tri_sum_old_tableterm)))))) \/ (((exists pfc_gap_tri_sum_old_tabletermrightoutside. pfc_gap_tri_sum_old_tabletermrightoutside+(S d)=(pfc_complement_tri_sum_old_tableterm)) /\ (((pfc_right_tri_sum_old_tableterm)=0))))) /\ (((pfc_value_tri_sum_old_table)=pfc_left_tri_sum_old_tableterm*pfc_right_tri_sum_old_tableterm))))))))))) -> (exists fs_u_pfc_tri_sum_old_actual fs_v_pfc_tri_sum_old_actual. ((((exists fs_h_pfc_tri_sum_old_actual_body_start. fs_h_pfc_tri_sum_old_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_start. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_start * S ((S (0)) * fs_v_pfc_tri_sum_old_actual) + (0))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_terminal. fs_h_pfc_tri_sum_old_actual_body_terminal + S (u) = S ((S (S N)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_terminal. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_terminal * S ((S (S N)) * fs_v_pfc_tri_sum_old_actual) + (u))) /\ forall fs_i_pfc_tri_sum_old_actual_body_steps. (exists fs_lt_pfc_tri_sum_old_actual_body_steps_bound. fs_lt_pfc_tri_sum_old_actual_body_steps_bound + S fs_i_pfc_tri_sum_old_actual_body_steps = S N) -> exists fs_a_pfc_tri_sum_old_actual_body_steps fs_r_pfc_tri_sum_old_actual_body_steps fs_s_pfc_tri_sum_old_actual_body_steps. ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_summand. fs_h_pfc_tri_sum_old_actual_body_steps_summand + S (fs_a_pfc_tri_sum_old_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * dc)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_summand. db = fs_q_pfc_tri_sum_old_actual_body_steps_summand * S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * dc) + (fs_a_pfc_tri_sum_old_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_partial. fs_h_pfc_tri_sum_old_actual_body_steps_partial + S (fs_r_pfc_tri_sum_old_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_partial. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_steps_partial * S ((S (fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual) + (fs_r_pfc_tri_sum_old_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_actual_body_steps_successor. fs_h_pfc_tri_sum_old_actual_body_steps_successor + S (fs_s_pfc_tri_sum_old_actual_body_steps) = S ((S (S fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual)) /\ exists fs_q_pfc_tri_sum_old_actual_body_steps_successor. fs_u_pfc_tri_sum_old_actual = fs_q_pfc_tri_sum_old_actual_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_old_actual_body_steps)) * fs_v_pfc_tri_sum_old_actual) + (fs_s_pfc_tri_sum_old_actual_body_steps))) /\ fs_s_pfc_tri_sum_old_actual_body_steps = fs_r_pfc_tri_sum_old_actual_body_steps + fs_a_pfc_tri_sum_old_actual_body_steps)))))) -> (forall pfc_index_tri_sum_new_table. (exists pfa_gap_tri_sum_new_tablebound. pfa_gap_tri_sum_new_tablebound + S (pfc_index_tri_sum_new_table) = (S N)) -> exists pfc_value_tri_sum_new_table. ((((exists ff_h_pfp_tri_sum_new_tableentry. ff_h_pfp_tri_sum_new_tableentry + S (pfc_value_tri_sum_new_table) = S ((S (pfc_index_tri_sum_new_table)) * ec)) /\ exists ff_q_pfp_tri_sum_new_tableentry. eb = ff_q_pfp_tri_sum_new_tableentry * S ((S (pfc_index_tri_sum_new_table)) * ec) + (pfc_value_tri_sum_new_table))) /\ ((exists pfc_complement_tri_sum_new_tableterm pfc_left_tri_sum_new_tableterm pfc_right_tri_sum_new_tableterm. (((pfc_index_tri_sum_new_table)+pfc_complement_tri_sum_new_tableterm=(N)) /\ ((((((exists pfa_gap_tri_sum_new_tabletermleftinside. pfa_gap_tri_sum_new_tabletermleftinside + S (pfc_index_tri_sum_new_table) = (S N)) /\ ((((exists ff_h_pfp_tri_sum_new_tabletermleftentry. ff_h_pfp_tri_sum_new_tabletermleftentry + S (pfc_left_tri_sum_new_tableterm) = S ((S (pfc_index_tri_sum_new_table)) * AC)) /\ exists ff_q_pfp_tri_sum_new_tabletermleftentry. AB = ff_q_pfp_tri_sum_new_tabletermleftentry * S ((S (pfc_index_tri_sum_new_table)) * AC) + (pfc_left_tri_sum_new_tableterm)))))) \/ (((exists pfc_gap_tri_sum_new_tabletermleftoutside. pfc_gap_tri_sum_new_tabletermleftoutside+(S N)=(pfc_index_tri_sum_new_table)) /\ (((pfc_left_tri_sum_new_tableterm)=0))))) /\ ((((((exists pfa_gap_tri_sum_new_tabletermrightinside. pfa_gap_tri_sum_new_tabletermrightinside + S (pfc_complement_tri_sum_new_tableterm) = (S d)) /\ ((((exists ff_h_pfp_tri_sum_new_tabletermrightentry. ff_h_pfp_tri_sum_new_tabletermrightentry + S (pfc_right_tri_sum_new_tableterm) = S ((S (pfc_complement_tri_sum_new_tableterm)) * bc)) /\ exists ff_q_pfp_tri_sum_new_tabletermrightentry. bb = ff_q_pfp_tri_sum_new_tabletermrightentry * S ((S (pfc_complement_tri_sum_new_tableterm)) * bc) + (pfc_right_tri_sum_new_tableterm)))))) \/ (((exists pfc_gap_tri_sum_new_tabletermrightoutside. pfc_gap_tri_sum_new_tabletermrightoutside+(S d)=(pfc_complement_tri_sum_new_tableterm)) /\ (((pfc_right_tri_sum_new_tableterm)=0))))) /\ (((pfc_value_tri_sum_new_table)=pfc_left_tri_sum_new_tableterm*pfc_right_tri_sum_new_tableterm))))))))))) -> (exists fs_u_pfc_tri_sum_new_actual fs_v_pfc_tri_sum_new_actual. ((((exists fs_h_pfc_tri_sum_new_actual_body_start. fs_h_pfc_tri_sum_new_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_start. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_start * S ((S (0)) * fs_v_pfc_tri_sum_new_actual) + (0))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_terminal. fs_h_pfc_tri_sum_new_actual_body_terminal + S (v) = S ((S (S N)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_terminal. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_terminal * S ((S (S N)) * fs_v_pfc_tri_sum_new_actual) + (v))) /\ forall fs_i_pfc_tri_sum_new_actual_body_steps. (exists fs_lt_pfc_tri_sum_new_actual_body_steps_bound. fs_lt_pfc_tri_sum_new_actual_body_steps_bound + S fs_i_pfc_tri_sum_new_actual_body_steps = S N) -> exists fs_a_pfc_tri_sum_new_actual_body_steps fs_r_pfc_tri_sum_new_actual_body_steps fs_s_pfc_tri_sum_new_actual_body_steps. ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_summand. fs_h_pfc_tri_sum_new_actual_body_steps_summand + S (fs_a_pfc_tri_sum_new_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * ec)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_summand. eb = fs_q_pfc_tri_sum_new_actual_body_steps_summand * S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * ec) + (fs_a_pfc_tri_sum_new_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_partial. fs_h_pfc_tri_sum_new_actual_body_steps_partial + S (fs_r_pfc_tri_sum_new_actual_body_steps) = S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_partial. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_steps_partial * S ((S (fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual) + (fs_r_pfc_tri_sum_new_actual_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_actual_body_steps_successor. fs_h_pfc_tri_sum_new_actual_body_steps_successor + S (fs_s_pfc_tri_sum_new_actual_body_steps) = S ((S (S fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual)) /\ exists fs_q_pfc_tri_sum_new_actual_body_steps_successor. fs_u_pfc_tri_sum_new_actual = fs_q_pfc_tri_sum_new_actual_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_new_actual_body_steps)) * fs_v_pfc_tri_sum_new_actual) + (fs_s_pfc_tri_sum_new_actual_body_steps))) /\ fs_s_pfc_tri_sum_new_actual_body_steps = fs_r_pfc_tri_sum_new_actual_body_steps + fs_a_pfc_tri_sum_new_actual_body_steps)))))) -> v=u+a*b

Constructive proof overview

Generated structural guide

Compare two independently coded actual antidiagonal sums: their first N terms agree and their last terms are zero and the new leading product.

The unchanged tactic script uses 10 declared prerequisites and contains 186 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sum_succ_decompose Alpha theorem; checked-use authorized PX0005 polynomial_diagonal_last_term_left_empty PX0006 polynomial_diagonal_last_term_left_append polynomial_diagonal_prefix_entry Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized PX0002 polynomial_diagonal_prefix_left_transport le_succ Alpha theorem; checked-use authorized beta_sum_transport_prefix Alpha theorem; checked-use authorized polynomial_diagonal_prefix_functional Alpha theorem; checked-use authorized beta_sum_functional Alpha theorem; checked-use authorized

Direct dependents

PX0008 prime_field_convolution_coefficient_append

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

186 script commands · 28 reading checkpoints · 8 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 (3)
polynomial diagonal last term left emptypolynomial diagonal last term left appendpolynomial diagonal prefix left transport

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 AB
  4. L4
    intro AC
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro N
  9. L9
    intro a
  10. L10
    intro b
02Fix variables and assumptionsL11–20

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

  1. L11
    intro db
  2. L12
    intro dc
  3. L13
    intro eb
  4. L14
    intro ec
  5. L15
    intro u
  6. L16
    intro v
  7. L17
    intro he
  8. L18
    intro ha
  9. L19
    intro hb
  10. L20
    intro hd
03Fix variables and assumptionsL21–23

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

  1. L21
    intro hu
  2. L22
    intro hetable
  3. L23
    intro hv
04Establish holdL24–30

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

  1. L24
    have hold : ∃ t. ∃ s. BetaAt(db,dc,N,t) ∧ (Sum(db,dc,N,s) ∧ u = s + t)Definitions: BetaAtSum
  2. L25
    specialize beta_sum_succ_decompose (db)
  3. L26
    specialize beta_sum_succ_decompose (dc)
  4. L27
    specialize beta_sum_succ_decompose (N)
  5. L28
    specialize beta_sum_succ_decompose (u)
  6. L29
    apply beta_sum_succ_decompose
  7. L30
    exact hu
05Separate the logical casesL31–34

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

  1. L31
    cases hold
  2. L32
    cases hold_witness
  3. L33
    cases hold_witness_witness
  4. L34
    cases hold_witness_witness_right
06Establish hnewL35–41

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

  1. L35
    have hnew : ∃ t. ∃ s. BetaAt(eb,ec,N,t) ∧ (Sum(eb,ec,N,s) ∧ v = s + t)Definitions: BetaAtSum
  2. L36
    specialize beta_sum_succ_decompose (eb)
  3. L37
    specialize beta_sum_succ_decompose (ec)
  4. L38
    specialize beta_sum_succ_decompose (N)
  5. L39
    specialize beta_sum_succ_decompose (v)
  6. L40
    apply beta_sum_succ_decompose
  7. L41
    exact hv
07Separate the logical casesL42–45

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

  1. L42
    cases hnew
  2. L43
    cases hnew_witness
  3. L44
    cases hnew_witness_witness
  4. L45
    cases hnew_witness_witness_right
08Establish hzL46–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial diagonal last term left empty.

  1. L46
    have hz : x=0
  2. L47
    specialize polynomial_diagonal_last_term_left_empty (ab)
  3. L48
    specialize polynomial_diagonal_last_term_left_empty (ac)
  4. L49
    specialize polynomial_diagonal_last_term_left_empty (bb)
  5. L50
    specialize polynomial_diagonal_last_term_left_empty (bc)
  6. L51
    specialize polynomial_diagonal_last_term_left_empty (S d)
  7. L52
    specialize polynomial_diagonal_last_term_left_empty (N)
  8. L53
    specialize polynomial_diagonal_last_term_left_empty (x)
  9. L54
    apply polynomial_diagonal_last_term_left_empty
  10. L55
    specialize polynomial_diagonal_prefix_entry (ab)
09Use earlier factsL56–65

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

  1. L56
    specialize polynomial_diagonal_prefix_entry (ac)
  2. L57
    specialize polynomial_diagonal_prefix_entry (N)
  3. L58
    specialize polynomial_diagonal_prefix_entry (bb)
  4. L59
    specialize polynomial_diagonal_prefix_entry (bc)
  5. L60
    specialize polynomial_diagonal_prefix_entry (S d)
  6. L61
    specialize polynomial_diagonal_prefix_entry (N)
  7. L62
    specialize polynomial_diagonal_prefix_entry (db)
  8. L63
    specialize polynomial_diagonal_prefix_entry (dc)
  9. L64
    specialize polynomial_diagonal_prefix_entry (S N)
  10. L65
    specialize polynomial_diagonal_prefix_entry (N)
10Use earlier factsL66–71

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

  1. L66
    specialize polynomial_diagonal_prefix_entry (x)
  2. L67
    apply polynomial_diagonal_prefix_entry
  3. L68
    exact hd
  4. L69
    specialize le_refl (S N)
  5. L70
    apply le_refl
  6. L71
    exact hold_witness_witness_left
11Establish htL72–81

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

  1. L72
    have ht : x2=a*b
  2. L73
    specialize polynomial_diagonal_last_term_left_append (AB)
  3. L74
    specialize polynomial_diagonal_last_term_left_append (AC)
  4. L75
    specialize polynomial_diagonal_last_term_left_append (bb)
  5. L76
    specialize polynomial_diagonal_last_term_left_append (bc)
  6. L77
    specialize polynomial_diagonal_last_term_left_append (d)
  7. L78
    specialize polynomial_diagonal_last_term_left_append (N)
  8. L79
    specialize polynomial_diagonal_last_term_left_append (a)
  9. L80
    specialize polynomial_diagonal_last_term_left_append (b)
  10. L81
    specialize polynomial_diagonal_last_term_left_append (x2)
12Use earlier factsL82–91

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

  1. L82
    apply polynomial_diagonal_last_term_left_append
  2. L83
    exact ha
  3. L84
    exact hb
  4. L85
    specialize polynomial_diagonal_prefix_entry (AB)
  5. L86
    specialize polynomial_diagonal_prefix_entry (AC)
  6. L87
    specialize polynomial_diagonal_prefix_entry (S N)
  7. L88
    specialize polynomial_diagonal_prefix_entry (bb)
  8. L89
    specialize polynomial_diagonal_prefix_entry (bc)
  9. L90
    specialize polynomial_diagonal_prefix_entry (S d)
  10. L91
    specialize polynomial_diagonal_prefix_entry (N)
13Use earlier factsL92–101

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

  1. L92
    specialize polynomial_diagonal_prefix_entry (eb)
  2. L93
    specialize polynomial_diagonal_prefix_entry (ec)
  3. L94
    specialize polynomial_diagonal_prefix_entry (S N)
  4. L95
    specialize polynomial_diagonal_prefix_entry (N)
  5. L96
    specialize polynomial_diagonal_prefix_entry (x2)
  6. L97
    apply polynomial_diagonal_prefix_entry
  7. L98
    exact hetable
  8. L99
    specialize le_refl (S N)
  9. L100
    apply le_refl
  10. L101
    exact hnew_witness_witness_left
14Establish hprefixL102–111

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

  1. L102
    have hprefix : PolynomialDiagonalPrefix(AB,AC,S N,bb,bc,S d,N,db,dc,N)Definitions: PolynomialDiagonalPrefix
  2. L103
    specialize polynomial_diagonal_prefix_left_transport (ab)
  3. L104
    specialize polynomial_diagonal_prefix_left_transport (ac)
  4. L105
    specialize polynomial_diagonal_prefix_left_transport (N)
  5. L106
    specialize polynomial_diagonal_prefix_left_transport (AB)
  6. L107
    specialize polynomial_diagonal_prefix_left_transport (AC)
  7. L108
    specialize polynomial_diagonal_prefix_left_transport (S N)
  8. L109
    specialize polynomial_diagonal_prefix_left_transport (bb)
  9. L110
    specialize polynomial_diagonal_prefix_left_transport (bc)
  10. L111
    specialize polynomial_diagonal_prefix_left_transport (S d)
15Use earlier factsL112–121

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

  1. L112
    specialize polynomial_diagonal_prefix_left_transport (N)
  2. L113
    specialize polynomial_diagonal_prefix_left_transport (N)
  3. L114
    specialize polynomial_diagonal_prefix_left_transport (db)
  4. L115
    specialize polynomial_diagonal_prefix_left_transport (dc)
  5. L116
    apply polynomial_diagonal_prefix_left_transport
  6. L117
    specialize le_refl (N)
  7. L118
    apply le_refl
  8. L119
    specialize le_succ (N)
  9. L120
    specialize le_succ (N)
  10. L121
    apply le_succ
16Use earlier factsL122–124

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

  1. L122
    specialize le_refl (N)
  2. L123
    apply le_refl
  3. L124
    exact he
17Fix variables and assumptionsL125–126

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

  1. L125
    intro j
  2. L126
    intro hj
18Use earlier factsL127–132

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

  1. L127
    specialize hd (j)
  2. L128
    apply hd
  3. L129
    specialize le_succ (S j)
  4. L130
    specialize le_succ (N)
  5. L131
    apply le_succ
  6. L132
    exact hj
19Establish hsL133–142

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

  1. L133
    have hs : Sum(eb,ec,N,x1)Definitions: Sum
  2. L134
    specialize beta_sum_transport_prefix (db)
  3. L135
    specialize beta_sum_transport_prefix (dc)
  4. L136
    specialize beta_sum_transport_prefix (eb)
  5. L137
    specialize beta_sum_transport_prefix (ec)
  6. L138
    specialize beta_sum_transport_prefix (N)
  7. L139
    specialize beta_sum_transport_prefix (x1)
  8. L140
    apply beta_sum_transport_prefix
  9. L141
    exact hold_witness_witness_right_left
  10. L142
    specialize polynomial_diagonal_prefix_functional (AB)
20Use earlier factsL143–152

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

  1. L143
    specialize polynomial_diagonal_prefix_functional (AC)
  2. L144
    specialize polynomial_diagonal_prefix_functional (S N)
  3. L145
    specialize polynomial_diagonal_prefix_functional (bb)
  4. L146
    specialize polynomial_diagonal_prefix_functional (bc)
  5. L147
    specialize polynomial_diagonal_prefix_functional (S d)
  6. L148
    specialize polynomial_diagonal_prefix_functional (N)
  7. L149
    specialize polynomial_diagonal_prefix_functional (db)
  8. L150
    specialize polynomial_diagonal_prefix_functional (dc)
  9. L151
    specialize polynomial_diagonal_prefix_functional (eb)
  10. L152
    specialize polynomial_diagonal_prefix_functional (ec)
21Use earlier factsL153–155

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

  1. L153
    specialize polynomial_diagonal_prefix_functional (N)
  2. L154
    apply polynomial_diagonal_prefix_functional
  3. L155
    exact hprefix
22Fix variables and assumptionsL156–157

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

  1. L156
    intro j
  2. L157
    intro hj
23Use earlier factsL158–163

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

  1. L158
    specialize hetable (j)
  2. L159
    apply hetable
  3. L160
    specialize le_succ (S j)
  4. L161
    specialize le_succ (N)
  5. L162
    apply le_succ
  6. L163
    exact hj
24Establish hbaseL164–172

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

  1. L164
    have hbase : x1=x3
  2. L165
    specialize beta_sum_functional (eb)
  3. L166
    specialize beta_sum_functional (ec)
  4. L167
    specialize beta_sum_functional (N)
  5. L168
    specialize beta_sum_functional (x1)
  6. L169
    specialize beta_sum_functional (x3)
  7. L170
    apply beta_sum_functional
  8. L171
    exact hs
  9. L172
    exact hnew_witness_witness_right_left
25Establish huvalueL173–182

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

  1. L173
    have huvalue : u=x1
  2. L174
    trans x1+x
  3. L175
    exact hold_witness_witness_right_right
  4. L176
    rewrite hz
  5. L177
    simp
  6. L178
    trans x3+x2
  7. L179
    exact hnew_witness_witness_right_right
  8. L180
    congr
  9. L181
    trans x1
  10. L182
    symm
26Use earlier factsL183–183

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

  1. L183
    exact hbase
27Calculate and transport equalitiesL184–184

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

  1. L184
    symm
28Use earlier factsL185–186

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

  1. L185
    exact huvalue
  2. L186
    exact ht

Library-wide reading audit

Original exact command ledger · 186 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro AB
  4. 0004intro AC
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro N
  9. 0009intro a
  10. 0010intro b
  11. 0011intro db
  12. 0012intro dc
  13. 0013intro eb
  14. 0014intro ec
  15. 0015intro u
  16. 0016intro v
  17. 0017intro he
  18. 0018intro ha
  19. 0019intro hb
  20. 0020intro hd
  21. 0021intro hu
  22. 0022intro hetable
  23. 0023intro hv
  24. 0024have hold : exists t s. ((((exists ff_h_pfp_tri_sum_old_last. ff_h_pfp_tri_sum_old_last + S (t) = S ((S (N)) * dc)) /\ exists ff_q_pfp_tri_sum_old_last. db = ff_q_pfp_tri_sum_old_last * S ((S (N)) * dc) + (t))) /\ (((exists fs_u_pfc_tri_sum_old_prefix fs_v_pfc_tri_sum_old_prefix. ((((exists fs_h_pfc_tri_sum_old_prefix_body_start. fs_h_pfc_tri_sum_old_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_old_prefix)) /\ exists fs_q_pfc_tri_sum_old_prefix_body_start. fs_u_pfc_tri_sum_old_prefix = fs_q_pfc_tri_sum_old_prefix_body_start * S ((S (0)) * fs_v_pfc_tri_sum_old_prefix) + (0))) /\ ((((exists fs_h_pfc_tri_sum_old_prefix_body_terminal. fs_h_pfc_tri_sum_old_prefix_body_terminal + S (s) = S ((S (N)) * fs_v_pfc_tri_sum_old_prefix)) /\ exists fs_q_pfc_tri_sum_old_prefix_body_terminal. fs_u_pfc_tri_sum_old_prefix = fs_q_pfc_tri_sum_old_prefix_body_terminal * S ((S (N)) * fs_v_pfc_tri_sum_old_prefix) + (s))) /\ forall fs_i_pfc_tri_sum_old_prefix_body_steps. (exists fs_lt_pfc_tri_sum_old_prefix_body_steps_bound. fs_lt_pfc_tri_sum_old_prefix_body_steps_bound + S fs_i_pfc_tri_sum_old_prefix_body_steps = N) -> exists fs_a_pfc_tri_sum_old_prefix_body_steps fs_r_pfc_tri_sum_old_prefix_body_steps fs_s_pfc_tri_sum_old_prefix_body_steps. ((((exists fs_h_pfc_tri_sum_old_prefix_body_steps_summand. fs_h_pfc_tri_sum_old_prefix_body_steps_summand + S (fs_a_pfc_tri_sum_old_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_old_prefix_body_steps)) * dc)) /\ exists fs_q_pfc_tri_sum_old_prefix_body_steps_summand. db = fs_q_pfc_tri_sum_old_prefix_body_steps_summand * S ((S (fs_i_pfc_tri_sum_old_prefix_body_steps)) * dc) + (fs_a_pfc_tri_sum_old_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_prefix_body_steps_partial. fs_h_pfc_tri_sum_old_prefix_body_steps_partial + S (fs_r_pfc_tri_sum_old_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_old_prefix_body_steps)) * fs_v_pfc_tri_sum_old_prefix)) /\ exists fs_q_pfc_tri_sum_old_prefix_body_steps_partial. fs_u_pfc_tri_sum_old_prefix = fs_q_pfc_tri_sum_old_prefix_body_steps_partial * S ((S (fs_i_pfc_tri_sum_old_prefix_body_steps)) * fs_v_pfc_tri_sum_old_prefix) + (fs_r_pfc_tri_sum_old_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_old_prefix_body_steps_successor. fs_h_pfc_tri_sum_old_prefix_body_steps_successor + S (fs_s_pfc_tri_sum_old_prefix_body_steps) = S ((S (S fs_i_pfc_tri_sum_old_prefix_body_steps)) * fs_v_pfc_tri_sum_old_prefix)) /\ exists fs_q_pfc_tri_sum_old_prefix_body_steps_successor. fs_u_pfc_tri_sum_old_prefix = fs_q_pfc_tri_sum_old_prefix_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_old_prefix_body_steps)) * fs_v_pfc_tri_sum_old_prefix) + (fs_s_pfc_tri_sum_old_prefix_body_steps))) /\ fs_s_pfc_tri_sum_old_prefix_body_steps = fs_r_pfc_tri_sum_old_prefix_body_steps + fs_a_pfc_tri_sum_old_prefix_body_steps)))))) /\ ((u=s+t)))))
  25. 0025specialize beta_sum_succ_decompose (db)
  26. 0026specialize beta_sum_succ_decompose (dc)
  27. 0027specialize beta_sum_succ_decompose (N)
  28. 0028specialize beta_sum_succ_decompose (u)
  29. 0029apply beta_sum_succ_decompose
  30. 0030exact hu
  31. 0031cases hold
  32. 0032cases hold_witness
  33. 0033cases hold_witness_witness
  34. 0034cases hold_witness_witness_right
  35. 0035have hnew : exists t s. ((((exists ff_h_pfp_tri_sum_new_last. ff_h_pfp_tri_sum_new_last + S (t) = S ((S (N)) * ec)) /\ exists ff_q_pfp_tri_sum_new_last. eb = ff_q_pfp_tri_sum_new_last * S ((S (N)) * ec) + (t))) /\ (((exists fs_u_pfc_tri_sum_new_prefix fs_v_pfc_tri_sum_new_prefix. ((((exists fs_h_pfc_tri_sum_new_prefix_body_start. fs_h_pfc_tri_sum_new_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_new_prefix)) /\ exists fs_q_pfc_tri_sum_new_prefix_body_start. fs_u_pfc_tri_sum_new_prefix = fs_q_pfc_tri_sum_new_prefix_body_start * S ((S (0)) * fs_v_pfc_tri_sum_new_prefix) + (0))) /\ ((((exists fs_h_pfc_tri_sum_new_prefix_body_terminal. fs_h_pfc_tri_sum_new_prefix_body_terminal + S (s) = S ((S (N)) * fs_v_pfc_tri_sum_new_prefix)) /\ exists fs_q_pfc_tri_sum_new_prefix_body_terminal. fs_u_pfc_tri_sum_new_prefix = fs_q_pfc_tri_sum_new_prefix_body_terminal * S ((S (N)) * fs_v_pfc_tri_sum_new_prefix) + (s))) /\ forall fs_i_pfc_tri_sum_new_prefix_body_steps. (exists fs_lt_pfc_tri_sum_new_prefix_body_steps_bound. fs_lt_pfc_tri_sum_new_prefix_body_steps_bound + S fs_i_pfc_tri_sum_new_prefix_body_steps = N) -> exists fs_a_pfc_tri_sum_new_prefix_body_steps fs_r_pfc_tri_sum_new_prefix_body_steps fs_s_pfc_tri_sum_new_prefix_body_steps. ((((exists fs_h_pfc_tri_sum_new_prefix_body_steps_summand. fs_h_pfc_tri_sum_new_prefix_body_steps_summand + S (fs_a_pfc_tri_sum_new_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_new_prefix_body_steps)) * ec)) /\ exists fs_q_pfc_tri_sum_new_prefix_body_steps_summand. eb = fs_q_pfc_tri_sum_new_prefix_body_steps_summand * S ((S (fs_i_pfc_tri_sum_new_prefix_body_steps)) * ec) + (fs_a_pfc_tri_sum_new_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_prefix_body_steps_partial. fs_h_pfc_tri_sum_new_prefix_body_steps_partial + S (fs_r_pfc_tri_sum_new_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_new_prefix_body_steps)) * fs_v_pfc_tri_sum_new_prefix)) /\ exists fs_q_pfc_tri_sum_new_prefix_body_steps_partial. fs_u_pfc_tri_sum_new_prefix = fs_q_pfc_tri_sum_new_prefix_body_steps_partial * S ((S (fs_i_pfc_tri_sum_new_prefix_body_steps)) * fs_v_pfc_tri_sum_new_prefix) + (fs_r_pfc_tri_sum_new_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_new_prefix_body_steps_successor. fs_h_pfc_tri_sum_new_prefix_body_steps_successor + S (fs_s_pfc_tri_sum_new_prefix_body_steps) = S ((S (S fs_i_pfc_tri_sum_new_prefix_body_steps)) * fs_v_pfc_tri_sum_new_prefix)) /\ exists fs_q_pfc_tri_sum_new_prefix_body_steps_successor. fs_u_pfc_tri_sum_new_prefix = fs_q_pfc_tri_sum_new_prefix_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_new_prefix_body_steps)) * fs_v_pfc_tri_sum_new_prefix) + (fs_s_pfc_tri_sum_new_prefix_body_steps))) /\ fs_s_pfc_tri_sum_new_prefix_body_steps = fs_r_pfc_tri_sum_new_prefix_body_steps + fs_a_pfc_tri_sum_new_prefix_body_steps)))))) /\ ((v=s+t)))))
  36. 0036specialize beta_sum_succ_decompose (eb)
  37. 0037specialize beta_sum_succ_decompose (ec)
  38. 0038specialize beta_sum_succ_decompose (N)
  39. 0039specialize beta_sum_succ_decompose (v)
  40. 0040apply beta_sum_succ_decompose
  41. 0041exact hv
  42. 0042cases hnew
  43. 0043cases hnew_witness
  44. 0044cases hnew_witness_witness
  45. 0045cases hnew_witness_witness_right
  46. 0046have hz : x=0
  47. 0047specialize polynomial_diagonal_last_term_left_empty (ab)
  48. 0048specialize polynomial_diagonal_last_term_left_empty (ac)
  49. 0049specialize polynomial_diagonal_last_term_left_empty (bb)
  50. 0050specialize polynomial_diagonal_last_term_left_empty (bc)
  51. 0051specialize polynomial_diagonal_last_term_left_empty (S d)
  52. 0052specialize polynomial_diagonal_last_term_left_empty (N)
  53. 0053specialize polynomial_diagonal_last_term_left_empty (x)
  54. 0054apply polynomial_diagonal_last_term_left_empty
  55. 0055specialize polynomial_diagonal_prefix_entry (ab)
  56. 0056specialize polynomial_diagonal_prefix_entry (ac)
  57. 0057specialize polynomial_diagonal_prefix_entry (N)
  58. 0058specialize polynomial_diagonal_prefix_entry (bb)
  59. 0059specialize polynomial_diagonal_prefix_entry (bc)
  60. 0060specialize polynomial_diagonal_prefix_entry (S d)
  61. 0061specialize polynomial_diagonal_prefix_entry (N)
  62. 0062specialize polynomial_diagonal_prefix_entry (db)
  63. 0063specialize polynomial_diagonal_prefix_entry (dc)
  64. 0064specialize polynomial_diagonal_prefix_entry (S N)
  65. 0065specialize polynomial_diagonal_prefix_entry (N)
  66. 0066specialize polynomial_diagonal_prefix_entry (x)
  67. 0067apply polynomial_diagonal_prefix_entry
  68. 0068exact hd
  69. 0069specialize le_refl (S N)
  70. 0070apply le_refl
  71. 0071exact hold_witness_witness_left
  72. 0072have ht : x2=a*b
  73. 0073specialize polynomial_diagonal_last_term_left_append (AB)
  74. 0074specialize polynomial_diagonal_last_term_left_append (AC)
  75. 0075specialize polynomial_diagonal_last_term_left_append (bb)
  76. 0076specialize polynomial_diagonal_last_term_left_append (bc)
  77. 0077specialize polynomial_diagonal_last_term_left_append (d)
  78. 0078specialize polynomial_diagonal_last_term_left_append (N)
  79. 0079specialize polynomial_diagonal_last_term_left_append (a)
  80. 0080specialize polynomial_diagonal_last_term_left_append (b)
  81. 0081specialize polynomial_diagonal_last_term_left_append (x2)
  82. 0082apply polynomial_diagonal_last_term_left_append
  83. 0083exact ha
  84. 0084exact hb
  85. 0085specialize polynomial_diagonal_prefix_entry (AB)
  86. 0086specialize polynomial_diagonal_prefix_entry (AC)
  87. 0087specialize polynomial_diagonal_prefix_entry (S N)
  88. 0088specialize polynomial_diagonal_prefix_entry (bb)
  89. 0089specialize polynomial_diagonal_prefix_entry (bc)
  90. 0090specialize polynomial_diagonal_prefix_entry (S d)
  91. 0091specialize polynomial_diagonal_prefix_entry (N)
  92. 0092specialize polynomial_diagonal_prefix_entry (eb)
  93. 0093specialize polynomial_diagonal_prefix_entry (ec)
  94. 0094specialize polynomial_diagonal_prefix_entry (S N)
  95. 0095specialize polynomial_diagonal_prefix_entry (N)
  96. 0096specialize polynomial_diagonal_prefix_entry (x2)
  97. 0097apply polynomial_diagonal_prefix_entry
  98. 0098exact hetable
  99. 0099specialize le_refl (S N)
  100. 0100apply le_refl
  101. 0101exact hnew_witness_witness_left
  102. 0102have hprefix : forall pfc_index_tri_sum_transported. (exists pfa_gap_tri_sum_transportedbound. pfa_gap_tri_sum_transportedbound + S (pfc_index_tri_sum_transported) = (N)) -> exists pfc_value_tri_sum_transported. ((((exists ff_h_pfp_tri_sum_transportedentry. ff_h_pfp_tri_sum_transportedentry + S (pfc_value_tri_sum_transported) = S ((S (pfc_index_tri_sum_transported)) * dc)) /\ exists ff_q_pfp_tri_sum_transportedentry. db = ff_q_pfp_tri_sum_transportedentry * S ((S (pfc_index_tri_sum_transported)) * dc) + (pfc_value_tri_sum_transported))) /\ ((exists pfc_complement_tri_sum_transportedterm pfc_left_tri_sum_transportedterm pfc_right_tri_sum_transportedterm. (((pfc_index_tri_sum_transported)+pfc_complement_tri_sum_transportedterm=(N)) /\ ((((((exists pfa_gap_tri_sum_transportedtermleftinside. pfa_gap_tri_sum_transportedtermleftinside + S (pfc_index_tri_sum_transported) = (S N)) /\ ((((exists ff_h_pfp_tri_sum_transportedtermleftentry. ff_h_pfp_tri_sum_transportedtermleftentry + S (pfc_left_tri_sum_transportedterm) = S ((S (pfc_index_tri_sum_transported)) * AC)) /\ exists ff_q_pfp_tri_sum_transportedtermleftentry. AB = ff_q_pfp_tri_sum_transportedtermleftentry * S ((S (pfc_index_tri_sum_transported)) * AC) + (pfc_left_tri_sum_transportedterm)))))) \/ (((exists pfc_gap_tri_sum_transportedtermleftoutside. pfc_gap_tri_sum_transportedtermleftoutside+(S N)=(pfc_index_tri_sum_transported)) /\ (((pfc_left_tri_sum_transportedterm)=0))))) /\ ((((((exists pfa_gap_tri_sum_transportedtermrightinside. pfa_gap_tri_sum_transportedtermrightinside + S (pfc_complement_tri_sum_transportedterm) = (S d)) /\ ((((exists ff_h_pfp_tri_sum_transportedtermrightentry. ff_h_pfp_tri_sum_transportedtermrightentry + S (pfc_right_tri_sum_transportedterm) = S ((S (pfc_complement_tri_sum_transportedterm)) * bc)) /\ exists ff_q_pfp_tri_sum_transportedtermrightentry. bb = ff_q_pfp_tri_sum_transportedtermrightentry * S ((S (pfc_complement_tri_sum_transportedterm)) * bc) + (pfc_right_tri_sum_transportedterm)))))) \/ (((exists pfc_gap_tri_sum_transportedtermrightoutside. pfc_gap_tri_sum_transportedtermrightoutside+(S d)=(pfc_complement_tri_sum_transportedterm)) /\ (((pfc_right_tri_sum_transportedterm)=0))))) /\ (((pfc_value_tri_sum_transported)=pfc_left_tri_sum_transportedterm*pfc_right_tri_sum_transportedterm))))))))))
  103. 0103specialize polynomial_diagonal_prefix_left_transport (ab)
  104. 0104specialize polynomial_diagonal_prefix_left_transport (ac)
  105. 0105specialize polynomial_diagonal_prefix_left_transport (N)
  106. 0106specialize polynomial_diagonal_prefix_left_transport (AB)
  107. 0107specialize polynomial_diagonal_prefix_left_transport (AC)
  108. 0108specialize polynomial_diagonal_prefix_left_transport (S N)
  109. 0109specialize polynomial_diagonal_prefix_left_transport (bb)
  110. 0110specialize polynomial_diagonal_prefix_left_transport (bc)
  111. 0111specialize polynomial_diagonal_prefix_left_transport (S d)
  112. 0112specialize polynomial_diagonal_prefix_left_transport (N)
  113. 0113specialize polynomial_diagonal_prefix_left_transport (N)
  114. 0114specialize polynomial_diagonal_prefix_left_transport (db)
  115. 0115specialize polynomial_diagonal_prefix_left_transport (dc)
  116. 0116apply polynomial_diagonal_prefix_left_transport
  117. 0117specialize le_refl (N)
  118. 0118apply le_refl
  119. 0119specialize le_succ (N)
  120. 0120specialize le_succ (N)
  121. 0121apply le_succ
  122. 0122specialize le_refl (N)
  123. 0123apply le_refl
  124. 0124exact he
  125. 0125intro j
  126. 0126intro hj
  127. 0127specialize hd (j)
  128. 0128apply hd
  129. 0129specialize le_succ (S j)
  130. 0130specialize le_succ (N)
  131. 0131apply le_succ
  132. 0132exact hj
  133. 0133have hs : exists fs_u_pfc_tri_sum_same_prefix fs_v_pfc_tri_sum_same_prefix. ((((exists fs_h_pfc_tri_sum_same_prefix_body_start. fs_h_pfc_tri_sum_same_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_sum_same_prefix)) /\ exists fs_q_pfc_tri_sum_same_prefix_body_start. fs_u_pfc_tri_sum_same_prefix = fs_q_pfc_tri_sum_same_prefix_body_start * S ((S (0)) * fs_v_pfc_tri_sum_same_prefix) + (0))) /\ ((((exists fs_h_pfc_tri_sum_same_prefix_body_terminal. fs_h_pfc_tri_sum_same_prefix_body_terminal + S (x1) = S ((S (N)) * fs_v_pfc_tri_sum_same_prefix)) /\ exists fs_q_pfc_tri_sum_same_prefix_body_terminal. fs_u_pfc_tri_sum_same_prefix = fs_q_pfc_tri_sum_same_prefix_body_terminal * S ((S (N)) * fs_v_pfc_tri_sum_same_prefix) + (x1))) /\ forall fs_i_pfc_tri_sum_same_prefix_body_steps. (exists fs_lt_pfc_tri_sum_same_prefix_body_steps_bound. fs_lt_pfc_tri_sum_same_prefix_body_steps_bound + S fs_i_pfc_tri_sum_same_prefix_body_steps = N) -> exists fs_a_pfc_tri_sum_same_prefix_body_steps fs_r_pfc_tri_sum_same_prefix_body_steps fs_s_pfc_tri_sum_same_prefix_body_steps. ((((exists fs_h_pfc_tri_sum_same_prefix_body_steps_summand. fs_h_pfc_tri_sum_same_prefix_body_steps_summand + S (fs_a_pfc_tri_sum_same_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_same_prefix_body_steps)) * ec)) /\ exists fs_q_pfc_tri_sum_same_prefix_body_steps_summand. eb = fs_q_pfc_tri_sum_same_prefix_body_steps_summand * S ((S (fs_i_pfc_tri_sum_same_prefix_body_steps)) * ec) + (fs_a_pfc_tri_sum_same_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_same_prefix_body_steps_partial. fs_h_pfc_tri_sum_same_prefix_body_steps_partial + S (fs_r_pfc_tri_sum_same_prefix_body_steps) = S ((S (fs_i_pfc_tri_sum_same_prefix_body_steps)) * fs_v_pfc_tri_sum_same_prefix)) /\ exists fs_q_pfc_tri_sum_same_prefix_body_steps_partial. fs_u_pfc_tri_sum_same_prefix = fs_q_pfc_tri_sum_same_prefix_body_steps_partial * S ((S (fs_i_pfc_tri_sum_same_prefix_body_steps)) * fs_v_pfc_tri_sum_same_prefix) + (fs_r_pfc_tri_sum_same_prefix_body_steps))) /\ ((((exists fs_h_pfc_tri_sum_same_prefix_body_steps_successor. fs_h_pfc_tri_sum_same_prefix_body_steps_successor + S (fs_s_pfc_tri_sum_same_prefix_body_steps) = S ((S (S fs_i_pfc_tri_sum_same_prefix_body_steps)) * fs_v_pfc_tri_sum_same_prefix)) /\ exists fs_q_pfc_tri_sum_same_prefix_body_steps_successor. fs_u_pfc_tri_sum_same_prefix = fs_q_pfc_tri_sum_same_prefix_body_steps_successor * S ((S (S fs_i_pfc_tri_sum_same_prefix_body_steps)) * fs_v_pfc_tri_sum_same_prefix) + (fs_s_pfc_tri_sum_same_prefix_body_steps))) /\ fs_s_pfc_tri_sum_same_prefix_body_steps = fs_r_pfc_tri_sum_same_prefix_body_steps + fs_a_pfc_tri_sum_same_prefix_body_steps)))))
  134. 0134specialize beta_sum_transport_prefix (db)
  135. 0135specialize beta_sum_transport_prefix (dc)
  136. 0136specialize beta_sum_transport_prefix (eb)
  137. 0137specialize beta_sum_transport_prefix (ec)
  138. 0138specialize beta_sum_transport_prefix (N)
  139. 0139specialize beta_sum_transport_prefix (x1)
  140. 0140apply beta_sum_transport_prefix
  141. 0141exact hold_witness_witness_right_left
  142. 0142specialize polynomial_diagonal_prefix_functional (AB)
  143. 0143specialize polynomial_diagonal_prefix_functional (AC)
  144. 0144specialize polynomial_diagonal_prefix_functional (S N)
  145. 0145specialize polynomial_diagonal_prefix_functional (bb)
  146. 0146specialize polynomial_diagonal_prefix_functional (bc)
  147. 0147specialize polynomial_diagonal_prefix_functional (S d)
  148. 0148specialize polynomial_diagonal_prefix_functional (N)
  149. 0149specialize polynomial_diagonal_prefix_functional (db)
  150. 0150specialize polynomial_diagonal_prefix_functional (dc)
  151. 0151specialize polynomial_diagonal_prefix_functional (eb)
  152. 0152specialize polynomial_diagonal_prefix_functional (ec)
  153. 0153specialize polynomial_diagonal_prefix_functional (N)
  154. 0154apply polynomial_diagonal_prefix_functional
  155. 0155exact hprefix
  156. 0156intro j
  157. 0157intro hj
  158. 0158specialize hetable (j)
  159. 0159apply hetable
  160. 0160specialize le_succ (S j)
  161. 0161specialize le_succ (N)
  162. 0162apply le_succ
  163. 0163exact hj
  164. 0164have hbase : x1=x3
  165. 0165specialize beta_sum_functional (eb)
  166. 0166specialize beta_sum_functional (ec)
  167. 0167specialize beta_sum_functional (N)
  168. 0168specialize beta_sum_functional (x1)
  169. 0169specialize beta_sum_functional (x3)
  170. 0170apply beta_sum_functional
  171. 0171exact hs
  172. 0172exact hnew_witness_witness_right_left
  173. 0173have huvalue : u=x1
  174. 0174trans x1+x
  175. 0175exact hold_witness_witness_right_right
  176. 0176rewrite hz
  177. 0177simp
  178. 0178trans x3+x2
  179. 0179exact hnew_witness_witness_right_right
  180. 0180congr
  181. 0181trans x1
  182. 0182symm
  183. 0183exact hbase
  184. 0184symm
  185. 0185exact huvalue
  186. 0186exact ht