CD0012

finite_bit_intersection_exists

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

Construct an actual characteristic intersection code and its exact finite count.

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 d e l n 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 ((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 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))))) -> exists u v q. (((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 ((q)) = 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) + ((q)))) /\ 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)) * (v))) /\ exists ff_q_fms_count_summand. (u) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (v)) + (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)) * (v))) /\ exists ff_q_fms_count_decoded. (u) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (v)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (l)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) /\ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) /\ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1)))))))

Constructive proof overview

Generated structural guide

Construct an actual characteristic intersection code and its exact finite count.

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

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

Proof neighborhood

Direct dependencies

beta_pointwise_mul_prefix_exists Alpha theorem; checked-use authorized beta_at_exists Stable theorem; checked-use authorized CD0001 finite_bit_entry_cases CD0010 finite_bit_product_cases bit_count_exists Stable theorem; checked-use authorized CD0011 finite_bit_intersection_from_product

Direct dependents

CD0016 finite_bit_union_exists CD0038 finite_modular_dyson_transform_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

98 script commands · 23 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.

Named ingredients (3)
finite bit entry casesfinite bit product casesfinite bit intersection from product

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

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro m
  8. L8
    intro hn
  9. L9
    intro hm
02Establish hcodeL10–16

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

  1. L10
    have hcode : ∃ u. ∃ v. ∀ fms_i_product. ∀ fms_a_product. ∀ fms_z_product. ∀ fms_w_product. Lt(fms_i_product,l) → BetaAt(b,c,fms_i_product,fms_a_product) → BetaAt(d,e,fms_i_product,fms_z_product) → BetaAt(u,v,fms_i_product,fms_w_product) → fms_w_product = fms_a_product · fms_z_productDefinitions: LtBetaAt
  2. L11
    specialize beta_pointwise_mul_prefix_exists b
  3. L12
    specialize beta_pointwise_mul_prefix_exists c
  4. L13
    specialize beta_pointwise_mul_prefix_exists d
  5. L14
    specialize beta_pointwise_mul_prefix_exists e
  6. L15
    specialize beta_pointwise_mul_prefix_exists l
  7. L16
    apply beta_pointwise_mul_prefix_exists
03Separate the logical casesL17–20

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

  1. L17
    cases hcode
  2. L18
    cases hcode_witness
  3. L19
    cases hn
  4. L20
    cases hm
04Establish hbitsL21–23

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

  1. L21
    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. L22
    intro i
  3. L23
    intro hi
