BT00T6 · Bertrand theorem

beta_pascal_table_prefix_extend

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Append one semantic Pascal row to both outer beta prefixes.

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.

Statement with defined notation

∀ bb. ∀ bc. ∀ sb. ∀ sc. ∀ w. ∀ r. (∀ x. Lt(x,r) → ∃ y. ∃ z. BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (x = 0 ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(y,z,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. n = S k ∧ m = 0))) ∨ (∃ n. ∃ m. ∃ k. x = S n ∧ (BetaAt(bb,bc,n,m) ∧ (BetaAt(sb,sc,n,k) ∧ (∀ i. Lt(i,w) → ∃ j. BetaAt(y,z,i,j) ∧ (i = 0 ∧ j = 1 ∨ (∃ u. ∃ v. ∃ x0. i = S u ∧ (BetaAt(m,k,u,v) ∧ (BetaAt(m,k,S u,x0) ∧ j = v + x0))))))))))) → ∃ x. ∃ y. ∃ z. ∃ n. ∀ m. Lt(m,S r) → ∃ k. ∃ i. BetaAt(x,y,m,k) ∧ (BetaAt(z,n,m,i) ∧ (m = 0 ∧ (∀ j. Lt(j,w) → ∃ u. BetaAt(k,i,j,u) ∧ (j = 0 ∧ u = 1 ∨ (∃ v. j = S v ∧ u = 0))) ∨ (∃ j. ∃ u. ∃ v. m = S j ∧ (BetaAt(x,y,j,u) ∧ (BetaAt(z,n,j,v) ∧ (∀ x0. Lt(x0,w) → ∃ x1. BetaAt(k,i,x0,x1) ∧ (x0 = 0 ∧ x1 = 1 ∨ (∃ x2. ∃ x3. ∃ x4. x0 = S x2 ∧ (BetaAt(u,v,x2,x3) ∧ (BetaAt(u,v,S x2,x4) ∧ x1 = x3 + x4))))))))))

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

22 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0013 BetaAt

60 occurrences

