BT00TH · Bertrand theorem

beta_pascal_table_successor_cell_recurrence

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

A decoded successor table cell is the sum of predecessor cells.

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. ∀ i. ∀ j. ∀ b. ∀ c. ∀ z. (∀ x. Lt(x,r) → ∃ y. ∃ n. BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,n) ∧ (x = 0 ∧ (∀ m. Lt(m,w) → ∃ k. BetaAt(y,n,m,k) ∧ (m = 0 ∧ k = 1 ∨ (∃ u. m = S u ∧ k = 0))) ∨ (∃ m. ∃ k. ∃ u. x = S m ∧ (BetaAt(bb,bc,m,k) ∧ (BetaAt(sb,sc,m,u) ∧ (∀ v. Lt(v,w) → ∃ x0. BetaAt(y,n,v,x0) ∧ (v = 0 ∧ x0 = 1 ∨ (∃ x1. ∃ x2. ∃ x3. v = S x1 ∧ (BetaAt(k,u,x1,x2) ∧ (BetaAt(k,u,S x1,x3) ∧ x0 = x2 + x3))))))))))) → Lt(S i,r) → Lt(S j,w) → BetaAt(bb,bc,S i,b) → BetaAt(sb,sc,S i,c) → BetaAt(b,c,S j,z) → ∃ x. ∃ y. ∃ n. ∃ m. BetaAt(bb,bc,i,x) ∧ (BetaAt(sb,sc,i,y) ∧ (BetaAt(x,y,j,n) ∧ (BetaAt(x,y,S j,m) ∧ z = n + m)))

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

20 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

18 occurrences

