CD0013

finite_bit_complement_exists

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

Construct the genuine characteristic complement and prove its count adds to the ambient size.

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 b c l n. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> exists d e m. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ ((forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * c)) /\ exists fs_q_fms_complement_a. b = fs_q_fms_complement_a * S ((S (fms_i_complement)) * c) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * e)) /\ exists fs_q_fms_complement_b. d = fs_q_fms_complement_b * S ((S (fms_i_complement)) * e) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))) /\ n+m=l)

Constructive proof overview

Generated structural guide

Construct the genuine characteristic complement and prove its count adds to the ambient size.

The unchanged tactic script uses 5 declared prerequisites and contains 106 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sign_factor_prefix_exists Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized bit_count_exists Stable theorem; checked-use authorized complementary_bit_counts_add_length Alpha theorem; checked-use authorized

Direct dependents

CD0016 finite_bit_union_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

106 script commands · 33 reading checkpoints · 7 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.

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–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hn
02Establish hcodeL6–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sign factor prefix exists.

  1. L6
    have hcode : ∃ d. ∃ e. ∀ fms_i_sign. ∀ fms_a_sign. Lt(fms_i_sign,l) → BetaAt(b,c,fms_i_sign,fms_a_sign) → fms_a_sign = 0 ∧ BetaAt(d,e,fms_i_sign,1) ∨ fms_a_sign = 1 ∧ BetaAt(d,e,fms_i_sign,0)Definitions: LtBetaAt
  2. L7
    specialize beta_sign_factor_prefix_exists b
  3. L8
    specialize beta_sign_factor_prefix_exists c
  4. L9
    specialize beta_sign_factor_prefix_exists 0
  5. L10
    specialize beta_sign_factor_prefix_exists l
  6. L11
    specialize beta_sign_factor_prefix_exists n
  7. L12
    apply beta_sign_factor_prefix_exists
  8. L13
    exact hn
03Separate the logical casesL14–15

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

  1. L14
    cases hcode
  2. L15
    cases hcode_witness
04Establish hbitsL16–18

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

  1. L16
    have hbits : forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (l)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (x1))) /\ exists ff_q_fms_bits_decoded. (x) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (x1)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))
  2. L17
    intro i
  3. L18
    intro hi
