BT00TG · Bertrand theorem

choose_self

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

The recurrence-defined diagonal binomial coefficient 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,n,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

22 occurrences

Exact expanded native-PA statement
forall n z. (((exists bcf_lt_gap_bcs_choose_out_of_range. bcf_lt_gap_bcs_choose_out_of_range + S (n) = n) /\ z = 0) \/ ((exists bcf_le_gap_bcs_choose_in_range. bcf_le_gap_bcs_choose_in_range + (n) = n) /\ (exists bcf_row_code_code_bcs_choose bcf_row_code_scale_bcs_choose bcf_row_scale_code_bcs_choose bcf_row_scale_scale_bcs_choose bcf_row_code_bcs_choose bcf_row_scale_bcs_choose. ((forall bcf_row_index_bcs_choose_table. (exists bcf_lt_gap_bcs_choose_table_row_bound. bcf_lt_gap_bcs_choose_table_row_bound + S (bcf_row_index_bcs_choose_table) = S (n)) -> exists bcf_row_code_bcs_choose_table bcf_row_scale_bcs_choose_table. ((((exists bcf_height_bcs_choose_table_decoded_row_code. bcf_height_bcs_choose_table_decoded_row_code + S (bcf_row_code_bcs_choose_table) = S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_row_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_row_code * S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_code_scale_bcs_choose) + (bcf_row_code_bcs_choose_table))) /\ ((((exists bcf_height_bcs_choose_table_decoded_row_scale. bcf_height_bcs_choose_table_decoded_row_scale + S (bcf_row_scale_bcs_choose_table) = S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_row_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_row_scale * S ((S (bcf_row_index_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose) + (bcf_row_scale_bcs_choose_table))) /\ ((bcf_row_index_bcs_choose_table = 0 /\ (forall bcf_index_bcs_choose_table_zero_row. (exists bcf_lt_gap_bcs_choose_table_zero_row_bound. bcf_lt_gap_bcs_choose_table_zero_row_bound + S (bcf_index_bcs_choose_table_zero_row) = S (n)) -> exists bcf_value_bcs_choose_table_zero_row. ((((exists bcf_height_bcs_choose_table_zero_row_entry. bcf_height_bcs_choose_table_zero_row_entry + S (bcf_value_bcs_choose_table_zero_row) = S ((S (bcf_index_bcs_choose_table_zero_row)) * bcf_row_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_zero_row_entry. bcf_row_code_bcs_choose_table = bcf_quotient_bcs_choose_table_zero_row_entry * S ((S (bcf_index_bcs_choose_table_zero_row)) * bcf_row_scale_bcs_choose_table) + (bcf_value_bcs_choose_table_zero_row))) /\ ((bcf_index_bcs_choose_table_zero_row = 0 /\ bcf_value_bcs_choose_table_zero_row = 1) \/ exists bcf_predecessor_bcs_choose_table_zero_row. bcf_index_bcs_choose_table_zero_row = S bcf_predecessor_bcs_choose_table_zero_row /\ bcf_value_bcs_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_choose_table bcf_previous_code_bcs_choose_table bcf_previous_scale_bcs_choose_table. bcf_row_index_bcs_choose_table = S bcf_predecessor_bcs_choose_table /\ ((((exists bcf_height_bcs_choose_table_decoded_previous_code. bcf_height_bcs_choose_table_decoded_previous_code + S (bcf_previous_code_bcs_choose_table) = S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_previous_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_code_scale_bcs_choose) + (bcf_previous_code_bcs_choose_table))) /\ ((((exists bcf_height_bcs_choose_table_decoded_previous_scale. bcf_height_bcs_choose_table_decoded_previous_scale + S (bcf_previous_scale_bcs_choose_table) = S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_table_decoded_previous_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_choose_table)) * bcf_row_scale_scale_bcs_choose) + (bcf_previous_scale_bcs_choose_table))) /\ (forall bcf_index_bcs_choose_table_row_step. (exists bcf_lt_gap_bcs_choose_table_row_step_bound. bcf_lt_gap_bcs_choose_table_row_step_bound + S (bcf_index_bcs_choose_table_row_step) = S (n)) -> exists bcf_value_bcs_choose_table_row_step. ((((exists bcf_height_bcs_choose_table_row_step_entry. bcf_height_bcs_choose_table_row_step_entry + S (bcf_value_bcs_choose_table_row_step) = S ((S (bcf_index_bcs_choose_table_row_step)) * bcf_row_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_entry. bcf_row_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_entry * S ((S (bcf_index_bcs_choose_table_row_step)) * bcf_row_scale_bcs_choose_table) + (bcf_value_bcs_choose_table_row_step))) /\ ((bcf_index_bcs_choose_table_row_step = 0 /\ bcf_value_bcs_choose_table_row_step = 1) \/ exists bcf_predecessor_bcs_choose_table_row_step bcf_left_bcs_choose_table_row_step bcf_right_bcs_choose_table_row_step. bcf_index_bcs_choose_table_row_step = S bcf_predecessor_bcs_choose_table_row_step /\ ((((exists bcf_height_bcs_choose_table_row_step_previous_left. bcf_height_bcs_choose_table_row_step_previous_left + S (bcf_left_bcs_choose_table_row_step) = S ((S (bcf_predecessor_bcs_choose_table_row_step)) * bcf_previous_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_previous_left. bcf_previous_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_choose_table_row_step)) * bcf_previous_scale_bcs_choose_table) + (bcf_left_bcs_choose_table_row_step))) /\ ((((exists bcf_height_bcs_choose_table_row_step_previous_right. bcf_height_bcs_choose_table_row_step_previous_right + S (bcf_right_bcs_choose_table_row_step) = S ((S (S (bcf_predecessor_bcs_choose_table_row_step))) * bcf_previous_scale_bcs_choose_table)) /\ exists bcf_quotient_bcs_choose_table_row_step_previous_right. bcf_previous_code_bcs_choose_table = bcf_quotient_bcs_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_choose_table_row_step))) * bcf_previous_scale_bcs_choose_table) + (bcf_right_bcs_choose_table_row_step))) /\ bcf_value_bcs_choose_table_row_step = bcf_left_bcs_choose_table_row_step + bcf_right_bcs_choose_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_choose_decoded_row_code. bcf_height_bcs_choose_decoded_row_code + S (bcf_row_code_bcs_choose) = S ((S (n)) * bcf_row_code_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_row_code. bcf_row_code_code_bcs_choose = bcf_quotient_bcs_choose_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_choose) + (bcf_row_code_bcs_choose))) /\ ((((exists bcf_height_bcs_choose_decoded_row_scale. bcf_height_bcs_choose_decoded_row_scale + S (bcf_row_scale_bcs_choose) = S ((S (n)) * bcf_row_scale_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_row_scale. bcf_row_scale_code_bcs_choose = bcf_quotient_bcs_choose_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_choose) + (bcf_row_scale_bcs_choose))) /\ (((exists bcf_height_bcs_choose_decoded_value. bcf_height_bcs_choose_decoded_value + S (z) = S ((S (n)) * bcf_row_scale_bcs_choose)) /\ exists bcf_quotient_bcs_choose_decoded_value. bcf_row_code_bcs_choose = bcf_quotient_bcs_choose_decoded_value * S ((S (n)) * bcf_row_scale_bcs_choose) + (z))))))))) -> z = 1

Proof neighborhood

Direct theorem prerequisites

BT001B lt_irrefl_expanded BT000E le_refl BT00TF beta_pascal_table_diagonal_boundary

Direct theorem dependents

BT00TJ choose_succ_succ BT00TK choose_self_of_eq

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

48 script commands · 10 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
lt irrefl expandedle reflbeta pascal table diagonal boundary
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–9

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

  1. L7
    specialize lt_irrefl_expanded n
  2. L8
    apply lt_irrefl_expanded
  3. L9
    exact hchoose_left_left
04Separate the logical casesL10–19

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

  1. L10
    cases hchoose_right
  2. L11
    cases hchoose_right_right
  3. L12
    cases hchoose_right_right_witness
  4. L13
    cases hchoose_right_right_witness_witness
  5. L14
    cases hchoose_right_right_witness_witness_witness
  6. L15
    cases hchoose_right_right_witness_witness_witness_witness
  7. L16
    cases hchoose_right_right_witness_witness_witness_witness_witness
  8. L17
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness
  9. L18
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
  10. L19
    cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
05Establish hboundL20–22

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

  1. L20
    have hbound : Lt(n,S n)Definitions: Lt(n,S n)Original native command in the exact edition
  2. L21
    specialize le_refl (S n)
  3. L22
    exact le_refl
06Establish htable_familyL23–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pascal table diagonal boundary.

  1. L23
    have htable_family : ∀ bcf_row_index_bcs_table_family. Lt(bcf_row_index_bcs_table_family,S n) → ∀ y. ∀ z. BetaAt(x,x1,bcf_row_index_bcs_table_family,y) → BetaAt(x2,x3,bcf_row_index_bcs_table_family,z) → (Lt(bcf_row_index_bcs_table_family,S n) → ∀ m. BetaAt(y,z,bcf_row_index_bcs_table_family,m) → m = 1) ∧ (∀ m. ∀ k. Lt(bcf_row_index_bcs_table_family,m) → Lt(m,S n) → BetaAt(y,z,m,k) → k = 0)Definitions: Lt(bcf_row_index_bcs_table_family,S n)BetaAt(x,x1,bcf_row_index_bcs_table_family,y)BetaAt(x2,x3,bcf_row_index_bcs_table_family,z)BetaAt(y,z,bcf_row_index_bcs_table_family,m)Lt(bcf_row_index_bcs_table_family,m)Lt(m,S n)BetaAt(y,z,m,k)Original native command in the exact edition
  2. L24
    specialize beta_pascal_table_diagonal_boundary x
  3. L25
    specialize beta_pascal_table_diagonal_boundary x1
  4. L26
    specialize beta_pascal_table_diagonal_boundary x2
  5. L27
    specialize beta_pascal_table_diagonal_boundary x3
  6. L28
    specialize beta_pascal_table_diagonal_boundary (S n)
  7. L29
    specialize beta_pascal_table_diagonal_boundary (S n)
  8. L30
    apply beta_pascal_table_diagonal_boundary
  9. L31
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_left
07Establish hrow_familyL32–35

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

  1. L32
    have hrow_family : ∀ bcf_row_code_bcs_row_family. ∀ bcf_row_scale_bcs_row_family. BetaAt(x,x1,n,bcf_row_code_bcs_row_family) → BetaAt(x2,x3,n,bcf_row_scale_bcs_row_family) → (Lt(n,S n) → ∀ y. BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,n,y) → y = 1) ∧ (∀ y. ∀ z. Lt(n,y) → Lt(y,S n) → BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,y,z) → z = 0)Definitions: BetaAt(x,x1,n,bcf_row_code_bcs_row_family)BetaAt(x2,x3,n,bcf_row_scale_bcs_row_family)Lt(n,S n)BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,n,y)Lt(n,y)Lt(y,S n)BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,y,z)Original native command in the exact edition
  2. L33
    specialize htable_family n
  3. L34
    apply htable_family
  4. L35
    exact hbound
08Establish hboundaryL36–41

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

  1. L36
    have hboundary : (Lt(n,S n) → ∀ x. BetaAt(x4,x5,n,x) → x = 1) ∧ (∀ x. ∀ y. Lt(n,x) → Lt(x,S n) → BetaAt(x4,x5,x,y) → y = 0)Definitions: Lt(n,S n)BetaAt(x4,x5,n,x)Lt(n,x)Lt(x,S n)BetaAt(x4,x5,x,y)Original native command in the exact edition
  2. L37
    specialize hrow_family x4
  3. L38
    specialize hrow_family x5
  4. L39
    apply hrow_family
  5. L40
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
  6. L41
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
09Separate the logical casesL42–42

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

  1. L42
    cases hboundary
10Establish hdiagonalL43–48

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

  1. L43
    have hdiagonal : ∀ z. BetaAt(x4,x5,n,z) → z = 1Definitions: BetaAt(x4,x5,n,z)Original native command in the exact edition
  2. L44
    apply hboundary_left
  3. L45
    exact hbound
  4. L46
    specialize hdiagonal z
  5. L47
    apply hdiagonal
  6. L48
    exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro n
  2. 0002intro z
  3. 0003intro hchoose
  4. 0004cases hchoose
  5. 0005cases hchoose_left
  6. 0006exfalso
  7. 0007specialize lt_irrefl_expanded n
  8. 0008apply lt_irrefl_expanded
  9. 0009exact hchoose_left_left
  10. 0010cases hchoose_right
  11. 0011cases hchoose_right_right
  12. 0012cases hchoose_right_right_witness
  13. 0013cases hchoose_right_right_witness_witness
  14. 0014cases hchoose_right_right_witness_witness_witness
  15. 0015cases hchoose_right_right_witness_witness_witness_witness
  16. 0016cases hchoose_right_right_witness_witness_witness_witness_witness
  17. 0017cases hchoose_right_right_witness_witness_witness_witness_witness_witness
  18. 0018cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right
  19. 0019cases hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right
  20. 0020have hbound : Lt(n,S n)
    Exact native replay linehave hbound : exists bcf_lt_gap_bcs_row_bound. bcf_lt_gap_bcs_row_bound + S (n) = S n
  21. 0021specialize le_refl (S n)
  22. 0022exact le_refl
  23. 0023have htable_family : ∀ bcf_row_index_bcs_table_family. Lt(bcf_row_index_bcs_table_family,S n) → ∀ y. ∀ z. BetaAt(x,x1,bcf_row_index_bcs_table_family,y) → BetaAt(x2,x3,bcf_row_index_bcs_table_family,z) → (Lt(bcf_row_index_bcs_table_family,S n) → ∀ m. BetaAt(y,z,bcf_row_index_bcs_table_family,m) → m = 1) ∧ (∀ m. ∀ k. Lt(bcf_row_index_bcs_table_family,m) → Lt(m,S n) → BetaAt(y,z,m,k) → k = 0)
    Exact native replay linehave htable_family : forall bcf_row_index_bcs_table_family. (exists bcf_lt_gap_bcs_table_family_bound. bcf_lt_gap_bcs_table_family_bound + S (bcf_row_index_bcs_table_family) = S n) -> (forall bcf_row_code_bcs_table_family_rows bcf_row_scale_bcs_table_family_rows. (((exists bcf_height_bcs_table_family_rows_code_at. bcf_height_bcs_table_family_rows_code_at + S (bcf_row_code_bcs_table_family_rows) = S ((S (bcf_row_index_bcs_table_family)) * x1)) /\ exists bcf_quotient_bcs_table_family_rows_code_at. x = bcf_quotient_bcs_table_family_rows_code_at * S ((S (bcf_row_index_bcs_table_family)) * x1) + (bcf_row_code_bcs_table_family_rows))) -> (((exists bcf_height_bcs_table_family_rows_scale_at. bcf_height_bcs_table_family_rows_scale_at + S (bcf_row_scale_bcs_table_family_rows) = S ((S (bcf_row_index_bcs_table_family)) * x3)) /\ exists bcf_quotient_bcs_table_family_rows_scale_at. x2 = bcf_quotient_bcs_table_family_rows_scale_at * S ((S (bcf_row_index_bcs_table_family)) * x3) + (bcf_row_scale_bcs_table_family_rows))) -> ((((exists bcf_lt_gap_bcs_table_family_rows_boundary_diagonal_bound. bcf_lt_gap_bcs_table_family_rows_boundary_diagonal_bound + S (bcf_row_index_bcs_table_family) = S n) -> forall bcf_diagonal_value_bcs_table_family_rows_boundary. (((exists bcf_height_bcs_table_family_rows_boundary_diagonal_at. bcf_height_bcs_table_family_rows_boundary_diagonal_at + S (bcf_diagonal_value_bcs_table_family_rows_boundary) = S ((S (bcf_row_index_bcs_table_family)) * bcf_row_scale_bcs_table_family_rows)) /\ exists bcf_quotient_bcs_table_family_rows_boundary_diagonal_at. bcf_row_code_bcs_table_family_rows = bcf_quotient_bcs_table_family_rows_boundary_diagonal_at * S ((S (bcf_row_index_bcs_table_family)) * bcf_row_scale_bcs_table_family_rows) + (bcf_diagonal_value_bcs_table_family_rows_boundary))) -> bcf_diagonal_value_bcs_table_family_rows_boundary = 1) /\ forall bcf_above_index_bcs_table_family_rows_boundary bcf_above_value_bcs_table_family_rows_boundary. (exists bcf_lt_gap_bcs_table_family_rows_boundary_above_order. bcf_lt_gap_bcs_table_family_rows_boundary_above_order + S (bcf_row_index_bcs_table_family) = bcf_above_index_bcs_table_family_rows_boundary) -> (exists bcf_lt_gap_bcs_table_family_rows_boundary_above_bound. bcf_lt_gap_bcs_table_family_rows_boundary_above_bound + S (bcf_above_index_bcs_table_family_rows_boundary) = S n) -> (((exists bcf_height_bcs_table_family_rows_boundary_above_at. bcf_height_bcs_table_family_rows_boundary_above_at + S (bcf_above_value_bcs_table_family_rows_boundary) = S ((S (bcf_above_index_bcs_table_family_rows_boundary)) * bcf_row_scale_bcs_table_family_rows)) /\ exists bcf_quotient_bcs_table_family_rows_boundary_above_at. bcf_row_code_bcs_table_family_rows = bcf_quotient_bcs_table_family_rows_boundary_above_at * S ((S (bcf_above_index_bcs_table_family_rows_boundary)) * bcf_row_scale_bcs_table_family_rows) + (bcf_above_value_bcs_table_family_rows_boundary))) -> bcf_above_value_bcs_table_family_rows_boundary = 0)))
  24. 0024specialize beta_pascal_table_diagonal_boundary x
  25. 0025specialize beta_pascal_table_diagonal_boundary x1
  26. 0026specialize beta_pascal_table_diagonal_boundary x2
  27. 0027specialize beta_pascal_table_diagonal_boundary x3
  28. 0028specialize beta_pascal_table_diagonal_boundary (S n)
  29. 0029specialize beta_pascal_table_diagonal_boundary (S n)
  30. 0030apply beta_pascal_table_diagonal_boundary
  31. 0031exact hchoose_right_right_witness_witness_witness_witness_witness_witness_left
  32. 0032have hrow_family : ∀ bcf_row_code_bcs_row_family. ∀ bcf_row_scale_bcs_row_family. BetaAt(x,x1,n,bcf_row_code_bcs_row_family) → BetaAt(x2,x3,n,bcf_row_scale_bcs_row_family) → (Lt(n,S n) → ∀ y. BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,n,y) → y = 1) ∧ (∀ y. ∀ z. Lt(n,y) → Lt(y,S n) → BetaAt(bcf_row_code_bcs_row_family,bcf_row_scale_bcs_row_family,y,z) → z = 0)
    Exact native replay linehave hrow_family : forall bcf_row_code_bcs_row_family bcf_row_scale_bcs_row_family. (((exists bcf_height_bcs_row_family_code_at. bcf_height_bcs_row_family_code_at + S (bcf_row_code_bcs_row_family) = S ((S (n)) * x1)) /\ exists bcf_quotient_bcs_row_family_code_at. x = bcf_quotient_bcs_row_family_code_at * S ((S (n)) * x1) + (bcf_row_code_bcs_row_family))) -> (((exists bcf_height_bcs_row_family_scale_at. bcf_height_bcs_row_family_scale_at + S (bcf_row_scale_bcs_row_family) = S ((S (n)) * x3)) /\ exists bcf_quotient_bcs_row_family_scale_at. x2 = bcf_quotient_bcs_row_family_scale_at * S ((S (n)) * x3) + (bcf_row_scale_bcs_row_family))) -> ((((exists bcf_lt_gap_bcs_row_family_boundary_diagonal_bound. bcf_lt_gap_bcs_row_family_boundary_diagonal_bound + S (n) = S n) -> forall bcf_diagonal_value_bcs_row_family_boundary. (((exists bcf_height_bcs_row_family_boundary_diagonal_at. bcf_height_bcs_row_family_boundary_diagonal_at + S (bcf_diagonal_value_bcs_row_family_boundary) = S ((S (n)) * bcf_row_scale_bcs_row_family)) /\ exists bcf_quotient_bcs_row_family_boundary_diagonal_at. bcf_row_code_bcs_row_family = bcf_quotient_bcs_row_family_boundary_diagonal_at * S ((S (n)) * bcf_row_scale_bcs_row_family) + (bcf_diagonal_value_bcs_row_family_boundary))) -> bcf_diagonal_value_bcs_row_family_boundary = 1) /\ forall bcf_above_index_bcs_row_family_boundary bcf_above_value_bcs_row_family_boundary. (exists bcf_lt_gap_bcs_row_family_boundary_above_order. bcf_lt_gap_bcs_row_family_boundary_above_order + S (n) = bcf_above_index_bcs_row_family_boundary) -> (exists bcf_lt_gap_bcs_row_family_boundary_above_bound. bcf_lt_gap_bcs_row_family_boundary_above_bound + S (bcf_above_index_bcs_row_family_boundary) = S n) -> (((exists bcf_height_bcs_row_family_boundary_above_at. bcf_height_bcs_row_family_boundary_above_at + S (bcf_above_value_bcs_row_family_boundary) = S ((S (bcf_above_index_bcs_row_family_boundary)) * bcf_row_scale_bcs_row_family)) /\ exists bcf_quotient_bcs_row_family_boundary_above_at. bcf_row_code_bcs_row_family = bcf_quotient_bcs_row_family_boundary_above_at * S ((S (bcf_above_index_bcs_row_family_boundary)) * bcf_row_scale_bcs_row_family) + (bcf_above_value_bcs_row_family_boundary))) -> bcf_above_value_bcs_row_family_boundary = 0))
  33. 0033specialize htable_family n
  34. 0034apply htable_family
  35. 0035exact hbound
  36. 0036have hboundary : (Lt(n,S n) → ∀ x. BetaAt(x4,x5,n,x) → x = 1) ∧ (∀ x. ∀ y. Lt(n,x) → Lt(x,S n) → BetaAt(x4,x5,x,y) → y = 0)
    Exact native replay linehave hboundary : (((exists bcf_lt_gap_bcs_boundary_diagonal_bound. bcf_lt_gap_bcs_boundary_diagonal_bound + S (n) = S n) -> forall bcf_diagonal_value_bcs_boundary. (((exists bcf_height_bcs_boundary_diagonal_at. bcf_height_bcs_boundary_diagonal_at + S (bcf_diagonal_value_bcs_boundary) = S ((S (n)) * x5)) /\ exists bcf_quotient_bcs_boundary_diagonal_at. x4 = bcf_quotient_bcs_boundary_diagonal_at * S ((S (n)) * x5) + (bcf_diagonal_value_bcs_boundary))) -> bcf_diagonal_value_bcs_boundary = 1) /\ forall bcf_above_index_bcs_boundary bcf_above_value_bcs_boundary. (exists bcf_lt_gap_bcs_boundary_above_order. bcf_lt_gap_bcs_boundary_above_order + S (n) = bcf_above_index_bcs_boundary) -> (exists bcf_lt_gap_bcs_boundary_above_bound. bcf_lt_gap_bcs_boundary_above_bound + S (bcf_above_index_bcs_boundary) = S n) -> (((exists bcf_height_bcs_boundary_above_at. bcf_height_bcs_boundary_above_at + S (bcf_above_value_bcs_boundary) = S ((S (bcf_above_index_bcs_boundary)) * x5)) /\ exists bcf_quotient_bcs_boundary_above_at. x4 = bcf_quotient_bcs_boundary_above_at * S ((S (bcf_above_index_bcs_boundary)) * x5) + (bcf_above_value_bcs_boundary))) -> bcf_above_value_bcs_boundary = 0)
  37. 0037specialize hrow_family x4
  38. 0038specialize hrow_family x5
  39. 0039apply hrow_family
  40. 0040exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_left
  41. 0041exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_left
  42. 0042cases hboundary
  43. 0043have hdiagonal : ∀ z. BetaAt(x4,x5,n,z) → z = 1
    Exact native replay linehave hdiagonal : forall z. (((exists bcf_height_bcs_diagonal_family. bcf_height_bcs_diagonal_family + S (z) = S ((S (n)) * x5)) /\ exists bcf_quotient_bcs_diagonal_family. x4 = bcf_quotient_bcs_diagonal_family * S ((S (n)) * x5) + (z))) -> z = 1
  44. 0044apply hboundary_left
  45. 0045exact hbound
  46. 0046specialize hdiagonal z
  47. 0047apply hdiagonal
  48. 0048exact hchoose_right_right_witness_witness_witness_witness_witness_witness_right_right_right