Exact expanded native-PA statement
forall bb bc sb sc w r i j b c z. (forall bcf_row_index_bptscr_table. (exists bcf_lt_gap_bptscr_table_row_bound. bcf_lt_gap_bptscr_table_row_bound + S (bcf_row_index_bptscr_table) = r) -> exists bcf_row_code_bptscr_table bcf_row_scale_bptscr_table. ((((exists bcf_height_bptscr_table_decoded_row_code. bcf_height_bptscr_table_decoded_row_code + S (bcf_row_code_bptscr_table) = S ((S (bcf_row_index_bptscr_table)) * bc)) /\ exists bcf_quotient_bptscr_table_decoded_row_code. bb = bcf_quotient_bptscr_table_decoded_row_code * S ((S (bcf_row_index_bptscr_table)) * bc) + (bcf_row_code_bptscr_table))) /\ ((((exists bcf_height_bptscr_table_decoded_row_scale. bcf_height_bptscr_table_decoded_row_scale + S (bcf_row_scale_bptscr_table) = S ((S (bcf_row_index_bptscr_table)) * sc)) /\ exists bcf_quotient_bptscr_table_decoded_row_scale. sb = bcf_quotient_bptscr_table_decoded_row_scale * S ((S (bcf_row_index_bptscr_table)) * sc) + (bcf_row_scale_bptscr_table))) /\ ((bcf_row_index_bptscr_table = 0 /\ (forall bcf_index_bptscr_table_zero_row. (exists bcf_lt_gap_bptscr_table_zero_row_bound. bcf_lt_gap_bptscr_table_zero_row_bound + S (bcf_index_bptscr_table_zero_row) = w) -> exists bcf_value_bptscr_table_zero_row. ((((exists bcf_height_bptscr_table_zero_row_entry. bcf_height_bptscr_table_zero_row_entry + S (bcf_value_bptscr_table_zero_row) = S ((S (bcf_index_bptscr_table_zero_row)) * bcf_row_scale_bptscr_table)) /\ exists bcf_quotient_bptscr_table_zero_row_entry. bcf_row_code_bptscr_table = bcf_quotient_bptscr_table_zero_row_entry * S ((S (bcf_index_bptscr_table_zero_row)) * bcf_row_scale_bptscr_table) + (bcf_value_bptscr_table_zero_row))) /\ ((bcf_index_bptscr_table_zero_row = 0 /\ bcf_value_bptscr_table_zero_row = 1) \/ exists bcf_predecessor_bptscr_table_zero_row. bcf_index_bptscr_table_zero_row = S bcf_predecessor_bptscr_table_zero_row /\ bcf_value_bptscr_table_zero_row = 0)))) \/ exists bcf_predecessor_bptscr_table bcf_previous_code_bptscr_table bcf_previous_scale_bptscr_table. bcf_row_index_bptscr_table = S bcf_predecessor_bptscr_table /\ ((((exists bcf_height_bptscr_table_decoded_previous_code. bcf_height_bptscr_table_decoded_previous_code + S (bcf_previous_code_bptscr_table) = S ((S (bcf_predecessor_bptscr_table)) * bc)) /\ exists bcf_quotient_bptscr_table_decoded_previous_code. bb = bcf_quotient_bptscr_table_decoded_previous_code * S ((S (bcf_predecessor_bptscr_table)) * bc) + (bcf_previous_code_bptscr_table))) /\ ((((exists bcf_height_bptscr_table_decoded_previous_scale. bcf_height_bptscr_table_decoded_previous_scale + S (bcf_previous_scale_bptscr_table) = S ((S (bcf_predecessor_bptscr_table)) * sc)) /\ exists bcf_quotient_bptscr_table_decoded_previous_scale. sb = bcf_quotient_bptscr_table_decoded_previous_scale * S ((S (bcf_predecessor_bptscr_table)) * sc) + (bcf_previous_scale_bptscr_table))) /\ (forall bcf_index_bptscr_table_row_step. (exists bcf_lt_gap_bptscr_table_row_step_bound. bcf_lt_gap_bptscr_table_row_step_bound + S (bcf_index_bptscr_table_row_step) = w) -> exists bcf_value_bptscr_table_row_step. ((((exists bcf_height_bptscr_table_row_step_entry. bcf_height_bptscr_table_row_step_entry + S (bcf_value_bptscr_table_row_step) = S ((S (bcf_index_bptscr_table_row_step)) * bcf_row_scale_bptscr_table)) /\ exists bcf_quotient_bptscr_table_row_step_entry. bcf_row_code_bptscr_table = bcf_quotient_bptscr_table_row_step_entry * S ((S (bcf_index_bptscr_table_row_step)) * bcf_row_scale_bptscr_table) + (bcf_value_bptscr_table_row_step))) /\ ((bcf_index_bptscr_table_row_step = 0 /\ bcf_value_bptscr_table_row_step = 1) \/ exists bcf_predecessor_bptscr_table_row_step bcf_left_bptscr_table_row_step bcf_right_bptscr_table_row_step. bcf_index_bptscr_table_row_step = S bcf_predecessor_bptscr_table_row_step /\ ((((exists bcf_height_bptscr_table_row_step_previous_left. bcf_height_bptscr_table_row_step_previous_left + S (bcf_left_bptscr_table_row_step) = S ((S (bcf_predecessor_bptscr_table_row_step)) * bcf_previous_scale_bptscr_table)) /\ exists bcf_quotient_bptscr_table_row_step_previous_left. bcf_previous_code_bptscr_table = bcf_quotient_bptscr_table_row_step_previous_left * S ((S (bcf_predecessor_bptscr_table_row_step)) * bcf_previous_scale_bptscr_table) + (bcf_left_bptscr_table_row_step))) /\ ((((exists bcf_height_bptscr_table_row_step_previous_right. bcf_height_bptscr_table_row_step_previous_right + S (bcf_right_bptscr_table_row_step) = S ((S (S (bcf_predecessor_bptscr_table_row_step))) * bcf_previous_scale_bptscr_table)) /\ exists bcf_quotient_bptscr_table_row_step_previous_right. bcf_previous_code_bptscr_table = bcf_quotient_bptscr_table_row_step_previous_right * S ((S (S (bcf_predecessor_bptscr_table_row_step))) * bcf_previous_scale_bptscr_table) + (bcf_right_bptscr_table_row_step))) /\ bcf_value_bptscr_table_row_step = bcf_left_bptscr_table_row_step + bcf_right_bptscr_table_row_step))))))))))) -> (exists bcf_lt_gap_bptscr_row_bound. bcf_lt_gap_bptscr_row_bound + S (S i) = r) -> (exists bcf_lt_gap_bptscr_cell_bound. bcf_lt_gap_bptscr_cell_bound + S (S j) = w) -> (((exists bcf_height_bptscr_row_code_at. bcf_height_bptscr_row_code_at + S (b) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptscr_row_code_at. bb = bcf_quotient_bptscr_row_code_at * S ((S (S i)) * bc) + (b))) -> (((exists bcf_height_bptscr_row_scale_at. bcf_height_bptscr_row_scale_at + S (c) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptscr_row_scale_at. sb = bcf_quotient_bptscr_row_scale_at * S ((S (S i)) * sc) + (c))) -> (((exists bcf_height_bptscr_current_at. bcf_height_bptscr_current_at + S (z) = S ((S (S j)) * c)) /\ exists bcf_quotient_bptscr_current_at. b = bcf_quotient_bptscr_current_at * S ((S (S j)) * c) + (z))) -> (exists bcf_previous_code_bptscr_result bcf_previous_scale_bptscr_result bcf_left_value_bptscr_result bcf_right_value_bptscr_result. (((exists bcf_height_bptscr_result_previous_code_at. bcf_height_bptscr_result_previous_code_at + S (bcf_previous_code_bptscr_result) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptscr_result_previous_code_at. bb = bcf_quotient_bptscr_result_previous_code_at * S ((S (i)) * bc) + (bcf_previous_code_bptscr_result))) /\ ((((exists bcf_height_bptscr_result_previous_scale_at. bcf_height_bptscr_result_previous_scale_at + S (bcf_previous_scale_bptscr_result) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptscr_result_previous_scale_at. sb = bcf_quotient_bptscr_result_previous_scale_at * S ((S (i)) * sc) + (bcf_previous_scale_bptscr_result))) /\ ((((exists bcf_height_bptscr_result_left_at. bcf_height_bptscr_result_left_at + S (bcf_left_value_bptscr_result) = S ((S (j)) * bcf_previous_scale_bptscr_result)) /\ exists bcf_quotient_bptscr_result_left_at. bcf_previous_code_bptscr_result = bcf_quotient_bptscr_result_left_at * S ((S (j)) * bcf_previous_scale_bptscr_result) + (bcf_left_value_bptscr_result))) /\ ((((exists bcf_height_bptscr_result_right_at. bcf_height_bptscr_result_right_at + S (bcf_right_value_bptscr_result) = S ((S (S (j))) * bcf_previous_scale_bptscr_result)) /\ exists bcf_quotient_bptscr_result_right_at. bcf_previous_code_bptscr_result = bcf_quotient_bptscr_result_right_at * S ((S (S (j))) * bcf_previous_scale_bptscr_result) + (bcf_right_value_bptscr_result))) /\ z = bcf_left_value_bptscr_result + bcf_right_value_bptscr_result))))

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT000C succ_ne_zero BT000D succ_injective

Direct theorem dependents

BT00TI choose_succ_succ_of_lt

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

128 script commands · 33 reading checkpoints · 12 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 (3)
beta at uniquesucc ne zerosucc injective
01Fix variables and assumptionsL1–10

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 i
  8. L8
    intro j
  9. L9
    intro b
  10. L10
    intro c
02Fix variables and assumptionsL11–17

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

  1. L11
    intro z
  2. L12
    intro htable
  3. L13
    intro hrow_bound
  4. L14
    intro hcell_bound
  5. L15
    intro hrow_code
  6. L16
    intro hrow_scale
  7. L17
    intro hcurrent
03Establish hrowL18–21

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

  1. L18
    have hrow · expand full local formula (624 characters)have hrow : ∃ bcf_row_code_bptscr_semantic_row. ∃ bcf_row_scale_bptscr_semantic_row. BetaAt(bb,bc,S i,bcf_row_code_bptscr_semantic_row) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptscr_semantic_row) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,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,S i,bcf_row_code_bptscr_semantic_row)BetaAt(sb,sc,S i,bcf_row_scale_bptscr_semantic_row)Lt(x,w)BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L19
    specialize htable (S i)
  3. L20
    apply htable
  4. L21
    exact hrow_bound
04Separate the logical casesL22–25

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

  1. L22
    cases hrow
  2. L23
    cases hrow_witness
  3. L24
    cases hrow_witness_witness
  4. L25
    cases hrow_witness_witness_right
05Establish hcodeL26–34

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

  1. L26
    have hcode : b = x
  2. L27
    specialize beta_at_unique bb
  3. L28
    specialize beta_at_unique bc
  4. L29
    specialize beta_at_unique (S i)
  5. L30
    specialize beta_at_unique b
  6. L31
    specialize beta_at_unique x
  7. L32
    apply beta_at_unique
  8. L33
    exact hrow_code
  9. L34
    exact hrow_witness_witness_left
06Establish hscaleL35–43

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

  1. L35
    have hscale : c = x1
  2. L36
    specialize beta_at_unique sb
  3. L37
    specialize beta_at_unique sc
  4. L38
    specialize beta_at_unique (S i)
  5. L39
    specialize beta_at_unique c
  6. L40
    specialize beta_at_unique x1
  7. L41
    apply beta_at_unique
  8. L42
    exact hrow_scale
  9. L43
    exact hrow_witness_witness_right_left
07Separate the logical casesL44–46

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

  1. L44
    cases hrow_witness_witness_right_right
  2. L45
    cases hrow_witness_witness_right_right_left
  3. L46
    exfalso
08Use earlier factsL47–49

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

  1. L47
    specialize succ_ne_zero i
  2. L48
    apply succ_ne_zero
  3. L49
    exact hrow_witness_witness_right_right_left_left
09Separate the logical casesL50–55

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

  1. L50
    cases hrow_witness_witness_right_right_right
  2. L51
    cases hrow_witness_witness_right_right_right_witness
  3. L52
    cases hrow_witness_witness_right_right_right_witness_witness
  4. L53
    cases hrow_witness_witness_right_right_right_witness_witness_witness
  5. L54
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  6. L55
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
10Establish hpredecessorL56–60

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

  1. L56
    have hpredecessor : i = x2
  2. L57
    specialize succ_injective i
  3. L58
    specialize succ_injective x2
  4. L59
    apply succ_injective
  5. L60
    exact hrow_witness_witness_right_right_right_witness_witness_witness_left
11Establish hprevious_codeL61–64

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

  1. L61
    have hprevious_code : BetaAt(bb,bc,i,x3)Definitions: BetaAt(bb,bc,i,x3)Original native command in the exact edition
  2. L62
    rewrite hpredecessor
  3. L63
    rewrite hpredecessor
  4. L64
    exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
12Establish hprevious_scaleL65–68

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

  1. L65
    have hprevious_scale : BetaAt(sb,sc,i,x4)Definitions: BetaAt(sb,sc,i,x4)Original native command in the exact edition
  2. L66
    rewrite hpredecessor
  3. L67
    rewrite hpredecessor
  4. L68
    exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
13Establish hsemantic_currentL69–73

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

  1. L69
    have hsemantic_current : BetaAt(x,x1,S j,z)Definitions: BetaAt(x,x1,S j,z)Original native command in the exact edition
  2. L70
    rewrite <- hcode
  3. L71
    rewrite <- hscale
  4. L72
    rewrite <- hscale
  5. L73
    exact hcurrent
14Establish hcellL74–77

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

  1. L74
    have hcell : ∃ bcf_cell_value_bptscr_semantic_cell. BetaAt(x,x1,S j,bcf_cell_value_bptscr_semantic_cell) ∧ (S j = 0 ∧ bcf_cell_value_bptscr_semantic_cell = 1 ∨ (∃ y. ∃ z. ∃ n. S j = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptscr_semantic_cell = z + n))))Definitions: BetaAt(x,x1,S j,bcf_cell_value_bptscr_semantic_cell)BetaAt(x3,x4,y,z)BetaAt(x3,x4,S y,n)Original native command in the exact edition
  2. L75
    specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S j)
  3. L76
    apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  4. L77
    exact hcell_bound
