BL0010

binary_length_successor_step

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A binary-length witness for n constructively produces one for S n.

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 first-order arithmetic statement

forall n l. ((((n) = 0 /\ (l) = 1) \/ exists ff_exponent_bl_length ff_lower_bl_length ff_upper_bl_length. (((l) = S ff_exponent_bl_length) /\ ((exists ff_positive_bl_length. ff_positive_bl_length + 1 = (n)) /\ ((exists pa_b_bl_length_lower pa_c_bl_length_lower. ((forall pa_i_bl_length_lower_repeat. (exists pa_lt_bl_length_lower_repeat_bound. pa_lt_bl_length_lower_repeat_bound + S pa_i_bl_length_lower_repeat = ff_exponent_bl_length) -> (((exists pa_h_bl_length_lower_repeat_decoded. pa_h_bl_length_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_length_lower_repeat)) * pa_c_bl_length_lower)) /\ exists pa_q_bl_length_lower_repeat_decoded. pa_b_bl_length_lower = pa_q_bl_length_lower_repeat_decoded * S ((S (pa_i_bl_length_lower_repeat)) * pa_c_bl_length_lower) + (2)))) /\ (exists pa_u_bl_length_lower_product pa_v_bl_length_lower_product. ((((exists pa_h_bl_length_lower_product_start. pa_h_bl_length_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_start. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_start * S ((S (0)) * pa_v_bl_length_lower_product) + (1))) /\ ((((exists pa_h_bl_length_lower_product_terminal. pa_h_bl_length_lower_product_terminal + S (ff_lower_bl_length) = S ((S (ff_exponent_bl_length)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_terminal. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_terminal * S ((S (ff_exponent_bl_length)) * pa_v_bl_length_lower_product) + (ff_lower_bl_length))) /\ forall pa_i_bl_length_lower_product. (exists pa_lt_bl_length_lower_product_bound. pa_lt_bl_length_lower_product_bound + S pa_i_bl_length_lower_product = ff_exponent_bl_length) -> exists pa_p_bl_length_lower_product pa_r_bl_length_lower_product pa_s_bl_length_lower_product. ((((exists pa_h_bl_length_lower_product_factor. pa_h_bl_length_lower_product_factor + S (pa_p_bl_length_lower_product) = S ((S (pa_i_bl_length_lower_product)) * pa_c_bl_length_lower)) /\ exists pa_q_bl_length_lower_product_factor. pa_b_bl_length_lower = pa_q_bl_length_lower_product_factor * S ((S (pa_i_bl_length_lower_product)) * pa_c_bl_length_lower) + (pa_p_bl_length_lower_product))) /\ ((((exists pa_h_bl_length_lower_product_partial. pa_h_bl_length_lower_product_partial + S (pa_r_bl_length_lower_product) = S ((S (pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_partial. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_partial * S ((S (pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product) + (pa_r_bl_length_lower_product))) /\ ((((exists pa_h_bl_length_lower_product_successor. pa_h_bl_length_lower_product_successor + S (pa_s_bl_length_lower_product) = S ((S (S pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product)) /\ exists pa_q_bl_length_lower_product_successor. pa_u_bl_length_lower_product = pa_q_bl_length_lower_product_successor * S ((S (S pa_i_bl_length_lower_product)) * pa_v_bl_length_lower_product) + (pa_s_bl_length_lower_product))) /\ pa_s_bl_length_lower_product = pa_r_bl_length_lower_product * pa_p_bl_length_lower_product)))))))) /\ ((exists pa_b_bl_length_upper pa_c_bl_length_upper. ((forall pa_i_bl_length_upper_repeat. (exists pa_lt_bl_length_upper_repeat_bound. pa_lt_bl_length_upper_repeat_bound + S pa_i_bl_length_upper_repeat = l) -> (((exists pa_h_bl_length_upper_repeat_decoded. pa_h_bl_length_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_length_upper_repeat)) * pa_c_bl_length_upper)) /\ exists pa_q_bl_length_upper_repeat_decoded. pa_b_bl_length_upper = pa_q_bl_length_upper_repeat_decoded * S ((S (pa_i_bl_length_upper_repeat)) * pa_c_bl_length_upper) + (2)))) /\ (exists pa_u_bl_length_upper_product pa_v_bl_length_upper_product. ((((exists pa_h_bl_length_upper_product_start. pa_h_bl_length_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_start. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_start * S ((S (0)) * pa_v_bl_length_upper_product) + (1))) /\ ((((exists pa_h_bl_length_upper_product_terminal. pa_h_bl_length_upper_product_terminal + S (ff_upper_bl_length) = S ((S (l)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_terminal. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_terminal * S ((S (l)) * pa_v_bl_length_upper_product) + (ff_upper_bl_length))) /\ forall pa_i_bl_length_upper_product. (exists pa_lt_bl_length_upper_product_bound. pa_lt_bl_length_upper_product_bound + S pa_i_bl_length_upper_product = l) -> exists pa_p_bl_length_upper_product pa_r_bl_length_upper_product pa_s_bl_length_upper_product. ((((exists pa_h_bl_length_upper_product_factor. pa_h_bl_length_upper_product_factor + S (pa_p_bl_length_upper_product) = S ((S (pa_i_bl_length_upper_product)) * pa_c_bl_length_upper)) /\ exists pa_q_bl_length_upper_product_factor. pa_b_bl_length_upper = pa_q_bl_length_upper_product_factor * S ((S (pa_i_bl_length_upper_product)) * pa_c_bl_length_upper) + (pa_p_bl_length_upper_product))) /\ ((((exists pa_h_bl_length_upper_product_partial. pa_h_bl_length_upper_product_partial + S (pa_r_bl_length_upper_product) = S ((S (pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_partial. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_partial * S ((S (pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product) + (pa_r_bl_length_upper_product))) /\ ((((exists pa_h_bl_length_upper_product_successor. pa_h_bl_length_upper_product_successor + S (pa_s_bl_length_upper_product) = S ((S (S pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product)) /\ exists pa_q_bl_length_upper_product_successor. pa_u_bl_length_upper_product = pa_q_bl_length_upper_product_successor * S ((S (S pa_i_bl_length_upper_product)) * pa_v_bl_length_upper_product) + (pa_s_bl_length_upper_product))) /\ pa_s_bl_length_upper_product = pa_r_bl_length_upper_product * pa_p_bl_length_upper_product)))))))) /\ ((exists ff_lower_gap_bl_length. ff_lower_gap_bl_length + (ff_lower_bl_length) = (n)) /\ (exists ff_upper_gap_bl_length. ff_upper_gap_bl_length + S (n) = (ff_upper_bl_length))))))))) -> exists L. ((((S n) = 0 /\ (L) = 1) \/ exists ff_exponent_bl_successor ff_lower_bl_successor ff_upper_bl_successor. (((L) = S ff_exponent_bl_successor) /\ ((exists ff_positive_bl_successor. ff_positive_bl_successor + 1 = (S n)) /\ ((exists pa_b_bl_successor_lower pa_c_bl_successor_lower. ((forall pa_i_bl_successor_lower_repeat. (exists pa_lt_bl_successor_lower_repeat_bound. pa_lt_bl_successor_lower_repeat_bound + S pa_i_bl_successor_lower_repeat = ff_exponent_bl_successor) -> (((exists pa_h_bl_successor_lower_repeat_decoded. pa_h_bl_successor_lower_repeat_decoded + S (2) = S ((S (pa_i_bl_successor_lower_repeat)) * pa_c_bl_successor_lower)) /\ exists pa_q_bl_successor_lower_repeat_decoded. pa_b_bl_successor_lower = pa_q_bl_successor_lower_repeat_decoded * S ((S (pa_i_bl_successor_lower_repeat)) * pa_c_bl_successor_lower) + (2)))) /\ (exists pa_u_bl_successor_lower_product pa_v_bl_successor_lower_product. ((((exists pa_h_bl_successor_lower_product_start. pa_h_bl_successor_lower_product_start + S (1) = S ((S (0)) * pa_v_bl_successor_lower_product)) /\ exists pa_q_bl_successor_lower_product_start. pa_u_bl_successor_lower_product = pa_q_bl_successor_lower_product_start * S ((S (0)) * pa_v_bl_successor_lower_product) + (1))) /\ ((((exists pa_h_bl_successor_lower_product_terminal. pa_h_bl_successor_lower_product_terminal + S (ff_lower_bl_successor) = S ((S (ff_exponent_bl_successor)) * pa_v_bl_successor_lower_product)) /\ exists pa_q_bl_successor_lower_product_terminal. pa_u_bl_successor_lower_product = pa_q_bl_successor_lower_product_terminal * S ((S (ff_exponent_bl_successor)) * pa_v_bl_successor_lower_product) + (ff_lower_bl_successor))) /\ forall pa_i_bl_successor_lower_product. (exists pa_lt_bl_successor_lower_product_bound. pa_lt_bl_successor_lower_product_bound + S pa_i_bl_successor_lower_product = ff_exponent_bl_successor) -> exists pa_p_bl_successor_lower_product pa_r_bl_successor_lower_product pa_s_bl_successor_lower_product. ((((exists pa_h_bl_successor_lower_product_factor. pa_h_bl_successor_lower_product_factor + S (pa_p_bl_successor_lower_product) = S ((S (pa_i_bl_successor_lower_product)) * pa_c_bl_successor_lower)) /\ exists pa_q_bl_successor_lower_product_factor. pa_b_bl_successor_lower = pa_q_bl_successor_lower_product_factor * S ((S (pa_i_bl_successor_lower_product)) * pa_c_bl_successor_lower) + (pa_p_bl_successor_lower_product))) /\ ((((exists pa_h_bl_successor_lower_product_partial. pa_h_bl_successor_lower_product_partial + S (pa_r_bl_successor_lower_product) = S ((S (pa_i_bl_successor_lower_product)) * pa_v_bl_successor_lower_product)) /\ exists pa_q_bl_successor_lower_product_partial. pa_u_bl_successor_lower_product = pa_q_bl_successor_lower_product_partial * S ((S (pa_i_bl_successor_lower_product)) * pa_v_bl_successor_lower_product) + (pa_r_bl_successor_lower_product))) /\ ((((exists pa_h_bl_successor_lower_product_successor. pa_h_bl_successor_lower_product_successor + S (pa_s_bl_successor_lower_product) = S ((S (S pa_i_bl_successor_lower_product)) * pa_v_bl_successor_lower_product)) /\ exists pa_q_bl_successor_lower_product_successor. pa_u_bl_successor_lower_product = pa_q_bl_successor_lower_product_successor * S ((S (S pa_i_bl_successor_lower_product)) * pa_v_bl_successor_lower_product) + (pa_s_bl_successor_lower_product))) /\ pa_s_bl_successor_lower_product = pa_r_bl_successor_lower_product * pa_p_bl_successor_lower_product)))))))) /\ ((exists pa_b_bl_successor_upper pa_c_bl_successor_upper. ((forall pa_i_bl_successor_upper_repeat. (exists pa_lt_bl_successor_upper_repeat_bound. pa_lt_bl_successor_upper_repeat_bound + S pa_i_bl_successor_upper_repeat = L) -> (((exists pa_h_bl_successor_upper_repeat_decoded. pa_h_bl_successor_upper_repeat_decoded + S (2) = S ((S (pa_i_bl_successor_upper_repeat)) * pa_c_bl_successor_upper)) /\ exists pa_q_bl_successor_upper_repeat_decoded. pa_b_bl_successor_upper = pa_q_bl_successor_upper_repeat_decoded * S ((S (pa_i_bl_successor_upper_repeat)) * pa_c_bl_successor_upper) + (2)))) /\ (exists pa_u_bl_successor_upper_product pa_v_bl_successor_upper_product. ((((exists pa_h_bl_successor_upper_product_start. pa_h_bl_successor_upper_product_start + S (1) = S ((S (0)) * pa_v_bl_successor_upper_product)) /\ exists pa_q_bl_successor_upper_product_start. pa_u_bl_successor_upper_product = pa_q_bl_successor_upper_product_start * S ((S (0)) * pa_v_bl_successor_upper_product) + (1))) /\ ((((exists pa_h_bl_successor_upper_product_terminal. pa_h_bl_successor_upper_product_terminal + S (ff_upper_bl_successor) = S ((S (L)) * pa_v_bl_successor_upper_product)) /\ exists pa_q_bl_successor_upper_product_terminal. pa_u_bl_successor_upper_product = pa_q_bl_successor_upper_product_terminal * S ((S (L)) * pa_v_bl_successor_upper_product) + (ff_upper_bl_successor))) /\ forall pa_i_bl_successor_upper_product. (exists pa_lt_bl_successor_upper_product_bound. pa_lt_bl_successor_upper_product_bound + S pa_i_bl_successor_upper_product = L) -> exists pa_p_bl_successor_upper_product pa_r_bl_successor_upper_product pa_s_bl_successor_upper_product. ((((exists pa_h_bl_successor_upper_product_factor. pa_h_bl_successor_upper_product_factor + S (pa_p_bl_successor_upper_product) = S ((S (pa_i_bl_successor_upper_product)) * pa_c_bl_successor_upper)) /\ exists pa_q_bl_successor_upper_product_factor. pa_b_bl_successor_upper = pa_q_bl_successor_upper_product_factor * S ((S (pa_i_bl_successor_upper_product)) * pa_c_bl_successor_upper) + (pa_p_bl_successor_upper_product))) /\ ((((exists pa_h_bl_successor_upper_product_partial. pa_h_bl_successor_upper_product_partial + S (pa_r_bl_successor_upper_product) = S ((S (pa_i_bl_successor_upper_product)) * pa_v_bl_successor_upper_product)) /\ exists pa_q_bl_successor_upper_product_partial. pa_u_bl_successor_upper_product = pa_q_bl_successor_upper_product_partial * S ((S (pa_i_bl_successor_upper_product)) * pa_v_bl_successor_upper_product) + (pa_r_bl_successor_upper_product))) /\ ((((exists pa_h_bl_successor_upper_product_successor. pa_h_bl_successor_upper_product_successor + S (pa_s_bl_successor_upper_product) = S ((S (S pa_i_bl_successor_upper_product)) * pa_v_bl_successor_upper_product)) /\ exists pa_q_bl_successor_upper_product_successor. pa_u_bl_successor_upper_product = pa_q_bl_successor_upper_product_successor * S ((S (S pa_i_bl_successor_upper_product)) * pa_v_bl_successor_upper_product) + (pa_s_bl_successor_upper_product))) /\ pa_s_bl_successor_upper_product = pa_r_bl_successor_upper_product * pa_p_bl_successor_upper_product)))))))) /\ ((exists ff_lower_gap_bl_successor. ff_lower_gap_bl_successor + (ff_lower_bl_successor) = (S n)) /\ (exists ff_upper_gap_bl_successor. ff_upper_gap_bl_successor + S (S n) = (ff_upper_bl_successor)))))))))

Constructive proof overview

Generated structural guide

A binary-length witness for n constructively produces one for S n.

The unchanged tactic script uses 6 declared prerequisites and contains 75 exact native proof lines.

Alpha v34 checked-use · first admitted v22 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BL000E binary_length_one BL0005 binary_power_two_exists BL000A binary_power_two_strict_growth le_eq_or_lt Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized

Direct dependents

BL0011 binary_length_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

75 script commands · 42 reading checkpoints · 3 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 (3)
binary length onebinary power two existsbinary power two strict growth

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 l
  3. L3
    intro hlength
02Separate the logical casesL4–5

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

  1. L4
    cases hlength
  2. L5
    cases hlength_left
03Construct an explicit witnessL6–6

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

  1. L6
    exists 1
04Calculate and transport equalitiesL7–10

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

  1. L7
    rewrite hlength_left_left
  2. L8
    rewrite hlength_left_left
  3. L9
    rewrite hlength_left_left
  4. L10
    rewrite hlength_left_left
05Use earlier factsL11–11

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

  1. L11
    exact binary_length_one
06Separate the logical casesL12–19

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

  1. L12
    cases hlength_right
  2. L13
    cases hlength_right_witness
  3. L14
    cases hlength_right_witness_witness
  4. L15
    cases hlength_right_witness_witness_witness
  5. L16
    cases hlength_right_witness_witness_witness_right
  6. L17
    cases hlength_right_witness_witness_witness_right_right
  7. L18
    cases hlength_right_witness_witness_witness_right_right_right
  8. L19
    cases hlength_right_witness_witness_witness_right_right_right_right
07Establish hcasesL20–24

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

  1. L20
    have hcases : S n = x2 \/ exists gap. gap + S (S n) = x2
  2. L21
    specialize le_eq_or_lt (S n)
  3. L22
    specialize le_eq_or_lt x2
  4. L23
    apply le_eq_or_lt
  5. L24
    exact hlength_right_witness_witness_witness_right_right_right_right_right
08Separate the logical casesL25–25

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

  1. L25
    cases hcases
09Establish hnextL26–28

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

  1. L26
    have hnext : ∃ q. PowTwo(S l,q)Definitions: PowTwo
  2. L27
    specialize binary_power_two_exists (S l)
  3. L28
    exact binary_power_two_exists
10Separate the logical casesL29–29

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

  1. L29
    cases hnext
11Establish hstrictL30–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary power two strict growth.

  1. L30
    have hstrict : exists gap. gap + S x2 = x3
  2. L31
    specialize binary_power_two_strict_growth l
  3. L32
    specialize binary_power_two_strict_growth x2
  4. L33
    specialize binary_power_two_strict_growth x3
  5. L34
    apply binary_power_two_strict_growth
  6. L35
    exact hlength_right_witness_witness_witness_right_right_right_left
  7. L36
    exact hnext_witness
12Construct an explicit witnessL37–37

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

  1. L37
    exists S l
13Separate the logical casesL38–38

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

  1. L38
    right
14Construct an explicit witnessL39–41

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

  1. L39
    exists l
  2. L40
    exists x2
  3. L41
    exists x3
15Separate the logical casesL42–42

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

  1. L42
    split
16Calculate and transport equalitiesL43–43

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

  1. L43
    refl
17Separate the logical casesL44–44

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

  1. L44
    split
18Construct an explicit witnessL45–45

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

  1. L45
    exists n
19Calculate and transport equalitiesL46–46

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

  1. L46
    simp
20Separate the logical casesL47–47

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

  1. L47
    split
21Use earlier factsL48–48

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

  1. L48
    exact hlength_right_witness_witness_witness_right_right_right_left
22Separate the logical casesL49–49

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

  1. L49
    split
23Use earlier factsL50–50

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

  1. L50
    exact hnext_witness
24Separate the logical casesL51–51

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

  1. L51
    split
25Calculate and transport equalitiesL52–52

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

  1. L52
    rewrite hcases_left
26Use earlier factsL53–53

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

  1. L53
    apply le_refl
27Calculate and transport equalitiesL54–54

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

  1. L54
    rewrite hcases_left
28Use earlier factsL55–55

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

  1. L55
    exact hstrict
29Construct an explicit witnessL56–56

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

  1. L56
    exists l
30Separate the logical casesL57–57

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

  1. L57
    right
31Construct an explicit witnessL58–60

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

  1. L58
    exists x
  2. L59
    exists x1
  3. L60
    exists x2
32Separate the logical casesL61–61

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

  1. L61
    split
33Use earlier factsL62–62

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

  1. L62
    exact hlength_right_witness_witness_witness_left
34Separate the logical casesL63–63

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

  1. L63
    split
35Construct an explicit witnessL64–64

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

  1. L64
    exists n
36Calculate and transport equalitiesL65–65

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

  1. L65
    simp
37Separate the logical casesL66–66

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

  1. L66
    split
38Use earlier factsL67–67

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

  1. L67
    exact hlength_right_witness_witness_witness_right_right_left
39Separate the logical casesL68–68

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

  1. L68
    split
40Use earlier factsL69–69

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

  1. L69
    exact hlength_right_witness_witness_witness_right_right_right_left
41Separate the logical casesL70–70

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

  1. L70
    split
42Use earlier factsL71–75

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

  1. L71
    specialize le_succ x1
  2. L72
    specialize le_succ n
  3. L73
    apply le_succ
  4. L74
    exact hlength_right_witness_witness_witness_right_right_right_right_left
  5. L75
    exact hcases_right

Library-wide reading audit

Original exact command ledger · 75 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003intro hlength
  4. 0004cases hlength
  5. 0005cases hlength_left
  6. 0006exists 1
  7. 0007rewrite hlength_left_left
  8. 0008rewrite hlength_left_left
  9. 0009rewrite hlength_left_left
  10. 0010rewrite hlength_left_left
  11. 0011exact binary_length_one
  12. 0012cases hlength_right
  13. 0013cases hlength_right_witness
  14. 0014cases hlength_right_witness_witness
  15. 0015cases hlength_right_witness_witness_witness
  16. 0016cases hlength_right_witness_witness_witness_right
  17. 0017cases hlength_right_witness_witness_witness_right_right
  18. 0018cases hlength_right_witness_witness_witness_right_right_right
  19. 0019cases hlength_right_witness_witness_witness_right_right_right_right
  20. 0020have hcases : S n = x2 \/ exists gap. gap + S (S n) = x2
  21. 0021specialize le_eq_or_lt (S n)
  22. 0022specialize le_eq_or_lt x2
  23. 0023apply le_eq_or_lt
  24. 0024exact hlength_right_witness_witness_witness_right_right_right_right_right
  25. 0025cases hcases
  26. 0026have hnext : exists q. (exists pa_b_bl_successor_next pa_c_bl_successor_next. ((forall pa_i_bl_successor_next_repeat. (exists pa_lt_bl_successor_next_repeat_bound. pa_lt_bl_successor_next_repeat_bound + S pa_i_bl_successor_next_repeat = S l) -> (((exists pa_h_bl_successor_next_repeat_decoded. pa_h_bl_successor_next_repeat_decoded + S (2) = S ((S (pa_i_bl_successor_next_repeat)) * pa_c_bl_successor_next)) /\ exists pa_q_bl_successor_next_repeat_decoded. pa_b_bl_successor_next = pa_q_bl_successor_next_repeat_decoded * S ((S (pa_i_bl_successor_next_repeat)) * pa_c_bl_successor_next) + (2)))) /\ (exists pa_u_bl_successor_next_product pa_v_bl_successor_next_product. ((((exists pa_h_bl_successor_next_product_start. pa_h_bl_successor_next_product_start + S (1) = S ((S (0)) * pa_v_bl_successor_next_product)) /\ exists pa_q_bl_successor_next_product_start. pa_u_bl_successor_next_product = pa_q_bl_successor_next_product_start * S ((S (0)) * pa_v_bl_successor_next_product) + (1))) /\ ((((exists pa_h_bl_successor_next_product_terminal. pa_h_bl_successor_next_product_terminal + S (q) = S ((S (S l)) * pa_v_bl_successor_next_product)) /\ exists pa_q_bl_successor_next_product_terminal. pa_u_bl_successor_next_product = pa_q_bl_successor_next_product_terminal * S ((S (S l)) * pa_v_bl_successor_next_product) + (q))) /\ forall pa_i_bl_successor_next_product. (exists pa_lt_bl_successor_next_product_bound. pa_lt_bl_successor_next_product_bound + S pa_i_bl_successor_next_product = S l) -> exists pa_p_bl_successor_next_product pa_r_bl_successor_next_product pa_s_bl_successor_next_product. ((((exists pa_h_bl_successor_next_product_factor. pa_h_bl_successor_next_product_factor + S (pa_p_bl_successor_next_product) = S ((S (pa_i_bl_successor_next_product)) * pa_c_bl_successor_next)) /\ exists pa_q_bl_successor_next_product_factor. pa_b_bl_successor_next = pa_q_bl_successor_next_product_factor * S ((S (pa_i_bl_successor_next_product)) * pa_c_bl_successor_next) + (pa_p_bl_successor_next_product))) /\ ((((exists pa_h_bl_successor_next_product_partial. pa_h_bl_successor_next_product_partial + S (pa_r_bl_successor_next_product) = S ((S (pa_i_bl_successor_next_product)) * pa_v_bl_successor_next_product)) /\ exists pa_q_bl_successor_next_product_partial. pa_u_bl_successor_next_product = pa_q_bl_successor_next_product_partial * S ((S (pa_i_bl_successor_next_product)) * pa_v_bl_successor_next_product) + (pa_r_bl_successor_next_product))) /\ ((((exists pa_h_bl_successor_next_product_successor. pa_h_bl_successor_next_product_successor + S (pa_s_bl_successor_next_product) = S ((S (S pa_i_bl_successor_next_product)) * pa_v_bl_successor_next_product)) /\ exists pa_q_bl_successor_next_product_successor. pa_u_bl_successor_next_product = pa_q_bl_successor_next_product_successor * S ((S (S pa_i_bl_successor_next_product)) * pa_v_bl_successor_next_product) + (pa_s_bl_successor_next_product))) /\ pa_s_bl_successor_next_product = pa_r_bl_successor_next_product * pa_p_bl_successor_next_product))))))))
  27. 0027specialize binary_power_two_exists (S l)
  28. 0028exact binary_power_two_exists
  29. 0029cases hnext
  30. 0030have hstrict : exists gap. gap + S x2 = x3
  31. 0031specialize binary_power_two_strict_growth l
  32. 0032specialize binary_power_two_strict_growth x2
  33. 0033specialize binary_power_two_strict_growth x3
  34. 0034apply binary_power_two_strict_growth
  35. 0035exact hlength_right_witness_witness_witness_right_right_right_left
  36. 0036exact hnext_witness
  37. 0037exists S l
  38. 0038right
  39. 0039exists l
  40. 0040exists x2
  41. 0041exists x3
  42. 0042split
  43. 0043refl
  44. 0044split
  45. 0045exists n
  46. 0046simp
  47. 0047split
  48. 0048exact hlength_right_witness_witness_witness_right_right_right_left
  49. 0049split
  50. 0050exact hnext_witness
  51. 0051split
  52. 0052rewrite hcases_left
  53. 0053apply le_refl
  54. 0054rewrite hcases_left
  55. 0055exact hstrict
  56. 0056exists l
  57. 0057right
  58. 0058exists x
  59. 0059exists x1
  60. 0060exists x2
  61. 0061split
  62. 0062exact hlength_right_witness_witness_witness_left
  63. 0063split
  64. 0064exists n
  65. 0065simp
  66. 0066split
  67. 0067exact hlength_right_witness_witness_witness_right_right_left
  68. 0068split
  69. 0069exact hlength_right_witness_witness_witness_right_right_right_left
  70. 0070split
  71. 0071specialize le_succ x1
  72. 0072specialize le_succ n
  73. 0073apply le_succ
  74. 0074exact hlength_right_witness_witness_witness_right_right_right_right_left
  75. 0075exact hcases_right