BT00TS

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.

Exact expanded 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)

Structural proof guide

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

Direct prerequisites: add_succ_left, choose_exists, choose_symmetry, choose_succ_succ, choose_upper_eq_transport. The authored body proceeds by case analysis (2), intermediate claims (6), equality transport (1).

Proof neighborhood

Direct dependencies

BT0001 add_succ_left BT00T8 choose_exists BT00TL choose_symmetry BT00TJ choose_succ_succ BT00TR choose_upper_eq_transport

Direct dependents

BT00TU central_binom_succ_recurrence BT00VL central_binom_recurrence_double_bundle

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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.

Named ingredients (5)
add succ leftchoose existschoose symmetrychoose succ succchoose upper eq transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
  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
  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 exact 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 : ((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 : 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 : 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