15Separate the logical casesL78–79

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

  1. L78
    cases hcell
  2. L79
    cases hcell_witness
16Establish hvalueL80–88

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

  1. L80
    have hvalue : z = x5
  2. L81
    specialize beta_at_unique x
  3. L82
    specialize beta_at_unique x1
  4. L83
    specialize beta_at_unique (S j)
  5. L84
    specialize beta_at_unique z
  6. L85
    specialize beta_at_unique x5
  7. L86
    apply beta_at_unique
  8. L87
    exact hsemantic_current
  9. L88
    exact hcell_witness_left
17Separate the logical casesL89–91

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

  1. L89
    cases hcell_witness_right
  2. L90
    cases hcell_witness_right_left
  3. L91
    exfalso
18Use earlier factsL92–94

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

  1. L92
    specialize succ_ne_zero j
  2. L93
    apply succ_ne_zero
  3. L94
    exact hcell_witness_right_left_left
19Separate the logical casesL95–100

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

  1. L95
    cases hcell_witness_right_right
  2. L96
    cases hcell_witness_right_right_witness
  3. L97
    cases hcell_witness_right_right_witness_witness
  4. L98
    cases hcell_witness_right_right_witness_witness_witness
  5. L99
    cases hcell_witness_right_right_witness_witness_witness_right
  6. L100
    cases hcell_witness_right_right_witness_witness_witness_right_right