05Establish haL19–23

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

  1. L19
    have ha : exists a. ((exists fs_h_fms_comp_source. fs_h_fms_comp_source + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_comp_source. b = fs_q_fms_comp_source * S ((S (i)) * c) + (a))
  2. L20
    specialize beta_at_exists b
  3. L21
    specialize beta_at_exists c
  4. L22
    specialize beta_at_exists i
  5. L23
    apply beta_at_exists
06Separate the logical casesL24–24

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

  1. L24
    cases ha
07Establish hcL25–30

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

  1. L25
    have hc : (x2=0 /\ (((exists fs_h_fms_comp_one. fs_h_fms_comp_one + S (1) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_one. x = fs_q_fms_comp_one * S ((S (i)) * x1) + (1)))) \/ (x2=1 /\ (((exists fs_h_fms_comp_zero. fs_h_fms_comp_zero + S (0) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_zero. x = fs_q_fms_comp_zero * S ((S (i)) * x1) + (0))))
  2. L26
    specialize hcode_witness_witness i
  3. L27
    specialize hcode_witness_witness x2
  4. L28
    apply hcode_witness_witness
  5. L29
    exact hi
  6. L30
    exact ha_witness
08Separate the logical casesL31–32

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

  1. L31
    cases hc
  2. L32
    cases hc_left
09Construct an explicit witnessL33–33

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

  1. L33
    exists 1
10Separate the logical casesL34–34

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

  1. L34
    split
11Use earlier factsL35–35

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

  1. L35
    exact hc_left_right
12Separate the logical casesL36–36

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

  1. L36
    right
13Calculate and transport equalitiesL37–37

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

  1. L37
    refl
14Separate the logical casesL38–38

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

  1. L38
    cases hc_right
15Construct an explicit witnessL39–39

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

  1. L39
    exists 0
16Separate the logical casesL40–40

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

  1. L40
    split
17Use earlier factsL41–41

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

  1. L41
    exact hc_right_right
18Separate the logical casesL42–42

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

  1. L42
    left
19Calculate and transport equalitiesL43–43

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

  1. L43
    refl
20Establish hcompL44–50

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

  1. L44
    have hcomp : ∀ fms_i_complement. ∀ fms_a_complement. ∀ fms_v_complement. Lt(fms_i_complement,l) → BetaAt(b,c,fms_i_complement,fms_a_complement) → BetaAt(x,x1,fms_i_complement,fms_v_complement) → fms_a_complement = 0 ∧ fms_v_complement = 1 ∨ fms_a_complement = 1 ∧ fms_v_complement = 0Definitions: LtBetaAt
  2. L45
    intro i
  3. L46
    intro a
  4. L47
    intro v
  5. L48
    intro hi
  6. L49
    intro ha
  7. L50
    intro hv
21Establish hcL51–56

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

  1. L51
    have hc : (a=0 /\ (((exists fs_h_fms_comp_univ_one. fs_h_fms_comp_univ_one + S (1) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_univ_one. x = fs_q_fms_comp_univ_one * S ((S (i)) * x1) + (1)))) \/ (a=1 /\ (((exists fs_h_fms_comp_univ_zero. fs_h_fms_comp_univ_zero + S (0) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_univ_zero. x = fs_q_fms_comp_univ_zero * S ((S (i)) * x1) + (0))))
  2. L52
    specialize hcode_witness_witness i
  3. L53
    specialize hcode_witness_witness a
  4. L54
    apply hcode_witness_witness
  5. L55
    exact hi
  6. L56
    exact ha
22Separate the logical casesL57–60

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

  1. L57
    cases hc
  2. L58
    cases hc_left
  3. L59
    left
  4. L60
    split
23Use earlier factsL61–69

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

  1. L61
    exact hc_left_left
  2. L62
    specialize beta_at_unique x
  3. L63
    specialize beta_at_unique x1
  4. L64
    specialize beta_at_unique i
  5. L65
    specialize beta_at_unique v
  6. L66
    specialize beta_at_unique 1
  7. L67
    apply beta_at_unique
  8. L68
    exact hv
  9. L69
    exact hc_left_right
24Separate the logical casesL70–72

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

  1. L70
    cases hc_right
  2. L71
    right
  3. L72
    split
25Use earlier factsL73–81

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

  1. L73
    exact hc_right_left
  2. L74
    specialize beta_at_unique x
  3. L75
    specialize beta_at_unique x1
  4. L76
    specialize beta_at_unique i
  5. L77
    specialize beta_at_unique v
  6. L78
    specialize beta_at_unique 0
  7. L79
    apply beta_at_unique
  8. L80
    exact hv
  9. L81
    exact hc_right_right
26Establish hcountL82–87

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

  1. L82
    have hcount : ∃ m. BitCount(x,x1,l,m)Definitions: BitCount
  2. L83
    specialize bit_count_exists x
  3. L84
    specialize bit_count_exists x1
  4. L85
    specialize bit_count_exists l
  5. L86
    apply bit_count_exists
  6. L87
    exact hbits
27Separate the logical casesL88–88

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

  1. L88
    cases hcount
28Construct an explicit witnessL89–91

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

  1. L89
    exists x
  2. L90
    exists x1
  3. L91
    exists x2
29Separate the logical casesL92–92

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

  1. L92
    split
30Use earlier factsL93–93

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

  1. L93
    exact hcount_witness
31Separate the logical casesL94–94

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

  1. L94
    split
32Use earlier factsL95–104

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

  1. L95
    exact hcomp
  2. L96
    specialize complementary_bit_counts_add_length b
  3. L97
    specialize complementary_bit_counts_add_length c
  4. L98
    specialize complementary_bit_counts_add_length x
  5. L99
    specialize complementary_bit_counts_add_length x1
  6. L100
    specialize complementary_bit_counts_add_length l
  7. L101
    specialize complementary_bit_counts_add_length n
  8. L102
    specialize complementary_bit_counts_add_length x2
  9. L103
    apply complementary_bit_counts_add_length
  10. L104
    exact hn
33Use earlier factsL105–106

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

  1. L105
    exact hcount_witness
  2. L106
    exact hcomp

Library-wide reading audit

Original exact command ledger · 106 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hn
  6. 0006have hcode : exists d e. forall fms_i_sign fms_a_sign. (exists fms_gap_sign. fms_gap_sign + S (fms_i_sign) = (l)) -> (((exists fs_h_fms_sign_a. fs_h_fms_sign_a + S (fms_a_sign) = S ((S (fms_i_sign)) * c)) /\ exists fs_q_fms_sign_a. b = fs_q_fms_sign_a * S ((S (fms_i_sign)) * c) + (fms_a_sign))) -> ((fms_a_sign=0 /\ (((exists fs_h_fms_sign_one. fs_h_fms_sign_one + S (1) = S ((S (fms_i_sign)) * e)) /\ exists fs_q_fms_sign_one. d = fs_q_fms_sign_one * S ((S (fms_i_sign)) * e) + (1)))) \/ (fms_a_sign=1 /\ (((exists fs_h_fms_sign_zero. fs_h_fms_sign_zero + S (0) = S ((S (fms_i_sign)) * e)) /\ exists fs_q_fms_sign_zero. d = fs_q_fms_sign_zero * S ((S (fms_i_sign)) * e) + (0)))))
  7. 0007specialize beta_sign_factor_prefix_exists b
  8. 0008specialize beta_sign_factor_prefix_exists c
  9. 0009specialize beta_sign_factor_prefix_exists 0
  10. 0010specialize beta_sign_factor_prefix_exists l
  11. 0011specialize beta_sign_factor_prefix_exists n
  12. 0012apply beta_sign_factor_prefix_exists
  13. 0013exact hn
  14. 0014cases hcode
  15. 0015cases hcode_witness
  16. 0016have hbits : forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (l)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (x1))) /\ exists ff_q_fms_bits_decoded. (x) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (x1)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))
  17. 0017intro i
  18. 0018intro hi
  19. 0019have ha : exists a. ((exists fs_h_fms_comp_source. fs_h_fms_comp_source + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_comp_source. b = fs_q_fms_comp_source * S ((S (i)) * c) + (a))
  20. 0020specialize beta_at_exists b
  21. 0021specialize beta_at_exists c
  22. 0022specialize beta_at_exists i
  23. 0023apply beta_at_exists
  24. 0024cases ha
  25. 0025have hc : (x2=0 /\ (((exists fs_h_fms_comp_one. fs_h_fms_comp_one + S (1) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_one. x = fs_q_fms_comp_one * S ((S (i)) * x1) + (1)))) \/ (x2=1 /\ (((exists fs_h_fms_comp_zero. fs_h_fms_comp_zero + S (0) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_zero. x = fs_q_fms_comp_zero * S ((S (i)) * x1) + (0))))
  26. 0026specialize hcode_witness_witness i
  27. 0027specialize hcode_witness_witness x2
  28. 0028apply hcode_witness_witness
  29. 0029exact hi
  30. 0030exact ha_witness
  31. 0031cases hc
  32. 0032cases hc_left
  33. 0033exists 1
  34. 0034split
  35. 0035exact hc_left_right
  36. 0036right
  37. 0037refl
  38. 0038cases hc_right
  39. 0039exists 0
  40. 0040split
  41. 0041exact hc_right_right
  42. 0042left
  43. 0043refl
  44. 0044have hcomp : forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * c)) /\ exists fs_q_fms_complement_a. b = fs_q_fms_complement_a * S ((S (fms_i_complement)) * c) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * x1)) /\ exists fs_q_fms_complement_b. x = fs_q_fms_complement_b * S ((S (fms_i_complement)) * x1) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))
  45. 0045intro i
  46. 0046intro a
  47. 0047intro v
  48. 0048intro hi
  49. 0049intro ha
  50. 0050intro hv
  51. 0051have hc : (a=0 /\ (((exists fs_h_fms_comp_univ_one. fs_h_fms_comp_univ_one + S (1) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_univ_one. x = fs_q_fms_comp_univ_one * S ((S (i)) * x1) + (1)))) \/ (a=1 /\ (((exists fs_h_fms_comp_univ_zero. fs_h_fms_comp_univ_zero + S (0) = S ((S (i)) * x1)) /\ exists fs_q_fms_comp_univ_zero. x = fs_q_fms_comp_univ_zero * S ((S (i)) * x1) + (0))))
  52. 0052specialize hcode_witness_witness i
  53. 0053specialize hcode_witness_witness a
  54. 0054apply hcode_witness_witness
  55. 0055exact hi
  56. 0056exact ha
  57. 0057cases hc
  58. 0058cases hc_left
  59. 0059left
  60. 0060split
  61. 0061exact hc_left_left
  62. 0062specialize beta_at_unique x
  63. 0063specialize beta_at_unique x1
  64. 0064specialize beta_at_unique i
  65. 0065specialize beta_at_unique v
  66. 0066specialize beta_at_unique 1
  67. 0067apply beta_at_unique
  68. 0068exact hv
  69. 0069exact hc_left_right
  70. 0070cases hc_right
  71. 0071right
  72. 0072split
  73. 0073exact hc_right_left
  74. 0074specialize beta_at_unique x
  75. 0075specialize beta_at_unique x1
  76. 0076specialize beta_at_unique i
  77. 0077specialize beta_at_unique v
  78. 0078specialize beta_at_unique 0
  79. 0079apply beta_at_unique
  80. 0080exact hv
  81. 0081exact hc_right_right
  82. 0082have hcount : exists m. ((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (x1))) /\ exists ff_q_fms_count_summand. (x) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (x1)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (x1))) /\ exists ff_q_fms_count_decoded. (x) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (x1)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))
  83. 0083specialize bit_count_exists x
  84. 0084specialize bit_count_exists x1
  85. 0085specialize bit_count_exists l
  86. 0086apply bit_count_exists
  87. 0087exact hbits
  88. 0088cases hcount
  89. 0089exists x
  90. 0090exists x1
  91. 0091exists x2
  92. 0092split
  93. 0093exact hcount_witness
  94. 0094split
  95. 0095exact hcomp
  96. 0096specialize complementary_bit_counts_add_length b
  97. 0097specialize complementary_bit_counts_add_length c
  98. 0098specialize complementary_bit_counts_add_length x
  99. 0099specialize complementary_bit_counts_add_length x1
  100. 0100specialize complementary_bit_counts_add_length l
  101. 0101specialize complementary_bit_counts_add_length n
  102. 0102specialize complementary_bit_counts_add_length x2
  103. 0103apply complementary_bit_counts_add_length
  104. 0104exact hn
  105. 0105exact hcount_witness
  106. 0106exact hcomp