Exact expanded native-PA statement
forall bb bc sb sc w r. (forall bcf_row_index_bptpe_before. (exists bcf_lt_gap_bptpe_before_row_bound. bcf_lt_gap_bptpe_before_row_bound + S (bcf_row_index_bptpe_before) = r) -> exists bcf_row_code_bptpe_before bcf_row_scale_bptpe_before. ((((exists bcf_height_bptpe_before_decoded_row_code. bcf_height_bptpe_before_decoded_row_code + S (bcf_row_code_bptpe_before) = S ((S (bcf_row_index_bptpe_before)) * bc)) /\ exists bcf_quotient_bptpe_before_decoded_row_code. bb = bcf_quotient_bptpe_before_decoded_row_code * S ((S (bcf_row_index_bptpe_before)) * bc) + (bcf_row_code_bptpe_before))) /\ ((((exists bcf_height_bptpe_before_decoded_row_scale. bcf_height_bptpe_before_decoded_row_scale + S (bcf_row_scale_bptpe_before) = S ((S (bcf_row_index_bptpe_before)) * sc)) /\ exists bcf_quotient_bptpe_before_decoded_row_scale. sb = bcf_quotient_bptpe_before_decoded_row_scale * S ((S (bcf_row_index_bptpe_before)) * sc) + (bcf_row_scale_bptpe_before))) /\ ((bcf_row_index_bptpe_before = 0 /\ (forall bcf_index_bptpe_before_zero_row. (exists bcf_lt_gap_bptpe_before_zero_row_bound. bcf_lt_gap_bptpe_before_zero_row_bound + S (bcf_index_bptpe_before_zero_row) = w) -> exists bcf_value_bptpe_before_zero_row. ((((exists bcf_height_bptpe_before_zero_row_entry. bcf_height_bptpe_before_zero_row_entry + S (bcf_value_bptpe_before_zero_row) = S ((S (bcf_index_bptpe_before_zero_row)) * bcf_row_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_zero_row_entry. bcf_row_code_bptpe_before = bcf_quotient_bptpe_before_zero_row_entry * S ((S (bcf_index_bptpe_before_zero_row)) * bcf_row_scale_bptpe_before) + (bcf_value_bptpe_before_zero_row))) /\ ((bcf_index_bptpe_before_zero_row = 0 /\ bcf_value_bptpe_before_zero_row = 1) \/ exists bcf_predecessor_bptpe_before_zero_row. bcf_index_bptpe_before_zero_row = S bcf_predecessor_bptpe_before_zero_row /\ bcf_value_bptpe_before_zero_row = 0)))) \/ exists bcf_predecessor_bptpe_before bcf_previous_code_bptpe_before bcf_previous_scale_bptpe_before. bcf_row_index_bptpe_before = S bcf_predecessor_bptpe_before /\ ((((exists bcf_height_bptpe_before_decoded_previous_code. bcf_height_bptpe_before_decoded_previous_code + S (bcf_previous_code_bptpe_before) = S ((S (bcf_predecessor_bptpe_before)) * bc)) /\ exists bcf_quotient_bptpe_before_decoded_previous_code. bb = bcf_quotient_bptpe_before_decoded_previous_code * S ((S (bcf_predecessor_bptpe_before)) * bc) + (bcf_previous_code_bptpe_before))) /\ ((((exists bcf_height_bptpe_before_decoded_previous_scale. bcf_height_bptpe_before_decoded_previous_scale + S (bcf_previous_scale_bptpe_before) = S ((S (bcf_predecessor_bptpe_before)) * sc)) /\ exists bcf_quotient_bptpe_before_decoded_previous_scale. sb = bcf_quotient_bptpe_before_decoded_previous_scale * S ((S (bcf_predecessor_bptpe_before)) * sc) + (bcf_previous_scale_bptpe_before))) /\ (forall bcf_index_bptpe_before_row_step. (exists bcf_lt_gap_bptpe_before_row_step_bound. bcf_lt_gap_bptpe_before_row_step_bound + S (bcf_index_bptpe_before_row_step) = w) -> exists bcf_value_bptpe_before_row_step. ((((exists bcf_height_bptpe_before_row_step_entry. bcf_height_bptpe_before_row_step_entry + S (bcf_value_bptpe_before_row_step) = S ((S (bcf_index_bptpe_before_row_step)) * bcf_row_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_entry. bcf_row_code_bptpe_before = bcf_quotient_bptpe_before_row_step_entry * S ((S (bcf_index_bptpe_before_row_step)) * bcf_row_scale_bptpe_before) + (bcf_value_bptpe_before_row_step))) /\ ((bcf_index_bptpe_before_row_step = 0 /\ bcf_value_bptpe_before_row_step = 1) \/ exists bcf_predecessor_bptpe_before_row_step bcf_left_bptpe_before_row_step bcf_right_bptpe_before_row_step. bcf_index_bptpe_before_row_step = S bcf_predecessor_bptpe_before_row_step /\ ((((exists bcf_height_bptpe_before_row_step_previous_left. bcf_height_bptpe_before_row_step_previous_left + S (bcf_left_bptpe_before_row_step) = S ((S (bcf_predecessor_bptpe_before_row_step)) * bcf_previous_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_previous_left. bcf_previous_code_bptpe_before = bcf_quotient_bptpe_before_row_step_previous_left * S ((S (bcf_predecessor_bptpe_before_row_step)) * bcf_previous_scale_bptpe_before) + (bcf_left_bptpe_before_row_step))) /\ ((((exists bcf_height_bptpe_before_row_step_previous_right. bcf_height_bptpe_before_row_step_previous_right + S (bcf_right_bptpe_before_row_step) = S ((S (S (bcf_predecessor_bptpe_before_row_step))) * bcf_previous_scale_bptpe_before)) /\ exists bcf_quotient_bptpe_before_row_step_previous_right. bcf_previous_code_bptpe_before = bcf_quotient_bptpe_before_row_step_previous_right * S ((S (S (bcf_predecessor_bptpe_before_row_step))) * bcf_previous_scale_bptpe_before) + (bcf_right_bptpe_before_row_step))) /\ bcf_value_bptpe_before_row_step = bcf_left_bptpe_before_row_step + bcf_right_bptpe_before_row_step))))))))))) -> exists db dc eb ec. (forall bcf_row_index_bptpe_after. (exists bcf_lt_gap_bptpe_after_row_bound. bcf_lt_gap_bptpe_after_row_bound + S (bcf_row_index_bptpe_after) = S (r)) -> exists bcf_row_code_bptpe_after bcf_row_scale_bptpe_after. ((((exists bcf_height_bptpe_after_decoded_row_code. bcf_height_bptpe_after_decoded_row_code + S (bcf_row_code_bptpe_after) = S ((S (bcf_row_index_bptpe_after)) * dc)) /\ exists bcf_quotient_bptpe_after_decoded_row_code. db = bcf_quotient_bptpe_after_decoded_row_code * S ((S (bcf_row_index_bptpe_after)) * dc) + (bcf_row_code_bptpe_after))) /\ ((((exists bcf_height_bptpe_after_decoded_row_scale. bcf_height_bptpe_after_decoded_row_scale + S (bcf_row_scale_bptpe_after) = S ((S (bcf_row_index_bptpe_after)) * ec)) /\ exists bcf_quotient_bptpe_after_decoded_row_scale. eb = bcf_quotient_bptpe_after_decoded_row_scale * S ((S (bcf_row_index_bptpe_after)) * ec) + (bcf_row_scale_bptpe_after))) /\ ((bcf_row_index_bptpe_after = 0 /\ (forall bcf_index_bptpe_after_zero_row. (exists bcf_lt_gap_bptpe_after_zero_row_bound. bcf_lt_gap_bptpe_after_zero_row_bound + S (bcf_index_bptpe_after_zero_row) = w) -> exists bcf_value_bptpe_after_zero_row. ((((exists bcf_height_bptpe_after_zero_row_entry. bcf_height_bptpe_after_zero_row_entry + S (bcf_value_bptpe_after_zero_row) = S ((S (bcf_index_bptpe_after_zero_row)) * bcf_row_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_zero_row_entry. bcf_row_code_bptpe_after = bcf_quotient_bptpe_after_zero_row_entry * S ((S (bcf_index_bptpe_after_zero_row)) * bcf_row_scale_bptpe_after) + (bcf_value_bptpe_after_zero_row))) /\ ((bcf_index_bptpe_after_zero_row = 0 /\ bcf_value_bptpe_after_zero_row = 1) \/ exists bcf_predecessor_bptpe_after_zero_row. bcf_index_bptpe_after_zero_row = S bcf_predecessor_bptpe_after_zero_row /\ bcf_value_bptpe_after_zero_row = 0)))) \/ exists bcf_predecessor_bptpe_after bcf_previous_code_bptpe_after bcf_previous_scale_bptpe_after. bcf_row_index_bptpe_after = S bcf_predecessor_bptpe_after /\ ((((exists bcf_height_bptpe_after_decoded_previous_code. bcf_height_bptpe_after_decoded_previous_code + S (bcf_previous_code_bptpe_after) = S ((S (bcf_predecessor_bptpe_after)) * dc)) /\ exists bcf_quotient_bptpe_after_decoded_previous_code. db = bcf_quotient_bptpe_after_decoded_previous_code * S ((S (bcf_predecessor_bptpe_after)) * dc) + (bcf_previous_code_bptpe_after))) /\ ((((exists bcf_height_bptpe_after_decoded_previous_scale. bcf_height_bptpe_after_decoded_previous_scale + S (bcf_previous_scale_bptpe_after) = S ((S (bcf_predecessor_bptpe_after)) * ec)) /\ exists bcf_quotient_bptpe_after_decoded_previous_scale. eb = bcf_quotient_bptpe_after_decoded_previous_scale * S ((S (bcf_predecessor_bptpe_after)) * ec) + (bcf_previous_scale_bptpe_after))) /\ (forall bcf_index_bptpe_after_row_step. (exists bcf_lt_gap_bptpe_after_row_step_bound. bcf_lt_gap_bptpe_after_row_step_bound + S (bcf_index_bptpe_after_row_step) = w) -> exists bcf_value_bptpe_after_row_step. ((((exists bcf_height_bptpe_after_row_step_entry. bcf_height_bptpe_after_row_step_entry + S (bcf_value_bptpe_after_row_step) = S ((S (bcf_index_bptpe_after_row_step)) * bcf_row_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_entry. bcf_row_code_bptpe_after = bcf_quotient_bptpe_after_row_step_entry * S ((S (bcf_index_bptpe_after_row_step)) * bcf_row_scale_bptpe_after) + (bcf_value_bptpe_after_row_step))) /\ ((bcf_index_bptpe_after_row_step = 0 /\ bcf_value_bptpe_after_row_step = 1) \/ exists bcf_predecessor_bptpe_after_row_step bcf_left_bptpe_after_row_step bcf_right_bptpe_after_row_step. bcf_index_bptpe_after_row_step = S bcf_predecessor_bptpe_after_row_step /\ ((((exists bcf_height_bptpe_after_row_step_previous_left. bcf_height_bptpe_after_row_step_previous_left + S (bcf_left_bptpe_after_row_step) = S ((S (bcf_predecessor_bptpe_after_row_step)) * bcf_previous_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_previous_left. bcf_previous_code_bptpe_after = bcf_quotient_bptpe_after_row_step_previous_left * S ((S (bcf_predecessor_bptpe_after_row_step)) * bcf_previous_scale_bptpe_after) + (bcf_left_bptpe_after_row_step))) /\ ((((exists bcf_height_bptpe_after_row_step_previous_right. bcf_height_bptpe_after_row_step_previous_right + S (bcf_right_bptpe_after_row_step) = S ((S (S (bcf_predecessor_bptpe_after_row_step))) * bcf_previous_scale_bptpe_after)) /\ exists bcf_quotient_bptpe_after_row_step_previous_right. bcf_previous_code_bptpe_after = bcf_quotient_bptpe_after_row_step_previous_right * S ((S (S (bcf_predecessor_bptpe_after_row_step))) * bcf_previous_scale_bptpe_after) + (bcf_right_bptpe_after_row_step))) /\ bcf_value_bptpe_after_row_step = bcf_left_bptpe_after_row_step + bcf_right_bptpe_after_row_step)))))))))))

Proof neighborhood

Direct theorem prerequisites

BT000Q zero_or_succ BT000E le_refl BT0019 lt_to_le BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt BT00T3 beta_pascal_zero_row_exists BT00T5 beta_pascal_row_step_exists

Direct theorem dependents

BT00T7 beta_pascal_table_prefix_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

261 script commands · 92 reading checkpoints · 17 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 (7)
zero or succle refllt to lebeta prefix extendfinite lt succ eq or ltbeta pascal zero row existsbeta pascal row step exists
01Fix variables and assumptionsL1–7

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

  1. L1
    intro bb
  2. L2
    intro bc
  3. L3
    intro sb
  4. L4
    intro sc
  5. L5
    intro w
  6. L6
    intro r
  7. L7
    intro htable
02Use earlier factsL8–8

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

  1. L8
    specialize zero_or_succ r
03Separate the logical casesL9–9

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

  1. L9
    cases zero_or_succ
04Establish hzeroL10–12

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

  1. L10
    have hzero : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Definitions: Lt(x,w)BetaAt(b,c,x,y)Original native command in the exact edition
  2. L11
    specialize beta_pascal_zero_row_exists w
  3. L12
    exact beta_pascal_zero_row_exists
05Separate the logical casesL13–14

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

  1. L13
    cases hzero
  2. L14
    cases hzero_witness
06Establish hcode_extendL15–20

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

  1. L15
    have hcode_extend : ∃ db. ∃ dc. BetaAt(db,dc,r,x) ∧ (∀ y. ∀ z. Lt(y,r) → BetaAt(bb,bc,y,z) → BetaAt(db,dc,y,z))Definitions: BetaAt(db,dc,r,x)Lt(y,r)BetaAt(bb,bc,y,z)BetaAt(db,dc,y,z)Original native command in the exact edition
  2. L16
    specialize beta_prefix_extend r
  3. L17
    specialize beta_prefix_extend bb
  4. L18
    specialize beta_prefix_extend bc
  5. L19
    specialize beta_prefix_extend x
  6. L20
    exact beta_prefix_extend
07Separate the logical casesL21–23

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

  1. L21
    cases hcode_extend
  2. L22
    cases hcode_extend_witness
  3. L23
    cases hcode_extend_witness_witness
08Establish hscale_extendL24–29

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

  1. L24
    have hscale_extend : ∃ eb. ∃ ec. BetaAt(eb,ec,r,x1) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(sb,sc,x,y) → BetaAt(eb,ec,x,y))Definitions: BetaAt(eb,ec,r,x1)Lt(x,r)BetaAt(sb,sc,x,y)BetaAt(eb,ec,x,y)Original native command in the exact edition
  2. L25
    specialize beta_prefix_extend r
  3. L26
    specialize beta_prefix_extend sb
  4. L27
    specialize beta_prefix_extend sc
  5. L28
    specialize beta_prefix_extend x1
  6. L29
    exact beta_prefix_extend
09Separate the logical casesL30–32

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

  1. L30
    cases hscale_extend
  2. L31
    cases hscale_extend_witness
  3. L32
    cases hscale_extend_witness_witness
10Construct an explicit witnessL33–36

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

  1. L33
    exists x2
  2. L34
    exists x3
  3. L35
    exists x4
  4. L36
    exists x5
11Fix variables and assumptionsL37–38

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

  1. L37
    intro i
  2. L38
    intro hi
12Establish hsplitL39–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L39
    have hsplit : i = r ∨ Lt(i,r)Definitions: Lt(i,r)Original native command in the exact edition
  2. L40
    specialize finite_lt_succ_eq_or_lt r
  3. L41
    specialize finite_lt_succ_eq_or_lt i
  4. L42
    apply finite_lt_succ_eq_or_lt
  5. L43
    exact hi
13Separate the logical casesL44–44

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

  1. L44
    cases hsplit
14Construct an explicit witnessL45–46

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

  1. L45
    exists x
  2. L46
    exists x1
15Separate the logical casesL47–47

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

  1. L47
    split
16Calculate and transport equalitiesL48–49

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

  1. L48
    rewrite hsplit_left
  2. L49
    rewrite hsplit_left
17Use earlier factsL50–50

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

  1. L50
    exact hcode_extend_witness_witness_left
18Separate the logical casesL51–51

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

  1. L51
    split
19Calculate and transport equalitiesL52–53

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

  1. L52
    rewrite hsplit_left
  2. L53
    rewrite hsplit_left
20Use earlier factsL54–54

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

  1. L54
    exact hscale_extend_witness_witness_left
21Separate the logical casesL55–56

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

  1. L55
    left
  2. L56
    split
22Calculate and transport equalitiesL57–57

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

  1. L57
    trans r
23Use earlier factsL58–61

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

  1. L58
    exact hsplit_left
  2. L59
    exact zero_or_succ_left
  3. L60
    exact hzero_witness_witness
  4. L61
    specialize htable i
24Establish holdL62–64

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

  1. L62
    have hold : ∃ b. ∃ c. BetaAt(bb,bc,i,b) ∧ (BetaAt(sb,sc,i,c) ∧ (i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(b,c,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))Definitions: BetaAt(bb,bc,i,b)BetaAt(sb,sc,i,c)Lt(x,w)BetaAt(b,c,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(b,c,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L63
    apply htable
  3. L64
    exact hsplit_right
25Separate the logical casesL65–68

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

  1. L65
    cases hold
  2. L66
    cases hold_witness
  3. L67
    cases hold_witness_witness
  4. L68
    cases hold_witness_witness_right
26Construct an explicit witnessL69–70

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

  1. L69
    exists x6
  2. L70
    exists x7
27Separate the logical casesL71–71

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

  1. L71
    split
28Use earlier factsL72–76

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

  1. L72
    specialize hcode_extend_witness_witness_right i
  2. L73
    specialize hcode_extend_witness_witness_right x6
  3. L74
    apply hcode_extend_witness_witness_right
  4. L75
    exact hsplit_right
  5. L76
    exact hold_witness_witness_left
29Separate the logical casesL77–77

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

  1. L77
    split
30Use earlier factsL78–82

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

  1. L78
    specialize hscale_extend_witness_witness_right i
  2. L79
    specialize hscale_extend_witness_witness_right x7
  3. L80
    apply hscale_extend_witness_witness_right
  4. L81
    exact hsplit_right
  5. L82
    exact hold_witness_witness_right_left
31Separate the logical casesL83–84

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

  1. L83
    cases hold_witness_witness_right_right
  2. L84
    left
32Use earlier factsL85–85

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

  1. L85
    exact hold_witness_witness_right_right_left
33Separate the logical casesL86–92

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

  1. L86
    cases hold_witness_witness_right_right_right
  2. L87
    cases hold_witness_witness_right_right_right_witness
  3. L88
    cases hold_witness_witness_right_right_right_witness_witness
  4. L89
    cases hold_witness_witness_right_right_right_witness_witness_witness
  5. L90
    cases hold_witness_witness_right_right_right_witness_witness_witness_right
  6. L91
    cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  7. L92
    right
34Construct an explicit witnessL93–95

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

  1. L93
    exists x8
  2. L94
    exists x9
  3. L95
    exists x10
35Separate the logical casesL96–96

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

  1. L96
    split
36Use earlier factsL97–97

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

  1. L97
    exact hold_witness_witness_right_right_right_witness_witness_witness_left
37Establish hpred_boundL98–98

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

  1. L98
    have hpred_bound : Lt(x8,r)Definitions: Lt(x8,r)Original native command in the exact edition
38Establish hi_leL99–105

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L99
  2. L100
    specialize lt_to_le i
  3. L101
    specialize lt_to_le r
  4. L102
    apply lt_to_le
  5. L103
    exact hsplit_right
  6. L104
    rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  7. L105
    exact hi_le
39Separate the logical casesL106–106

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

  1. L106
    split
40Use earlier factsL107–111

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

  1. L107
    specialize hcode_extend_witness_witness_right x8
  2. L108
    specialize hcode_extend_witness_witness_right x9
  3. L109
    apply hcode_extend_witness_witness_right
  4. L110
    exact hpred_bound
  5. L111
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
41Separate the logical casesL112–112

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

  1. L112
    split
42Use earlier factsL113–118

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

  1. L113
    specialize hscale_extend_witness_witness_right x8
  2. L114
    specialize hscale_extend_witness_witness_right x10
  3. L115
    apply hscale_extend_witness_witness_right
  4. L116
    exact hpred_bound
  5. L117
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  6. L118
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right
43Separate the logical casesL119–119

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

  1. L119
    cases zero_or_succ_right
44Establish hboundL120–123

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

  1. L120
    have hbound : Lt(x,r)Definitions: Lt(x,r)Original native command in the exact edition
  2. L121
    rewrite zero_or_succ_right_witness
  3. L122
    specialize le_refl (S x)
  4. L123
    exact le_refl
45Establish hpreviousL124–127

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

  1. L124
    have hprevious : ∃ pb. ∃ pc. BetaAt(bb,bc,x,pb) ∧ (BetaAt(sb,sc,x,pc) ∧ (x = 0 ∧ (∀ y. Lt(y,w) → ∃ z. BetaAt(pb,pc,y,z) ∧ (y = 0 ∧ z = 1 ∨ (∃ n. y = S n ∧ z = 0))) ∨ (∃ y. ∃ z. ∃ n. x = S y ∧ (BetaAt(bb,bc,y,z) ∧ (BetaAt(sb,sc,y,n) ∧ (∀ m. Lt(m,w) → ∃ k. BetaAt(pb,pc,m,k) ∧ (m = 0 ∧ k = 1 ∨ (∃ i. ∃ j. ∃ u. m = S i ∧ (BetaAt(z,n,i,j) ∧ (BetaAt(z,n,S i,u) ∧ k = j + u))))))))))Definitions: BetaAt(bb,bc,x,pb)BetaAt(sb,sc,x,pc)Lt(y,w)BetaAt(pb,pc,y,z)BetaAt(bb,bc,y,z)BetaAt(sb,sc,y,n)Lt(m,w)BetaAt(pb,pc,m,k)BetaAt(z,n,i,j)BetaAt(z,n,S i,u)Original native command in the exact edition
  2. L125
    specialize htable x
  3. L126
    apply htable
  4. L127
    exact hbound
46Separate the logical casesL128–131

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

  1. L128
    cases hprevious
  2. L129
    cases hprevious_witness
  3. L130
    cases hprevious_witness_witness
  4. L131
    cases hprevious_witness_witness_right
47Establish hstepL132–136

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

  1. L132
    have hstep : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. ∃ n. ∃ m. x = S z ∧ (BetaAt(x1,x2,z,n) ∧ (BetaAt(x1,x2,S z,m) ∧ y = n + m))))Definitions: Lt(x,w)BetaAt(b,c,x,y)BetaAt(x1,x2,z,n)BetaAt(x1,x2,S z,m)Original native command in the exact edition
  2. L133
    specialize beta_pascal_row_step_exists x1
  3. L134
    specialize beta_pascal_row_step_exists x2
  4. L135
    specialize beta_pascal_row_step_exists w
  5. L136
    exact beta_pascal_row_step_exists
48Separate the logical casesL137–138

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

  1. L137
    cases hstep
  2. L138
    cases hstep_witness
49Establish hcode_extendL139–144

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

  1. L139
    have hcode_extend : ∃ db. ∃ dc. BetaAt(db,dc,r,x3) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(bb,bc,x,y) → BetaAt(db,dc,x,y))Definitions: BetaAt(db,dc,r,x3)Lt(x,r)BetaAt(bb,bc,x,y)BetaAt(db,dc,x,y)Original native command in the exact edition
  2. L140
    specialize beta_prefix_extend r
  3. L141
    specialize beta_prefix_extend bb
  4. L142
    specialize beta_prefix_extend bc
  5. L143
    specialize beta_prefix_extend x3
  6. L144
    exact beta_prefix_extend
50Separate the logical casesL145–147

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

  1. L145
    cases hcode_extend
  2. L146
    cases hcode_extend_witness
  3. L147
    cases hcode_extend_witness_witness
51Establish hscale_extendL148–153

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

  1. L148
    have hscale_extend : ∃ eb. ∃ ec. BetaAt(eb,ec,r,x4) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(sb,sc,x,y) → BetaAt(eb,ec,x,y))Definitions: BetaAt(eb,ec,r,x4)Lt(x,r)BetaAt(sb,sc,x,y)BetaAt(eb,ec,x,y)Original native command in the exact edition
  2. L149
    specialize beta_prefix_extend r
  3. L150
    specialize beta_prefix_extend sb
  4. L151
    specialize beta_prefix_extend sc
  5. L152
    specialize beta_prefix_extend x4
  6. L153
    exact beta_prefix_extend
52Separate the logical casesL154–156

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

  1. L154
    cases hscale_extend
  2. L155
    cases hscale_extend_witness
  3. L156
    cases hscale_extend_witness_witness
53Construct an explicit witnessL157–160

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

  1. L157
    exists x5
  2. L158
    exists x6
  3. L159
    exists x7
  4. L160
    exists x8
54Fix variables and assumptionsL161–162

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

  1. L161
    intro i
  2. L162
    intro hi
55Establish hsplitL163–167

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L163
    have hsplit : i = r ∨ Lt(i,r)Definitions: Lt(i,r)Original native command in the exact edition
  2. L164
    specialize finite_lt_succ_eq_or_lt r
  3. L165
    specialize finite_lt_succ_eq_or_lt i
  4. L166
    apply finite_lt_succ_eq_or_lt
  5. L167
    exact hi
56Separate the logical casesL168–168

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

  1. L168
    cases hsplit
57Construct an explicit witnessL169–170

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

  1. L169
    exists x3
  2. L170
    exists x4
58Separate the logical casesL171–171

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

  1. L171
    split
59Calculate and transport equalitiesL172–173

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

  1. L172
    rewrite hsplit_left
  2. L173
    rewrite hsplit_left
60Use earlier factsL174–174

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

  1. L174
    exact hcode_extend_witness_witness_left
61Separate the logical casesL175–175

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

  1. L175
    split
62Calculate and transport equalitiesL176–177

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

  1. L176
    rewrite hsplit_left
  2. L177
    rewrite hsplit_left
63Use earlier factsL178–178

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

  1. L178
    exact hscale_extend_witness_witness_left
64Separate the logical casesL179–179

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

  1. L179
    right
65Construct an explicit witnessL180–182

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

  1. L180
    exists x
  2. L181
    exists x1
  3. L182
    exists x2
66Separate the logical casesL183–183

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

  1. L183
    split
67Calculate and transport equalitiesL184–184

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

  1. L184
    trans r
68Use earlier factsL185–186

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

  1. L185
    exact hsplit_left
  2. L186
    exact zero_or_succ_right_witness
69Establish hpred_boundL187–190

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

  1. L187
    have hpred_bound : Lt(x,r)Definitions: Lt(x,r)Original native command in the exact edition
  2. L188
    rewrite zero_or_succ_right_witness
  3. L189
    specialize le_refl (S x)
  4. L190
    exact le_refl
70Separate the logical casesL191–191

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

  1. L191
    split
71Use earlier factsL192–196

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

  1. L192
    specialize hcode_extend_witness_witness_right x
  2. L193
    specialize hcode_extend_witness_witness_right x1
  3. L194
    apply hcode_extend_witness_witness_right
  4. L195
    exact hpred_bound
  5. L196
    exact hprevious_witness_witness_left
72Separate the logical casesL197–197

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

  1. L197
    split
73Use earlier factsL198–204

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

  1. L198
    specialize hscale_extend_witness_witness_right x
  2. L199
    specialize hscale_extend_witness_witness_right x2
  3. L200
    apply hscale_extend_witness_witness_right
  4. L201
    exact hpred_bound
  5. L202
    exact hprevious_witness_witness_right_left
  6. L203
    exact hstep_witness_witness
  7. L204
    specialize htable i
74Establish holdL205–207

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

  1. L205
    have hold : ∃ b. ∃ c. BetaAt(bb,bc,i,b) ∧ (BetaAt(sb,sc,i,c) ∧ (i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(b,c,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))Definitions: BetaAt(bb,bc,i,b)BetaAt(sb,sc,i,c)Lt(x,w)BetaAt(b,c,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(b,c,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L206
    apply htable
  3. L207
    exact hsplit_right
75Separate the logical casesL208–211

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

  1. L208
    cases hold
  2. L209
    cases hold_witness
  3. L210
    cases hold_witness_witness
  4. L211
    cases hold_witness_witness_right
76Construct an explicit witnessL212–213

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

  1. L212
    exists x9
  2. L213
    exists x10
77Separate the logical casesL214–214

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

  1. L214
    split
78Use earlier factsL215–219

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

  1. L215
    specialize hcode_extend_witness_witness_right i
  2. L216
    specialize hcode_extend_witness_witness_right x9
  3. L217
    apply hcode_extend_witness_witness_right
  4. L218
    exact hsplit_right
  5. L219
    exact hold_witness_witness_left
79Separate the logical casesL220–220

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

  1. L220
    split
80Use earlier factsL221–225

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

  1. L221
    specialize hscale_extend_witness_witness_right i
  2. L222
    specialize hscale_extend_witness_witness_right x10
  3. L223
    apply hscale_extend_witness_witness_right
  4. L224
    exact hsplit_right
  5. L225
    exact hold_witness_witness_right_left
81Separate the logical casesL226–227

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

  1. L226
    cases hold_witness_witness_right_right
  2. L227
    left
82Use earlier factsL228–228

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

  1. L228
    exact hold_witness_witness_right_right_left
83Separate the logical casesL229–235

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

  1. L229
    cases hold_witness_witness_right_right_right
  2. L230
    cases hold_witness_witness_right_right_right_witness
  3. L231
    cases hold_witness_witness_right_right_right_witness_witness
  4. L232
    cases hold_witness_witness_right_right_right_witness_witness_witness
  5. L233
    cases hold_witness_witness_right_right_right_witness_witness_witness_right
  6. L234
    cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  7. L235
    right
84Construct an explicit witnessL236–238

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

  1. L236
    exists x11
  2. L237
    exists x12
  3. L238
    exists x13
85Separate the logical casesL239–239

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

  1. L239
    split
86Use earlier factsL240–240

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

  1. L240
    exact hold_witness_witness_right_right_right_witness_witness_witness_left
87Establish hpred_boundL241–241

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

  1. L241
    have hpred_bound : Lt(x11,r)Definitions: Lt(x11,r)Original native command in the exact edition
88Establish hi_leL242–248

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt to le.

  1. L242
  2. L243
    specialize lt_to_le i
  3. L244
    specialize lt_to_le r
  4. L245
    apply lt_to_le
  5. L246
    exact hsplit_right
  6. L247
    rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  7. L248
    exact hi_le
89Separate the logical casesL249–249

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

  1. L249
    split
90Use earlier factsL250–254

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

  1. L250
    specialize hcode_extend_witness_witness_right x11
  2. L251
    specialize hcode_extend_witness_witness_right x12
  3. L252
    apply hcode_extend_witness_witness_right
  4. L253
    exact hpred_bound
  5. L254
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
91Separate the logical casesL255–255

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

  1. L255
    split
92Use earlier factsL256–261

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

  1. L256
    specialize hscale_extend_witness_witness_right x11
  2. L257
    specialize hscale_extend_witness_witness_right x13
  3. L258
    apply hscale_extend_witness_witness_right
  4. L259
    exact hpred_bound
  5. L260
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  6. L261
    exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 261 lines
  1. 0001intro bb
  2. 0002intro bc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro w
  6. 0006intro r
  7. 0007intro htable
  8. 0008specialize zero_or_succ r
  9. 0009cases zero_or_succ
  10. 0010have hzero : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))
    Exact native replay linehave hzero : exists b c. (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))
  11. 0011specialize beta_pascal_zero_row_exists w
  12. 0012exact beta_pascal_zero_row_exists
  13. 0013cases hzero
  14. 0014cases hzero_witness
  15. 0015have hcode_extend : ∃ db. ∃ dc. BetaAt(db,dc,r,x) ∧ (∀ y. ∀ z. Lt(y,r) → BetaAt(bb,bc,y,z) → BetaAt(db,dc,y,z))
    Exact native replay linehave hcode_extend : exists db dc. ((((exists bcf_height_bptpe_code_append. bcf_height_bptpe_code_append + S (x) = S ((S (r)) * dc)) /\ exists bcf_quotient_bptpe_code_append. db = bcf_quotient_bptpe_code_append * S ((S (r)) * dc) + (x))) /\ forall i a. (exists bcf_lt_gap_bptpe_code_old_bound. bcf_lt_gap_bptpe_code_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_code_old. bcf_height_bptpe_code_old + S (a) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptpe_code_old. bb = bcf_quotient_bptpe_code_old * S ((S (i)) * bc) + (a))) -> (((exists bcf_height_bptpe_code_new. bcf_height_bptpe_code_new + S (a) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptpe_code_new. db = bcf_quotient_bptpe_code_new * S ((S (i)) * dc) + (a))))
  16. 0016specialize beta_prefix_extend r
  17. 0017specialize beta_prefix_extend bb
  18. 0018specialize beta_prefix_extend bc
  19. 0019specialize beta_prefix_extend x
  20. 0020exact beta_prefix_extend
  21. 0021cases hcode_extend
  22. 0022cases hcode_extend_witness
  23. 0023cases hcode_extend_witness_witness
  24. 0024have hscale_extend : ∃ eb. ∃ ec. BetaAt(eb,ec,r,x1) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(sb,sc,x,y) → BetaAt(eb,ec,x,y))
    Exact native replay linehave hscale_extend : exists eb ec. ((((exists bcf_height_bptpe_scale_append. bcf_height_bptpe_scale_append + S (x1) = S ((S (r)) * ec)) /\ exists bcf_quotient_bptpe_scale_append. eb = bcf_quotient_bptpe_scale_append * S ((S (r)) * ec) + (x1))) /\ forall i a. (exists bcf_lt_gap_bptpe_scale_old_bound. bcf_lt_gap_bptpe_scale_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_scale_old. bcf_height_bptpe_scale_old + S (a) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptpe_scale_old. sb = bcf_quotient_bptpe_scale_old * S ((S (i)) * sc) + (a))) -> (((exists bcf_height_bptpe_scale_new. bcf_height_bptpe_scale_new + S (a) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptpe_scale_new. eb = bcf_quotient_bptpe_scale_new * S ((S (i)) * ec) + (a))))
  25. 0025specialize beta_prefix_extend r
  26. 0026specialize beta_prefix_extend sb
  27. 0027specialize beta_prefix_extend sc
  28. 0028specialize beta_prefix_extend x1
  29. 0029exact beta_prefix_extend
  30. 0030cases hscale_extend
  31. 0031cases hscale_extend_witness
  32. 0032cases hscale_extend_witness_witness
  33. 0033exists x2
  34. 0034exists x3
  35. 0035exists x4
  36. 0036exists x5
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hsplit : i = r ∨ Lt(i,r)
    Exact native replay linehave hsplit : i = r \/ exists gap. gap + S i = r
  40. 0040specialize finite_lt_succ_eq_or_lt r
  41. 0041specialize finite_lt_succ_eq_or_lt i
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hsplit
  45. 0045exists x
  46. 0046exists x1
  47. 0047split
  48. 0048rewrite hsplit_left
  49. 0049rewrite hsplit_left
  50. 0050exact hcode_extend_witness_witness_left
  51. 0051split
  52. 0052rewrite hsplit_left
  53. 0053rewrite hsplit_left
  54. 0054exact hscale_extend_witness_witness_left
  55. 0055left
  56. 0056split
  57. 0057trans r
  58. 0058exact hsplit_left
  59. 0059exact zero_or_succ_left
  60. 0060exact hzero_witness_witness
  61. 0061specialize htable i
  62. 0062have hold : ∃ b. ∃ c. BetaAt(bb,bc,i,b) ∧ (BetaAt(sb,sc,i,c) ∧ (i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(b,c,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Exact native replay linehave hold : exists b c. (((exists h. h + S b = S ((S i) * bc)) /\ exists q. bb = q * S ((S i) * bc) + b) /\ (((exists h. h + S c = S ((S i) * sc)) /\ exists q. sb = q * S ((S i) * sc) + c) /\ (((i = 0 /\ (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. i = S predecessor /\ (((exists h. h + S previous_code = S ((S predecessor) * bc)) /\ exists q. bb = q * S ((S predecessor) * bc) + previous_code) /\ (((exists h. h + S previous_scale = S ((S predecessor) * sc)) /\ exists q. sb = q * S ((S predecessor) * sc) + previous_scale) /\ forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p u v. j = S p /\ (((exists h. h + S u = S ((S p) * previous_scale)) /\ exists q. previous_code = q * S ((S p) * previous_scale) + u) /\ (((exists h. h + S v = S ((S (S p)) * previous_scale)) /\ exists q. previous_code = q * S ((S (S p)) * previous_scale) + v) /\ value = u + v))))))))))
  63. 0063apply htable
  64. 0064exact hsplit_right
  65. 0065cases hold
  66. 0066cases hold_witness
  67. 0067cases hold_witness_witness
  68. 0068cases hold_witness_witness_right
  69. 0069exists x6
  70. 0070exists x7
  71. 0071split
  72. 0072specialize hcode_extend_witness_witness_right i
  73. 0073specialize hcode_extend_witness_witness_right x6
  74. 0074apply hcode_extend_witness_witness_right
  75. 0075exact hsplit_right
  76. 0076exact hold_witness_witness_left
  77. 0077split
  78. 0078specialize hscale_extend_witness_witness_right i
  79. 0079specialize hscale_extend_witness_witness_right x7
  80. 0080apply hscale_extend_witness_witness_right
  81. 0081exact hsplit_right
  82. 0082exact hold_witness_witness_right_left
  83. 0083cases hold_witness_witness_right_right
  84. 0084left
  85. 0085exact hold_witness_witness_right_right_left
  86. 0086cases hold_witness_witness_right_right_right
  87. 0087cases hold_witness_witness_right_right_right_witness
  88. 0088cases hold_witness_witness_right_right_right_witness_witness
  89. 0089cases hold_witness_witness_right_right_right_witness_witness_witness
  90. 0090cases hold_witness_witness_right_right_right_witness_witness_witness_right
  91. 0091cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  92. 0092right
  93. 0093exists x8
  94. 0094exists x9
  95. 0095exists x10
  96. 0096split
  97. 0097exact hold_witness_witness_right_right_right_witness_witness_witness_left
  98. 0098have hpred_bound : Lt(x8,r)
    Exact native replay linehave hpred_bound : exists gap. gap + S x8 = r
  99. 0099have hi_le : Le(i,r)
    Exact native replay linehave hi_le : exists gap. gap + i = r
  100. 0100specialize lt_to_le i
  101. 0101specialize lt_to_le r
  102. 0102apply lt_to_le
  103. 0103exact hsplit_right
  104. 0104rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  105. 0105exact hi_le
  106. 0106split
  107. 0107specialize hcode_extend_witness_witness_right x8
  108. 0108specialize hcode_extend_witness_witness_right x9
  109. 0109apply hcode_extend_witness_witness_right
  110. 0110exact hpred_bound
  111. 0111exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
  112. 0112split
  113. 0113specialize hscale_extend_witness_witness_right x8
  114. 0114specialize hscale_extend_witness_witness_right x10
  115. 0115apply hscale_extend_witness_witness_right
  116. 0116exact hpred_bound
  117. 0117exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  118. 0118exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right
  119. 0119cases zero_or_succ_right
  120. 0120have hbound : Lt(x,r)
    Exact native replay linehave hbound : exists gap. gap + S x = r
  121. 0121rewrite zero_or_succ_right_witness
  122. 0122specialize le_refl (S x)
  123. 0123exact le_refl
  124. 0124have hprevious : ∃ pb. ∃ pc. BetaAt(bb,bc,x,pb) ∧ (BetaAt(sb,sc,x,pc) ∧ (x = 0 ∧ (∀ y. Lt(y,w) → ∃ z. BetaAt(pb,pc,y,z) ∧ (y = 0 ∧ z = 1 ∨ (∃ n. y = S n ∧ z = 0))) ∨ (∃ y. ∃ z. ∃ n. x = S y ∧ (BetaAt(bb,bc,y,z) ∧ (BetaAt(sb,sc,y,n) ∧ (∀ m. Lt(m,w) → ∃ k. BetaAt(pb,pc,m,k) ∧ (m = 0 ∧ k = 1 ∨ (∃ i. ∃ j. ∃ u. m = S i ∧ (BetaAt(z,n,i,j) ∧ (BetaAt(z,n,S i,u) ∧ k = j + u))))))))))
    Exact native replay linehave hprevious : exists pb pc. (((exists h. h + S pb = S ((S x) * bc)) /\ exists q. bb = q * S ((S x) * bc) + pb) /\ (((exists h. h + S pc = S ((S x) * sc)) /\ exists q. sb = q * S ((S x) * sc) + pc) /\ (((x = 0 /\ (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * pc)) /\ exists q. pb = q * S ((S j) * pc) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. x = S predecessor /\ (((exists h. h + S previous_code = S ((S predecessor) * bc)) /\ exists q. bb = q * S ((S predecessor) * bc) + previous_code) /\ (((exists h. h + S previous_scale = S ((S predecessor) * sc)) /\ exists q. sb = q * S ((S predecessor) * sc) + previous_scale) /\ forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * pc)) /\ exists q. pb = q * S ((S j) * pc) + value) /\ ((j = 0 /\ value = 1) \/ exists p u v. j = S p /\ (((exists h. h + S u = S ((S p) * previous_scale)) /\ exists q. previous_code = q * S ((S p) * previous_scale) + u) /\ (((exists h. h + S v = S ((S (S p)) * previous_scale)) /\ exists q. previous_code = q * S ((S (S p)) * previous_scale) + v) /\ value = u + v))))))))))
  125. 0125specialize htable x
  126. 0126apply htable
  127. 0127exact hbound
  128. 0128cases hprevious
  129. 0129cases hprevious_witness
  130. 0130cases hprevious_witness_witness
  131. 0131cases hprevious_witness_witness_right
  132. 0132have hstep : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. ∃ n. ∃ m. x = S z ∧ (BetaAt(x1,x2,z,n) ∧ (BetaAt(x1,x2,S z,m) ∧ y = n + m))))
    Exact native replay linehave hstep : exists b c. (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists predecessor u v. j = S predecessor /\ (((exists h. h + S u = S ((S predecessor) * x2)) /\ exists q. x1 = q * S ((S predecessor) * x2) + u) /\ (((exists h. h + S v = S ((S (S predecessor)) * x2)) /\ exists q. x1 = q * S ((S (S predecessor)) * x2) + v) /\ value = u + v)))))
  133. 0133specialize beta_pascal_row_step_exists x1
  134. 0134specialize beta_pascal_row_step_exists x2
  135. 0135specialize beta_pascal_row_step_exists w
  136. 0136exact beta_pascal_row_step_exists
  137. 0137cases hstep
  138. 0138cases hstep_witness
  139. 0139have hcode_extend : ∃ db. ∃ dc. BetaAt(db,dc,r,x3) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(bb,bc,x,y) → BetaAt(db,dc,x,y))
    Exact native replay linehave hcode_extend : exists db dc. ((((exists bcf_height_bptpe_code_append. bcf_height_bptpe_code_append + S (x3) = S ((S (r)) * dc)) /\ exists bcf_quotient_bptpe_code_append. db = bcf_quotient_bptpe_code_append * S ((S (r)) * dc) + (x3))) /\ forall i a. (exists bcf_lt_gap_bptpe_code_old_bound. bcf_lt_gap_bptpe_code_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_code_old. bcf_height_bptpe_code_old + S (a) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptpe_code_old. bb = bcf_quotient_bptpe_code_old * S ((S (i)) * bc) + (a))) -> (((exists bcf_height_bptpe_code_new. bcf_height_bptpe_code_new + S (a) = S ((S (i)) * dc)) /\ exists bcf_quotient_bptpe_code_new. db = bcf_quotient_bptpe_code_new * S ((S (i)) * dc) + (a))))
  140. 0140specialize beta_prefix_extend r
  141. 0141specialize beta_prefix_extend bb
  142. 0142specialize beta_prefix_extend bc
  143. 0143specialize beta_prefix_extend x3
  144. 0144exact beta_prefix_extend
  145. 0145cases hcode_extend
  146. 0146cases hcode_extend_witness
  147. 0147cases hcode_extend_witness_witness
  148. 0148have hscale_extend : ∃ eb. ∃ ec. BetaAt(eb,ec,r,x4) ∧ (∀ x. ∀ y. Lt(x,r) → BetaAt(sb,sc,x,y) → BetaAt(eb,ec,x,y))
    Exact native replay linehave hscale_extend : exists eb ec. ((((exists bcf_height_bptpe_scale_append. bcf_height_bptpe_scale_append + S (x4) = S ((S (r)) * ec)) /\ exists bcf_quotient_bptpe_scale_append. eb = bcf_quotient_bptpe_scale_append * S ((S (r)) * ec) + (x4))) /\ forall i a. (exists bcf_lt_gap_bptpe_scale_old_bound. bcf_lt_gap_bptpe_scale_old_bound + S (i) = r) -> (((exists bcf_height_bptpe_scale_old. bcf_height_bptpe_scale_old + S (a) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptpe_scale_old. sb = bcf_quotient_bptpe_scale_old * S ((S (i)) * sc) + (a))) -> (((exists bcf_height_bptpe_scale_new. bcf_height_bptpe_scale_new + S (a) = S ((S (i)) * ec)) /\ exists bcf_quotient_bptpe_scale_new. eb = bcf_quotient_bptpe_scale_new * S ((S (i)) * ec) + (a))))
  149. 0149specialize beta_prefix_extend r
  150. 0150specialize beta_prefix_extend sb
  151. 0151specialize beta_prefix_extend sc
  152. 0152specialize beta_prefix_extend x4
  153. 0153exact beta_prefix_extend
  154. 0154cases hscale_extend
  155. 0155cases hscale_extend_witness
  156. 0156cases hscale_extend_witness_witness
  157. 0157exists x5
  158. 0158exists x6
  159. 0159exists x7
  160. 0160exists x8
  161. 0161intro i
  162. 0162intro hi
  163. 0163have hsplit : i = r ∨ Lt(i,r)
    Exact native replay linehave hsplit : i = r \/ exists gap. gap + S i = r
  164. 0164specialize finite_lt_succ_eq_or_lt r
  165. 0165specialize finite_lt_succ_eq_or_lt i
  166. 0166apply finite_lt_succ_eq_or_lt
  167. 0167exact hi
  168. 0168cases hsplit
  169. 0169exists x3
  170. 0170exists x4
  171. 0171split
  172. 0172rewrite hsplit_left
  173. 0173rewrite hsplit_left
  174. 0174exact hcode_extend_witness_witness_left
  175. 0175split
  176. 0176rewrite hsplit_left
  177. 0177rewrite hsplit_left
  178. 0178exact hscale_extend_witness_witness_left
  179. 0179right
  180. 0180exists x
  181. 0181exists x1
  182. 0182exists x2
  183. 0183split
  184. 0184trans r
  185. 0185exact hsplit_left
  186. 0186exact zero_or_succ_right_witness
  187. 0187have hpred_bound : Lt(x,r)
    Exact native replay linehave hpred_bound : exists gap. gap + S x = r
  188. 0188rewrite zero_or_succ_right_witness
  189. 0189specialize le_refl (S x)
  190. 0190exact le_refl
  191. 0191split
  192. 0192specialize hcode_extend_witness_witness_right x
  193. 0193specialize hcode_extend_witness_witness_right x1
  194. 0194apply hcode_extend_witness_witness_right
  195. 0195exact hpred_bound
  196. 0196exact hprevious_witness_witness_left
  197. 0197split
  198. 0198specialize hscale_extend_witness_witness_right x
  199. 0199specialize hscale_extend_witness_witness_right x2
  200. 0200apply hscale_extend_witness_witness_right
  201. 0201exact hpred_bound
  202. 0202exact hprevious_witness_witness_right_left
  203. 0203exact hstep_witness_witness
  204. 0204specialize htable i
  205. 0205have hold : ∃ b. ∃ c. BetaAt(bb,bc,i,b) ∧ (BetaAt(sb,sc,i,c) ∧ (i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(b,c,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ j. ∃ u. n = S k ∧ (BetaAt(y,z,k,j) ∧ (BetaAt(y,z,S k,u) ∧ m = j + u))))))))))
    Exact native replay linehave hold : exists b c. (((exists h. h + S b = S ((S i) * bc)) /\ exists q. bb = q * S ((S i) * bc) + b) /\ (((exists h. h + S c = S ((S i) * sc)) /\ exists q. sb = q * S ((S i) * sc) + c) /\ (((i = 0 /\ (forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p. j = S p /\ value = 0)))) \/ exists predecessor previous_code previous_scale. i = S predecessor /\ (((exists h. h + S previous_code = S ((S predecessor) * bc)) /\ exists q. bb = q * S ((S predecessor) * bc) + previous_code) /\ (((exists h. h + S previous_scale = S ((S predecessor) * sc)) /\ exists q. sb = q * S ((S predecessor) * sc) + previous_scale) /\ forall j. (exists gap. gap + S j = w) -> exists value. (((exists h. h + S value = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + value) /\ ((j = 0 /\ value = 1) \/ exists p u v. j = S p /\ (((exists h. h + S u = S ((S p) * previous_scale)) /\ exists q. previous_code = q * S ((S p) * previous_scale) + u) /\ (((exists h. h + S v = S ((S (S p)) * previous_scale)) /\ exists q. previous_code = q * S ((S (S p)) * previous_scale) + v) /\ value = u + v))))))))))
  206. 0206apply htable
  207. 0207exact hsplit_right
  208. 0208cases hold
  209. 0209cases hold_witness
  210. 0210cases hold_witness_witness
  211. 0211cases hold_witness_witness_right
  212. 0212exists x9
  213. 0213exists x10
  214. 0214split
  215. 0215specialize hcode_extend_witness_witness_right i
  216. 0216specialize hcode_extend_witness_witness_right x9
  217. 0217apply hcode_extend_witness_witness_right
  218. 0218exact hsplit_right
  219. 0219exact hold_witness_witness_left
  220. 0220split
  221. 0221specialize hscale_extend_witness_witness_right i
  222. 0222specialize hscale_extend_witness_witness_right x10
  223. 0223apply hscale_extend_witness_witness_right
  224. 0224exact hsplit_right
  225. 0225exact hold_witness_witness_right_left
  226. 0226cases hold_witness_witness_right_right
  227. 0227left
  228. 0228exact hold_witness_witness_right_right_left
  229. 0229cases hold_witness_witness_right_right_right
  230. 0230cases hold_witness_witness_right_right_right_witness
  231. 0231cases hold_witness_witness_right_right_right_witness_witness
  232. 0232cases hold_witness_witness_right_right_right_witness_witness_witness
  233. 0233cases hold_witness_witness_right_right_right_witness_witness_witness_right
  234. 0234cases hold_witness_witness_right_right_right_witness_witness_witness_right_right
  235. 0235right
  236. 0236exists x11
  237. 0237exists x12
  238. 0238exists x13
  239. 0239split
  240. 0240exact hold_witness_witness_right_right_right_witness_witness_witness_left
  241. 0241have hpred_bound : Lt(x11,r)
    Exact native replay linehave hpred_bound : exists gap. gap + S x11 = r
  242. 0242have hi_le : Le(i,r)
    Exact native replay linehave hi_le : exists gap. gap + i = r
  243. 0243specialize lt_to_le i
  244. 0244specialize lt_to_le r
  245. 0245apply lt_to_le
  246. 0246exact hsplit_right
  247. 0247rewrite hold_witness_witness_right_right_right_witness_witness_witness_left at hi_le
  248. 0248exact hi_le
  249. 0249split
  250. 0250specialize hcode_extend_witness_witness_right x11
  251. 0251specialize hcode_extend_witness_witness_right x12
  252. 0252apply hcode_extend_witness_witness_right
  253. 0253exact hpred_bound
  254. 0254exact hold_witness_witness_right_right_right_witness_witness_witness_right_left
  255. 0255split
  256. 0256specialize hscale_extend_witness_witness_right x11
  257. 0257specialize hscale_extend_witness_witness_right x13
  258. 0258apply hscale_extend_witness_witness_right
  259. 0259exact hpred_bound
  260. 0260exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_left
  261. 0261exact hold_witness_witness_right_right_right_witness_witness_witness_right_right_right