20Establish hcell_predecessorL101–105

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

  1. L101
    have hcell_predecessor : j = x6
  2. L102
    specialize succ_injective j
  3. L103
    specialize succ_injective x6
  4. L104
    apply succ_injective
  5. L105
    exact hcell_witness_right_right_witness_witness_witness_left
21Establish hleftL106–109

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

  1. L106
    have hleft : BetaAt(x3,x4,j,x7)Definitions: BetaAt(x3,x4,j,x7)Original native command in the exact edition
  2. L107
    rewrite hcell_predecessor
  3. L108
    rewrite hcell_predecessor
  4. L109
    exact hcell_witness_right_right_witness_witness_witness_right_left
22Establish hrightL110–113

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

  1. L110
    have hright : BetaAt(x3,x4,S j,x8)Definitions: BetaAt(x3,x4,S j,x8)Original native command in the exact edition
  2. L111
    rewrite hcell_predecessor
  3. L112
    rewrite hcell_predecessor
  4. L113
    exact hcell_witness_right_right_witness_witness_witness_right_right_left
23Construct an explicit witnessL114–117

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

  1. L114
    exists x3
  2. L115
    exists x4
  3. L116
    exists x7
  4. L117
    exists x8
24Separate the logical casesL118–118

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

  1. L118
    split
