BT00TL · Bertrand theorem

choose_symmetry

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

Complementary columns have equal relational Choose values.

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. ∀ k. ∀ j. ∀ x. ∀ y. k + j = n → Choose(n,k,x) → Choose(n,j,y) → x = y

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

2 occurrences

In local proof propositions

PD0041 Choose

4 occurrences

Exact expanded native-PA statement
forall n k j x y. k + j = n -> (((exists bcf_lt_gap_bcsym_left_out_of_range. bcf_lt_gap_bcsym_left_out_of_range + S (n) = k) /\ x = 0) \/ ((exists bcf_le_gap_bcsym_left_in_range. bcf_le_gap_bcsym_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcsym_left bcf_row_code_scale_bcsym_left bcf_row_scale_code_bcsym_left bcf_row_scale_scale_bcsym_left bcf_row_code_bcsym_left bcf_row_scale_bcsym_left. ((forall bcf_row_index_bcsym_left_table. (exists bcf_lt_gap_bcsym_left_table_row_bound. bcf_lt_gap_bcsym_left_table_row_bound + S (bcf_row_index_bcsym_left_table) = S (n)) -> exists bcf_row_code_bcsym_left_table bcf_row_scale_bcsym_left_table. ((((exists bcf_height_bcsym_left_table_decoded_row_code. bcf_height_bcsym_left_table_decoded_row_code + S (bcf_row_code_bcsym_left_table) = S ((S (bcf_row_index_bcsym_left_table)) * bcf_row_code_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_table_decoded_row_code. bcf_row_code_code_bcsym_left = bcf_quotient_bcsym_left_table_decoded_row_code * S ((S (bcf_row_index_bcsym_left_table)) * bcf_row_code_scale_bcsym_left) + (bcf_row_code_bcsym_left_table))) /\ ((((exists bcf_height_bcsym_left_table_decoded_row_scale. bcf_height_bcsym_left_table_decoded_row_scale + S (bcf_row_scale_bcsym_left_table) = S ((S (bcf_row_index_bcsym_left_table)) * bcf_row_scale_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_table_decoded_row_scale. bcf_row_scale_code_bcsym_left = bcf_quotient_bcsym_left_table_decoded_row_scale * S ((S (bcf_row_index_bcsym_left_table)) * bcf_row_scale_scale_bcsym_left) + (bcf_row_scale_bcsym_left_table))) /\ ((bcf_row_index_bcsym_left_table = 0 /\ (forall bcf_index_bcsym_left_table_zero_row. (exists bcf_lt_gap_bcsym_left_table_zero_row_bound. bcf_lt_gap_bcsym_left_table_zero_row_bound + S (bcf_index_bcsym_left_table_zero_row) = S (n)) -> exists bcf_value_bcsym_left_table_zero_row. ((((exists bcf_height_bcsym_left_table_zero_row_entry. bcf_height_bcsym_left_table_zero_row_entry + S (bcf_value_bcsym_left_table_zero_row) = S ((S (bcf_index_bcsym_left_table_zero_row)) * bcf_row_scale_bcsym_left_table)) /\ exists bcf_quotient_bcsym_left_table_zero_row_entry. bcf_row_code_bcsym_left_table = bcf_quotient_bcsym_left_table_zero_row_entry * S ((S (bcf_index_bcsym_left_table_zero_row)) * bcf_row_scale_bcsym_left_table) + (bcf_value_bcsym_left_table_zero_row))) /\ ((bcf_index_bcsym_left_table_zero_row = 0 /\ bcf_value_bcsym_left_table_zero_row = 1) \/ exists bcf_predecessor_bcsym_left_table_zero_row. bcf_index_bcsym_left_table_zero_row = S bcf_predecessor_bcsym_left_table_zero_row /\ bcf_value_bcsym_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcsym_left_table bcf_previous_code_bcsym_left_table bcf_previous_scale_bcsym_left_table. bcf_row_index_bcsym_left_table = S bcf_predecessor_bcsym_left_table /\ ((((exists bcf_height_bcsym_left_table_decoded_previous_code. bcf_height_bcsym_left_table_decoded_previous_code + S (bcf_previous_code_bcsym_left_table) = S ((S (bcf_predecessor_bcsym_left_table)) * bcf_row_code_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_table_decoded_previous_code. bcf_row_code_code_bcsym_left = bcf_quotient_bcsym_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcsym_left_table)) * bcf_row_code_scale_bcsym_left) + (bcf_previous_code_bcsym_left_table))) /\ ((((exists bcf_height_bcsym_left_table_decoded_previous_scale. bcf_height_bcsym_left_table_decoded_previous_scale + S (bcf_previous_scale_bcsym_left_table) = S ((S (bcf_predecessor_bcsym_left_table)) * bcf_row_scale_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_table_decoded_previous_scale. bcf_row_scale_code_bcsym_left = bcf_quotient_bcsym_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcsym_left_table)) * bcf_row_scale_scale_bcsym_left) + (bcf_previous_scale_bcsym_left_table))) /\ (forall bcf_index_bcsym_left_table_row_step. (exists bcf_lt_gap_bcsym_left_table_row_step_bound. bcf_lt_gap_bcsym_left_table_row_step_bound + S (bcf_index_bcsym_left_table_row_step) = S (n)) -> exists bcf_value_bcsym_left_table_row_step. ((((exists bcf_height_bcsym_left_table_row_step_entry. bcf_height_bcsym_left_table_row_step_entry + S (bcf_value_bcsym_left_table_row_step) = S ((S (bcf_index_bcsym_left_table_row_step)) * bcf_row_scale_bcsym_left_table)) /\ exists bcf_quotient_bcsym_left_table_row_step_entry. bcf_row_code_bcsym_left_table = bcf_quotient_bcsym_left_table_row_step_entry * S ((S (bcf_index_bcsym_left_table_row_step)) * bcf_row_scale_bcsym_left_table) + (bcf_value_bcsym_left_table_row_step))) /\ ((bcf_index_bcsym_left_table_row_step = 0 /\ bcf_value_bcsym_left_table_row_step = 1) \/ exists bcf_predecessor_bcsym_left_table_row_step bcf_left_bcsym_left_table_row_step bcf_right_bcsym_left_table_row_step. bcf_index_bcsym_left_table_row_step = S bcf_predecessor_bcsym_left_table_row_step /\ ((((exists bcf_height_bcsym_left_table_row_step_previous_left. bcf_height_bcsym_left_table_row_step_previous_left + S (bcf_left_bcsym_left_table_row_step) = S ((S (bcf_predecessor_bcsym_left_table_row_step)) * bcf_previous_scale_bcsym_left_table)) /\ exists bcf_quotient_bcsym_left_table_row_step_previous_left. bcf_previous_code_bcsym_left_table = bcf_quotient_bcsym_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcsym_left_table_row_step)) * bcf_previous_scale_bcsym_left_table) + (bcf_left_bcsym_left_table_row_step))) /\ ((((exists bcf_height_bcsym_left_table_row_step_previous_right. bcf_height_bcsym_left_table_row_step_previous_right + S (bcf_right_bcsym_left_table_row_step) = S ((S (S (bcf_predecessor_bcsym_left_table_row_step))) * bcf_previous_scale_bcsym_left_table)) /\ exists bcf_quotient_bcsym_left_table_row_step_previous_right. bcf_previous_code_bcsym_left_table = bcf_quotient_bcsym_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcsym_left_table_row_step))) * bcf_previous_scale_bcsym_left_table) + (bcf_right_bcsym_left_table_row_step))) /\ bcf_value_bcsym_left_table_row_step = bcf_left_bcsym_left_table_row_step + bcf_right_bcsym_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcsym_left_decoded_row_code. bcf_height_bcsym_left_decoded_row_code + S (bcf_row_code_bcsym_left) = S ((S (n)) * bcf_row_code_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_decoded_row_code. bcf_row_code_code_bcsym_left = bcf_quotient_bcsym_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcsym_left) + (bcf_row_code_bcsym_left))) /\ ((((exists bcf_height_bcsym_left_decoded_row_scale. bcf_height_bcsym_left_decoded_row_scale + S (bcf_row_scale_bcsym_left) = S ((S (n)) * bcf_row_scale_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_decoded_row_scale. bcf_row_scale_code_bcsym_left = bcf_quotient_bcsym_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcsym_left) + (bcf_row_scale_bcsym_left))) /\ (((exists bcf_height_bcsym_left_decoded_value. bcf_height_bcsym_left_decoded_value + S (x) = S ((S (k)) * bcf_row_scale_bcsym_left)) /\ exists bcf_quotient_bcsym_left_decoded_value. bcf_row_code_bcsym_left = bcf_quotient_bcsym_left_decoded_value * S ((S (k)) * bcf_row_scale_bcsym_left) + (x))))))))) -> (((exists bcf_lt_gap_bcsym_right_out_of_range. bcf_lt_gap_bcsym_right_out_of_range + S (n) = j) /\ y = 0) \/ ((exists bcf_le_gap_bcsym_right_in_range. bcf_le_gap_bcsym_right_in_range + (j) = n) /\ (exists bcf_row_code_code_bcsym_right bcf_row_code_scale_bcsym_right bcf_row_scale_code_bcsym_right bcf_row_scale_scale_bcsym_right bcf_row_code_bcsym_right bcf_row_scale_bcsym_right. ((forall bcf_row_index_bcsym_right_table. (exists bcf_lt_gap_bcsym_right_table_row_bound. bcf_lt_gap_bcsym_right_table_row_bound + S (bcf_row_index_bcsym_right_table) = S (n)) -> exists bcf_row_code_bcsym_right_table bcf_row_scale_bcsym_right_table. ((((exists bcf_height_bcsym_right_table_decoded_row_code. bcf_height_bcsym_right_table_decoded_row_code + S (bcf_row_code_bcsym_right_table) = S ((S (bcf_row_index_bcsym_right_table)) * bcf_row_code_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_table_decoded_row_code. bcf_row_code_code_bcsym_right = bcf_quotient_bcsym_right_table_decoded_row_code * S ((S (bcf_row_index_bcsym_right_table)) * bcf_row_code_scale_bcsym_right) + (bcf_row_code_bcsym_right_table))) /\ ((((exists bcf_height_bcsym_right_table_decoded_row_scale. bcf_height_bcsym_right_table_decoded_row_scale + S (bcf_row_scale_bcsym_right_table) = S ((S (bcf_row_index_bcsym_right_table)) * bcf_row_scale_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_table_decoded_row_scale. bcf_row_scale_code_bcsym_right = bcf_quotient_bcsym_right_table_decoded_row_scale * S ((S (bcf_row_index_bcsym_right_table)) * bcf_row_scale_scale_bcsym_right) + (bcf_row_scale_bcsym_right_table))) /\ ((bcf_row_index_bcsym_right_table = 0 /\ (forall bcf_index_bcsym_right_table_zero_row. (exists bcf_lt_gap_bcsym_right_table_zero_row_bound. bcf_lt_gap_bcsym_right_table_zero_row_bound + S (bcf_index_bcsym_right_table_zero_row) = S (n)) -> exists bcf_value_bcsym_right_table_zero_row. ((((exists bcf_height_bcsym_right_table_zero_row_entry. bcf_height_bcsym_right_table_zero_row_entry + S (bcf_value_bcsym_right_table_zero_row) = S ((S (bcf_index_bcsym_right_table_zero_row)) * bcf_row_scale_bcsym_right_table)) /\ exists bcf_quotient_bcsym_right_table_zero_row_entry. bcf_row_code_bcsym_right_table = bcf_quotient_bcsym_right_table_zero_row_entry * S ((S (bcf_index_bcsym_right_table_zero_row)) * bcf_row_scale_bcsym_right_table) + (bcf_value_bcsym_right_table_zero_row))) /\ ((bcf_index_bcsym_right_table_zero_row = 0 /\ bcf_value_bcsym_right_table_zero_row = 1) \/ exists bcf_predecessor_bcsym_right_table_zero_row. bcf_index_bcsym_right_table_zero_row = S bcf_predecessor_bcsym_right_table_zero_row /\ bcf_value_bcsym_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcsym_right_table bcf_previous_code_bcsym_right_table bcf_previous_scale_bcsym_right_table. bcf_row_index_bcsym_right_table = S bcf_predecessor_bcsym_right_table /\ ((((exists bcf_height_bcsym_right_table_decoded_previous_code. bcf_height_bcsym_right_table_decoded_previous_code + S (bcf_previous_code_bcsym_right_table) = S ((S (bcf_predecessor_bcsym_right_table)) * bcf_row_code_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_table_decoded_previous_code. bcf_row_code_code_bcsym_right = bcf_quotient_bcsym_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcsym_right_table)) * bcf_row_code_scale_bcsym_right) + (bcf_previous_code_bcsym_right_table))) /\ ((((exists bcf_height_bcsym_right_table_decoded_previous_scale. bcf_height_bcsym_right_table_decoded_previous_scale + S (bcf_previous_scale_bcsym_right_table) = S ((S (bcf_predecessor_bcsym_right_table)) * bcf_row_scale_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_table_decoded_previous_scale. bcf_row_scale_code_bcsym_right = bcf_quotient_bcsym_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcsym_right_table)) * bcf_row_scale_scale_bcsym_right) + (bcf_previous_scale_bcsym_right_table))) /\ (forall bcf_index_bcsym_right_table_row_step. (exists bcf_lt_gap_bcsym_right_table_row_step_bound. bcf_lt_gap_bcsym_right_table_row_step_bound + S (bcf_index_bcsym_right_table_row_step) = S (n)) -> exists bcf_value_bcsym_right_table_row_step. ((((exists bcf_height_bcsym_right_table_row_step_entry. bcf_height_bcsym_right_table_row_step_entry + S (bcf_value_bcsym_right_table_row_step) = S ((S (bcf_index_bcsym_right_table_row_step)) * bcf_row_scale_bcsym_right_table)) /\ exists bcf_quotient_bcsym_right_table_row_step_entry. bcf_row_code_bcsym_right_table = bcf_quotient_bcsym_right_table_row_step_entry * S ((S (bcf_index_bcsym_right_table_row_step)) * bcf_row_scale_bcsym_right_table) + (bcf_value_bcsym_right_table_row_step))) /\ ((bcf_index_bcsym_right_table_row_step = 0 /\ bcf_value_bcsym_right_table_row_step = 1) \/ exists bcf_predecessor_bcsym_right_table_row_step bcf_left_bcsym_right_table_row_step bcf_right_bcsym_right_table_row_step. bcf_index_bcsym_right_table_row_step = S bcf_predecessor_bcsym_right_table_row_step /\ ((((exists bcf_height_bcsym_right_table_row_step_previous_left. bcf_height_bcsym_right_table_row_step_previous_left + S (bcf_left_bcsym_right_table_row_step) = S ((S (bcf_predecessor_bcsym_right_table_row_step)) * bcf_previous_scale_bcsym_right_table)) /\ exists bcf_quotient_bcsym_right_table_row_step_previous_left. bcf_previous_code_bcsym_right_table = bcf_quotient_bcsym_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcsym_right_table_row_step)) * bcf_previous_scale_bcsym_right_table) + (bcf_left_bcsym_right_table_row_step))) /\ ((((exists bcf_height_bcsym_right_table_row_step_previous_right. bcf_height_bcsym_right_table_row_step_previous_right + S (bcf_right_bcsym_right_table_row_step) = S ((S (S (bcf_predecessor_bcsym_right_table_row_step))) * bcf_previous_scale_bcsym_right_table)) /\ exists bcf_quotient_bcsym_right_table_row_step_previous_right. bcf_previous_code_bcsym_right_table = bcf_quotient_bcsym_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcsym_right_table_row_step))) * bcf_previous_scale_bcsym_right_table) + (bcf_right_bcsym_right_table_row_step))) /\ bcf_value_bcsym_right_table_row_step = bcf_left_bcsym_right_table_row_step + bcf_right_bcsym_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcsym_right_decoded_row_code. bcf_height_bcsym_right_decoded_row_code + S (bcf_row_code_bcsym_right) = S ((S (n)) * bcf_row_code_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_decoded_row_code. bcf_row_code_code_bcsym_right = bcf_quotient_bcsym_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcsym_right) + (bcf_row_code_bcsym_right))) /\ ((((exists bcf_height_bcsym_right_decoded_row_scale. bcf_height_bcsym_right_decoded_row_scale + S (bcf_row_scale_bcsym_right) = S ((S (n)) * bcf_row_scale_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_decoded_row_scale. bcf_row_scale_code_bcsym_right = bcf_quotient_bcsym_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcsym_right) + (bcf_row_scale_bcsym_right))) /\ (((exists bcf_height_bcsym_right_decoded_value. bcf_height_bcsym_right_decoded_value + S (y) = S ((S (j)) * bcf_row_scale_bcsym_right)) /\ exists bcf_quotient_bcsym_right_decoded_value. bcf_row_code_bcsym_right = bcf_quotient_bcsym_right_decoded_value * S ((S (j)) * bcf_row_scale_bcsym_right) + (y))))))))) -> x = y

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT0001 add_succ_left BT0002 add_comm BT00T8 choose_exists BT00TE choose_zero BT00TK choose_self_of_eq BT00TJ choose_succ_succ

Direct theorem dependents

BT00TS central_binom_succ_double_middle

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

178 script commands · 41 reading checkpoints · 18 local claims

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

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

Named ingredients (7)
zero addadd succ leftadd commchoose existschoose zerochoose self of eqchoose succ succ
01Induction on nL1–1

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

  1. L1
    induction n
02Induction on kL2–2

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

  1. L2
    induction k
03Induction on jL3–8

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

  1. L3
    induction j
  2. L4
    intro x
  3. L5
    intro y
  4. L6
    intro hsum
  5. L7
    intro hleft
  6. L8
    intro hright
04Establish hxL9–13

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

  1. L9
    have hx : x = 1
  2. L10
    specialize choose_zero 0
  3. L11
    specialize choose_zero x
  4. L12
    apply choose_zero
  5. L13
    exact hleft
05Establish hyL14–23

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

  1. L14
    have hy : y = 1
  2. L15
    specialize choose_zero 0
  3. L16
    specialize choose_zero y
  4. L17
    apply choose_zero
  5. L18
    exact hright
  6. L19
    trans 1
  7. L20
    exact hx
  8. L21
    symm
  9. L22
    exact hy
  10. L23
    intro x
06Fix variables and assumptionsL24–27

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

  1. L24
    intro y
  2. L25
    intro hsum
  3. L26
    intro hleft
  4. L27
    intro hright
07Use earlier factsL28–28

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

  1. L28
    specialize zero_add (S j)
08Calculate and transport equalitiesL29–29

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

  1. L29
    rewrite zero_add at hsum
09Separate the logical casesL30–30

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

  1. L30
    exfalso
10Use earlier factsL31–32

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

  1. L31
    apply PA1
  2. L32
    exact hsum
11Fix variables and assumptionsL33–38

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

  1. L33
    intro j
  2. L34
    intro x
  3. L35
    intro y
  4. L36
    intro hsum
  5. L37
    intro hleft
  6. L38
    intro hright
12Use earlier factsL39–40

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

  1. L39
    specialize add_succ_left k
  2. L40
    specialize add_succ_left j
13Calculate and transport equalitiesL41–41

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

  1. L41
    rewrite add_succ_left at hsum
14Separate the logical casesL42–42

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

  1. L42
    exfalso
15Use earlier factsL43–44

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

  1. L43
    apply PA1
  2. L44
    exact hsum
16Induction on kL45–51

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

  1. L45
    induction k
  2. L46
    intro j
  3. L47
    intro x
  4. L48
    intro y
  5. L49
    intro hsum
  6. L50
    intro hleft
  7. L51
    intro hright
17Establish hxL52–56

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

  1. L52
    have hx : x = 1
  2. L53
    specialize choose_zero (S n)
  3. L54
    specialize choose_zero x
  4. L55
    apply choose_zero
  5. L56
    exact hleft
18Establish hjL57–61

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

  1. L57
    have hj : j = S n
  2. L58
    trans 0 + j
  3. L59
    symm
  4. L60
    apply zero_add
  5. L61
    exact hsum
19Establish hyL62–71

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

  1. L62
    have hy : y = 1
  2. L63
    specialize choose_self_of_eq (S n)
  3. L64
    specialize choose_self_of_eq j
  4. L65
    specialize choose_self_of_eq y
  5. L66
    apply choose_self_of_eq
  6. L67
    exact hj
  7. L68
    exact hright
  8. L69
    trans 1
  9. L70
    exact hx
  10. L71
    symm
20Use earlier factsL72–72

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

  1. L72
    exact hy
21Induction on jL73–78

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

  1. L73
    induction j
  2. L74
    intro x
  3. L75
    intro y
  4. L76
    intro hsum
  5. L77
    intro hleft
  6. L78
    intro hright
22Establish hkL79–81

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

  1. L79
    have hk : S k = S n
  2. L80
    rewrite PA3 at hsum
  3. L81
    exact hsum
23Establish hxL82–88

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

  1. L82
    have hx : x = 1
  2. L83
    specialize choose_self_of_eq (S n)
  3. L84
    specialize choose_self_of_eq (S k)
  4. L85
    specialize choose_self_of_eq x
  5. L86
    apply choose_self_of_eq
  6. L87
    exact hk
  7. L88
    exact hleft
24Establish hyL89–98

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

  1. L89
    have hy : y = 1
  2. L90
    specialize choose_zero (S n)
  3. L91
    specialize choose_zero y
  4. L92
    apply choose_zero
  5. L93
    exact hright
  6. L94
    trans 1
  7. L95
    exact hx
  8. L96
    symm
  9. L97
    exact hy
  10. L98
    intro x
25Fix variables and assumptionsL99–102

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

  1. L99
    intro y
  2. L100
    intro hsum
  3. L101
    intro hleft
  4. L102
    intro hright
26Establish ha_existsL103–106

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

  1. L103
    have ha_exists : ∃ a. Choose(n,k,a)Definitions: Choose(n,k,a)Original native command in the exact edition
  2. L104
    specialize choose_exists n
  3. L105
    specialize choose_exists k
  4. L106
    exact choose_exists
27Separate the logical casesL107–107

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

  1. L107
    cases ha_exists
28Establish hb_existsL108–111

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

  1. L108
    have hb_exists : ∃ b. Choose(n,S k,b)Definitions: Choose(n,S k,b)Original native command in the exact edition
  2. L109
    specialize choose_exists n
  3. L110
    specialize choose_exists (S k)
  4. L111
    exact choose_exists
29Separate the logical casesL112–112

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

  1. L112
    cases hb_exists
30Establish hc_existsL113–116

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

  1. L113
    have hc_exists : ∃ c. Choose(n,j,c)Definitions: Choose(n,j,c)Original native command in the exact edition
  2. L114
    specialize choose_exists n
  3. L115
    specialize choose_exists j
  4. L116
    exact choose_exists
31Separate the logical casesL117–117

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

  1. L117
    cases hc_exists
32Establish hd_existsL118–121

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

  1. L118
    have hd_exists : ∃ d. Choose(n,S j,d)Definitions: Choose(n,S j,d)Original native command in the exact edition
  2. L119
    specialize choose_exists n
  3. L120
    specialize choose_exists (S j)
  4. L121
    exact choose_exists
33Separate the logical casesL122–122

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

  1. L122
    cases hd_exists
34Establish hleft_complementL123–128

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

  1. L123
    have hleft_complement : S k + j = n
  2. L124
    apply PA2
  3. L125
    trans S k + S j
  4. L126
    symm
  5. L127
    apply PA4
  6. L128
    exact hsum
35Establish hright_complementL129–135

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

  1. L129
    have hright_complement : k + S j = n
  2. L130
    trans S (k + j)
  3. L131
    apply PA4
  4. L132
    trans S k + j
  5. L133
    symm
  6. L134
    apply add_succ_left
  7. L135
    exact hleft_complement
36Establish hx_sumL136–145

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

  1. L136
    have hx_sum : x = x1 + x2
  2. L137
    specialize choose_succ_succ n
  3. L138
    specialize choose_succ_succ k
  4. L139
    specialize choose_succ_succ x1
  5. L140
    specialize choose_succ_succ x2
  6. L141
    specialize choose_succ_succ x
  7. L142
    apply choose_succ_succ
  8. L143
    exact ha_exists_witness
  9. L144
    exact hb_exists_witness
  10. L145
    exact hleft
37Establish hy_sumL146–155

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

  1. L146
    have hy_sum : y = x3 + x4
  2. L147
    specialize choose_succ_succ n
  3. L148
    specialize choose_succ_succ j
  4. L149
    specialize choose_succ_succ x3
  5. L150
    specialize choose_succ_succ x4
  6. L151
    specialize choose_succ_succ y
  7. L152
    apply choose_succ_succ
  8. L153
    exact hc_exists_witness
  9. L154
    exact hd_exists_witness
  10. L155
    exact hright
38Establish hfirstL156–164

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

  1. L156
    have hfirst : x1 = x4
  2. L157
    specialize IH k
  3. L158
    specialize IH (S j)
  4. L159
    specialize IH x1
  5. L160
    specialize IH x4
  6. L161
    apply IH
  7. L162
    exact hright_complement
  8. L163
    exact ha_exists_witness
  9. L164
    exact hd_exists_witness
39Establish hsecondL165–174

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

  1. L165
    have hsecond : x2 = x3
  2. L166
    specialize IH (S k)
  3. L167
    specialize IH j
  4. L168
    specialize IH x2
  5. L169
    specialize IH x3
  6. L170
    apply IH
  7. L171
    exact hleft_complement
  8. L172
    exact hb_exists_witness
  9. L173
    exact hc_exists_witness
  10. L174
    rewrite hx_sum
40Calculate and transport equalitiesL175–177

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

  1. L175
    rewrite hy_sum
  2. L176
    rewrite hfirst
  3. L177
    rewrite hsecond
41Use earlier factsL178–178

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

  1. L178
    apply add_comm

Library-wide reading audit

Original defined command ledger · 178 lines
  1. 0001induction n
  2. 0002induction k
  3. 0003induction j
  4. 0004intro x
  5. 0005intro y
  6. 0006intro hsum
  7. 0007intro hleft
  8. 0008intro hright
  9. 0009have hx : x = 1
  10. 0010specialize choose_zero 0
  11. 0011specialize choose_zero x
  12. 0012apply choose_zero
  13. 0013exact hleft
  14. 0014have hy : y = 1
  15. 0015specialize choose_zero 0
  16. 0016specialize choose_zero y
  17. 0017apply choose_zero
  18. 0018exact hright
  19. 0019trans 1
  20. 0020exact hx
  21. 0021symm
  22. 0022exact hy
  23. 0023intro x
  24. 0024intro y
  25. 0025intro hsum
  26. 0026intro hleft
  27. 0027intro hright
  28. 0028specialize zero_add (S j)
  29. 0029rewrite zero_add at hsum
  30. 0030exfalso
  31. 0031apply PA1
  32. 0032exact hsum
  33. 0033intro j
  34. 0034intro x
  35. 0035intro y
  36. 0036intro hsum
  37. 0037intro hleft
  38. 0038intro hright
  39. 0039specialize add_succ_left k
  40. 0040specialize add_succ_left j
  41. 0041rewrite add_succ_left at hsum
  42. 0042exfalso
  43. 0043apply PA1
  44. 0044exact hsum
  45. 0045induction k
  46. 0046intro j
  47. 0047intro x
  48. 0048intro y
  49. 0049intro hsum
  50. 0050intro hleft
  51. 0051intro hright
  52. 0052have hx : x = 1
  53. 0053specialize choose_zero (S n)
  54. 0054specialize choose_zero x
  55. 0055apply choose_zero
  56. 0056exact hleft
  57. 0057have hj : j = S n
  58. 0058trans 0 + j
  59. 0059symm
  60. 0060apply zero_add
  61. 0061exact hsum
  62. 0062have hy : y = 1
  63. 0063specialize choose_self_of_eq (S n)
  64. 0064specialize choose_self_of_eq j
  65. 0065specialize choose_self_of_eq y
  66. 0066apply choose_self_of_eq
  67. 0067exact hj
  68. 0068exact hright
  69. 0069trans 1
  70. 0070exact hx
  71. 0071symm
  72. 0072exact hy
  73. 0073induction j
  74. 0074intro x
  75. 0075intro y
  76. 0076intro hsum
  77. 0077intro hleft
  78. 0078intro hright
  79. 0079have hk : S k = S n
  80. 0080rewrite PA3 at hsum
  81. 0081exact hsum
  82. 0082have hx : x = 1
  83. 0083specialize choose_self_of_eq (S n)
  84. 0084specialize choose_self_of_eq (S k)
  85. 0085specialize choose_self_of_eq x
  86. 0086apply choose_self_of_eq
  87. 0087exact hk
  88. 0088exact hleft
  89. 0089have hy : y = 1
  90. 0090specialize choose_zero (S n)
  91. 0091specialize choose_zero y
  92. 0092apply choose_zero
  93. 0093exact hright
  94. 0094trans 1
  95. 0095exact hx
  96. 0096symm
  97. 0097exact hy
  98. 0098intro x
  99. 0099intro y
  100. 0100intro hsum
  101. 0101intro hleft
  102. 0102intro hright
  103. 0103have ha_exists : ∃ a. Choose(n,k,a)
    Exact native replay linehave ha_exists : exists a. (((exists bcf_lt_gap_bcs_previous_left_out_of_range. bcf_lt_gap_bcs_previous_left_out_of_range + S (n) = k) /\ a = 0) \/ ((exists bcf_le_gap_bcs_previous_left_in_range. bcf_le_gap_bcs_previous_left_in_range + (k) = n) /\ (exists bcf_row_code_code_bcs_previous_left bcf_row_code_scale_bcs_previous_left bcf_row_scale_code_bcs_previous_left bcf_row_scale_scale_bcs_previous_left bcf_row_code_bcs_previous_left bcf_row_scale_bcs_previous_left. ((forall bcf_row_index_bcs_previous_left_table. (exists bcf_lt_gap_bcs_previous_left_table_row_bound. bcf_lt_gap_bcs_previous_left_table_row_bound + S (bcf_row_index_bcs_previous_left_table) = S (n)) -> exists bcf_row_code_bcs_previous_left_table bcf_row_scale_bcs_previous_left_table. ((((exists bcf_height_bcs_previous_left_table_decoded_row_code. bcf_height_bcs_previous_left_table_decoded_row_code + S (bcf_row_code_bcs_previous_left_table) = S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_row_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_row_code * S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left) + (bcf_row_code_bcs_previous_left_table))) /\ ((((exists bcf_height_bcs_previous_left_table_decoded_row_scale. bcf_height_bcs_previous_left_table_decoded_row_scale + S (bcf_row_scale_bcs_previous_left_table) = S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_row_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_row_scale * S ((S (bcf_row_index_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_row_scale_bcs_previous_left_table))) /\ ((bcf_row_index_bcs_previous_left_table = 0 /\ (forall bcf_index_bcs_previous_left_table_zero_row. (exists bcf_lt_gap_bcs_previous_left_table_zero_row_bound. bcf_lt_gap_bcs_previous_left_table_zero_row_bound + S (bcf_index_bcs_previous_left_table_zero_row) = S (n)) -> exists bcf_value_bcs_previous_left_table_zero_row. ((((exists bcf_height_bcs_previous_left_table_zero_row_entry. bcf_height_bcs_previous_left_table_zero_row_entry + S (bcf_value_bcs_previous_left_table_zero_row) = S ((S (bcf_index_bcs_previous_left_table_zero_row)) * bcf_row_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_zero_row_entry. bcf_row_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_zero_row_entry * S ((S (bcf_index_bcs_previous_left_table_zero_row)) * bcf_row_scale_bcs_previous_left_table) + (bcf_value_bcs_previous_left_table_zero_row))) /\ ((bcf_index_bcs_previous_left_table_zero_row = 0 /\ bcf_value_bcs_previous_left_table_zero_row = 1) \/ exists bcf_predecessor_bcs_previous_left_table_zero_row. bcf_index_bcs_previous_left_table_zero_row = S bcf_predecessor_bcs_previous_left_table_zero_row /\ bcf_value_bcs_previous_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_previous_left_table bcf_previous_code_bcs_previous_left_table bcf_previous_scale_bcs_previous_left_table. bcf_row_index_bcs_previous_left_table = S bcf_predecessor_bcs_previous_left_table /\ ((((exists bcf_height_bcs_previous_left_table_decoded_previous_code. bcf_height_bcs_previous_left_table_decoded_previous_code + S (bcf_previous_code_bcs_previous_left_table) = S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_previous_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_code_scale_bcs_previous_left) + (bcf_previous_code_bcs_previous_left_table))) /\ ((((exists bcf_height_bcs_previous_left_table_decoded_previous_scale. bcf_height_bcs_previous_left_table_decoded_previous_scale + S (bcf_previous_scale_bcs_previous_left_table) = S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_table_decoded_previous_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_previous_left_table)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_previous_scale_bcs_previous_left_table))) /\ (forall bcf_index_bcs_previous_left_table_row_step. (exists bcf_lt_gap_bcs_previous_left_table_row_step_bound. bcf_lt_gap_bcs_previous_left_table_row_step_bound + S (bcf_index_bcs_previous_left_table_row_step) = S (n)) -> exists bcf_value_bcs_previous_left_table_row_step. ((((exists bcf_height_bcs_previous_left_table_row_step_entry. bcf_height_bcs_previous_left_table_row_step_entry + S (bcf_value_bcs_previous_left_table_row_step) = S ((S (bcf_index_bcs_previous_left_table_row_step)) * bcf_row_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_entry. bcf_row_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_entry * S ((S (bcf_index_bcs_previous_left_table_row_step)) * bcf_row_scale_bcs_previous_left_table) + (bcf_value_bcs_previous_left_table_row_step))) /\ ((bcf_index_bcs_previous_left_table_row_step = 0 /\ bcf_value_bcs_previous_left_table_row_step = 1) \/ exists bcf_predecessor_bcs_previous_left_table_row_step bcf_left_bcs_previous_left_table_row_step bcf_right_bcs_previous_left_table_row_step. bcf_index_bcs_previous_left_table_row_step = S bcf_predecessor_bcs_previous_left_table_row_step /\ ((((exists bcf_height_bcs_previous_left_table_row_step_previous_left. bcf_height_bcs_previous_left_table_row_step_previous_left + S (bcf_left_bcs_previous_left_table_row_step) = S ((S (bcf_predecessor_bcs_previous_left_table_row_step)) * bcf_previous_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_previous_left. bcf_previous_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_previous_left_table_row_step)) * bcf_previous_scale_bcs_previous_left_table) + (bcf_left_bcs_previous_left_table_row_step))) /\ ((((exists bcf_height_bcs_previous_left_table_row_step_previous_right. bcf_height_bcs_previous_left_table_row_step_previous_right + S (bcf_right_bcs_previous_left_table_row_step) = S ((S (S (bcf_predecessor_bcs_previous_left_table_row_step))) * bcf_previous_scale_bcs_previous_left_table)) /\ exists bcf_quotient_bcs_previous_left_table_row_step_previous_right. bcf_previous_code_bcs_previous_left_table = bcf_quotient_bcs_previous_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_previous_left_table_row_step))) * bcf_previous_scale_bcs_previous_left_table) + (bcf_right_bcs_previous_left_table_row_step))) /\ bcf_value_bcs_previous_left_table_row_step = bcf_left_bcs_previous_left_table_row_step + bcf_right_bcs_previous_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_previous_left_decoded_row_code. bcf_height_bcs_previous_left_decoded_row_code + S (bcf_row_code_bcs_previous_left) = S ((S (n)) * bcf_row_code_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_row_code. bcf_row_code_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_previous_left) + (bcf_row_code_bcs_previous_left))) /\ ((((exists bcf_height_bcs_previous_left_decoded_row_scale. bcf_height_bcs_previous_left_decoded_row_scale + S (bcf_row_scale_bcs_previous_left) = S ((S (n)) * bcf_row_scale_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_row_scale. bcf_row_scale_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_previous_left) + (bcf_row_scale_bcs_previous_left))) /\ (((exists bcf_height_bcs_previous_left_decoded_value. bcf_height_bcs_previous_left_decoded_value + S (a) = S ((S (k)) * bcf_row_scale_bcs_previous_left)) /\ exists bcf_quotient_bcs_previous_left_decoded_value. bcf_row_code_bcs_previous_left = bcf_quotient_bcs_previous_left_decoded_value * S ((S (k)) * bcf_row_scale_bcs_previous_left) + (a)))))))))
  104. 0104specialize choose_exists n
  105. 0105specialize choose_exists k
  106. 0106exact choose_exists
  107. 0107cases ha_exists
  108. 0108have hb_exists : ∃ b. Choose(n,S k,b)
    Exact native replay linehave hb_exists : exists b. (((exists bcf_lt_gap_bcs_current_left_out_of_range. bcf_lt_gap_bcs_current_left_out_of_range + S (n) = S k) /\ b = 0) \/ ((exists bcf_le_gap_bcs_current_left_in_range. bcf_le_gap_bcs_current_left_in_range + (S k) = n) /\ (exists bcf_row_code_code_bcs_current_left bcf_row_code_scale_bcs_current_left bcf_row_scale_code_bcs_current_left bcf_row_scale_scale_bcs_current_left bcf_row_code_bcs_current_left bcf_row_scale_bcs_current_left. ((forall bcf_row_index_bcs_current_left_table. (exists bcf_lt_gap_bcs_current_left_table_row_bound. bcf_lt_gap_bcs_current_left_table_row_bound + S (bcf_row_index_bcs_current_left_table) = S (n)) -> exists bcf_row_code_bcs_current_left_table bcf_row_scale_bcs_current_left_table. ((((exists bcf_height_bcs_current_left_table_decoded_row_code. bcf_height_bcs_current_left_table_decoded_row_code + S (bcf_row_code_bcs_current_left_table) = S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_row_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_row_code * S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left) + (bcf_row_code_bcs_current_left_table))) /\ ((((exists bcf_height_bcs_current_left_table_decoded_row_scale. bcf_height_bcs_current_left_table_decoded_row_scale + S (bcf_row_scale_bcs_current_left_table) = S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_row_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_row_scale * S ((S (bcf_row_index_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left) + (bcf_row_scale_bcs_current_left_table))) /\ ((bcf_row_index_bcs_current_left_table = 0 /\ (forall bcf_index_bcs_current_left_table_zero_row. (exists bcf_lt_gap_bcs_current_left_table_zero_row_bound. bcf_lt_gap_bcs_current_left_table_zero_row_bound + S (bcf_index_bcs_current_left_table_zero_row) = S (n)) -> exists bcf_value_bcs_current_left_table_zero_row. ((((exists bcf_height_bcs_current_left_table_zero_row_entry. bcf_height_bcs_current_left_table_zero_row_entry + S (bcf_value_bcs_current_left_table_zero_row) = S ((S (bcf_index_bcs_current_left_table_zero_row)) * bcf_row_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_zero_row_entry. bcf_row_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_zero_row_entry * S ((S (bcf_index_bcs_current_left_table_zero_row)) * bcf_row_scale_bcs_current_left_table) + (bcf_value_bcs_current_left_table_zero_row))) /\ ((bcf_index_bcs_current_left_table_zero_row = 0 /\ bcf_value_bcs_current_left_table_zero_row = 1) \/ exists bcf_predecessor_bcs_current_left_table_zero_row. bcf_index_bcs_current_left_table_zero_row = S bcf_predecessor_bcs_current_left_table_zero_row /\ bcf_value_bcs_current_left_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_current_left_table bcf_previous_code_bcs_current_left_table bcf_previous_scale_bcs_current_left_table. bcf_row_index_bcs_current_left_table = S bcf_predecessor_bcs_current_left_table /\ ((((exists bcf_height_bcs_current_left_table_decoded_previous_code. bcf_height_bcs_current_left_table_decoded_previous_code + S (bcf_previous_code_bcs_current_left_table) = S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_previous_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_code_scale_bcs_current_left) + (bcf_previous_code_bcs_current_left_table))) /\ ((((exists bcf_height_bcs_current_left_table_decoded_previous_scale. bcf_height_bcs_current_left_table_decoded_previous_scale + S (bcf_previous_scale_bcs_current_left_table) = S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_table_decoded_previous_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_current_left_table)) * bcf_row_scale_scale_bcs_current_left) + (bcf_previous_scale_bcs_current_left_table))) /\ (forall bcf_index_bcs_current_left_table_row_step. (exists bcf_lt_gap_bcs_current_left_table_row_step_bound. bcf_lt_gap_bcs_current_left_table_row_step_bound + S (bcf_index_bcs_current_left_table_row_step) = S (n)) -> exists bcf_value_bcs_current_left_table_row_step. ((((exists bcf_height_bcs_current_left_table_row_step_entry. bcf_height_bcs_current_left_table_row_step_entry + S (bcf_value_bcs_current_left_table_row_step) = S ((S (bcf_index_bcs_current_left_table_row_step)) * bcf_row_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_entry. bcf_row_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_entry * S ((S (bcf_index_bcs_current_left_table_row_step)) * bcf_row_scale_bcs_current_left_table) + (bcf_value_bcs_current_left_table_row_step))) /\ ((bcf_index_bcs_current_left_table_row_step = 0 /\ bcf_value_bcs_current_left_table_row_step = 1) \/ exists bcf_predecessor_bcs_current_left_table_row_step bcf_left_bcs_current_left_table_row_step bcf_right_bcs_current_left_table_row_step. bcf_index_bcs_current_left_table_row_step = S bcf_predecessor_bcs_current_left_table_row_step /\ ((((exists bcf_height_bcs_current_left_table_row_step_previous_left. bcf_height_bcs_current_left_table_row_step_previous_left + S (bcf_left_bcs_current_left_table_row_step) = S ((S (bcf_predecessor_bcs_current_left_table_row_step)) * bcf_previous_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_previous_left. bcf_previous_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_current_left_table_row_step)) * bcf_previous_scale_bcs_current_left_table) + (bcf_left_bcs_current_left_table_row_step))) /\ ((((exists bcf_height_bcs_current_left_table_row_step_previous_right. bcf_height_bcs_current_left_table_row_step_previous_right + S (bcf_right_bcs_current_left_table_row_step) = S ((S (S (bcf_predecessor_bcs_current_left_table_row_step))) * bcf_previous_scale_bcs_current_left_table)) /\ exists bcf_quotient_bcs_current_left_table_row_step_previous_right. bcf_previous_code_bcs_current_left_table = bcf_quotient_bcs_current_left_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_current_left_table_row_step))) * bcf_previous_scale_bcs_current_left_table) + (bcf_right_bcs_current_left_table_row_step))) /\ bcf_value_bcs_current_left_table_row_step = bcf_left_bcs_current_left_table_row_step + bcf_right_bcs_current_left_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_current_left_decoded_row_code. bcf_height_bcs_current_left_decoded_row_code + S (bcf_row_code_bcs_current_left) = S ((S (n)) * bcf_row_code_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_row_code. bcf_row_code_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_current_left) + (bcf_row_code_bcs_current_left))) /\ ((((exists bcf_height_bcs_current_left_decoded_row_scale. bcf_height_bcs_current_left_decoded_row_scale + S (bcf_row_scale_bcs_current_left) = S ((S (n)) * bcf_row_scale_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_row_scale. bcf_row_scale_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_current_left) + (bcf_row_scale_bcs_current_left))) /\ (((exists bcf_height_bcs_current_left_decoded_value. bcf_height_bcs_current_left_decoded_value + S (b) = S ((S (S k)) * bcf_row_scale_bcs_current_left)) /\ exists bcf_quotient_bcs_current_left_decoded_value. bcf_row_code_bcs_current_left = bcf_quotient_bcs_current_left_decoded_value * S ((S (S k)) * bcf_row_scale_bcs_current_left) + (b)))))))))
  109. 0109specialize choose_exists n
  110. 0110specialize choose_exists (S k)
  111. 0111exact choose_exists
  112. 0112cases hb_exists
  113. 0113have hc_exists : ∃ c. Choose(n,j,c)
    Exact native replay linehave hc_exists : exists c. (((exists bcf_lt_gap_bcs_previous_right_out_of_range. bcf_lt_gap_bcs_previous_right_out_of_range + S (n) = j) /\ c = 0) \/ ((exists bcf_le_gap_bcs_previous_right_in_range. bcf_le_gap_bcs_previous_right_in_range + (j) = n) /\ (exists bcf_row_code_code_bcs_previous_right bcf_row_code_scale_bcs_previous_right bcf_row_scale_code_bcs_previous_right bcf_row_scale_scale_bcs_previous_right bcf_row_code_bcs_previous_right bcf_row_scale_bcs_previous_right. ((forall bcf_row_index_bcs_previous_right_table. (exists bcf_lt_gap_bcs_previous_right_table_row_bound. bcf_lt_gap_bcs_previous_right_table_row_bound + S (bcf_row_index_bcs_previous_right_table) = S (n)) -> exists bcf_row_code_bcs_previous_right_table bcf_row_scale_bcs_previous_right_table. ((((exists bcf_height_bcs_previous_right_table_decoded_row_code. bcf_height_bcs_previous_right_table_decoded_row_code + S (bcf_row_code_bcs_previous_right_table) = S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_row_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_row_code * S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right) + (bcf_row_code_bcs_previous_right_table))) /\ ((((exists bcf_height_bcs_previous_right_table_decoded_row_scale. bcf_height_bcs_previous_right_table_decoded_row_scale + S (bcf_row_scale_bcs_previous_right_table) = S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_row_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_row_scale * S ((S (bcf_row_index_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_row_scale_bcs_previous_right_table))) /\ ((bcf_row_index_bcs_previous_right_table = 0 /\ (forall bcf_index_bcs_previous_right_table_zero_row. (exists bcf_lt_gap_bcs_previous_right_table_zero_row_bound. bcf_lt_gap_bcs_previous_right_table_zero_row_bound + S (bcf_index_bcs_previous_right_table_zero_row) = S (n)) -> exists bcf_value_bcs_previous_right_table_zero_row. ((((exists bcf_height_bcs_previous_right_table_zero_row_entry. bcf_height_bcs_previous_right_table_zero_row_entry + S (bcf_value_bcs_previous_right_table_zero_row) = S ((S (bcf_index_bcs_previous_right_table_zero_row)) * bcf_row_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_zero_row_entry. bcf_row_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_zero_row_entry * S ((S (bcf_index_bcs_previous_right_table_zero_row)) * bcf_row_scale_bcs_previous_right_table) + (bcf_value_bcs_previous_right_table_zero_row))) /\ ((bcf_index_bcs_previous_right_table_zero_row = 0 /\ bcf_value_bcs_previous_right_table_zero_row = 1) \/ exists bcf_predecessor_bcs_previous_right_table_zero_row. bcf_index_bcs_previous_right_table_zero_row = S bcf_predecessor_bcs_previous_right_table_zero_row /\ bcf_value_bcs_previous_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_previous_right_table bcf_previous_code_bcs_previous_right_table bcf_previous_scale_bcs_previous_right_table. bcf_row_index_bcs_previous_right_table = S bcf_predecessor_bcs_previous_right_table /\ ((((exists bcf_height_bcs_previous_right_table_decoded_previous_code. bcf_height_bcs_previous_right_table_decoded_previous_code + S (bcf_previous_code_bcs_previous_right_table) = S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_previous_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_code_scale_bcs_previous_right) + (bcf_previous_code_bcs_previous_right_table))) /\ ((((exists bcf_height_bcs_previous_right_table_decoded_previous_scale. bcf_height_bcs_previous_right_table_decoded_previous_scale + S (bcf_previous_scale_bcs_previous_right_table) = S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_table_decoded_previous_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_previous_right_table)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_previous_scale_bcs_previous_right_table))) /\ (forall bcf_index_bcs_previous_right_table_row_step. (exists bcf_lt_gap_bcs_previous_right_table_row_step_bound. bcf_lt_gap_bcs_previous_right_table_row_step_bound + S (bcf_index_bcs_previous_right_table_row_step) = S (n)) -> exists bcf_value_bcs_previous_right_table_row_step. ((((exists bcf_height_bcs_previous_right_table_row_step_entry. bcf_height_bcs_previous_right_table_row_step_entry + S (bcf_value_bcs_previous_right_table_row_step) = S ((S (bcf_index_bcs_previous_right_table_row_step)) * bcf_row_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_entry. bcf_row_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_entry * S ((S (bcf_index_bcs_previous_right_table_row_step)) * bcf_row_scale_bcs_previous_right_table) + (bcf_value_bcs_previous_right_table_row_step))) /\ ((bcf_index_bcs_previous_right_table_row_step = 0 /\ bcf_value_bcs_previous_right_table_row_step = 1) \/ exists bcf_predecessor_bcs_previous_right_table_row_step bcf_left_bcs_previous_right_table_row_step bcf_right_bcs_previous_right_table_row_step. bcf_index_bcs_previous_right_table_row_step = S bcf_predecessor_bcs_previous_right_table_row_step /\ ((((exists bcf_height_bcs_previous_right_table_row_step_previous_left. bcf_height_bcs_previous_right_table_row_step_previous_left + S (bcf_left_bcs_previous_right_table_row_step) = S ((S (bcf_predecessor_bcs_previous_right_table_row_step)) * bcf_previous_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_previous_left. bcf_previous_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_previous_right_table_row_step)) * bcf_previous_scale_bcs_previous_right_table) + (bcf_left_bcs_previous_right_table_row_step))) /\ ((((exists bcf_height_bcs_previous_right_table_row_step_previous_right. bcf_height_bcs_previous_right_table_row_step_previous_right + S (bcf_right_bcs_previous_right_table_row_step) = S ((S (S (bcf_predecessor_bcs_previous_right_table_row_step))) * bcf_previous_scale_bcs_previous_right_table)) /\ exists bcf_quotient_bcs_previous_right_table_row_step_previous_right. bcf_previous_code_bcs_previous_right_table = bcf_quotient_bcs_previous_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_previous_right_table_row_step))) * bcf_previous_scale_bcs_previous_right_table) + (bcf_right_bcs_previous_right_table_row_step))) /\ bcf_value_bcs_previous_right_table_row_step = bcf_left_bcs_previous_right_table_row_step + bcf_right_bcs_previous_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_previous_right_decoded_row_code. bcf_height_bcs_previous_right_decoded_row_code + S (bcf_row_code_bcs_previous_right) = S ((S (n)) * bcf_row_code_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_row_code. bcf_row_code_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_previous_right) + (bcf_row_code_bcs_previous_right))) /\ ((((exists bcf_height_bcs_previous_right_decoded_row_scale. bcf_height_bcs_previous_right_decoded_row_scale + S (bcf_row_scale_bcs_previous_right) = S ((S (n)) * bcf_row_scale_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_row_scale. bcf_row_scale_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_previous_right) + (bcf_row_scale_bcs_previous_right))) /\ (((exists bcf_height_bcs_previous_right_decoded_value. bcf_height_bcs_previous_right_decoded_value + S (c) = S ((S (j)) * bcf_row_scale_bcs_previous_right)) /\ exists bcf_quotient_bcs_previous_right_decoded_value. bcf_row_code_bcs_previous_right = bcf_quotient_bcs_previous_right_decoded_value * S ((S (j)) * bcf_row_scale_bcs_previous_right) + (c)))))))))
  114. 0114specialize choose_exists n
  115. 0115specialize choose_exists j
  116. 0116exact choose_exists
  117. 0117cases hc_exists
  118. 0118have hd_exists : ∃ d. Choose(n,S j,d)
    Exact native replay linehave hd_exists : exists d. (((exists bcf_lt_gap_bcs_current_right_out_of_range. bcf_lt_gap_bcs_current_right_out_of_range + S (n) = S j) /\ d = 0) \/ ((exists bcf_le_gap_bcs_current_right_in_range. bcf_le_gap_bcs_current_right_in_range + (S j) = n) /\ (exists bcf_row_code_code_bcs_current_right bcf_row_code_scale_bcs_current_right bcf_row_scale_code_bcs_current_right bcf_row_scale_scale_bcs_current_right bcf_row_code_bcs_current_right bcf_row_scale_bcs_current_right. ((forall bcf_row_index_bcs_current_right_table. (exists bcf_lt_gap_bcs_current_right_table_row_bound. bcf_lt_gap_bcs_current_right_table_row_bound + S (bcf_row_index_bcs_current_right_table) = S (n)) -> exists bcf_row_code_bcs_current_right_table bcf_row_scale_bcs_current_right_table. ((((exists bcf_height_bcs_current_right_table_decoded_row_code. bcf_height_bcs_current_right_table_decoded_row_code + S (bcf_row_code_bcs_current_right_table) = S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_row_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_row_code * S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right) + (bcf_row_code_bcs_current_right_table))) /\ ((((exists bcf_height_bcs_current_right_table_decoded_row_scale. bcf_height_bcs_current_right_table_decoded_row_scale + S (bcf_row_scale_bcs_current_right_table) = S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_row_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_row_scale * S ((S (bcf_row_index_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right) + (bcf_row_scale_bcs_current_right_table))) /\ ((bcf_row_index_bcs_current_right_table = 0 /\ (forall bcf_index_bcs_current_right_table_zero_row. (exists bcf_lt_gap_bcs_current_right_table_zero_row_bound. bcf_lt_gap_bcs_current_right_table_zero_row_bound + S (bcf_index_bcs_current_right_table_zero_row) = S (n)) -> exists bcf_value_bcs_current_right_table_zero_row. ((((exists bcf_height_bcs_current_right_table_zero_row_entry. bcf_height_bcs_current_right_table_zero_row_entry + S (bcf_value_bcs_current_right_table_zero_row) = S ((S (bcf_index_bcs_current_right_table_zero_row)) * bcf_row_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_zero_row_entry. bcf_row_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_zero_row_entry * S ((S (bcf_index_bcs_current_right_table_zero_row)) * bcf_row_scale_bcs_current_right_table) + (bcf_value_bcs_current_right_table_zero_row))) /\ ((bcf_index_bcs_current_right_table_zero_row = 0 /\ bcf_value_bcs_current_right_table_zero_row = 1) \/ exists bcf_predecessor_bcs_current_right_table_zero_row. bcf_index_bcs_current_right_table_zero_row = S bcf_predecessor_bcs_current_right_table_zero_row /\ bcf_value_bcs_current_right_table_zero_row = 0)))) \/ exists bcf_predecessor_bcs_current_right_table bcf_previous_code_bcs_current_right_table bcf_previous_scale_bcs_current_right_table. bcf_row_index_bcs_current_right_table = S bcf_predecessor_bcs_current_right_table /\ ((((exists bcf_height_bcs_current_right_table_decoded_previous_code. bcf_height_bcs_current_right_table_decoded_previous_code + S (bcf_previous_code_bcs_current_right_table) = S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_previous_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_previous_code * S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_code_scale_bcs_current_right) + (bcf_previous_code_bcs_current_right_table))) /\ ((((exists bcf_height_bcs_current_right_table_decoded_previous_scale. bcf_height_bcs_current_right_table_decoded_previous_scale + S (bcf_previous_scale_bcs_current_right_table) = S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_table_decoded_previous_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_table_decoded_previous_scale * S ((S (bcf_predecessor_bcs_current_right_table)) * bcf_row_scale_scale_bcs_current_right) + (bcf_previous_scale_bcs_current_right_table))) /\ (forall bcf_index_bcs_current_right_table_row_step. (exists bcf_lt_gap_bcs_current_right_table_row_step_bound. bcf_lt_gap_bcs_current_right_table_row_step_bound + S (bcf_index_bcs_current_right_table_row_step) = S (n)) -> exists bcf_value_bcs_current_right_table_row_step. ((((exists bcf_height_bcs_current_right_table_row_step_entry. bcf_height_bcs_current_right_table_row_step_entry + S (bcf_value_bcs_current_right_table_row_step) = S ((S (bcf_index_bcs_current_right_table_row_step)) * bcf_row_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_entry. bcf_row_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_entry * S ((S (bcf_index_bcs_current_right_table_row_step)) * bcf_row_scale_bcs_current_right_table) + (bcf_value_bcs_current_right_table_row_step))) /\ ((bcf_index_bcs_current_right_table_row_step = 0 /\ bcf_value_bcs_current_right_table_row_step = 1) \/ exists bcf_predecessor_bcs_current_right_table_row_step bcf_left_bcs_current_right_table_row_step bcf_right_bcs_current_right_table_row_step. bcf_index_bcs_current_right_table_row_step = S bcf_predecessor_bcs_current_right_table_row_step /\ ((((exists bcf_height_bcs_current_right_table_row_step_previous_left. bcf_height_bcs_current_right_table_row_step_previous_left + S (bcf_left_bcs_current_right_table_row_step) = S ((S (bcf_predecessor_bcs_current_right_table_row_step)) * bcf_previous_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_previous_left. bcf_previous_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_previous_left * S ((S (bcf_predecessor_bcs_current_right_table_row_step)) * bcf_previous_scale_bcs_current_right_table) + (bcf_left_bcs_current_right_table_row_step))) /\ ((((exists bcf_height_bcs_current_right_table_row_step_previous_right. bcf_height_bcs_current_right_table_row_step_previous_right + S (bcf_right_bcs_current_right_table_row_step) = S ((S (S (bcf_predecessor_bcs_current_right_table_row_step))) * bcf_previous_scale_bcs_current_right_table)) /\ exists bcf_quotient_bcs_current_right_table_row_step_previous_right. bcf_previous_code_bcs_current_right_table = bcf_quotient_bcs_current_right_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcs_current_right_table_row_step))) * bcf_previous_scale_bcs_current_right_table) + (bcf_right_bcs_current_right_table_row_step))) /\ bcf_value_bcs_current_right_table_row_step = bcf_left_bcs_current_right_table_row_step + bcf_right_bcs_current_right_table_row_step))))))))))) /\ ((((exists bcf_height_bcs_current_right_decoded_row_code. bcf_height_bcs_current_right_decoded_row_code + S (bcf_row_code_bcs_current_right) = S ((S (n)) * bcf_row_code_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_row_code. bcf_row_code_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcs_current_right) + (bcf_row_code_bcs_current_right))) /\ ((((exists bcf_height_bcs_current_right_decoded_row_scale. bcf_height_bcs_current_right_decoded_row_scale + S (bcf_row_scale_bcs_current_right) = S ((S (n)) * bcf_row_scale_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_row_scale. bcf_row_scale_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcs_current_right) + (bcf_row_scale_bcs_current_right))) /\ (((exists bcf_height_bcs_current_right_decoded_value. bcf_height_bcs_current_right_decoded_value + S (d) = S ((S (S j)) * bcf_row_scale_bcs_current_right)) /\ exists bcf_quotient_bcs_current_right_decoded_value. bcf_row_code_bcs_current_right = bcf_quotient_bcs_current_right_decoded_value * S ((S (S j)) * bcf_row_scale_bcs_current_right) + (d)))))))))
  119. 0119specialize choose_exists n
  120. 0120specialize choose_exists (S j)
  121. 0121exact choose_exists
  122. 0122cases hd_exists
  123. 0123have hleft_complement : S k + j = n
  124. 0124apply PA2
  125. 0125trans S k + S j
  126. 0126symm
  127. 0127apply PA4
  128. 0128exact hsum
  129. 0129have hright_complement : k + S j = n
  130. 0130trans S (k + j)
  131. 0131apply PA4
  132. 0132trans S k + j
  133. 0133symm
  134. 0134apply add_succ_left
  135. 0135exact hleft_complement
  136. 0136have hx_sum : x = x1 + x2
  137. 0137specialize choose_succ_succ n
  138. 0138specialize choose_succ_succ k
  139. 0139specialize choose_succ_succ x1
  140. 0140specialize choose_succ_succ x2
  141. 0141specialize choose_succ_succ x
  142. 0142apply choose_succ_succ
  143. 0143exact ha_exists_witness
  144. 0144exact hb_exists_witness
  145. 0145exact hleft
  146. 0146have hy_sum : y = x3 + x4
  147. 0147specialize choose_succ_succ n
  148. 0148specialize choose_succ_succ j
  149. 0149specialize choose_succ_succ x3
  150. 0150specialize choose_succ_succ x4
  151. 0151specialize choose_succ_succ y
  152. 0152apply choose_succ_succ
  153. 0153exact hc_exists_witness
  154. 0154exact hd_exists_witness
  155. 0155exact hright
  156. 0156have hfirst : x1 = x4
  157. 0157specialize IH k
  158. 0158specialize IH (S j)
  159. 0159specialize IH x1
  160. 0160specialize IH x4
  161. 0161apply IH
  162. 0162exact hright_complement
  163. 0163exact ha_exists_witness
  164. 0164exact hd_exists_witness
  165. 0165have hsecond : x2 = x3
  166. 0166specialize IH (S k)
  167. 0167specialize IH j
  168. 0168specialize IH x2
  169. 0169specialize IH x3
  170. 0170apply IH
  171. 0171exact hleft_complement
  172. 0172exact hb_exists_witness
  173. 0173exact hc_exists_witness
  174. 0174rewrite hx_sum
  175. 0175rewrite hy_sum
  176. 0176rewrite hfirst
  177. 0177rewrite hsecond
  178. 0178apply add_comm