BT00TF · Bertrand theorem

beta_pascal_table_diagonal_boundary

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

Every decoded Pascal row has diagonal one and zeros above it.

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. Lt(x,r) → ∀ y. ∀ z. BetaAt(bb,bc,x,y) → BetaAt(sb,sc,x,z) → (Lt(x,w) → ∀ n. BetaAt(y,z,x,n) → n = 1) ∧ (∀ n. ∀ m. Lt(x,n) → Lt(n,w) → BetaAt(y,z,n,m) → m = 0)

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

19 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

59 occurrences

Exact expanded native-PA statement
forall bb bc sb sc w r. (forall bcf_row_index_bptdb_table. (exists bcf_lt_gap_bptdb_table_row_bound. bcf_lt_gap_bptdb_table_row_bound + S (bcf_row_index_bptdb_table) = r) -> exists bcf_row_code_bptdb_table bcf_row_scale_bptdb_table. ((((exists bcf_height_bptdb_table_decoded_row_code. bcf_height_bptdb_table_decoded_row_code + S (bcf_row_code_bptdb_table) = S ((S (bcf_row_index_bptdb_table)) * bc)) /\ exists bcf_quotient_bptdb_table_decoded_row_code. bb = bcf_quotient_bptdb_table_decoded_row_code * S ((S (bcf_row_index_bptdb_table)) * bc) + (bcf_row_code_bptdb_table))) /\ ((((exists bcf_height_bptdb_table_decoded_row_scale. bcf_height_bptdb_table_decoded_row_scale + S (bcf_row_scale_bptdb_table) = S ((S (bcf_row_index_bptdb_table)) * sc)) /\ exists bcf_quotient_bptdb_table_decoded_row_scale. sb = bcf_quotient_bptdb_table_decoded_row_scale * S ((S (bcf_row_index_bptdb_table)) * sc) + (bcf_row_scale_bptdb_table))) /\ ((bcf_row_index_bptdb_table = 0 /\ (forall bcf_index_bptdb_table_zero_row. (exists bcf_lt_gap_bptdb_table_zero_row_bound. bcf_lt_gap_bptdb_table_zero_row_bound + S (bcf_index_bptdb_table_zero_row) = w) -> exists bcf_value_bptdb_table_zero_row. ((((exists bcf_height_bptdb_table_zero_row_entry. bcf_height_bptdb_table_zero_row_entry + S (bcf_value_bptdb_table_zero_row) = S ((S (bcf_index_bptdb_table_zero_row)) * bcf_row_scale_bptdb_table)) /\ exists bcf_quotient_bptdb_table_zero_row_entry. bcf_row_code_bptdb_table = bcf_quotient_bptdb_table_zero_row_entry * S ((S (bcf_index_bptdb_table_zero_row)) * bcf_row_scale_bptdb_table) + (bcf_value_bptdb_table_zero_row))) /\ ((bcf_index_bptdb_table_zero_row = 0 /\ bcf_value_bptdb_table_zero_row = 1) \/ exists bcf_predecessor_bptdb_table_zero_row. bcf_index_bptdb_table_zero_row = S bcf_predecessor_bptdb_table_zero_row /\ bcf_value_bptdb_table_zero_row = 0)))) \/ exists bcf_predecessor_bptdb_table bcf_previous_code_bptdb_table bcf_previous_scale_bptdb_table. bcf_row_index_bptdb_table = S bcf_predecessor_bptdb_table /\ ((((exists bcf_height_bptdb_table_decoded_previous_code. bcf_height_bptdb_table_decoded_previous_code + S (bcf_previous_code_bptdb_table) = S ((S (bcf_predecessor_bptdb_table)) * bc)) /\ exists bcf_quotient_bptdb_table_decoded_previous_code. bb = bcf_quotient_bptdb_table_decoded_previous_code * S ((S (bcf_predecessor_bptdb_table)) * bc) + (bcf_previous_code_bptdb_table))) /\ ((((exists bcf_height_bptdb_table_decoded_previous_scale. bcf_height_bptdb_table_decoded_previous_scale + S (bcf_previous_scale_bptdb_table) = S ((S (bcf_predecessor_bptdb_table)) * sc)) /\ exists bcf_quotient_bptdb_table_decoded_previous_scale. sb = bcf_quotient_bptdb_table_decoded_previous_scale * S ((S (bcf_predecessor_bptdb_table)) * sc) + (bcf_previous_scale_bptdb_table))) /\ (forall bcf_index_bptdb_table_row_step. (exists bcf_lt_gap_bptdb_table_row_step_bound. bcf_lt_gap_bptdb_table_row_step_bound + S (bcf_index_bptdb_table_row_step) = w) -> exists bcf_value_bptdb_table_row_step. ((((exists bcf_height_bptdb_table_row_step_entry. bcf_height_bptdb_table_row_step_entry + S (bcf_value_bptdb_table_row_step) = S ((S (bcf_index_bptdb_table_row_step)) * bcf_row_scale_bptdb_table)) /\ exists bcf_quotient_bptdb_table_row_step_entry. bcf_row_code_bptdb_table = bcf_quotient_bptdb_table_row_step_entry * S ((S (bcf_index_bptdb_table_row_step)) * bcf_row_scale_bptdb_table) + (bcf_value_bptdb_table_row_step))) /\ ((bcf_index_bptdb_table_row_step = 0 /\ bcf_value_bptdb_table_row_step = 1) \/ exists bcf_predecessor_bptdb_table_row_step bcf_left_bptdb_table_row_step bcf_right_bptdb_table_row_step. bcf_index_bptdb_table_row_step = S bcf_predecessor_bptdb_table_row_step /\ ((((exists bcf_height_bptdb_table_row_step_previous_left. bcf_height_bptdb_table_row_step_previous_left + S (bcf_left_bptdb_table_row_step) = S ((S (bcf_predecessor_bptdb_table_row_step)) * bcf_previous_scale_bptdb_table)) /\ exists bcf_quotient_bptdb_table_row_step_previous_left. bcf_previous_code_bptdb_table = bcf_quotient_bptdb_table_row_step_previous_left * S ((S (bcf_predecessor_bptdb_table_row_step)) * bcf_previous_scale_bptdb_table) + (bcf_left_bptdb_table_row_step))) /\ ((((exists bcf_height_bptdb_table_row_step_previous_right. bcf_height_bptdb_table_row_step_previous_right + S (bcf_right_bptdb_table_row_step) = S ((S (S (bcf_predecessor_bptdb_table_row_step))) * bcf_previous_scale_bptdb_table)) /\ exists bcf_quotient_bptdb_table_row_step_previous_right. bcf_previous_code_bptdb_table = bcf_quotient_bptdb_table_row_step_previous_right * S ((S (S (bcf_predecessor_bptdb_table_row_step))) * bcf_previous_scale_bptdb_table) + (bcf_right_bptdb_table_row_step))) /\ bcf_value_bptdb_table_row_step = bcf_left_bptdb_table_row_step + bcf_right_bptdb_table_row_step))))))))))) -> forall i. (exists bcf_lt_gap_bptdb_row_bound. bcf_lt_gap_bptdb_row_bound + S (i) = r) -> forall b c. (((exists bcf_height_bptdb_row_code_at. bcf_height_bptdb_row_code_at + S (b) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptdb_row_code_at. bb = bcf_quotient_bptdb_row_code_at * S ((S (i)) * bc) + (b))) -> (((exists bcf_height_bptdb_row_scale_at. bcf_height_bptdb_row_scale_at + S (c) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptdb_row_scale_at. sb = bcf_quotient_bptdb_row_scale_at * S ((S (i)) * sc) + (c))) -> ((((exists bcf_lt_gap_bptdb_boundary_diagonal_bound. bcf_lt_gap_bptdb_boundary_diagonal_bound + S (i) = w) -> forall bcf_diagonal_value_bptdb_boundary. (((exists bcf_height_bptdb_boundary_diagonal_at. bcf_height_bptdb_boundary_diagonal_at + S (bcf_diagonal_value_bptdb_boundary) = S ((S (i)) * c)) /\ exists bcf_quotient_bptdb_boundary_diagonal_at. b = bcf_quotient_bptdb_boundary_diagonal_at * S ((S (i)) * c) + (bcf_diagonal_value_bptdb_boundary))) -> bcf_diagonal_value_bptdb_boundary = 1) /\ forall bcf_above_index_bptdb_boundary bcf_above_value_bptdb_boundary. (exists bcf_lt_gap_bptdb_boundary_above_order. bcf_lt_gap_bptdb_boundary_above_order + S (i) = bcf_above_index_bptdb_boundary) -> (exists bcf_lt_gap_bptdb_boundary_above_bound. bcf_lt_gap_bptdb_boundary_above_bound + S (bcf_above_index_bptdb_boundary) = w) -> (((exists bcf_height_bptdb_boundary_above_at. bcf_height_bptdb_boundary_above_at + S (bcf_above_value_bptdb_boundary) = S ((S (bcf_above_index_bptdb_boundary)) * c)) /\ exists bcf_quotient_bptdb_boundary_above_at. b = bcf_quotient_bptdb_boundary_above_at * S ((S (bcf_above_index_bptdb_boundary)) * c) + (bcf_above_value_bptdb_boundary))) -> bcf_above_value_bptdb_boundary = 0))

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT000C succ_ne_zero BT000D succ_injective BT0017 le_of_succ_le_succ BT0019 lt_to_le BT000E le_refl BT0042 beta_at_unique

Direct theorem dependents

BT00TG choose_self

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

369 script commands · 83 reading checkpoints · 45 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)
add eq zero rightsucc ne zerosucc injectivele of succ le succlt to lele reflbeta at unique
01Fix variables and assumptionsL1–8

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
  8. L8
    intro i
02Induction on iL9–14

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L9
    induction i
  2. L10
    intro hir
  3. L11
    intro b
  4. L12
    intro c
  5. L13
    intro hbb
  6. L14
    intro hsb
03Establish hrowL15–18

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

  1. L15
    have hrow : ∃ bcf_row_code_bptdb_base_row. ∃ bcf_row_scale_bptdb_base_row. BetaAt(bb,bc,0,bcf_row_code_bptdb_base_row) ∧ (BetaAt(sb,sc,0,bcf_row_scale_bptdb_base_row) ∧ (0 = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))Definitions: BetaAt(bb,bc,0,bcf_row_code_bptdb_base_row)BetaAt(sb,sc,0,bcf_row_scale_bptdb_base_row)Lt(x,w)BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,n,m)BetaAt(y,z,k,i)BetaAt(y,z,S k,j)Original native command in the exact edition
  2. L16
    specialize htable 0
  3. L17
    apply htable
  4. L18
    exact hir