05Establish haL24–28

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

  1. L24
    have ha : exists a. ((exists fs_h_fms_inter_exists_a. fs_h_fms_inter_exists_a + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_inter_exists_a. b = fs_q_fms_inter_exists_a * S ((S (i)) * c) + (a))
  2. L25
    specialize beta_at_exists b
  3. L26
    specialize beta_at_exists c
  4. L27
    specialize beta_at_exists i
  5. L28
    apply beta_at_exists
06Separate the logical casesL29–29

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

  1. L29
    cases ha
07Establish hbL30–34

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

  1. L30
    have hb : exists a. ((exists fs_h_fms_inter_exists_b. fs_h_fms_inter_exists_b + S (a) = S ((S (i)) * e)) /\ exists fs_q_fms_inter_exists_b. d = fs_q_fms_inter_exists_b * S ((S (i)) * e) + (a))
  2. L31
    specialize beta_at_exists d
  3. L32
    specialize beta_at_exists e
  4. L33
    specialize beta_at_exists i
  5. L34
    apply beta_at_exists
08Separate the logical casesL35–35

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

  1. L35
    cases hb
09Establish hwL36–40

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

  1. L36
    have hw : exists a. ((exists fs_h_fms_inter_exists_w. fs_h_fms_inter_exists_w + S (a) = S ((S (i)) * x1)) /\ exists fs_q_fms_inter_exists_w. x = fs_q_fms_inter_exists_w * S ((S (i)) * x1) + (a))
  2. L37
    specialize beta_at_exists x
  3. L38
    specialize beta_at_exists x1
  4. L39
    specialize beta_at_exists i
  5. L40
    apply beta_at_exists
10Separate the logical casesL41–41

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

  1. L41
    cases hw
11Establish heL42–51

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

  1. L42
    have he : x4=x2*x3
  2. L43
    specialize hcode_witness_witness i
  3. L44
    specialize hcode_witness_witness x2
  4. L45
    specialize hcode_witness_witness x3
  5. L46
    specialize hcode_witness_witness x4
  6. L47
    apply hcode_witness_witness
  7. L48
    exact hi
  8. L49
    exact ha_witness
  9. L50
    exact hb_witness
  10. L51
    exact hw_witness
12Construct an explicit witnessL52–52

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

  1. L52
    exists x4
13Separate the logical casesL53–53

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

  1. L53
    split
14Use earlier factsL54–54

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

  1. L54
    exact hw_witness
15Calculate and transport equalitiesL55–56

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

  1. L55
    rewrite he
  2. L56
    rewrite he
16Use earlier factsL57–66

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

  1. L57
    specialize finite_bit_product_cases x2
  2. L58
    specialize finite_bit_product_cases x3
  3. L59
    apply finite_bit_product_cases
  4. L60
    specialize finite_bit_entry_cases b
  5. L61
    specialize finite_bit_entry_cases c
  6. L62
    specialize finite_bit_entry_cases l
  7. L63
    specialize finite_bit_entry_cases i
  8. L64
    specialize finite_bit_entry_cases x2
  9. L65
    apply finite_bit_entry_cases
  10. L66
    exact hn_right
17Use earlier factsL67–76

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

  1. L67
    exact hi
  2. L68
    exact ha_witness
  3. L69
    specialize finite_bit_entry_cases d
  4. L70
    specialize finite_bit_entry_cases e
  5. L71
    specialize finite_bit_entry_cases l
  6. L72
    specialize finite_bit_entry_cases i
  7. L73
    specialize finite_bit_entry_cases x3
  8. L74
    apply finite_bit_entry_cases
  9. L75
    exact hm_right
  10. L76
    exact hi
18Use earlier factsL77–77

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

  1. L77
    exact hb_witness
19Establish hcountL78–83

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

  1. L78
    have hcount : ∃ q. BitCount(x,x1,l,q)Definitions: BitCount
  2. L79
    specialize bit_count_exists x
  3. L80
    specialize bit_count_exists x1
  4. L81
    specialize bit_count_exists l
  5. L82
    apply bit_count_exists
  6. L83
    exact hbits
20Separate the logical casesL84–84

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

  1. L84
    cases hcount
21Construct an explicit witnessL85–87

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

  1. L85
    exists x
  2. L86
    exists x1
  3. L87
    exists x2
22Separate the logical casesL88–88

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

  1. L88
    split
23Use earlier factsL89–98

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

  1. L89
    exact hcount_witness
  2. L90
    specialize finite_bit_intersection_from_product b
  3. L91
    specialize finite_bit_intersection_from_product c
  4. L92
    specialize finite_bit_intersection_from_product d
  5. L93
    specialize finite_bit_intersection_from_product e
  6. L94
    specialize finite_bit_intersection_from_product x
  7. L95
    specialize finite_bit_intersection_from_product x1
  8. L96
    specialize finite_bit_intersection_from_product l
  9. L97
    apply finite_bit_intersection_from_product
  10. L98
    exact hcode_witness_witness

Library-wide reading audit

Original exact command ledger · 98 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hn
  9. 0009intro hm
  10. 0010have hcode : exists u v. forall fms_i_product fms_a_product fms_z_product fms_w_product. (exists fms_gap_product. fms_gap_product + S (fms_i_product) = (l)) -> (((exists fs_h_fms_product_a. fs_h_fms_product_a + S (fms_a_product) = S ((S (fms_i_product)) * c)) /\ exists fs_q_fms_product_a. b = fs_q_fms_product_a * S ((S (fms_i_product)) * c) + (fms_a_product))) -> (((exists fs_h_fms_product_b. fs_h_fms_product_b + S (fms_z_product) = S ((S (fms_i_product)) * e)) /\ exists fs_q_fms_product_b. d = fs_q_fms_product_b * S ((S (fms_i_product)) * e) + (fms_z_product))) -> (((exists fs_h_fms_product_w. fs_h_fms_product_w + S (fms_w_product) = S ((S (fms_i_product)) * v)) /\ exists fs_q_fms_product_w. u = fs_q_fms_product_w * S ((S (fms_i_product)) * v) + (fms_w_product))) -> fms_w_product=fms_a_product*fms_z_product
  11. 0011specialize beta_pointwise_mul_prefix_exists b
  12. 0012specialize beta_pointwise_mul_prefix_exists c
  13. 0013specialize beta_pointwise_mul_prefix_exists d
  14. 0014specialize beta_pointwise_mul_prefix_exists e
  15. 0015specialize beta_pointwise_mul_prefix_exists l
  16. 0016apply beta_pointwise_mul_prefix_exists
  17. 0017cases hcode
  18. 0018cases hcode_witness
  19. 0019cases hn
  20. 0020cases hm
  21. 0021have 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))
  22. 0022intro i
  23. 0023intro hi
  24. 0024have ha : exists a. ((exists fs_h_fms_inter_exists_a. fs_h_fms_inter_exists_a + S (a) = S ((S (i)) * c)) /\ exists fs_q_fms_inter_exists_a. b = fs_q_fms_inter_exists_a * S ((S (i)) * c) + (a))
  25. 0025specialize beta_at_exists b
  26. 0026specialize beta_at_exists c
  27. 0027specialize beta_at_exists i
  28. 0028apply beta_at_exists
  29. 0029cases ha
  30. 0030have hb : exists a. ((exists fs_h_fms_inter_exists_b. fs_h_fms_inter_exists_b + S (a) = S ((S (i)) * e)) /\ exists fs_q_fms_inter_exists_b. d = fs_q_fms_inter_exists_b * S ((S (i)) * e) + (a))
  31. 0031specialize beta_at_exists d
  32. 0032specialize beta_at_exists e
  33. 0033specialize beta_at_exists i
  34. 0034apply beta_at_exists
  35. 0035cases hb
  36. 0036have hw : exists a. ((exists fs_h_fms_inter_exists_w. fs_h_fms_inter_exists_w + S (a) = S ((S (i)) * x1)) /\ exists fs_q_fms_inter_exists_w. x = fs_q_fms_inter_exists_w * S ((S (i)) * x1) + (a))
  37. 0037specialize beta_at_exists x
  38. 0038specialize beta_at_exists x1
  39. 0039specialize beta_at_exists i
  40. 0040apply beta_at_exists
  41. 0041cases hw
  42. 0042have he : x4=x2*x3
  43. 0043specialize hcode_witness_witness i
  44. 0044specialize hcode_witness_witness x2
  45. 0045specialize hcode_witness_witness x3
  46. 0046specialize hcode_witness_witness x4
  47. 0047apply hcode_witness_witness
  48. 0048exact hi
  49. 0049exact ha_witness
  50. 0050exact hb_witness
  51. 0051exact hw_witness
  52. 0052exists x4
  53. 0053split
  54. 0054exact hw_witness
  55. 0055rewrite he
  56. 0056rewrite he
  57. 0057specialize finite_bit_product_cases x2
  58. 0058specialize finite_bit_product_cases x3
  59. 0059apply finite_bit_product_cases
  60. 0060specialize finite_bit_entry_cases b
  61. 0061specialize finite_bit_entry_cases c
  62. 0062specialize finite_bit_entry_cases l
  63. 0063specialize finite_bit_entry_cases i
  64. 0064specialize finite_bit_entry_cases x2
  65. 0065apply finite_bit_entry_cases
  66. 0066exact hn_right
  67. 0067exact hi
  68. 0068exact ha_witness
  69. 0069specialize finite_bit_entry_cases d
  70. 0070specialize finite_bit_entry_cases e
  71. 0071specialize finite_bit_entry_cases l
  72. 0072specialize finite_bit_entry_cases i
  73. 0073specialize finite_bit_entry_cases x3
  74. 0074apply finite_bit_entry_cases
  75. 0075exact hm_right
  76. 0076exact hi
  77. 0077exact hb_witness
  78. 0078have hcount : exists q. ((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 ((q)) = 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) + ((q)))) /\ 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))))
  79. 0079specialize bit_count_exists x
  80. 0080specialize bit_count_exists x1
  81. 0081specialize bit_count_exists l
  82. 0082apply bit_count_exists
  83. 0083exact hbits
  84. 0084cases hcount
  85. 0085exists x
  86. 0086exists x1
  87. 0087exists x2
  88. 0088split
  89. 0089exact hcount_witness
  90. 0090specialize finite_bit_intersection_from_product b
  91. 0091specialize finite_bit_intersection_from_product c
  92. 0092specialize finite_bit_intersection_from_product d
  93. 0093specialize finite_bit_intersection_from_product e
  94. 0094specialize finite_bit_intersection_from_product x
  95. 0095specialize finite_bit_intersection_from_product x1
  96. 0096specialize finite_bit_intersection_from_product l
  97. 0097apply finite_bit_intersection_from_product
  98. 0098exact hcode_witness_witness