BT00TE · Bertrand theorem

choose_zero

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

The zeroth entry of every Pascal row is one.

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

∀ n. ∀ z. Choose(n,0,z) → z = 1

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

PD0041 Choose

1 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

17 occurrences

Exact expanded native-PA statement
forall n z. (((exists bcf_lt_gap_bclz_choose_out_of_range. bcf_lt_gap_bclz_choose_out_of_range + S (n) = 0) /\ z = 0) \/ ((exists bcf_le_gap_bclz_choose_in_range. bcf_le_gap_bclz_choose_in_range + (0) = n) /\ (exists bcf_row_code_code_bclz_choose bcf_row_code_scale_bclz_choose bcf_row_scale_code_bclz_choose bcf_row_scale_scale_bclz_choose bcf_row_code_bclz_choose bcf_row_scale_bclz_choose. ((forall bcf_row_index_bclz_choose_table. (exists bcf_lt_gap_bclz_choose_table_row_bound. bcf_lt_gap_bclz_choose_table_row_bound + S (bcf_row_index_bclz_choose_table) = S (n)) -> exists bcf_row_code_bclz_choose_table bcf_row_scale_bclz_choose_table. ((((exists bcf_height_bclz_choose_table_decoded_row_code. bcf_height_bclz_choose_table_decoded_row_code + S (bcf_row_code_bclz_choose_table) = S ((S (bcf_row_index_bclz_choose_table)) * bcf_row_code_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_table_decoded_row_code. bcf_row_code_code_bclz_choose = bcf_quotient_bclz_choose_table_decoded_row_code * S ((S (bcf_row_index_bclz_choose_table)) * bcf_row_code_scale_bclz_choose) + (bcf_row_code_bclz_choose_table))) /\ ((((exists bcf_height_bclz_choose_table_decoded_row_scale. bcf_height_bclz_choose_table_decoded_row_scale + S (bcf_row_scale_bclz_choose_table) = S ((S (bcf_row_index_bclz_choose_table)) * bcf_row_scale_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_table_decoded_row_scale. bcf_row_scale_code_bclz_choose = bcf_quotient_bclz_choose_table_decoded_row_scale * S ((S (bcf_row_index_bclz_choose_table)) * bcf_row_scale_scale_bclz_choose) + (bcf_row_scale_bclz_choose_table))) /\ ((bcf_row_index_bclz_choose_table = 0 /\ (forall bcf_index_bclz_choose_table_zero_row. (exists bcf_lt_gap_bclz_choose_table_zero_row_bound. bcf_lt_gap_bclz_choose_table_zero_row_bound + S (bcf_index_bclz_choose_table_zero_row) = S (n)) -> exists bcf_value_bclz_choose_table_zero_row. ((((exists bcf_height_bclz_choose_table_zero_row_entry. bcf_height_bclz_choose_table_zero_row_entry + S (bcf_value_bclz_choose_table_zero_row) = S ((S (bcf_index_bclz_choose_table_zero_row)) * bcf_row_scale_bclz_choose_table)) /\ exists bcf_quotient_bclz_choose_table_zero_row_entry. bcf_row_code_bclz_choose_table = bcf_quotient_bclz_choose_table_zero_row_entry * S ((S (bcf_index_bclz_choose_table_zero_row)) * bcf_row_scale_bclz_choose_table) + (bcf_value_bclz_choose_table_zero_row))) /\ ((bcf_index_bclz_choose_table_zero_row = 0 /\ bcf_value_bclz_choose_table_zero_row = 1) \/ exists bcf_predecessor_bclz_choose_table_zero_row. bcf_index_bclz_choose_table_zero_row = S bcf_predecessor_bclz_choose_table_zero_row /\ bcf_value_bclz_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bclz_choose_table bcf_previous_code_bclz_choose_table bcf_previous_scale_bclz_choose_table. bcf_row_index_bclz_choose_table = S bcf_predecessor_bclz_choose_table /\ ((((exists bcf_height_bclz_choose_table_decoded_previous_code. bcf_height_bclz_choose_table_decoded_previous_code + S (bcf_previous_code_bclz_choose_table) = S ((S (bcf_predecessor_bclz_choose_table)) * bcf_row_code_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_table_decoded_previous_code. bcf_row_code_code_bclz_choose = bcf_quotient_bclz_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bclz_choose_table)) * bcf_row_code_scale_bclz_choose) + (bcf_previous_code_bclz_choose_table))) /\ ((((exists bcf_height_bclz_choose_table_decoded_previous_scale. bcf_height_bclz_choose_table_decoded_previous_scale + S (bcf_previous_scale_bclz_choose_table) = S ((S (bcf_predecessor_bclz_choose_table)) * bcf_row_scale_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_table_decoded_previous_scale. bcf_row_scale_code_bclz_choose = bcf_quotient_bclz_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bclz_choose_table)) * bcf_row_scale_scale_bclz_choose) + (bcf_previous_scale_bclz_choose_table))) /\ (forall bcf_index_bclz_choose_table_row_step. (exists bcf_lt_gap_bclz_choose_table_row_step_bound. bcf_lt_gap_bclz_choose_table_row_step_bound + S (bcf_index_bclz_choose_table_row_step) = S (n)) -> exists bcf_value_bclz_choose_table_row_step. ((((exists bcf_height_bclz_choose_table_row_step_entry. bcf_height_bclz_choose_table_row_step_entry + S (bcf_value_bclz_choose_table_row_step) = S ((S (bcf_index_bclz_choose_table_row_step)) * bcf_row_scale_bclz_choose_table)) /\ exists bcf_quotient_bclz_choose_table_row_step_entry. bcf_row_code_bclz_choose_table = bcf_quotient_bclz_choose_table_row_step_entry * S ((S (bcf_index_bclz_choose_table_row_step)) * bcf_row_scale_bclz_choose_table) + (bcf_value_bclz_choose_table_row_step))) /\ ((bcf_index_bclz_choose_table_row_step = 0 /\ bcf_value_bclz_choose_table_row_step = 1) \/ exists bcf_predecessor_bclz_choose_table_row_step bcf_left_bclz_choose_table_row_step bcf_right_bclz_choose_table_row_step. bcf_index_bclz_choose_table_row_step = S bcf_predecessor_bclz_choose_table_row_step /\ ((((exists bcf_height_bclz_choose_table_row_step_previous_left. bcf_height_bclz_choose_table_row_step_previous_left + S (bcf_left_bclz_choose_table_row_step) = S ((S (bcf_predecessor_bclz_choose_table_row_step)) * bcf_previous_scale_bclz_choose_table)) /\ exists bcf_quotient_bclz_choose_table_row_step_previous_left. bcf_previous_code_bclz_choose_table = bcf_quotient_bclz_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bclz_choose_table_row_step)) * bcf_previous_scale_bclz_choose_table) + (bcf_left_bclz_choose_table_row_step))) /\ ((((exists bcf_height_bclz_choose_table_row_step_previous_right. bcf_height_bclz_choose_table_row_step_previous_right + S (bcf_right_bclz_choose_table_row_step) = S ((S (S (bcf_predecessor_bclz_choose_table_row_step))) * bcf_previous_scale_bclz_choose_table)) /\ exists bcf_quotient_bclz_choose_table_row_step_previous_right. bcf_previous_code_bclz_choose_table = bcf_quotient_bclz_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bclz_choose_table_row_step))) * bcf_previous_scale_bclz_choose_table) + (bcf_right_bclz_choose_table_row_step))) /\ bcf_value_bclz_choose_table_row_step = bcf_left_bclz_choose_table_row_step + bcf_right_bclz_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bclz_choose_decoded_row_code. bcf_height_bclz_choose_decoded_row_code + S (bcf_row_code_bclz_choose) = S ((S (n)) * bcf_row_code_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_decoded_row_code. bcf_row_code_code_bclz_choose = bcf_quotient_bclz_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bclz_choose) + (bcf_row_code_bclz_choose))) /\ ((((exists bcf_height_bclz_choose_decoded_row_scale. bcf_height_bclz_choose_decoded_row_scale + S (bcf_row_scale_bclz_choose) = S ((S (n)) * bcf_row_scale_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_decoded_row_scale. bcf_row_scale_code_bclz_choose = bcf_quotient_bclz_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bclz_choose) + (bcf_row_scale_bclz_choose))) /\ (((exists bcf_height_bclz_choose_decoded_value. bcf_height_bclz_choose_decoded_value + S (z) = S ((S (0)) * bcf_row_scale_bclz_choose)) /\ exists bcf_quotient_bclz_choose_decoded_value. bcf_row_code_bclz_choose = bcf_quotient_bclz_choose_decoded_value * S ((S (0)) * bcf_row_scale_bclz_choose) + (z))))))))) -> z = 1

Proof neighborhood

Direct theorem prerequisites

BT000W zero_le BT001I lt_not_le BT000E le_refl BT0016 succ_le_succ BT000C succ_ne_zero BT0042 beta_at_unique

Direct theorem dependents

BT00TL choose_symmetry BT00TM choose_positive BT00TQ central_binom_zero BT00TT choose_weighted_vertical

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

130 script commands · 29 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 (6)
zero lelt not lele reflsucc le succsucc ne zerobeta at unique
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro z
  3. L3
    intro hchoose
02Separate the logical casesL4–6

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

  1. L4
    cases hchoose
  2. L5
    cases hchoose_left
  3. L6
    exfalso
03Use earlier factsL7–12

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

  1. L7
    specialize lt_not_le n
  2. L8
    specialize lt_not_le 0
  3. L9
    apply lt_not_le
  4. L10
    exact hchoose_left_left
  5. L11
    specialize zero_le n
  6. L12
    exact zero_le
04Separate the logical casesL13–22

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

  1. L13
    cases hchoose_right
  2. L14
    cases hchoose_right_right
  3. L15
    cases hchoose_right_right_witness
  4. L16
    cases hchoose_right_right_witness_witness
  5. L17
    cases hchoose_right_right_witness_witness_witness
  6. L18
    cases hchoose_right_right_witness_witness_witness_witness
  7. L19
    cases hchoose_right_right_witness_witness_witness_witness_witness
  8. L20
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness
  9. L21
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
  10. L22
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
05Establish hrow_boundL23–25

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

  1. L23
    have hrow_bound : Lt(n,S n)Definitions: Lt(n,S n)Original native command in the exact edition
  2. L24
    specialize le_refl (S n)
  3. L25
    exact le_refl
06Establish hinner_boundL26–31

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

  1. L26
    have hinner_bound : Lt(0,S n)Definitions: Lt(0,S n)Original native command in the exact edition
  2. L27
    specialize succ_le_succ 0
  3. L28
    specialize succ_le_succ n
  4. L29
    apply succ_le_succ
  5. L30
    specialize zero_le n
  6. L31
    exact zero_le
07Establish hrowL32–35

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

  1. L32
    have hrow : ∃ bcf_row_code_bclz_table_row. ∃ bcf_row_scale_bclz_table_row. BetaAt(x,x1,n,bcf_row_code_bclz_table_row) ∧ (BetaAt(x2,x3,n,bcf_row_scale_bclz_table_row) ∧ (n = 0 ∧ (∀ y. Lt(y,S n) → ∃ z. BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,y,z) ∧ (y = 0 ∧ z = 1 ∨ (∃ m. y = S m ∧ z = 0))) ∨ (∃ y. ∃ z. ∃ m. n = S y ∧ (BetaAt(x,x1,y,z) ∧ (BetaAt(x2,x3,y,m) ∧ (∀ k. Lt(k,S n) → ∃ i. BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,k,i) ∧ (k = 0 ∧ i = 1 ∨ (∃ j. ∃ u. ∃ v. k = S j ∧ (BetaAt(z,m,j,u) ∧ (BetaAt(z,m,S j,v) ∧ i = u + v))))))))))Definitions: BetaAt(x,x1,n,bcf_row_code_bclz_table_row)BetaAt(x2,x3,n,bcf_row_scale_bclz_table_row)Lt(y,S n)BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,y,z)BetaAt(x,x1,y,z)BetaAt(x2,x3,y,m)Lt(k,S n)BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,k,i)BetaAt(z,m,j,u)BetaAt(z,m,S j,v)Original native command in the exact edition
  2. L33
    specialize hchoose_right_right_witness_witness_witness_witness_witness_witness_left n
  3. L34
    apply hchoose_right_right_witness_witness_witness_witness_witness_witness_left
  4. L35
    exact hrow_bound
08Separate the logical casesL36–39

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

  1. L36
    cases hrow
  2. L37
    cases hrow_witness
  3. L38
    cases hrow_witness_witness
  4. L39
    cases hrow_witness_witness_right
09Establish hcodeL40–48

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

  1. L40
    have hcode : x4 = x6
  2. L41
    specialize beta_at_unique x
  3. L42
    specialize beta_at_unique x1
  4. L43
    specialize beta_at_unique n
  5. L44
    specialize beta_at_unique x4
  6. L45
    specialize beta_at_unique x6
  7. L46
    apply beta_at_unique
  8. L47
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
  9. L48
    exact hrow_witness_witness_left
10Establish hscaleL49–57

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

  1. L49
    have hscale : x5 = x7
  2. L50
    specialize beta_at_unique x2
  3. L51
    specialize beta_at_unique x3
  4. L52
    specialize beta_at_unique n
  5. L53
    specialize beta_at_unique x5
  6. L54
    specialize beta_at_unique x7
  7. L55
    apply beta_at_unique
  8. L56
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  9. L57
    exact hrow_witness_witness_right_left
11Establish hvalueL58–62

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

  1. L58
    have hvalue : BetaAt(x6,x7,0,z)Definitions: BetaAt(x6,x7,0,z)Original native command in the exact edition
  2. L59
    rewrite <- hcode
  3. L60
    rewrite <- hscale
  4. L61
    rewrite <- hscale
  5. L62
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right
12Separate the logical casesL63–64

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

  1. L63
    cases hrow_witness_witness_right_right
  2. L64
    cases hrow_witness_witness_right_right_left
13Establish hcellL65–68

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. L65
    have hcell : ∃ bcf_cell_value_bclz_zero_cell. BetaAt(x6,x7,0,bcf_cell_value_bclz_zero_cell) ∧ (0 = 0 ∧ bcf_cell_value_bclz_zero_cell = 1 ∨ (∃ x. 0 = S x ∧ bcf_cell_value_bclz_zero_cell = 0))Definitions: BetaAt(x6,x7,0,bcf_cell_value_bclz_zero_cell)Original native command in the exact edition
  2. L66
    specialize hrow_witness_witness_right_right_left_right 0
  3. L67
    apply hrow_witness_witness_right_right_left_right
  4. L68
    exact hinner_bound
14Separate the logical casesL69–70

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

  1. L69
    cases hcell
  2. L70
    cases hcell_witness
15Establish hzvalueL71–79

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

  1. L71
    have hzvalue : z = x8
  2. L72
    specialize beta_at_unique x6
  3. L73
    specialize beta_at_unique x7
  4. L74
    specialize beta_at_unique 0
  5. L75
    specialize beta_at_unique z
  6. L76
    specialize beta_at_unique x8
  7. L77
    apply beta_at_unique
  8. L78
    exact hvalue
  9. L79
    exact hcell_witness_left
16Separate the logical casesL80–81

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

  1. L80
    cases hcell_witness_right
  2. L81
    cases hcell_witness_right_left
17Calculate and transport equalitiesL82–82

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

  1. L82
    trans x8
18Use earlier factsL83–84

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

  1. L83
    exact hzvalue
  2. L84
    exact hcell_witness_right_left_right
19Separate the logical casesL85–87

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

  1. L85
    cases hcell_witness_right_right
  2. L86
    cases hcell_witness_right_right_witness
  3. L87
    exfalso
20Establish hbadL88–93

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

  1. L88
    have hbad : S x9 = 0
  2. L89
    symm
  3. L90
    exact hcell_witness_right_right_witness_left
  4. L91
    specialize succ_ne_zero x9
  5. L92
    apply succ_ne_zero
  6. L93
    exact hbad
21Separate the logical casesL94–99

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

  1. L94
    cases hrow_witness_witness_right_right_right
  2. L95
    cases hrow_witness_witness_right_right_right_witness
  3. L96
    cases hrow_witness_witness_right_right_right_witness_witness
  4. L97
    cases hrow_witness_witness_right_right_right_witness_witness_witness
  5. L98
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  6. L99
    cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
22Establish hcellL100–103

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. L100
    have hcell : ∃ bcf_cell_value_bclz_step_cell. BetaAt(x6,x7,0,bcf_cell_value_bclz_step_cell) ∧ (0 = 0 ∧ bcf_cell_value_bclz_step_cell = 1 ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(x9,x10,x,y) ∧ (BetaAt(x9,x10,S x,z) ∧ bcf_cell_value_bclz_step_cell = y + z))))Definitions: BetaAt(x6,x7,0,bcf_cell_value_bclz_step_cell)BetaAt(x9,x10,x,y)BetaAt(x9,x10,S x,z)Original native command in the exact edition
  2. L101
    specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right 0
  3. L102
    apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  4. L103
    exact hinner_bound
23Separate the logical casesL104–105

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

  1. L104
    cases hcell
  2. L105
    cases hcell_witness
24Establish hzvalueL106–114

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

  1. L106
    have hzvalue : z = x11
  2. L107
    specialize beta_at_unique x6
  3. L108
    specialize beta_at_unique x7
  4. L109
    specialize beta_at_unique 0
  5. L110
    specialize beta_at_unique z
  6. L111
    specialize beta_at_unique x11
  7. L112
    apply beta_at_unique
  8. L113
    exact hvalue
  9. L114
    exact hcell_witness_left
25Separate the logical casesL115–116

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

  1. L115
    cases hcell_witness_right
  2. L116
    cases hcell_witness_right_left
26Calculate and transport equalitiesL117–117

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

  1. L117
    trans x11
27Use earlier factsL118–119

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

  1. L118
    exact hzvalue
  2. L119
    exact hcell_witness_right_left_right
28Separate the logical casesL120–124

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
  3. L122
    cases hcell_witness_right_right_witness_witness
  4. L123
    cases hcell_witness_right_right_witness_witness_witness
  5. L124
    exfalso
29Establish hbadL125–130

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

  1. L125
    have hbad : S x12 = 0
  2. L126
    symm
  3. L127
    exact hcell_witness_right_right_witness_witness_witness_left
  4. L128
    specialize succ_ne_zero x12
  5. L129
    apply succ_ne_zero
  6. L130
    exact hbad

Library-wide reading audit

Original defined command ledger · 130 lines
  1. 0001intro n
  2. 0002intro z
  3. 0003intro hchoose
  4. 0004cases hchoose
  5. 0005cases hchoose_left
  6. 0006exfalso
  7. 0007specialize lt_not_le n
  8. 0008specialize lt_not_le 0
  9. 0009apply lt_not_le
  10. 0010exact hchoose_left_left
  11. 0011specialize zero_le n
  12. 0012exact zero_le
  13. 0013cases hchoose_right
  14. 0014cases hchoose_right_right
  15. 0015cases hchoose_right_right_witness
  16. 0016cases hchoose_right_right_witness_witness
  17. 0017cases hchoose_right_right_witness_witness_witness
  18. 0018cases hchoose_right_right_witness_witness_witness_witness
  19. 0019cases hchoose_right_right_witness_witness_witness_witness_witness
  20. 0020cases hchoose_right_right_witness_witness_witness_witness_witness_witness
  21. 0021cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
  22. 0022cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
  23. 0023have hrow_bound : Lt(n,S n)
    Exact native replay linehave hrow_bound : exists bcf_lt_gap_bclz_row_bound. bcf_lt_gap_bclz_row_bound + S (n) = S n
  24. 0024specialize le_refl (S n)
  25. 0025exact le_refl
  26. 0026have hinner_bound : Lt(0,S n)
    Exact native replay linehave hinner_bound : exists bcf_lt_gap_bclz_inner_bound. bcf_lt_gap_bclz_inner_bound + S (0) = S n
  27. 0027specialize succ_le_succ 0
  28. 0028specialize succ_le_succ n
  29. 0029apply succ_le_succ
  30. 0030specialize zero_le n
  31. 0031exact zero_le
  32. 0032have hrow : ∃ bcf_row_code_bclz_table_row. ∃ bcf_row_scale_bclz_table_row. BetaAt(x,x1,n,bcf_row_code_bclz_table_row) ∧ (BetaAt(x2,x3,n,bcf_row_scale_bclz_table_row) ∧ (n = 0 ∧ (∀ y. Lt(y,S n) → ∃ z. BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,y,z) ∧ (y = 0 ∧ z = 1 ∨ (∃ m. y = S m ∧ z = 0))) ∨ (∃ y. ∃ z. ∃ m. n = S y ∧ (BetaAt(x,x1,y,z) ∧ (BetaAt(x2,x3,y,m) ∧ (∀ k. Lt(k,S n) → ∃ i. BetaAt(bcf_row_code_bclz_table_row,bcf_row_scale_bclz_table_row,k,i) ∧ (k = 0 ∧ i = 1 ∨ (∃ j. ∃ u. ∃ v. k = S j ∧ (BetaAt(z,m,j,u) ∧ (BetaAt(z,m,S j,v) ∧ i = u + v))))))))))
    Exact native replay linehave hrow : exists bcf_row_code_bclz_table_row bcf_row_scale_bclz_table_row. ((((exists bcf_height_bclz_table_row_decoded_row_code. bcf_height_bclz_table_row_decoded_row_code + S (bcf_row_code_bclz_table_row) = S ((S (n)) * x1)) /\ exists bcf_quotient_bclz_table_row_decoded_row_code. x = bcf_quotient_bclz_table_row_decoded_row_code * S ((S (n)) * x1) + (bcf_row_code_bclz_table_row))) /\ ((((exists bcf_height_bclz_table_row_decoded_row_scale. bcf_height_bclz_table_row_decoded_row_scale + S (bcf_row_scale_bclz_table_row) = S ((S (n)) * x3)) /\ exists bcf_quotient_bclz_table_row_decoded_row_scale. x2 = bcf_quotient_bclz_table_row_decoded_row_scale * S ((S (n)) * x3) + (bcf_row_scale_bclz_table_row))) /\ ((n = 0 /\ (forall bcf_index_bclz_table_row_zero_row. (exists bcf_lt_gap_bclz_table_row_zero_row_bound. bcf_lt_gap_bclz_table_row_zero_row_bound + S (bcf_index_bclz_table_row_zero_row) = S n) -> exists bcf_value_bclz_table_row_zero_row. ((((exists bcf_height_bclz_table_row_zero_row_entry. bcf_height_bclz_table_row_zero_row_entry + S (bcf_value_bclz_table_row_zero_row) = S ((S (bcf_index_bclz_table_row_zero_row)) * bcf_row_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_zero_row_entry. bcf_row_code_bclz_table_row = bcf_quotient_bclz_table_row_zero_row_entry * S ((S (bcf_index_bclz_table_row_zero_row)) * bcf_row_scale_bclz_table_row) + (bcf_value_bclz_table_row_zero_row))) /\ ((bcf_index_bclz_table_row_zero_row = 0 /\ bcf_value_bclz_table_row_zero_row = 1) \/ exists bcf_predecessor_bclz_table_row_zero_row. bcf_index_bclz_table_row_zero_row = S bcf_predecessor_bclz_table_row_zero_row /\ bcf_value_bclz_table_row_zero_row = 0)))) \/ exists bcf_predecessor_bclz_table_row bcf_previous_code_bclz_table_row bcf_previous_scale_bclz_table_row. n = S bcf_predecessor_bclz_table_row /\ ((((exists bcf_height_bclz_table_row_decoded_previous_code. bcf_height_bclz_table_row_decoded_previous_code + S (bcf_previous_code_bclz_table_row) = S ((S (bcf_predecessor_bclz_table_row)) * x1)) /\ exists bcf_quotient_bclz_table_row_decoded_previous_code. x = bcf_quotient_bclz_table_row_decoded_previous_code * S ((S (bcf_predecessor_bclz_table_row)) * x1) + (bcf_previous_code_bclz_table_row))) /\ ((((exists bcf_height_bclz_table_row_decoded_previous_scale. bcf_height_bclz_table_row_decoded_previous_scale + S (bcf_previous_scale_bclz_table_row) = S ((S (bcf_predecessor_bclz_table_row)) * x3)) /\ exists bcf_quotient_bclz_table_row_decoded_previous_scale. x2 = bcf_quotient_bclz_table_row_decoded_previous_scale * S ((S (bcf_predecessor_bclz_table_row)) * x3) + (bcf_previous_scale_bclz_table_row))) /\ (forall bcf_index_bclz_table_row_row_step. (exists bcf_lt_gap_bclz_table_row_row_step_bound. bcf_lt_gap_bclz_table_row_row_step_bound + S (bcf_index_bclz_table_row_row_step) = S n) -> exists bcf_value_bclz_table_row_row_step. ((((exists bcf_height_bclz_table_row_row_step_entry. bcf_height_bclz_table_row_row_step_entry + S (bcf_value_bclz_table_row_row_step) = S ((S (bcf_index_bclz_table_row_row_step)) * bcf_row_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_entry. bcf_row_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_entry * S ((S (bcf_index_bclz_table_row_row_step)) * bcf_row_scale_bclz_table_row) + (bcf_value_bclz_table_row_row_step))) /\ ((bcf_index_bclz_table_row_row_step = 0 /\ bcf_value_bclz_table_row_row_step = 1) \/ exists bcf_predecessor_bclz_table_row_row_step bcf_left_bclz_table_row_row_step bcf_right_bclz_table_row_row_step. bcf_index_bclz_table_row_row_step = S bcf_predecessor_bclz_table_row_row_step /\ ((((exists bcf_height_bclz_table_row_row_step_previous_left. bcf_height_bclz_table_row_row_step_previous_left + S (bcf_left_bclz_table_row_row_step) = S ((S (bcf_predecessor_bclz_table_row_row_step)) * bcf_previous_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_previous_left. bcf_previous_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_previous_left * S ((S (bcf_predecessor_bclz_table_row_row_step)) * bcf_previous_scale_bclz_table_row) + (bcf_left_bclz_table_row_row_step))) /\ ((((exists bcf_height_bclz_table_row_row_step_previous_right. bcf_height_bclz_table_row_row_step_previous_right + S (bcf_right_bclz_table_row_row_step) = S ((S (S (bcf_predecessor_bclz_table_row_row_step))) * bcf_previous_scale_bclz_table_row)) /\ exists bcf_quotient_bclz_table_row_row_step_previous_right. bcf_previous_code_bclz_table_row = bcf_quotient_bclz_table_row_row_step_previous_right * S ((S (S (bcf_predecessor_bclz_table_row_row_step))) * bcf_previous_scale_bclz_table_row) + (bcf_right_bclz_table_row_row_step))) /\ bcf_value_bclz_table_row_row_step = bcf_left_bclz_table_row_row_step + bcf_right_bclz_table_row_row_step))))))))))
  33. 0033specialize hchoose_right_right_witness_witness_witness_witness_witness_witness_left n
  34. 0034apply hchoose_right_right_witness_witness_witness_witness_witness_witness_left
  35. 0035exact hrow_bound
  36. 0036cases hrow
  37. 0037cases hrow_witness
  38. 0038cases hrow_witness_witness
  39. 0039cases hrow_witness_witness_right
  40. 0040have hcode : x4 = x6
  41. 0041specialize beta_at_unique x
  42. 0042specialize beta_at_unique x1
  43. 0043specialize beta_at_unique n
  44. 0044specialize beta_at_unique x4
  45. 0045specialize beta_at_unique x6
  46. 0046apply beta_at_unique
  47. 0047exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
  48. 0048exact hrow_witness_witness_left
  49. 0049have hscale : x5 = x7
  50. 0050specialize beta_at_unique x2
  51. 0051specialize beta_at_unique x3
  52. 0052specialize beta_at_unique n
  53. 0053specialize beta_at_unique x5
  54. 0054specialize beta_at_unique x7
  55. 0055apply beta_at_unique
  56. 0056exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  57. 0057exact hrow_witness_witness_right_left
  58. 0058have hvalue : BetaAt(x6,x7,0,z)
    Exact native replay linehave hvalue : ((exists bcf_height_bclz_semantic_at. bcf_height_bclz_semantic_at + S (z) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_semantic_at. x6 = bcf_quotient_bclz_semantic_at * S ((S (0)) * x7) + (z))
  59. 0059rewrite <- hcode
  60. 0060rewrite <- hscale
  61. 0061rewrite <- hscale
  62. 0062exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right
  63. 0063cases hrow_witness_witness_right_right
  64. 0064cases hrow_witness_witness_right_right_left
  65. 0065have hcell : ∃ bcf_cell_value_bclz_zero_cell. BetaAt(x6,x7,0,bcf_cell_value_bclz_zero_cell) ∧ (0 = 0 ∧ bcf_cell_value_bclz_zero_cell = 1 ∨ (∃ x. 0 = S x ∧ bcf_cell_value_bclz_zero_cell = 0))
    Exact native replay linehave hcell : exists bcf_cell_value_bclz_zero_cell. ((((exists bcf_height_bclz_zero_cell_entry. bcf_height_bclz_zero_cell_entry + S (bcf_cell_value_bclz_zero_cell) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_zero_cell_entry. x6 = bcf_quotient_bclz_zero_cell_entry * S ((S (0)) * x7) + (bcf_cell_value_bclz_zero_cell))) /\ ((0 = 0 /\ bcf_cell_value_bclz_zero_cell = 1) \/ exists bcf_cell_predecessor_bclz_zero_cell. 0 = S bcf_cell_predecessor_bclz_zero_cell /\ bcf_cell_value_bclz_zero_cell = 0))
  66. 0066specialize hrow_witness_witness_right_right_left_right 0
  67. 0067apply hrow_witness_witness_right_right_left_right
  68. 0068exact hinner_bound
  69. 0069cases hcell
  70. 0070cases hcell_witness
  71. 0071have hzvalue : z = x8
  72. 0072specialize beta_at_unique x6
  73. 0073specialize beta_at_unique x7
  74. 0074specialize beta_at_unique 0
  75. 0075specialize beta_at_unique z
  76. 0076specialize beta_at_unique x8
  77. 0077apply beta_at_unique
  78. 0078exact hvalue
  79. 0079exact hcell_witness_left
  80. 0080cases hcell_witness_right
  81. 0081cases hcell_witness_right_left
  82. 0082trans x8
  83. 0083exact hzvalue
  84. 0084exact hcell_witness_right_left_right
  85. 0085cases hcell_witness_right_right
  86. 0086cases hcell_witness_right_right_witness
  87. 0087exfalso
  88. 0088have hbad : S x9 = 0
  89. 0089symm
  90. 0090exact hcell_witness_right_right_witness_left
  91. 0091specialize succ_ne_zero x9
  92. 0092apply succ_ne_zero
  93. 0093exact hbad
  94. 0094cases hrow_witness_witness_right_right_right
  95. 0095cases hrow_witness_witness_right_right_right_witness
  96. 0096cases hrow_witness_witness_right_right_right_witness_witness
  97. 0097cases hrow_witness_witness_right_right_right_witness_witness_witness
  98. 0098cases hrow_witness_witness_right_right_right_witness_witness_witness_right
  99. 0099cases hrow_witness_witness_right_right_right_witness_witness_witness_right_right
  100. 0100have hcell : ∃ bcf_cell_value_bclz_step_cell. BetaAt(x6,x7,0,bcf_cell_value_bclz_step_cell) ∧ (0 = 0 ∧ bcf_cell_value_bclz_step_cell = 1 ∨ (∃ x. ∃ y. ∃ z. 0 = S x ∧ (BetaAt(x9,x10,x,y) ∧ (BetaAt(x9,x10,S x,z) ∧ bcf_cell_value_bclz_step_cell = y + z))))
    Exact native replay linehave hcell : exists bcf_cell_value_bclz_step_cell. ((((exists bcf_height_bclz_step_cell_entry. bcf_height_bclz_step_cell_entry + S (bcf_cell_value_bclz_step_cell) = S ((S (0)) * x7)) /\ exists bcf_quotient_bclz_step_cell_entry. x6 = bcf_quotient_bclz_step_cell_entry * S ((S (0)) * x7) + (bcf_cell_value_bclz_step_cell))) /\ ((0 = 0 /\ bcf_cell_value_bclz_step_cell = 1) \/ exists bcf_cell_predecessor_bclz_step_cell bcf_cell_left_bclz_step_cell bcf_cell_right_bclz_step_cell. 0 = S bcf_cell_predecessor_bclz_step_cell /\ ((((exists bcf_height_bclz_step_cell_previous_left. bcf_height_bclz_step_cell_previous_left + S (bcf_cell_left_bclz_step_cell) = S ((S (bcf_cell_predecessor_bclz_step_cell)) * x10)) /\ exists bcf_quotient_bclz_step_cell_previous_left. x9 = bcf_quotient_bclz_step_cell_previous_left * S ((S (bcf_cell_predecessor_bclz_step_cell)) * x10) + (bcf_cell_left_bclz_step_cell))) /\ ((((exists bcf_height_bclz_step_cell_previous_right. bcf_height_bclz_step_cell_previous_right + S (bcf_cell_right_bclz_step_cell) = S ((S (S (bcf_cell_predecessor_bclz_step_cell))) * x10)) /\ exists bcf_quotient_bclz_step_cell_previous_right. x9 = bcf_quotient_bclz_step_cell_previous_right * S ((S (S (bcf_cell_predecessor_bclz_step_cell))) * x10) + (bcf_cell_right_bclz_step_cell))) /\ bcf_cell_value_bclz_step_cell = bcf_cell_left_bclz_step_cell + bcf_cell_right_bclz_step_cell))))
  101. 0101specialize hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right 0
  102. 0102apply hrow_witness_witness_right_right_right_witness_witness_witness_right_right_right
  103. 0103exact hinner_bound
  104. 0104cases hcell
  105. 0105cases hcell_witness
  106. 0106have hzvalue : z = x11
  107. 0107specialize beta_at_unique x6
  108. 0108specialize beta_at_unique x7
  109. 0109specialize beta_at_unique 0
  110. 0110specialize beta_at_unique z
  111. 0111specialize beta_at_unique x11
  112. 0112apply beta_at_unique
  113. 0113exact hvalue
  114. 0114exact hcell_witness_left
  115. 0115cases hcell_witness_right
  116. 0116cases hcell_witness_right_left
  117. 0117trans x11
  118. 0118exact hzvalue
  119. 0119exact hcell_witness_right_left_right
  120. 0120cases hcell_witness_right_right
  121. 0121cases hcell_witness_right_right_witness
  122. 0122cases hcell_witness_right_right_witness_witness
  123. 0123cases hcell_witness_right_right_witness_witness_witness
  124. 0124exfalso
  125. 0125have hbad : S x12 = 0
  126. 0126symm
  127. 0127exact hcell_witness_right_right_witness_witness_witness_left
  128. 0128specialize succ_ne_zero x12
  129. 0129apply succ_ne_zero
  130. 0130exact hbad