04Separate the logical casesL19–22

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

  1. L19
    cases hrow
  2. L20
    cases hrow_witness
  3. L21
    cases hrow_witness_witness
  4. L22
    cases hrow_witness_witness_right
05Establish hcodeL23–31

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

  1. L23
    have hcode : b = x
  2. L24
    specialize beta_at_unique bb
  3. L25
    specialize beta_at_unique bc
  4. L26
    specialize beta_at_unique 0
  5. L27
    specialize beta_at_unique b
  6. L28
    specialize beta_at_unique x
  7. L29
    apply beta_at_unique
  8. L30
    exact hbb
  9. L31
    exact hrow_witness_witness_left
06Establish hscaleL32–40

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

  1. L32
    have hscale : c = x1
  2. L33
    specialize beta_at_unique sb
  3. L34
    specialize beta_at_unique sc
  4. L35
    specialize beta_at_unique 0
  5. L36
    specialize beta_at_unique c
  6. L37
    specialize beta_at_unique x1
  7. L38
    apply beta_at_unique
  8. L39
    exact hsb
  9. L40
    exact hrow_witness_witness_right_left
07Separate the logical casesL41–43

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

  1. L41
    cases hrow_witness_witness_right_right
  2. L42
    cases hrow_witness_witness_right_right_left
  3. L43
    split
08Fix variables and assumptionsL44–46

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

  1. L44
    intro hiw
  2. L45
    intro z
  3. L46
    intro htarget
09Establish hsemanticL47–51

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

  1. L47
    have hsemantic : BetaAt(x,x1,0,z)Definitions: BetaAt(x,x1,0,z)Original native command in the exact edition
  2. L48
    rewrite <- hcode
  3. L49
    rewrite <- hscale
  4. L50
    rewrite <- hscale
  5. L51
    exact htarget
10Establish hcellL52–55

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

  1. L52
    have hcell : ∃ bcf_cell_value_bptdb_base_diagonal_cell. BetaAt(x,x1,0,bcf_cell_value_bptdb_base_diagonal_cell) ∧ (0 = 0 ∧ bcf_cell_value_bptdb_base_diagonal_cell = 1 ∨ (∃ y. 0 = S y ∧ bcf_cell_value_bptdb_base_diagonal_cell = 0))Definitions: BetaAt(x,x1,0,bcf_cell_value_bptdb_base_diagonal_cell)Original native command in the exact edition
  2. L53
    specialize hrow_witness_witness_right_right_left_right 0
  3. L54
    apply hrow_witness_witness_right_right_left_right
  4. L55
    exact hiw
11Separate the logical casesL56–57

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

  1. L56
    cases hcell
  2. L57
    cases hcell_witness
12Establish hvalueL58–66

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

  1. L58
    have hvalue : z = x2
  2. L59
    specialize beta_at_unique x
  3. L60
    specialize beta_at_unique x1
  4. L61
    specialize beta_at_unique 0
  5. L62
    specialize beta_at_unique z
  6. L63
    specialize beta_at_unique x2
  7. L64
    apply beta_at_unique
  8. L65
    exact hsemantic
  9. L66
    exact hcell_witness_left
13Separate the logical casesL67–68

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

  1. L67
    cases hcell_witness_right
  2. L68
    cases hcell_witness_right_left
14Calculate and transport equalitiesL69–69

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

  1. L69
    trans x2
15Use earlier factsL70–71

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

  1. L70
    exact hvalue
  2. L71
    exact hcell_witness_right_left_right
16Separate the logical casesL72–74

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

  1. L72
    cases hcell_witness_right_right
  2. L73
    cases hcell_witness_right_right_witness
  3. L74
    exfalso
17Establish hbadL75–84

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

  1. L75
    have hbad : S x3 = 0
  2. L76
    symm
  3. L77
    exact hcell_witness_right_right_witness_left
  4. L78
    specialize succ_ne_zero x3
  5. L79
    apply succ_ne_zero
  6. L80
    exact hbad
  7. L81
    intro j
  8. L82
    intro z
  9. L83
    intro hij
  10. L84
    intro hjw
18Fix variables and assumptionsL85–85

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

  1. L85
    intro htarget
19Establish hsemanticL86–90

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

  1. L86
    have hsemantic : BetaAt(x,x1,j,z)Definitions: BetaAt(x,x1,j,z)Original native command in the exact edition
  2. L87
    rewrite <- hcode
  3. L88
    rewrite <- hscale
  4. L89
    rewrite <- hscale
  5. L90
    exact htarget
20Establish hcellL91–94

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

  1. L91
    have hcell : ∃ bcf_cell_value_bptdb_base_above_cell. BetaAt(x,x1,j,bcf_cell_value_bptdb_base_above_cell) ∧ (j = 0 ∧ bcf_cell_value_bptdb_base_above_cell = 1 ∨ (∃ y. j = S y ∧ bcf_cell_value_bptdb_base_above_cell = 0))Definitions: BetaAt(x,x1,j,bcf_cell_value_bptdb_base_above_cell)Original native command in the exact edition
  2. L92
    specialize hrow_witness_witness_right_right_left_right j
  3. L93
    apply hrow_witness_witness_right_right_left_right
  4. L94
    exact hjw
21Separate the logical casesL95–96

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

  1. L95
    cases hcell
  2. L96
    cases hcell_witness
22Establish hvalueL97–105

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

  1. L97
    have hvalue : z = x2
  2. L98
    specialize beta_at_unique x
  3. L99
    specialize beta_at_unique x1
  4. L100
    specialize beta_at_unique j
  5. L101
    specialize beta_at_unique z
  6. L102
    specialize beta_at_unique x2
  7. L103
    apply beta_at_unique
  8. L104
    exact hsemantic
  9. L105
    exact hcell_witness_left
23Separate the logical casesL106–108

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

  1. L106
    cases hcell_witness_right
  2. L107
    cases hcell_witness_right_left
  3. L108
    cases hij
24Establish hbadL109–115

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

  1. L109
    have hbad : S 0 = 0
  2. L110
    specialize add_eq_zero_right x3
  3. L111
    specialize add_eq_zero_right (S 0)
  4. L112
    apply add_eq_zero_right
  5. L113
    trans j
  6. L114
    exact hij_witness
  7. L115
    exact hcell_witness_right_left_left
25Separate the logical casesL116–116

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

  1. L116
    exfalso
26Use earlier factsL117–119

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

  1. L117
    specialize succ_ne_zero 0
  2. L118
    apply succ_ne_zero
  3. L119
    exact hbad
27Separate the logical casesL120–121

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

  1. L120
    cases hcell_witness_right_right
  2. L121
    cases hcell_witness_right_right_witness
28Calculate and transport equalitiesL122–122

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

  1. L122
    trans x2
29Use earlier factsL123–124

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

  1. L123
    exact hvalue
  2. L124
    exact hcell_witness_right_right_witness_right
30Separate the logical casesL125–129

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

  1. L125
    cases hrow_witness_witness_right_right_right
  2. L126
    cases hrow_witness_witness_right_right_right_witness
  3. L127
    cases hrow_witness_witness_right_right_right_witness_witness
  4. L128
    cases hrow_witness_witness_right_right_right_witness_witness_witness
  5. L129
    exfalso
31Establish hbadL130–139

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

  1. L130
    have hbad : S x2 = 0
  2. L131
    symm
  3. L132
    exact hrow_witness_witness_right_right_right_witness_witness_witness_left
  4. L133
    specialize succ_ne_zero x2
  5. L134
    apply succ_ne_zero
  6. L135
    exact hbad
  7. L136
    intro hir
  8. L137
    intro b
  9. L138
    intro c
  10. L139
    intro hbb
32Fix variables and assumptionsL140–140

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

  1. L140
    intro hsb
33Establish hrowL141–144

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

  1. L141
    have hrow : ∃ bcf_row_code_bptdb_step_row. ∃ bcf_row_scale_bptdb_step_row. BetaAt(bb,bc,S i,bcf_row_code_bptdb_step_row) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptdb_step_row) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptdb_step_row,bcf_row_scale_bptdb_step_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_bptdb_step_row,bcf_row_scale_bptdb_step_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_bptdb_step_row)BetaAt(sb,sc,S i,bcf_row_scale_bptdb_step_row)Lt(x,w)BetaAt(bcf_row_code_bptdb_step_row,bcf_row_scale_bptdb_step_row,x,y)BetaAt(bb,bc,x,y)BetaAt(sb,sc,x,z)Lt(n,w)BetaAt(bcf_row_code_bptdb_step_row,bcf_row_scale_bptdb_step_row,n,m)BetaAt(y,z,k,j)BetaAt(y,z,S k,u)Original native command in the exact edition
  2. L142
    specialize htable (S i)
  3. L143
    apply htable
  4. L144
    exact hir
34Separate the logical casesL145–148

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

  1. L145
    cases hrow
  2. L146
    cases hrow_witness
  3. L147
    cases hrow_witness_witness
  4. L148
    cases hrow_witness_witness_right
35Establish hcodeL149–157

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

  1. L149
    have hcode : b = x
  2. L150
    specialize beta_at_unique bb
  3. L151
    specialize beta_at_unique bc
  4. L152
    specialize beta_at_unique (S i)
  5. L153
    specialize beta_at_unique b
  6. L154
    specialize beta_at_unique x
  7. L155
    apply beta_at_unique
  8. L156
    exact hbb
  9. L157
    exact hrow_witness_witness_left
36Establish hscaleL158–166

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

  1. L158
    have hscale : c = x1
  2. L159
    specialize beta_at_unique sb
  3. L160
    specialize beta_at_unique sc
  4. L161
    specialize beta_at_unique (S i)
  5. L162
    specialize beta_at_unique c
  6. L163
    specialize beta_at_unique x1
  7. L164
    apply beta_at_unique
  8. L165
    exact hsb
  9. L166
    exact hrow_witness_witness_right_left
37Separate the logical casesL167–169

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

  1. L167
    cases hrow_witness_witness_right_right
  2. L168
    cases hrow_witness_witness_right_right_left
  3. L169
    exfalso
38Use earlier factsL170–172

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

  1. L170
    specialize succ_ne_zero i
  2. L171
    apply succ_ne_zero
  3. L172
    exact hrow_witness_witness_right_right_left_left