25Use earlier factsL119–119

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

  1. L119
    exact hprevious_code
26Separate the logical casesL120–120

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

  1. L120
    split
27Use earlier factsL121–121

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

  1. L121
    exact hprevious_scale
28Separate the logical casesL122–122

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

  1. L122
    split
29Use earlier factsL123–123

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

  1. L123
    exact hleft
30Separate the logical casesL124–124

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

  1. L124
    split
31Use earlier factsL125–125

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

  1. L125
    exact hright
32Calculate and transport equalitiesL126–126

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

  1. L126
    trans x5
33Use earlier factsL127–128

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

  1. L127
    exact hvalue
  2. L128
    exact hcell_witness_right_right_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 128 lines
  1. 0001intro bb
  2. 0002intro bc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro w
  6. 0006intro r
  7. 0007intro i
  8. 0008intro j
  9. 0009intro b
  10. 0010intro c
  11. 0011intro z
  12. 0012intro htable
  13. 0013intro hrow_bound
  14. 0014intro hcell_bound
  15. 0015intro hrow_code
  16. 0016intro hrow_scale
  17. 0017intro hcurrent
  18. 0018have hrow : ∃ bcf_row_code_bptscr_semantic_row. ∃ bcf_row_scale_bptscr_semantic_row. BetaAt(bb,bc,S i,bcf_row_code_bptscr_semantic_row) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptscr_semantic_row) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. S i = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptscr_semantic_row,bcf_row_scale_bptscr_semantic_row,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 hrow : exists bcf_row_code_bptscr_semantic_row bcf_row_scale_bptscr_semantic_row. ((((exists bcf_height_bptscr_semantic_row_decoded_row_code. bcf_height_bptscr_semantic_row_decoded_row_code + S (bcf_row_code_bptscr_semantic_row) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_row_code. bb = bcf_quotient_bptscr_semantic_row_decoded_row_code * S ((S (S i)) * bc) + (bcf_row_code_bptscr_semantic_row))) /\ ((((exists bcf_height_bptscr_semantic_row_decoded_row_scale. bcf_height_bptscr_semantic_row_decoded_row_scale + S (bcf_row_scale_bptscr_semantic_row) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_row_scale. sb = bcf_quotient_bptscr_semantic_row_decoded_row_scale * S ((S (S i)) * sc) + (bcf_row_scale_bptscr_semantic_row))) /\ ((S i = 0 /\ (forall bcf_index_bptscr_semantic_row_zero_row. (exists bcf_lt_gap_bptscr_semantic_row_zero_row_bound. bcf_lt_gap_bptscr_semantic_row_zero_row_bound + S (bcf_index_bptscr_semantic_row_zero_row) = w) -> exists bcf_value_bptscr_semantic_row_zero_row. ((((exists bcf_height_bptscr_semantic_row_zero_row_entry. bcf_height_bptscr_semantic_row_zero_row_entry + S (bcf_value_bptscr_semantic_row_zero_row) = S ((S (bcf_index_bptscr_semantic_row_zero_row)) * bcf_row_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_zero_row_entry. bcf_row_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_zero_row_entry * S ((S (bcf_index_bptscr_semantic_row_zero_row)) * bcf_row_scale_bptscr_semantic_row) + (bcf_value_bptscr_semantic_row_zero_row))) /\ ((bcf_index_bptscr_semantic_row_zero_row = 0 /\ bcf_value_bptscr_semantic_row_zero_row = 1) \/ exists bcf_predecessor_bptscr_semantic_row_zero_row. bcf_index_bptscr_semantic_row_zero_row = S bcf_predecessor_bptscr_semantic_row_zero_row /\ bcf_value_bptscr_semantic_row_zero_row = 0)))) \/ exists bcf_predecessor_bptscr_semantic_row bcf_previous_code_bptscr_semantic_row bcf_previous_scale_bptscr_semantic_row. S i = S bcf_predecessor_bptscr_semantic_row /\ ((((exists bcf_height_bptscr_semantic_row_decoded_previous_code. bcf_height_bptscr_semantic_row_decoded_previous_code + S (bcf_previous_code_bptscr_semantic_row) = S ((S (bcf_predecessor_bptscr_semantic_row)) * bc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_previous_code. bb = bcf_quotient_bptscr_semantic_row_decoded_previous_code * S ((S (bcf_predecessor_bptscr_semantic_row)) * bc) + (bcf_previous_code_bptscr_semantic_row))) /\ ((((exists bcf_height_bptscr_semantic_row_decoded_previous_scale. bcf_height_bptscr_semantic_row_decoded_previous_scale + S (bcf_previous_scale_bptscr_semantic_row) = S ((S (bcf_predecessor_bptscr_semantic_row)) * sc)) /\ exists bcf_quotient_bptscr_semantic_row_decoded_previous_scale. sb = bcf_quotient_bptscr_semantic_row_decoded_previous_scale * S ((S (bcf_predecessor_bptscr_semantic_row)) * sc) + (bcf_previous_scale_bptscr_semantic_row))) /\ (forall bcf_index_bptscr_semantic_row_row_step. (exists bcf_lt_gap_bptscr_semantic_row_row_step_bound. bcf_lt_gap_bptscr_semantic_row_row_step_bound + S (bcf_index_bptscr_semantic_row_row_step) = w) -> exists bcf_value_bptscr_semantic_row_row_step. ((((exists bcf_height_bptscr_semantic_row_row_step_entry. bcf_height_bptscr_semantic_row_row_step_entry + S (bcf_value_bptscr_semantic_row_row_step) = S ((S (bcf_index_bptscr_semantic_row_row_step)) * bcf_row_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_entry. bcf_row_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_entry * S ((S (bcf_index_bptscr_semantic_row_row_step)) * bcf_row_scale_bptscr_semantic_row) + (bcf_value_bptscr_semantic_row_row_step))) /\ ((bcf_index_bptscr_semantic_row_row_step = 0 /\ bcf_value_bptscr_semantic_row_row_step = 1) \/ exists bcf_predecessor_bptscr_semantic_row_row_step bcf_left_bptscr_semantic_row_row_step bcf_right_bptscr_semantic_row_row_step. bcf_index_bptscr_semantic_row_row_step = S bcf_predecessor_bptscr_semantic_row_row_step /\ ((((exists bcf_height_bptscr_semantic_row_row_step_previous_left. bcf_height_bptscr_semantic_row_row_step_previous_left + S (bcf_left_bptscr_semantic_row_row_step) = S ((S (bcf_predecessor_bptscr_semantic_row_row_step)) * bcf_previous_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_previous_left. bcf_previous_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_previous_left * S ((S (bcf_predecessor_bptscr_semantic_row_row_step)) * bcf_previous_scale_bptscr_semantic_row) + (bcf_left_bptscr_semantic_row_row_step))) /\ ((((exists bcf_height_bptscr_semantic_row_row_step_previous_right. bcf_height_bptscr_semantic_row_row_step_previous_right + S (bcf_right_bptscr_semantic_row_row_step) = S ((S (S (bcf_predecessor_bptscr_semantic_row_row_step))) * bcf_previous_scale_bptscr_semantic_row)) /\ exists bcf_quotient_bptscr_semantic_row_row_step_previous_right. bcf_previous_code_bptscr_semantic_row = bcf_quotient_bptscr_semantic_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptscr_semantic_row_row_step))) * bcf_previous_scale_bptscr_semantic_row) + (bcf_right_bptscr_semantic_row_row_step))) /\ bcf_value_bptscr_semantic_row_row_step = bcf_left_bptscr_semantic_row_row_step + bcf_right_bptscr_semantic_row_row_step))))))))))
  19. 0019specialize htable (S i)
  20. 0020apply htable
  21. 0021exact hrow_bound
  22. 0022cases hrow
  23. 0023cases hrow_witness
  24. 0024cases hrow_witness_witness
  25. 0025cases hrow_witness_witness_right
  26. 0026have hcode : b = x
  27. 0027specialize beta_at_unique bb
  28. 0028specialize beta_at_unique bc
  29. 0029specialize beta_at_unique (S i)
  30. 0030specialize beta_at_unique b
  31. 0031specialize beta_at_unique x
  32. 0032apply beta_at_unique
  33. 0033exact hrow_code
  34. 0034exact hrow_witness_witness_left
  35. 0035have hscale : c = x1
  36. 0036specialize beta_at_unique sb
  37. 0037specialize beta_at_unique sc
  38. 0038specialize beta_at_unique (S i)
  39. 0039specialize beta_at_unique c
  40. 0040specialize beta_at_unique x1
  41. 0041apply beta_at_unique
  42. 0042exact hrow_scale
  43. 0043exact hrow_witness_witness_right_left
  44. 0044cases hrow_witness_witness_right_right
  45. 0045cases hrow_witness_witness_right_right_left
  46. 0046exfalso
  47. 0047specialize succ_ne_zero i
  48. 0048apply succ_ne_zero
  49. 0049exact hrow_witness_witness_right_right_left_left
  50. 0050cases hrow_witness_witness_right_right_right
  51. 0051cases hrow_witness_witness_right_right_right_witness
  52. 0052cases hrow_witness_witness_right_right_right_witness_witness
  53. 0053cases hrow_witness_witness_right_right_right_witness_witness_witness
  54. 0054cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  55. 0055cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
  56. 0056have hpredecessor : i = x2
  57. 0057specialize succ_injective i
  58. 0058specialize succ_injective x2
  59. 0059apply succ_injective
  60. 0060exact hrow_witness_witness_right_right_right_witness_witness_witness_left
  61. 0061have hprevious_code : BetaAt(bb,bc,i,x3)
    Exact native replay linehave hprevious_code : ((exists bcf_height_bptscr_previous_code_at. bcf_height_bptscr_previous_code_at + S (x3) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptscr_previous_code_at. bb = bcf_quotient_bptscr_previous_code_at * S ((S (i)) * bc) + (x3))
  62. 0062rewrite hpredecessor
  63. 0063rewrite hpredecessor
  64. 0064exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
  65. 0065have hprevious_scale : BetaAt(sb,sc,i,x4)
    Exact native replay linehave hprevious_scale : ((exists bcf_height_bptscr_previous_scale_at. bcf_height_bptscr_previous_scale_at + S (x4) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptscr_previous_scale_at. sb = bcf_quotient_bptscr_previous_scale_at * S ((S (i)) * sc) + (x4))
  66. 0066rewrite hpredecessor
  67. 0067rewrite hpredecessor
  68. 0068exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
  69. 0069have hsemantic_current : BetaAt(x,x1,S j,z)
    Exact native replay linehave hsemantic_current : ((exists bcf_height_bptscr_semantic_current_at. bcf_height_bptscr_semantic_current_at + S (z) = S ((S (S j)) * x1)) /\ exists bcf_quotient_bptscr_semantic_current_at. x = bcf_quotient_bptscr_semantic_current_at * S ((S (S j)) * x1) + (z))
  70. 0070rewrite <- hcode
  71. 0071rewrite <- hscale
  72. 0072rewrite <- hscale
  73. 0073exact hcurrent
  74. 0074have hcell : ∃ bcf_cell_value_bptscr_semantic_cell. BetaAt(x,x1,S j,bcf_cell_value_bptscr_semantic_cell) ∧ (S j = 0 ∧ bcf_cell_value_bptscr_semantic_cell = 1 ∨ (∃ y. ∃ z. ∃ n. S j = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptscr_semantic_cell = z + n))))
    Exact native replay linehave hcell : exists bcf_cell_value_bptscr_semantic_cell. ((((exists bcf_height_bptscr_semantic_cell_entry. bcf_height_bptscr_semantic_cell_entry + S (bcf_cell_value_bptscr_semantic_cell) = S ((S (S j)) * x1)) /\ exists bcf_quotient_bptscr_semantic_cell_entry. x = bcf_quotient_bptscr_semantic_cell_entry * S ((S (S j)) * x1) + (bcf_cell_value_bptscr_semantic_cell))) /\ ((S j = 0 /\ bcf_cell_value_bptscr_semantic_cell = 1) \/ exists bcf_cell_predecessor_bptscr_semantic_cell bcf_cell_left_bptscr_semantic_cell bcf_cell_right_bptscr_semantic_cell. S j = S bcf_cell_predecessor_bptscr_semantic_cell /\ ((((exists bcf_height_bptscr_semantic_cell_previous_left. bcf_height_bptscr_semantic_cell_previous_left + S (bcf_cell_left_bptscr_semantic_cell) = S ((S (bcf_cell_predecessor_bptscr_semantic_cell)) * x4)) /\ exists bcf_quotient_bptscr_semantic_cell_previous_left. x3 = bcf_quotient_bptscr_semantic_cell_previous_left * S ((S (bcf_cell_predecessor_bptscr_semantic_cell)) * x4) + (bcf_cell_left_bptscr_semantic_cell))) /\ ((((exists bcf_height_bptscr_semantic_cell_previous_right. bcf_height_bptscr_semantic_cell_previous_right + S (bcf_cell_right_bptscr_semantic_cell) = S ((S (S (bcf_cell_predecessor_bptscr_semantic_cell))) * x4)) /\ exists bcf_quotient_bptscr_semantic_cell_previous_right. x3 = bcf_quotient_bptscr_semantic_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptscr_semantic_cell))) * x4) + (bcf_cell_right_bptscr_semantic_cell))) /\ bcf_cell_value_bptscr_semantic_cell = bcf_cell_left_bptscr_semantic_cell + bcf_cell_right_bptscr_semantic_cell))))
  75. 0075specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S j)
  76. 0076apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  77. 0077exact hcell_bound
  78. 0078cases hcell
  79. 0079cases hcell_witness
  80. 0080have hvalue : z = x5
  81. 0081specialize beta_at_unique x
  82. 0082specialize beta_at_unique x1
  83. 0083specialize beta_at_unique (S j)
  84. 0084specialize beta_at_unique z
  85. 0085specialize beta_at_unique x5
  86. 0086apply beta_at_unique
  87. 0087exact hsemantic_current
  88. 0088exact hcell_witness_left
  89. 0089cases hcell_witness_right
  90. 0090cases hcell_witness_right_left
  91. 0091exfalso
  92. 0092specialize succ_ne_zero j
  93. 0093apply succ_ne_zero
  94. 0094exact hcell_witness_right_left_left
  95. 0095cases hcell_witness_right_right
  96. 0096cases hcell_witness_right_right_witness
  97. 0097cases hcell_witness_right_right_witness_witness
  98. 0098cases hcell_witness_right_right_witness_witness_witness
  99. 0099cases hcell_witness_right_right_witness_witness_witness_right
  100. 0100cases hcell_witness_right_right_witness_witness_witness_right_right
  101. 0101have hcell_predecessor : j = x6
  102. 0102specialize succ_injective j
  103. 0103specialize succ_injective x6
  104. 0104apply succ_injective
  105. 0105exact hcell_witness_right_right_witness_witness_witness_left
  106. 0106have hleft : BetaAt(x3,x4,j,x7)
    Exact native replay linehave hleft : ((exists bcf_height_bptscr_returned_left_at. bcf_height_bptscr_returned_left_at + S (x7) = S ((S (j)) * x4)) /\ exists bcf_quotient_bptscr_returned_left_at. x3 = bcf_quotient_bptscr_returned_left_at * S ((S (j)) * x4) + (x7))
  107. 0107rewrite hcell_predecessor
  108. 0108rewrite hcell_predecessor
  109. 0109exact hcell_witness_right_right_witness_witness_witness_right_left
  110. 0110have hright : BetaAt(x3,x4,S j,x8)
    Exact native replay linehave hright : ((exists bcf_height_bptscr_returned_right_at. bcf_height_bptscr_returned_right_at + S (x8) = S ((S (S j)) * x4)) /\ exists bcf_quotient_bptscr_returned_right_at. x3 = bcf_quotient_bptscr_returned_right_at * S ((S (S j)) * x4) + (x8))
  111. 0111rewrite hcell_predecessor
  112. 0112rewrite hcell_predecessor
  113. 0113exact hcell_witness_right_right_witness_witness_witness_right_right_left
  114. 0114exists x3
  115. 0115exists x4
  116. 0116exists x7
  117. 0117exists x8
  118. 0118split
  119. 0119exact hprevious_code
  120. 0120split
  121. 0121exact hprevious_scale
  122. 0122split
  123. 0123exact hleft
  124. 0124split
  125. 0125exact hright
  126. 0126trans x5
  127. 0127exact hvalue
  128. 0128exact hcell_witness_right_right_witness_witness_witness_right_right_right