BT00TS · Bertrand theorem

central_binom_succ_double_middle

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

A successor central binomial is twice its odd-row middle value.

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. ∀ d. CentralBinom(S n,d) → ∃ x. Choose(S (n + n),n,x) ∧ d = x + x

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 PD0042 CentralBinom

2 occurrences

In local proof propositions

PD0041 Choose

3 occurrences

Exact expanded native-PA statement
forall n d. (((exists bcf_lt_gap_bcbsdm_successor_out_of_range. bcf_lt_gap_bcbsdm_successor_out_of_range + S (S n + S n) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbsdm_successor_in_range. bcf_le_gap_bcbsdm_successor_in_range + (S n) = S n + S n) /\ (exists bcf_row_code_code_bcbsdm_successor bcf_row_code_scale_bcbsdm_successor bcf_row_scale_code_bcbsdm_successor bcf_row_scale_scale_bcbsdm_successor bcf_row_code_bcbsdm_successor bcf_row_scale_bcbsdm_successor. ((forall bcf_row_index_bcbsdm_successor_table. (exists bcf_lt_gap_bcbsdm_successor_table_row_bound. bcf_lt_gap_bcbsdm_successor_table_row_bound + S (bcf_row_index_bcbsdm_successor_table) = S (S n + S n)) -> exists bcf_row_code_bcbsdm_successor_table bcf_row_scale_bcbsdm_successor_table. ((((exists bcf_height_bcbsdm_successor_table_decoded_row_code. bcf_height_bcbsdm_successor_table_decoded_row_code + S (bcf_row_code_bcbsdm_successor_table) = S ((S (bcf_row_index_bcbsdm_successor_table)) * bcf_row_code_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_table_decoded_row_code. bcf_row_code_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_table_decoded_row_code * S ((S (bcf_row_index_bcbsdm_successor_table)) * bcf_row_code_scale_bcbsdm_successor) + (bcf_row_code_bcbsdm_successor_table))) /\ ((((exists bcf_height_bcbsdm_successor_table_decoded_row_scale. bcf_height_bcbsdm_successor_table_decoded_row_scale + S (bcf_row_scale_bcbsdm_successor_table) = S ((S (bcf_row_index_bcbsdm_successor_table)) * bcf_row_scale_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_table_decoded_row_scale. bcf_row_scale_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_table_decoded_row_scale * S ((S (bcf_row_index_bcbsdm_successor_table)) * bcf_row_scale_scale_bcbsdm_successor) + (bcf_row_scale_bcbsdm_successor_table))) /\ ((bcf_row_index_bcbsdm_successor_table = 0 /\ (forall bcf_index_bcbsdm_successor_table_zero_row. (exists bcf_lt_gap_bcbsdm_successor_table_zero_row_bound. bcf_lt_gap_bcbsdm_successor_table_zero_row_bound + S (bcf_index_bcbsdm_successor_table_zero_row) = S (S n + S n)) -> exists bcf_value_bcbsdm_successor_table_zero_row. ((((exists bcf_height_bcbsdm_successor_table_zero_row_entry. bcf_height_bcbsdm_successor_table_zero_row_entry + S (bcf_value_bcbsdm_successor_table_zero_row) = S ((S (bcf_index_bcbsdm_successor_table_zero_row)) * bcf_row_scale_bcbsdm_successor_table)) /\ exists bcf_quotient_bcbsdm_successor_table_zero_row_entry. bcf_row_code_bcbsdm_successor_table = bcf_quotient_bcbsdm_successor_table_zero_row_entry * S ((S (bcf_index_bcbsdm_successor_table_zero_row)) * bcf_row_scale_bcbsdm_successor_table) + (bcf_value_bcbsdm_successor_table_zero_row))) /\ ((bcf_index_bcbsdm_successor_table_zero_row = 0 /\ bcf_value_bcbsdm_successor_table_zero_row = 1) \/ exists bcf_predecessor_bcbsdm_successor_table_zero_row. bcf_index_bcbsdm_successor_table_zero_row = S bcf_predecessor_bcbsdm_successor_table_zero_row /\ bcf_value_bcbsdm_successor_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsdm_successor_table bcf_previous_code_bcbsdm_successor_table bcf_previous_scale_bcbsdm_successor_table. bcf_row_index_bcbsdm_successor_table = S bcf_predecessor_bcbsdm_successor_table /\ ((((exists bcf_height_bcbsdm_successor_table_decoded_previous_code. bcf_height_bcbsdm_successor_table_decoded_previous_code + S (bcf_previous_code_bcbsdm_successor_table) = S ((S (bcf_predecessor_bcbsdm_successor_table)) * bcf_row_code_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_table_decoded_previous_code. bcf_row_code_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsdm_successor_table)) * bcf_row_code_scale_bcbsdm_successor) + (bcf_previous_code_bcbsdm_successor_table))) /\ ((((exists bcf_height_bcbsdm_successor_table_decoded_previous_scale. bcf_height_bcbsdm_successor_table_decoded_previous_scale + S (bcf_previous_scale_bcbsdm_successor_table) = S ((S (bcf_predecessor_bcbsdm_successor_table)) * bcf_row_scale_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_table_decoded_previous_scale. bcf_row_scale_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsdm_successor_table)) * bcf_row_scale_scale_bcbsdm_successor) + (bcf_previous_scale_bcbsdm_successor_table))) /\ (forall bcf_index_bcbsdm_successor_table_row_step. (exists bcf_lt_gap_bcbsdm_successor_table_row_step_bound. bcf_lt_gap_bcbsdm_successor_table_row_step_bound + S (bcf_index_bcbsdm_successor_table_row_step) = S (S n + S n)) -> exists bcf_value_bcbsdm_successor_table_row_step. ((((exists bcf_height_bcbsdm_successor_table_row_step_entry. bcf_height_bcbsdm_successor_table_row_step_entry + S (bcf_value_bcbsdm_successor_table_row_step) = S ((S (bcf_index_bcbsdm_successor_table_row_step)) * bcf_row_scale_bcbsdm_successor_table)) /\ exists bcf_quotient_bcbsdm_successor_table_row_step_entry. bcf_row_code_bcbsdm_successor_table = bcf_quotient_bcbsdm_successor_table_row_step_entry * S ((S (bcf_index_bcbsdm_successor_table_row_step)) * bcf_row_scale_bcbsdm_successor_table) + (bcf_value_bcbsdm_successor_table_row_step))) /\ ((bcf_index_bcbsdm_successor_table_row_step = 0 /\ bcf_value_bcbsdm_successor_table_row_step = 1) \/ exists bcf_predecessor_bcbsdm_successor_table_row_step bcf_left_bcbsdm_successor_table_row_step bcf_right_bcbsdm_successor_table_row_step. bcf_index_bcbsdm_successor_table_row_step = S bcf_predecessor_bcbsdm_successor_table_row_step /\ ((((exists bcf_height_bcbsdm_successor_table_row_step_previous_left. bcf_height_bcbsdm_successor_table_row_step_previous_left + S (bcf_left_bcbsdm_successor_table_row_step) = S ((S (bcf_predecessor_bcbsdm_successor_table_row_step)) * bcf_previous_scale_bcbsdm_successor_table)) /\ exists bcf_quotient_bcbsdm_successor_table_row_step_previous_left. bcf_previous_code_bcbsdm_successor_table = bcf_quotient_bcbsdm_successor_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsdm_successor_table_row_step)) * bcf_previous_scale_bcbsdm_successor_table) + (bcf_left_bcbsdm_successor_table_row_step))) /\ ((((exists bcf_height_bcbsdm_successor_table_row_step_previous_right. bcf_height_bcbsdm_successor_table_row_step_previous_right + S (bcf_right_bcbsdm_successor_table_row_step) = S ((S (S (bcf_predecessor_bcbsdm_successor_table_row_step))) * bcf_previous_scale_bcbsdm_successor_table)) /\ exists bcf_quotient_bcbsdm_successor_table_row_step_previous_right. bcf_previous_code_bcbsdm_successor_table = bcf_quotient_bcbsdm_successor_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsdm_successor_table_row_step))) * bcf_previous_scale_bcbsdm_successor_table) + (bcf_right_bcbsdm_successor_table_row_step))) /\ bcf_value_bcbsdm_successor_table_row_step = bcf_left_bcbsdm_successor_table_row_step + bcf_right_bcbsdm_successor_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsdm_successor_decoded_row_code. bcf_height_bcbsdm_successor_decoded_row_code + S (bcf_row_code_bcbsdm_successor) = S ((S (S n + S n)) * bcf_row_code_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_decoded_row_code. bcf_row_code_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_decoded_row_code * S ((S (S n + S n)) * bcf_row_code_scale_bcbsdm_successor) + (bcf_row_code_bcbsdm_successor))) /\ ((((exists bcf_height_bcbsdm_successor_decoded_row_scale. bcf_height_bcbsdm_successor_decoded_row_scale + S (bcf_row_scale_bcbsdm_successor) = S ((S (S n + S n)) * bcf_row_scale_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_decoded_row_scale. bcf_row_scale_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_decoded_row_scale * S ((S (S n + S n)) * bcf_row_scale_scale_bcbsdm_successor) + (bcf_row_scale_bcbsdm_successor))) /\ (((exists bcf_height_bcbsdm_successor_decoded_value. bcf_height_bcbsdm_successor_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbsdm_successor)) /\ exists bcf_quotient_bcbsdm_successor_decoded_value. bcf_row_code_bcbsdm_successor = bcf_quotient_bcbsdm_successor_decoded_value * S ((S (S n)) * bcf_row_scale_bcbsdm_successor) + (d))))))))) -> exists m. ((((exists bcf_lt_gap_bcbsdm_middle_out_of_range. bcf_lt_gap_bcbsdm_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbsdm_middle_in_range. bcf_le_gap_bcbsdm_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbsdm_middle bcf_row_code_scale_bcbsdm_middle bcf_row_scale_code_bcbsdm_middle bcf_row_scale_scale_bcbsdm_middle bcf_row_code_bcbsdm_middle bcf_row_scale_bcbsdm_middle. ((forall bcf_row_index_bcbsdm_middle_table. (exists bcf_lt_gap_bcbsdm_middle_table_row_bound. bcf_lt_gap_bcbsdm_middle_table_row_bound + S (bcf_row_index_bcbsdm_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbsdm_middle_table bcf_row_scale_bcbsdm_middle_table. ((((exists bcf_height_bcbsdm_middle_table_decoded_row_code. bcf_height_bcbsdm_middle_table_decoded_row_code + S (bcf_row_code_bcbsdm_middle_table) = S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_row_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle) + (bcf_row_code_bcbsdm_middle_table))) /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_row_scale. bcf_height_bcbsdm_middle_table_decoded_row_scale + S (bcf_row_scale_bcbsdm_middle_table) = S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_row_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_row_scale_bcbsdm_middle_table))) /\ ((bcf_row_index_bcbsdm_middle_table = 0 /\ (forall bcf_index_bcbsdm_middle_table_zero_row. (exists bcf_lt_gap_bcbsdm_middle_table_zero_row_bound. bcf_lt_gap_bcbsdm_middle_table_zero_row_bound + S (bcf_index_bcbsdm_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbsdm_middle_table_zero_row. ((((exists bcf_height_bcbsdm_middle_table_zero_row_entry. bcf_height_bcbsdm_middle_table_zero_row_entry + S (bcf_value_bcbsdm_middle_table_zero_row) = S ((S (bcf_index_bcbsdm_middle_table_zero_row)) * bcf_row_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_zero_row_entry. bcf_row_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_zero_row_entry * S ((S (bcf_index_bcbsdm_middle_table_zero_row)) * bcf_row_scale_bcbsdm_middle_table) + (bcf_value_bcbsdm_middle_table_zero_row))) /\ ((bcf_index_bcbsdm_middle_table_zero_row = 0 /\ bcf_value_bcbsdm_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbsdm_middle_table_zero_row. bcf_index_bcbsdm_middle_table_zero_row = S bcf_predecessor_bcbsdm_middle_table_zero_row /\ bcf_value_bcbsdm_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsdm_middle_table bcf_previous_code_bcbsdm_middle_table bcf_previous_scale_bcbsdm_middle_table. bcf_row_index_bcbsdm_middle_table = S bcf_predecessor_bcbsdm_middle_table /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_previous_code. bcf_height_bcbsdm_middle_table_decoded_previous_code + S (bcf_previous_code_bcbsdm_middle_table) = S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_previous_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle) + (bcf_previous_code_bcbsdm_middle_table))) /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_previous_scale. bcf_height_bcbsdm_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbsdm_middle_table) = S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_previous_scale_bcbsdm_middle_table))) /\ (forall bcf_index_bcbsdm_middle_table_row_step. (exists bcf_lt_gap_bcbsdm_middle_table_row_step_bound. bcf_lt_gap_bcbsdm_middle_table_row_step_bound + S (bcf_index_bcbsdm_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbsdm_middle_table_row_step. ((((exists bcf_height_bcbsdm_middle_table_row_step_entry. bcf_height_bcbsdm_middle_table_row_step_entry + S (bcf_value_bcbsdm_middle_table_row_step) = S ((S (bcf_index_bcbsdm_middle_table_row_step)) * bcf_row_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_entry. bcf_row_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_entry * S ((S (bcf_index_bcbsdm_middle_table_row_step)) * bcf_row_scale_bcbsdm_middle_table) + (bcf_value_bcbsdm_middle_table_row_step))) /\ ((bcf_index_bcbsdm_middle_table_row_step = 0 /\ bcf_value_bcbsdm_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbsdm_middle_table_row_step bcf_left_bcbsdm_middle_table_row_step bcf_right_bcbsdm_middle_table_row_step. bcf_index_bcbsdm_middle_table_row_step = S bcf_predecessor_bcbsdm_middle_table_row_step /\ ((((exists bcf_height_bcbsdm_middle_table_row_step_previous_left. bcf_height_bcbsdm_middle_table_row_step_previous_left + S (bcf_left_bcbsdm_middle_table_row_step) = S ((S (bcf_predecessor_bcbsdm_middle_table_row_step)) * bcf_previous_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_previous_left. bcf_previous_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsdm_middle_table_row_step)) * bcf_previous_scale_bcbsdm_middle_table) + (bcf_left_bcbsdm_middle_table_row_step))) /\ ((((exists bcf_height_bcbsdm_middle_table_row_step_previous_right. bcf_height_bcbsdm_middle_table_row_step_previous_right + S (bcf_right_bcbsdm_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbsdm_middle_table_row_step))) * bcf_previous_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_previous_right. bcf_previous_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsdm_middle_table_row_step))) * bcf_previous_scale_bcbsdm_middle_table) + (bcf_right_bcbsdm_middle_table_row_step))) /\ bcf_value_bcbsdm_middle_table_row_step = bcf_left_bcbsdm_middle_table_row_step + bcf_right_bcbsdm_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsdm_middle_decoded_row_code. bcf_height_bcbsdm_middle_decoded_row_code + S (bcf_row_code_bcbsdm_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_row_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_middle) + (bcf_row_code_bcbsdm_middle))) /\ ((((exists bcf_height_bcbsdm_middle_decoded_row_scale. bcf_height_bcbsdm_middle_decoded_row_scale + S (bcf_row_scale_bcbsdm_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_row_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_row_scale_bcbsdm_middle))) /\ (((exists bcf_height_bcbsdm_middle_decoded_value. bcf_height_bcbsdm_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_value. bcf_row_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbsdm_middle) + (m))))))))) /\ d = m + m)

Proof neighborhood

Direct theorem prerequisites

BT0001 add_succ_left BT00T8 choose_exists BT00TL choose_symmetry BT00TJ choose_succ_succ BT00TR choose_upper_eq_transport

Direct theorem dependents

BT00TU central_binom_succ_recurrence BT00VL central_binom_recurrence_double_bundle

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

55 script commands · 15 reading checkpoints · 6 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 (5)
add succ leftchoose existschoose symmetrychoose succ succchoose upper eq transport
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro d
  3. L3
    intro hsuccessor
02Establish hupperL4–10

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

  1. L4
    have hupper : S n + S n = S (S (n + n))
  2. L5
    trans S (n + S n)
  3. L6
    specialize add_succ_left n
  4. L7
    specialize add_succ_left (S n)
  5. L8
    apply add_succ_left
  6. L9
    congr
  7. L10
    apply PA4
03Establish hnormalizedL11–18

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

  1. L11
    have hnormalized : Choose(S S (n + n),S n,d)Definitions: Choose(S S (n + n),S n,d)Original native command in the exact edition
  2. L12
    specialize choose_upper_eq_transport (S n + S n)
  3. L13
    specialize choose_upper_eq_transport (S (S (n + n)))
  4. L14
    specialize choose_upper_eq_transport (S n)
  5. L15
    specialize choose_upper_eq_transport d
  6. L16
    apply choose_upper_eq_transport
  7. L17
    exact hupper
  8. L18
    exact hsuccessor
04Establish hmiddle_existsL19–22

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

  1. L19
    have hmiddle_exists : ∃ m. Choose(S (n + n),n,m)Definitions: Choose(S (n + n),n,m)Original native command in the exact edition
  2. L20
    specialize choose_exists (S (n + n))
  3. L21
    specialize choose_exists n
  4. L22
    exact choose_exists
05Separate the logical casesL23–23

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

  1. L23
    cases hmiddle_exists
06Establish hmirror_existsL24–27

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

  1. L24
    have hmirror_exists : ∃ r. Choose(S (n + n),S n,r)Definitions: Choose(S (n + n),S n,r)Original native command in the exact edition
  2. L25
    specialize choose_exists (S (n + n))
  3. L26
    specialize choose_exists (S n)
  4. L27
    exact choose_exists
07Separate the logical casesL28–28

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

  1. L28
    cases hmirror_exists
08Establish hsymL29–38

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

  1. L29
    have hsym : x = x1
  2. L30
    specialize choose_symmetry (S (n + n))
  3. L31
    specialize choose_symmetry n
  4. L32
    specialize choose_symmetry (S n)
  5. L33
    specialize choose_symmetry x
  6. L34
    specialize choose_symmetry x1
  7. L35
    apply choose_symmetry
  8. L36
    apply PA4
  9. L37
    exact hmiddle_exists_witness
  10. L38
    exact hmirror_exists_witness
09Establish hsumL39–48

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

  1. L39
    have hsum : d = x + x1
  2. L40
    specialize choose_succ_succ (S (n + n))
  3. L41
    specialize choose_succ_succ n
  4. L42
    specialize choose_succ_succ x
  5. L43
    specialize choose_succ_succ x1
  6. L44
    specialize choose_succ_succ d
  7. L45
    apply choose_succ_succ
  8. L46
    exact hmiddle_exists_witness
  9. L47
    exact hmirror_exists_witness
  10. L48
    exact hnormalized
10Construct an explicit witnessL49–49

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

  1. L49
    exists x
11Separate the logical casesL50–50

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

  1. L50
    split
12Use earlier factsL51–51

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

  1. L51
    exact hmiddle_exists_witness
13Calculate and transport equalitiesL52–52

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

  1. L52
    trans x + x1
14Use earlier factsL53–53

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

  1. L53
    exact hsum
15Calculate and transport equalitiesL54–55

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

  1. L54
    rewrite <- hsym
  2. L55
    refl

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro n
  2. 0002intro d
  3. 0003intro hsuccessor
  4. 0004have hupper : S n + S n = S (S (n + n))
  5. 0005trans S (n + S n)
  6. 0006specialize add_succ_left n
  7. 0007specialize add_succ_left (S n)
  8. 0008apply add_succ_left
  9. 0009congr
  10. 0010apply PA4
  11. 0011have hnormalized : Choose(S S (n + n),S n,d)
    Exact native replay linehave hnormalized : ((exists bcf_lt_gap_bcbsdm_normalized_out_of_range. bcf_lt_gap_bcbsdm_normalized_out_of_range + S (S (S (n + n))) = S n) /\ d = 0) \/ ((exists bcf_le_gap_bcbsdm_normalized_in_range. bcf_le_gap_bcbsdm_normalized_in_range + (S n) = S (S (n + n))) /\ (exists bcf_row_code_code_bcbsdm_normalized bcf_row_code_scale_bcbsdm_normalized bcf_row_scale_code_bcbsdm_normalized bcf_row_scale_scale_bcbsdm_normalized bcf_row_code_bcbsdm_normalized bcf_row_scale_bcbsdm_normalized. ((forall bcf_row_index_bcbsdm_normalized_table. (exists bcf_lt_gap_bcbsdm_normalized_table_row_bound. bcf_lt_gap_bcbsdm_normalized_table_row_bound + S (bcf_row_index_bcbsdm_normalized_table) = S (S (S (n + n)))) -> exists bcf_row_code_bcbsdm_normalized_table bcf_row_scale_bcbsdm_normalized_table. ((((exists bcf_height_bcbsdm_normalized_table_decoded_row_code. bcf_height_bcbsdm_normalized_table_decoded_row_code + S (bcf_row_code_bcbsdm_normalized_table) = S ((S (bcf_row_index_bcbsdm_normalized_table)) * bcf_row_code_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_table_decoded_row_code. bcf_row_code_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_table_decoded_row_code * S ((S (bcf_row_index_bcbsdm_normalized_table)) * bcf_row_code_scale_bcbsdm_normalized) + (bcf_row_code_bcbsdm_normalized_table))) /\ ((((exists bcf_height_bcbsdm_normalized_table_decoded_row_scale. bcf_height_bcbsdm_normalized_table_decoded_row_scale + S (bcf_row_scale_bcbsdm_normalized_table) = S ((S (bcf_row_index_bcbsdm_normalized_table)) * bcf_row_scale_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_table_decoded_row_scale. bcf_row_scale_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_table_decoded_row_scale * S ((S (bcf_row_index_bcbsdm_normalized_table)) * bcf_row_scale_scale_bcbsdm_normalized) + (bcf_row_scale_bcbsdm_normalized_table))) /\ ((bcf_row_index_bcbsdm_normalized_table = 0 /\ (forall bcf_index_bcbsdm_normalized_table_zero_row. (exists bcf_lt_gap_bcbsdm_normalized_table_zero_row_bound. bcf_lt_gap_bcbsdm_normalized_table_zero_row_bound + S (bcf_index_bcbsdm_normalized_table_zero_row) = S (S (S (n + n)))) -> exists bcf_value_bcbsdm_normalized_table_zero_row. ((((exists bcf_height_bcbsdm_normalized_table_zero_row_entry. bcf_height_bcbsdm_normalized_table_zero_row_entry + S (bcf_value_bcbsdm_normalized_table_zero_row) = S ((S (bcf_index_bcbsdm_normalized_table_zero_row)) * bcf_row_scale_bcbsdm_normalized_table)) /\ exists bcf_quotient_bcbsdm_normalized_table_zero_row_entry. bcf_row_code_bcbsdm_normalized_table = bcf_quotient_bcbsdm_normalized_table_zero_row_entry * S ((S (bcf_index_bcbsdm_normalized_table_zero_row)) * bcf_row_scale_bcbsdm_normalized_table) + (bcf_value_bcbsdm_normalized_table_zero_row))) /\ ((bcf_index_bcbsdm_normalized_table_zero_row = 0 /\ bcf_value_bcbsdm_normalized_table_zero_row = 1) \/ exists bcf_predecessor_bcbsdm_normalized_table_zero_row. bcf_index_bcbsdm_normalized_table_zero_row = S bcf_predecessor_bcbsdm_normalized_table_zero_row /\ bcf_value_bcbsdm_normalized_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsdm_normalized_table bcf_previous_code_bcbsdm_normalized_table bcf_previous_scale_bcbsdm_normalized_table. bcf_row_index_bcbsdm_normalized_table = S bcf_predecessor_bcbsdm_normalized_table /\ ((((exists bcf_height_bcbsdm_normalized_table_decoded_previous_code. bcf_height_bcbsdm_normalized_table_decoded_previous_code + S (bcf_previous_code_bcbsdm_normalized_table) = S ((S (bcf_predecessor_bcbsdm_normalized_table)) * bcf_row_code_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_table_decoded_previous_code. bcf_row_code_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsdm_normalized_table)) * bcf_row_code_scale_bcbsdm_normalized) + (bcf_previous_code_bcbsdm_normalized_table))) /\ ((((exists bcf_height_bcbsdm_normalized_table_decoded_previous_scale. bcf_height_bcbsdm_normalized_table_decoded_previous_scale + S (bcf_previous_scale_bcbsdm_normalized_table) = S ((S (bcf_predecessor_bcbsdm_normalized_table)) * bcf_row_scale_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_table_decoded_previous_scale. bcf_row_scale_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsdm_normalized_table)) * bcf_row_scale_scale_bcbsdm_normalized) + (bcf_previous_scale_bcbsdm_normalized_table))) /\ (forall bcf_index_bcbsdm_normalized_table_row_step. (exists bcf_lt_gap_bcbsdm_normalized_table_row_step_bound. bcf_lt_gap_bcbsdm_normalized_table_row_step_bound + S (bcf_index_bcbsdm_normalized_table_row_step) = S (S (S (n + n)))) -> exists bcf_value_bcbsdm_normalized_table_row_step. ((((exists bcf_height_bcbsdm_normalized_table_row_step_entry. bcf_height_bcbsdm_normalized_table_row_step_entry + S (bcf_value_bcbsdm_normalized_table_row_step) = S ((S (bcf_index_bcbsdm_normalized_table_row_step)) * bcf_row_scale_bcbsdm_normalized_table)) /\ exists bcf_quotient_bcbsdm_normalized_table_row_step_entry. bcf_row_code_bcbsdm_normalized_table = bcf_quotient_bcbsdm_normalized_table_row_step_entry * S ((S (bcf_index_bcbsdm_normalized_table_row_step)) * bcf_row_scale_bcbsdm_normalized_table) + (bcf_value_bcbsdm_normalized_table_row_step))) /\ ((bcf_index_bcbsdm_normalized_table_row_step = 0 /\ bcf_value_bcbsdm_normalized_table_row_step = 1) \/ exists bcf_predecessor_bcbsdm_normalized_table_row_step bcf_left_bcbsdm_normalized_table_row_step bcf_right_bcbsdm_normalized_table_row_step. bcf_index_bcbsdm_normalized_table_row_step = S bcf_predecessor_bcbsdm_normalized_table_row_step /\ ((((exists bcf_height_bcbsdm_normalized_table_row_step_previous_left. bcf_height_bcbsdm_normalized_table_row_step_previous_left + S (bcf_left_bcbsdm_normalized_table_row_step) = S ((S (bcf_predecessor_bcbsdm_normalized_table_row_step)) * bcf_previous_scale_bcbsdm_normalized_table)) /\ exists bcf_quotient_bcbsdm_normalized_table_row_step_previous_left. bcf_previous_code_bcbsdm_normalized_table = bcf_quotient_bcbsdm_normalized_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsdm_normalized_table_row_step)) * bcf_previous_scale_bcbsdm_normalized_table) + (bcf_left_bcbsdm_normalized_table_row_step))) /\ ((((exists bcf_height_bcbsdm_normalized_table_row_step_previous_right. bcf_height_bcbsdm_normalized_table_row_step_previous_right + S (bcf_right_bcbsdm_normalized_table_row_step) = S ((S (S (bcf_predecessor_bcbsdm_normalized_table_row_step))) * bcf_previous_scale_bcbsdm_normalized_table)) /\ exists bcf_quotient_bcbsdm_normalized_table_row_step_previous_right. bcf_previous_code_bcbsdm_normalized_table = bcf_quotient_bcbsdm_normalized_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsdm_normalized_table_row_step))) * bcf_previous_scale_bcbsdm_normalized_table) + (bcf_right_bcbsdm_normalized_table_row_step))) /\ bcf_value_bcbsdm_normalized_table_row_step = bcf_left_bcbsdm_normalized_table_row_step + bcf_right_bcbsdm_normalized_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsdm_normalized_decoded_row_code. bcf_height_bcbsdm_normalized_decoded_row_code + S (bcf_row_code_bcbsdm_normalized) = S ((S (S (S (n + n)))) * bcf_row_code_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_decoded_row_code. bcf_row_code_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_decoded_row_code * S ((S (S (S (n + n)))) * bcf_row_code_scale_bcbsdm_normalized) + (bcf_row_code_bcbsdm_normalized))) /\ ((((exists bcf_height_bcbsdm_normalized_decoded_row_scale. bcf_height_bcbsdm_normalized_decoded_row_scale + S (bcf_row_scale_bcbsdm_normalized) = S ((S (S (S (n + n)))) * bcf_row_scale_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_decoded_row_scale. bcf_row_scale_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_decoded_row_scale * S ((S (S (S (n + n)))) * bcf_row_scale_scale_bcbsdm_normalized) + (bcf_row_scale_bcbsdm_normalized))) /\ (((exists bcf_height_bcbsdm_normalized_decoded_value. bcf_height_bcbsdm_normalized_decoded_value + S (d) = S ((S (S n)) * bcf_row_scale_bcbsdm_normalized)) /\ exists bcf_quotient_bcbsdm_normalized_decoded_value. bcf_row_code_bcbsdm_normalized = bcf_quotient_bcbsdm_normalized_decoded_value * S ((S (S n)) * bcf_row_scale_bcbsdm_normalized) + (d))))))))
  12. 0012specialize choose_upper_eq_transport (S n + S n)
  13. 0013specialize choose_upper_eq_transport (S (S (n + n)))
  14. 0014specialize choose_upper_eq_transport (S n)
  15. 0015specialize choose_upper_eq_transport d
  16. 0016apply choose_upper_eq_transport
  17. 0017exact hupper
  18. 0018exact hsuccessor
  19. 0019have hmiddle_exists : ∃ m. Choose(S (n + n),n,m)
    Exact native replay linehave hmiddle_exists : exists m. (((exists bcf_lt_gap_bcbsdm_middle_out_of_range. bcf_lt_gap_bcbsdm_middle_out_of_range + S (S (n + n)) = n) /\ m = 0) \/ ((exists bcf_le_gap_bcbsdm_middle_in_range. bcf_le_gap_bcbsdm_middle_in_range + (n) = S (n + n)) /\ (exists bcf_row_code_code_bcbsdm_middle bcf_row_code_scale_bcbsdm_middle bcf_row_scale_code_bcbsdm_middle bcf_row_scale_scale_bcbsdm_middle bcf_row_code_bcbsdm_middle bcf_row_scale_bcbsdm_middle. ((forall bcf_row_index_bcbsdm_middle_table. (exists bcf_lt_gap_bcbsdm_middle_table_row_bound. bcf_lt_gap_bcbsdm_middle_table_row_bound + S (bcf_row_index_bcbsdm_middle_table) = S (S (n + n))) -> exists bcf_row_code_bcbsdm_middle_table bcf_row_scale_bcbsdm_middle_table. ((((exists bcf_height_bcbsdm_middle_table_decoded_row_code. bcf_height_bcbsdm_middle_table_decoded_row_code + S (bcf_row_code_bcbsdm_middle_table) = S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_row_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_row_code * S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle) + (bcf_row_code_bcbsdm_middle_table))) /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_row_scale. bcf_height_bcbsdm_middle_table_decoded_row_scale + S (bcf_row_scale_bcbsdm_middle_table) = S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_row_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_row_scale * S ((S (bcf_row_index_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_row_scale_bcbsdm_middle_table))) /\ ((bcf_row_index_bcbsdm_middle_table = 0 /\ (forall bcf_index_bcbsdm_middle_table_zero_row. (exists bcf_lt_gap_bcbsdm_middle_table_zero_row_bound. bcf_lt_gap_bcbsdm_middle_table_zero_row_bound + S (bcf_index_bcbsdm_middle_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbsdm_middle_table_zero_row. ((((exists bcf_height_bcbsdm_middle_table_zero_row_entry. bcf_height_bcbsdm_middle_table_zero_row_entry + S (bcf_value_bcbsdm_middle_table_zero_row) = S ((S (bcf_index_bcbsdm_middle_table_zero_row)) * bcf_row_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_zero_row_entry. bcf_row_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_zero_row_entry * S ((S (bcf_index_bcbsdm_middle_table_zero_row)) * bcf_row_scale_bcbsdm_middle_table) + (bcf_value_bcbsdm_middle_table_zero_row))) /\ ((bcf_index_bcbsdm_middle_table_zero_row = 0 /\ bcf_value_bcbsdm_middle_table_zero_row = 1) \/ exists bcf_predecessor_bcbsdm_middle_table_zero_row. bcf_index_bcbsdm_middle_table_zero_row = S bcf_predecessor_bcbsdm_middle_table_zero_row /\ bcf_value_bcbsdm_middle_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsdm_middle_table bcf_previous_code_bcbsdm_middle_table bcf_previous_scale_bcbsdm_middle_table. bcf_row_index_bcbsdm_middle_table = S bcf_predecessor_bcbsdm_middle_table /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_previous_code. bcf_height_bcbsdm_middle_table_decoded_previous_code + S (bcf_previous_code_bcbsdm_middle_table) = S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_previous_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_code_scale_bcbsdm_middle) + (bcf_previous_code_bcbsdm_middle_table))) /\ ((((exists bcf_height_bcbsdm_middle_table_decoded_previous_scale. bcf_height_bcbsdm_middle_table_decoded_previous_scale + S (bcf_previous_scale_bcbsdm_middle_table) = S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_table_decoded_previous_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsdm_middle_table)) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_previous_scale_bcbsdm_middle_table))) /\ (forall bcf_index_bcbsdm_middle_table_row_step. (exists bcf_lt_gap_bcbsdm_middle_table_row_step_bound. bcf_lt_gap_bcbsdm_middle_table_row_step_bound + S (bcf_index_bcbsdm_middle_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbsdm_middle_table_row_step. ((((exists bcf_height_bcbsdm_middle_table_row_step_entry. bcf_height_bcbsdm_middle_table_row_step_entry + S (bcf_value_bcbsdm_middle_table_row_step) = S ((S (bcf_index_bcbsdm_middle_table_row_step)) * bcf_row_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_entry. bcf_row_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_entry * S ((S (bcf_index_bcbsdm_middle_table_row_step)) * bcf_row_scale_bcbsdm_middle_table) + (bcf_value_bcbsdm_middle_table_row_step))) /\ ((bcf_index_bcbsdm_middle_table_row_step = 0 /\ bcf_value_bcbsdm_middle_table_row_step = 1) \/ exists bcf_predecessor_bcbsdm_middle_table_row_step bcf_left_bcbsdm_middle_table_row_step bcf_right_bcbsdm_middle_table_row_step. bcf_index_bcbsdm_middle_table_row_step = S bcf_predecessor_bcbsdm_middle_table_row_step /\ ((((exists bcf_height_bcbsdm_middle_table_row_step_previous_left. bcf_height_bcbsdm_middle_table_row_step_previous_left + S (bcf_left_bcbsdm_middle_table_row_step) = S ((S (bcf_predecessor_bcbsdm_middle_table_row_step)) * bcf_previous_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_previous_left. bcf_previous_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsdm_middle_table_row_step)) * bcf_previous_scale_bcbsdm_middle_table) + (bcf_left_bcbsdm_middle_table_row_step))) /\ ((((exists bcf_height_bcbsdm_middle_table_row_step_previous_right. bcf_height_bcbsdm_middle_table_row_step_previous_right + S (bcf_right_bcbsdm_middle_table_row_step) = S ((S (S (bcf_predecessor_bcbsdm_middle_table_row_step))) * bcf_previous_scale_bcbsdm_middle_table)) /\ exists bcf_quotient_bcbsdm_middle_table_row_step_previous_right. bcf_previous_code_bcbsdm_middle_table = bcf_quotient_bcbsdm_middle_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsdm_middle_table_row_step))) * bcf_previous_scale_bcbsdm_middle_table) + (bcf_right_bcbsdm_middle_table_row_step))) /\ bcf_value_bcbsdm_middle_table_row_step = bcf_left_bcbsdm_middle_table_row_step + bcf_right_bcbsdm_middle_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsdm_middle_decoded_row_code. bcf_height_bcbsdm_middle_decoded_row_code + S (bcf_row_code_bcbsdm_middle) = S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_row_code. bcf_row_code_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_middle) + (bcf_row_code_bcbsdm_middle))) /\ ((((exists bcf_height_bcbsdm_middle_decoded_row_scale. bcf_height_bcbsdm_middle_decoded_row_scale + S (bcf_row_scale_bcbsdm_middle) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_row_scale. bcf_row_scale_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_middle) + (bcf_row_scale_bcbsdm_middle))) /\ (((exists bcf_height_bcbsdm_middle_decoded_value. bcf_height_bcbsdm_middle_decoded_value + S (m) = S ((S (n)) * bcf_row_scale_bcbsdm_middle)) /\ exists bcf_quotient_bcbsdm_middle_decoded_value. bcf_row_code_bcbsdm_middle = bcf_quotient_bcbsdm_middle_decoded_value * S ((S (n)) * bcf_row_scale_bcbsdm_middle) + (m)))))))))
  20. 0020specialize choose_exists (S (n + n))
  21. 0021specialize choose_exists n
  22. 0022exact choose_exists
  23. 0023cases hmiddle_exists
  24. 0024have hmirror_exists : ∃ r. Choose(S (n + n),S n,r)
    Exact native replay linehave hmirror_exists : exists r. (((exists bcf_lt_gap_bcbsdm_mirror_out_of_range. bcf_lt_gap_bcbsdm_mirror_out_of_range + S (S (n + n)) = S n) /\ r = 0) \/ ((exists bcf_le_gap_bcbsdm_mirror_in_range. bcf_le_gap_bcbsdm_mirror_in_range + (S n) = S (n + n)) /\ (exists bcf_row_code_code_bcbsdm_mirror bcf_row_code_scale_bcbsdm_mirror bcf_row_scale_code_bcbsdm_mirror bcf_row_scale_scale_bcbsdm_mirror bcf_row_code_bcbsdm_mirror bcf_row_scale_bcbsdm_mirror. ((forall bcf_row_index_bcbsdm_mirror_table. (exists bcf_lt_gap_bcbsdm_mirror_table_row_bound. bcf_lt_gap_bcbsdm_mirror_table_row_bound + S (bcf_row_index_bcbsdm_mirror_table) = S (S (n + n))) -> exists bcf_row_code_bcbsdm_mirror_table bcf_row_scale_bcbsdm_mirror_table. ((((exists bcf_height_bcbsdm_mirror_table_decoded_row_code. bcf_height_bcbsdm_mirror_table_decoded_row_code + S (bcf_row_code_bcbsdm_mirror_table) = S ((S (bcf_row_index_bcbsdm_mirror_table)) * bcf_row_code_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_table_decoded_row_code. bcf_row_code_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_table_decoded_row_code * S ((S (bcf_row_index_bcbsdm_mirror_table)) * bcf_row_code_scale_bcbsdm_mirror) + (bcf_row_code_bcbsdm_mirror_table))) /\ ((((exists bcf_height_bcbsdm_mirror_table_decoded_row_scale. bcf_height_bcbsdm_mirror_table_decoded_row_scale + S (bcf_row_scale_bcbsdm_mirror_table) = S ((S (bcf_row_index_bcbsdm_mirror_table)) * bcf_row_scale_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_table_decoded_row_scale. bcf_row_scale_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_table_decoded_row_scale * S ((S (bcf_row_index_bcbsdm_mirror_table)) * bcf_row_scale_scale_bcbsdm_mirror) + (bcf_row_scale_bcbsdm_mirror_table))) /\ ((bcf_row_index_bcbsdm_mirror_table = 0 /\ (forall bcf_index_bcbsdm_mirror_table_zero_row. (exists bcf_lt_gap_bcbsdm_mirror_table_zero_row_bound. bcf_lt_gap_bcbsdm_mirror_table_zero_row_bound + S (bcf_index_bcbsdm_mirror_table_zero_row) = S (S (n + n))) -> exists bcf_value_bcbsdm_mirror_table_zero_row. ((((exists bcf_height_bcbsdm_mirror_table_zero_row_entry. bcf_height_bcbsdm_mirror_table_zero_row_entry + S (bcf_value_bcbsdm_mirror_table_zero_row) = S ((S (bcf_index_bcbsdm_mirror_table_zero_row)) * bcf_row_scale_bcbsdm_mirror_table)) /\ exists bcf_quotient_bcbsdm_mirror_table_zero_row_entry. bcf_row_code_bcbsdm_mirror_table = bcf_quotient_bcbsdm_mirror_table_zero_row_entry * S ((S (bcf_index_bcbsdm_mirror_table_zero_row)) * bcf_row_scale_bcbsdm_mirror_table) + (bcf_value_bcbsdm_mirror_table_zero_row))) /\ ((bcf_index_bcbsdm_mirror_table_zero_row = 0 /\ bcf_value_bcbsdm_mirror_table_zero_row = 1) \/ exists bcf_predecessor_bcbsdm_mirror_table_zero_row. bcf_index_bcbsdm_mirror_table_zero_row = S bcf_predecessor_bcbsdm_mirror_table_zero_row /\ bcf_value_bcbsdm_mirror_table_zero_row = 0)))) \/ exists bcf_predecessor_bcbsdm_mirror_table bcf_previous_code_bcbsdm_mirror_table bcf_previous_scale_bcbsdm_mirror_table. bcf_row_index_bcbsdm_mirror_table = S bcf_predecessor_bcbsdm_mirror_table /\ ((((exists bcf_height_bcbsdm_mirror_table_decoded_previous_code. bcf_height_bcbsdm_mirror_table_decoded_previous_code + S (bcf_previous_code_bcbsdm_mirror_table) = S ((S (bcf_predecessor_bcbsdm_mirror_table)) * bcf_row_code_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_table_decoded_previous_code. bcf_row_code_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_table_decoded_previous_code * S ((S (bcf_predecessor_bcbsdm_mirror_table)) * bcf_row_code_scale_bcbsdm_mirror) + (bcf_previous_code_bcbsdm_mirror_table))) /\ ((((exists bcf_height_bcbsdm_mirror_table_decoded_previous_scale. bcf_height_bcbsdm_mirror_table_decoded_previous_scale + S (bcf_previous_scale_bcbsdm_mirror_table) = S ((S (bcf_predecessor_bcbsdm_mirror_table)) * bcf_row_scale_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_table_decoded_previous_scale. bcf_row_scale_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_table_decoded_previous_scale * S ((S (bcf_predecessor_bcbsdm_mirror_table)) * bcf_row_scale_scale_bcbsdm_mirror) + (bcf_previous_scale_bcbsdm_mirror_table))) /\ (forall bcf_index_bcbsdm_mirror_table_row_step. (exists bcf_lt_gap_bcbsdm_mirror_table_row_step_bound. bcf_lt_gap_bcbsdm_mirror_table_row_step_bound + S (bcf_index_bcbsdm_mirror_table_row_step) = S (S (n + n))) -> exists bcf_value_bcbsdm_mirror_table_row_step. ((((exists bcf_height_bcbsdm_mirror_table_row_step_entry. bcf_height_bcbsdm_mirror_table_row_step_entry + S (bcf_value_bcbsdm_mirror_table_row_step) = S ((S (bcf_index_bcbsdm_mirror_table_row_step)) * bcf_row_scale_bcbsdm_mirror_table)) /\ exists bcf_quotient_bcbsdm_mirror_table_row_step_entry. bcf_row_code_bcbsdm_mirror_table = bcf_quotient_bcbsdm_mirror_table_row_step_entry * S ((S (bcf_index_bcbsdm_mirror_table_row_step)) * bcf_row_scale_bcbsdm_mirror_table) + (bcf_value_bcbsdm_mirror_table_row_step))) /\ ((bcf_index_bcbsdm_mirror_table_row_step = 0 /\ bcf_value_bcbsdm_mirror_table_row_step = 1) \/ exists bcf_predecessor_bcbsdm_mirror_table_row_step bcf_left_bcbsdm_mirror_table_row_step bcf_right_bcbsdm_mirror_table_row_step. bcf_index_bcbsdm_mirror_table_row_step = S bcf_predecessor_bcbsdm_mirror_table_row_step /\ ((((exists bcf_height_bcbsdm_mirror_table_row_step_previous_left. bcf_height_bcbsdm_mirror_table_row_step_previous_left + S (bcf_left_bcbsdm_mirror_table_row_step) = S ((S (bcf_predecessor_bcbsdm_mirror_table_row_step)) * bcf_previous_scale_bcbsdm_mirror_table)) /\ exists bcf_quotient_bcbsdm_mirror_table_row_step_previous_left. bcf_previous_code_bcbsdm_mirror_table = bcf_quotient_bcbsdm_mirror_table_row_step_previous_left * S ((S (bcf_predecessor_bcbsdm_mirror_table_row_step)) * bcf_previous_scale_bcbsdm_mirror_table) + (bcf_left_bcbsdm_mirror_table_row_step))) /\ ((((exists bcf_height_bcbsdm_mirror_table_row_step_previous_right. bcf_height_bcbsdm_mirror_table_row_step_previous_right + S (bcf_right_bcbsdm_mirror_table_row_step) = S ((S (S (bcf_predecessor_bcbsdm_mirror_table_row_step))) * bcf_previous_scale_bcbsdm_mirror_table)) /\ exists bcf_quotient_bcbsdm_mirror_table_row_step_previous_right. bcf_previous_code_bcbsdm_mirror_table = bcf_quotient_bcbsdm_mirror_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcbsdm_mirror_table_row_step))) * bcf_previous_scale_bcbsdm_mirror_table) + (bcf_right_bcbsdm_mirror_table_row_step))) /\ bcf_value_bcbsdm_mirror_table_row_step = bcf_left_bcbsdm_mirror_table_row_step + bcf_right_bcbsdm_mirror_table_row_step))))))))))) /\ ((((exists bcf_height_bcbsdm_mirror_decoded_row_code. bcf_height_bcbsdm_mirror_decoded_row_code + S (bcf_row_code_bcbsdm_mirror) = S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_decoded_row_code. bcf_row_code_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_decoded_row_code * S ((S (S (n + n))) * bcf_row_code_scale_bcbsdm_mirror) + (bcf_row_code_bcbsdm_mirror))) /\ ((((exists bcf_height_bcbsdm_mirror_decoded_row_scale. bcf_height_bcbsdm_mirror_decoded_row_scale + S (bcf_row_scale_bcbsdm_mirror) = S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_decoded_row_scale. bcf_row_scale_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_decoded_row_scale * S ((S (S (n + n))) * bcf_row_scale_scale_bcbsdm_mirror) + (bcf_row_scale_bcbsdm_mirror))) /\ (((exists bcf_height_bcbsdm_mirror_decoded_value. bcf_height_bcbsdm_mirror_decoded_value + S (r) = S ((S (S n)) * bcf_row_scale_bcbsdm_mirror)) /\ exists bcf_quotient_bcbsdm_mirror_decoded_value. bcf_row_code_bcbsdm_mirror = bcf_quotient_bcbsdm_mirror_decoded_value * S ((S (S n)) * bcf_row_scale_bcbsdm_mirror) + (r)))))))))
  25. 0025specialize choose_exists (S (n + n))
  26. 0026specialize choose_exists (S n)
  27. 0027exact choose_exists
  28. 0028cases hmirror_exists
  29. 0029have hsym : x = x1
  30. 0030specialize choose_symmetry (S (n + n))
  31. 0031specialize choose_symmetry n
  32. 0032specialize choose_symmetry (S n)
  33. 0033specialize choose_symmetry x
  34. 0034specialize choose_symmetry x1
  35. 0035apply choose_symmetry
  36. 0036apply PA4
  37. 0037exact hmiddle_exists_witness
  38. 0038exact hmirror_exists_witness
  39. 0039have hsum : d = x + x1
  40. 0040specialize choose_succ_succ (S (n + n))
  41. 0041specialize choose_succ_succ n
  42. 0042specialize choose_succ_succ x
  43. 0043specialize choose_succ_succ x1
  44. 0044specialize choose_succ_succ d
  45. 0045apply choose_succ_succ
  46. 0046exact hmiddle_exists_witness
  47. 0047exact hmirror_exists_witness
  48. 0048exact hnormalized
  49. 0049exists x
  50. 0050split
  51. 0051exact hmiddle_exists_witness
  52. 0052trans x + x1
  53. 0053exact hsum
  54. 0054rewrite <- hsym
  55. 0055refl