39Separate the logical casesL173–178

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

  1. L173
    cases hrow_witness_witness_right_right_right
  2. L174
    cases hrow_witness_witness_right_right_right_witness
  3. L175
    cases hrow_witness_witness_right_right_right_witness_witness
  4. L176
    cases hrow_witness_witness_right_right_right_witness_witness_witness
  5. L177
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  6. L178
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
40Establish hpredecessorL179–183

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

  1. L179
    have hpredecessor : i = x2
  2. L180
    specialize succ_injective i
  3. L181
    specialize succ_injective x2
  4. L182
    apply succ_injective
  5. L183
    exact hrow_witness_witness_right_right_right_witness_witness_witness_left
41Establish hprevious_row_boundL184–188

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

  1. L184
    have hprevious_row_bound : Lt(i,r)Definitions: Lt(i,r)Original native command in the exact edition
  2. L185
    specialize lt_to_le (S i)
  3. L186
    specialize lt_to_le r
  4. L187
    apply lt_to_le
  5. L188
    exact hir
42Establish hprevious_codeL189–192

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

  1. L189
    have hprevious_code : BetaAt(bb,bc,i,x3)Definitions: BetaAt(bb,bc,i,x3)Original native command in the exact edition
  2. L190
    rewrite hpredecessor
  3. L191
    rewrite hpredecessor
  4. L192
    exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
43Establish hprevious_scaleL193–196

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

  1. L193
    have hprevious_scale : BetaAt(sb,sc,i,x4)Definitions: BetaAt(sb,sc,i,x4)Original native command in the exact edition
  2. L194
    rewrite hpredecessor
  3. L195
    rewrite hpredecessor
  4. L196
    exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
44Establish hprevious_familyL197–199

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

  1. L197
    have hprevious_family : ∀ bcf_row_code_bptdb_previous_family. ∀ bcf_row_scale_bptdb_previous_family. BetaAt(bb,bc,i,bcf_row_code_bptdb_previous_family) → BetaAt(sb,sc,i,bcf_row_scale_bptdb_previous_family) → (Lt(i,w) → ∀ x. BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,i,x) → x = 1) ∧ (∀ x. ∀ y. Lt(i,x) → Lt(x,w) → BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,x,y) → y = 0)Definitions: BetaAt(bb,bc,i,bcf_row_code_bptdb_previous_family)BetaAt(sb,sc,i,bcf_row_scale_bptdb_previous_family)Lt(i,w)BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,i,x)Lt(i,x)Lt(x,w)BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,x,y)Original native command in the exact edition
  2. L198
    apply IH
  3. L199
    exact hprevious_row_bound
45Establish hprevious_boundaryL200–205

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

  1. L200
    have hprevious_boundary : (Lt(i,w) → ∀ x. BetaAt(x3,x4,i,x) → x = 1) ∧ (∀ x. ∀ y. Lt(i,x) → Lt(x,w) → BetaAt(x3,x4,x,y) → y = 0)Definitions: Lt(i,w)BetaAt(x3,x4,i,x)Lt(i,x)Lt(x,w)BetaAt(x3,x4,x,y)Original native command in the exact edition
  2. L201
    specialize hprevious_family x3
  3. L202
    specialize hprevious_family x4
  4. L203
    apply hprevious_family
  5. L204
    exact hprevious_code
  6. L205
    exact hprevious_scale
46Separate the logical casesL206–207

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

  1. L206
    cases hprevious_boundary
  2. L207
    split
47Fix variables and assumptionsL208–210

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

  1. L208
    intro hiw
  2. L209
    intro z
  3. L210
    intro htarget
48Establish hsemanticL211–215

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

  1. L211
    have hsemantic : BetaAt(x,x1,S i,z)Definitions: BetaAt(x,x1,S i,z)Original native command in the exact edition
  2. L212
    rewrite <- hcode
  3. L213
    rewrite <- hscale
  4. L214
    rewrite <- hscale
  5. L215
    exact htarget
49Establish hcellL216–219

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. L216
    have hcell : ∃ bcf_cell_value_bptdb_step_diagonal_cell. BetaAt(x,x1,S i,bcf_cell_value_bptdb_step_diagonal_cell) ∧ (S i = 0 ∧ bcf_cell_value_bptdb_step_diagonal_cell = 1 ∨ (∃ y. ∃ z. ∃ n. S i = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptdb_step_diagonal_cell = z + n))))Definitions: BetaAt(x,x1,S i,bcf_cell_value_bptdb_step_diagonal_cell)BetaAt(x3,x4,y,z)BetaAt(x3,x4,S y,n)Original native command in the exact edition
  2. L217
    specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S i)
  3. L218
    apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  4. L219
    exact hiw
50Separate the logical casesL220–221

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

  1. L220
    cases hcell
  2. L221
    cases hcell_witness
51Establish hvalueL222–230

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

  1. L222
    have hvalue : z = x5
  2. L223
    specialize beta_at_unique x
  3. L224
    specialize beta_at_unique x1
  4. L225
    specialize beta_at_unique (S i)
  5. L226
    specialize beta_at_unique z
  6. L227
    specialize beta_at_unique x5
  7. L228
    apply beta_at_unique
  8. L229
    exact hsemantic
  9. L230
    exact hcell_witness_left
52Separate the logical casesL231–233

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

  1. L231
    cases hcell_witness_right
  2. L232
    cases hcell_witness_right_left
  3. L233
    exfalso
53Use earlier factsL234–236

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

  1. L234
    specialize succ_ne_zero i
  2. L235
    apply succ_ne_zero
  3. L236
    exact hcell_witness_right_left_left
54Separate the logical casesL237–242

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

  1. L237
    cases hcell_witness_right_right
  2. L238
    cases hcell_witness_right_right_witness
  3. L239
    cases hcell_witness_right_right_witness_witness
  4. L240
    cases hcell_witness_right_right_witness_witness_witness
  5. L241
    cases hcell_witness_right_right_witness_witness_witness_right
  6. L242
    cases hcell_witness_right_right_witness_witness_witness_right_right
55Establish hcell_predecessorL243–247

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

  1. L243
    have hcell_predecessor : i = x6
  2. L244
    specialize succ_injective i
  3. L245
    specialize succ_injective x6
  4. L246
    apply succ_injective
  5. L247
    exact hcell_witness_right_right_witness_witness_witness_left
56Establish hleft_atL248–251

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

  1. L248
    have hleft_at : BetaAt(x3,x4,i,x7)Definitions: BetaAt(x3,x4,i,x7)Original native command in the exact edition
  2. L249
    rewrite hcell_predecessor
  3. L250
    rewrite hcell_predecessor
  4. L251
    exact hcell_witness_right_right_witness_witness_witness_right_left
57Establish hright_atL252–255

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

  1. L252
    have hright_at : BetaAt(x3,x4,S i,x8)Definitions: BetaAt(x3,x4,S i,x8)Original native command in the exact edition
  2. L253
    rewrite hcell_predecessor
  3. L254
    rewrite hcell_predecessor
  4. L255
    exact hcell_witness_right_right_witness_witness_witness_right_right_left
58Establish hprevious_diagonal_boundL256–260

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

  1. L256
    have hprevious_diagonal_bound : Lt(i,w)Definitions: Lt(i,w)Original native command in the exact edition
  2. L257
    specialize lt_to_le (S i)
  3. L258
    specialize lt_to_le w
  4. L259
    apply lt_to_le
  5. L260
    exact hiw
59Establish hdiagonal_familyL261–263

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

  1. L261
    have hdiagonal_family : ∀ z. BetaAt(x3,x4,i,z) → z = 1Definitions: BetaAt(x3,x4,i,z)Original native command in the exact edition
  2. L262
    apply hprevious_boundary_left
  3. L263
    exact hprevious_diagonal_bound
60Establish hleft_oneL264–267

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

  1. L264
    have hleft_one : x7 = 1
  2. L265
    specialize hdiagonal_family x7
  3. L266
    apply hdiagonal_family
  4. L267
    exact hleft_at
61Establish hstrict_successorL268–270

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

  1. L268
    have hstrict_successor : Lt(i,S i)Definitions: Lt(i,S i)Original native command in the exact edition
  2. L269
    specialize le_refl (S i)
  3. L270
    exact le_refl
62Establish hright_zeroL271–280

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

  1. L271
    have hright_zero : x8 = 0
  2. L272
    specialize hprevious_boundary_right (S i)
  3. L273
    specialize hprevious_boundary_right x8
  4. L274
    apply hprevious_boundary_right
  5. L275
    exact hstrict_successor
  6. L276
    exact hiw
  7. L277
    exact hright_at
  8. L278
    trans x5
  9. L279
    exact hvalue
  10. L280
    rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
63Calculate and transport equalitiesL281–281

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

  1. L281
    simp [hleft_one, hright_zero]
64Fix variables and assumptionsL282–286

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

  1. L282
    intro j
  2. L283
    intro z
  3. L284
    intro hij
  4. L285
    intro hjw
  5. L286
    intro htarget
65Establish hsemanticL287–291

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

  1. L287
    have hsemantic : BetaAt(x,x1,j,z)Definitions: BetaAt(x,x1,j,z)Original native command in the exact edition
  2. L288
    rewrite <- hcode
  3. L289
    rewrite <- hscale
  4. L290
    rewrite <- hscale
  5. L291
    exact htarget
66Establish hcellL292–295

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. L292
    have hcell : ∃ bcf_cell_value_bptdb_step_above_cell. BetaAt(x,x1,j,bcf_cell_value_bptdb_step_above_cell) ∧ (j = 0 ∧ bcf_cell_value_bptdb_step_above_cell = 1 ∨ (∃ y. ∃ z. ∃ n. j = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptdb_step_above_cell = z + n))))Definitions: BetaAt(x,x1,j,bcf_cell_value_bptdb_step_above_cell)BetaAt(x3,x4,y,z)BetaAt(x3,x4,S y,n)Original native command in the exact edition
  2. L293
    specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right j
  3. L294
    apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  4. L295
    exact hjw
67Separate the logical casesL296–297

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

  1. L296
    cases hcell
  2. L297
    cases hcell_witness
68Establish hvalueL298–306

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

  1. L298
    have hvalue : z = x5
  2. L299
    specialize beta_at_unique x
  3. L300
    specialize beta_at_unique x1
  4. L301
    specialize beta_at_unique j
  5. L302
    specialize beta_at_unique z
  6. L303
    specialize beta_at_unique x5
  7. L304
    apply beta_at_unique
  8. L305
    exact hsemantic
  9. L306
    exact hcell_witness_left
69Separate the logical casesL307–309

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

  1. L307
    cases hcell_witness_right
  2. L308
    cases hcell_witness_right_left
  3. L309
    cases hij
70Establish hbadL310–316

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

  1. L310
    have hbad : S (S i) = 0
  2. L311
    specialize add_eq_zero_right x6
  3. L312
    specialize add_eq_zero_right (S (S i))
  4. L313
    apply add_eq_zero_right
  5. L314
    trans j
  6. L315
    exact hij_witness
  7. L316
    exact hcell_witness_right_left_left
71Separate the logical casesL317–317

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

  1. L317
    exfalso
72Use earlier factsL318–320

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

  1. L318
    specialize succ_ne_zero (S i)
  2. L319
    apply succ_ne_zero
  3. L320
    exact hbad
73Separate the logical casesL321–326

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

  1. L321
    cases hcell_witness_right_right
  2. L322
    cases hcell_witness_right_right_witness
  3. L323
    cases hcell_witness_right_right_witness_witness
  4. L324
    cases hcell_witness_right_right_witness_witness_witness
  5. L325
    cases hcell_witness_right_right_witness_witness_witness_right
  6. L326
    cases hcell_witness_right_right_witness_witness_witness_right_right
74Establish hshifted_orderL327–329

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

  1. L327
    have hshifted_order : Lt(S i,S x6)Definitions: Lt(S i,S x6)Original native command in the exact edition
  2. L328
    rewrite <- hcell_witness_right_right_witness_witness_witness_left
  3. L329
    exact hij
75Establish hprevious_left_orderL330–334

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

  1. L330
    have hprevious_left_order : Lt(i,x6)Definitions: Lt(i,x6)Original native command in the exact edition
  2. L331
    specialize le_of_succ_le_succ (S i)
  3. L332
    specialize le_of_succ_le_succ x6
  4. L333
    apply le_of_succ_le_succ
  5. L334
    exact hshifted_order
76Establish hprevious_right_orderL335–339

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

  1. L335
    have hprevious_right_order : Lt(i,S x6)Definitions: Lt(i,S x6)Original native command in the exact edition
  2. L336
    specialize lt_to_le (S i)
  3. L337
    specialize lt_to_le (S x6)
  4. L338
    apply lt_to_le
  5. L339
    exact hshifted_order
77Establish hprevious_right_boundL340–342

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

  1. L340
    have hprevious_right_bound : Lt(S x6,w)Definitions: Lt(S x6,w)Original native command in the exact edition
  2. L341
    rewrite <- hcell_witness_right_right_witness_witness_witness_left
  3. L342
    exact hjw
78Establish hprevious_left_boundL343–347

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

  1. L343
    have hprevious_left_bound : Lt(x6,w)Definitions: Lt(x6,w)Original native command in the exact edition
  2. L344
    specialize lt_to_le (S x6)
  3. L345
    specialize lt_to_le w
  4. L346
    apply lt_to_le
  5. L347
    exact hprevious_right_bound
79Establish hleft_atL348–349

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

  1. L348
    have hleft_at : BetaAt(x3,x4,x6,x7)Definitions: BetaAt(x3,x4,x6,x7)Original native command in the exact edition
  2. L349
    exact hcell_witness_right_right_witness_witness_witness_right_left
80Establish hright_atL350–351

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

  1. L350
    have hright_at : BetaAt(x3,x4,S x6,x8)Definitions: BetaAt(x3,x4,S x6,x8)Original native command in the exact edition
  2. L351
    exact hcell_witness_right_right_witness_witness_witness_right_right_left
81Establish hleft_zeroL352–358

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

  1. L352
    have hleft_zero : x7 = 0
  2. L353
    specialize hprevious_boundary_right x6
  3. L354
    specialize hprevious_boundary_right x7
  4. L355
    apply hprevious_boundary_right
  5. L356
    exact hprevious_left_order
  6. L357
    exact hprevious_left_bound
  7. L358
    exact hleft_at
82Establish hright_zeroL359–368

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

  1. L359
    have hright_zero : x8 = 0
  2. L360
    specialize hprevious_boundary_right (S x6)
  3. L361
    specialize hprevious_boundary_right x8
  4. L362
    apply hprevious_boundary_right
  5. L363
    exact hprevious_right_order
  6. L364
    exact hprevious_right_bound
  7. L365
    exact hright_at
  8. L366
    trans x5
  9. L367
    exact hvalue
  10. L368
    rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
83Calculate and transport equalitiesL369–369

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

  1. L369
    simp [hleft_zero, hright_zero]

Library-wide reading audit

Original defined command ledger · 369 lines
  1. 0001intro bb
  2. 0002intro bc
  3. 0003intro sb
  4. 0004intro sc
  5. 0005intro w
  6. 0006intro r
  7. 0007intro htable
  8. 0008intro i
  9. 0009induction i
  10. 0010intro hir
  11. 0011intro b
  12. 0012intro c
  13. 0013intro hbb
  14. 0014intro hsb
  15. 0015have hrow : ∃ bcf_row_code_bptdb_base_row. ∃ bcf_row_scale_bptdb_base_row. BetaAt(bb,bc,0,bcf_row_code_bptdb_base_row) ∧ (BetaAt(sb,sc,0,bcf_row_scale_bptdb_base_row) ∧ (0 = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))) ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(bb,bc,x,y) ∧ (BetaAt(sb,sc,x,z) ∧ (∀ n. Lt(n,w) → ∃ m. BetaAt(bcf_row_code_bptdb_base_row,bcf_row_scale_bptdb_base_row,n,m) ∧ (n = 0 ∧ m = 1 ∨ (∃ k. ∃ i. ∃ j. n = S k ∧ (BetaAt(y,z,k,i) ∧ (BetaAt(y,z,S k,j) ∧ m = i + j))))))))))
    Exact native replay linehave hrow : exists bcf_row_code_bptdb_base_row bcf_row_scale_bptdb_base_row. ((((exists bcf_height_bptdb_base_row_decoded_row_code. bcf_height_bptdb_base_row_decoded_row_code + S (bcf_row_code_bptdb_base_row) = S ((S (0)) * bc)) /\ exists bcf_quotient_bptdb_base_row_decoded_row_code. bb = bcf_quotient_bptdb_base_row_decoded_row_code * S ((S (0)) * bc) + (bcf_row_code_bptdb_base_row))) /\ ((((exists bcf_height_bptdb_base_row_decoded_row_scale. bcf_height_bptdb_base_row_decoded_row_scale + S (bcf_row_scale_bptdb_base_row) = S ((S (0)) * sc)) /\ exists bcf_quotient_bptdb_base_row_decoded_row_scale. sb = bcf_quotient_bptdb_base_row_decoded_row_scale * S ((S (0)) * sc) + (bcf_row_scale_bptdb_base_row))) /\ ((0 = 0 /\ (forall bcf_index_bptdb_base_row_zero_row. (exists bcf_lt_gap_bptdb_base_row_zero_row_bound. bcf_lt_gap_bptdb_base_row_zero_row_bound + S (bcf_index_bptdb_base_row_zero_row) = w) -> exists bcf_value_bptdb_base_row_zero_row. ((((exists bcf_height_bptdb_base_row_zero_row_entry. bcf_height_bptdb_base_row_zero_row_entry + S (bcf_value_bptdb_base_row_zero_row) = S ((S (bcf_index_bptdb_base_row_zero_row)) * bcf_row_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_zero_row_entry. bcf_row_code_bptdb_base_row = bcf_quotient_bptdb_base_row_zero_row_entry * S ((S (bcf_index_bptdb_base_row_zero_row)) * bcf_row_scale_bptdb_base_row) + (bcf_value_bptdb_base_row_zero_row))) /\ ((bcf_index_bptdb_base_row_zero_row = 0 /\ bcf_value_bptdb_base_row_zero_row = 1) \/ exists bcf_predecessor_bptdb_base_row_zero_row. bcf_index_bptdb_base_row_zero_row = S bcf_predecessor_bptdb_base_row_zero_row /\ bcf_value_bptdb_base_row_zero_row = 0)))) \/ exists bcf_predecessor_bptdb_base_row bcf_previous_code_bptdb_base_row bcf_previous_scale_bptdb_base_row. 0 = S bcf_predecessor_bptdb_base_row /\ ((((exists bcf_height_bptdb_base_row_decoded_previous_code. bcf_height_bptdb_base_row_decoded_previous_code + S (bcf_previous_code_bptdb_base_row) = S ((S (bcf_predecessor_bptdb_base_row)) * bc)) /\ exists bcf_quotient_bptdb_base_row_decoded_previous_code. bb = bcf_quotient_bptdb_base_row_decoded_previous_code * S ((S (bcf_predecessor_bptdb_base_row)) * bc) + (bcf_previous_code_bptdb_base_row))) /\ ((((exists bcf_height_bptdb_base_row_decoded_previous_scale. bcf_height_bptdb_base_row_decoded_previous_scale + S (bcf_previous_scale_bptdb_base_row) = S ((S (bcf_predecessor_bptdb_base_row)) * sc)) /\ exists bcf_quotient_bptdb_base_row_decoded_previous_scale. sb = bcf_quotient_bptdb_base_row_decoded_previous_scale * S ((S (bcf_predecessor_bptdb_base_row)) * sc) + (bcf_previous_scale_bptdb_base_row))) /\ (forall bcf_index_bptdb_base_row_row_step. (exists bcf_lt_gap_bptdb_base_row_row_step_bound. bcf_lt_gap_bptdb_base_row_row_step_bound + S (bcf_index_bptdb_base_row_row_step) = w) -> exists bcf_value_bptdb_base_row_row_step. ((((exists bcf_height_bptdb_base_row_row_step_entry. bcf_height_bptdb_base_row_row_step_entry + S (bcf_value_bptdb_base_row_row_step) = S ((S (bcf_index_bptdb_base_row_row_step)) * bcf_row_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_entry. bcf_row_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_entry * S ((S (bcf_index_bptdb_base_row_row_step)) * bcf_row_scale_bptdb_base_row) + (bcf_value_bptdb_base_row_row_step))) /\ ((bcf_index_bptdb_base_row_row_step = 0 /\ bcf_value_bptdb_base_row_row_step = 1) \/ exists bcf_predecessor_bptdb_base_row_row_step bcf_left_bptdb_base_row_row_step bcf_right_bptdb_base_row_row_step. bcf_index_bptdb_base_row_row_step = S bcf_predecessor_bptdb_base_row_row_step /\ ((((exists bcf_height_bptdb_base_row_row_step_previous_left. bcf_height_bptdb_base_row_row_step_previous_left + S (bcf_left_bptdb_base_row_row_step) = S ((S (bcf_predecessor_bptdb_base_row_row_step)) * bcf_previous_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_previous_left. bcf_previous_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_previous_left * S ((S (bcf_predecessor_bptdb_base_row_row_step)) * bcf_previous_scale_bptdb_base_row) + (bcf_left_bptdb_base_row_row_step))) /\ ((((exists bcf_height_bptdb_base_row_row_step_previous_right. bcf_height_bptdb_base_row_row_step_previous_right + S (bcf_right_bptdb_base_row_row_step) = S ((S (S (bcf_predecessor_bptdb_base_row_row_step))) * bcf_previous_scale_bptdb_base_row)) /\ exists bcf_quotient_bptdb_base_row_row_step_previous_right. bcf_previous_code_bptdb_base_row = bcf_quotient_bptdb_base_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptdb_base_row_row_step))) * bcf_previous_scale_bptdb_base_row) + (bcf_right_bptdb_base_row_row_step))) /\ bcf_value_bptdb_base_row_row_step = bcf_left_bptdb_base_row_row_step + bcf_right_bptdb_base_row_row_step))))))))))
  16. 0016specialize htable 0
  17. 0017apply htable
  18. 0018exact hir
  19. 0019cases hrow
  20. 0020cases hrow_witness
  21. 0021cases hrow_witness_witness
  22. 0022cases hrow_witness_witness_right
  23. 0023have hcode : b = x
  24. 0024specialize beta_at_unique bb
  25. 0025specialize beta_at_unique bc
  26. 0026specialize beta_at_unique 0
  27. 0027specialize beta_at_unique b
  28. 0028specialize beta_at_unique x
  29. 0029apply beta_at_unique
  30. 0030exact hbb
  31. 0031exact hrow_witness_witness_left
  32. 0032have hscale : c = x1
  33. 0033specialize beta_at_unique sb
  34. 0034specialize beta_at_unique sc
  35. 0035specialize beta_at_unique 0
  36. 0036specialize beta_at_unique c
  37. 0037specialize beta_at_unique x1
  38. 0038apply beta_at_unique
  39. 0039exact hsb
  40. 0040exact hrow_witness_witness_right_left
  41. 0041cases hrow_witness_witness_right_right
  42. 0042cases hrow_witness_witness_right_right_left
  43. 0043split
  44. 0044intro hiw
  45. 0045intro z
  46. 0046intro htarget
  47. 0047have hsemantic : BetaAt(x,x1,0,z)
    Exact native replay linehave hsemantic : ((exists bcf_height_bptdb_base_diagonal_semantic. bcf_height_bptdb_base_diagonal_semantic + S (z) = S ((S (0)) * x1)) /\ exists bcf_quotient_bptdb_base_diagonal_semantic. x = bcf_quotient_bptdb_base_diagonal_semantic * S ((S (0)) * x1) + (z))
  48. 0048rewrite <- hcode
  49. 0049rewrite <- hscale
  50. 0050rewrite <- hscale
  51. 0051exact htarget
  52. 0052have hcell : ∃ bcf_cell_value_bptdb_base_diagonal_cell. BetaAt(x,x1,0,bcf_cell_value_bptdb_base_diagonal_cell) ∧ (0 = 0 ∧ bcf_cell_value_bptdb_base_diagonal_cell = 1 ∨ (∃ y. 0 = S y ∧ bcf_cell_value_bptdb_base_diagonal_cell = 0))
    Exact native replay linehave hcell : exists bcf_cell_value_bptdb_base_diagonal_cell. ((((exists bcf_height_bptdb_base_diagonal_cell_entry. bcf_height_bptdb_base_diagonal_cell_entry + S (bcf_cell_value_bptdb_base_diagonal_cell) = S ((S (0)) * x1)) /\ exists bcf_quotient_bptdb_base_diagonal_cell_entry. x = bcf_quotient_bptdb_base_diagonal_cell_entry * S ((S (0)) * x1) + (bcf_cell_value_bptdb_base_diagonal_cell))) /\ ((0 = 0 /\ bcf_cell_value_bptdb_base_diagonal_cell = 1) \/ exists bcf_cell_predecessor_bptdb_base_diagonal_cell. 0 = S bcf_cell_predecessor_bptdb_base_diagonal_cell /\ bcf_cell_value_bptdb_base_diagonal_cell = 0))
  53. 0053specialize hrow_witness_witness_right_right_left_right 0
  54. 0054apply hrow_witness_witness_right_right_left_right
  55. 0055exact hiw
  56. 0056cases hcell
  57. 0057cases hcell_witness
  58. 0058have hvalue : z = x2
  59. 0059specialize beta_at_unique x
  60. 0060specialize beta_at_unique x1
  61. 0061specialize beta_at_unique 0
  62. 0062specialize beta_at_unique z
  63. 0063specialize beta_at_unique x2
  64. 0064apply beta_at_unique
  65. 0065exact hsemantic
  66. 0066exact hcell_witness_left
  67. 0067cases hcell_witness_right
  68. 0068cases hcell_witness_right_left
  69. 0069trans x2
  70. 0070exact hvalue
  71. 0071exact hcell_witness_right_left_right
  72. 0072cases hcell_witness_right_right
  73. 0073cases hcell_witness_right_right_witness
  74. 0074exfalso
  75. 0075have hbad : S x3 = 0
  76. 0076symm
  77. 0077exact hcell_witness_right_right_witness_left
  78. 0078specialize succ_ne_zero x3
  79. 0079apply succ_ne_zero
  80. 0080exact hbad
  81. 0081intro j
  82. 0082intro z
  83. 0083intro hij
  84. 0084intro hjw
  85. 0085intro htarget
  86. 0086have hsemantic : BetaAt(x,x1,j,z)
    Exact native replay linehave hsemantic : ((exists bcf_height_bptdb_base_above_semantic. bcf_height_bptdb_base_above_semantic + S (z) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_base_above_semantic. x = bcf_quotient_bptdb_base_above_semantic * S ((S (j)) * x1) + (z))
  87. 0087rewrite <- hcode
  88. 0088rewrite <- hscale
  89. 0089rewrite <- hscale
  90. 0090exact htarget
  91. 0091have hcell : ∃ bcf_cell_value_bptdb_base_above_cell. BetaAt(x,x1,j,bcf_cell_value_bptdb_base_above_cell) ∧ (j = 0 ∧ bcf_cell_value_bptdb_base_above_cell = 1 ∨ (∃ y. j = S y ∧ bcf_cell_value_bptdb_base_above_cell = 0))
    Exact native replay linehave hcell : exists bcf_cell_value_bptdb_base_above_cell. ((((exists bcf_height_bptdb_base_above_cell_entry. bcf_height_bptdb_base_above_cell_entry + S (bcf_cell_value_bptdb_base_above_cell) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_base_above_cell_entry. x = bcf_quotient_bptdb_base_above_cell_entry * S ((S (j)) * x1) + (bcf_cell_value_bptdb_base_above_cell))) /\ ((j = 0 /\ bcf_cell_value_bptdb_base_above_cell = 1) \/ exists bcf_cell_predecessor_bptdb_base_above_cell. j = S bcf_cell_predecessor_bptdb_base_above_cell /\ bcf_cell_value_bptdb_base_above_cell = 0))
  92. 0092specialize hrow_witness_witness_right_right_left_right j
  93. 0093apply hrow_witness_witness_right_right_left_right
  94. 0094exact hjw
  95. 0095cases hcell
  96. 0096cases hcell_witness
  97. 0097have hvalue : z = x2
  98. 0098specialize beta_at_unique x
  99. 0099specialize beta_at_unique x1
  100. 0100specialize beta_at_unique j
  101. 0101specialize beta_at_unique z
  102. 0102specialize beta_at_unique x2
  103. 0103apply beta_at_unique
  104. 0104exact hsemantic
  105. 0105exact hcell_witness_left
  106. 0106cases hcell_witness_right
  107. 0107cases hcell_witness_right_left
  108. 0108cases hij
  109. 0109have hbad : S 0 = 0
  110. 0110specialize add_eq_zero_right x3
  111. 0111specialize add_eq_zero_right (S 0)
  112. 0112apply add_eq_zero_right
  113. 0113trans j
  114. 0114exact hij_witness
  115. 0115exact hcell_witness_right_left_left
  116. 0116exfalso
  117. 0117specialize succ_ne_zero 0
  118. 0118apply succ_ne_zero
  119. 0119exact hbad
  120. 0120cases hcell_witness_right_right
  121. 0121cases hcell_witness_right_right_witness
  122. 0122trans x2
  123. 0123exact hvalue
  124. 0124exact hcell_witness_right_right_witness_right
  125. 0125cases hrow_witness_witness_right_right_right
  126. 0126cases hrow_witness_witness_right_right_right_witness
  127. 0127cases hrow_witness_witness_right_right_right_witness_witness
  128. 0128cases hrow_witness_witness_right_right_right_witness_witness_witness
  129. 0129exfalso
  130. 0130have hbad : S x2 = 0
  131. 0131symm
  132. 0132exact hrow_witness_witness_right_right_right_witness_witness_witness_left
  133. 0133specialize succ_ne_zero x2
  134. 0134apply succ_ne_zero
  135. 0135exact hbad
  136. 0136intro hir
  137. 0137intro b
  138. 0138intro c
  139. 0139intro hbb
  140. 0140intro hsb
  141. 0141have hrow : ∃ bcf_row_code_bptdb_step_row. ∃ bcf_row_scale_bptdb_step_row. BetaAt(bb,bc,S i,bcf_row_code_bptdb_step_row) ∧ (BetaAt(sb,sc,S i,bcf_row_scale_bptdb_step_row) ∧ (S i = 0 ∧ (∀ x. Lt(x,w) → ∃ y. BetaAt(bcf_row_code_bptdb_step_row,bcf_row_scale_bptdb_step_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_bptdb_step_row,bcf_row_scale_bptdb_step_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_bptdb_step_row bcf_row_scale_bptdb_step_row. ((((exists bcf_height_bptdb_step_row_decoded_row_code. bcf_height_bptdb_step_row_decoded_row_code + S (bcf_row_code_bptdb_step_row) = S ((S (S i)) * bc)) /\ exists bcf_quotient_bptdb_step_row_decoded_row_code. bb = bcf_quotient_bptdb_step_row_decoded_row_code * S ((S (S i)) * bc) + (bcf_row_code_bptdb_step_row))) /\ ((((exists bcf_height_bptdb_step_row_decoded_row_scale. bcf_height_bptdb_step_row_decoded_row_scale + S (bcf_row_scale_bptdb_step_row) = S ((S (S i)) * sc)) /\ exists bcf_quotient_bptdb_step_row_decoded_row_scale. sb = bcf_quotient_bptdb_step_row_decoded_row_scale * S ((S (S i)) * sc) + (bcf_row_scale_bptdb_step_row))) /\ ((S i = 0 /\ (forall bcf_index_bptdb_step_row_zero_row. (exists bcf_lt_gap_bptdb_step_row_zero_row_bound. bcf_lt_gap_bptdb_step_row_zero_row_bound + S (bcf_index_bptdb_step_row_zero_row) = w) -> exists bcf_value_bptdb_step_row_zero_row. ((((exists bcf_height_bptdb_step_row_zero_row_entry. bcf_height_bptdb_step_row_zero_row_entry + S (bcf_value_bptdb_step_row_zero_row) = S ((S (bcf_index_bptdb_step_row_zero_row)) * bcf_row_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_zero_row_entry. bcf_row_code_bptdb_step_row = bcf_quotient_bptdb_step_row_zero_row_entry * S ((S (bcf_index_bptdb_step_row_zero_row)) * bcf_row_scale_bptdb_step_row) + (bcf_value_bptdb_step_row_zero_row))) /\ ((bcf_index_bptdb_step_row_zero_row = 0 /\ bcf_value_bptdb_step_row_zero_row = 1) \/ exists bcf_predecessor_bptdb_step_row_zero_row. bcf_index_bptdb_step_row_zero_row = S bcf_predecessor_bptdb_step_row_zero_row /\ bcf_value_bptdb_step_row_zero_row = 0)))) \/ exists bcf_predecessor_bptdb_step_row bcf_previous_code_bptdb_step_row bcf_previous_scale_bptdb_step_row. S i = S bcf_predecessor_bptdb_step_row /\ ((((exists bcf_height_bptdb_step_row_decoded_previous_code. bcf_height_bptdb_step_row_decoded_previous_code + S (bcf_previous_code_bptdb_step_row) = S ((S (bcf_predecessor_bptdb_step_row)) * bc)) /\ exists bcf_quotient_bptdb_step_row_decoded_previous_code. bb = bcf_quotient_bptdb_step_row_decoded_previous_code * S ((S (bcf_predecessor_bptdb_step_row)) * bc) + (bcf_previous_code_bptdb_step_row))) /\ ((((exists bcf_height_bptdb_step_row_decoded_previous_scale. bcf_height_bptdb_step_row_decoded_previous_scale + S (bcf_previous_scale_bptdb_step_row) = S ((S (bcf_predecessor_bptdb_step_row)) * sc)) /\ exists bcf_quotient_bptdb_step_row_decoded_previous_scale. sb = bcf_quotient_bptdb_step_row_decoded_previous_scale * S ((S (bcf_predecessor_bptdb_step_row)) * sc) + (bcf_previous_scale_bptdb_step_row))) /\ (forall bcf_index_bptdb_step_row_row_step. (exists bcf_lt_gap_bptdb_step_row_row_step_bound. bcf_lt_gap_bptdb_step_row_row_step_bound + S (bcf_index_bptdb_step_row_row_step) = w) -> exists bcf_value_bptdb_step_row_row_step. ((((exists bcf_height_bptdb_step_row_row_step_entry. bcf_height_bptdb_step_row_row_step_entry + S (bcf_value_bptdb_step_row_row_step) = S ((S (bcf_index_bptdb_step_row_row_step)) * bcf_row_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_entry. bcf_row_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_entry * S ((S (bcf_index_bptdb_step_row_row_step)) * bcf_row_scale_bptdb_step_row) + (bcf_value_bptdb_step_row_row_step))) /\ ((bcf_index_bptdb_step_row_row_step = 0 /\ bcf_value_bptdb_step_row_row_step = 1) \/ exists bcf_predecessor_bptdb_step_row_row_step bcf_left_bptdb_step_row_row_step bcf_right_bptdb_step_row_row_step. bcf_index_bptdb_step_row_row_step = S bcf_predecessor_bptdb_step_row_row_step /\ ((((exists bcf_height_bptdb_step_row_row_step_previous_left. bcf_height_bptdb_step_row_row_step_previous_left + S (bcf_left_bptdb_step_row_row_step) = S ((S (bcf_predecessor_bptdb_step_row_row_step)) * bcf_previous_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_previous_left. bcf_previous_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_previous_left * S ((S (bcf_predecessor_bptdb_step_row_row_step)) * bcf_previous_scale_bptdb_step_row) + (bcf_left_bptdb_step_row_row_step))) /\ ((((exists bcf_height_bptdb_step_row_row_step_previous_right. bcf_height_bptdb_step_row_row_step_previous_right + S (bcf_right_bptdb_step_row_row_step) = S ((S (S (bcf_predecessor_bptdb_step_row_row_step))) * bcf_previous_scale_bptdb_step_row)) /\ exists bcf_quotient_bptdb_step_row_row_step_previous_right. bcf_previous_code_bptdb_step_row = bcf_quotient_bptdb_step_row_row_step_previous_right * S ((S (S (bcf_predecessor_bptdb_step_row_row_step))) * bcf_previous_scale_bptdb_step_row) + (bcf_right_bptdb_step_row_row_step))) /\ bcf_value_bptdb_step_row_row_step = bcf_left_bptdb_step_row_row_step + bcf_right_bptdb_step_row_row_step))))))))))
  142. 0142specialize htable (S i)
  143. 0143apply htable
  144. 0144exact hir
  145. 0145cases hrow
  146. 0146cases hrow_witness
  147. 0147cases hrow_witness_witness
  148. 0148cases hrow_witness_witness_right
  149. 0149have hcode : b = x
  150. 0150specialize beta_at_unique bb
  151. 0151specialize beta_at_unique bc
  152. 0152specialize beta_at_unique (S i)
  153. 0153specialize beta_at_unique b
  154. 0154specialize beta_at_unique x
  155. 0155apply beta_at_unique
  156. 0156exact hbb
  157. 0157exact hrow_witness_witness_left
  158. 0158have hscale : c = x1
  159. 0159specialize beta_at_unique sb
  160. 0160specialize beta_at_unique sc
  161. 0161specialize beta_at_unique (S i)
  162. 0162specialize beta_at_unique c
  163. 0163specialize beta_at_unique x1
  164. 0164apply beta_at_unique
  165. 0165exact hsb
  166. 0166exact hrow_witness_witness_right_left
  167. 0167cases hrow_witness_witness_right_right
  168. 0168cases hrow_witness_witness_right_right_left
  169. 0169exfalso
  170. 0170specialize succ_ne_zero i
  171. 0171apply succ_ne_zero
  172. 0172exact hrow_witness_witness_right_right_left_left
  173. 0173cases hrow_witness_witness_right_right_right
  174. 0174cases hrow_witness_witness_right_right_right_witness
  175. 0175cases hrow_witness_witness_right_right_right_witness_witness
  176. 0176cases hrow_witness_witness_right_right_right_witness_witness_witness
  177. 0177cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  178. 0178cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
  179. 0179have hpredecessor : i = x2
  180. 0180specialize succ_injective i
  181. 0181specialize succ_injective x2
  182. 0182apply succ_injective
  183. 0183exact hrow_witness_witness_right_right_right_witness_witness_witness_left
  184. 0184have hprevious_row_bound : Lt(i,r)
    Exact native replay linehave hprevious_row_bound : exists bcf_lt_gap_bptdb_previous_row_bound. bcf_lt_gap_bptdb_previous_row_bound + S (i) = r
  185. 0185specialize lt_to_le (S i)
  186. 0186specialize lt_to_le r
  187. 0187apply lt_to_le
  188. 0188exact hir
  189. 0189have hprevious_code : BetaAt(bb,bc,i,x3)
    Exact native replay linehave hprevious_code : ((exists bcf_height_bptdb_previous_code_at. bcf_height_bptdb_previous_code_at + S (x3) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptdb_previous_code_at. bb = bcf_quotient_bptdb_previous_code_at * S ((S (i)) * bc) + (x3))
  190. 0190rewrite hpredecessor
  191. 0191rewrite hpredecessor
  192. 0192exact hrow_witness_witness_right_right_right_witness_witness_witness_right_left
  193. 0193have hprevious_scale : BetaAt(sb,sc,i,x4)
    Exact native replay linehave hprevious_scale : ((exists bcf_height_bptdb_previous_scale_at. bcf_height_bptdb_previous_scale_at + S (x4) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptdb_previous_scale_at. sb = bcf_quotient_bptdb_previous_scale_at * S ((S (i)) * sc) + (x4))
  194. 0194rewrite hpredecessor
  195. 0195rewrite hpredecessor
  196. 0196exact hrow_witness_witness_right_right_right_witness_witness_witness_right_right_left
  197. 0197have hprevious_family : ∀ bcf_row_code_bptdb_previous_family. ∀ bcf_row_scale_bptdb_previous_family. BetaAt(bb,bc,i,bcf_row_code_bptdb_previous_family) → BetaAt(sb,sc,i,bcf_row_scale_bptdb_previous_family) → (Lt(i,w) → ∀ x. BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,i,x) → x = 1) ∧ (∀ x. ∀ y. Lt(i,x) → Lt(x,w) → BetaAt(bcf_row_code_bptdb_previous_family,bcf_row_scale_bptdb_previous_family,x,y) → y = 0)
    Exact native replay linehave hprevious_family : forall bcf_row_code_bptdb_previous_family bcf_row_scale_bptdb_previous_family. (((exists bcf_height_bptdb_previous_family_code_at. bcf_height_bptdb_previous_family_code_at + S (bcf_row_code_bptdb_previous_family) = S ((S (i)) * bc)) /\ exists bcf_quotient_bptdb_previous_family_code_at. bb = bcf_quotient_bptdb_previous_family_code_at * S ((S (i)) * bc) + (bcf_row_code_bptdb_previous_family))) -> (((exists bcf_height_bptdb_previous_family_scale_at. bcf_height_bptdb_previous_family_scale_at + S (bcf_row_scale_bptdb_previous_family) = S ((S (i)) * sc)) /\ exists bcf_quotient_bptdb_previous_family_scale_at. sb = bcf_quotient_bptdb_previous_family_scale_at * S ((S (i)) * sc) + (bcf_row_scale_bptdb_previous_family))) -> ((((exists bcf_lt_gap_bptdb_previous_family_boundary_diagonal_bound. bcf_lt_gap_bptdb_previous_family_boundary_diagonal_bound + S (i) = w) -> forall bcf_diagonal_value_bptdb_previous_family_boundary. (((exists bcf_height_bptdb_previous_family_boundary_diagonal_at. bcf_height_bptdb_previous_family_boundary_diagonal_at + S (bcf_diagonal_value_bptdb_previous_family_boundary) = S ((S (i)) * bcf_row_scale_bptdb_previous_family)) /\ exists bcf_quotient_bptdb_previous_family_boundary_diagonal_at. bcf_row_code_bptdb_previous_family = bcf_quotient_bptdb_previous_family_boundary_diagonal_at * S ((S (i)) * bcf_row_scale_bptdb_previous_family) + (bcf_diagonal_value_bptdb_previous_family_boundary))) -> bcf_diagonal_value_bptdb_previous_family_boundary = 1) /\ forall bcf_above_index_bptdb_previous_family_boundary bcf_above_value_bptdb_previous_family_boundary. (exists bcf_lt_gap_bptdb_previous_family_boundary_above_order. bcf_lt_gap_bptdb_previous_family_boundary_above_order + S (i) = bcf_above_index_bptdb_previous_family_boundary) -> (exists bcf_lt_gap_bptdb_previous_family_boundary_above_bound. bcf_lt_gap_bptdb_previous_family_boundary_above_bound + S (bcf_above_index_bptdb_previous_family_boundary) = w) -> (((exists bcf_height_bptdb_previous_family_boundary_above_at. bcf_height_bptdb_previous_family_boundary_above_at + S (bcf_above_value_bptdb_previous_family_boundary) = S ((S (bcf_above_index_bptdb_previous_family_boundary)) * bcf_row_scale_bptdb_previous_family)) /\ exists bcf_quotient_bptdb_previous_family_boundary_above_at. bcf_row_code_bptdb_previous_family = bcf_quotient_bptdb_previous_family_boundary_above_at * S ((S (bcf_above_index_bptdb_previous_family_boundary)) * bcf_row_scale_bptdb_previous_family) + (bcf_above_value_bptdb_previous_family_boundary))) -> bcf_above_value_bptdb_previous_family_boundary = 0))
  198. 0198apply IH
  199. 0199exact hprevious_row_bound
  200. 0200have hprevious_boundary : (Lt(i,w) → ∀ x. BetaAt(x3,x4,i,x) → x = 1) ∧ (∀ x. ∀ y. Lt(i,x) → Lt(x,w) → BetaAt(x3,x4,x,y) → y = 0)
    Exact native replay linehave hprevious_boundary : (((exists bcf_lt_gap_bptdb_previous_boundary_diagonal_bound. bcf_lt_gap_bptdb_previous_boundary_diagonal_bound + S (i) = w) -> forall bcf_diagonal_value_bptdb_previous_boundary. (((exists bcf_height_bptdb_previous_boundary_diagonal_at. bcf_height_bptdb_previous_boundary_diagonal_at + S (bcf_diagonal_value_bptdb_previous_boundary) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_previous_boundary_diagonal_at. x3 = bcf_quotient_bptdb_previous_boundary_diagonal_at * S ((S (i)) * x4) + (bcf_diagonal_value_bptdb_previous_boundary))) -> bcf_diagonal_value_bptdb_previous_boundary = 1) /\ forall bcf_above_index_bptdb_previous_boundary bcf_above_value_bptdb_previous_boundary. (exists bcf_lt_gap_bptdb_previous_boundary_above_order. bcf_lt_gap_bptdb_previous_boundary_above_order + S (i) = bcf_above_index_bptdb_previous_boundary) -> (exists bcf_lt_gap_bptdb_previous_boundary_above_bound. bcf_lt_gap_bptdb_previous_boundary_above_bound + S (bcf_above_index_bptdb_previous_boundary) = w) -> (((exists bcf_height_bptdb_previous_boundary_above_at. bcf_height_bptdb_previous_boundary_above_at + S (bcf_above_value_bptdb_previous_boundary) = S ((S (bcf_above_index_bptdb_previous_boundary)) * x4)) /\ exists bcf_quotient_bptdb_previous_boundary_above_at. x3 = bcf_quotient_bptdb_previous_boundary_above_at * S ((S (bcf_above_index_bptdb_previous_boundary)) * x4) + (bcf_above_value_bptdb_previous_boundary))) -> bcf_above_value_bptdb_previous_boundary = 0)
  201. 0201specialize hprevious_family x3
  202. 0202specialize hprevious_family x4
  203. 0203apply hprevious_family
  204. 0204exact hprevious_code
  205. 0205exact hprevious_scale
  206. 0206cases hprevious_boundary
  207. 0207split
  208. 0208intro hiw
  209. 0209intro z
  210. 0210intro htarget
  211. 0211have hsemantic : BetaAt(x,x1,S i,z)
    Exact native replay linehave hsemantic : ((exists bcf_height_bptdb_step_diagonal_semantic. bcf_height_bptdb_step_diagonal_semantic + S (z) = S ((S (S i)) * x1)) /\ exists bcf_quotient_bptdb_step_diagonal_semantic. x = bcf_quotient_bptdb_step_diagonal_semantic * S ((S (S i)) * x1) + (z))
  212. 0212rewrite <- hcode
  213. 0213rewrite <- hscale
  214. 0214rewrite <- hscale
  215. 0215exact htarget
  216. 0216have hcell : ∃ bcf_cell_value_bptdb_step_diagonal_cell. BetaAt(x,x1,S i,bcf_cell_value_bptdb_step_diagonal_cell) ∧ (S i = 0 ∧ bcf_cell_value_bptdb_step_diagonal_cell = 1 ∨ (∃ y. ∃ z. ∃ n. S i = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptdb_step_diagonal_cell = z + n))))
    Exact native replay linehave hcell : exists bcf_cell_value_bptdb_step_diagonal_cell. ((((exists bcf_height_bptdb_step_diagonal_cell_entry. bcf_height_bptdb_step_diagonal_cell_entry + S (bcf_cell_value_bptdb_step_diagonal_cell) = S ((S (S i)) * x1)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_entry. x = bcf_quotient_bptdb_step_diagonal_cell_entry * S ((S (S i)) * x1) + (bcf_cell_value_bptdb_step_diagonal_cell))) /\ ((S i = 0 /\ bcf_cell_value_bptdb_step_diagonal_cell = 1) \/ exists bcf_cell_predecessor_bptdb_step_diagonal_cell bcf_cell_left_bptdb_step_diagonal_cell bcf_cell_right_bptdb_step_diagonal_cell. S i = S bcf_cell_predecessor_bptdb_step_diagonal_cell /\ ((((exists bcf_height_bptdb_step_diagonal_cell_previous_left. bcf_height_bptdb_step_diagonal_cell_previous_left + S (bcf_cell_left_bptdb_step_diagonal_cell) = S ((S (bcf_cell_predecessor_bptdb_step_diagonal_cell)) * x4)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_previous_left. x3 = bcf_quotient_bptdb_step_diagonal_cell_previous_left * S ((S (bcf_cell_predecessor_bptdb_step_diagonal_cell)) * x4) + (bcf_cell_left_bptdb_step_diagonal_cell))) /\ ((((exists bcf_height_bptdb_step_diagonal_cell_previous_right. bcf_height_bptdb_step_diagonal_cell_previous_right + S (bcf_cell_right_bptdb_step_diagonal_cell) = S ((S (S (bcf_cell_predecessor_bptdb_step_diagonal_cell))) * x4)) /\ exists bcf_quotient_bptdb_step_diagonal_cell_previous_right. x3 = bcf_quotient_bptdb_step_diagonal_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptdb_step_diagonal_cell))) * x4) + (bcf_cell_right_bptdb_step_diagonal_cell))) /\ bcf_cell_value_bptdb_step_diagonal_cell = bcf_cell_left_bptdb_step_diagonal_cell + bcf_cell_right_bptdb_step_diagonal_cell))))
  217. 0217specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right (S i)
  218. 0218apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  219. 0219exact hiw
  220. 0220cases hcell
  221. 0221cases hcell_witness
  222. 0222have hvalue : z = x5
  223. 0223specialize beta_at_unique x
  224. 0224specialize beta_at_unique x1
  225. 0225specialize beta_at_unique (S i)
  226. 0226specialize beta_at_unique z
  227. 0227specialize beta_at_unique x5
  228. 0228apply beta_at_unique
  229. 0229exact hsemantic
  230. 0230exact hcell_witness_left
  231. 0231cases hcell_witness_right
  232. 0232cases hcell_witness_right_left
  233. 0233exfalso
  234. 0234specialize succ_ne_zero i
  235. 0235apply succ_ne_zero
  236. 0236exact hcell_witness_right_left_left
  237. 0237cases hcell_witness_right_right
  238. 0238cases hcell_witness_right_right_witness
  239. 0239cases hcell_witness_right_right_witness_witness
  240. 0240cases hcell_witness_right_right_witness_witness_witness
  241. 0241cases hcell_witness_right_right_witness_witness_witness_right
  242. 0242cases hcell_witness_right_right_witness_witness_witness_right_right
  243. 0243have hcell_predecessor : i = x6
  244. 0244specialize succ_injective i
  245. 0245specialize succ_injective x6
  246. 0246apply succ_injective
  247. 0247exact hcell_witness_right_right_witness_witness_witness_left
  248. 0248have hleft_at : BetaAt(x3,x4,i,x7)
    Exact native replay linehave hleft_at : ((exists bcf_height_bptdb_step_previous_left. bcf_height_bptdb_step_previous_left + S (x7) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_step_previous_left. x3 = bcf_quotient_bptdb_step_previous_left * S ((S (i)) * x4) + (x7))
  249. 0249rewrite hcell_predecessor
  250. 0250rewrite hcell_predecessor
  251. 0251exact hcell_witness_right_right_witness_witness_witness_right_left
  252. 0252have hright_at : BetaAt(x3,x4,S i,x8)
    Exact native replay linehave hright_at : ((exists bcf_height_bptdb_step_previous_right. bcf_height_bptdb_step_previous_right + S (x8) = S ((S (S i)) * x4)) /\ exists bcf_quotient_bptdb_step_previous_right. x3 = bcf_quotient_bptdb_step_previous_right * S ((S (S i)) * x4) + (x8))
  253. 0253rewrite hcell_predecessor
  254. 0254rewrite hcell_predecessor
  255. 0255exact hcell_witness_right_right_witness_witness_witness_right_right_left
  256. 0256have hprevious_diagonal_bound : Lt(i,w)
    Exact native replay linehave hprevious_diagonal_bound : exists bcf_lt_gap_bptdb_previous_diagonal_bound. bcf_lt_gap_bptdb_previous_diagonal_bound + S (i) = w
  257. 0257specialize lt_to_le (S i)
  258. 0258specialize lt_to_le w
  259. 0259apply lt_to_le
  260. 0260exact hiw
  261. 0261have hdiagonal_family : ∀ z. BetaAt(x3,x4,i,z) → z = 1
    Exact native replay linehave hdiagonal_family : forall z. (((exists bcf_height_bptdb_previous_diagonal_family. bcf_height_bptdb_previous_diagonal_family + S (z) = S ((S (i)) * x4)) /\ exists bcf_quotient_bptdb_previous_diagonal_family. x3 = bcf_quotient_bptdb_previous_diagonal_family * S ((S (i)) * x4) + (z))) -> z = 1
  262. 0262apply hprevious_boundary_left
  263. 0263exact hprevious_diagonal_bound
  264. 0264have hleft_one : x7 = 1
  265. 0265specialize hdiagonal_family x7
  266. 0266apply hdiagonal_family
  267. 0267exact hleft_at
  268. 0268have hstrict_successor : Lt(i,S i)
    Exact native replay linehave hstrict_successor : exists bcf_lt_gap_bptdb_strict_successor. bcf_lt_gap_bptdb_strict_successor + S (i) = S i
  269. 0269specialize le_refl (S i)
  270. 0270exact le_refl
  271. 0271have hright_zero : x8 = 0
  272. 0272specialize hprevious_boundary_right (S i)
  273. 0273specialize hprevious_boundary_right x8
  274. 0274apply hprevious_boundary_right
  275. 0275exact hstrict_successor
  276. 0276exact hiw
  277. 0277exact hright_at
  278. 0278trans x5
  279. 0279exact hvalue
  280. 0280rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
  281. 0281simp [hleft_one, hright_zero]
  282. 0282intro j
  283. 0283intro z
  284. 0284intro hij
  285. 0285intro hjw
  286. 0286intro htarget
  287. 0287have hsemantic : BetaAt(x,x1,j,z)
    Exact native replay linehave hsemantic : ((exists bcf_height_bptdb_step_above_semantic. bcf_height_bptdb_step_above_semantic + S (z) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_step_above_semantic. x = bcf_quotient_bptdb_step_above_semantic * S ((S (j)) * x1) + (z))
  288. 0288rewrite <- hcode
  289. 0289rewrite <- hscale
  290. 0290rewrite <- hscale
  291. 0291exact htarget
  292. 0292have hcell : ∃ bcf_cell_value_bptdb_step_above_cell. BetaAt(x,x1,j,bcf_cell_value_bptdb_step_above_cell) ∧ (j = 0 ∧ bcf_cell_value_bptdb_step_above_cell = 1 ∨ (∃ y. ∃ z. ∃ n. j = S y ∧ (BetaAt(x3,x4,y,z) ∧ (BetaAt(x3,x4,S y,n) ∧ bcf_cell_value_bptdb_step_above_cell = z + n))))
    Exact native replay linehave hcell : exists bcf_cell_value_bptdb_step_above_cell. ((((exists bcf_height_bptdb_step_above_cell_entry. bcf_height_bptdb_step_above_cell_entry + S (bcf_cell_value_bptdb_step_above_cell) = S ((S (j)) * x1)) /\ exists bcf_quotient_bptdb_step_above_cell_entry. x = bcf_quotient_bptdb_step_above_cell_entry * S ((S (j)) * x1) + (bcf_cell_value_bptdb_step_above_cell))) /\ ((j = 0 /\ bcf_cell_value_bptdb_step_above_cell = 1) \/ exists bcf_cell_predecessor_bptdb_step_above_cell bcf_cell_left_bptdb_step_above_cell bcf_cell_right_bptdb_step_above_cell. j = S bcf_cell_predecessor_bptdb_step_above_cell /\ ((((exists bcf_height_bptdb_step_above_cell_previous_left. bcf_height_bptdb_step_above_cell_previous_left + S (bcf_cell_left_bptdb_step_above_cell) = S ((S (bcf_cell_predecessor_bptdb_step_above_cell)) * x4)) /\ exists bcf_quotient_bptdb_step_above_cell_previous_left. x3 = bcf_quotient_bptdb_step_above_cell_previous_left * S ((S (bcf_cell_predecessor_bptdb_step_above_cell)) * x4) + (bcf_cell_left_bptdb_step_above_cell))) /\ ((((exists bcf_height_bptdb_step_above_cell_previous_right. bcf_height_bptdb_step_above_cell_previous_right + S (bcf_cell_right_bptdb_step_above_cell) = S ((S (S (bcf_cell_predecessor_bptdb_step_above_cell))) * x4)) /\ exists bcf_quotient_bptdb_step_above_cell_previous_right. x3 = bcf_quotient_bptdb_step_above_cell_previous_right * S ((S (S (bcf_cell_predecessor_bptdb_step_above_cell))) * x4) + (bcf_cell_right_bptdb_step_above_cell))) /\ bcf_cell_value_bptdb_step_above_cell = bcf_cell_left_bptdb_step_above_cell + bcf_cell_right_bptdb_step_above_cell))))
  293. 0293specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right j
  294. 0294apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  295. 0295exact hjw
  296. 0296cases hcell
  297. 0297cases hcell_witness
  298. 0298have hvalue : z = x5
  299. 0299specialize beta_at_unique x
  300. 0300specialize beta_at_unique x1
  301. 0301specialize beta_at_unique j
  302. 0302specialize beta_at_unique z
  303. 0303specialize beta_at_unique x5
  304. 0304apply beta_at_unique
  305. 0305exact hsemantic
  306. 0306exact hcell_witness_left
  307. 0307cases hcell_witness_right
  308. 0308cases hcell_witness_right_left
  309. 0309cases hij
  310. 0310have hbad : S (S i) = 0
  311. 0311specialize add_eq_zero_right x6
  312. 0312specialize add_eq_zero_right (S (S i))
  313. 0313apply add_eq_zero_right
  314. 0314trans j
  315. 0315exact hij_witness
  316. 0316exact hcell_witness_right_left_left
  317. 0317exfalso
  318. 0318specialize succ_ne_zero (S i)
  319. 0319apply succ_ne_zero
  320. 0320exact hbad
  321. 0321cases hcell_witness_right_right
  322. 0322cases hcell_witness_right_right_witness
  323. 0323cases hcell_witness_right_right_witness_witness
  324. 0324cases hcell_witness_right_right_witness_witness_witness
  325. 0325cases hcell_witness_right_right_witness_witness_witness_right
  326. 0326cases hcell_witness_right_right_witness_witness_witness_right_right
  327. 0327have hshifted_order : Lt(S i,S x6)
    Exact native replay linehave hshifted_order : exists bcf_lt_gap_bptdb_shifted_above_order. bcf_lt_gap_bptdb_shifted_above_order + S (S i) = S x6
  328. 0328rewrite <- hcell_witness_right_right_witness_witness_witness_left
  329. 0329exact hij
  330. 0330have hprevious_left_order : Lt(i,x6)
    Exact native replay linehave hprevious_left_order : exists bcf_lt_gap_bptdb_previous_left_order. bcf_lt_gap_bptdb_previous_left_order + S (i) = x6
  331. 0331specialize le_of_succ_le_succ (S i)
  332. 0332specialize le_of_succ_le_succ x6
  333. 0333apply le_of_succ_le_succ
  334. 0334exact hshifted_order
  335. 0335have hprevious_right_order : Lt(i,S x6)
    Exact native replay linehave hprevious_right_order : exists bcf_lt_gap_bptdb_previous_right_order. bcf_lt_gap_bptdb_previous_right_order + S (i) = S x6
  336. 0336specialize lt_to_le (S i)
  337. 0337specialize lt_to_le (S x6)
  338. 0338apply lt_to_le
  339. 0339exact hshifted_order
  340. 0340have hprevious_right_bound : Lt(S x6,w)
    Exact native replay linehave hprevious_right_bound : exists bcf_lt_gap_bptdb_previous_right_bound. bcf_lt_gap_bptdb_previous_right_bound + S (S x6) = w
  341. 0341rewrite <- hcell_witness_right_right_witness_witness_witness_left
  342. 0342exact hjw
  343. 0343have hprevious_left_bound : Lt(x6,w)
    Exact native replay linehave hprevious_left_bound : exists bcf_lt_gap_bptdb_previous_left_bound. bcf_lt_gap_bptdb_previous_left_bound + S (x6) = w
  344. 0344specialize lt_to_le (S x6)
  345. 0345specialize lt_to_le w
  346. 0346apply lt_to_le
  347. 0347exact hprevious_right_bound
  348. 0348have hleft_at : BetaAt(x3,x4,x6,x7)
    Exact native replay linehave hleft_at : ((exists bcf_height_bptdb_above_previous_left. bcf_height_bptdb_above_previous_left + S (x7) = S ((S (x6)) * x4)) /\ exists bcf_quotient_bptdb_above_previous_left. x3 = bcf_quotient_bptdb_above_previous_left * S ((S (x6)) * x4) + (x7))
  349. 0349exact hcell_witness_right_right_witness_witness_witness_right_left
  350. 0350have hright_at : BetaAt(x3,x4,S x6,x8)
    Exact native replay linehave hright_at : ((exists bcf_height_bptdb_above_previous_right. bcf_height_bptdb_above_previous_right + S (x8) = S ((S (S x6)) * x4)) /\ exists bcf_quotient_bptdb_above_previous_right. x3 = bcf_quotient_bptdb_above_previous_right * S ((S (S x6)) * x4) + (x8))
  351. 0351exact hcell_witness_right_right_witness_witness_witness_right_right_left
  352. 0352have hleft_zero : x7 = 0
  353. 0353specialize hprevious_boundary_right x6
  354. 0354specialize hprevious_boundary_right x7
  355. 0355apply hprevious_boundary_right
  356. 0356exact hprevious_left_order
  357. 0357exact hprevious_left_bound
  358. 0358exact hleft_at
  359. 0359have hright_zero : x8 = 0
  360. 0360specialize hprevious_boundary_right (S x6)
  361. 0361specialize hprevious_boundary_right x8
  362. 0362apply hprevious_boundary_right
  363. 0363exact hprevious_right_order
  364. 0364exact hprevious_right_bound
  365. 0365exact hright_at
  366. 0366trans x5
  367. 0367exact hvalue
  368. 0368rewrite hcell_witness_right_right_witness_witness_witness_right_right_right
  369. 0369simp [hleft_zero, hright_zero]